grammar formula :: formula_ ::= | judgement :: :: judgement | formula1 .. formulan :: :: dots | E_k ( tid ) gives kinf :: :: lookup_k {{ com Kind lookup }} {{ hol (FLOOKUP [[E_k]] [[tid]] = SOME [[kinf]]) }} {{ lem Map.lookup [[tid]] [[E_k]] = Just [[kinf]] }} | E_a ( tid ) gives tinf :: :: lookup_a | E_t ( id ) gives tinf :: :: lookup_t {{ com Type lookup }} {{ hol (FLOOKUP [[E_t]] [[id]] = SOME [[tinf]]) }} {{ lem Map.lookup [[id]] [[E_t]] = Just [[tinf]] }} | E_k ( tid ) <-| k :: :: update_k {{ com Update the kind associated with id to k }} {{ lem [[true]] (*TODO: update_k needs to be rewritten*) }} | E_r ( id0 .. idn ) gives t , ts :: :: lookup_r {{ com Record lookup }} {{ lem [[true]] (*TODO write a proper lookup for E_r *) }} | E_r ( t ) gives id0 : t0 .. idn : tn :: :: lookup_rt {{ com Record looup by type }} {{ lem [[true]] (* write a proper lookup for E_r *) }} | E_e ( t ) gives enumerate_map :: :: lookup_e {{ com Enumeration lookup by type }} {{ lem Map.lookup [[t]] [[E_e]] = Just [[enumerate_map]] }} | dom ( E_t1 ) inter dom ( E_t2 ) = emptyset :: :: E_t_disjoint {{ hol (DISJOINT (FDOM [[E_t1]]) (FDOM [[E_t2]])) }} {{ lem disjoint (Map.domain [[E_t1]]) (Map.domain [[E_t2]]) }} | dom ( E_k1 ) inter dom ( E_k2 ) = emptyset :: :: E_k_disjoint {{ hol (DISJOINT (FDOM [[E_f1]]) (FDOM [[E_f2]])) }} {{ lem disjoint (Map.domain [[E_f1]]) (Map.domain [[E_f2]]) }} | disjoint doms ( E_t1 , .... , E_tn ) :: :: E_x_disjoint_many {{ hol (FOLDR (\E b. case b of NONE => NONE | SOME s => if DISJOINT (FDOM E) s then SOME (FDOM E UNION s) else NONE) (SOME {}) [[E_t1....E_tn]] <> NONE) }} {{ lem disjoint_all (List.map Map.domain [[E_t1 .... E_tn]]) }} {{ com Pairwise disjoint domains }} | id NOTIN dom ( E_k ) :: :: notin_dom_k {{ hol ([[id]] NOTIN FDOM [[E_k]]) }} {{ lem Pervasives.not (Map.member [[id]] [[E_k]]) }} | id NOTIN dom ( E_t ) :: :: notin_dom_t {{ hol ([[id]] NOTIN FDOM [[E_t]]) }} {{ lem Pervasives.not (Map.member [[id]] [[E_t]]) }} | id0 : t0 .. idn : tn SUBSET id'0 : t'0 .. id'i : t'i :: :: subsetFields {{ lem ((Set.fromList [[id0 t0..idn tn]]) subset (Set.fromList [[id'0 t'0..id'i t'i]])) }} | num1 lt ... lt numn :: :: increasing | num1 gt ... gt numn :: :: decreasing | exp1 == exp2 :: :: exp_eqn {{ ichl ([[exp1]] = [[exp2]]) }} | E_k1 == E_k2 :: :: E_k_eqn {{ ichl ([[E_k1]] = [[E_k2]]) }} | E_k1 ~= E_k2 :: :: E_k_approx {{ lem ([[E_k1]] = [[E_k2]]) (* Todo, not quite equality *) }} {{ ich arb }} | E_t1 == E_t2 :: :: E_t_eqn {{ ichl ([[E_t1]] = [[E_t2]]) }} | 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]]) }} | S_N1 == S_N2 :: :: S_N_eqn {{ ichl ([[S_N1]] = [[S_N2]]) }} | id == 'id :: :: id_eq | x1 NOTEQ x2 :: :: id_neq | I1 == I2 :: :: I_eqn {{ ichl ([[I1]] = [[I2]]) }} | effect1 == effect2 :: :: Ef_eqn {{ ichl ([[effect1]] = [[effect2]]) }} | t1 == t2 :: :: t_eq {{ ichl ([[t1]] = [[t2]]) }} | ne == ne' :: :: ne_eq {{ ichl ([[ne]] = [[ne']]) }} | kid == fresh_kid ( E_d ) :: :: kid_eq {{ ichl ([[kid]] = fresh_kid [[E_d]]) }} defns check_t :: '' ::= defn E_k |-t t ok :: :: check_t :: check_t_ {{ lemwcf witness type check_t_witness; check check_t_w_check; }} {{ com Well-formed types }} by E_k('x) gives K_Typ ------------------------------------------------------------ :: var E_k |-t 'x ok E_k('x) gives K_infer E_k('x) <-| K_Typ ------------------------------------------------------------ :: varInfer E_k |-t 'x ok E_k |-t t1 ok E_k |-t t2 ok E_k |-e effect ok ------------------------------------------------------------ :: fn E_k |-t t1 -> t2 effect ok E_k |-t t1 ok .... E_k |-t tn ok ------------------------------------------------------------ :: tup E_k |-t (t1 , .... , tn) ok E_k(x) gives K_Lam(k1..kn -> K_Typ) E_k,k1 |- t_arg1 ok .. E_k,kn |- t_argn ok ------------------------------------------------------------ :: app E_k |-t x < t_arg1 .. t_argn > ok defn E_k |-e effect ok :: :: check_ef :: check_ef_ {{ com Well-formed effects }} {{ lemwcf witness type check_ef_witness; check check_ef_w_check; }} by E_k('x) gives K_Efct ----------------------------------------------------------- :: var E_k |-e 'x ok E_k('x) gives K_infer E_k('x) <-| K_Efct ------------------------------------------------------------ :: varInfer E_k |-e 'x ok ------------------------------------------------------------- :: set E_k |-e { base_effect1 , .. , base_effectn } ok defn E_k |-n ne ok :: :: check_n :: check_n_ {{ com Well-formed numeric expressions }} {{ lemwcf witness type check_n_witness; check check_n_w_check; }} by E_k('x) gives K_Nat ----------------------------------------------------------- :: var E_k |-n 'x ok E_k('x) gives K_infer E_k('x) <-| K_Nat ------------------------------------------------------------ :: varInfer E_k |-n 'x ok ----------------------------------------------------------- :: num E_k |-n num ok E_k |-n ne1 ok E_k |-n ne2 ok ----------------------------------------------------------- :: sum E_k |-n ne1 + ne2 ok E_k |-n ne1 ok E_k |-n ne2 ok ------------------------------------------------------------ :: mult E_k |-n ne1 * ne2 ok E_k |-n ne ok ------------------------------------------------------------ :: exp E_k |-n 2 ** ne ok defn E_k |-o order ok :: :: check_ord :: check_ord_ {{ com Well-formed numeric expressions }} {{ lemwcf witness type check_ord_witness; check check_ord_w_check; }} by E_k('x) gives K_Ord ----------------------------------------------------------- :: var E_k |-o 'x ok E_k('x) gives K_infer E_k('x) <-| K_Ord ------------------------------------------------------------ :: varInfer E_k |-o 'x ok defn E_k , k |- t_arg ok :: :: check_targs :: check_targs_ {{ com Well-formed type arguments kind check matching the application type variable }} {{ lemwcf witness type check_targs_witness; check check_targs_w_check; }} by E_k |-t t ok --------------------------------------------------------- :: typ E_k , K_Typ |- t ok E_k |-e effect ok --------------------------------------------------------- :: eff E_k , K_Efct |- effect ok E_k |-n ne ok --------------------------------------------------------- :: nat E_k , K_Nat |- ne ok E_k |-o order ok --------------------------------------------------------- :: ord E_k, K_Ord |- order ok defns convert_kind :: '' ::= defn E_k |- kind ~> k :: :: convert_kind :: convert_kind_ {{ lemwcf witness type convert_kind_witness; check convert_kind_w_check; }} by -------------------- :: Typ E_k |- Type ~> K_Typ defns convert_typ :: '' ::= defn E_d |- quant_item ~> E_k1 , S_N :: :: convert_quants :: convert_quants_ {{ com Convert source quantifiers to kind environments and constraints }} {{ lemwcf witness type convert_quants_witness; check convert_quants_w_check; }} by E_k |- kind ~> k ----------------------------------------------------------- :: kind |- kind 'x ~> {'x |-> k}, {} E_k('x) gives k ----------------------------------------------------------- :: nokind |- 'x ~> {'x |-> k},{} |- nexp1 ~> ne1 |- nexp2 ~> ne2 ----------------------------------------------------------- :: eq E_d |- nexp1 = nexp2 ~> {}, {ne1 = ne2} |- nexp1 ~> ne1 |- nexp2 ~> ne2 ----------------------------------------------------------- :: gteq E_d |- nexp1 >= nexp2 ~> {}, {ne1 >= ne2} |- nexp1 ~> ne1 |- nexp2 ~> ne2 ----------------------------------------------------------- :: lteq E_d |- nexp1 <= nexp2 ~> {}, {ne1 <= ne2} ----------------------------------------------------------- :: in E_d |- 'x IN {num1 , ... , numn} ~> {}, {'x IN {num1 , ..., numn}} defn E_d |- typschm ~> t , E_k , S_N :: :: convert_typschm :: convert_typschm_ {{ com Convert source types with typeschemes to internal types and kind environments }} {{ lemwcf witness type convert_typschm_witness; check convert_typschm_w_check; }} by E_d |- typ ~> t ----------------------------------------------------------- :: noquant E_d |- 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_d |- forall quant_item1 , ... , quant_itemn . typ ~> t, E_k, S_N1 u+ ... u+ S_Nn defn E_d |- typ ~> t :: :: convert_typ :: convert_typ_ {{ com Convert source types to internal types }} {{ lemwcf witness type convert_typ_witness; check convert_typ_w_check; }} by E_k('x) gives K_Typ ------------------------------------------------------------ :: var |- 'x ~> 'x E_k(x) gives K_Typ ------------------------------------------------------------ :: id |- x ~> x E_d |- typ1 ~> t1 E_d |- typ2 ~> t2 ------------------------------------------------------------ :: fn E_d |- typ1->typ2 effectkw effect ~> t1->t2 effect E_d |- typ1 ~> t1 .... E_d |- typn ~> tn ------------------------------------------------------------ :: tup E_d |- ( typ1 , .... , typn ) ~> (t1 , .... , tn) E_k(x) gives K_Lam (k1..kn -> K_Typ) ,k1 |- typ_arg1 ~> t_arg1 .. ,kn |- typ_argn ~> t_argn ------------------------------------------------------------ :: app |- x ~> x defn E_d , k |- typ_arg ~> t_arg :: :: convert_targ :: convert_targ_ {{ com Convert source type arguments to internals }} {{ lemwcf witness type convert_targ_witness; check convert_targ_w_check; }} by E_d |- typ ~> t ------------------------------------- :: typ E_d, K_Typ |- typ ~> t defn |- nexp ~> ne :: :: convert_nexp :: convert_nexp_ {{ com Convert and normalize numeric expressions }} {{ lemwcf witness type convert_nexp_witness; check convert_nexp_w_check; }} by ------------------------------------------------------------ :: var |- 'x ~> 'x ------------------------------------------------------------ :: num |- num ~> num |- nexp1 ~> ne1 |- nexp2 ~> ne2 ------------------------------------------------------------ :: mult |- nexp1 * nexp2 ~> ne1 * ne2 |- nexp1 ~> ne1 |- nexp2 ~> ne2 ----------------------------------------------------------- :: add |- nexp1 + nexp2 ~> ne1 + ne2 |- nexp ~> ne ------------------------------------------------------------ :: exp |- 2** nexp ~> 2 ** ne defn E_d |- t ~= t' :: :: conforms_to :: conforms_to_ by E_k |-t t ok ------------------------------------------------------------ :: refl |- t ~= t E_d |- t1 ~= t2 E_d |- t2 ~= t3 ------------------------------------------------------------ :: trans E_d |- t1 ~= t3 ------------------------------------------------------------ :: var E_d |- 'x ~= t ------------------------------------------------------------ :: var2 E_d |- t ~= 'x E_a(x) gives u |- u ~= t ------------------------------------------------------------ :: abbrev |- x ~= t E_a(x) gives u |- t ~= u ------------------------------------------------------------ :: abbrev2 |- t ~= x E_d |- t1 ~= u1 .... E_d |- tn ~= un ------------------------------------------------------------ :: tup E_d |- (t1,....,tn) ~= (u1,....,un) E_k(x) gives K_Lam (k1 .. kn -> K_Typ) ,k1 |- t_arg1 ~= t_arg'1 .. ,kn |- t_argn ~= t_arg'n ------------------------------------------------------------ :: app |- x ~= x x' NOTEQ x E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u |- x ~= u [ t_arg'1/tid1 .. t_arg'm/tidm ] ------------------------------------------------------------ :: appAbbrev |- x < t_arg1 .. t_argn> ~= x' x' NOTEQ x E_a(x') gives {tid1|->kinf1, .. ,tidn|->kinfn}, S_N, tag, u |- u [ t_arg1/tid1 .. t_argn/tidn ] ~= x ------------------------------------------------------------ :: appAbbrev2 |- x' < t_arg1 .. t_argn> ~= x E_d |- t ~= u ------------------------------------------------------------ :: register E_d |- register ~= u defn E_d , k |- t_arg ~= t_arg' :: :: targconforms :: targconforms_ {{ lemwcf witness type check_targeq_witness; check check_targeq_w_check; }} by E_d |- t ~= t' ------------------------------------------------------------ :: typ E_d, K_Typ |- t ~= t' ----------------------------------------------------------- :: nexp E_d, K_Nat |- ne ~= ne' defn E_d |- t ~< t' , S_N :: :: consistent_typ :: consistent_typ_ by E_k |-t t ok ------------------------------------------------------------ :: refl |- t ~< t,{} E_d |- t1 ~< t2,S_N1 E_d |- t2 ~< t3,S_N2 ------------------------------------------------------------ :: trans E_d |- t1 ~< t3, S_N1 u+ S_N2 E_a(x) gives {},S_N1,tag,u |- u ~< t,S_N ------------------------------------------------------------ :: abbrev |- x ~< t , S_N u+ S_N1 E_a(x) gives {},S_N1,tag,u |- t ~< u,S_N ------------------------------------------------------------ :: abbrev2 |- t ~< x , S_N u+ S_N1 ------------------------------------------------------------ :: var E_d |- 'x ~< t,{} ------------------------------------------------------------ :: var2 E_d |- t ~< 'x,{} E_d |- t1 ~< u1, S_N1 .... E_d |- tn ~< un, S_Nn ------------------------------------------------------------ :: tup E_d |- (t1,....,tn) ~< (u1,....,un), S_N1 u+ .... u+ S_Nn ----------------------------------------------------------- :: range E_d |- range ~< range, { ne3 <= ne1, ne2 <= ne4 } E_d |- t ~< t', S_N ---------------------------------------------------------- :: vector E_d |- vector ~< vector , {ne1=ne3,ne2=ne3} u+ S_N E_k(x) gives K_Lam (k1 .. kn -> K_Typ) ,k1 |- t_arg1 ~< t_arg'1,S_N1 .. ,kn |- t_argn ~< t_arg'n,S_Nn ------------------------------------------------------------ :: app |- x ~< x , S_N1 u+ .. u+ S_Nn x' NOTEQ x E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u |- x ~< u [ t_arg'1/tid1 .. t_arg'm/tidm ] ,S_N2 ------------------------------------------------------------ :: appAbbrev |- x < t_arg1 .. t_argn> ~< x' , S_N u+ S_N2 x' NOTEQ x E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u |- u [ t_arg'1/tid1 .. t_arg'm/tidm ] ~< x ,S_N2 ------------------------------------------------------------ :: appAbbrev2 |- x' ~< x < t_arg1 .. t_argn> , S_N u+ S_N2 defn E_d , k |- t_arg ~< t_arg' , S_N :: :: targ_consistent :: targ_consistent_ by E_d |- t ~< t', S_N ------------------------------------------------------------ :: typ E_d, K_Typ |- t ~< t',S_N ----------------------------------------------------------- :: nexp E_d, K_Nat |- ne ~< ne',{ne=ne'} defn E_d , t' |- exp : t gives t'' , exp' , S_N , effect :: :: coerce_typ :: coerce_typ_ {{ lemwcf witness type coerce_typ_witness; check coerce_typ_w_check; }} by E_d, u1 |- id1 : t1 gives u1, exp1, S_N1,effect1 .. E_d, un|- idn: tn gives un,expn, S_Nn,effectn exp' == switch exp { case (id1, .., idn) -> (exp1,..,expn) } -------------------------------------- :: tuple E_d, (u1 , .. , un) |- exp : (t1 , .. , tn) gives (u1 , .. , un), exp', S_N1 u+ .. u+ S_Nn, pure E_d |- u ~< t,S_N exp' == (annot) exp ------------------------------------------------- :: vectorUpdateStart E_d, vector< ne1 ne2 ord t > |- exp : vector gives vector , exp', S_N u+ {ne2=ne4}, pure E_d |- u ~< bit, S_N exp' == to_num exp -------------------------------------------------- :: toNum E_d, range |- exp : vector gives range, exp', S_N u+ {ne1=zero, ne2 >= 2**ne4}, pure exp' == to_vec exp -------------------------------------- :: fromNum E_d, vector |- exp: range gives vector,exp', {ne3 = zero, ne4 <= 2** ne2}, pure E_d |- typ ~> t exp' == (typ) exp E_d, u |- exp':t gives t',exp'', S_N, pure -------------------------------------- :: readReg E_d, u |- exp : register gives t', exp'', S_N, {rreg} exp' == exp[numZero] -------------------------------------- :: accessVecBit E_d, bit |- exp : vector gives bit,exp', { ne1=one},pure E_d |- range ~< range,S_N exp' == switch exp { case bitzero -> numZero case bitone -> numOne} -------------------------------------- :: bitToNum E_d, range |- exp : bit gives range, exp',S_N,pure E_d |- range ~< range,S_N exp' == switch exp { case numZero -> bitzero case numOne -> bitone } ------------------------------------- :: numToBit E_d, bit |- range : range gives bit, exp',S_N,pure E_e(x) gives { idi//i/> } exp' == switch exp { idi//i/> } ne3 == count( ) ------------------------------------------------ :: toEnumerate , x |- exp : range gives x,exp', {ne1<=zero,ne2<=ne3},pure E_e(x) gives { idi//i/> } exp' == switch exp { numi//i/> } ne3 == count( ) |- range ~< range, S_N ------------------------------------------------ :: fromEnumerate ,range |- exp: x gives range, exp', S_N,pure E_d |- t ~< u, S_N -------------------------------------- :: eq E_d, u |- exp: t gives t, exp, S_N,pure defns check_lit :: '' ::= defn t |- lit : t' => lit' , S_N :: :: check_lit :: check_lit_ {{ com Typing literal constants, coercing to expected type t }} by ------------------------------------------------------------ :: true bit |- true : bool => bitone, {} ------------------------------------------------------------ :: false bit |- false : bool => bitzero, {} ------------------------------------------------------------ :: num range |- num : range < num, zero> => num , { nexp <= num, num <= nexp' } num = 0 ------------------------------------------------------------ :: numbitzero bit |- num : range < num, zero> => bitzero, {} num = 1 ------------------------------------------------------------ :: numbitone bit |- num : range < num, zero> => bitone, {} ------------------------------------------------------------- :: string string |- string : string, {} num = bitlength(hex) ------------------------------------------------------------ :: hex |- hex : vector zero num inc :T_id: bit num = bitlength(bin) ------------------------------------------------------------ :: bin |- bin : vector zero num inc :T_id: bit ------------------------------------------------------------ :: unit |- () : unit ------------------------------------------------------------ :: bitzero |- bitzero : bit ------------------------------------------------------------ :: bitone |- bitone : bit defns check_pat :: '' ::= defn E , t |- pat : t' gives pat' , E_t , S_N :: :: check_pat :: check_pat_ {{ com Typing patterns, building their binding environment }} by |- lit : t ------------------------------------------------------------ :: lit E |- lit : t gives {}, {} E_k |-t t ok ------------------------------------------------------------ :: wild > |- _ : t gives {}, {} E |- pat : t gives E_t1,S_N id NOTIN dom(E_t1) ------------------------------------------------------------ :: as E |- (pat as id) : t gives (E_t1 u+ {id|->t}),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 E_d |- typ ~> t |- pat : t gives E_t1,S_N ------------------------------------------------------------ :: typ |- (typ) pat : t gives E_t1,S_N E_t(id) gives (t1*..*tn) -> id t_args { } 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 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}),{} E_t(id) gives {},{},Default,t ------------------------------------------------------------ :: var_default |- :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 :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 ----------------------------------------------------------- :: vector E |- [ pat1 , .. , patn ] : vector :t_arg_nexp: 'x num+'x 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: 'x :t_arg_nexp: 'x2 inc t gives (E_t1 u+ ... u+ E_tn), {'x<=num1, 'x2 >= 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: 'x :t_arg_nexp: 'x2 dec t gives (E_t1 u+ ... u+ E_tn), {'x>=num1,'x2<=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: 'x :t_arg_nexp: 'x2 inc t gives (E_t1 u+ ... u+ E_tn),{'x<=ne1,'x2>= 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: 'x :t_arg_nexp: 'x2 inc t gives (E_t1 u+ ... u+ E_tn),{'x>=ne1,'x2>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ 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 E |- (pat1, ...., patn) : (t1 * .... * tn) 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) ------------------------------------------------------------ :: list E |- [||pat1, .., patn ||] : list t gives (E_t1 u+ .. u+ E_tn),S_N1 u+ .. u+ S_Nn defns check_exp :: '' ::= defn E , t |- exp : t' gives exp' , I , E_t :: :: check_exp :: check_exp_ {{ com Typing expressions, collecting nexp constraints, effects, and new bindings }} by |- exp : u gives ,E_t1 E_d |- exp : u :> t,exp', S_N2 ------------------------------------------------------------ :: coerce |- exp : t gives ,E_t1 E_t(id) gives t ------------------------------------------------------------ :: var |- id : t gives Ie,E_t E_t(id) gives register t ------------------------------------------------------------ :: reg |- id : t gives <{},{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 {} Ctor {} |- exp : t' gives I,E_t ------------------------------------------------------------ :: ctor |- :E_app: 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 effect tag S_N |- exp : t' gives I,E_t ------------------------------------------------------------ :: app |- :E_app: id(exp) : t gives I u+ , E_t E_t(id) gives t' -> t effect tag S_N |- (exp1,exp2) : t' gives I,E_t ------------------------------------------------------------ :: infix_app |- :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/> ------------------------------------------------------------ :: record > |- { semi_opt} : id t_args gives u+ , E_t > |- exp : id t_args gives I,E_t E_r(id t_args) gives > |- expi : ti gives Ii,E_t//i/> SUBSET ------------------------------------------------------------ :: recup > |- { 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 ------------------------------------------------------------ :: vector 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_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>,E_t 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>,E_t 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: 'x :t_arg_nexp: 'x2 order t gives I1 u+ I2 u+ I3 u+ <{ne <= ne2, 'x >= ne2 , 'x <= ne2+ne2', ne2+ne'2<=ne3, ne+ne'>=ne3+ne'3, 'x2 <=ne3 + ne'3},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 : 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>,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 : t > |- exp : id t_args gives I,E_t ------------------------------------------------------------ :: field > |- 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 ------------------------------------------------------------ :: case |- switch exp { expi//i/> }: u gives I u+ //i/>, inter u- |- exp : t gives I,E_t ------------------------------------------------------------ :: typed |- (typ) exp : t gives I,E_t |- letbind gives E_t1, S_N, effect, {} <(E_t u+ E_t1),E_d> |- exp : t gives I2, E_t2 ------------------------------------------------------------ :: let |- letbind in exp : t gives u+ I2, E_t 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_t 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_t 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_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}) ----------------------------------------------------------- :: 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 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_t |- lit : t ------------------------------------------------------------ :: lit |- lit : t gives Ie,E_t |- exp : t gives I, E_t1 ------------------------------------------------------------ :: blockbase |- { exp } : t gives I, E_t |- 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 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 <{},{ 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 {, wmem, } Extern {} |- exp : t1 gives I,E_t1 ---------------------------------------------------------- :: wmem |- :LEXP_memory: id(exp) : t gives I u+ <{},{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: '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 |- 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 ---------------------------------------------------------- :: wrecord > |- lexp.id : t gives I,E_t defn E |- letbind gives 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 ------------------------------------------------------------ :: val_annot > |- let typschm pat = exp gives E_t1, S_N u+ S_N1 u+ S_N2, effect, E_k2 |- 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, effect,{} defns check_defs :: '' ::= defn 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 ----------------------------------------------------------- :: abbrev E_d |- typedef id name_scm_opt = typschm gives <{},<{id |-> K_Abbrev t},{},{}>> E_d |- typ1 ~> t1 .. E_d |- typn ~> tn E_r = { {id1:t1, .., idn:tn} |-> id } ----------------------------------------------------------- :: unquant_record E_d |- typedef id name_scm_opt = const struct { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<{id |-> 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_record |- typedef id 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 ------------------------------------------------------------ :: 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 {} } ------------------------------------------------------------ :: quant_union |- 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} } ------------------------------------------------------------- :: enumerate E_d |- typedef id 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_ {{ com Check a function definition }} by E_t(id) gives E_k',S_N',None, t1 -> t effect None S_N' 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''''') ------------------------------------------------------------- :: 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+ ) ------------------------------------------------------------- :: 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+ ) ------------------------------------------------------------- :: rec_function_no_spec > |- function rec forall . typ effectkw effect gives 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+ ) ------------------------------------------------------------- :: 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 > |- 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+ ) ------------------------------------------------------------- :: 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_no_spec > |- function forall . typ effectkw effect gives 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+ ) ------------------------------------------------------------- :: function_no_spec2 |- function typ effectkw effect gives E_t', S_N defn E |- val_spec gives E_t :: :: check_spec :: check_spec_ {{ com Check a value specification }} by E_d |- typschm ~> t, E_k1, S_N -------------------------------------------------------- :: val_spec |- val typschm id gives {id |-> E_k1,S_N,None,t } E_d |- typschm ~> t, E_k1, S_N -------------------------------------------------------- :: extern |- val extern typschm id = string gives {id |-> E_k1,S_N,Extern,t} defn E_d |- default_spec gives E_t , E_k1 :: :: check_default :: check_default_ {{ com Check a default typing specification }} by E_k |- base_kind ~> k ------------------------------------------------------------ :: kind |- default base_kind 'x gives {}, {'x |-> k default } E_d |- typschm ~> t,E_k1,S_N ------------------------------------------------------------ :: typ E_d |- default typschm id gives {id |-> E_k1,S_N,Default,t},{} defn E |- def gives def' , E' :: :: check_def :: check_def_ {{ com Check a definition }} by E_d |- type_def gives E --------------------------------------------------------- :: tdef |- type_def gives u+ E E |- fundef gives E_t,S_N --------------------------------------------------------- :: fdef 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},empty> E |- val_spec gives E_t --------------------------------------------------------- :: vspec E |- val_spec gives E u+ E_d |- default_spec gives E_t1, E_k1 --------------------------------------------------------- :: default |- default_spec gives <(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> defn E |- defs gives 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 ------------------------------------------------------------ :: defs E |- def gives E2