From caf7734e5540300856bf8fe2bbcbf3f1faed5c39 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Wed, 23 Oct 2013 18:07:42 +0100 Subject: Thread type environment through expressions because of block adding new variables, say in each branch of an if, that we want to be visible beyond it. --- language/l2.ott | 26 +++++-- language/l2_rules.ott | 195 ++++++++++++++++++++------------------------------ 2 files changed, 96 insertions(+), 125 deletions(-) (limited to 'language') diff --git a/language/l2.ott b/language/l2.ott index 2e37a490..50f9a353 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -1087,9 +1087,8 @@ S_N {{ tex \Sigma^{\textsc{N} } }} :: '' ::= {{ phantom }} I :: '' ::= {{ phantom }} {{ com Information given by type checking an expression; tag only reflects the immediate exp }} - | < S_N , effects , tag > :: :: I - | Ir :: :: reset {{ com resets the tag of an I. }} {{ tex {\ottnt{I}_{\textit{reset} } } }} - | Ie :: :: Iempty {{ com Empty constraints, effetcs, tag }} {{ tex {\ottnt{I}_{\epsilon} } }} + | < S_N , effects > :: :: I + | Ie :: :: Iempty {{ com Empty constraints, effetcs }} {{ tex {\ottnt{I}_{\epsilon} } }} | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effects, setting None for the tag }} E :: '' ::= {{ phantom }} @@ -1120,13 +1119,26 @@ S_N {{ tex \Sigma^{\textsc{N} } }} :: '' ::= {{ phantom }} {{ hol (id |-> t) }} {{ lem map x f_desc }} {{ com Type environments }} - | { id1 |-> t1 , .. , idn |-> tn } :: :: concrete + | { id1 |-> t1 , .. , idn |-> tn } :: :: base {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 t1 .. idn tn]]) }} {{ lem (List.fold_right (fun (x,f) m -> Pmap.add x f m) [[id1 t1 .. idn tn]] Pmap.empty) }} - | E_t1 u+ .. u+ E_tn :: M :: union - {{ hol (FOLDR FUNION FEMPTY [[E_t1..E_tn]]) }} - {{ lem (List.fold_right union_map [[E_t1..E_tn]] Pmap.empty) }} + | ( E_t1 u+ .... u+ E_tn ) :: M :: union + {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }} + {{ lem (List.fold_right union_map [[E_t1....E_tn]] Pmap.empty) }} {{ ocaml (assert false) }} + | u+ E_t1 .. E_tn :: M :: multi_union + {{ hol arb }} + {{ lem arb }} + {{ ocaml assert false }} + | ( E_t1 inter .... inter E_tn ) :: M :: intersect + {{ hol arb }} + {{ lem syntax error }} + {{ ocaml (assert false) }} + | inter E_t1 .. E_tn :: M :: multi_inter + {{ hol arb }} + {{ lem arb }} + {{ ocaml assert false }} + field_typs :: 'FT_' ::= {{ phantom }} {{ com Record fields }} diff --git a/language/l2_rules.ott b/language/l2_rules.ott index 7d05457e..c07f41a0 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -370,7 +370,7 @@ E_k |-t t ok |- pat : t gives E_t1,S_N id NOTIN dom(E_t1) ------------------------------------------------------------ :: as - |- (pat as id) : t gives E_t1 u+ {id|->t},S_N + |- (pat as id) : t gives (E_t1 u+ {id|->t}),S_N E_k |- typ ~> t |- pat : t gives E_t1,S_N @@ -381,190 +381,149 @@ E_t(id) gives (t1*..*tn) -> id t_args effect { } Ctor |- pat1 : t1 gives E_t1,S_N1 .. |- patn : tn gives E_tn,S_Nn disjoint doms(E_t1,..,E_tn) ------------------------------------------------------------ :: ident_constr - |- id pat1 .. patn : id t_args gives E_t1 u+ .. u+ E_tn, S_N1 u+ .. u+ S_Nn + |- id pat1 .. patn : id t_args gives u+ E_t1 .. E_tn, S_N1 u+ .. u+ S_Nn E_k |-t t ok ------------------------------------------------------------ :: var - |- :P_id: id : t gives E_t u+ {id|->t},{} + |- :P_id: id : t gives (E_t u+ {id|->t}),{} E_r() gives id t_args, () |- pati : ti gives E_ti,S_Ni//i/> disjoint doms() ------------------------------------------------------------ :: record - |- { semi_opt } : id t_args gives u+ , u+ + |- { semi_opt } : id t_args gives :E_t_multi_union: u+ , u+ -E |- pat1 : t gives E_t1,S_N1 ... E |- patn : t gives E_tn,S_Nn -disjoint doms(E_t1 , ... , E_tn) -length(pat1 ... patn) = num +E |- pat1 : t gives E_t1,S_N1 .. E |- patn : t gives E_tn,S_Nn +disjoint doms(E_t1 , .. , E_tn) +length(pat1 .. patn) = num ----------------------------------------------------------- :: vector -E |- [ pat1 , ... , patn ] : vector :t_arg_nexp: id num+id inc t gives E_t1 u+ ... u+ E_tn,S_N1 u+ ... u+ S_Nn +E |- [ pat1 , .. , patn ] : vector :t_arg_nexp: id num+id inc t gives (E_t1 u+ .. u+ E_tn),S_N1 u+ .. u+ S_Nn E |- pat1 : t gives E_t1,S_N1 ... E |- patn : t gives E_tn,S_Nn disjoint doms(E_t1 , ... , E_tn) num1 lt ... lt numn ----------------------------------------------------------- :: indexedVectorInc -E |- [ num1 = pat1 , ... , numn = patn ] : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives E_t1 u+ ... u+ E_tn, {id<=num1, id' >= numn + (- num1)} u+ S_N1 u+ ... u+ S_Nn +E |- [ num1 = pat1 , ... , numn = patn ] : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives (E_t1 u+ ... u+ E_tn), {id<=num1, id' >= numn + (- num1)} u+ S_N1 u+ ... u+ S_Nn E |- pat1 : t gives E_t1,S_N1 ... E |- patn : t gives E_tn,S_Nn disjoint doms(E_t1 , ... , E_tn) num1 gt ... gt numn ----------------------------------------------------------- :: indexedVectorDec -E |- [ num1 = pat1 , ... , numn = patn ] : vector :t_arg_nexp: id :t_arg_nexp: id' dec t gives E_t1 u+ ... u+ E_tn, {id>=num1,id'<=num1 +(-numn)} u+ S_N1 u+ ... u+ S_Nn +E |- [ num1 = pat1 , ... , numn = patn ] : vector :t_arg_nexp: id :t_arg_nexp: id' dec t gives (E_t1 u+ ... u+ E_tn), {id>=num1,id'<=num1 +(-numn)} u+ S_N1 u+ ... u+ S_Nn E |- pat1 : vector ne1 ne'1 inc t gives E_t1,S_N1 ... E |- patn : vector nen ne'n inc t gives E_tn,S_Nn disjoint doms(E_t1 , ... , E_tn) S_N0 = consistent_increase ne1 ne'1 ... nen ne'n ----------------------------------------------------------- :: vectorConcatInc -E |- pat1 : ... : patn : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives E_t1 u+ ... u+ E_tn,{id<=ne1,id'>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ S_Nn +E |- pat1 : ... : patn : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives (E_t1 u+ ... u+ E_tn),{id<=ne1,id'>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ S_Nn E |- pat1 : vector ne1 ne'1 dec t gives E_t1,S_N1 ... E |- patn : vector nen ne'n dec t gives E_tn,S_Nn disjoint doms(E_t1 , ... , E_tn) S_N0 = consistent_decrease ne1 ne'1 ... nen ne'n ----------------------------------------------------------- :: vectorConcatDec -E |- pat1 : ... : patn : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives E_t1 u+ ... u+ E_tn,{id>=ne1,id'>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ S_Nn +E |- pat1 : ... : patn : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives (E_t1 u+ ... u+ E_tn),{id>=ne1,id'>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ S_Nn |- pat1 : t1 gives E_t1,S_N1 .... |- patn : tn gives E_tn,S_Nn disjoint doms(E_t1,....,E_tn) ------------------------------------------------------------ :: tup - |- (pat1, ...., patn) : (t1 * .... * tn) gives E_t1 u+ .... u+ E_tn,S_N1 u+ .... u+ S_Nn + |- (pat1, ...., patn) : (t1 * .... * tn) gives (E_t1 u+ .... u+ E_tn),S_N1 u+ .... u+ S_Nn E_k |-t t ok |- pat1 : t gives E_t1,S_N1 .. |- patn : t gives E_tn,S_Nn disjoint doms(E_t1,..,E_tn) ------------------------------------------------------------ :: list - |- [|pat1, .., patn |] : list t gives E_t1 u+ .. u+ E_tn,S_N1 u+ .. u+ S_Nn + |- [|pat1, .., patn |] : list t gives (E_t1 u+ .. u+ E_tn),S_N1 u+ .. u+ S_Nn - -%% % -%% % -%% % defns -%% % id_field :: '' ::= -%% % -%% % defn -%% % E |- id field :: :: id_field :: id_field_ -%% % {{ com Check that the identifier is a permissible field identifier }} -%% % by -%% % -%% % E_f(x) gives f_desc -%% % ------------------------------------------------------------ :: empty -%% % |- x l1 l2 field -%% % -%% % -%% % E_m(x) gives E -%% % x NOTIN dom(E_f) -%% % E |- z_l l2 field -%% % ------------------------------------------------------------ :: cons -%% % |- x l1. z_l l2 field -%% % -%% % defns -%% % id_value :: '' ::= -%% % -%% % defn -%% % E |- id value :: :: id_value :: id_value_ -%% % {{ com Check that the identifier is a permissible value identifier }} -%% % by -%% % -%% % E_x(x) gives v_desc -%% % ------------------------------------------------------------ :: empty -%% % |- x l1 l2 value -%% % -%% % -%% % E_m(x) gives E -%% % x NOTIN dom(E_x) -%% % E |- z_l l2 value -%% % ------------------------------------------------------------ :: cons -%% % |- x l1. z_l l2 value -%% % defns check_exp :: '' ::= defn -E |- exp : t gives I :: :: check_exp :: check_exp_ -{{ com Typing expressions, collecting nexp constraints and effects }} +E |- exp : t gives I , E_t :: :: check_exp :: check_exp_ +{{ com Typing expressions, collecting nexp constraints, effects, and new bindings }} by -%% TODO::: if t is a reg, need to distinguish here between reg and ref cell access, and add to effect if reg, and maybe add to tag +%% TODO::: if t is a reg, need to distinguish here between reg and ref cell access, and add to effect if reg E_t(id) gives t ------------------------------------------------------------ :: var - |- id : t gives Ie + |- id : t gives Ie,E_t E_t(id) gives t' -> t effect {} Ctor {} - |- exp : t' gives I + |- exp : t' gives I,E_t ------------------------------------------------------------ :: ctor - |- id exp : t gives Ir + |- id exp : t gives I,E_t E_t(id) gives t' -> t effects tag S_N - |- exp : t' gives + |- exp : t' gives I,E_t ------------------------------------------------------------ :: app - |- id exp : t gives + |- id exp : t gives I u+ , E_t E_t(id) gives (t1 * t2) -> t effects tag S_N - |- exp1 : t1 gives - |- exp2 : t2 gives + |- exp1 : t1 gives I2,E_t + |- exp2 : t2 gives I3,E_t ------------------------------------------------------------ :: infix_app - |- :E_app_infix: exp1 id exp2 : t gives + |- :E_app_infix: exp1 id exp2 : t gives I2 u+ I3 u+ , E_t E_r() gives id t_args, - |- expi : ti gives Ii//i/> + |- expi : ti gives Ii,E_t//i/> ------------------------------------------------------------ :: record - |- { semi_opt} : id t_args gives u+ + |- { semi_opt} : id t_args gives u+ , E_t - |- exp : id t_args gives I + |- exp : id t_args gives I,E_t E_r(id t_args) gives - |- expi : ti gives Ii//i/> + |- expi : ti gives Ii,E_t//i/> SUBSET ------------------------------------------------------------ :: recup - |- { exp with semi_opt } : id t_args gives I + |- { exp with semi_opt } : id t_args gives I u+ , E_t -E |- exp1 : t gives I1 ... E |- expn : t gives In +E |- exp1 : t gives I1,E_t ... E |- expn : t gives In,E_t length(exp1 ... expn) = num ------------------------------------------------------------ :: vector -E |- [ exp1 , ... , expn ] : vector zero num inc t gives I1 u+ ... u+ In +E |- [ exp1 , ... , expn ] : vector zero num inc t gives I1 u+ ... u+ In, E_t -E |- exp1 : vector ne ne' inc t gives I1 -E |- exp2 : enum ne2 ne2' inc gives I2 +E |- exp1 : vector ne ne' inc t gives I1,E_t +E |- exp2 : enum ne2 ne2' inc gives I2,E_t ------------------------------------------------------------- :: vectorgetInc -E |- :E_vector_access: exp1 [ exp2 ] : t gives I1 u+ I2 u+ <{ne<=ne2,ne2+ne2'<=ne+ne'},pure,None> +E |- :E_vector_access: exp1 [ exp2 ] : t gives I1 u+ I2 u+ <{ne<=ne2,ne2+ne2'<=ne+ne'},pure>,E_t -E |- exp1 : vector ne ne' dec t gives I1 -E |- exp2 : enum ne2 ne'2 dec gives I2 +E |- exp1 : vector ne ne' dec t gives I1,E_t +E |- exp2 : enum ne2 ne'2 dec gives I2,E_t ------------------------------------------------------------- :: vectorgetDec -E |- :E_vector_access: exp1 [ exp2 ] : t gives I1 u+ I2 u+ <{ne>=ne2,ne2+(-ne2')<=ne+(-ne')},pure,None> +E |- :E_vector_access: exp1 [ exp2 ] : t gives I1 u+ I2 u+ <{ne>=ne2,ne2+(-ne2')<=ne+(-ne')},pure>,E_t -E |- exp1 : vector ne ne' order t gives I1 -E |- exp2 : enum ne2 ne'2 order gives I2 -E |- exp3 : enum ne3 ne'3 order gives I3 +E |- exp1 : vector ne ne' order t gives I1,E_t +E |- exp2 : enum ne2 ne'2 order gives I2,E_t +E |- exp3 : enum ne3 ne'3 order gives I3,E_t ------------------------------------------------------------- :: vectorsub -E |- :E_vector_subrange: exp1[ exp2 : exp3 ] : vector :t_arg_nexp: id :t_arg_nexp: id' order t gives I1 u+ I2 u+ I3 u+ <{ne <= ne2, id >= ne2 , id <= ne2+ne2', ne2+ne'2<=ne3, ne+ne'>=ne3+ne'3, id' <=ne3 + ne'3},pure,None> +E |- :E_vector_subrange: exp1[ exp2 : exp3 ] : vector :t_arg_nexp: id :t_arg_nexp: id' order t gives I1 u+ I2 u+ I3 u+ <{ne <= ne2, id >= ne2 , id <= ne2+ne2', ne2+ne'2<=ne3, ne+ne'>=ne3+ne'3, id' <=ne3 + ne'3},pure>,E_t -E |- exp : vector ne1 ne2 order t gives I -E |- exp1 : enum ne3 ne4 order gives I1 -E |- exp2 : t gives I2 +E |- exp : vector ne1 ne2 order t gives I,E_t +E |- exp1 : enum ne3 ne4 order gives I1,E_t +E |- exp2 : t gives I2,E_t ------------------------------------------------------------ :: vectorup -E |- [ exp with exp1 = exp2 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ <{ne1 <= ne3, ne1 + ne2 >= ne3 + ne4},pure,None> +E |- [ exp with exp1 = exp2 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ <{ne1 <= ne3, ne1 + ne2 >= ne3 + ne4},pure>,E_t -E |- exp : vector ne1 ne2 order t gives I -E |- exp1 : enum ne3 ne4 order gives I1 -E |- exp2 : enum ne5 ne6 order gives I2 -E |- exp3 : vector ne7 ne8 order t gives I3 +E |- exp : vector ne1 ne2 order t gives I,E_t +E |- exp1 : enum ne3 ne4 order gives I1,E_t +E |- exp2 : enum ne5 ne6 order gives I2,E_t +E |- exp3 : vector ne7 ne8 order t gives I3,E_t ------------------------------------------------------------ :: vecrangeup -E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ I3 u+ <{ne1 <= ne3, ne1 <= ne5,ne3+ne4 <= ne5, ne1 + ne2 <= ne5 + ne6 + (- ne3) + (- ne4), ne7 + ne8 = ne1 + ne2 + (- ne3) + (- ne4)},pure,None> +E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ I3 u+ <{ne1 <= ne3, ne1 <= ne5,ne3+ne4 <= ne5, ne1 + ne2 <= ne5 + ne6 + (- ne3) + (- ne4), ne7 + ne8 = ne1 + ne2 + (- ne3) + (- ne4)},pure>,E_t -E |- exp : vector ne1 ne2 order t gives I -E |- exp1 : enum ne3 ne4 order gives I1 -E |- exp2 : enum ne5 ne6 order gives I2 -E |- exp3 : t gives I3 +E |- exp : vector ne1 ne2 order t gives I,E_t +E |- exp1 : enum ne3 ne4 order gives I1,E_t +E |- exp2 : enum ne5 ne6 order gives I2,E_t +E |- exp3 : t gives I3,E_t ------------------------------------------------------------ :: vecrangeupvalue -E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ I3 u+ <{ne1 <= ne3, ne1 <= ne5,ne3+ne4 <= ne5, ne1 + ne2 <= ne5 + ne6 + (- ne3) + (- ne4)},pure,None> +E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ I3 u+ <{ne1 <= ne3, ne1 <= ne5,ne3+ne4 <= ne5, ne1 + ne2 <= ne5 + ne6 + (- ne3) + (- ne4)},pure>,E_t E_r (id t_args) gives id : t - |- exp : id t_args gives I + |- exp : id t_args gives I,E_t ------------------------------------------------------------ :: field - |- exp.id : t gives Ir + |- exp.id : t gives I,E_t %% % %% % @@ -572,10 +531,10 @@ E_r (id t_args) gives id : t %% % ------------------------------------------------------------ :: case %% % TD,E,E_l |- match exp with bar_opt expi li//i/> l end : u gives S_c' union ,S_N' union - |- exp : t gives I + |- exp : t gives I,E_t E_k |- typ ~> t ------------------------------------------------------------ :: typed - |- (typ) exp : t gives Ir + |- (typ) exp : t gives I,E_t %% % %KATHYCOMMENT: where does E_l1 come from? %% % TD,E,E_l1 |- letbind gives E_l2, S_c1,S_N1 @@ -583,35 +542,35 @@ E_k |- typ ~> t %% % ------------------------------------------------------------ :: let %% % TD,E,E_l |- let letbind in exp : t gives S_c1 union S_c2,S_N1 union S_N2 -E |- exp1 : t1 gives I1 .... E |- expn : tn gives In +E |- exp1 : t1 gives I1,E_t .... E |- expn : tn gives In,E_t ------------------------------------------------------------ :: tup -E |- (exp1, .... , expn) : (t1 * .... * tn) gives I1 u+ .... u+ In +E |- (exp1, .... , expn) : (t1 * .... * tn) gives I1 u+ .... u+ In,E_t -E |- exp1 : t gives I1 .. E |- expn : t gives In +E |- exp1 : t gives I1,E_t .. E |- expn : t gives In,E_t ------------------------------------------------------------ :: list -E |- [|exp1, .., expn |] : list t gives I1 u+ .. u+ In +E |- [|exp1, .., expn |] : list t gives I1 u+ .. u+ In,E_t -E |- exp1 : bool gives I1 -E |- exp2 : t gives I2 -E |- exp3 : t gives I3 +E |- exp1 : bool gives I1,E_t +E |- exp2 : t gives I2,E_t2 +E |- exp3 : t gives I3,E_t3 ------------------------------------------------------------ :: if -E |- if exp1 then exp2 else exp3 : t gives I1 u+ I2 u+ I3 +E |- if exp1 then exp2 else exp3 : t gives I1 u+ I2 u+ I3,(E_t2 inter E_t3) - |- exp1 : enum ne1 ne2 order gives I1 - |- exp2 : enum ne3 ne4 order gives I2 - |- exp3 : enum ne5 ne6 order gives I3 - enum ne1 ne3+ne4 order},E_r,E_k> |- exp4 : t gives I4 + |- exp1 : enum ne1 ne2 order gives I1,E_t + |- exp2 : enum ne3 ne4 order gives I2,E_t + |- exp3 : enum ne5 ne6 order gives I3,E_t +<(E_t u+ {id |-> enum ne1 ne3+ne4 order}),E_r,E_k> |- exp4 : t gives I4,(E_t u+ {id |-> enum ne1 ne3+ne4 order}) ----------------------------------------------------------- :: for - |- foreach id from exp1 to exp2 by exp3 exp4 : t gives I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure,None> + |- foreach id from exp1 to exp2 by exp3 exp4 : t gives I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure>,E_t -E |- exp1 : t gives I1 -E |- exp2 : list t gives I2 +E |- exp1 : t gives I1,E_t +E |- exp2 : list t gives I2,E_t ------------------------------------------------------------ :: cons -E |- exp1 :: exp2 : list t gives I1 u+ I2 +E |- exp1 :: exp2 : list t gives I1 u+ I2,E_t |- lit : t ------------------------------------------------------------ :: lit -E |- lit : t gives Ie + |- lit : t gives Ie,E_t %% % defn -- cgit v1.2.3