%%% Stine Søndergaard %%% DIKU, summer 2006 %%% Coercion semantics for subtyping % --- % --- record labels :: syntax % --- lab : type. %name lab L. lab_0 : lab. lab_n : lab -> lab. % --- % --- record labels :: non-equality % --- neq_lab : lab -> lab -> type. %name neq_lab NELP. neq_lab_0n : neq_lab lab_0 (lab_n L). neq_lab_n0 : neq_lab (lab_n L) lab_0. neq_lab_nn : neq_lab (lab_n L) (lab_n L') <- neq_lab L L'. % --- % --- record labels :: equality of non-equality proofs % --- eq_neq_lab : neq_lab L L' -> neq_lab L L' -> type. %name eq_neq_lab ENELP. eq_neq_lab_r : eq_neq_lab NELP NELP. eq_neq_lab_ext : eq_neq_lab NELP NELP' -> eq_neq_lab (neq_lab_nn NELP) (neq_lab_nn NELP') -> type. %mode eq_neq_lab_ext +ENELP -ENELP'. eq_neq_lab_ext_r : eq_neq_lab_ext eq_neq_lab_r eq_neq_lab_r. %worlds () (eq_neq_lab_ext _ _). %total {} (eq_neq_lab_ext _ _). % --- % --- record labels :: uniqueness of non-equality proving % --- neq_lab_unq : {NELP : neq_lab L L'} {NELP' : neq_lab L L'} eq_neq_lab NELP NELP' -> type. %mode neq_lab_unq +NELP +NELP' -ENELP. neq_lab_unq_0n : neq_lab_unq neq_lab_0n neq_lab_0n eq_neq_lab_r. neq_lab_unq_n0 : neq_lab_unq neq_lab_n0 neq_lab_n0 eq_neq_lab_r. neq_lab_unq_nn : neq_lab_unq (neq_lab_nn NELP) (neq_lab_nn NELP') ENELP' <- neq_lab_unq NELP NELP' ENELP <- eq_neq_lab_ext ENELP ENELP'. %worlds () (neq_lab_unq _ _ _). %total NELP (neq_lab_unq NELP _ _). % --- % --- terms :: syntax % --- % source s_exp : type. %name s_exp ES. s_rexp : type. %name s_rexp RES. s_lam : (s_exp -> s_exp) -> s_exp. s_app : s_exp -> s_exp -> s_exp. s_proj : s_exp -> lab -> s_exp. s_record : s_rexp -> s_exp. s_rcd_empty : s_rexp. s_rcd_ext : lab -> s_exp -> s_rexp -> s_rexp. % target t_exp : type. %name t_exp ET. t_rexp : type. %name t_rexp RET. t_unit : t_exp. t_lam : (t_exp -> t_exp) -> t_exp. t_app : t_exp -> t_exp -> t_exp. t_proj : t_exp -> lab -> t_exp. t_record : t_rexp -> t_exp. t_rcd_empty : t_rexp. t_rcd_ext : lab -> t_exp -> t_rexp -> t_rexp. % --- % --- types :: syntax % --- % source s_tp : type. %name s_tp TS. s_rtp : type. %name s_rtp RTS. s_top : s_tp. s_arrow : s_tp -> s_tp -> s_tp. s_valid_labs : s_rtp -> type. %name s_valid_labs VLPS. s_record_type : {RTS} s_valid_labs RTS -> s_tp. s_rcdt_empty : s_rtp. s_rcdt_ext : lab -> s_tp -> s_rtp -> s_rtp. % target t_tp : type. %name t_tp TT. t_rtp : type. %name t_rtp RTT. t_unit_type : t_tp. t_arrow : t_tp -> t_tp -> t_tp. t_valid_labs : t_rtp -> type. %name t_valid_labs VLPT. t_record_type : {RTT} t_valid_labs RTT -> t_tp. t_rcdt_empty : t_rtp. t_rcdt_ext : lab -> t_tp -> t_rtp -> t_rtp. % --- % --- record labels :: is label l fresh or is it already present in the % --- given record? % --- % source s_fresh_lab : s_rtp -> lab -> type. %name s_fresh_lab FLPS. s_fresh_lab_empty : s_fresh_lab s_rcdt_empty L'. s_fresh_lab_ext : s_fresh_lab (s_rcdt_ext L TS RTS) L' <- neq_lab L L' <- s_fresh_lab RTS L'. % target t_fresh_lab : t_rtp -> lab -> type. %name t_fresh_lab FLPT. t_fresh_lab_empty : t_fresh_lab t_rcdt_empty L'. t_fresh_lab_ext : t_fresh_lab (t_rcdt_ext L TT RTT) L' <- neq_lab L L' <- t_fresh_lab RTT L'. % --- % --- record labels :: are all labels different in the given record? % --- % source s_valid_labs_empty : s_valid_labs s_rcdt_empty. s_valid_labs_ext : s_valid_labs (s_rcdt_ext L TS RTS) <- s_fresh_lab RTS L <- s_valid_labs RTS. % target t_valid_labs_empty : t_valid_labs t_rcdt_empty. t_valid_labs_ext : t_valid_labs (t_rcdt_ext L TT RTT) <- t_fresh_lab RTT L <- t_valid_labs RTT. % --- % --- record labels :: equality of "fresh label" proofs % --- eq_fresh_lab : t_fresh_lab RTT L -> t_fresh_lab RTT' L -> type. %name eq_fresh_lab EFLP. eq_fresh_lab_r : eq_fresh_lab FLPT FLPT. eq_fresh_lab_ext : {TT} eq_neq_lab NELP NELP' -> eq_fresh_lab FLPT FLPT' -> eq_fresh_lab ((t_fresh_lab_ext FLPT NELP) : t_fresh_lab (t_rcdt_ext L' TT RTT) L) ((t_fresh_lab_ext FLPT' NELP') : t_fresh_lab (t_rcdt_ext L' TT RTT) L) -> type. %mode eq_fresh_lab_ext +TT +ENELP +EFLP -EFLP'. eq_fresh_lab_ext_r : eq_fresh_lab_ext T eq_neq_lab_r eq_fresh_lab_r eq_fresh_lab_r. %worlds () (eq_fresh_lab_ext _ _ _ _). %total {} (eq_fresh_lab_ext _ _ _ _). % --- % --- record labels :: equality of "all different labels" proofs % --- eq_valid_labs : t_valid_labs RTT -> t_valid_labs RTT' -> type. %name eq_valid_labs EVLP. eq_valid_labs_r : eq_valid_labs VLPT VLPT. eq_valid_labs_ext : {TT} eq_fresh_lab (FLPT : t_fresh_lab RTT L) (FLPT' : t_fresh_lab RTT L) -> eq_valid_labs (VLPT : t_valid_labs RTT) (VLPT' : t_valid_labs RTT) -> eq_valid_labs ((t_valid_labs_ext VLPT FLPT) : t_valid_labs (t_rcdt_ext L TT RTT)) ((t_valid_labs_ext VLPT' FLPT') : t_valid_labs (t_rcdt_ext L TT RTT)) -> type. %mode eq_valid_labs_ext +TT +EFLP +EVLP -EVLP'. eq_valid_labs_ext_r : eq_valid_labs_ext TT eq_fresh_lab_r eq_valid_labs_r eq_valid_labs_r. %worlds () (eq_valid_labs_ext _ _ _ _). %total {} (eq_valid_labs_ext _ _ _ _). % --- % --- types :: equality % --- eq_type : t_tp -> t_tp -> type. %name eq_type ETP. eq_type_r : eq_type TT TT. eq_rtype : t_rtp -> t_rtp -> type. %name eq_rtype ERTP. eq_rtype_r : eq_rtype RTT RTT. eq_type_arrow : eq_type TT1 TT1' -> eq_type TT2 TT2' -> eq_type (t_arrow TT1 TT2) (t_arrow TT1' TT2') -> type. %mode eq_type_arrow +ETP1 +ETP2 -ETP. eq_type_arrow_r : eq_type_arrow eq_type_r eq_type_r eq_type_r. %worlds () (eq_type_arrow _ _ _). %total {} (eq_type_arrow _ _ _). eq_rtype_ext : eq_type TT TT' -> eq_rtype RTT RTT' -> eq_rtype (t_rcdt_ext L TT RTT) (t_rcdt_ext L TT' RTT') -> type. %mode +{TT} +{TT'} +{RTT} +{RTT'} +{L} +{ETP : eq_type TT TT'} +{ERTP : eq_rtype RTT RTT'} -{ERTP' : eq_rtype (t_rcdt_ext L TT RTT) (t_rcdt_ext L TT' RTT')} eq_rtype_ext ETP ERTP ERTP'. eq_rtype_ext_r : eq_rtype_ext eq_type_r eq_rtype_r eq_rtype_r. %worlds () (eq_rtype_ext _ _ _). %total {} (eq_rtype_ext _ _ _). eq_type_record : eq_rtype RTT RTT' -> eq_valid_labs (VLPT : t_valid_labs RTT) (VLPT': t_valid_labs RTT') -> eq_type (t_record_type RTT VLPT) (t_record_type RTT' VLPT') -> type. %mode eq_type_record +ERTP +EVLP -ETP. eq_type_record_r : eq_type_record eq_rtype_r eq_valid_labs_r eq_type_r. %worlds () (eq_type_record _ _ _). %total {} (eq_type_record _ _ _). % --- % --- record labels :: uniqueness of "fresh label" proving % --- fresh_lab_unq : {RTT} {FLPT : t_fresh_lab RTT L} {FLPT' : t_fresh_lab RTT L} eq_fresh_lab FLPT FLPT' -> type. %mode fresh_lab_unq +RTT +FLPT +FLPT' -EFLP. fresh_lab_unq_empty : fresh_lab_unq t_rcdt_empty t_fresh_lab_empty t_fresh_lab_empty eq_fresh_lab_r. fresh_lab_unq_ext : fresh_lab_unq (t_rcdt_ext L TT RTT) (t_fresh_lab_ext FLPT NELP) (t_fresh_lab_ext FLPT' NELP') EFLP' <- fresh_lab_unq RTT FLPT FLPT' EFLP <- neq_lab_unq NELP NELP' ENELP <- eq_fresh_lab_ext TT ENELP EFLP EFLP'. %worlds () (fresh_lab_unq _ _ _ _). %total FLPT (fresh_lab_unq _ FLPT _ _). fresh_lab_unq' : eq_rtype RTT RTT' -> {FLPT : t_fresh_lab RTT L} {FLPT' : t_fresh_lab RTT' L} eq_fresh_lab FLPT FLPT' -> type. %mode fresh_lab_unq' +ERTP +FLPT +FLPT' -EFLP. fresh_lab_unq'_r : fresh_lab_unq' (eq_rtype_r : eq_rtype RTT RTT) FLPT FLPT' EFLP <- fresh_lab_unq RTT FLPT FLPT' EFLP. %worlds () (fresh_lab_unq' _ _ _ _). %total FLPT (fresh_lab_unq' _ FLPT _ _). % --- % --- record labels :: uniqueness of "all different labels" proving % --- valid_labs_unq : {RTT} {VLPT : t_valid_labs RTT} {VLPT' : t_valid_labs RTT} eq_valid_labs VLPT VLPT' -> type. %mode valid_labs_unq +RTT +VLPT +VLPT' -EVLP. valid_labs_unq_empty : valid_labs_unq t_rcdt_empty t_valid_labs_empty t_valid_labs_empty eq_valid_labs_r. valid_labs_unq_ext : valid_labs_unq (t_rcdt_ext L TT RTT) (t_valid_labs_ext VLPT FLPT) (t_valid_labs_ext VLPT' FLPT') EVLP' <- valid_labs_unq RTT VLPT VLPT' EVLP <- fresh_lab_unq RTT FLPT FLPT' EFLP <- eq_valid_labs_ext TT EFLP EVLP EVLP'. %worlds () (valid_labs_unq _ _ _ _). %total VLPT (valid_labs_unq _ VLPT _ _). valid_labs_unq' : eq_rtype RTT RTT' -> {VLPT : t_valid_labs RTT} {VLPT' : t_valid_labs RTT'} eq_valid_labs VLPT VLPT' -> type. %mode valid_labs_unq' +ERTP +VLPT +VLPT' -EVLP. valid_labs_unq'_r : valid_labs_unq' (eq_rtype_r : eq_rtype RTT RTT) VLPT VLPT' EVLP <- valid_labs_unq RTT VLPT VLPT' EVLP. %worlds () (valid_labs_unq' _ _ _ _). %total VLPT (valid_labs_unq' _ VLPT _ _). % --- % --- types :: translation of a source type into a target type % --- trans_type : s_tp -> t_tp -> type. %name trans_type TTP. trans_rtype : s_rtp -> t_rtp -> type. %name trans_rtype TRTP. trans_type_top : trans_type s_top t_unit_type. trans_type_arrow : trans_type (s_arrow TS1 TS2) (t_arrow TT1 TT2) <- trans_type TS1 TT1 <- trans_type TS2 TT2. trans_rtype_empty : trans_rtype s_rcdt_empty t_rcdt_empty. trans_rtype_ext : trans_rtype (s_rcdt_ext L TS RTS) (t_rcdt_ext L TT RTT) <- trans_type TS TT <- trans_rtype RTS RTT. trans_type_record : {VLPT} trans_type (s_record_type RTS VLPS) (t_record_type RTT VLPT) <- trans_rtype RTS RTT. % --- % --- record labels :: translation of "fresh label" proof for source record % --- into "fresh label" proof for translated record % --- trans_fresh_lab : trans_rtype RTS RTT -> s_fresh_lab RTS L -> t_fresh_lab RTT L -> type. %mode trans_fresh_lab +TRTP +FLPS -FLPT. trans_fresh_lab_empty : trans_fresh_lab trans_rtype_empty s_fresh_lab_empty t_fresh_lab_empty. trans_fresh_lab_ext : trans_fresh_lab (trans_rtype_ext TRTP TTP) (s_fresh_lab_ext FLPS NELP) (t_fresh_lab_ext FLPT NELP) <- trans_fresh_lab TRTP FLPS FLPT. %worlds () (trans_fresh_lab _ _ _). %total TRTP (trans_fresh_lab TRTP _ _). % --- % --- record labels :: translation of "all different labels" proof for source % --- record into "all different labels" proof for translated % --- record % --- trans_valid_labs : trans_rtype RTS RTT -> s_valid_labs RTS -> t_valid_labs RTT -> type. %mode trans_valid_labs +TRTP +VLPS -VLPT. trans_valid_labs_empty: trans_valid_labs trans_rtype_empty s_valid_labs_empty t_valid_labs_empty. trans_valid_labs_ext : trans_valid_labs (trans_rtype_ext TRTP TTP) (s_valid_labs_ext VLPS FLPS) (t_valid_labs_ext VLPT FLPT) <- trans_valid_labs TRTP VLPS VLPT <- trans_fresh_lab TRTP FLPS FLPT. %worlds () (trans_valid_labs _ _ _). %total TRTP (trans_valid_labs TRTP _ _). % --- % --- types :: existence property of type translation % --- trans_type_exists : {TS} (trans_type TS TT) -> type. %mode trans_type_exists +TS -TTP. trans_rtype_exists : {RTS} (trans_rtype RTS RTT) -> type. %mode trans_rtype_exists +RTS -TRTP. trans_type_exists_top : trans_type_exists s_top trans_type_top. trans_type_exists_arrow : trans_type_exists (s_arrow TS1 TS2) (trans_type_arrow TTP2 TTP1) <- trans_type_exists TS1 TTP1 <- trans_type_exists TS2 TTP2. trans_rtype_exists_empty : trans_rtype_exists s_rcdt_empty trans_rtype_empty. trans_rtype_exists_ext : trans_rtype_exists (s_rcdt_ext L TS RTS) (trans_rtype_ext TRTP TTP) <- trans_type_exists TS TTP <- trans_rtype_exists RTS TRTP. trans_type_exists_record : trans_type_exists (s_record_type RTS VLPS) (trans_type_record VLPT TRTP) <- trans_rtype_exists RTS TRTP <- trans_valid_labs TRTP VLPS VLPT. %worlds () (trans_type_exists _ _) (trans_rtype_exists _ _). %total (TS RTS) (trans_type_exists TS _) (trans_rtype_exists RTS _). % --- % --- types :: uniqueness property of type translation % --- trans_type_unq : {TS} (trans_type TS TT) -> (trans_type TS TT') -> (eq_type TT TT') -> type. %mode trans_type_unq +TS +TTP +TTP' -ETP. trans_rtype_unq : {RTS} (trans_rtype RTS RTT) -> (trans_rtype RTS RTT') -> (eq_rtype RTT RTT') -> type. %mode trans_rtype_unq +RTS +TRTP +TRTP' -ERTP. trans_type_unq_top : trans_type_unq s_top trans_type_top trans_type_top eq_type_r. trans_type_unq_arrow : trans_type_unq (s_arrow TS1 TS2) (trans_type_arrow TTP2 TTP1) (trans_type_arrow TTP2' TTP1') ETP <- trans_type_unq TS1 TTP1 TTP1' ETP1 <- trans_type_unq TS2 TTP2 TTP2' ETP2 <- eq_type_arrow ETP1 ETP2 ETP. trans_rtype_unq_empty : trans_rtype_unq s_rcdt_empty trans_rtype_empty trans_rtype_empty eq_rtype_r. trans_rtype_unq_ext : trans_rtype_unq (s_rcdt_ext L TS RTS) (trans_rtype_ext TRTP TTP) (trans_rtype_ext TRTP' TTP') ERTP' <- trans_type_unq TS TTP TTP' ETP <- trans_rtype_unq RTS TRTP TRTP' ERTP <- eq_rtype_ext ETP ERTP ERTP'. trans_type_unq_record : trans_type_unq (s_record_type RTS VLPS) (trans_type_record VLPT TRTP) (trans_type_record VLPT' TRTP') ETP <- trans_rtype_unq RTS TRTP TRTP' ERTP <- valid_labs_unq' ERTP VLPT VLPT' EVLP <- eq_type_record ERTP EVLP ETP. %worlds () (trans_type_unq _ _ _ _) (trans_rtype_unq _ _ _ _). %total (TS RTS) (trans_type_unq TS _ _ _) (trans_rtype_unq RTS _ _ _). % --- % --- record labels :: is l:t a member of the given record? % --- % source s_member_lab : lab -> s_tp -> s_rtp -> type. %name s_member_lab MLPS. %mode s_member_lab +L +TS +RTS'. s_member_lab_front : s_member_lab L TS (s_rcdt_ext L TS RTS). s_member_lab_inner : s_member_lab L TS (s_rcdt_ext L' TS' RTS') <- s_member_lab L TS RTS'. % target t_member_lab : lab -> t_tp -> t_rtp -> type. %name t_member_lab MLPT. %mode t_member_lab +L +TT +RTT'. t_member_lab_front : t_member_lab L TT (t_rcdt_ext L TT RTT). t_member_lab_inner : t_member_lab L TT (t_rcdt_ext L' TT' RTT') <- t_member_lab L TT RTT'. % --- % --- record labels :: equality of "member label" proofs % --- eq_member_lab : eq_type TT TT' -> t_member_lab L TT RTT -> t_member_lab L TT' RTT -> type. %mode eq_member_lab +ETP +MLPT -MLPT'. eq_member_lab_r : eq_member_lab eq_type_r MLPT MLPT. %worlds () (eq_member_lab _ _ _). %total {} (eq_member_lab _ _ _). % --- % --- types :: subtyping % --- sub : s_tp -> s_tp -> type. %name sub SP. rsub : s_rtp -> s_rtp -> type. %name rsub RSP. sub_top : sub TS s_top. sub_refl : sub TS TS. sub_arrow : sub (s_arrow TS1 TS2) (s_arrow TS1' TS2') <- sub TS1' TS1 <- sub TS2 TS2'. rsub_empty : rsub RTS s_rcdt_empty. rsub_ext : rsub RTS (s_rcdt_ext L TS RTS') <- s_member_lab L TS' RTS <- sub TS' TS <- rsub RTS RTS'. sub_record : sub (s_record_type RTS VLPS) (s_record_type RTS' VLPS') <- rsub RTS RTS'. sub_trans : sub TS1 TS2 <- sub TS1 TS <- sub TS TS2. % --- % --- types :: translation of a subtyping derivation into a function of the % --- target language % --- trans_sub : sub TS1 TS2 -> (t_exp -> t_exp) -> type. %name trans_sub TSP. %mode trans_sub +SP -C. trans_rsub : rsub RTS1 RTS2 -> (t_exp -> t_rexp) -> type. %name trans_rsub TRSP. %mode trans_rsub +RSP -RC. trans_sub_refl : trans_sub sub_refl ([y] y). trans_sub_top : trans_sub sub_top ([y] t_unit). trans_sub_trans : trans_sub (sub_trans SP2 SP1) ([y] (C2 (C1 y))) <- trans_sub SP1 C1 <- trans_sub SP2 C2. trans_sub_arrow : trans_sub (sub_arrow SP2 SP1) ([f] (t_lam ([y] (C2 (t_app f (C1 y)))))) <- trans_sub SP1 C1 <- trans_sub SP2 C2. trans_rsub_empty : trans_rsub rsub_empty ([r] t_rcd_empty). trans_rsub_ext : trans_rsub (rsub_ext RSP SP (MLPS : s_member_lab L _ _)) ([r] (t_rcd_ext L (C (t_proj r L)) (RC r))) <- trans_sub SP C <- trans_rsub RSP RC. trans_sub_record : trans_sub (sub_record RSP) ([r] (t_record (RC r))) <- trans_rsub RSP RC. % --- % --- terms :: typing % --- % source s_of : s_exp -> s_tp -> type. %name s_of OPS. s_rof : s_rexp -> s_rtp -> type. %name s_rof ROPS. s_of_lam : s_of (s_lam [x] ES x) (s_arrow TS TS') <- {x} s_of x TS -> s_of (ES x) TS'. s_of_app : s_of (s_app ES1 ES2) TS' <- s_of ES1 (s_arrow TS TS') <- s_of ES2 TS. s_of_proj : s_of (s_proj ES L) TS <- s_of ES (s_record_type RTS VLPS) <- s_member_lab L TS RTS. s_of_record : s_of (s_record RES) (s_record_type RTS VLPS) <- s_rof RES RTS. s_rof_empty : s_rof s_rcd_empty s_rcdt_empty. s_rof_ext : s_rof (s_rcd_ext L ES RES) (s_rcdt_ext L TS RTS) <- s_of ES TS <- s_rof RES RTS. s_of_sub : s_of ES TS <- s_of ES TS' <- sub TS' TS. % target t_of : t_exp -> t_tp -> type. %name t_of OPT. t_rof : t_rexp -> t_rtp -> type. %name t_rof ROPT. t_of_unit : t_of t_unit t_unit_type. t_of_lam : t_of (t_lam [y] ET y) (t_arrow TT TT') <- {y:t_exp} t_of y TT -> t_of (ET y) TT'. t_of_app : t_of (t_app ET1 ET2) TT' <- t_of ET1 (t_arrow TT TT') <- t_of ET2 TT. t_of_proj : t_of (t_proj ET L) TT <- t_of ET (t_record_type RTT VLPT) <- t_member_lab L TT RTT. t_of_record : t_of (t_record RET) (t_record_type RTT VLPT) <- t_rof RET RTT. t_rof_empty : t_rof t_rcd_empty t_rcdt_empty. t_rof_ext : t_rof (t_rcd_ext L ET RET) (t_rcdt_ext L TT RTT) <- t_of ET TT <- t_rof RET RTT. % --- % --- terms :: equality of typings % --- eq_of : eq_type TT TT' -> t_of ET TT -> t_of ET TT' -> type. %mode eq_of +ETP +OPT -OPT'. eq_of_r : eq_of eq_type_r OPT OPT. eq_of2 : eq_type TT1 TT1' -> eq_type TT2 TT2' -> ({y} t_of y TT1 -> t_of (ET y) TT2) -> ({y} t_of y TT1' -> t_of (ET y) TT2') -> type. %mode eq_of2 +ETP +ETP' +OPT -OPT'. eq_of2_r : eq_of2 eq_type_r eq_type_r OPT OPT. % --- % --- record labels :: translation of "member label" proof for source record % --- into "member label" proof for translated record % --- trans_member_lab : trans_rtype RTS RTT -> s_member_lab L TS RTS -> t_member_lab L TT RTT -> trans_type TS TT -> type. %mode trans_member_lab +TRTP +MLPS -MLPT -TTP. trans_member_lab_front : trans_member_lab (trans_rtype_ext TRTP TTP) s_member_lab_front t_member_lab_front TTP. trans_member_lab_inner : trans_member_lab (trans_rtype_ext TRTP TTP') (s_member_lab_inner MLPS) (t_member_lab_inner MLPT) TTP <- trans_member_lab TRTP MLPS MLPT TTP. %worlds () (trans_member_lab _ _ _ _). %total MLPS (trans_member_lab _ MLPS _ _). % --- % --- lemma 15.6.1: % --- C :: ts1 <: ts2 % --- % --- ts1 ~> tt1 % --- ts2 ~> tt2 % --- % --- => y : tt1 |- [C] y : tt2 % --- lemma-15-6-1 : (trans_sub (SP : sub TS1 TS2) C) -> (trans_type TS1 TT1) -> (trans_type TS2 TT2) -> ({y} t_of y TT1 -> t_of (C y) TT2) -> type. %mode lemma-15-6-1 +TSP +TTP1 +TTP2 -OPT. lemma-15-6-1-r : {VLPT1} (trans_rsub (RSP : rsub RTS1 RTS2) RC) -> (trans_rtype RTS1 RTT1) -> (trans_rtype RTS2 RTT2) -> ({y} t_of y (t_record_type RTT1 VLPT1) -> t_rof (RC y) RTT2) -> type. %mode lemma-15-6-1-r +VLPT1 +TRSP +TRTP1 +TRTP2 -OPT. lemma-15-6-1_refl : lemma-15-6-1 trans_sub_refl TTP TTP' OPT <- trans_type_unq TS TTP TTP' ETP <- eq_of2 eq_type_r ETP ([y][opy]opy) OPT. lemma-15-6-1_top : lemma-15-6-1 trans_sub_top TTP trans_type_top ([y][opy] t_of_unit). lemma-15-6-1_trans : lemma-15-6-1 (trans_sub_trans (TSP2 : trans_sub (SP2 : sub TS3 TS2) C2) (TSP1 : trans_sub (SP1 : sub TS1 TS3) C1)) TTP1 TTP2 ([y][opy] (OPT2 (C1 y) (OPT1 y opy))) <- trans_type_exists TS3 TTP3 <- lemma-15-6-1 TSP1 TTP1 TTP3 OPT1 <- lemma-15-6-1 TSP2 TTP3 TTP2 OPT2. lemma-15-6-1_arrow : lemma-15-6-1 (trans_sub_arrow (TSP2 : trans_sub (SP2 : sub TS2 TS2') C2) (TSP1 : trans_sub (SP1 : sub TS1' TS1) C1)) (trans_type_arrow TTP2 TTP1) (trans_type_arrow TTP2' TTP1') ([f][opf] (t_of_lam ([y][opy] (OPT2 (t_app f (C1 y)) (t_of_app (OPT1 y opy) opf))))) <- lemma-15-6-1 TSP1 TTP1' TTP1 OPT1 <- lemma-15-6-1 TSP2 TTP2 TTP2' OPT2. lemma-15-6-1_record : lemma-15-6-1 (trans_sub_record TRSP) (trans_type_record VLPT1 TRTP1) (trans_type_record VLPT2 TRTP2) ([y][opy] (t_of_record (OPT y opy))) <- lemma-15-6-1-r VLPT1 TRSP TRTP1 TRTP2 OPT. lemma-15-6-1-r_empty : lemma-15-6-1-r VLPT trans_rsub_empty TRTP trans_rtype_empty ([y][opy] t_rof_empty). % RTS <: L:TS, RTS' % where % RTS = L:TS' + RTS0 lemma-15-6-1-r_ext : lemma-15-6-1-r VLPT ((trans_rsub_ext TRSP TSP) : (trans_rsub (rsub_ext (RSP : rsub RTS RTS') (SP : sub TS' TS) (MLPS: s_member_lab L TS' RTS)) _)) (TRTP : trans_rtype RTS RTT) (trans_rtype_ext (TRTP' : trans_rtype RTS' RTT') (TTP : trans_type TS TT)) ([y][opy] (t_rof_ext (ROPT y opy) (OPT (t_proj y L) (t_of_proj MLPT' opy)))) <- trans_type_exists TS' TTP' <- lemma-15-6-1 TSP TTP' TTP OPT <- lemma-15-6-1-r VLPT TRSP TRTP TRTP' ROPT <- trans_member_lab TRTP MLPS MLPT TTP'' <- trans_type_unq TS' TTP'' TTP' ETP <- eq_member_lab ETP MLPT MLPT'. % --- % --- terms :: translation of typing derivation in the source language into a % --- term of the target language % --- trans_of : s_of ES TS -> t_exp -> type. %name trans_of TOP. %mode trans_of +OPS -ET. trans_rof : s_rof RES RTS -> t_rexp -> type. %name trans_rof TROP. %mode trans_rof +ROPS -RET. trans_of_lam : trans_of (s_of_lam OPS) (t_lam ET) <- ({x}{opx}{y} (trans_of opx y -> trans_of ((OPS x) opx) (ET y))). trans_of_app : trans_of (s_of_app OPS2 OPS1) (t_app ET1 ET2) <- trans_of OPS1 ET1 <- trans_of OPS2 ET2. trans_of_proj : trans_of (s_of_proj (MLPS : s_member_lab L _ _) OPS) (t_proj ET L) <- trans_of OPS ET. trans_of_sub : trans_of (s_of_sub SP OPS) (C ET) <- trans_sub SP C <- trans_of OPS ET. trans_rof_empty : trans_rof s_rof_empty t_rcd_empty. trans_rof_ext : trans_rof ((s_rof_ext ROPS OPS) : s_rof (s_rcd_ext L _ _) _) (t_rcd_ext L ET RET) <- trans_of OPS ET <- trans_rof ROPS RET. trans_of_record : trans_of (s_of_record ROPS) (t_record RET) <- trans_rof ROPS RET. %block bl1 : some {TS} block {x : s_exp}{opx : s_of x TS}{y : t_exp}{topx : trans_of opx y}. %worlds (bl1) (trans_of _ _) (trans_rof _ _) (trans_sub _ _) (trans_rsub _ _). %total (SP RSP) (trans_sub SP _) (trans_rsub RSP _). %total (OPS ROPS) (trans_of OPS _) (trans_rof ROPS _). % --- % --- lemma 15-6-2 : D :: G |- es : ts => [G] |- [D] : tt, ts ~> tt % --- lemma-15-6-2 : {OPS : s_of ES TS} trans_of OPS ET -> t_of ET TT -> trans_type TS TT -> type. %mode lemma-15-6-2 +OPS +TOP -OPT -TTP. lemma-15-6-2-r : {ROPS : s_rof RES RTS} trans_rof ROPS ET -> t_rof ET RTT -> trans_rtype RTS RTT -> type. %mode lemma-15-6-2-r +ROPS +TROP -ROPT -TRTP. lemma-15-6-2_lam : lemma-15-6-2 ((s_of_lam OPS) : s_of _ (s_arrow TS1 _)) (trans_of_lam TOP) (t_of_lam OPT) (trans_type_arrow TTP2 TTP1) <- trans_type_exists TS1 TTP1 <- ({x}{opx : s_of x TS1}{y}{topx : trans_of opx y}{opy : t_of y TT1} (lemma-15-6-2 opx topx opy TTP1 -> lemma-15-6-2 (OPS x opx) (TOP x opx y topx) (OPT y opy) TTP2)). lemma-15-6-2_app : lemma-15-6-2 (s_of_app (OPS2 : s_of _ TS11) OPS1) (trans_of_app TOP2 TOP1) (t_of_app OPT2' OPT1) TTP12 <- lemma-15-6-2 OPS1 TOP1 OPT1 (trans_type_arrow TTP12 TTP11) <- lemma-15-6-2 OPS2 TOP2 OPT2 TTP11' <- trans_type_unq TS11 TTP11' TTP11 ETP <- eq_of ETP OPT2 OPT2'. lemma-15-6-2_record : lemma-15-6-2 ((s_of_record ROPS) : (s_of _ (s_record_type _ VLPS))) (trans_of_record TROP) (t_of_record ROPT) (trans_type_record VLPT TRTP) <- lemma-15-6-2-r ROPS TROP ROPT TRTP <- trans_valid_labs TRTP VLPS VLPT. lemma-15-6-2_proj : lemma-15-6-2 (s_of_proj MLPS OPS) (trans_of_proj TOP) (t_of_proj MLPT OPT) TTP <- lemma-15-6-2 OPS TOP OPT (trans_type_record VLPT TRTP) <- trans_member_lab TRTP MLPS MLPT TTP. lemma-15-6-2_sub : lemma-15-6-2 (s_of_sub SP OPS) (trans_of_sub (TOP : trans_of OPS ET) (TSP : trans_sub (SP : sub TS TS') C)) (OPT' ET OPT) TTP' <- lemma-15-6-2 OPS TOP OPT TTP <- trans_type_exists TS' TTP' <- lemma-15-6-1 TSP TTP TTP' OPT'. lemma-15-6-2-r_empty : lemma-15-6-2-r s_rof_empty trans_rof_empty t_rof_empty trans_rtype_empty. lemma-15-6-2-r_ext : lemma-15-6-2-r (s_rof_ext ROPS OPS) (trans_rof_ext TROP TOP) (t_rof_ext ROPT OPT) (trans_rtype_ext TRTP TTP) <- lemma-15-6-2 OPS TOP OPT TTP <- lemma-15-6-2-r ROPS TROP ROPT TRTP. %block bl2 : some {TS}{TT}{TTP : trans_type TS TT} block {x : s_exp}{opx : s_of x TS}{y : t_exp}{topx : trans_of opx y} {opy : t_of y TT}{l : lemma-15-6-2 opx topx opy TTP}. %worlds (bl2) (lemma-15-6-1 _ _ _ _) (lemma-15-6-1-r _ _ _ _ _) (lemma-15-6-2 _ _ _ _) (lemma-15-6-2-r _ _ _ _) (eq_of _ _ _) (eq_of2 _ _ _ _). %total {} (eq_of _ _ _). %total {} (eq_of2 _ _ _ _). %total (TSP TRSP) (lemma-15-6-1 TSP _ _ _) (lemma-15-6-1-r _ TRSP _ _ _). %total (OPS ROPS) (lemma-15-6-2 OPS _ _ _) (lemma-15-6-2-r ROPS _ _ _).