From 00fba411174ee2c273daa15ac0c72ff72ff47138 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Fri, 8 Nov 2013 18:35:02 +0000 Subject: Type system, almost certainly has omissions or flaws I've forgotten, but seems to be complete. Will update with corrections as necessary during implementation phase. --- language/l2_rules.ott | 503 +++++++++++++++++++++++++++++--------------------- 1 file changed, 291 insertions(+), 212 deletions(-) diff --git a/language/l2_rules.ott b/language/l2_rules.ott index 26bd899b..696c8509 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -23,6 +23,7 @@ t , u :: 'T_' ::= {{ phantom }} | ( t1 * .... * tn ) :: :: tup | id t_args :: :: app | register t_args :: :: reg_app + | t [ t1 / id1 ... tn / idn ] :: :: subst tag :: 'Tag_' ::= {{ phantom }} {{ com Data indicating where the identifier arises and thus information necessary in compilation }} @@ -160,18 +161,24 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }} | Ie :: :: Iempty {{ com Empty constraints, effects }} {{ tex {\ottnt{I}_{\epsilon} } }} | I1 u+ .. u+ In :: :: Iunion {{ com Unions the constraints and effects }} - E :: '' ::= {{ phantom }} + E :: '' ::= {{ hol ((string,env_body) fmaptree) }} {{ lem env }} - {{ com Environments }} - | < E_t , E_r , E_k > :: :: E + {{ com Definition environment and lexical environment }} + | < E_t , E_d > :: :: E {{ hol arb }} - {{ lem (Env [[E_k]] [[E_r]] [[E_t]]) }} + {{ lem (Env [[E_t]] [[E_d]] }} | empty :: M :: E_empty {{ hol arb }} {{ lem EnvEmp }} {{ ocaml assert false }} | E u+ E' :: :: E_union + + E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::= + {{ com Environments storing top level information, such as defined records, enumerations, and kinds }} + | < E_k , E_r , E_e > :: :: base + | empty :: :: empty + | E_d u+ E_d' :: :: union kinf :: 'kinf_' ::= {{ com Whether a kind is default or from a local binding }} @@ -242,6 +249,14 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }} {{ lem (List.fold_right union_map [[E_r1..E_rn]] Pmap.empty) }} {{ ocaml (assert false) }} + enumerate_map :: '' ::= + | { num1 |-> id1 ... numn |-> idn } :: :: enum_map + + E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::= + {{ com Enumeration environments }} + | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn } :: :: base + | E_e1 u+ .. u+ E_en :: :: union + ts :: ts_ ::= {{ phantom }} | t1 , .. , tn :: :: lst @@ -269,6 +284,9 @@ formula :: formula_ ::= | E_r ( t ) gives id0 : t0 .. idn : tn :: :: lookup_rt {{ com Record looup by type }} + | E_e ( t ) gives enumerate_map :: :: lookup_e + {{ com Enumeration lookup by type }} + | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset :: :: E_t_disjoint {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }} {{ lem disjoint (Pmap.domain [[E_t1]]) (Pmap.domain [[E_t2]]) }} @@ -308,7 +326,13 @@ formula :: formula_ ::= | E_r1 = E_r2 :: :: E_r_eqn {{ ichl ([[E_r1]] = [[E_r2]]) }} + + | E_e1 = E_e2 :: :: E_e_eqn + {{ ichl ([[E_e1]] = [[E_e2]]) }} + | E_d1 = E_d2 :: :: E_d_eqn + {{ ichl ([[E_d1]] = [[E_d2]]) }} + | E1 = E2 :: :: E_eqn {{ ichl ([[E1]] = [[E2]]) }} @@ -456,44 +480,44 @@ defns teq :: '' ::= defn -E_k |- t1 = t2 :: :: teq :: teq_ +E_d |- t1 = t2 :: :: teq :: teq_ {{ com Type equality }} by E_k |-t t ok ------------------------------------------------------------ :: refl -E_k |- t = t + |- t = t -E_k |- t2 = t1 +E_d |- t2 = t1 ------------------------------------------------------------ :: sym -E_k |- t1 = t2 +E_d |- t1 = t2 -E_k |- t1 = t2 -E_k |- t2 = t3 +E_d |- t1 = t2 +E_d |- t2 = t3 ------------------------------------------------------------ :: trans -E_k |- t1 = t3 +E_d |- t1 = t3 E_k(id) gives K_Abbrev u -E_k |- u = t + |- u = t ------------------------------------------------------------ :: abbrev -E_k |- id = t + |- id = t -E_k |- t1 = t3 -E_k |- t2 = t4 +E_d |- t1 = t3 +E_d |- t2 = t4 ------------------------------------------------------------ :: arrow -E_k |- t1 -> t2 effects tag = t3 -> t4 effects tag +E_d |- t1 -> t2 effects tag = t3 -> t4 effects tag -E_k |- t1 = u1 .... E_k |- tn = un +E_d |- t1 = u1 .... E_d |- tn = un ------------------------------------------------------------ :: tup -E_k |- (t1*....*tn) = (u1*....*un) +E_d |- (t1*....*tn) = (u1*....*un) E_k(id) gives K_Lam (k1 .. kn -> K_Typ) -E_k,k1 |- t_arg1 = t_arg'1 .. E_k,kn |- t_argn = t_arg'n +,k1 |- t_arg1 = t_arg'1 .. ,kn |- t_argn = t_arg'n ------------------------------------------------------------ :: app -E_k |- id t_arg1 .. t_argn = id t_arg'1 .. t_arg'n + |- id t_arg1 .. t_argn = id t_arg'1 .. t_arg'n defn -E_k , k |- t_arg = t_arg' :: :: targeq :: targeq_ by +E_d , k |- t_arg = t_arg' :: :: targeq :: targeq_ by defns convert_kind :: '' ::= @@ -505,81 +529,81 @@ defns convert_typ :: '' ::= defn -E_k |- quant_item ~> E_k1 , S_N :: :: convert_quants :: convert_quants_ +E_d |- quant_item ~> E_k1 , S_N :: :: convert_quants :: convert_quants_ {{ com Convert source quantifiers to kind environments and constraints }} by E_k |- kind ~> k ----------------------------------------------------------- :: kind -E_k |- kind id ~> {id |-> k}, {} + |- kind id ~> {id |-> k}, {} E_k(id) gives k ----------------------------------------------------------- :: nokind -E_k |- id ~> {id |-> k},{} + |- id ~> {id |-> k},{} |- nexp1 ~> ne1 |- nexp2 ~> ne2 ----------------------------------------------------------- :: eq -E_k |- nexp1 = nexp2 ~> {}, {ne1 = ne2} +E_d |- nexp1 = nexp2 ~> {}, {ne1 = ne2} |- nexp1 ~> ne1 |- nexp2 ~> ne2 ----------------------------------------------------------- :: gteq -E_k |- nexp1 >= nexp2 ~> {}, {ne1 >= ne2} +E_d |- nexp1 >= nexp2 ~> {}, {ne1 >= ne2} |- nexp1 ~> ne1 |- nexp2 ~> ne2 ----------------------------------------------------------- :: lteq -E_k |- nexp1 <= nexp2 ~> {}, {ne1 <= ne2} +E_d |- nexp1 <= nexp2 ~> {}, {ne1 <= ne2} ----------------------------------------------------------- :: in -E_k |- id IN {num1 , ... , numn} ~> {}, {id IN {num1 , ..., numn}} +E_d |- id IN {num1 , ... , numn} ~> {}, {id IN {num1 , ..., numn}} defn -E_k |- typschm ~> t , E_k2 , S_N :: :: convert_typschm :: convert_typschm_ +E_d |- typschm ~> t , E_k2 , S_N :: :: convert_typschm :: convert_typschm_ {{ com Convert source types with typeschemes to internal types and kind environments }} by -E_k |- typ ~> t +E_d |- typ ~> t ----------------------------------------------------------- :: noquant -E_k |- typ ~> t,E_k,{} +E_d |- typ ~> t,{},{} -E_k |- quant_item1 ~> E_k1, S_N1 ... E_k |- quant_itemn ~> E_kn, S_Nn -E_k u+ E_k1 u+ ... u+ E_kn |- typ ~> t +E_d |- quant_item1 ~> E_k1, S_N1 ... E_d |- quant_itemn ~> E_kn, S_Nn +E_k = E_k1 u+ ... u+ E_kn +E_d u+ |- typ ~> t ----------------------------------------------------------- :: quant -E_k |- forall quant_item1 , ... , quant_itemn . typ ~> t, E_k1 u+ ... u+ E_kn, S_N1 u+ ... u+ S_Nn +E_d |- forall quant_item1 , ... , quant_itemn . typ ~> t, E_k, S_N1 u+ ... u+ S_Nn defn -E_k |- typ ~> t :: :: convert_typ :: convert_typ_ +E_d |- typ ~> t :: :: convert_typ :: convert_typ_ {{ com Convert source types to internal types }} by E_k(id) gives K_Typ ------------------------------------------------------------ :: var -E_k |- :Typ_var: id ~> id + |- :Typ_var: id ~> id -E_k |- typ1 ~> t1 -E_k |- typ2 ~> t2 -E_k |-e effects ok +E_d |- typ1 ~> t1 +E_d |- typ2 ~> t2 ------------------------------------------------------------ :: fn -E_k |- typ1->typ2 effects ~> t1->t2 effects None +E_d |- typ1->typ2 effects ~> t1->t2 effects None -E_k |- typ1 ~> t1 .... E_k |- typn ~> tn +E_d |- typ1 ~> t1 .... E_d |- typn ~> tn ------------------------------------------------------------ :: tup -E_k |- typ1 * .... * typn ~> (t1 * .... * tn) +E_d |- typ1 * .... * typn ~> (t1 * .... * tn) E_k(id) gives K_Lam (k1..kn -> K_Typ) -E_k,k1 |- typ_arg1 ~> t_arg1 .. E_k,kn |- typ_argn ~> t_argn +,k1 |- typ_arg1 ~> t_arg1 .. ,kn |- typ_argn ~> t_argn ------------------------------------------------------------ :: app -E_k |- id typ_arg1 .. typ_argn ~> id t_arg1 .. t_argn + |- id typ_arg1 .. typ_argn ~> id t_arg1 .. t_argn -E_k |- typ ~> t1 -E_k |- t1 = t2 +E_d |- typ ~> t1 +E_d |- t1 = t2 ------------------------------------------------------------ :: eq -E_k |- typ ~> t2 +E_d |- typ ~> t2 defn -E_k , k |- typ_arg ~> t_arg :: :: convert_targ :: convert_targ_ +E_d , k |- typ_arg ~> t_arg :: :: convert_targ :: convert_targ_ {{ com Convert source type arguments to internals }} by @@ -609,23 +633,33 @@ by |- 2 ** nexp ~> 2 ** ne defn -E_k |- t :> t' , S_N :: :: coerce_typ :: coerce_typ_ by +E_d |- t :> t' , S_N :: :: coerce_typ :: coerce_typ_ by -E_k |- t = u +E_d |- t = u -------------------------------------- :: eq -E_k |- t :> u, {} +E_d |- t :> u, {} -E_k |- t1 :> u1, S_N1 .. E_k |- tn :> un, S_Nn +E_d |- t1 :> u1, S_N1 .. E_d |- tn :> un, S_Nn -------------------------------------- :: tuple -E_k |- (t1 * .. * tn) :> (u1 * .. * un), S_N1 u+ .. u+ S_Nn +E_d |- (t1 * .. * tn) :> (u1 * .. * un), S_N1 u+ .. u+ S_Nn -------------------------------------- :: enum -E_k |- enum ne1 ne2 order :> enum ne3 ne4 order, {ne3 <= ne1, ne3+ne4 >= ne1 + ne2} +E_d |- enum ne1 ne2 order :> enum ne3 ne4 order, {ne3 <= ne1, ne3+ne4 >= ne1 + ne2} + +E_e(t) gives { idi//i/> num |-> id id'j//j/> } +------------------------------------------------ :: to_enumerate + |- enum num zero order :> t, {} --------------------------------------- :: toEnum -E_k |- vector ne1 ne2 order :t_arg_typ: bit :> enum ne3 ne4 order, { ne3 = zero, ne4 = 2** ne2} +E_e(t) gives { num1 |-> id1 ... numn |-> idn } +------------------------------------------------ :: from_enumerate + |- t :> enum num1 numn + (- num1) inc, {} + +-------------------------------------- :: to_num +E_d |- vector ne1 ne2 order :t_arg_typ: bit :> enum ne3 ne4 order, { ne3 = zero, ne4 = 2** ne2} + +-------------------------------------- :: from_num +E_d |- enum ne1 ne2 order :> vector ne3 ne4 order :t_arg_typ: bit, {ne3 = zero, ne4 = 2** ne1 + ne2} -%% Will also need environment of enumerations to converte between defns check_lit :: '' ::= @@ -642,7 +676,7 @@ by |- false : bool ------------------------------------------------------------ :: num - |- num : enum num num inc + |- num : enum num zero inc ------------------------------------------------------------- :: string |- string : string @@ -679,43 +713,42 @@ E |- lit : t gives {}, {} E_k |-t t ok ------------------------------------------------------------ :: wild - |- _ : t gives {}, {} -% This case should perhaps indicate the generation of a type variable, with kind Typ +> |- _ : t gives {}, {} - |- pat : t gives E_t1,S_N +E |- 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 +E |- (pat as id) : t gives (E_t1 u+ {id|->t}),S_N - |- pat : t gives E_t1,S_N + |- pat : t gives E_t1,S_N E_t(id) gives {}, {}, Default, t ------------------------------------------------------------ :: as_default - |- (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 +E_d |- typ ~> t + |- pat : t gives E_t1,S_N ------------------------------------------------------------ :: typ - |- ( pat) : t gives E_t1,S_N + |- ( pat) : t gives E_t1,S_N 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 + |- 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 u+ E_t1 .. 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_t(id) gives {},{},Default,t ------------------------------------------------------------ :: var_default - |- :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/> +> |- pati : ti gives E_ti,S_Ni//i/> disjoint doms() ------------------------------------------------------------ :: record - |- { semi_opt } : id t_args gives :E_t_multi_union: 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) @@ -747,16 +780,15 @@ 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 - |- pat1 : t1 gives E_t1,S_N1 .... |- patn : tn gives E_tn,S_Nn +E |- pat1 : t1 gives E_t1,S_N1 .... E |- 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 +E |- (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 +E |- pat1 : t gives E_t1,S_N1 .. E |- 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 +E |- [|pat1, .., patn |] : list t gives (E_t1 u+ .. u+ E_tn),S_N1 u+ .. u+ S_Nn defns @@ -767,45 +799,56 @@ E |- exp : t gives I , E_t :: :: check_exp :: check_exp_ {{ com Typing expressions, collecting nexp constraints, effects, and new bindings }} by -E |- exp : u gives ,E_t1 -E_k |- u :> t, S_N2 + |- exp : u gives ,E_t1 +E_d |- u :> t, S_N2 ------------------------------------------------------------ :: coerce - |- exp : t gives ,E_t1 - -%% TODO::: if t is a reg, need to distinguish here between reg and ref cell access, and add to effect if reg, need to look at possible type variables introduced here and do substitutions + |- exp : t gives ,E_t1 E_t(id) gives t ------------------------------------------------------------ :: var - |- id : t gives Ie,E_t + |- id : t gives Ie,E_t + +E_t(id) gives register t +------------------------------------------------------------ :: reg + |- id : t gives <{},effect {rreg}>,E_t + +E_t(id) gives reg t +----------------------------------------------------------- :: local + |- id : t gives Ie,E_t + +E_t(id) gives { ki//i/>},S_N,tag,u +t = u [] +----------------------------------------------------------- :: ty_app + |- id : t gives ,E_t % Need to take into account possible type variables here E_t(id) gives t' -> t effect {} Ctor {} - |- exp : t' gives I,E_t + |- exp : t' gives I,E_t ------------------------------------------------------------ :: ctor - |- id exp : t gives I,E_t + |- id exp : t gives I,E_t % Need to take into account possible type variables on result of id E_t(id) gives t' -> t effects tag S_N - |- exp : t' gives I,E_t + |- exp : t' gives I,E_t ------------------------------------------------------------ :: app - |- id exp : t gives I u+ , E_t - + |- id exp : t gives I u+ , E_t + E_t(id) gives t' -> t effects tag S_N - |- (exp1,exp2) : t' gives I,E_t + |- (exp1,exp2) : t' gives I,E_t ------------------------------------------------------------ :: infix_app - |- :E_app_infix: exp1 id exp2 : t gives I u+ , E_t + |- :E_app_infix: exp1 id exp2 : t gives I u+ , E_t E_r() gives id t_args, - |- expi : ti gives Ii,E_t//i/> +> |- expi : ti gives Ii,E_t//i/> ------------------------------------------------------------ :: record - |- { semi_opt} : id t_args gives u+ , E_t +> |- { semi_opt} : id t_args gives u+ , E_t - |- exp : id t_args gives I,E_t +> |- exp : id t_args gives I,E_t E_r(id t_args) gives - |- expi : ti gives Ii,E_t//i/> +> |- expi : ti gives Ii,E_t//i/> SUBSET ------------------------------------------------------------ :: recup - |- { exp with semi_opt } : id t_args gives I u+ , E_t +> |- { exp with semi_opt } : id t_args gives I u+ , E_t E |- exp1 : t gives I1,E_t ... E |- expn : t gives In,E_t length(exp1 ... expn) = num @@ -850,24 +893,24 @@ E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I E_r (id t_args) gives id : t - |- exp : id t_args gives I,E_t +> |- exp : id t_args gives I,E_t ------------------------------------------------------------ :: field - |- exp.id : t gives I,E_t +> |- exp.id : t gives I,E_t - |- pati : t gives E_ti,S_Ni//i/> - |- expi : u gives Ii,E_t'i//i/> - |- exp : t gives I,E_t + |- pati : t gives E_ti,S_Ni//i/> + |- expi : u gives Ii,E_t'i//i/> + |- exp : t gives I,E_t ------------------------------------------------------------ :: case - |- switch exp { expi//i/> }: u gives I u+ //i/>, inter u- + |- switch exp { expi//i/> }: u gives I u+ //i/>, inter u- -E |- exp : t gives I,E_t + |- exp : t gives I,E_t ------------------------------------------------------------ :: typed - |- (typ) exp : t gives I,E_t + |- (typ) exp : t gives I,E_t - |- letbind gives E_t1, S_N, effects, {} -<(E_t u+ E_t1),E_r,E_k> |- exp : t gives I2, E_t2 + |- letbind gives E_t1, S_N, effects, {} +<(E_t u+ E_t1),E_d> |- exp : t gives I2, E_t2 ------------------------------------------------------------ :: let - |- letbind in exp : t gives u+ I2, E_t + |- letbind in exp : t gives u+ I2, E_t E |- exp1 : t1 gives I1,E_t .... E |- expn : tn gives In,E_t ------------------------------------------------------------ :: tup @@ -883,12 +926,12 @@ E |- exp3 : t gives I3,E_t3 ------------------------------------------------------------ :: if 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,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}) + |- 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}) ----------------------------------------------------------- :: 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 + |- 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_t E |- exp2 : list t gives I2,E_t @@ -897,97 +940,132 @@ E |- exp1 :: exp2 : list t gives I1 u+ I2,E_t |- lit : t ------------------------------------------------------------ :: lit - |- lit : t gives Ie,E_t + |- lit : t gives Ie,E_t - |- exp : t gives I, E_t1 + |- exp : t gives I, E_t1 ------------------------------------------------------------ :: blockbase - |- { exp } : t gives I, E_t + |- { exp } : t gives I, E_t - |- exp : u gives I1, E_t1 -<(E_t u+ E_t1),E_r,E_k> |- { } : t gives I2, E_t2 + |- exp : u gives I1, E_t1 +<(E_t u+ E_t1),E_d> |- { } : t gives I2, E_t2 ------------------------------------------------------------ :: blockrec - |- { exp ; } : t gives I1 u+ I2, E_t + |- { exp ; } : t gives I1 u+ I2, E_t -%% % defn -%% % TD , E , E_l |- funcl gives { x |-> t } , S_c , S_N :: :: check_funcl :: check_funcl_ -%% % {{ com Build the environment for a function definition clause, collecting typeclass and index constraints }} -%% % by -%% % -%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln -%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N -%% % disjoint doms(E_l1,...,E_ln) -%% % TD,E |- typ ~> u -%% % ------------------------------------------------------------ :: annot -%% % TD,E,E_l |- x l1 pat1 ... patn : typ = exp l2 gives {x |-> curry((t1 * ... * tn), u)}, S_c,S_N -%% % -%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln -%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N -%% % disjoint doms(E_l1,...,E_ln) -%% % ------------------------------------------------------------ :: noannot -%% % TD,E,E_l |- x l1 pat1 ... patn = exp l2 gives {x |-> curry((t1 * ... * tn), u)}, S_c,S_N -%% % +E |- exp:t gives I1, E_t1 +E |- lexp:t gives I2, E_t2 +------------------------------------------------------------ :: assign +E |- lexp := exp : unit gives I u+ I2, E_t2 + +defn +E |- lexp : t gives I , E_t :: :: check_lexp :: check_lexp_ +{{ com Check the left hand side of an assignment }} +by + +E_t(id) gives register t +---------------------------------------------------------- :: wreg + |- id : t gives <{},effect{ wreg }>, E_t + +E_t(id) gives reg t +---------------------------------------------------------- :: wlocl + |- id : t gives Ie, E_t + +E_t(id) gives t +---------------------------------------------------------- :: var + |- id : t gives Ie,E_t + +id NOTIN dom(E_t) +---------------------------------------------------------- :: wnew + |- id : t gives Ie, {id |-> reg t} + +E_t(id) gives t1 -> t effect {, wmem, } Extern {} + |- exp : t1 gives I,E_t1 +---------------------------------------------------------- :: wmem + |- id exp : t gives I u+ <{},effect{wmem}>,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 |- 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: id1 :Ne_var: id2 order t gives I1 u+ I2 u+ I3 u+ <{ne5<=ne1, ne1+ne2 <= ne3, ne3+ne4<= ne5+ne6, id1 <= ne1, id2 <= ne2+ne3+ne4},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 (id1 t_args) gives id : t +> |- lexp : id1 t_args gives I,E_t +---------------------------------------------------------- :: wrecord +> |- lexp.id : t gives I,E_t defn E |- letbind gives E_t , S_N , effects , E_k :: :: check_letbind :: check_letbind_ {{ com Build the environment for a let binding, collecting index constraints }} by - |- pat : t gives E_t1, S_N1 - |- exp : t gives ,E_t2 -E_k |- typschm ~> t,E_k2,S_N + |- typschm ~> t,E_k2,S_N +> |- pat : t gives E_t1, S_N1 +> |- exp : t gives ,E_t2 ------------------------------------------------------------ :: val_annot - |- let typschm pat = exp gives E_t1, S_N u+ S_N1 u+ S_N2, effects, E_k2 +> |- let typschm pat = exp gives E_t1, S_N u+ S_N1 u+ S_N2, effects, E_k2 - |- pat : t gives E_t1,S_N1 -<(E_t u+ E_t1),E_r,E_k> |- exp : t gives ,E_t2 + |- pat : t gives E_t1,S_N1 +<(E_t u+ E_t1),E_d> |- exp : t gives ,E_t2 ------------------------------------------------------------ :: val_noannot - |- let pat = exp gives E_t1, S_N1 u+ S_N2, effects,{} + |- let pat = exp gives E_t1, S_N1 u+ S_N2, effects,{} defns check_defs :: '' ::= defn -E_k1 |- type_def gives E_t , E_k , E_r :: :: check_td :: check_td_ +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_k |- typschm ~> t,E_k1,S_N +E_d |- typschm ~> t,E_k1,S_N ----------------------------------------------------------- :: abbrev -E_k |- typedef id naming_scheme_opt = typschm gives {},{id |-> K_Abbrev t},{} +E_d |- typedef id naming_scheme_opt = typschm gives <{},<{id |-> K_Abbrev t},{},{}>> -E_k |- typ1 ~> t1 .. E_k |- typn ~> tn +E_d |- typ1 ~> t1 .. E_d |- typn ~> tn E_r = { {id1:t1, .., idn:tn} |-> id } ----------------------------------------------------------- :: unquant_record -E_k |- typedef id naming_scheme_opt = const struct { typ1 id1 ; .. ; typn idn semi_opt } gives {},{id |-> K_Typ},E_r +E_d |- typedef id naming_scheme_opt = const struct { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<{id |-> K_Typ},E_r,{}>> -E_ki, S_Ni//i/> -E_k u+ |- typ1 ~> t1 .. E_k u+ |- typn ~> tn + |- 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_r = { {id1:t1, .., idn:tn} |-> {id'1 |-> k1, ..,id'm |-> km}, u+, None, id :t_arg_typ: id'1 .. :t_arg_typ: id'm } +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_record -E_k |- typedef id naming_scheme_opt = const struct forall . { typ1 id1 ; .. ; typn idn semi_opt } gives {},E_k1,E_r + |- typedef id naming_scheme_opt = const struct forall . { typ1 id1 ; .. ; typn idn semi_opt } gives <{},> E_t = { id1 |-> t1 -> :T_var: id pure Ctor {}, ..., idn |-> tn -> :T_var: id pure Ctor {} } E_k1 = { id |-> K_Typ } -E_k u+ E_k1 |- typ1 ~> t1 ... E_k u+ E_k1 |- typn ~> tn + |- typ1 ~> t1 ... |- typn ~> tn ------------------------------------------------------------ :: unquant_union -E_k |- typedef id naming_scheme_opt = const union { typ1 id1 ; ... ; typn idn semi_opt } gives E_t,E_k1,{} + |- typedef id naming_scheme_opt = const union { typ1 id1 ; ... ; typn idn semi_opt } gives > - E_ki, S_Ni//i/> + |- quant_itemi ~> E_ki, S_Ni//i/> { id'1 |-> k1, ... , id'm |-> km } = u+ E_k1 = { id |-> K_Lam (k1 ... km -> K_Typ) } u+ -E_k u+ E_k1 |- typ1 ~> t1 ... E_k u+ E_k1 |- typn ~> tn + |- typ1 ~> t1 ... |- typn ~> tn t = id :t_arg_typ: id'1 ... :t_arg_typ: id'm E_t = { id1 |-> E_k1, u+, Ctor, t1 -> t pure Ctor {}, ... , idn |-> E_k1, u+, Ctor, tn -> t pure Ctor {} } ------------------------------------------------------------ :: quant_union -E_k |- typedef id naming_scheme_opt = const union forall . { typ1 id1 ; ... ; typn idn semi_opt } gives E_t,E_k1,{} + |- typedef id naming_scheme_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} } ------------------------------------------------------------- :: enumerate -E_k |- typedef id naming_scheme_opt = enumerate { id1 ; ... ; idn semi_opt } gives E_t,{id |-> K_Typ},{} +E_d |- typedef id naming_scheme_opt = enumerate { id1 ; ... ; idn semi_opt } gives K_Typ},{},E_e>> defn E |- fundef gives E_t , S_N :: :: check_fd :: check_fd_ @@ -995,91 +1073,92 @@ E |- fundef gives E_t , S_N :: :: check_fd :: check_fd_ by E_t(id) gives E_k1,S_N1,None, t1 -> t effects None S_N1 - E_ki,S_Ni//i/> + E_ki,S_Ni//i/> S_N2 = u+ E_k1 ~= -E_k1 u+ E_k |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> - |- expj : t gives ,E_t'j//j/> +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_N3 = u+ effects = u+ S_N = resolve ( S_N1 u+ S_N2 u+ S_N3) ------------------------------------------------------------- :: rec_function - |- function rec forall . typ effects gives E_t, S_N + |- function rec forall . typ effects gives E_t, S_N E_t(id) gives t1 -> t effects None S_N1 -E_k |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> - |- expj : t gives ,E_t'j//j/> +E_d |- typ ~> t + |- patj : t1 gives E_tj,S_N'j//j/> + |- expj : t gives ,E_t'j//j/> effects = u+ S_N = resolve (S_N1 u+ ) ------------------------------------------------------------- :: rec_function2 - |- function rec typ effects gives E_t, S_N + |- function rec typ effects gives E_t, S_N - E_ki,S_Ni//i/> + |- quant_itemi ~> E_ki,S_Ni//i/> S_N1 = u+ E_k2 = E_k u+ -E_k2 |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> + |- typ ~> t +> |- patj : t1 gives E_tj,S_N'j//j/> E_t2 = (E_t u+ {id |-> t1 -> t effects None S_N1}) - |- expj : t gives ,E_t'j//j/> +> |- expj : t gives ,E_t'j//j/> effects = u+ S_N = resolve (S_N1 u+ ) ------------------------------------------------------------- :: rec_function_no_spec - |- function rec forall . typ effects gives E_t2, S_N +> |- function rec forall . typ effects gives E_t2, S_N -E_k |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> +E_d |- typ ~> t + |- patj : t1 gives E_tj,S_N'j//j/> E_t2 = (E_t u+ {id |-> t1 -> t effects None {}}) - |- expj : t gives ,E_t'j//j/> + |- expj : t gives ,E_t'j//j/> effects = u+ S_N = resolve (u+ ) ------------------------------------------------------------- :: rec_function_no_spec2 - |- function rec typ effects gives E_t2, S_N + |- function rec typ effects gives E_t2, S_N t2 = t1 -> t effects None S_N1 E_t(id) gives E_k1,S_N1,None, t2 - E_ki,S_Ni//i/> + |- quant_itemi ~> E_ki,S_Ni//i/> S_N2 = u+ E_k1 ~= -E_k1 u+ E_k |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> - t1->t effects None S_N1}) u+ E_tj),E_r,E_k u+ E_k1> |- expj : t gives ,E_t'j//j/> + |- typ ~> t +> |- patj : t1 gives E_tj,S_N'j//j/> + t2} u+ E_tj),> |- expj : t gives ,E_t'j//j/> S_N3 = u+ effects = u+ S_N = resolve ( S_N1 u+ S_N2 u+ S_N3) ------------------------------------------------------------- :: function - |- function forall . typ effects gives E_t, S_N +> |- function forall . typ effects gives E_t, S_N E_t(id) gives t1 -> t effects None S_N1 -E_k |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> - |- expj : t gives ,E_t'j//j/> +E_d |- typ ~> t + |- patj : t1 gives E_tj,S_N'j//j/> + t1 -> t effects None S_N1} u+ E_tj),E_d> |- expj : t gives ,E_t'j//j/> effects = u+ S_N = resolve (S_N1 u+ ) ------------------------------------------------------------- :: function2 - |- function rec typ effects gives E_t, S_N + |- function typ effects gives E_t, S_N - E_ki,S_Ni//i/> + |- quant_itemi ~> E_ki,S_Ni//i/> S_N1 = u+ E_k2 = E_k u+ -E_k2 |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> + |- typ ~> t +> |- patj : t1 gives E_tj,S_N'j//j/> E_t2 = (E_t u+ {id |-> t1 -> t effects None S_N1}) - |- expj : t gives ,E_t'j//j/> +> |- expj : t gives ,E_t'j//j/> effects = u+ S_N = resolve (S_N1 u+ ) ------------------------------------------------------------- :: function_no_spec - |- function rec forall . typ effects gives E_t2, S_N +> |- function forall . typ effects gives E_t2, S_N -E_k |- typ ~> t - |- patj : t1 gives E_tj,S_N'j//j/> -E_t2 = (E_t u+ {id |-> t1 -> t effects None {}}) - |- expj : t gives ,E_t'j//j/> +E_d |- typ ~> t + |- patj : t1 gives E_tj,S_N'j//j/> +E_t2 = (E_t u+ {id |-> t1 -> t effects None S_N}) + |- expj : t gives ,E_t'j//j/> effects = u+ S_N = resolve (u+ ) ------------------------------------------------------------- :: function_no_spec2 - |- function rec typ effects gives E_t2, S_N + |- function typ effects gives E_t2, S_N defn @@ -1087,26 +1166,26 @@ E |- val_spec gives E_t :: :: check_spec :: check_spec_ {{ com Check a value specification }} by -E_k |- typschm ~> t, E_k1, S_N +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,None,t } -E_k |- typschm ~> t, E_k1, S_N +E_d |- typschm ~> t, E_k1, S_N -------------------------------------------------------- :: extern - |- val extern typschm id = string gives {id |-> E_k1,S_N,Extern,t} + |- val extern typschm id = string gives {id |-> E_k1,S_N,Extern,t} defn -E_k |- default_typing_spec gives E_t , E_k1 :: :: check_default :: check_default_ +E_d |- default_typing_spec gives E_t , E_k1 :: :: check_default :: check_default_ {{ com Check a default typing specification }} by E_k |- base_kind ~> k ------------------------------------------------------------ :: kind -E_k |- default base_kind id gives {}, {id |-> k default } + |- default base_kind id gives {}, {id |-> k default } -E_k |- typschm ~> t,E_k1,S_N +E_d |- typschm ~> t,E_k1,S_N ------------------------------------------------------------ :: typ -E_k |- default typschm id gives {id |-> E_k1,S_N,Default,t},{} +E_d |- default typschm id gives {id |-> E_k1,S_N,Default,t},{} defn @@ -1114,30 +1193,30 @@ E |- def gives E' :: :: check_def :: check_def_ {{ com Check a definition }} by -E_k |- type_def gives E_t1,E_k1,E_r1 +E_d |- type_def gives E --------------------------------------------------------- :: tdef -|- type_def gives u+ +|- type_def gives u+ E E |- fundef gives E_t,S_N --------------------------------------------------------- :: fdef -E |- fundef gives E u+ +E |- fundef gives E u+ E |- letbind gives {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},{},{}> +E |- letbind gives 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 E u+ -E_k |- default_typing_spec gives E_t, E_k +E_d |- default_typing_spec gives E_t1, E_k1 --------------------------------------------------------- :: default - |- default_typing_spec gives E u+ + |- default_typing_spec gives <(E_t u+ E_t1),E_d u+ > -E_k |- typ ~> t +E_d |- typ ~> t ---------------------------------------------------------- :: register - |- register typ id gives E u+ <{id |-> register t},{},{}> + |- register typ id gives <(E_t u+ {id |-> register t}),E_d> defn E |- defs gives E' :: :: check_defs :: check_defs_ -- cgit v1.2.3