% % typeof+sub E A : (Non-elaboration) source typing, including subsumption rule (typeof+sub/sub) % typeof+sub : exp -> ty -> type. %name typeof+sub _Type. % % sub A B Coe CoeTyping Subtyping: A is a subtype of B, % with source coercion x : A |- (Coe x) : B % sub : {A : ty} {B : ty} {Coe : exp -> exp} {CoeTyping : {e:exp} typeof e A -> typeof (Coe e) B} type. %name sub _Sub. %mode sub +A +B -Coe -CoeTyping. % Top typeof+sub/topintro : is-value V -> typeof+sub V topty. % Intersection typeof+sub/sectintro : typeof+sub E A1 -> typeof+sub E A2 -> typeof+sub E (sectty A1 A2). typeof+sub/sectelim1 : typeof+sub E (sectty A1 A2) -> typeof+sub E A1. typeof+sub/sectelim2 : typeof+sub E (sectty A1 A2) -> typeof+sub E A2. % Merge typeof+sub/merge1 : typeof+sub E1 A -> typeof+sub (merge E1 E2) A. typeof+sub/merge2 : typeof+sub E2 A -> typeof+sub (merge E1 E2) A. % Unions typeof+sub/unintro1 : typeof+sub E A1 -> typeof+sub E (unty A1 A2). typeof+sub/unintro2 : typeof+sub E A2 -> typeof+sub E (unty A1 A2). typeof+sub/unelim : fill EC EH -> typeof+sub E' (unty A1 A2) -> ({x1 : exp} typeof+sub x1 A1 -> typeof+sub (EH x1) C) -> ({x2 : exp} typeof+sub x2 A2 -> typeof+sub (EH x2) C) -> typeof+sub (EH E') C. % direct typeof+sub/direct : fill EC EH -> typeof+sub E' A1 -> ({x1 : exp} typeof+sub x1 A1 -> typeof+sub (EH x1) C) -> typeof+sub (EH E') C. % Arrow typeof+sub/arrintro : ({x : exp} typeof+sub x Adom -> typeof+sub (Ebody x) Acod) -> typeof+sub (lam ([x] Ebody x)) (arr Adom Acod). typeof+sub/arrelim : typeof+sub E1 (arr Adom Acod) -> typeof+sub E2 Adom -> typeof+sub (app E1 E2) Acod. % fix typeof+sub/fix : ({u : exp} typeof+sub u A -> typeof+sub (Ebody u) A) -> typeof+sub (fix ([u] Ebody u)) A. % Subsumption typeof+sub/sub : {Coe} {CoeTyping} typeof+sub E A -> sub A B Coe CoeTyping -> typeof+sub E B. % unit-sub/refl: sub unitty unitty. % sub/refl : sub A A ([e] e) ([e] [D] D). % % Subtyping rules % % These are rather verbose because they carry along a complete typing derivation % (in the subsumption-free typeof.elf system) for the coercion. sub/arr: %{ {B1:ty} {A1:ty} {Arg : exp -> exp} {DArg : {e':exp} typeof e' B1 -> typeof (Arg e') A1} {A2:ty} {B2:ty} {Res:exp -> exp} {DRes : {e:exp} typeof e A2 -> typeof (Res e) B2} }% sub B1 A1 Arg DArg -> sub A2 B2 Res DRes -> sub (arr A1 A2) (arr B1 B2) ([f : exp] lam ([e'] Res (app f (Arg e')))) ([f : exp] [Dfun : typeof f (arr A1 A2)] typeof/arrintro ([e' : exp] [TyArg : typeof e' B1] DRes (app f (Arg e')) (typeof/arrelim Dfun (DArg e' TyArg)))). sub/sect-left-1: sub A1 B Coe CoeTyping -> sub (sectty A1 A2) B Coe ([x] [Dx] CoeTyping x (typeof/sectelim1 Dx)). sub/sect-left-2: sub A2 B Coe CoeTyping -> sub (sectty A1 A2) B Coe ([x] [Dx] CoeTyping x (typeof/sectelim2 Dx)). sub/sect-right: sub A B1 Coe1 CoeTyping1 -> sub A B2 Coe2 CoeTyping2 -> sub A (sectty B1 B2) ([e] merge (Coe1 e) (Coe2 e)) ([x] [Dx] typeof/sectintro (typeof/merge1 (CoeTyping1 x Dx)) (typeof/merge2 (CoeTyping2 x Dx))). sub/top-right : sub A topty ([e] unit) ([e] [D] typeof/topintro is-value/unit). sub/top = sub/top-right. sub/union-right-1 : sub A B1 Coe CoeTyping -> sub A (unty B1 B2) Coe ([x] [Dx] typeof/unintro1 (CoeTyping x Dx)). sub/union-right-2 : sub A B2 Coe CoeTyping -> sub A (unty B1 B2) Coe ([x] [Dx] typeof/unintro2 (CoeTyping x Dx)). sub/union-left : sub A1 B Coe1 CoeTyping1 -> sub A2 B Coe2 CoeTyping2 -> sub (unty A1 A2) B ([e] app (lam ([y] (merge (Coe1 y) (Coe2 y)))) e) ([x] [Dx] typeof/unelim (ec/app2 (lam ([e] (merge (Coe1 e) (Coe2 e)))) (is-value/lam) (ec/hole)) (fill/app2 (fill/hole)) Dx ([x1] [Dx1] typeof/arrelim (typeof/arrintro ([y] [Dy] typeof/merge1 (CoeTyping1 y Dy))) Dx1) ([x2] [Dx2] typeof/arrelim (typeof/arrintro ([y] [Dy] typeof/merge2 (CoeTyping2 y Dy))) Dx2)). %freeze sub.