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_t ( id ) gives overload tinf : tinf1 ... tinfn :: :: lookup_over_t {{ com Overloaded type lookup }} | 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 select ( conformsto ( t , t' ) ) of tinflist gives tinf' :: :: selectoverload :: so_ {{ tex [[select]]_{(\textbf{conformsto} ([[t]],[[t']]))} ([[tinflist]]) [[gives]] [[tinf']] }} by 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 } ---------------------------------------------------------- :: atomRange E_d |- atom ~< range, { ne1 <= ne, ne <= ne2 } ---------------------------------------------------------- :: atom E_d |- atom ~< atom, { ne1 = ne2 } ---------------------------------------------------------- :: rangeAtom E_d |- range ~< atom<'x>, { ne1 <= 'x, 'x <= ne2 } 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 : atom < num > => num , { ne <= num, num <= ne' } ------------------------------------------------------------ :: numToVec vector |- num : atom < num > => to_vec num , { num + one <= 2**ne' } ------------------------------------------------------------ :: numbitzero bit |- numZero : atom < zero > => bitzero, {} ------------------------------------------------------------ :: numbitone bit |- numOne : atom < 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'), ,{} E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect ui == ( implicit, t0 , .. , tm ) ,(t0,..,tm) |- (exp0,..,expm) : ui' gives (exp0',..,expm'),I,E_t' E_d,t |- :E_app: id (annot, exp'0, .., exp'm) : uj gives uj', exp'',S_N',effect' ------------------------------------------------------------ :: appImplicit ,t |- :E_app: id(exp0,..,expm) : uj gives exp'', I u+ u+ , E_t E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect ,ui |- exp : ui' gives exp',I,E_t' E_d,t |- :E_app: id (exp') : uj gives uj', exp'',S_N',effect' ------------------------------------------------------------ :: app ,t |- :E_app: id(exp) : uj gives exp'', I u+ u+ , E_t E_t(id) gives overload {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u : tinf1 ... tinfn u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect ,ui |- exp : ui' gives exp',I,E_t' select (conformsto( ui', t)) of tinf1 ... tinfn gives tinf <({id |-> tinf} u+ E_t), E_d>, t |- :E_app: id (exp) : t' gives exp'',I', E_t'' ------------------------------------------------------------ :: appOverload ,t |- :E_app: id(exp) : uj gives exp'', I u+ I' u+ u+ , E_t E_t(id) gives {tid0 |-> kinf0, .. ,tidn |-> kinfn}, S_N, tag, u u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect ,ui |- (exp1,exp2) : ui' gives (exp1', exp2'), I,E_t' E_d,t |- :E_app_infix: exp1' id exp2' : uj gives uj', exp, S_N', effect' ------------------------------------------------------------ :: infix_app ,t |- :E_app_infix: exp1 id exp2 : t gives exp, I u+ u+ , E_t E_t(id) gives overload {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u : tinf1 ... tinfn u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect ,ui |- (exp1,exp2) : ui' gives (exp1', exp2'), I,E_t' select (conformsto( ui', t)) of tinf1 ... tinfn gives tinf <({id |-> tinf} u+ E_t), E_d>, t |- :E_app_infix: exp1 id exp2 : t' gives exp, I',E_t'' ------------------------------------------------------------ :: infix_appOverload ,t |- :E_app_infix: exp1 id exp2 : t gives exp, I u+ I u+ 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 : x gives exp', I,E_t E_r(x) gives >,ti |- expi : ui gives expi',Ii,E_t//i/> SUBSET |- ui ~< ti,S_N'i//i/> ------------------------------------------------------------ :: recup > ,t |- { exp with semi_opt } : x gives {exp' with }, I u+ , E_t ,t |- exp1 : u1 gives exp'1,I1,E_t' ... ,t |- expn : un gives exp'n,In,E_t' E_d |- u1 ~< t, S_N1 ... E_d |- un ~< t, S_Nn length(exp1 ... expn) == ne S_N == {ne=ne2} u+ S_N1 u+ ... u+ S_Nn ------------------------------------------------------------ :: vector E, vector |- [ exp1 , ... , expn ] : vector gives [exp'1,...,exp'n], u+ 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 : vector gives exp'1, I1,E_t E, range |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t E,range |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t ------------------------------------------------------------- :: vectorsubInc E, vector |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne >= ne4, ne <= ne'4,ne'<=ne4+ne'6,ne4 <= ne2, ne4+ne6' <= ne'2},pure>,E_t E, vector |- exp1 : vector< ne2 ne'2 dec u> gives exp'1, I1,E_t E, range |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t E,range |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t ------------------------------------------------------------- :: vectorsubDec E, vector |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector gives exp'1[exp'2:exp'3], I1 u+ I2 u+ I3 u+ <{ne <= ne4, ne >= ne'4,ne'<=ne'6+(-ne4),ne4' >= ne2, ne'6+(-ne4) <= ne'2},pure>,E_t E, vector |- 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,vector |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t E,atom |- exp1 : atom gives exp1',I1,E_t E,atom |- exp2 : atom gives exp2', I2,E_t E,vector |- exp3 : vector gives exp3',I3,E_t I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7, ne12 = ne8 + (-ne6) , ne6 + one <= ne8},pure> ------------------------------------------------------------ :: vecrangeupInc E,vector |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t E,vector |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t E,atom |- exp1 : atom gives exp1',I1,E_t E,atom |- exp2 : atom gives exp2', I2,E_t E,u |- exp3 : u' gives exp3',I3,E_t I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7 },pure> ------------------------------------------------------------ :: vecrangeupvalueInc E,vector |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t E,vector |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t E,atom |- exp1 : atom gives exp1',I1,E_t E,atom |- exp2 : atom gives exp2', I2,E_t E,vector |- exp3 : vector gives exp3',I3,E_t I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> ------------------------------------------------------------ :: vecrangeupDec E,vector |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t E,vector |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t E,atom |- exp1 : atom gives exp1',I1,E_t E,atom |- exp2 : atom gives exp2', I2,E_t E,u |- exp3 : u' gives exp3',I3,E_t I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> ------------------------------------------------------------ :: vecrangeupvalueDec E,vector |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t E_r (x) gives id : u >,t'' |- exp : x< t_args> gives exp', I,E_t E_d,t |- exp'.id : u gives t', exp1', S_N', effect ------------------------------------------------------------ :: field >,t |- exp.id : u gives exp1',I u+ ,E_t ,t'' |- exp : 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''',I u+ ,E_t |- letbind gives E_t1, S_N, effect, {} <(E_t u+ E_t1),E_d>,t |- exp : u gives exp', I2, E_t2 ------------------------------------------------------------ :: let ,t |- letbind in exp : t gives exp', u+ I2, E_t E,t1 |- exp1 : u1 gives exp1',I1,E_t1 .... E,tn |- expn : un gives expn',In,E_tn ------------------------------------------------------------ :: tup E,(t1, ...., tn) |- (exp1, .... , expn) : (u1 , .... , un) gives (exp1', ...., expn'), I1 u+ .... u+ In,E_t ,t |- exp1 : u1 gives exp1', I1,E_t1 .. ,t |- expn : un gives expn', In,E_tn E_d |- u1 ~< t,S_N1 .. E_d |- un ~< t,S_Nn ------------------------------------------------------------ :: list ,list |- [||exp1, .., expn ||] : list gives [|| exp1', .., expn' ||], u+ I1 u+ .. u+ In, E_t E,bit |- exp1 : bit gives exp1',I1,E_t' E,t |- exp2 : u1 gives exp2',I2,E_t2 E,t |- exp3 : u2 gives exp3',I3,E_t3 E_d |- u1 ~< t,S_N1 E_d |- u2 ~< t,S_N2 ------------------------------------------------------------ :: if ,t |- if exp1 then exp2 else exp3 : u gives if exp1' then exp2' else exp3', u+ I1 u+ I2 u+ I3,(E_t2 inter E_t3) ,range |- exp1 : range< ne7 ne8> gives exp1', I1,E_t ,range |- exp2 : range< ne9 ne10> gives exp2', I2,E_t ,range |- exp3 : range< ne11 ne12> gives exp3',I3,E_t <(E_t u+ {id |-> range< ne1 ne4>}),E_d>,unit |- exp4 : t gives exp4',I4,E_t' ----------------------------------------------------------- :: for ,unit |- foreach (id from exp1 to exp2 by exp3) exp4 : t gives foreach (id from exp1' to exp2' by exp3') exp4', I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure>,E_t E,t |- exp1 : u gives exp1',I1,E_t E,list |- exp2 : list gives exp2',I2,E_t ------------------------------------------------------------ :: cons E,list |- exp1 :: exp2 : list gives exp1'::exp2', I1 u+ I2,E_t t |- lit : u => exp,S_N ------------------------------------------------------------ :: lit E,t |- lit : u gives exp,,E_t ,unit |- exp : unit gives exp', I, E_t1 ------------------------------------------------------------ :: blockbase ,unit |- { exp } : unit gives {exp'}, I, E_t ,unit |- exp : unit gives exp', I1, E_t1 <(E_t u+ E_t1),E_d>,unit |- { } : unit gives {}, I2, E_t2 ------------------------------------------------------------ :: blockrec ,unit |- { exp ; } : unit gives {exp'; }, I1 u+ I2, E_t ,unit |- exp : unit gives exp', I, E_t1 ------------------------------------------------------------ :: nondetbase ,unit |- nondet { exp } : unit gives {exp'}, I, E_t ,unit |- exp : unit gives exp', I1, E_t1 <(E_t u+ E_t1),E_d>,unit |- nondet { } : unit gives {}, I2, E_t2 ------------------------------------------------------------ :: nondetrec ,unit |- nondet { exp ; } : unit gives {exp'; }, I1 u+ I2, E_t E,t |- exp:u gives exp', I1, E_t1 E |- lexp:t gives lexp', I2, E_t2 ------------------------------------------------------------ :: assign E,unit |- lexp := exp : unit gives lexp' := exp', I u+ I2, E_t2 defn E |- lexp : t gives lexp' , I , E_t :: :: check_lexp :: check_lexp_ {{ com Check the left hand side of an assignment }} by E_t(id) gives register ---------------------------------------------------------- :: wreg |- id : t gives id,<{},{ wreg }>, E_t E_t(id) gives reg ---------------------------------------------------------- :: wlocl |- id : t gives id,Ie, E_t E_t(id) gives t ---------------------------------------------------------- :: var |- id : t gives id,Ie,E_t id NOTIN dom(E_t) ---------------------------------------------------------- :: wnew |- id : t gives id,Ie, {id |-> reg} E_t(id) gives E_k, S_N, Extern, t1 -> t {, wmem, } ,t1 |- exp : u1 gives exp',I,E_t1 ---------------------------------------------------------- :: wmem |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ ,E_t E,atom |- exp : u gives exp',I1,E_t E |- lexp : vector gives lexp',I2,E_t ---------------------------------------------------------- :: wbitInc E |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne1 <= ne, ne1 + ne2 >= ne},pure>,E_t E,atom |- exp : u gives exp',I1,E_t E |- lexp : vector gives lexp',I2,E_t ---------------------------------------------------------- :: wbitDec E |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne <= ne1, ne1 + (-ne2) <= ne},pure>,E_t E |- exp1 : enum ne1 ne2 order gives I1,E_t E |- exp2 : enum ne3 ne4 order gives I2,E_t 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