diff options
Diffstat (limited to 'language/l2_rules.ott')
| -rw-r--r-- | language/l2_rules.ott | 1565 |
1 files changed, 264 insertions, 1301 deletions
diff --git a/language/l2_rules.ott b/language/l2_rules.ott index 7fb54c9a..9e1b79fb 100644 --- a/language/l2_rules.ott +++ b/language/l2_rules.ott @@ -1,1461 +1,424 @@ -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_t - | E_a ( tid ) gives ne :: :: lookup_a_ne - - - | 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]]) }} +grammar - | E_k1 ~= E_k2 :: :: E_k_approx - {{ lem ([[E_k1]] = [[E_k2]]) (* Todo, not quite equality *) }} - {{ ich arb }} +mut :: 'mut_' ::= + | immutable :: :: immutable + | mutable :: :: mutable - | E_t1 == E_t2 :: :: E_t_eqn - {{ ichl ([[E_t1]] = [[E_t2]]) }} +lvar :: 'lvar_' ::= + | register typ :: :: register + | enum typ :: :: enum + | local mut typ :: :: local + | union typquant typ :: :: union + | unbound :: :: unbound + - | 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]]) }} +G {{ tex \Gamma }}, D {{ tex \Delta }} :: 'G_' ::= {{ com Type environment }} + | empty :: :: empty {{ tex \epsilon }} {{ com Empty context }} + | G , x1 : typ1 , .. , xn : typn :: :: type_list {{ com List of variables and their types }} +% | G , x1 : k1 , .. , xn : kn :: :: kind_list {{ com List of variables and their kinds }} + | G , kid1 , .. , kidn :: :: kid_list +% | G , quant_item1 , .. , quant_itemn :: :: quant_list +% | G , { nec1 , .. , necn } :: :: constraint_list {{ com Constraints }} + | G , G1 .. Gn :: :: merge {{ com Merge or disjoint union }} + | G , id : lvar :: :: add_local - | 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]]) }} +formula :: formula_ ::= + | judgement :: :: judgement + | formula1 .. formulan :: :: dots + | G ( id ) = lvar :: :: lookup_id + | G ( typ1 , id ) = typ2 :: :: lookup_record_field + | G ( typ1 ) = typ2 :: :: lookup_typ + | nexp = length [|| exp , exp1 , .. , expn ||] :: :: vector_length + | order_inc :: :: default_order_inc + | order_dec :: :: default_order_dec + | G |= nexp1 <= nexp2 :: :: prove_lteq defns -check_t :: '' ::= + declarative :: '' ::= 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 ------------------------------------------------------------ :: id -E_k |-n x ok - -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 ------------------------------------------------------------ :: minus -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; }} + G |- typ1 ~< typ2 :: :: subtype :: subtype_ + {{ com $[[typ1]]$ is a subtype of $[[typ2]]$ }} + {{ tex [[G]] \vdash [[typ1]] \preccurlyeq [[typ2]] }} 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 +----------------- :: refl +G |- typ ~< typ ------------------------------------------------------------- :: inc -E_k |-o inc ok +--------------------- :: wild +G |- _ ~< _ ------------------------------------------------------------- :: dec -E_k |-o dec 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 +------------- :: id +G |- id ~< id -E_k |-e effect ok ---------------------------------------------------------- :: eff -E_k , K_Efct |- effect ok +G |- typ1 ~< typ'1 .. G |- typn ~< typ'n +--------------------------------------------------- :: tuple +G |- (typ1 , .. , typn ) ~< (typ'1, .. , typ'n) -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; }} +G |-l lit => typ :: :: infer_lit :: infer_lit_ +{{ com Infer that type of $[[lit]]$ is $[[typ]]$ }} +{{ tex [[G]] \vdash_l [[lit]] \Rightarrow [[typ]] }} by --------------------- :: Typ -E_k |- Type ~> K_Typ -defns -convert_typ :: '' ::= +----------------------------- :: unit +G |-l () => unit -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 -<E_k,E_a,E_r,E_e> |- kind 'x ~> {'x |-> k}, {} +-------------------- :: zero +G |-l bitzero => bit -E_k('x) gives k ------------------------------------------------------------ :: nokind -<E_k,E_a,E_r,E_e> |- 'x ~> {'x |-> k},{} +-------------------- :: one +G |-l bitone => bit -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: eq -E_d |- nexp1 = nexp2 ~> {}, {ne1 = ne2} -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: gteq -E_d |- nexp1 >= nexp2 ~> {}, {ne1 >= ne2} +---------------------- :: num +G |-l num => atom < num > -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: lteq -E_d |- nexp1 <= nexp2 ~> {}, {ne1 <= ne2} ------------------------------------------------------------ :: in -E_d |- 'x IN {num1 , ... , numn} ~> {}, {'x IN {num1 , ..., numn}} +---------------------- :: true +G |-l true => bool -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+ <E_k,{},{},{}> |- typ ~> t ------------------------------------------------------------ :: quant -E_d |- forall quant_item1 , ... , quant_itemn . typ ~> t, E_k, S_N1 u+ ... u+ S_Nn +---------------------- :: false +G |-l false => bool 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; }} +G |- lexp := exp => typ -| D :: :: bind_assignment :: bind_assignment_ +{{ com Bind assignment returning updated environment }} +{{ tex [[G]] \vdash [[lexp]] := [[exp]] \Rightarrow [[typ]] \dashv [[D]] }} by - -E_k('x) gives K_Typ ------------------------------------------------------------- :: var -<E_k,E_a,E_r,E_e> |- 'x ~> 'x - -E_k(x) gives K_Typ ------------------------------------------------------------- :: id -<E_k,E_a,E_r,E_e> |- 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) -<E_k,E_a,E_r,E_e>,k1 |- typ_arg1 ~> t_arg1 .. <E_k,E_a,E_r,E_e>,kn |- typ_argn ~> t_argn ------------------------------------------------------------- :: app -<E_k,E_a,E_r,E_e> |- x <typ_arg1, .. ,typ_argn> ~> x <t_arg1 .. t_argn> + +G |- exp => typ +G |- id <= typ -| D +------------------------------- :: id +G |- id := exp => unit -| D 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; }} +G |- pat <= typ -| D :: :: bind_pat :: bind_pat_ +{{ tex [[G]] \vdash [[pat]] \Leftarrow [[typ]] \dashv [[D]] }} 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 - -------------------------------------------------------------- :: id -|- x ~> x ------------------------------------------------------------- :: var -|- 'x ~> 'x +G |- lit <= typ +------------------- :: lit +G |- lit <= typ -| G ------------------------------------------------------------- :: num -|- num ~> num +%% FIXME do add_local +G(id) = local mutable typ' +---------------------- :: local +G |- id <= typ -| G -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------- :: mult -|- nexp1 * nexp2 ~> ne1 * ne2 +G(id) = unbound +---------------------- :: unbound +G |- id <= typ -| G -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: add -|- nexp1 + nexp2 ~> ne1 + ne2 -|- nexp1 ~> ne1 -|- nexp2 ~> ne2 ------------------------------------------------------------ :: sub -|- nexp1 - nexp2 ~> ne1 - ne2 +G(id) = enum typ' +G |- typ' ~< typ +---------------------- :: enum +G |- id <= typ -| G -|- nexp ~> ne ------------------------------------------------------------- :: exp -|- 2** nexp ~> 2 ** ne -defn -E_d |-n ne ~= ne' :: :: conforms_to_ne :: conforms_to_ne_ -by - -E_k |-n ne ok ------------------------------------------------------------- :: refl -<E_k,E_a,E_r,E_e> |-n ne ~= ne - -E_d |-n ne1 ~= ne2 -E_d |-n ne2 ~= ne3 ------------------------------------------------------------- :: trans -E_d |-n ne1 ~= ne3 +---------------------- :: wild +G |- _ <= typ -| G -E_d |-n ne2 ~= ne1 -------------------------------------------------------------- :: assoc -E_d |-n ne1 ~= ne2 -E_a(x) gives ne -<E_k,E_a,E_r,E_e> |-n ne ~= ne' ------------------------------------------------------------- :: abbrev -<E_k,E_a,E_r,E_e> |-n x ~= ne' +%% FIXME Should be fold? +G |- pat1 <= typ1 -| G1 .. G |- patn <= typn -| Gn +------------------------------------------------------- :: tup +G |- (pat1 , .. , patn ) <= (typ1 , .. , typn ) -| G , G1 .. Gn -:formula_ne_eq: num == num' ------------------------------------------------------------ :: constants -E_d |-n num ~= num' ------------------------------------------------------------- :: rest -E_d |-n ne ~= ne' defn -E_d |- t ~= t' :: :: conforms_to :: conforms_to_ -{{ com Relate t and t' when t can be used where t' is expected without consideration for non-constant nats }} +G |- pat => typ -| D :: :: infer_pat :: infer_pat_ +{{ tex [[G]] \vdash [[pat]] \Leftarrow [[typ]] \dashv [[D]] }} by -E_k |-t t ok ------------------------------------------------------------- :: refl -<E_k,E_a,E_r,E_e> |- t ~= t - -E_d |- t1 ~= t2 -E_d |- t2 ~= t3 ------------------------------------------------------------- :: trans -E_d |- t1 ~= t3 +G(id) = enum typ +-------------------- :: id +G |- id => typ -| G ------------------------------------------------------------- :: var -E_d |- 'x ~= t ------------------------------------------------------------- :: var2 -E_d |- t ~= 'x +G |- pat <= typ -| D +------------------------------- :: typ +G |- (typ) pat => typ -| D -E_a(x) gives u -<E_k,E_a,E_r,E_e> |- u ~= t ------------------------------------------------------------- :: abbrev -<E_k,E_a,E_r,E_e> |- x ~= t -E_a(x) gives u -<E_k,E_a,E_r,E_e> |- t ~= u ------------------------------------------------------------- :: abbrev2 -<E_k,E_a,E_r,E_e> |- t ~= x +G |-l lit => typ +----------------------- :: lit +G |- lit => typ -| G - -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) -<E_k,E_a,E_r,E_e>,k1 |- t_arg1 ~= t_arg'1 .. <E_k,E_a,E_r,E_e>,kn |- t_argn ~= t_arg'n ------------------------------------------------------------- :: app -<E_k,E_a,E_r,E_e> |- x <t_arg1 .. t_argn> ~= x <t_arg'1 .. t_arg'n> +defn +G |-i id => typ :: :: infer_id :: infer_id_ +{{ com Infer type of indentifier }} +{{ tex [[G]] \vdash_i [[id]] \Rightarrow [[typ]] }} +by ------------------------------------------------------------- :: atom -E_d |- atom<ne> ~= range<ne1 ne2> +G(id) = local mut typ +---------------------- :: local +G |-i id => typ ------------------------------------------------------------- :: atom2 -E_d |- range<ne1 ne2> ~= atom<ne> -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u -<E_k,E_a,E_r,E_e> |- x <t_arg1 .. t_argn> ~= u [ t_arg'1/tid1 .. t_arg'm/tidm ] ------------------------------------------------------------- :: appAbbrev -<E_k,E_a,E_r,E_e> |- x < t_arg1 .. t_argn> ~= x' <t_arg'1 .. t_arg'm> +G(id) = enum typ +---------------------- :: enum +G |-i id => typ -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidn|->kinfn}, S_N, tag, u -<E_k,E_a,E_r,E_e> |- u [ t_arg1/tid1 .. t_argn/tidn ] ~= x <t_arg'1 .. t_arg'm> ------------------------------------------------------------- :: appAbbrev2 -<E_k,E_a,E_r,E_e> |- x' < t_arg1 .. t_argn> ~= x <t_arg'1 .. t_arg'm> -E_d |- t ~= u ------------------------------------------------------------- :: register -E_d |- register<t> ~= u +G(id) = register typ +---------------------- :: register +G |-i id => typ -E_d |- t ~= u ------------------------------------------------------------- :: reg -E_d |- reg<t> ~= u +G(id) = union typquant typ +------------------------------------- :: union +G |-i id => typ defn -E_d , k |- t_arg ~= t_arg' :: :: targconforms :: targconforms_ -{{ lemwcf witness type check_targeq_witness; check check_targeq_w_check; }} +G |-f exp . id => typ :: :: infer_field :: infer_field_ +{{ tex [[G]] \vdash_f [[exp]] . [[id]] \Rightarrow [[typ]] }} by -E_d |- t ~= t' ------------------------------------------------------------- :: typ -E_d, K_Typ |- t ~= t' - -E_d |-n ne ~= ne' ------------------------------------------------------------ :: nexp -E_d, K_Nat |- ne ~= ne' -defn -E_d |-c t ~= t' :: :: conforms_to_upto_coerce :: conforms_to_upto_coerce_ -{{ com Relate t and t' when t can be used where t' is expected upto applying coercions to t }} -by +G |- exp => typ1 +G ( typ1 ) = register [ id2 ] +G ( id2 ) = (base,top,ranges) +ranges ( id ) = vec_typ +---------------------------- :: register +G |-f exp . id => vec_typ -E_d |- t ~= t' -------------------------------------------------------------- :: base -E_d |-c t ~= t' -E_d |-n ne2 ~= one -------------------------------------------------------------- :: bitToVec -E_d |-c bit ~= vector<ne ne2 order bit> -E_d |-n ne2 ~= one -------------------------------------------------------------- :: vecToBit -E_d |-c vector<ne ne2 order bit> ~= bit +G |- exp => typ1 +G ( typ1 , id ) = typ +---------------------------- :: record +G |-f exp . id => typ -------------------------------------------------------------- :: vecToAtom -E_d |-c vector<ne ne2 order bit> ~= atom<ne3> -------------------------------------------------------------- :: vecToRange -E_d |-c vector<ne ne2 order bit> ~= range<ne3 ne4> +defn +G |- exp1 => n_constraint :: :: infer_flow :: infer_flow_ +by -E_e(x) gives enumerate_map -------------------------------------------------------------- :: enumToRange -<E_k,E_a,E_r,E_e> |-c x ~= range<ne1 ne2> -E_e(x) gives enumerate_map -------------------------------------------------------------- :: rangeToEnum -<E_k,E_a,E_r,E_e> |-c range<ne1 ne2> ~= x +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: lteq +G |- :E_app: lteq_atom_atom ( x , y ) => nexp1 <= nexp2 -E_e(x) gives enumerate_map -------------------------------------------------------------- :: enumToAtom -<E_k,E_a,E_r,E_e> |-c x ~= atom<ne> -E_e(x) gives enumerate_map -------------------------------------------------------------- :: atomToEnum -<E_k,E_a,E_r,E_e> |-c atom<ne> ~= x +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: gteq +G |- :E_app: gteq_atom_atom ( x , y ) => nexp1 >= nexp2 -E_d |-c t1 ~= u1 .... E_d |-c tn ~= un ------------------------------------------------------------- :: tup -E_d |-c (t1,....,tn) ~= (u1,....,un) +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: lt +G |- :E_app: lt_atom_atom ( x , y ) => nexp1 + numOne <= nexp2 -E_k(x) gives K_Lam (k1 .. kn -> K_Typ) -<E_k,E_a,E_r,E_e>,k1 |-c t_arg1 ~= t_arg'1 .. <E_k,E_a,E_r,E_e>,kn |-c t_argn ~= t_arg'n ------------------------------------------------------------- :: app -<E_k,E_a,E_r,E_e> |-c x <t_arg1 .. t_argn> ~= x <t_arg'1 .. t_arg'n> +G |- x => atom < nexp1 > +G |- y => atom < nexp2 > +---------------------------- :: gt +G |- :E_app: lteq_atom_atom ( x , y ) => nexp1 >= nexp2 + numOne -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u -<E_k,E_a,E_r,E_e> |-c x <t_arg1 .. t_argn> ~= u [ t_arg'1/tid1 .. t_arg'm/tidm ] ------------------------------------------------------------- :: appAbbrev -<E_k,E_a,E_r,E_e> |-c x < t_arg1 .. t_argn> ~= x' <t_arg'1 .. t_arg'm> +G |- id => range <nexp1 , nexp2 > +G |- y => atom < nexp > +------------------------------------------------------------------------------- :: lt_range_atom +G |- :E_app: lt_range_atom ( id , y ) => range < nexp1 , min (nexp - 1 , nexp2 ) > -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidn|->kinfn}, S_N, tag, u -<E_k,E_a,E_r,E_e> |-c u [ t_arg1/tid1 .. t_argn/tidn ] ~= x <t_arg'1 .. t_arg'm> ------------------------------------------------------------- :: appAbbrev2 -<E_k,E_a,E_r,E_e> |-c x' < t_arg1 .. t_argn> ~= x <t_arg'1 .. t_arg'm> -E_d |-c t ~= u ------------------------------------------------------------- :: register -E_d |-c register<t> ~= u -E_d |-c t ~= u ------------------------------------------------------------- :: reg -E_d |-c reg<t> ~= u defn -E_d , k |-c t_arg ~= t_arg' :: :: targconforms_coerce :: targconforms_coerce_ + G |- exp => typ :: :: infer_exp :: infer_exp_ +{{ com Infer that type of $[[exp]]$ is $[[typ]]$ }} +{{ tex [[G]] \vdash [[exp]] \Rightarrow [[typ]] }} by -E_d |-c t ~= t' ------------------------------------------------------------- :: typ -E_d, K_Typ |-c t ~= t' -E_d |-n ne ~= ne' ------------------------------------------------------------ :: nexp -E_d, K_Nat |-c ne ~= ne' +G |- exp1 <= unit ... G |- expn <= unit +------------------------------------------ :: nondet +G |- nondet { exp1 ; ... ; expn } => unit -defn -E_d |- select ( conformsto ( t , t' ) ) of tinflist gives tinflist' :: :: selectoverload :: so_ -{{ tex [[select]]_{[[conformsto]] ([[t]],[[t']])} ([[tinflist]]) [[gives]] [[tinflist']] }} -by +G |-i id => typ +---------------- :: id +G |- id => typ -E_d |- ti ~= ti' -E_d |- tj' ~= tj -E_d |- select (full(ti,tj)) of tinf0 .. tinfm tinf'0 .. tinf'n gives empty ---------------------------------------------------------- :: full -E_d |- select (full( ti, tj)) of tinf0 .. tinfm E_k,S_N,tag, ti' -> tj' effect tinf'0 .. tinf'n gives E_k,S_N,tag,ti' -> tj' -E_d |- ti ~= ti' -E_d |- select (parm(ti,tj)) of tinf0 .. tinfm gives empty --------------------------------------------------------- :: parm -E_d |- select (parm( ti, tj)) of tinf0 .. tinfm E_k,S_N,tag,ti' -> t effect tinf'0 .. tinf'n gives E_k,S_N,tag,ti' -> t +G |-l lit => typ +---------------- :: lit +G |- lit => typ -defn -E_d , widening |- t ~< t' : t'' , S_N :: :: consistent_typ :: consistent_typ_ -{{ com t is consistent with t' if they match if t can be used where t' is needed after the constraints are solved, with no coercions needed. t'' is the consistent type when widening is required }} -by -E_k |-t t ok ------------------------------------------------------------- :: refl -<E_k,E_a,E_r,E_e>,widening |- t ~< t:t,{} - -E_d,widening |- t1 ~< t3:t4, S_N1 -E_d,widening |- t4 ~< t2: t5, S_N2 ------------------------------------------------------------- :: trans -E_d,widening |- t1 ~< t2: t5, S_N1 u+ S_N2 - -E_a(x) gives {},S_N1,tag,u -<E_k,E_a,E_r,E_e>,widening |- u ~< t:t', S_N ------------------------------------------------------------- :: abbrev -<E_k,E_a,E_r,E_e>,widening |- x ~< t : t', S_N u+ S_N1 - -E_a(x) gives {},S_N1,tag,u -<E_k,E_a,E_r,E_e>,widening |- t ~< u: t', S_N' ------------------------------------------------------------- :: abbrev2 -<E_k,E_a,E_r,E_e>,widening |- t ~< x : t', S_N u+ S_N1 - ------------------------------------------------------------- :: var -E_d,widening |- 'x ~< t:t, {} - ------------------------------------------------------------- :: var2 -E_d,widening |- t ~< 'x: t, {} - -E_d,widening |- t1 ~< u1:u'1, S_N1 .... E_d,widening |- tn ~< un:u'n, S_Nn ------------------------------------------------------------- :: tup -E_d,widening |- (t1,....,tn) ~< (u1,....,un): (u'1,....,u'n), S_N1 u+ .... u+ S_Nn +----------------------------------- :: sizeof +G |- sizeof nexp => atom < nexp > ------------------------------------------------------------ :: range -E_d,widening |- range <ne1 ne2> ~< range<ne3 ne4>: range<ne3 ne4>, { ne3 <= ne1, ne2 <= ne4 } +-------------------------------------------- :: constraint +G |- constraint n_constraint => bool ----------------------------------------------------------- :: atomRange -E_d,(nums,_) |- atom <ne> ~< range<ne1 ne2>: atom<ne>, { ne1 <= ne, ne <= ne2 } +G |-f exp . id => typ +------------------------ :: field +G |- exp . id => typ ----------------------------------------------------------- :: atom -E_d,(none,_) |- atom <ne1> ~< atom<ne2>: atom<ne2>, { ne1 = ne2 } +G |- exp1 => typ1 .... G |- expn => typn +---------------------------------------------------------- :: tuple +G |- ( exp1 , .... , expn ) => (typ1 , .... , typn ) -num1 lt num2 ----------------------------------------------------------- :: atomWidenConst -E_d,(nums,_) |- atom <num1> ~< atom<num2>: range<num1 num2>, {} -num2 lt num1 ---------------------------------------------------------- :: atomWidenConst2 -E_d,(nums,_) |- atom <num1> ~< atom<num2>: range<num2 num1>, {} ----------------------------------------------------------- :: rangeAtom -E_d,widening |- range<ne1 ne2> ~< atom<'x>: atom<'x>, { ne1 <= 'x, 'x <= ne2 } -E_d,(nums,none) |- t ~< t': t'', S_N ----------------------------------------------------------- :: vector -E_d,(_,none) |- vector <ne1 ne2 order t> ~< vector <ne3 ne4 order t'>: vector<ne3 ne4 order t''>, {ne2=ne4, ne1=ne3} u+ S_N +G |- lexp := exp => typ -| D +-------------------- :: assign +G |- lexp := exp => typ -E_d,(nums,none) |- t ~< t': t'', S_N ----------------------------------------------------------- :: vectorWiden -E_d,(_,vectors) |- vector <ne1 ne2 order t> ~< vector <ne3 ne4 order t'>: vector<ne3 ne4 order t''>, {ne2=ne4} u+ S_N -E_k(x) gives K_Lam (k1 .. kn -> K_Typ) -<E_k,E_a,E_r,E_e>,widening,k1 |- t_arg1 ~< t_arg'1,S_N1 .. <E_k,E_a,E_r,E_e>,widening,kn |- t_argn ~< t_arg'n,S_Nn ------------------------------------------------------------- :: app -<E_k,E_a,E_r,E_e>,widening |- x <t_arg1 .. t_argn> ~< x <t_arg'1 .. t_arg'n>:x<t_arg'1 .. t_arg'n>, S_N1 u+ .. u+ S_Nn -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u -<E_k,E_a,E_r,E_e>,widening |- x <t_arg1 .. t_argn> ~< u [ t_arg'1/tid1 .. t_arg'm/tidm ]: t ,S_N2 ------------------------------------------------------------- :: appAbbrev -<E_k,E_a,E_r,E_e>,widening |- x < t_arg1 .. t_argn> ~< x' <t_arg'1 .. t_arg'm>: x'<t_arg'1 .. t_arg'm>, S_N u+ S_N2 +---------------------------- :: record_update +G |- lexp . id := exp => typ -x' NOTEQ x -E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u -<E_k,E_a,E_r,E_e>,widening |- u [ t_arg'1/tid1 .. t_arg'm/tidm ] ~< x <t_arg1 .. t_argn>: t ,S_N2 ------------------------------------------------------------- :: appAbbrev2 -<E_k,E_a,E_r,E_e>,widening |- x' <t_arg'1 .. t_arg'm> ~< x < t_arg1 .. t_argn> :x<t_arg1 .. t_argn>, S_N u+ S_N2 -defn -E_d , widening , k |- t_arg ~< t_arg' , S_N :: :: targ_consistent :: targ_consistent_ -by +G |- exp <= typ +----------------------- :: cast +G |- ( typ ) exp => typ -E_d,widening |- t ~< t': t'', S_N ------------------------------------------------------------- :: typ -E_d,widening, K_Typ |- t ~< t',S_N ------------------------------------------------------------ :: nexp -E_d,widening, K_Nat |- ne ~< ne',{ne=ne'} -defn -E_d , widening, 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 +G |- :E_app: id ( exp1 , exp2 ) => typ +-------------------------------- :: app_infix +G |- exp1 id exp2 => typ -E_d, widening, u1 |- id1 : t1 gives u1, exp1, S_N1,effect1 .. E_d,widening, un|- idn: tn gives un,expn, S_Nn,effectn -exp' == switch exp { case (id1, .., idn) -> (exp1,..,expn) } --------------------------------------- :: tuple -E_d, widening, (u1 , .. , un) |- exp : (t1 , .. , tn) gives (u1 , .. , un), exp', S_N1 u+ .. u+ S_Nn, pure - -E_d,(nums,vectors) |- u ~< t: t',S_N -exp' == (annot) exp -------------------------------------------------- :: vectorUpdateStart -E_d, widening, vector< ne1 ne2 order t > |- exp : vector <ne3 ne4 order u> gives vector <ne3 ne4 order t'>, exp', S_N u+ {ne2=ne4}, pure - -E_d, (none,none) |- u ~< bit:bit, S_N -exp' == to_num exp --------------------------------------------------- :: toNum -E_d,widening, range<ne1 ne2> |- exp : vector <ne3 ne4 order u> gives range<ne1 ne2>, exp', S_N u+ {ne1=zero, ne2 >= 2**ne4}, pure - -exp' == to_vec exp --------------------------------------- :: fromNum -E_d,widening, vector<ne1 ne2 order bit> |- exp: range<ne3 ne4> gives vector<ne1 ne2 order bit>,exp', {ne3 = zero, ne4 <= 2** ne2}, pure - -E_d |- typ ~> t -exp' == (typ) exp -E_d,widening, u |- exp':t gives t',exp'', S_N, pure --------------------------------------- :: readReg -E_d,widening, u |- exp : register<t> gives t', exp'', S_N, {rreg} - -exp' == :E_tup_app: msb(exp) --------------------------------------- :: accessVecBit -E_d,widening, bit |- exp : vector<ne1 ne2 order bit> gives bit,exp', { ne1=one},pure - -E_d,widening |- range<zero one> ~< range<ne1 ne2>: t,S_N -exp' == switch exp { case bitzero -> numZero case bitone -> numOne} --------------------------------------- :: bitToNum -E_d,widening, range<ne1 ne2> |- exp : bit gives range<ne1 ne2>, exp',S_N,pure - -E_d,widening |- range<ne1 ne2> ~< range<zero one>: t,S_N -exp' == switch exp { case numZero -> bitzero case numOne -> bitone } -------------------------------------- :: numToBit -E_d, widening, bit |- exp : range<ne1 ne2> gives bit, exp',S_N,pure - -E_d,(nums,none) |- atom<ne> ~< range<zero one>: t,S_N -exp' == switch exp { case numZero -> bitzero case numOne -> bitone } -------------------------------------- :: numToBitAtom -E_d,widening, bit |- exp : atom<ne> gives bit, exp',S_N,pure - -E_e(x) gives { </numi |-> idi//i/> } -exp' == switch exp { </case numi -> idi//i/> } -ne3 == count( </numi//i/>) ------------------------------------------------- :: toEnumerate -<E_k,E_a,E_r,E_e>,widening, x |- exp : range<ne1 ne2> gives x,exp', {ne1<=zero,ne2<=ne3},pure - -E_e(x) gives { </numi |-> idi//i/> } -exp' == switch exp { </case idi -> numi//i/> } -ne3 == count( </numi//i/>) -<E_k,E_a,E_r,E_e>,(nums,none) |- range<zero ne3> ~< range<ne1 ne2>:t, S_N ------------------------------------------------- :: fromEnumerate -<E_k,E_a,E_r,E_e>,widening,range<ne1 ne2> |- exp: x gives range<zero ne3>, exp', S_N,pure - -E_d,widening |- t ~< u: u', S_N --------------------------------------- :: eq -E_d,widening, u |- exp: t gives u', exp, S_N,pure +--------------------------------------- :: app +G |- :E_app: id (exp1 , .. , expn ) => typ -defns -check_lit :: '' ::= - -defn -widening , t |- lit : t' => exp , S_N :: :: check_lit :: check_lit_ -{{ com Typing literal constants, coercing to expected type t }} -by - - ------------------------------------------------------------ :: num -widening, range <ne ne'> |- num : atom < num > => num , { ne <= num, num <= ne' } - ------------------------------------------------------------ :: numToVec -widening, vector <ne ne' order bit> |- num : atom < num > => to_vec num , { num + one <= 2**ne' } +G |- exp1 => bool +G |- exp2 => unit +------------------------------- :: while_loop +G |- while exp1 do exp2 => unit - ------------------------------------------------------------ :: numbitzero -widening, bit |- numZero : atom < zero > => bitzero, {} +G |- exp1 => unit +G |- exp2 => bool +------------------------------- :: until_loop +G |- repeat exp1 until exp2 => unit - ------------------------------------------------------------ :: numbitone -widening, bit |- numOne : atom < one > => bitone, {} - - ------------------------------------------------------------- :: string -widening, string |- :L_string: string : :T_string_typ: string => :E_lit: string, {} +G |- exp1 => range <nexp1,nexp1'> +G |- exp2 => range <nexp2,nexp2'> +G |= nexp1' <= nexp2 +G |- exp3 <= int +G |- exp4 => unit +----------------------------------------------------------------------- :: for_inc +G |- foreach ( id from exp1 to exp2 by exp3 in inc ) exp4 => unit - ne == bitlength(hex) - ------------------------------------------------------------ :: hex -widening, vector<ne1 ne2 order bit> |- hex : vector< ne1 ne order bit> => hex, {ne=ne2} +G |- exp1 => range <nexp1,nexp1'> +G |- exp2 => range <nexp2,nexp2'> +G |= nexp2' <= nexp1 +G |- exp3 <= int +G |- exp4 => unit +----------------------------------------------------------------------- :: for_dec +G |- foreach ( id from exp1 to exp2 by exp3 in dec ) exp4 => unit -ne == bitlength(bin) - ------------------------------------------------------------ :: bin -widening,vector<ne1 ne2 order bit> |- bin : vector< ne1 ne order bit> => bin, {ne=ne2} - ------------------------------------------------------------ :: unit -widening, unit |- () : unit => unit, {} +G |- foreach ( id from exp1 to exp2 by exp3 in inc) exp4 => typ +----------------------------------------------------------------------- :: forup +G |- foreach ( id from exp1 to exp2 by exp3 ) exp4 => typ - ------------------------------------------------------------ :: bitzero -widening, bit |- bitzero : bit => bitzero, {} - ------------------------------------------------------------ :: bitone -widening, bit |- bitone : bit => bitzero, {} +G |- foreach ( id from exp1 to exp2 by numOne in inc) exp3 => typ +----------------------------------------------------------------------- :: forupbyone +G |- foreach ( id from exp1 to exp2 ) exp3 => typ ------------------------------------------------------------- :: undef -widening, 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 +G |- foreach ( id from exp1 to exp2 by exp3 in dec) exp4 => typ +--------------------------------------------------------------------------- :: fordown +G |- foreach ( id from exp1 downto exp2 by exp3 ) exp4 => typ -lit NOTEQ undefined -(none,none),t |- lit : u => lit',S_N -E_d,(nums,none) |- u ~< t: t', S_N' ------------------------------------------------------------- :: lit -<E_t,E_d>, t |- lit : t' 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 - -E_t(id) gives {}, {}, Default, t' -<E_t,E_d>,t' |- pat : t gives pat', E_t1,S_N -E_d,(none,none) |- t' ~< u : u', S_N' ------------------------------------------------------------- :: asDefault -<E_t,E_d>,u |- (pat as id) : t gives (pat' as id), (E_t1 u+ {id|->t'}),S_N u+ S_N' - -E_d |- typ ~> t -<E_t,E_d>,t |- pat : t gives pat',E_t1,S_N ------------------------------------------------------------- :: typ -<E_t,E_d>,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 <t_args'> pure == (u'1,..,u'n) -> x <t_args> pure [t_arg1/tid1 .. t_argm/tidm] -<E_t,E_d>,u1 |- pat1 : t1 gives pat'1,E_t1,S_N1 .. <E_t,E_d>,un |- patn : tn gives pat'n,E_tn,S_Nn -disjoint doms(E_t1,..,E_tn) -E_d,(nums,vectors) |- x <t_args'> ~< t: t', S_N ------------------------------------------------------------- :: constr -<E_t,E_d>,t |- id(pat1, .., patn) : x<t_args'> 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 <t_args'> pure == unit -> x <t_args> pure [t_arg1/tid1 .. t_argm/tidm] -E_d,(nums,vectors) |- x <t_args'> ~< t: t', S_N -------------------------------------------------------------- :: identConstr -<E_t,E_d>, t |- :P_id: id : t gives :P_id: id, {}, S_N - -E_t(id) gives {},{},Default,t -E_d,(nums,vectors) |- t ~< u: u', S_N ------------------------------------------------------------- :: varDefault -<E_t,E_d>,u |- :P_id: id : t gives :P_id: id, (E_t u+ {id|->t}),S_N - ------------------------------------------------------------- :: var -<E_t,E_d>,t |- :P_id: id : t gives :P_id: id, (E_t u+ {id|->t}),{} - -E_r(</idi//i/>) gives x< t_args>, (</ti//i/>) -</<E_t,<E_k,E_a,E_r,E_e>>,ti |- pati : ui gives pat'i, E_ti,S_Ni//i/> -disjoint doms(</E_ti//i/>) -<E_k,E_a,E_r,E_e>,(nums,vectors) |- x<t_args> ~< t: t', S_N ------------------------------------------------------------- :: record -<E_t,<E_k,E_a,E_r,E_e>>,t |- { </idi = pati//i/> semi_opt } : x<t_args> gives {</idi=pat'i//i/> semi_opt }, :E_t_multi_union: u+ </E_ti//i/>, S_N u+ </S_Ni//i/> - -<E_t,E_d>,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... <E_t,E_d>,t |- patn : un gives pat'n, E_tn,S_Nn -disjoint doms(E_t1, ... ,E_tn) -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t: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 -<E_t,E_d>, vector<ne1 ne2 order t> |- [ 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} - -<E_t,E_d>,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... <E_t,E_d>,t |- patn : un gives pat'n, E_tn,S_Nn -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t: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 -<E_t,E_d>, vector<ne1 ne2 inc t> |- [ 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 - -<E_t,E_d>,t |- pat1 : u1 gives pat'1, E_t1,S_N1 ... <E_t,E_d>,t |- patn : un gives pat'n, E_tn,S_Nn -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t: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 -<E_t,E_d>, vector<ne1 ne2 dec t> |- [ 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 - -<E_t,E_d>, vector<ne''1 ne'''1 order t> |- pat1 : vector< ne''1 ne'1 order u1> gives pat'1, E_t1,S_N1 ... <E_t,E_d>, vector<ne''n ne'''n order t> |- pat1 : vector< ne''n ne'n order u1> gives pat'n, E_tn,S_Nn -E_d,(nums,vectors) |- u1 ~< t:t',S_N'1 ... E_d,(nums,vectors) |- un ~< t: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 -<E_t,E_d>, vector<ne1 ne2 order t> |- pat1 : ... : patn : vector<ne1 ne4 order t> 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 - -<E_t,E_d>,t |- pat1 : u1 gives pat'1,E_t1,S_N1 .. <E_t,E_d>,t |- patn : un gives pat'n,E_tn,S_Nn -disjoint doms(E_t1,..,E_tn) -E_d,(nums,none) |- u1 ~< t:t',S_N'1 .. E_d,(nums,none) |- un ~< t: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 -<E_t,E_d>, list<t> |- [||pat1, .., patn ||] : list< t> gives [|| pat'1, .. , pat'n ||],(E_t1 u+ .. u+ E_tn),S_N u+ S_N' +G |- foreach ( id from exp1 to exp2 by numOne in dec) exp3 => typ +------------------------------------------------------------------------- :: fordownbyone +G |- foreach ( id from exp1 downto exp2 ) exp3 => typ -defns -check_exp :: '' ::= - -defn -E , t , widening |- 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 <t_args> pure -u == x<t_args> [ t_arg0/tid0 .. t_argn/tidn] -E_d,widening |- u ~< t:t',S_N ------------------------------------------------------------ :: unaryCtor -<E_t,E_d>,t,widening |- id : x gives id, <S_N,pure>,{} - -E_t(id) gives {}, {},tag,u -E_d,widening,t |- id : u gives t', exp, S_N, effect ------------------------------------------------------------- :: localVar -<E_t,E_d>,t,widening |- id : u gives id, <S_N,effect>,{} - -E_t(id) gives {tid1|->kinf1, .., tidn |-> kinfn}, S_N,tag,u' -u == u'[t_arg1/tid1 .. t_argn/tidn] -E_d,widening,t |- id : u gives t', exp, S_N', effect ------------------------------------------------------------- :: otherVar -<E_t,E_d>,t,widening |- id : u gives id,<S_N u+ S_N' ,effect>,{} - -E_t(id) gives {tid0|->kinf0, .., tidn |-> kinfn}, {},Ctor, t'' -> x <t_args> pure -t' -> u pure == t'' -> x<t_args> pure [ t_arg0/tid0 .. t_argn/tidn] -E_d,widening |- u ~< t:t',S_N -<E_t,E_d>,t,widening |- exp : u' gives exp, <S_N',effect>,E_t' ------------------------------------------------------------- :: ctor -<E_t,E_d>,t,widening |- :E_app: id(exp) : t gives :E_app: id(exp'), <S_N u+ S_N, effect>,{} - -E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -ui == ( implicit<ne>, t0 , .. , tm ) -<E_t,E_d>,(t0,..,tm),widening |- (exp0,..,expm) : ui' gives (exp0',..,expm'),I,E_t' -E_d,widening,t |- :E_app: id (annot, exp'0, .., exp'm) : uj gives uj', exp'',S_N',effect' ------------------------------------------------------------- :: appImplicit -<E_t,E_d>,t,widening |- :E_app: id(exp0,..,expm) : uj gives exp'', I u+ <S_N,effect>u+ <S_N',effect'>, E_t - - -E_t(id) gives {tid0 |-> kinf0, .., tidn |-> kinfn}, S_N, tag, u -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -<E_t,E_d>,ui,widening |- exp : ui' gives exp',I,E_t' -E_d,widening,t |- :E_app: id (exp') : uj gives uj', exp'',S_N',effect' ------------------------------------------------------------- :: app -<E_t,E_d>,t,widening |- :E_app: id(exp) : uj gives exp'', I u+ <S_N,effect>u+ <S_N',effect'>, 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 -<E_t,E_d>,ui,widening |- exp : ui' gives exp',I,E_t' -E_d |- select (full( ui', t)) of tinf1 ... tinfn gives tinf -<({id |-> tinf} u+ E_t), E_d>, t,widening |- :E_app: id (exp) : t' gives exp'',I', E_t'' ------------------------------------------------------------- :: appOverload -<E_t,E_d>,t,widening |- :E_app: id(exp) : uj gives exp'', I u+ I' u+ <S_N,effect>u+ <S_N',effect'>, E_t - -E_t(id) gives {tid0 |-> kinf0, .. ,tidn |-> kinfn}, S_N, tag, u -u [t_arg0/tid0 .. t_argn/tidn] == ui -> uj effect -<E_t,E_d>,ui,widening |- (exp1,exp2) : ui' gives (exp1', exp2'), I,E_t' -E_d,widening,t |- :E_app_infix: exp1' id exp2' : uj gives uj', exp, S_N', effect' ------------------------------------------------------------- :: infix_app -<E_t,E_d>,t,widening |- :E_app_infix: exp1 id exp2 : t gives exp, I u+ <S_N, effect> u+ <S_N',effect'>, 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 -<E_t,E_d>,ui,widening |- (exp1,exp2) : ui' gives (exp1', exp2'), I,E_t' -E_d |- select (full( ui', t)) of tinf1 ... tinfn gives tinf -<({id |-> tinf} u+ E_t), E_d>, t, widening |- :E_app_infix: exp1 id exp2 : t' gives exp, I',E_t'' ------------------------------------------------------------- :: infix_appOverload -<E_t,E_d>,t,widening |- :E_app_infix: exp1 id exp2 : t gives exp, I u+ I u+ <S_N, effect> u+ <S_N',effect'>, E_t - - -E_r(</idi//i/>) gives x<t_args>, </ti//i/> -</ <E_t,<E_k,E_a,E_r,E_e>>,ti,widening |- expi : ui gives exp'i,<S_Ni,effecti>,E_t//i/> -</<E_k,E_a,E_r,E_e>,widening |- ui ~< ti: t'i,S_N'i//i/> -S_N == u+ </S_Ni//i/> -S_N' == u+ </S_N'i//i/> ------------------------------------------------------------- :: record -<E_t,<E_k,E_a,E_r,E_e>>,t,widening |- { </idi = expi//i/> semi_opt} : x<t_args> gives{ </idi=exp'i//i/> semi_opt}, u+ <S_N u+ S_N', u+ </effecti//i/>>, {} - -<E_t,<E_k,E_a,E_r,E_e>>,t,widening |- exp : x<t_args> gives exp', I,E_t -E_r(x<t_args>) gives </ id'n:t'n//n/> -</ <E_t,<E_k,E_a,E_r,E_e>>,ti,widening |- expi : ui gives expi',Ii,E_t//i/> -</idi:ti//i/> SUBSET </id'n : t'n//n/> -</<E_k,E_a,E_r,E_e>,widening |- ui ~< ti: t''i,S_N'i//i/> ------------------------------------------------------------- :: recup -<E_t,<E_k,E_a,E_r,E_e>> ,t,widening |- { exp with </idi = expi//i/> semi_opt } : x<t_args> gives {exp' with </idi = exp'i//i/>}, I u+ </Ii//i/>, E_t - -<E_t,E_d>,t,(nums,none) |- exp1 : u1 gives exp'1,I1,E_t' ... <E_t,E_d>,t,(nums,none) |- expn : un gives exp'n,In,E_t' -E_d,(nums,none) |- u1 ~< t: t', S_N1 ... E_d,(nums,none) |- un ~< t: t', S_Nn -length(exp1 ... expn) == ne -S_N == {ne=ne2} u+ S_N1 u+ ... u+ S_Nn ------------------------------------------------------------- :: vector -E, vector<ne1 ne2 order t>, widening |- [ exp1 , ... , expn ] : vector<ne1 num order t> gives [exp'1,...,exp'n], <S_N,pure> u+ I1 u+ ... u+ In , E_t - -E, vector<ne ne' order t>,(nums,none) |- exp1 : vector<ne1 ne1' inc u> gives exp'1,I1,E_t -E, range<ne2 ne2'>,(none,vectors) |- exp2 : range<ne3 ne3'> gives exp'2, I2,E_t -------------------------------------------------------------- :: vectorgetInc -E, t,widening |- :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<ne ne' order t>,(nums,none) |- exp1 : vector<ne1 ne1' dec u> gives exp'1,I1,E_t -E, range<ne2 ne2'>,(none,vectors) |- exp2 : range<ne3 ne3'> gives exp'2, I2,E_t -------------------------------------------------------------- :: vectorgetDec -E, t,widening |- :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<ne1 ne'1 inc t>,(nums,none) |- exp1 : vector<ne2 ne'2 inc u> gives exp'1, I1,E_t -E, range<ne3 ne3'>,(none,vectors) |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t -E,range <ne5 ne5'>,(none,vectors) |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t -------------------------------------------------------------- :: vectorsubInc -E, vector<ne ne' inc t>,widening |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector<ne7 ne'7 inc u> 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<ne1 ne'1 dec t>,(nums,none) |- exp1 : vector< ne2 ne'2 dec u> gives exp'1, I1,E_t -E, range<ne3 ne3'>,(none,vectors) |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t -E,range <ne5 ne5'>,(none,vectors) |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t -------------------------------------------------------------- :: vectorsubDec -E, vector<ne ne' dec t>,widening |- :E_vector_subrange: exp1[ exp2 .. exp3 ] : vector<ne7 ne'7 dec u> 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<ne ne' inc t>,(nums,none) |- exp : vector< ne1 ne2 inc u> gives exp',I,E_t -E, range<ne'1 ne'2>,(none,vectors) |- exp1 : range<ne3 ne4> gives exp'1,I1,E_t -E,t,(nums,vectors) |- exp2 : u gives exp'2,I2,E_t ------------------------------------------------------------- :: vectorupInc -E, vector<ne ne' inc t>,widening |- [ 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<ne ne' dec t>,(nums,none) |- exp : vector <ne1 ne2 dec u> gives exp',I,E_t -E, range<ne'1 ne'2>,(none,vectors) |- exp1 : range<ne3 ne4> gives exp'1,I1,E_t -E,t,(nums,vectors) |- exp2 : u gives exp'2,I2,E_t ------------------------------------------------------------- :: vectorupDec -E, vector<ne ne' dec t>,widening |- [ 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<ne1 ne2 order t>,(nums,none) |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t -E,atom<ne5>,(none,vectors) |- exp1 : atom<ne6> gives exp1',I1,E_t -E,atom<ne7>,(none,vectors) |- exp2 : atom<ne8> gives exp2', I2,E_t -E,vector<ne9 ne10 inc t>,(nums,vectors) |- exp3 : vector <ne11 ne12 inc u> gives exp3',I3,E_t -I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7, ne12 = ne8 + (-ne6) , ne6 + one <= ne8},pure> ------------------------------------------------------------- :: vecrangeupInc -E,vector<ne1 ne2 order t>,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 inc u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E,vector<ne1 ne2 order t>,(nums,none) |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t -E,atom<ne5>,(none,vectors) |- exp1 : atom<ne6> gives exp1',I1,E_t -E,atom<ne7>,(none,vectors) |- exp2 : atom<ne8> gives exp2', I2,E_t -E,u,(nums,vectors) |- exp3 : u' gives exp3',I3,E_t -I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7 },pure> ------------------------------------------------------------- :: vecrangeupvalueInc -E,vector<ne1 ne2 order t>,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 inc u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E,vector<ne1 ne2 order t>,(nums,none) |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t -E,atom<ne5>,(none,vectors) |- exp1 : atom<ne6> gives exp1',I1,E_t -E,atom<ne7>,(none,vectors) |- exp2 : atom<ne8> gives exp2', I2,E_t -E,vector<ne9 ne10 dec t>,(nums,vectors) |- exp3 : vector <ne11 ne12 dec u> gives exp3',I3,E_t -I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> ------------------------------------------------------------- :: vecrangeupDec -E,vector<ne1 ne2 order t>,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 dec u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E,vector<ne1 ne2 order t>,(nums,none) |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t -E,atom<ne5>,(none,vectors) |- exp1 : atom<ne6> gives exp1',I1,E_t -E,atom<ne7>,(none,vectors) |- exp2 : atom<ne8> gives exp2', I2,E_t -E,u,(nums,vectors) |- exp3 : u' gives exp3',I3,E_t -I4 == <{ ne5 <= ne3, ne3+(-ne4) <= ne6+(-ne8), ne8+one<=ne6 },pure> ------------------------------------------------------------- :: vecrangeupvalueDec -E,vector<ne1 ne2 order t>,widening |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] : vector <ne3 ne4 dec u> gives :E_vector_update_subrange:[ exp' with exp1' : exp2' = exp3'], (I u+ (I1 u+ (I2 u+ (I3 u+ I4)))),E_t - -E_r (x<t_args>) gives </idi : ti//i/> id : u </id'j : t'j//j/> -<E_t,<E_k,E_a,E_r,E_e>>,t'',widening |- exp : x< t_args> gives exp', I,E_t -E_d,widening,t |- exp'.id : u gives t', exp1', S_N', effect ------------------------------------------------------------- :: field -<E_t,<E_k,E_a,E_r,E_e>>,t,widening |- exp.id : u gives exp1',I u+ <S_N',effect>,E_t - -<E_t,E_d>,t'',widening |- exp : u gives exp',I,E_t -</<E_t,E_d>,u |- pati : u'i gives pat'i,E_ti,S_Ni//i/> -</<(E_t u+ E_ti),E_d>,t,widening |- expi : u''i gives exp'i,Ii,E_t'i//i/> ------------------------------------------------------------- :: case -<E_t,E_d>,t,widening |- switch exp { </case pati -> expi//i/> }: u gives switch exp' { </case pat'i -> exp'i//i/> }, I u+ </Ii u+ <S_Ni,pure>//i/>, E_t - -<E_t,E_d>,t'',widening |- exp : u gives exp',I,E_t -E_d |- typ ~> t' -E_d,widening,t' |- exp' : u gives u', exp'', S_N,effect -E_d,widening,t |- exp'' : t' gives u'', exp''', S_N', effect' ------------------------------------------------------------- :: typed -<E_t,E_d>,t,widening |- (typ) exp : t gives exp''',I u+ <S_N u+ S_N',effect u+ effect'>,E_t - -<E_t,E_d> |- letbind gives letbind', E_t1, S_N, effect, {} -<(E_t u+ E_t1),E_d>,t,widening |- exp : u gives exp', I2, E_t2 ------------------------------------------------------------- :: let -<E_t,E_d>,t,widening |- letbind in exp : t gives letbind' in exp', <S_N,effect> u+ I2, E_t - -E,t1,widening |- exp1 : u1 gives exp1',I1,E_t1 .... E,tn,widening |- expn : un gives expn',In,E_tn ------------------------------------------------------------- :: tup -E,(t1, ...., tn),widening |- (exp1, .... , expn) : (u1 , .... , un) gives (exp1', ...., expn'), I1 u+ .... u+ In,E_t - -<E_t,E_d>,t,(nums,none) |- exp1 : u1 gives exp1', I1,E_t1 .. <E_t,E_d>,t,(nums,none) |- expn : un gives expn', In,E_tn -E_d,(nums,none) |- u1 ~< t:t',S_N1 .. E_d,(nums,none) |- un ~< t:t',S_Nn ------------------------------------------------------------- :: list -<E_t,E_d>,list<t>,widening |- [||exp1, .., expn ||] : list<u> gives [|| exp1', .., expn' ||], <S_N1 u+ .. u+ S_Nn,pure> u+ I1 u+ .. u+ In, E_t - -E,bit,widening |- exp1 : bit gives exp1',I1,E_t' -E,t,widening |- exp2 : u1 gives exp2',I2,E_t2 -E,t,widening |- exp3 : u2 gives exp3',I3,E_t3 -E_d,widening |- u1 ~< t:t',S_N1 -E_d,widening |- u2 ~< t:t',S_N2 ------------------------------------------------------------- :: if -<E_t,E_d>,t,widening |- if exp1 then exp2 else exp3 : u gives if exp1' then exp2' else exp3', <S_N1 u+ S_N2,pure> u+ I1 u+ I2 u+ I3,(E_t2 inter E_t3) - -<E_t,E_d>,range<ne1 ne2>,widening |- exp1 : range< ne7 ne8> gives exp1', I1,E_t -<E_t,E_d>,range<ne3 ne4>,widening |- exp2 : range< ne9 ne10> gives exp2', I2,E_t -<E_t,E_d>,range<ne5 ne6>,widening |- exp3 : range< ne11 ne12> gives exp3',I3,E_t -<(E_t u+ {id |-> range< ne1 ne4>}),E_d>,unit,widening |- exp4 : t gives exp4',I4,E_t' ------------------------------------------------------------ :: for -<E_t,E_d>,unit,widening |- 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,widening |- exp1 : u gives exp1',I1,E_t -E,list<t>,widening |- exp2 : list<u> gives exp2',I2,E_t ------------------------------------------------------------- :: cons -E,list<t>,widening |- exp1 :: exp2 : list<u> gives exp1'::exp2', I1 u+ I2,E_t - -widening,t |- lit : u => exp,S_N ------------------------------------------------------------- :: lit -E,t,widening |- lit : u gives exp,<S_N,pure>,E_t - -<E_t,E_d>,unit,widening |- exp : unit gives exp', I, E_t1 ------------------------------------------------------------- :: blockbase -<E_t,E_d>,unit,widening |- { exp } : unit gives {exp'}, I, E_t - -<E_t,E_d>,unit,widening |- exp : unit gives exp', I1, E_t1 -<(E_t u+ E_t1),E_d>,unit,widening |- { </expi//i/> } : unit gives {</expi'//i/>}, I2, E_t2 ------------------------------------------------------------- :: blockrec -<E_t,E_d>,unit,widening |- { exp ; </expi//i/> } : unit gives {exp'; </expi'//i/>}, I1 u+ I2, E_t - -<E_t,E_d>,unit,widening |- exp : unit gives exp', I, E_t1 ------------------------------------------------------------- :: nondetbase -<E_t,E_d>,unit,widening |- nondet { exp } : unit gives {exp'}, I, E_t - -<E_t,E_d>,unit,widening |- exp : unit gives exp', I1, E_t1 -<(E_t u+ E_t1),E_d>,unit,widening |- nondet { </expi//i/> } : unit gives {</expi'//i/>}, I2, E_t2 ------------------------------------------------------------- :: nondetrec -<E_t,E_d>,unit,widening |- nondet { exp ; </expi//i/> } : unit gives {exp'; </expi'//i/>}, I1 u+ I2, E_t - -E,t,widening |- exp:u gives exp', I1, E_t1 -E,widening |- lexp:t gives lexp', I2, E_t2 ------------------------------------------------------------- :: assign -E,unit,widening |- lexp := exp : unit gives lexp' := exp', I u+ I2, E_t2 - -defn -E , widening |- lexp : t gives lexp' , I , E_t :: :: check_lexp :: check_lexp_ -{{ com Check the left hand side of an assignment }} -by +G |- exp1 => n_constraint +%G , flows , constrs |- exp2 => typ +%G , flows , negate constrs |- exp3 <= typ +-------------------------------------------- :: if +G |- if exp1 then exp2 else exp3 => typ -E_t(id) gives register<t> ----------------------------------------------------------- :: wreg -<E_t,E_d>,widening |- id : t gives id,<{},{ wreg }>, E_t - -E_t(id) gives reg<t> ----------------------------------------------------------- :: wlocl -<E_t,E_d>,widening |- id : t gives id,Ie, E_t - -E_t(id) gives t ----------------------------------------------------------- :: var -<E_t,E_d>,widening |- id : t gives id,Ie,E_t - -id NOTIN dom(E_t) ----------------------------------------------------------- :: wnew -<E_t,E_d>,widening |- id : t gives id,Ie, {id |-> reg<t>} - -E_t(id) gives register<t> -E_d |- typ ~> u -E_d,widening |- u ~< t : u, S_N ----------------------------------------------------------- :: wregCast -<E_t,E_d>,widening |- (typ) id : t gives id,<S_N,{ wreg }>, E_t - -E_t(id) gives reg<t> -E_d |- typ ~> u -E_d,widening |- u ~< t : u, S_N ----------------------------------------------------------- :: wloclCast -<E_t,E_d>,widening |- (typ) id : t gives id,<S_N,pure>, E_t - -E_t(id) gives t -E_d |- typ ~> u -E_d,widening |- u ~< t : u, S_N ----------------------------------------------------------- :: varCast -<E_t,E_d>,widening |- (typ) id : t gives id,<S_N,pure>,E_t - -id NOTIN dom(E_t) -E_d |- typ ~> t ----------------------------------------------------------- :: wnewCast -<E_t,E_d>, widening |- (typ) id : t gives id,Ie, {id |-> reg<t>} - - -E_t(id) gives E_k, S_N, Extern, (t1, .. ,tn, t) -> t' {</base_effecti//i/>, wmem, </base_effect'j//j/>} -<E_t,E_d>,(t1, .. , tn),widening |- exp : u1 gives exp',I,E_t1 ----------------------------------------------------------- :: wmem -<E_t,E_d>,widening |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ <S_N,{wmem}>,E_t - -E_t(id) gives E_k, S_N, Extern, (t1, ..,tn,t) -> t' {</base_effecti//i/>, wreg, </base_effect'j//j/>} -<E_t,E_d>,(t1,..,tn),widening |- exp : u1 gives exp',I,E_t1 ----------------------------------------------------------- :: wregCall -<E_t,E_d>,widening |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ <S_N,{wreg}>,E_t - -E,atom<ne>,(nums,none) |- exp : u gives exp',I1,E_t -E,(none,vectors) |- lexp : vector<ne1 ne2 inc t> gives lexp',I2,E_t ----------------------------------------------------------- :: wbitInc -E,widening |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne1 <= ne, ne1 + ne2 >= ne},pure>,E_t - -E,atom<ne>,(nums,none) |- exp : u gives exp',I1,E_t -E,(none,vectors) |- lexp : vector<ne1 ne2 dec t> gives lexp',I2,E_t ----------------------------------------------------------- :: wbitDec -E,widening |- lexp [exp] : t gives lexp'[exp'], I1 u+ I2 u+ <{ne <= ne1, ne1 + (-ne2) <= ne},pure>,E_t - -E,atom<ne1>,(nums,none) |- exp1 : u1 gives exp1',I1,E_t -E,atom<ne2>,(nums,none) |- exp2 : u2 gives exp2',I2,E_t -E,(none,vectors) |- lexp : vector<ne3 ne4 inc t> gives lexp',I3,E_t ----------------------------------------------------------- :: wsliceInc -E,widening |- lexp [exp1 : exp2] : vector< ne1 ne2 + (-ne1) inc t> gives lexp'[exp1':exp2'],I1 u+ I2 u+ I3 u+ <{ne3<=ne1, ne3+ne4<= ne2 + (-ne1)},pure> ,E_t - -E,atom<ne1>,(nums,none) |- exp1 : u1 gives exp1',I1,E_t -E,atom<ne2>,(nums,none) |- exp2 : u2 gives exp2',I2,E_t -E,(none,vectors) |- lexp : vector<ne3 ne4 inc t> gives lexp',I3,E_t ----------------------------------------------------------- :: wsliceDec -E,widening |- lexp [exp1 : exp2] : vector< ne1 ne2 + (-ne1) inc t> gives lexp'[exp1':exp2'],I1 u+ I2 u+ I3 u+ <{ne1<=ne3, ne3 + (-ne4)<= ne1 + (-ne2)},pure> ,E_t - - -E_r (x<t_args>) gives </idi : ti//i/> id : t </id'j : t'j//j/> -<E_t,<E_k,E_a,E_r,E_e>>,widening |- lexp : x<t_args> gives lexp',I,E_t ----------------------------------------------------------- :: wrecord -<E_t,<E_k,E_a,E_r,E_e>>,widening |- lexp.id : t gives lexp'.id,I,E_t +G |- :E_app: vector_access ( exp , exp' ) => typ +------------------------------ :: vector_access +G |- exp [ exp' ] => typ -defn -E |- letbind gives letbind' , E_t , S_N , effect , E_k :: :: check_letbind :: check_letbind_ -{{ com Build the environment for a let binding, collecting index constraints }} -by -<E_k,E_a,E_r,E_e> |- typschm ~> t,E_k2,S_N -<E_t,<E_k u+ E_k2,E_a,E_r,E_e>>,t |- pat : u gives pat',E_t1, S_N1 -<E_t,<E_k u+ E_k2,E_a,E_r,E_e>>,t,(none,none) |- exp : u' gives exp', <S_N2,effect>,E_t2 -<E_k u+ E_k2,E_a,E_r,E_e>,(none,none) |- u' ~< u, S_N3 ------------------------------------------------------------- :: val_annot -<E_t,<E_k,E_a,E_r,E_e>> |- let typschm pat = exp gives let typschm pat' = exp', E_t1, S_N u+ S_N1 u+ S_N2 u+ S_N3, effect, E_k2 - -<E_t,E_d>,t |- pat : u gives pat',E_t1,S_N1 -<(E_t u+ E_t1),E_d>,u |- exp : u' gives exp',<S_N2,effect>,E_t2 ------------------------------------------------------------- :: val_noannot -<E_t,E_d> |- let pat = exp gives let pat' = exp', E_t1, S_N1 u+ S_N2, effect,{} +G |- :E_app: vector_subrange ( exp , exp1 , exp2 ) => typ +--------------------------- :: vector_subrange +G |- exp [ exp1 .. exp2 ] => typ -defns -check_defs :: '' ::= -defn -E_d |- type_def gives E :: :: check_td :: check_td_ -{{ com Check a type definition }} -by +G |- :E_app: vector_update ( exp , exp1 , exp2 ) => typ +---------------------------------- :: vector_update +G |- :E_vector_update: [ exp with exp1 = exp2] => typ -E_d |- typschm ~> t,E_k,S_N ------------------------------------------------------------ :: abbrev -E_d |- typedef id name_scm_opt = typschm gives <{},<{},{id |-> E_k, S_N, None,t},{},{}>> - -E_d |- typ1 ~> t1 .. E_d |- typn ~> tn -E_r == { {id1:t1, .., idn:tn} |-> x } ------------------------------------------------------------ :: unquant_record -E_d |- typedef x name_scm_opt = const struct { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<{x |-> K_Typ},{},E_r,{}>> - -</ <E_k,E_a,E_r,E_e> |- quant_itemi ~>E_ki, S_Ni//i/> -<E_k u+ </E_ki//i/>,E_a,E_r,E_e> |- typ1 ~> t1 .. <E_k u+ </E_ki//i/>,E_a,E_r,E_e> |- typn ~> tn -{ x'1 |-> k1, .. ,x'm |-> km } == u+ </E_ki//i/> -E_r1 == { {id1:t1, .., idn:tn} |-> {x'1 |-> k1, ..,x'm |-> km}, u+</S_Ni//i/>, None, x< :t_arg_typ: x'1 .. :t_arg_typ: x'm> } -E_k1' == { x |-> K_Lam (k1 .. km -> K_Typ) } ------------------------------------------------------------ :: quant_record -<E_k,E_a,E_r,E_e> |- typedef x name_scm_opt = const struct forall </quant_itemi//i/> . { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<E_k',{},E_r1,{}>> - -E_t == { id1 |-> {},{},Ctor,t1 -> x pure , ..., idn |-> {},{},Ctor, tn -> x pure } -E_k1 == { x |-> K_Typ } -<E_k u+ E_k1,E_a,E_r,E_e> |- typ1 ~> t1 ... <E_k u+ E_k1,E_a,E_r,E_e> |- typn ~> tn ------------------------------------------------------------- :: unquant_union -<E_k,E_a,E_r,E_e> |- typedef x name_scm_opt = const union { typ1 id1 ; ... ; typn idn semi_opt } gives <E_t,<E_k1,{},{},{}>> - -</ <E_k,E_a,E_r,E_e> |- quant_itemi ~> E_ki, S_Ni//i/> -{ x'1 |-> k1, ... , x'm |-> km } == u+ </E_ki//i/> -E_k' == { x |-> K_Lam (k1 ... km -> K_Typ) } u+ </E_ki//i/> -<E_k u+ E_k',E_a,E_r,E_e> |- typ1 ~> t1 ... <E_k u+ E_k',E_a,E_r,E_e> |- typn ~> tn -t == x < :t_arg_typ: x'1 ... :t_arg_typ: x'm> -E_t == { id1 |-> E_k', u+</S_Ni//i/>, Ctor, t1 -> t pure, ... , idn |-> E_k', u+</S_Ni//i/>, Ctor, tn -> t pure } ------------------------------------------------------------- :: quant_union -<E_k,E_a,E_r,E_e> |- typedef id name_scm_opt = const union forall </quant_itemi//i/> . { typ1 id1 ; ... ; typn idn semi_opt } gives <E_t,<E_k',{},{},{}>> - -% Save these as enumerations for coercion -E_t == {id1 |-> x, ..., idn |-> x} -E_e == { x |-> { num1 |-> id1 ... numn |-> idn} } -------------------------------------------------------------- :: enumerate -E_d |- typedef x name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } gives <E_t,<{id |-> K_Typ},{},{},E_e>> -defn -E |- fundef gives fundef' , E_t , S_N :: :: check_fd :: check_fd_ -{{ com Check a function definition }} -by +G |- :E_app: vector_update_subrange ( exp , exp1 , exp2 , exp3 ) => typ +------------------------------------------ :: vector_update_subrange +G |- :E_vector_update_subrange: [ exp with exp1 : exp2 = exp3 ] => typ -E_t(id) gives E_k',S_N',Global, t1 -> t effect -</E_d |- quant_itemi ~> E_ki,S_Ni//i/> -S_N'' == u+ </S_Ni//i/> -E_k' == </E_ki//i/> -E_d1 == <E_k',{},{},{}> u+ E_d -E_d1 |- typ ~> u -E_d1 |- u ~< t, S_N2 -</<E_t,E_d1>,t1 |- patj : uj gives patj',E_tj,S_N'''j//j/> -</<(E_t u+ E_tj),E_d1>,u |- expj : u' gives expj',<S_N''''j,effect'j>,E_t'j//j/> -S_N''''' == S_N2 u+ </S_N'''j u+ S_N''''j//j/> -effect == u+ </effect'j//j/> -S_N == resolve ( S_N' u+ S_N'' u+ S_N''''') -------------------------------------------------------------- :: rec_function -<E_t,E_d> |- function rec forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives function rec forall </quant_itemi//i/>. typ effectkw effect </id patj' = expj'//j/>,E_t, S_N - -E_t(id) gives E_k', S_N', Global, t1 -> t effect -E_d |- typ ~> u -E_d |- u ~< t, S_N2 -</<E_t,E_d>,t1 |- patj : uj gives pat',E_tj,S_N''j//j/> -</<(E_t u+ E_tj),E_d>,u |- expj : uj' gives expj',<S_N'''j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (S_N2 u+ S_N' u+ </S_N''j u+ S_N'''j//j/>) -------------------------------------------------------------- :: rec_function2 -<E_t,E_d> |- function rec typ effectkw effect </id patj = expj//j/> gives function rec typ effectkw effect </id patj'=expj'//j/>,E_t, S_N - -</<E_k,E_a,E_r,E_e> |- quant_itemi ~> E_ki,S_Ni//i/> -S_N' == u+ </S_Ni//i/> -E_k' == E_k u+ </E_ki//i/> -<E_k',E_a,E_r,E_e> |- typ ~> t -</<E_t,<E_k',E_a,E_r,E_e>>, t1 |- patj : uj gives patj', E_tj,S_N''j//j/> -E_t' == (E_t u+ {id |-> E_k', S_N', Global, t1 -> t effect}) -</<(E_t' u+ E_tj),<E_k',E_a,E_r,E_e>>,t |- expj : u'j gives expj', <S_N'''j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (S_N' u+ </S_N''j u+ S_N'''j//j/>) -------------------------------------------------------------- :: rec_function_no_spec -<E_t,<E_k,E_a,E_r,E_e>> |- function rec forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives function rec forall </quant_itemi//i/> . typ effectkw effect </id patj' = expj'//j/>, E_t', S_N - -E_d |- typ ~> t -</<E_t,E_d>, t1 |- patj : uj gives patj', E_tj,S_N'j//j/> -E_t' == (E_t u+ {id |-> {}, {}, Global, t1 -> t effect}) -</<(E_t' u+ E_tj),E_d>,t |- expj : uj' gives expj', <S_N'j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (u+ </S_N'j u+ S_N''j//j/>) -------------------------------------------------------------- :: rec_function_no_spec2 -<E_t,E_d> |- function rec typ effectkw effect </id patj = expj//j/> gives function rec typ effectkw effect </id patj' = expj'//j/>, E_t', S_N - -E_t(id) gives E_k',S_N',Global, t1 -> t effect -</<E_k,E_a,E_r,E_e> |- quant_itemi ~> E_ki,S_Ni//i/> -S_N'' == u+ </S_Ni//i/> -E_k'' == </E_ki//i/> -<E_k'' u+ E_k,E_a,E_r,E_e> |- typ ~> u -<E_k'' u+ E_k, E_a,E_r,E_e> |- u ~< t, S_N2 -</<E_t,<E_k u+ E_k'',E_a,E_r,E_e>>, t1 |- patj : uj gives patj', E_tj,S_N''j//j/> -</<(E_t u- id u+ E_tj),<E_k u+ E_k'',E_a,E_r,E_e>>,t |- expj : uj' gives expj', <S_N'''j,effect'j>,E_t'j//j/> -S_N'''' == u+ </S_N''j u+ S_N'''j//j/> -effect == u+ </effect'j//j/> -S_N == resolve ( S_N' u+ S_N'' u+ S_N'''') -------------------------------------------------------------- :: function -<E_t,<E_k,E_a,E_r,E_e>> |- function forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives function forall </quant_itemi//i/> . typ effectkw effect </id patj' = expj'//j/>, E_t, S_N - -E_t(id) gives {}, S_N1, Global, t1 -> t effect -E_d |- typ ~> u -E_d |- u ~< t, S_N2 -</<E_t,E_d>,t1 |- patj : uj gives patj,E_tj,S_N'j//j/> -</<(E_t u- id u+ E_tj),E_d>, u |- expj : uj' gives expj', <S_N''j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (S_N1 u+ S_N2 u+ </S_N'j u+ S_N''j//j/>) -------------------------------------------------------------- :: function2 -<E_t,E_d> |- function typ effectkw effect </id patj = expj//j/> gives function typ effectkw effect </id patj' = expj'//j/>, E_t, S_N - -</<E_k,E_a,E_r,E_e> |- quant_itemi ~> E_ki,S_Ni//i/> -S_N' == u+ </S_Ni//i/> -E_k'' == E_k u+ </E_ki//i/> -<E_k'',E_a,E_r,E_e> |- typ ~> t -</<E_t,<E_k'',E_a,E_r,E_e>>,t1 |- patj : uj gives patj,E_tj,S_N''j//j/> -E_t' == (E_t u+ {id |-> E_k'', S_N', Global, t1 -> t effect}) -</<(E_t u+ E_tj),<E_k'',E_a,E_r,E_e>>,t |- expj : uj' gives expj', <S_N''j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (S_N' u+ </S_N'j u+ S_N''j//j/>) -------------------------------------------------------------- :: function_no_spec -<E_t,<E_k,E_a,E_r,E_e>> |- function forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives function forall </quant_itemi//i/>. typ effectkw effect </id patj' = expj'//j/>, E_t', S_N - -E_d |- typ ~> t -</<E_t,E_d>,t1 |- patj : uj gives patj', E_tj,S_N'j//j/> -E_t' == (E_t u+ {id |-> {},S_N, Global, t1 -> t effect}) -</<(E_t u+ E_tj),E_d>,t |- expj : uj' gives exp', <S_N'j,effect'j>,E_t'j//j/> -effect == u+ </effect'j//j/> -S_N == resolve (u+ </S_N'j u+ S_N''j//j/>) -------------------------------------------------------------- :: function_no_spec2 -<E_t,E_d> |- function typ effectkw effect </id patj = expj//j/> gives function typ effectkw effect </id patj' = expj'//j/>, E_t', S_N +G |- :E_app: vector_append ( exp1 , exp2 ) => typ +----------------------------------- :: vector_append +G |- exp1 : exp2 => typ -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 -<E_t,E_d> |- val typschm id gives {id |-> E_k1,S_N,Global,t } +order_inc +G |- exp => typ +G |- exp1 <= typ .. G |- expn <= typ +nexp = length [|| exp , exp1 , .. , expn ||] +-------------------------------------------- :: vector_inc +G |- [|| exp , exp1 , .. , expn ||] => typ [ numZero <: nexp ] -E_d |- typschm ~> t, E_k1, S_N --------------------------------------------------------- :: extern -<E_t,E_d> |- val extern typschm id = string gives {id |-> E_k1,S_N,Extern,t} +order_dec +G |- exp => typ +G |- exp1 <= typ .. G |- expn <= typ +nexp = length [|| exp , exp1 , .. , expn ||] +-------------------------------------------- :: vector_dec +G |- [|| exp , exp1 , .. , expn ||] => typ [ nexp :> numZero ] -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 -<E_k,E_a,E_r,E_e> |- default base_kind 'x gives {}, {'x |-> k default } +G |- exp1 <= bool +G |- exp2 <= string +----------------------------------- :: assert +G |- assert (exp1, exp2 ) => unit -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 }} + G |- exp <= typ :: :: check_exp :: check_exp_ +{{ com Check that type of $[[exp]]$ is $[[typ]]$ }} +{{ tex [[G]] \vdash [[exp]] \Leftarrow [[typ]] }} by -E_d |- type_def gives E ---------------------------------------------------------- :: tdef -<E_t,E_d>|- type_def gives type_def, <E_t,E_d> u+ E -E |- fundef gives fundef', E_t,S_N ---------------------------------------------------------- :: fdef -E |- fundef gives fundef', E u+ <E_t,empty> +G |- exp1 <= unit ... G |- expn <= unit +G |- exp <= typ +----------------------------------- :: block +G |- { exp1; ... ; expn ; exp } <= typ -E |- letbind gives letbind', {id1 |-> t1 , .. , idn |-> tn},S_N,pure,E_k -S_N1 == resolve(S_N) ---------------------------------------------------------- :: vdef -E |- letbind gives letbind', E u+ <{id1 |-> E_k,S_N,None,t1 , .. , idn |-> E_k,S_N,None,tn},empty> -E |- val_spec gives E_t ---------------------------------------------------------- :: vspec -E |- val_spec gives val_spec, E u+ <E_t,empty> -E_d |- default_spec gives E_t1, E_k1 ---------------------------------------------------------- :: default -<E_t,E_d> |- default_spec gives default_spec, <(E_t u+ E_t1),E_d u+ <E_k1,{},{},{}>> - -E_d |- typ ~> t ----------------------------------------------------------- :: register -<E_t,E_d> |- register typ id gives register typ id, <(E_t u+ {id |-> register<t>}),E_d> - -%TODO Add alias checking - -defn -E |- defs gives defs' , E' :: :: check_defs :: check_defs_ -{{ com Check definitions, potentially given default environment of built-in library }} -by - -:check_def: E |- def gives def', E1 -E u+ E1 |- </defi// i/> gives </defi'//i/>, E2 ------------------------------------------------------------- :: defs -E |- def </defi// i/> gives def' </defi'//i/>, E2 + |