From e1c2222da39ed29210c8f33563aa9570e52db80b Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Wed, 18 Feb 2015 11:37:24 +0000 Subject: expression type checking inline with rules, lexp still out of date; overloading resolution not modelled --- language/l2_rules.ott | 194 ++++++++++++++++++++++++++++++-------------------- language/l2_typ.ott | 3 + 2 files changed, 121 insertions(+), 76 deletions(-) diff --git a/language/l2_rules.ott b/language/l2_rules.ott index e348e14a..a4624527 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -760,6 +760,15 @@ E_d |- u ~< t,S_N ------------------------------------------------------------ :: ctor ,t |- :E_app: id(exp) : t gives :E_app: id(exp'), ,{} +E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u +u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect +ui == ( implicit, t0 , .. , tm ) +,(t0,..,tm) |- (exp0,..,expm) : ui' gives (exp0',..,expm'),I,E_t' +E_d,t |- :E_app: id (annot, exp'0, .., exp'm) : uj gives uj', exp'',S_N',effect' +------------------------------------------------------------ :: appImplicit +,t |- :E_app: id(exp0,..,expm) : uj gives exp'', I u+ u+ , E_t + + E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect ,ui |- exp : ui' gives exp',I,E_t' @@ -799,40 +808,42 @@ S_N' == u+ ------------------------------------------------------------ :: record >,t |- { semi_opt} : x gives{ semi_opt}, u+ >, {} ->,t |- exp : id t_args gives exp', I,E_t -E_r(id t_args) gives ->,ti |- expi : ui gives expi',Ii,E_t//i/> +>,t |- exp : x gives exp', I,E_t +E_r(x) gives +>,ti |- expi : ui gives expi',Ii,E_t//i/> SUBSET |- ui ~< ti,S_N'i//i/> ------------------------------------------------------------ :: recup -> ,t |- { exp with semi_opt } : id t_args gives {exp' with }, I u+ , E_t +> ,t |- { exp with semi_opt } : x gives {exp' with }, I u+ , E_t -E,t |- exp1 u1 t gives exp'1,I1,E_t ... E,t |- expn : un gives exp'n,In,E_t -length(exp1 ... expn) = num +,t |- exp1 : u1 gives exp'1,I1,E_t' ... ,t |- expn : un gives exp'n,In,E_t' +E_d |- u1 ~< t, S_N1 ... E_d |- un ~< t, S_Nn +length(exp1 ... expn) == ne +S_N == {ne=ne2} u+ S_N1 u+ ... u+ S_Nn ------------------------------------------------------------ :: vector -E, vector |- [ exp1 , ... , expn ] : vector gives [exp'1,...,exp'n], I1 u+ ... u+ In, E_t +E, vector |- [ exp1 , ... , expn ] : vector gives [exp'1,...,exp'n], u+ I1 u+ ... u+ In , E_t -E, vector |- exp1 : vector gives exp'1,I1,E_t +E, vector |- exp1 : vector gives exp'1,I1,E_t E, range |- exp2 : range gives exp'2, I2,E_t ------------------------------------------------------------- :: vectorgetInc E, t |- :E_vector_access: exp1 [ exp2 ] : u gives exp'1 [ exp'2], I1 u+ I2 u+ <{ne1<=ne3,ne3+ne3'<=ne1+ne1'},pure>,E_t -E, vector |- exp1 : vector gives exp'1,I1,E_t +E, vector |- exp1 : vector gives exp'1,I1,E_t E, range |- exp2 : range gives exp'2, I2,E_t ------------------------------------------------------------- :: vectorgetDec E, t |- :E_vector_access: exp1 [ exp2 ] : u gives exp'1 [ exp'2], I1 u+ I2 u+ <{ne1>=ne3,ne3+(-ne3')<=ne1+(-ne1')},pure>,E_t -E, vector |- exp1 : gives exp'1, I1,E_t +E, vector |- exp1 : vector gives exp'1, I1,E_t E, range |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t E,range |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t ------------------------------------------------------------- :: vectorsubInc -E, vector |- :E_vector_subrange: exp1[ exp2 : exp3 ] : vector gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne >= ne4, ne <= ne'4,ne'<=ne4+ne'6,ne4 <= ne2, ne4+ne6' <= ne'2},pure>,E_t +E, vector |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne >= ne4, ne <= ne'4,ne'<=ne4+ne'6,ne4 <= ne2, ne4+ne6' <= ne'2},pure>,E_t -E, vector |- exp1 : gives exp'1, I1,E_t +E, vector |- exp1 : vector< ne2 ne'2 dec u> gives exp'1, I1,E_t E, range |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t E,range |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t ------------------------------------------------------------- :: vectorsubDec -E, vector |- :E_vector_subrange: exp1[ exp2 : exp3 ] : vector gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne <= ne4, ne >= ne'4,ne'<=ne'6+(-ne4),ne4' >= ne2, ne'6+(-ne4) <= ne'2},pure>,E_t +E, vector |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne <= ne4, ne >= ne'4,ne'<=ne'6+(-ne4),ne4' >= ne2, ne'6+(-ne4) <= ne'2},pure>,E_t E, vector |- exp : vector< ne1 ne2 inc u> gives exp',I,E_t E, range |- exp1 : range gives exp'1,I1,E_t @@ -846,26 +857,43 @@ E,t |- exp2 : u gives exp'2,I2,E_t ------------------------------------------------------------ :: vectorupDec E, vector |- [ exp with exp1 = exp2 ] : vector< ne1 ne2 dec u> gives [exp' with exp'1 = exp'2], I u+ I1 u+ I2 u+ <{ne1 >= ne3, ne2 >= ne4},pure>,E_t -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>,E_t - -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>,E_t - - -E_r (id t_args) gives id : u ->,t'' |- exp : id t_args gives exp', I,E_t +E,vector |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t +E,atom |- exp1 : atom gives exp1',I1,E_t +E,atom |- exp2 : atom gives exp2', I2,E_t +E,vector |- exp3 : vector gives exp3',I3,E_t +I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7, ne12 = ne8 + (-ne6) , ne6 + one <= ne8},pure> +------------------------------------------------------------ :: vecrangeupInc +E,vector |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t + +E,vector |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t +E,atom |- exp1 : atom gives exp1',I1,E_t +E,atom |- exp2 : atom gives exp2', I2,E_t +E,u |- exp3 : u' gives exp3',I3,E_t +I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7 },pure> +------------------------------------------------------------ :: vecrangeupvalueInc +E,vector |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t + +E,vector |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t +E,atom |- exp1 : atom gives exp1',I1,E_t +E,atom |- exp2 : atom gives exp2', I2,E_t +E,vector |- exp3 : vector gives exp3',I3,E_t +I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> +------------------------------------------------------------ :: vecrangeupDec +E,vector |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t + +E,vector |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t +E,atom |- exp1 : atom gives exp1',I1,E_t +E,atom |- exp2 : atom gives exp2', I2,E_t +E,u |- exp3 : u' gives exp3',I3,E_t +I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> +------------------------------------------------------------ :: vecrangeupvalueDec +E,vector |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t + +E_r (x) gives id : u +>,t'' |- exp : x< t_args> gives exp', I,E_t E_d,t |- exp'.id : u gives t', exp1', S_N', effect ------------------------------------------------------------ :: field ->,t |- exp.id : u gives exp1',I u+ ,E_t +>,t |- exp.id : u gives exp1',I u+ ,E_t ,t'' |- exp : u gives exp',I,E_t ,u |- pati : u'i gives pat'i,E_ti,S_Ni//i/> @@ -874,94 +902,108 @@ E_d,t |- exp'.id : u gives t', exp1', S_N', effect ,t |- switch exp { expi//i/> }: u gives switch exp' { exp'i//i/> }, I u+ //i/>, E_t ,t'' |- exp : u gives exp',I,E_t -E_d |- typ |-> t' +E_d |- typ ~> t' E_d,t' |- exp' : u gives u', exp'', S_N,effect E_d,t |- exp'' : t' gives u'', exp''', S_N', effect' ------------------------------------------------------------ :: typed -,t |- (typ) exp : t gives exp''',Iu+,E_t +,t |- (typ) exp : t gives exp''',I u+ ,E_t |- letbind gives E_t1, S_N, effect, {} -<(E_t u+ E_t1),E_d> |- exp : t gives I2, E_t2 +<(E_t u+ E_t1),E_d>,t |- exp : u gives exp', I2, E_t2 ------------------------------------------------------------ :: let - |- letbind in exp : t gives u+ I2, E_t +,t |- letbind in exp : t gives exp', u+ I2, E_t -E |- exp1 : t1 gives I1,E_t .... E |- expn : tn gives In,E_t +E,t1 |- exp1 : u1 gives exp1',I1,E_t1 .... E,tn |- expn : un gives expn',In,E_tn ------------------------------------------------------------ :: tup -E |- (exp1, .... , expn) : (t1 * .... * tn) gives I1 u+ .... u+ In,E_t +E,(t1, ...., tn) |- (exp1, .... , expn) : (u1 , .... , un) gives (exp1', ...., expn'), I1 u+ .... u+ In,E_t -E |- exp1 : t gives I1,E_t .. E |- expn : t gives In,E_t +,t |- exp1 : u1 gives exp1', I1,E_t1 .. ,t |- expn : un gives expn', In,E_tn +E_d |- u1 ~< t,S_N1 .. E_d |- un ~< t,S_Nn ------------------------------------------------------------ :: list -E |- [||exp1, .., expn ||] : list t gives I1 u+ .. u+ In,E_t +,list |- [||exp1, .., expn ||] : list gives [|| exp1', .., expn' ||], u+ I1 u+ .. u+ In, E_t -E |- exp1 : bool gives I1,E_t -E |- exp2 : t gives I2,E_t2 -E |- exp3 : t gives I3,E_t3 +E,bit |- exp1 : bit gives exp1',I1,E_t' +E,t |- exp2 : u1 gives exp2',I2,E_t2 +E,t |- exp3 : u2 gives exp3',I3,E_t3 +E_d |- u1 ~< t,S_N1 +E_d |- u2 ~< t,S_N2 ------------------------------------------------------------ :: if -E |- if exp1 then exp2 else exp3 : t gives I1 u+ I2 u+ I3,(E_t2 inter E_t3) +,t |- if exp1 then exp2 else exp3 : u gives if exp1' then exp2' else exp3', u+ I1 u+ I2 u+ I3,(E_t2 inter E_t3) - |- 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_d> |- exp4 : t gives I4,(E_t u+ {id |-> enum ne1 ne3+ne4 order}) +,range |- exp1 : range< ne7 ne8> gives exp1', I1,E_t +,range |- exp2 : range< ne9 ne10> gives exp2', I2,E_t +,range |- exp3 : range< ne11 ne12> gives exp3',I3,E_t +<(E_t u+ {id |-> range< ne1 ne4>}),E_d>,unit |- exp4 : t gives exp4',I4,E_t' ----------------------------------------------------------- :: for - |- 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 +,unit |- foreach (id from exp1 to exp2 by exp3) exp4 : t gives foreach (id from exp1' to exp2' by exp3') exp4', I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure>,E_t -E |- exp1 : t gives I1,E_t -E |- exp2 : list t gives I2,E_t +E,t |- exp1 : u gives exp1',I1,E_t +E,list |- exp2 : list gives exp2',I2,E_t ------------------------------------------------------------ :: cons -E |- exp1 :: exp2 : list t gives I1 u+ I2,E_t +E,list |- exp1 :: exp2 : list gives exp1'::exp2', I1 u+ I2,E_t -|- lit : t +t |- lit : u => exp,S_N ------------------------------------------------------------ :: lit - |- lit : t gives Ie,E_t +E,t |- lit : u gives exp,,E_t - |- exp : t gives I, E_t1 +,unit |- exp : unit gives exp', I, E_t1 ------------------------------------------------------------ :: blockbase - |- { exp } : unit gives I, E_t +,unit |- { exp } : unit gives {exp'}, I, E_t - |- exp : u gives I1, E_t1 -<(E_t u+ E_t1),E_d> |- { } : t gives I2, E_t2 +,unit |- exp : unit gives exp', I1, E_t1 +<(E_t u+ E_t1),E_d>,unit |- { } : unit gives {}, I2, E_t2 ------------------------------------------------------------ :: blockrec - |- { exp ; } : t gives I1 u+ I2, E_t +,unit |- { exp ; } : unit gives {exp'; }, I1 u+ I2, E_t +,unit |- exp : unit gives exp', I, E_t1 +------------------------------------------------------------ :: nondetbase +,unit |- nondet { exp } : unit gives {exp'}, I, E_t - |- nondet { exp ; } : unit +,unit |- exp : unit gives exp', I1, E_t1 +<(E_t u+ E_t1),E_d>,unit |- nondet { } : unit gives {}, I2, E_t2 +------------------------------------------------------------ :: nondetrec +,unit |- nondet { exp ; } : unit gives {exp'; }, I1 u+ I2, E_t -E |- exp:t gives I1, E_t1 -E |- lexp:t gives I2, E_t2 +E,t |- exp:u gives exp', I1, E_t1 +E |- lexp:t gives lexp', I2, E_t2 ------------------------------------------------------------ :: assign -E |- lexp := exp : unit gives I u+ I2, E_t2 +E,unit |- lexp := exp : unit gives lexp' := exp', I u+ I2, E_t2 defn -E |- lexp : t gives I , E_t :: :: check_lexp :: check_lexp_ +E |- lexp : t gives lexp' , I , E_t :: :: check_lexp :: check_lexp_ {{ com Check the left hand side of an assignment }} by -E_t(id) gives register t +E_t(id) gives register ---------------------------------------------------------- :: wreg - |- id : t gives <{},{ wreg }>, E_t + |- id : t gives id,<{},{ wreg }>, E_t -E_t(id) gives reg t +E_t(id) gives reg ---------------------------------------------------------- :: wlocl - |- id : t gives Ie, E_t + |- id : t gives id,Ie, E_t E_t(id) gives t ---------------------------------------------------------- :: var - |- id : t gives Ie,E_t + |- id : t gives id,Ie,E_t id NOTIN dom(E_t) ---------------------------------------------------------- :: wnew - |- id : t gives Ie, {id |-> reg t} + |- id : t gives id,Ie, {id |-> reg} -E_t(id) gives t1 -> t {, wmem, } Extern {} - |- exp : t1 gives I,E_t1 +E_t(id) gives E_k, S_N, Extern, t1 -> t {, wmem, } +,t1 |- exp : u1 gives exp',I,E_t1 ---------------------------------------------------------- :: wmem - |- :LEXP_memory: id(exp) : t gives I u+ <{},{wmem}>,E_t + |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ ,E_t + +E,atom |- exp : u gives exp',I1,E_t +E |- lexp : vector gives lexp',I2,E_t +---------------------------------------------------------- :: wbitInc +E |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne1 <= ne, ne1 + ne2 >= ne},pure>,E_t -E |- exp : enum ne1 ne2 order gives I1,E_t -E |- lexp : vector ne3 ne4 order t gives I2,E_t ----------------------------------------------------------- :: wbit -E |- lexp [exp] : t gives I1 u+ I2 u+ <{ne3 <= ne1, ne1 + ne2 <= ne3 + ne4},pure>,E_t +E,atom |- exp : u gives exp',I1,E_t +E |- lexp : vector gives lexp',I2,E_t +---------------------------------------------------------- :: wbitDec +E |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne <= ne1, ne1 + (-ne2) <= ne},pure>,E_t E |- exp1 : enum ne1 ne2 order gives I1,E_t E |- exp2 : enum ne3 ne4 order gives I2,E_t diff --git a/language/l2_typ.ott b/language/l2_typ.ott index 21002502..77b956c5 100644 --- a/language/l2_typ.ott +++ b/language/l2_typ.ott @@ -53,6 +53,8 @@ t , u :: 'T_' ::= | atom < ne > :: S :: atom_app {{ ichlo T_app "atom" [ [[ne]] ] }} | vector < ne ne' order t > :: S :: vector_app {{ ichlo T_app "vector" [[ [ ne; ne'; ord; t ] ]] }} | list < t > :: S :: list_app {{ ichlo T_app "list" [[t]] }} + | reg < t > :: S :: box_app {{ ichlo T_app "reg" [[t]] }} + | implicit < ne > :: S :: implicit_app {{ ichlo T_app "implicit" [[ne]] }} | bit :: S :: bit_typ {{ ichlo T_id "bit" }} | string :: S :: string_typ {{ ichlo T_id "string" }} | unit :: S :: unit_typ {{ ichlo T_id "unit" }} @@ -348,6 +350,7 @@ grammar {{ lem (Inf [[S_N]] [[effect]]) }} | Ie :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }} {{ lem Iemp }} + | ( I1 u+ I2 ) :: :: singleunion {{ tex [[I1]] [[u+]] [[I2]] }} | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effect }} {{ lem (List.foldr inf_union Iemp [[I1..In]]) }} -- cgit v1.2.3