From a871de7a1cff3fbd11081deb16881ed352fb45ca Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Wed, 18 Feb 2015 15:40:30 +0000 Subject: All existing type rules in line with implementation (and no more red) Still to do: type rules for register aliases and relation for overloading selection --- language/l2_rules.ott | 311 +++++++++++++++++++++++++++----------------------- language/l2_typ.ott | 4 +- 2 files changed, 171 insertions(+), 144 deletions(-) diff --git a/language/l2_rules.ott b/language/l2_rules.ott index a4624527..44b74ef0 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -908,10 +908,10 @@ E_d,t |- exp'' : t' gives u'', exp''', S_N', effect' ------------------------------------------------------------ :: typed ,t |- (typ) exp : t gives exp''',I u+ ,E_t - |- letbind gives E_t1, S_N, effect, {} + |- letbind gives letbind', E_t1, S_N, effect, {} <(E_t u+ E_t1),E_d>,t |- exp : u gives exp', I2, E_t2 ------------------------------------------------------------ :: let -,t |- letbind in exp : t gives exp', u+ I2, E_t +,t |- letbind in exp : t gives letbind' in exp', u+ I2, E_t E,t1 |- exp1 : u1 gives exp1',I1,E_t1 .... E,tn |- expn : un gives expn',In,E_tn ------------------------------------------------------------ :: tup @@ -990,6 +990,30 @@ id NOTIN dom(E_t) ---------------------------------------------------------- :: wnew |- id : t gives id,Ie, {id |-> reg} +E_t(id) gives register +E_d |- typ ~> u +E_d |- u ~< t, S_N +---------------------------------------------------------- :: wregCast + |- (typ) id : t gives id,, E_t + +E_t(id) gives reg +E_d |- typ ~> u +E_d |- u ~< t, S_N +---------------------------------------------------------- :: wloclCast + |- (typ) id : t gives id,, E_t + +E_t(id) gives t +E_d |- typ ~> u +E_d |- u ~< t, S_N +---------------------------------------------------------- :: varCast + |- (typ) id : t gives id,,E_t + +id NOTIN dom(E_t) +E_d |- typ ~> t +---------------------------------------------------------- :: wnewCast + |- (typ) id : t gives id,Ie, {id |-> reg} + + E_t(id) gives E_k, S_N, Extern, t1 -> t {, wmem, } ,t1 |- exp : u1 gives exp',I,E_t1 ---------------------------------------------------------- :: wmem @@ -1005,38 +1029,40 @@ 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 -E |- lexp : vector ne5 ne6 order t gives I3,E_t ----------------------------------------------------------- :: wslice -E |- lexp [exp1 : exp2] : vector :Ne_var: 'x :Ne_var: 'x2 order t gives I1 u+ I2 u+ I3 u+ <{ne5<=ne1, ne1+ne2 <= ne3, ne3+ne4<= ne5+ne6, 'x <= ne1, 'x2 <= ne2+ne3+ne4},pure> ,E_t +E,atom |- exp1 : u1 gives exp1',I1,E_t +E,atom |- exp2 : u2 gives exp2',I2,E_t +E |- lexp : vector gives lexp',I3,E_t +---------------------------------------------------------- :: wsliceInc +E |- lexp [exp1 : exp2] : vector< ne1 ne2 + (-ne1) inc t> gives lexp'[exp1':exp2'],I1 u+ I2 u+ I3 u+ <{ne3<=ne1, ne3+ne4<= ne2 + (-ne1)},pure> ,E_t + +E,atom |- exp1 : u1 gives exp1',I1,E_t +E,atom |- exp2 : u2 gives exp2',I2,E_t +E |- lexp : vector gives lexp',I3,E_t +---------------------------------------------------------- :: wsliceDec +E |- lexp [exp1 : exp2] : vector< ne1 ne2 + (-ne1) inc t> gives lexp'[exp1':exp2'],I1 u+ I2 u+ I3 u+ <{ne1<=ne3, ne3 + (-ne4)<= ne1 + (-ne2)},pure> ,E_t -E |- exp1 : enum ne1 ne2 order gives I1,E_t -E |- exp2 : enum ne3 ne4 order gives I2,E_t -E |- lexp : vector ne5 ne6 order t gives I3,E_t ----------------------------------------------------------- :: wslice_spread -E |- lexp [exp1 : exp2] : t gives I1 u+ I2 u+ I3 u+ <{ne5<=ne1, ne1+ne2 <= ne3, ne3+ne4<= ne5+ne6},pure> ,E_t -E_r (id'' t_args) gives id : t -> |- lexp : id'' t_args gives I,E_t +E_r (x) gives id : t +> |- lexp : x gives lexp',I,E_t ---------------------------------------------------------- :: wrecord -> |- lexp.id : t gives I,E_t +> |- lexp.id : t gives lexp'.id,I,E_t defn -E |- letbind gives E_t , S_N , effect , E_k :: :: check_letbind :: check_letbind_ +E |- letbind gives letbind' , E_t , S_N , effect , E_k :: :: check_letbind :: check_letbind_ {{ com Build the environment for a let binding, collecting index constraints }} by - |- typschm ~> t,E_k2,S_N -> |- pat : t gives E_t1, S_N1 -> |- exp : t gives ,E_t2 + |- typschm ~> t,E_k2,S_N +>,t |- pat : u gives pat',E_t1, S_N1 +>,t |- exp : u' gives exp', ,E_t2 + |- u' ~< u, S_N3 ------------------------------------------------------------ :: val_annot -> |- let typschm pat = exp gives E_t1, S_N u+ S_N1 u+ S_N2, effect, E_k2 +> |- let typschm pat = exp gives let typschm pat' = exp', E_t1, S_N u+ S_N1 u+ S_N2 u+ S_N3, effect, E_k2 - |- pat : t gives E_t1,S_N1 -<(E_t u+ E_t1),E_d> |- exp : t gives ,E_t2 +,t |- pat : u gives pat',E_t1,S_N1 +<(E_t u+ E_t1),E_d>,u |- exp : u' gives exp',,E_t2 ------------------------------------------------------------ :: val_noannot - |- let pat = exp gives E_t1, S_N1 u+ S_N2, effect,{} + |- let pat = exp gives let pat' = exp', E_t1, S_N1 u+ S_N2, effect,{} defns check_defs :: '' ::= @@ -1046,137 +1072,139 @@ E_d |- type_def gives E :: :: check_td :: check_td_ {{ com Check a type definition }} by -%Does abbrev need a type environment? Ouch if yes -E_d |- typschm ~> t,E_k1,S_N +E_d |- typschm ~> t,E_k,S_N ----------------------------------------------------------- :: abbrev -E_d |- typedef id name_scm_opt = typschm gives <{},<{id |-> K_Abbrev t},{},{}>> +E_d |- typedef id name_scm_opt = typschm gives <{},<{},{id |-> E_k, S_N, None,t},{},{}>> E_d |- typ1 ~> t1 .. E_d |- typn ~> tn -E_r = { {id1:t1, .., idn:tn} |-> id } +E_r == { {id1:t1, .., idn:tn} |-> x } ----------------------------------------------------------- :: unquant_record -E_d |- typedef id name_scm_opt = const struct { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<{id |-> K_Typ},E_r,{}>> +E_d |- typedef x name_scm_opt = const struct { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<{x |-> K_Typ},{},E_r,{}>> - |- quant_itemi ~>E_ki, S_Ni//i/> -,E_r,E_e> |- typ1 ~> t1 .. ,E_r,E_e> |- typn ~> tn -{ id'1 |-> k1, .. ,id'm |-> km } = u+ -E_r1 = { {id1:t1, .., idn:tn} |-> {id'1 |-> k1, ..,id'm |-> km}, u+, None, id :t_arg_typ: id'1 .. :t_arg_typ: id'm } -E_k1' = { id |-> K_Lam (k1 .. km -> K_Typ) } + |- quant_itemi ~>E_ki, S_Ni//i/> +,E_a,E_r,E_e> |- typ1 ~> t1 .. ,E_a,E_r,E_e> |- typn ~> tn +{ x'1 |-> k1, .. ,x'm |-> km } == u+ +E_r1 == { {id1:t1, .., idn:tn} |-> {x'1 |-> k1, ..,x'm |-> km}, u+, None, x< :t_arg_typ: x'1 .. :t_arg_typ: x'm> } +E_k1' == { x |-> K_Lam (k1 .. km -> K_Typ) } ----------------------------------------------------------- :: quant_record - |- typedef id name_scm_opt = const struct forall . { typ1 id1 ; .. ; typn idn semi_opt } gives <{},> + |- typedef x name_scm_opt = const struct forall . { typ1 id1 ; .. ; typn idn semi_opt } gives <{},> -E_t = { id1 |-> t1 -> :T_id: id pure Ctor {}, ..., idn |-> tn -> :T_id: id pure Ctor {} } -E_k1 = { id |-> K_Typ } - |- typ1 ~> t1 ... |- typn ~> tn +E_t == { id1 |-> {},{},Ctor,t1 -> x pure , ..., idn |-> {},{},Ctor, tn -> x pure } +E_k1 == { x |-> K_Typ } + |- typ1 ~> t1 ... |- typn ~> tn ------------------------------------------------------------ :: unquant_union - |- typedef id name_scm_opt = const union { typ1 id1 ; ... ; typn idn semi_opt } gives > - - |- quant_itemi ~> E_ki, S_Ni//i/> -{ id'1 |-> k1, ... , id'm |-> km } = u+ -E_k' = { id |-> K_Lam (k1 ... km -> K_Typ) } u+ - |- typ1 ~> t1 ... |- typn ~> tn -t = id :t_arg_typ: id'1 ... :t_arg_typ: id'm -E_t = { id1 |-> E_k', u+, Ctor, t1 -> t pure Ctor {}, ... , idn |-> E_k', u+, Ctor, tn -> t pure Ctor {} } + |- typedef x name_scm_opt = const union { typ1 id1 ; ... ; typn idn semi_opt } gives > + + |- quant_itemi ~> E_ki, S_Ni//i/> +{ x'1 |-> k1, ... , x'm |-> km } == u+ +E_k' == { x |-> K_Lam (k1 ... km -> K_Typ) } u+ + |- typ1 ~> t1 ... |- typn ~> tn +t == x < :t_arg_typ: x'1 ... :t_arg_typ: x'm> +E_t == { id1 |-> E_k', u+, Ctor, t1 -> t pure, ... , idn |-> E_k', u+, Ctor, tn -> t pure } ------------------------------------------------------------ :: quant_union - |- typedef id name_scm_opt = const union forall . { typ1 id1 ; ... ; typn idn semi_opt } gives > + |- typedef id name_scm_opt = const union forall . { typ1 id1 ; ... ; typn idn semi_opt } gives > % Save these as enumerations for coercion -E_t = {id1 |-> id, ..., idn |-> id} -E_e = { id |-> { num1 |-> id1 ... numn |-> idn} } +E_t == {id1 |-> x, ..., idn |-> x} +E_e == { x |-> { num1 |-> id1 ... numn |-> idn} } ------------------------------------------------------------- :: enumerate -E_d |- typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } gives K_Typ},{},E_e>> +E_d |- typedef x name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } gives K_Typ},{},{},E_e>> defn -E |- fundef gives E_t , S_N :: :: check_fd :: check_fd_ +E |- fundef gives fundef' , E_t , S_N :: :: check_fd :: check_fd_ {{ com Check a function definition }} by -E_t(id) gives E_k',S_N',None, t1 -> t effect None S_N' +E_t(id) gives E_k',S_N',Global, t1 -> t effect E_ki,S_Ni//i/> -S_N'' = u+ -E_k' ~= -E_d1 = u+ E_d -E_d1 |- typ ~> t - |- patj : t1 gives E_tj,S_N'''j//j/> - |- expj : t gives ,E_t'j//j/> -S_N''''' = u+ -effect = u+ -S_N = resolve ( S_N' u+ S_N'' u+ S_N''''') +S_N'' == u+ +E_k' == +E_d1 == u+ E_d +E_d1 |- typ ~> u +E_d1 |- u ~< t, S_N2 +,t1 |- patj : uj gives patj',E_tj,S_N'''j//j/> +,u |- expj : u' gives expj',,E_t'j//j/> +S_N''''' == S_N2 u+ +effect == u+ +S_N == resolve ( S_N' u+ S_N'' u+ S_N''''') ------------------------------------------------------------- :: rec_function - |- function rec forall . typ effectkw effect gives E_t, S_N - -E_t(id) gives t1 -> t effect None S_N' -E_d |- typ ~> t - |- patj : t1 gives E_tj,S_N''j//j/> - |- expj : t gives ,E_t'j//j/> -effect = u+ -S_N = resolve (S_N' u+ ) + |- function rec forall . typ effectkw effect gives function rec forall . typ effectkw effect ,E_t, S_N + +E_t(id) gives E_k', S_N', Global, t1 -> t effect +E_d |- typ ~> u +E_d |- u ~< t, S_N2 +,t1 |- patj : uj gives pat',E_tj,S_N''j//j/> +,u |- expj : uj' gives expj',,E_t'j//j/> +effect == u+ +S_N == resolve (S_N2 u+ S_N' u+ ) ------------------------------------------------------------- :: rec_function2 - |- function rec typ effectkw effect gives E_t, S_N - - |- quant_itemi ~> E_ki,S_Ni//i/> -S_N' = u+ -E_k' = E_k u+ - |- typ ~> t -> |- patj : t1 gives E_tj,S_N''j//j/> -E_t' = (E_t u+ {id |-> t1 -> t effect None S_N'}) -> |- expj : t gives ,E_t'j//j/> -effect = u+ -S_N = resolve (S_N' u+ ) + |- function rec typ effectkw effect gives function rec typ effectkw effect ,E_t, S_N + + |- quant_itemi ~> E_ki,S_Ni//i/> +S_N' == u+ +E_k' == E_k u+ + |- typ ~> t +>, t1 |- patj : uj gives patj', E_tj,S_N''j//j/> +E_t' == (E_t u+ {id |-> E_k', S_N', Global, t1 -> t effect}) +>,t |- expj : u'j gives expj', ,E_t'j//j/> +effect == u+ +S_N == resolve (S_N' u+ ) ------------------------------------------------------------- :: rec_function_no_spec -> |- function rec forall . typ effectkw effect gives E_t', S_N +> |- function rec forall . typ effectkw effect gives function rec forall . typ effectkw effect , E_t', S_N E_d |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> -E_t' = (E_t u+ {id |-> t1 -> t effect None {}}) - |- expj : t gives ,E_t'j//j/> -effect = u+ -S_N = resolve (u+ ) +, t1 |- patj : uj gives patj', E_tj,S_N'j//j/> +E_t' == (E_t u+ {id |-> {}, {}, Global, t1 -> t effect}) +,t |- expj : uj' gives expj', ,E_t'j//j/> +effect == u+ +S_N == resolve (u+ ) ------------------------------------------------------------- :: rec_function_no_spec2 - |- function rec typ effectkw effect gives E_t', S_N - -t2 = t1 -> t effect None S_N' -E_t(id) gives E_k',S_N',None, t2 - |- quant_itemi ~> E_ki,S_Ni//i/> -S_N'' = u+ -E_k'' ~= - |- typ ~> t -> |- patj : t1 gives E_tj,S_N''j//j/> - t2} u+ E_tj),> |- expj : t gives ,E_t'j//j/> -S_N'''' = u+ -effect = u+ -S_N = resolve ( S_N' u+ S_N'' u+ S_N'''') + |- function rec typ effectkw effect gives function rec typ effectkw effect , E_t', S_N + +E_t(id) gives E_k',S_N',Global, t1 -> t effect + |- quant_itemi ~> E_ki,S_Ni//i/> +S_N'' == u+ +E_k'' == + |- typ ~> u + |- u ~< t, S_N2 +>, t1 |- patj : uj gives patj', E_tj,S_N''j//j/> +>,t |- expj : uj' gives expj', ,E_t'j//j/> +S_N'''' == u+ +effect == u+ +S_N == resolve ( S_N' u+ S_N'' u+ S_N'''') ------------------------------------------------------------- :: function -> |- function forall . typ effectkw effect gives E_t, S_N - -E_t(id) gives t1 -> t effect None S_N1 -E_d |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> - t1 -> t effect None S_N1} u+ E_tj),E_d> |- expj : t gives ,E_t'j//j/> -effect = u+ -S_N = resolve (S_N1 u+ ) +> |- function forall . typ effectkw effect gives function forall . typ effectkw effect , E_t, S_N + +E_t(id) gives {}, S_N1, Global, t1 -> t effect +E_d |- typ ~> u +E_d |- u ~< t, S_N2 +,t1 |- patj : uj gives patj,E_tj,S_N'j//j/> +, u |- expj : uj' gives expj', ,E_t'j//j/> +effect == u+ +S_N == resolve (S_N1 u+ S_N2 u+ ) ------------------------------------------------------------- :: function2 - |- function typ effectkw effect gives E_t, S_N - - |- quant_itemi ~> E_ki,S_Ni//i/> -S_N' = u+ -E_k'' = E_k u+ - |- typ ~> t -> |- patj : t1 gives E_tj,S_N''j//j/> -E_t' = (E_t u+ {id |-> t1 -> t effect None S_N'}) -> |- expj : t gives ,E_t'j//j/> -effect = u+ -S_N = resolve (S_N' u+ ) + |- function typ effectkw effect gives function typ effectkw effect , E_t, S_N + + |- quant_itemi ~> E_ki,S_Ni//i/> +S_N' == u+ +E_k'' == E_k u+ + |- typ ~> t +>,t1 |- patj : uj gives patj,E_tj,S_N''j//j/> +E_t' == (E_t u+ {id |-> E_k'', S_N', Global, t1 -> t effect}) +>,t |- expj : uj' gives expj', ,E_t'j//j/> +effect == u+ +S_N == resolve (S_N' u+ ) ------------------------------------------------------------- :: function_no_spec -> |- function forall . typ effectkw effect gives E_t', S_N +> |- function forall . typ effectkw effect gives function forall . typ effectkw effect , E_t', S_N E_d |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> -E_t' = (E_t u+ {id |-> t1 -> t effect None S_N}) - |- expj : t gives ,E_t'j//j/> -effect = u+ -S_N = resolve (u+ ) +,t1 |- patj : uj gives patj', E_tj,S_N'j//j/> +E_t' == (E_t u+ {id |-> {},S_N, Global, t1 -> t effect}) +,t |- expj : uj' gives exp', ,E_t'j//j/> +effect == u+ +S_N == resolve (u+ ) ------------------------------------------------------------- :: function_no_spec2 - |- function typ effectkw effect gives E_t', S_N + |- function typ effectkw effect gives function typ effectkw effect , E_t', S_N defn @@ -1186,7 +1214,7 @@ by E_d |- typschm ~> t, E_k1, S_N -------------------------------------------------------- :: val_spec - |- val typschm id gives {id |-> E_k1,S_N,None,t } + |- val typschm id gives {id |-> E_k1,S_N,Global,t } E_d |- typschm ~> t, E_k1, S_N -------------------------------------------------------- :: extern @@ -1199,7 +1227,7 @@ by E_k |- base_kind ~> k ------------------------------------------------------------ :: kind - |- default base_kind 'x gives {}, {'x |-> k default } + |- default base_kind 'x gives {}, {'x |-> k default } E_d |- typschm ~> t,E_k1,S_N ------------------------------------------------------------ :: typ @@ -1213,39 +1241,38 @@ by E_d |- type_def gives E --------------------------------------------------------- :: tdef -|- type_def gives u+ E +|- type_def gives type_def, u+ E -E |- fundef gives E_t,S_N +E |- fundef gives fundef', E_t,S_N --------------------------------------------------------- :: fdef -E |- fundef gives E u+ +E |- fundef gives fundef', E u+ -E |- letbind gives {id1 |-> t1 , .. , idn |-> tn},S_N,pure,E_k -S_N1 = resolve(S_N) +E |- letbind gives letbind', {id1 |-> t1 , .. , idn |-> tn},S_N,pure,E_k +S_N1 == resolve(S_N) --------------------------------------------------------- :: vdef -E |- letbind gives E u+ <{id1 |-> E_k,S_N,None,t1 , .. , idn |-> E_k,S_N,None,tn},empty> +E |- letbind gives letbind', E u+ <{id1 |-> E_k,S_N,None,t1 , .. , idn |-> E_k,S_N,None,tn},empty> E |- val_spec gives E_t --------------------------------------------------------- :: vspec -E |- val_spec gives E u+ +E |- val_spec gives val_spec, E u+ E_d |- default_spec gives E_t1, E_k1 --------------------------------------------------------- :: default - |- default_spec gives <(E_t u+ E_t1),E_d u+ > + |- default_spec gives default_spec, <(E_t u+ E_t1),E_d u+ > E_d |- typ ~> t ---------------------------------------------------------- :: register - |- register typ id gives <(E_t u+ {id |-> register t}),E_d> + |- register typ id gives register typ id, <(E_t u+ {id |-> register}),E_d> + +%TODO Add alias checking defn -E |- defs gives E' :: :: check_defs :: check_defs_ +E |- defs gives defs' , E' :: :: check_defs :: check_defs_ {{ com Check definitions, potentially given default environment of built-in library }} by ------------------------------------------------------------- :: empty -E |- gives E - -:check_def: E |- def gives E1 -E u+ E1 |- gives E2 +:check_def: E |- def gives def', E1 +E u+ E1 |- gives , E2 ------------------------------------------------------------ :: defs -E |- def gives E2 +E |- def gives def' , E2 diff --git a/language/l2_typ.ott b/language/l2_typ.ott index 77b956c5..d55499e0 100644 --- a/language/l2_typ.ott +++ b/language/l2_typ.ott @@ -267,10 +267,10 @@ grammar {{ hol arb }} {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }} {{ ocaml assert false }} - | E_t u- E_t1 .. E_tn :: M :: multi_set_minus + | E_t u- id1 .. idn :: M :: multi_set_minus {{ hol arb }} {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]])) - (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_t1..E_tn]]))))) }} + (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[id1..idn]]))))) }} {{ ocaml assert false }} | ( E_t1 inter .... inter E_tn ) :: M :: intersect {{ hol arb }} -- cgit v1.2.3