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 | lit1 NOTEQ lit2 :: ::lit_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 order 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' => exp , S_N :: :: check_lit :: check_lit_ {{ com Typing literal constants, coercing to expected type t }} by ------------------------------------------------------------ :: num range |- num : range < num num> => num , { ne <= num, num <= ne' } ------------------------------------------------------------ :: numToVec vector |- num : range < num num> => to_vec num , { num + one <= 2**ne' } ------------------------------------------------------------ :: numbitzero bit |- numZero : range < zero zero> => bitzero, {} ------------------------------------------------------------ :: numbitone bit |- numOne : range < one one> => bitone, {} ------------------------------------------------------------- :: string string |- :L_string: string : :T_string_typ: string => :E_lit: string, {} ne == bitlength(hex) ------------------------------------------------------------ :: hex vector |- hex : vector< ne1 ne order bit> => hex, {ne=ne2} ne == bitlength(bin) ------------------------------------------------------------ :: bin vector |- bin : vector< ne1 ne order bit> => bin, {ne=ne2} ------------------------------------------------------------ :: unit unit |- () : unit => unit, {} ------------------------------------------------------------ :: bitzero bit |- bitzero : bit => bitzero, {} ------------------------------------------------------------ :: bitone bit |- bitone : bit => bitzero, {} ------------------------------------------------------------ :: undef t |- undefined : t => undefined, {} 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 NOTEQ undefined t |- lit : u => lit',S_N E_d |- u ~< t,S_N' ------------------------------------------------------------ :: lit , t |- lit : u gives lit', {}, S_N u+ S_N' ------------------------------------------------------------ :: wild E, t |- _ : t gives _, {}, {} E,t |- pat : u gives pat',E_t1,S_N id NOTIN dom(E_t1) ------------------------------------------------------------ :: as E,t |- (pat as id) : u gives (pat' as id), (E_t1 u+ {id|->t}),S_N ,t' |- pat : t gives pat', E_t1,S_N E_t(id) gives {}, {}, Default, t' E_d |- t' ~< u,S_N' ------------------------------------------------------------ :: asDefault ,u |- (pat as id) : t gives (pat' as id), (E_t1 u+ {id|->t'}),S_N u+ S_N' E_d |- typ ~> t ,t |- pat : t gives pat',E_t1,S_N ------------------------------------------------------------ :: typ ,u |- (typ) pat : t gives pat',E_t1,S_N E_t(id) gives {tid1 |-> kinf1 , .. , tidm|-> kinfm}, S_N, Ctor, (u'1,..,u'n) -> x < t_arg1 .. t_argm > pure (u1,..,un) -> x pure == (u'1,..,u'n) -> x pure [t_arg1/tid1 .. t_argm/tidm] ,u1 |- pat1 : t1 gives pat'1,E_t1,S_N1 .. ,un |- patn : tn gives pat'n,E_tn,S_Nn disjoint doms(E_t1,..,E_tn) E_d |- x ~< t, S_N ------------------------------------------------------------ :: constr ,t |- id(pat1, .., patn) : x gives id(pat'1, ..,pat'n), u+ E_t1 .. E_tn, S_N u+ S_N1 u+ .. u+ S_Nn E_t(id) gives {tid1 |-> kinf1 , .. , tidm|-> kinfm}, S_N, Ctor, unit -> x < t_arg1 .. t_argm > pure unit -> x pure == unit -> x pure [t_arg1/tid1 .. t_argm/tidm] E_d |- x ~< t, S_N ------------------------------------------------------------- :: identConstr , t |- :P_id: id : t gives :P_id: id, {}, S_N E_t(id) gives {},{},Default,t E_d |- t ~< u, S_N ------------------------------------------------------------ :: varDefault ,u |- :P_id: id : t gives :P_id: id, (E_t u+ {id|->t}),S_N ------------------------------------------------------------ :: var ,t |- :P_id: id : t gives :P_id: id, (E_t u+ {id|->t}),{} E_r() gives x< t_args>, () >,ti |- pati : ui gives pat'i, E_ti,S_Ni//i/> disjoint doms() |- x ~< t,S_N ------------------------------------------------------------ :: record >,t |- { semi_opt } : x gives { semi_opt }, :E_t_multi_union: u+ , S_N u+ ,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... ,t |- patn : un gives pat'n, E_tn,S_Nn disjoint doms(E_t1, ... ,E_tn) E_d |- u1 ~< t,S_N'1 ... E_d |- un ~< t,S_N'n ne4==length(pat1 ... patn) S_N ==S_N1 u+ ... u+ S_Nn S_N' == S_N'1 u+ ... u+ S_N'n ----------------------------------------------------------- :: vector , vector |- [ pat1, ..., patn ] : vector< ne3 ne4 order u> gives [ pat'1, ..., pat'n ], (E_t1 u+ ... u+ E_tn), S_N u+ S_N' u+ {ne2=ne4} ,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... ,t |- patn : un gives pat'n, E_tn,S_Nn E_d |- u1 ~< t,S_N'1 ... E_d |- un ~< t,S_N'n ne4 == length(pat1 ... patn) disjoint doms(E_t1 , ... , E_tn) num1 lt ... lt numn S_N == S_N1 u+ ... u+ S_Nn S_N' == S_N'1 u+ ... u+ S_N'n ----------------------------------------------------------- :: indexedVectorInc , vector |- [ num1 = pat1 , ... , numn = patn ] : vector< ne3 ne4 inc t> gives [num1 = pat'1 , ... , numn = pat'n], (E_t1 u+ ... u+ E_tn), {ne1<=num1, ne2 >= ne4} u+ S_N1 u+ ... u+ S_Nn ,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... ,t |- patn : un gives pat'n, E_tn,S_Nn E_d |- u1 ~< t,S_N'1 ... E_d |- un ~< t,S_N'n ne4 == length(pat1 ... patn) disjoint doms(E_t1 , ... , E_tn) num1 gt ... gt numn S_N == S_N1 u+ ... u+ S_Nn S_N' == S_N'1 u+ ... u+ S_N'n ----------------------------------------------------------- :: indexedVectorDec , vector |- [ num1 = pat1 , ... , numn = patn ] : vector< ne3 ne4 dec t> gives [num1 = pat'1 , ... , numn = pat'n], (E_t1 u+ ... u+ E_tn), {ne1>=num1, ne2 >= ne4} u+ S_N1 u+ ... u+ S_Nn , vector |- pat1 : vector< ne''1 ne'1 order u1> gives pat'1, E_t1,S_N1 ... , vector |- pat1 : vector< ne''n ne'n order u1> gives pat'n, E_tn,S_Nn E_d |- u1 ~< t,S_N'1 ... E_d |- un ~< t,S_N'n disjoint doms(E_t1 , ... , E_tn) S_N == S_N1 u+ ... u+ S_Nn S_N' == S_N'1 u+ ... u+ S_N'n ----------------------------------------------------------- :: vectorConcat , vector |- pat1 : ... : patn : vector gives pat'1 : ... : pat'n, (E_t1 u+ ... u+ E_tn),{ne'1 + ... + ne'n <= ne2} u+ S_N u+ S_N' E,t1 |- pat1 : u1 gives pat'1,E_t1,S_N1 .... E,tn |- patn : un gives pat'n,E_tn,S_Nn disjoint doms(E_t1,....,E_tn) ------------------------------------------------------------ :: tup E,(t1, .... , tn) |- (pat1, ...., patn) : (u1 , .... , un) gives (pat'1, .... , pat'n), (E_t1 u+ .... u+ E_tn),S_N1 u+ .... u+ S_Nn ,t |- pat1 : u1 gives pat'1,E_t1,S_N1 .. ,t |- patn : un gives pat'n,E_tn,S_Nn disjoint doms(E_t1,..,E_tn) E_d |- u1 ~< t,S_N'1 .. E_d |- un ~< t,S_N'n disjoint doms(E_t1 , .. , E_tn) S_N == S_N1 u+ .. u+ S_Nn S_N' == S_N'1 u+ .. u+ S_N'n ------------------------------------------------------------ :: list , list |- [||pat1, .., patn ||] : list< t> gives [|| pat'1, .. , pat'n ||],(E_t1 u+ .. u+ E_tn),S_N u+ S_N' 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 E_t(id) gives {tid0|->kinf0, .., tidn |-> kinfn}, {},Ctor, unit -> x pure u == x [ t_arg0/tid0 .. t_argn/tidn] E_d |- u ~< t,S_N ----------------------------------------------------------- :: unaryCtor ,t |- id : x gives id, ,{} E_t(id) gives {}, {},tag,u E_d,t |- id : u gives t', exp, S_N, effect ------------------------------------------------------------ :: localVar ,t |- id : u gives id, ,{} E_t(id) gives {tid1|->kinf1, .., tidn |-> kinfn}, S_N,tag,u' u == u'[t_arg1/tid1 .. t_argn/tidn] E_d,t |- id : u gives t', exp, S_N', effect ------------------------------------------------------------ :: otherVar ,t |- id : u gives id,,{} E_t(id) gives {tid0|->kinf0, .., tidn |-> kinfn}, {},Ctor, t'' -> x pure t' -> u pure == t'' -> x pure [ t_arg0/tid0 .. t_argn/tidn] E_d |- u ~< t,S_N ,t' |- exp : u' gives exp, ,E_t' ------------------------------------------------------------ :: ctor ,t |- :E_app: id(exp) : t gives :E_app: id(exp'), ,{} % 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 x, >,ti |- expi : ui gives exp'i,,E_t//i/> |- ui ~< ti,S_N'i//i/> S_N == u+ 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/> SUBSET |- ui ~< ti,S_N'i//i/> ------------------------------------------------------------ :: recup > ,t |- { exp with semi_opt } : id t_args 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 ------------------------------------------------------------ :: vector E, vector |- [ exp1 , ... , expn ] : vector gives [exp'1,...,exp'n], I1 u+ ... u+ In, 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, 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, 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 |- exp1 : 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 |- exp : vector< ne1 ne2 inc u> gives exp',I,E_t E, range |- exp1 : range gives exp'1,I1,E_t E,t |- exp2 : u gives exp'2,I2,E_t ------------------------------------------------------------ :: vectorupInc E, vector |- [ exp with exp1 = exp2 ] : vector< ne1 ne2 inc u> gives [exp' with exp'1 = exp'2], I u+ I1 u+ I2 u+ <{ne1 <= ne3, ne2 >= ne4},pure>,E_t E, vector |- exp : vector gives exp',I,E_t E, range |- exp1 : range gives exp'1,I1,E_t 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_d,t |- exp'.id : u gives t', exp1', S_N', effect ------------------------------------------------------------ :: field >,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/> ,t |- expi : u''i gives exp'i,Ii,E_t'i//i/> ------------------------------------------------------------ :: case ,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,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 |- 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