path: root/language/l2_rules.ott

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
<E_k,E_a,E_r,E_e> |- kind 'x ~> {'x |-> k}, {}

E_k('x) gives k
----------------------------------------------------------- :: nokind
<E_k,E_a,E_r,E_e> |- '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+ <E_k,{},{},{}> |- 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
<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>

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
<E_k,E_a,E_r,E_e> |- 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
<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 

 
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>

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>

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


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
<E_k,E_a,E_r,E_e> |- 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
<E_k,E_a,E_r,E_e> |- u ~< t,S_N
------------------------------------------------------------ :: abbrev
<E_k,E_a,E_r,E_e> |- x ~< t , S_N u+ S_N1

E_a(x) gives {},S_N1,tag,u
<E_k,E_a,E_r,E_e> |- t ~< u,S_N
------------------------------------------------------------ :: abbrev2
<E_k,E_a,E_r,E_e> |- 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 <ne1 ne2> ~< range<ne3 ne4>, { ne3 <= ne1, ne2 <= ne4 }

---------------------------------------------------------- :: atomRange
E_d |- atom <ne> ~< range<ne1 ne2>, { ne1 <= ne, ne <= ne2 }

---------------------------------------------------------- :: atom
E_d |- atom <ne1> ~< atom<ne2>, { ne1 = ne2 }

---------------------------------------------------------- :: rangeAtom
E_d |- range<ne1 ne2> ~< atom<'x>, { ne1 <= 'x, 'x <= ne2 }

E_d |- t ~< t', S_N
---------------------------------------------------------- :: vector
E_d |- vector <ne1 ne2 order t> ~< vector <ne3 ne4 order t'>, {ne1=ne3,ne2=ne3} u+ S_N

E_k(x) gives K_Lam (k1 .. kn -> K_Typ)
<E_k,E_a,E_r,E_e>,k1 |- t_arg1 ~< t_arg'1,S_N1 .. <E_k,E_a,E_r,E_e>,kn |- t_argn ~< t_arg'n,S_Nn
------------------------------------------------------------ :: app
<E_k,E_a,E_r,E_e> |- x <t_arg1 .. t_argn> ~< 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> |- x <t_arg1 .. t_argn> ~< u [ t_arg'1/tid1 .. t_arg'm/tidm ] ,S_N2
------------------------------------------------------------ :: appAbbrev
<E_k,E_a,E_r,E_e> |- x < t_arg1 .. t_argn> ~< x' <t_arg'1 .. t_arg'm>, S_N u+ S_N2

x' NOTEQ x
E_a(x') gives {tid1|->kinf1, .. ,tidm|->kinfm}, S_N, tag, u
<E_k,E_a,E_r,E_e> |-  u [ t_arg'1/tid1 .. t_arg'm/tidm ]  ~< x <t_arg1 .. t_argn> ,S_N2
------------------------------------------------------------ :: appAbbrev2
<E_k,E_a,E_r,E_e> |- x' <t_arg'1 .. t_arg'm> ~<  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 <ne3 ne4 order u> gives vector <ne3 ne4 order t>, exp', S_N u+ {ne2=ne4}, pure

E_d |- u ~< bit, S_N
exp' == to_num exp 
-------------------------------------------------- :: toNum
E_d, 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, 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, u |- exp':t gives t',exp'', S_N, pure
-------------------------------------- :: readReg
E_d, u |- exp : register<t> gives t', exp'', S_N, {rreg}

exp' == exp[numZero]
-------------------------------------- :: accessVecBit
E_d, bit |- exp : vector<ne1 ne2 order bit> gives bit,exp', { ne1=one},pure

E_d |- range<zero one> ~< range<ne1 ne2>,S_N
exp' == switch exp { case bitzero -> numZero case bitone -> numOne}
-------------------------------------- :: bitToNum
E_d, range<ne1 ne2> |- exp : bit gives range<ne1 ne2>, exp',S_N,pure

E_d |- range<ne1 ne2> ~< range<zero one>,S_N
exp' == switch exp { case numZero -> bitzero case numOne -> bitone }
------------------------------------- :: numToBit
E_d, bit |- range : range<ne1 ne2> 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>, 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> |- range<zero ne3> ~< range<ne1 ne2>, S_N
------------------------------------------------ :: fromEnumerate
<E_k,E_a,E_r,E_e>,range<ne1 ne2> |- exp: x gives range<zero ne3>, 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 <ne ne'>  |- num : atom < num > => num , { ne <= num, num <= ne' }

 ------------------------------------------------------------ :: numToVec
vector <ne ne' order bit>  |- 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<ne1 ne2 order bit> |- hex : vector< ne1 ne order bit> => hex, {ne=ne2}

ne == bitlength(bin)
 ------------------------------------------------------------ :: bin 
vector<ne1 ne2 order bit> |- 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
<E_t,E_d>, 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

<E_t,E_d>,t' |- pat : t gives pat', E_t1,S_N
E_t(id) gives {}, {}, Default, t'
E_d |- t' ~< 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 |- x <t_args'> ~< 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 |- x <t_args'> ~< 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 |- t ~< 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> |- x<t_args> ~< 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 |- 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
<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 |- 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
<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 |- 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
<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 |- 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
<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 |- 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
<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'


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 <t_args> pure
u == x<t_args> [ t_arg0/tid0 .. t_argn/tidn] 
E_d |- u ~< t,S_N
----------------------------------------------------------- :: unaryCtor
<E_t,E_d>,t |- id : x gives id, <S_N,pure>,{}

E_t(id) gives {}, {},tag,u
E_d,t |- id : u gives t', exp, S_N, effect
------------------------------------------------------------ :: localVar
<E_t,E_d>,t |- 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,t |- id : u gives t', exp, S_N', effect
------------------------------------------------------------ :: otherVar
<E_t,E_d>,t |- 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 |- u ~< t,S_N
<E_t,E_d>,t' |- exp : u' gives exp, <S_N',effect>,E_t'
------------------------------------------------------------ :: ctor
<E_t,E_d>,t |- :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) |- (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
<E_t,E_d>,t |- :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 |- exp : ui' gives exp',I,E_t'
E_d,t |- :E_app: id (exp') : uj gives uj', exp'',S_N',effect' 
------------------------------------------------------------ :: app
<E_t,E_d>,t |- :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 |- 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
<E_t,E_d>,t |- :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 |- (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
<E_t,E_d>,t |- :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 |- (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
<E_t,E_d>,t |- :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 |- expi : ui gives exp'i,<S_Ni,effecti>,E_t//i/>
</<E_k,E_a,E_r,E_e> |- ui ~< ti,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 |- { </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 |- 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 |- 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> |- ui ~< ti,S_N'i//i/>
------------------------------------------------------------ :: recup
<E_t,<E_k,E_a,E_r,E_e>> ,t |- { 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 |- exp1 : u1 gives exp'1,I1,E_t' ... <E_t,E_d>,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<ne1 ne2 order t> |- [ 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> |- exp1 : vector<ne1 ne1' inc u> gives exp'1,I1,E_t
E, range<ne2 ne2'> |- exp2 : range<ne3 ne3'> 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<ne ne' order t> |- exp1 : vector<ne1 ne1' dec u> gives exp'1,I1,E_t
E, range<ne2 ne2'> |- exp2 : range<ne3 ne3'> 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<ne1 ne'1 inc t> |- exp1 : vector<ne2 ne'2 inc u> gives exp'1, I1,E_t
E, range<ne3 ne3'> |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t
E,range <ne5 ne5'> |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t
------------------------------------------------------------- :: vectorsubInc
E, vector<ne ne' inc t> |- :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> |- exp1 : vector< ne2 ne'2 dec u> gives exp'1, I1,E_t
E, range<ne3 ne3'> |- exp2 : range< ne4 ne'4> gives exp'2, I2,E_t
E,range <ne5 ne5'> |- exp3 : range< ne6 ne'6> gives exp'3, I3,E_t
------------------------------------------------------------- :: vectorsubDec
E, vector<ne ne' dec t> |- :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> |- exp : vector< ne1 ne2 inc u> gives exp',I,E_t
E, range<ne'1 ne'2> |- exp1 : range<ne3 ne4> gives exp'1,I1,E_t
E,t |- exp2 : u gives exp'2,I2,E_t
------------------------------------------------------------ :: vectorupInc
E, vector<ne ne' inc t> |- [ 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> |- exp : vector <ne1 ne2 dec u> gives exp',I,E_t
E, range<ne'1 ne'2> |- exp1 : range<ne3 ne4> gives exp'1,I1,E_t
E,t |- exp2 : u gives exp'2,I2,E_t
------------------------------------------------------------ :: vectorupDec
E, vector<ne ne' dec t> |- [ 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> |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t
E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t
E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t
E,vector<ne9 ne10 inc t> |- 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> |- :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> |- exp : vector< ne3 ne4 inc u> gives exp',I,E_t
E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t
E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t
E,u |- exp3 : u' gives exp3',I3,E_t
I4 == <{ ne3 <= ne5, ne3+ne4 <= ne7 },pure>
------------------------------------------------------------ :: vecrangeupvalueInc
E,vector<ne1 ne2 order t> |- :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> |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t
E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t
E,atom<ne7> |- exp2 : atom<ne8> gives exp2', I2,E_t
E,vector<ne9 ne10 dec t> |- 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> |- :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> |- exp : vector< ne3 ne4 dec u> gives exp',I,E_t
E,atom<ne5> |- exp1 : atom<ne6> gives exp1',I1,E_t
E,atom<ne7> |- exp2 : atom<ne8> 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<ne1 ne2 order t> |- :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''  |- exp : x< t_args> gives exp', I,E_t
E_d,t |- exp'.id : u gives t', exp1', S_N', effect
------------------------------------------------------------ :: field
<E_t,<E_k,E_a,E_r,E_e>>,t |- exp.id : u gives exp1',I u+ <S_N',effect>,E_t

<E_t,E_d>,t'' |- 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 |- expi : u''i gives exp'i,Ii,E_t'i//i/>
------------------------------------------------------------ :: case
<E_t,E_d>,t |- 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'' |- 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
<E_t,E_d>,t |- (typ) exp : t gives exp''',I u+ <S_N u+ S_N',effect u+ effect'>,E_t

<E_t,E_d> |- letbind gives E_t1, S_N, effect, {}
<(E_t u+ E_t1),E_d>,t |- exp : u gives exp', I2, E_t2
------------------------------------------------------------ :: let
<E_t,E_d>,t |- letbind in exp : t gives exp', <S_N,effect> 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
 
<E_t,E_d>,t |- exp1 : u1 gives exp1', I1,E_t1 .. <E_t,E_d>,t |- expn : un gives expn', In,E_tn
E_d |- u1 ~< t,S_N1 .. E_d |- un ~< t,S_Nn
------------------------------------------------------------ :: list
<E_t,E_d>,list<t> |- [||exp1, .., expn ||] : list<u> gives [|| exp1', .., expn' ||], <S_N1 u+ .. u+ S_Nn,pure> 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
<E_t,E_d>,t |- 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> |- exp1 : range< ne7 ne8> gives exp1', I1,E_t
<E_t,E_d>,range<ne3 ne4> |- exp2 : range< ne9 ne10> gives exp2', I2,E_t
<E_t,E_d>,range<ne5 ne6> |- 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
<E_t,E_d>,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<t> |- exp2 : list<u> gives exp2',I2,E_t
------------------------------------------------------------ :: cons
E,list<t> |- exp1 :: exp2 : list<u> gives exp1'::exp2', I1 u+ I2,E_t

t |- lit : u => exp,S_N
------------------------------------------------------------ :: lit
E,t |- lit : u gives exp,<S_N,pure>,E_t

<E_t,E_d>,unit |- exp : unit gives exp', I, E_t1
------------------------------------------------------------ :: blockbase
<E_t,E_d>,unit |- { exp } : unit gives {exp'}, I, E_t

<E_t,E_d>,unit |- exp : unit gives exp', I1, E_t1
<(E_t u+ E_t1),E_d>,unit |- { </expi//i/> } : unit gives {</expi'//i/>}, I2, E_t2
------------------------------------------------------------ :: blockrec
<E_t,E_d>,unit |- { exp ; </expi//i/> } : unit gives {exp'; </expi'//i/>}, I1 u+ I2, E_t

<E_t,E_d>,unit |- exp : unit gives exp', I, E_t1
------------------------------------------------------------ :: nondetbase
<E_t,E_d>,unit |- nondet { exp } : unit gives {exp'}, I, E_t

<E_t,E_d>,unit |- exp : unit gives exp', I1, E_t1
<(E_t u+ E_t1),E_d>,unit |- nondet { </expi//i/> } : unit gives {</expi'//i/>}, I2, E_t2
------------------------------------------------------------ :: nondetrec
<E_t,E_d>,unit |- nondet { exp ; </expi//i/> } : unit gives {exp'; </expi'//i/>}, 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<t>
---------------------------------------------------------- :: wreg
<E_t,E_d> |- id : t gives id,<{},{ wreg }>, E_t

E_t(id) gives reg<t>
---------------------------------------------------------- :: wlocl
<E_t,E_d> |- id : t gives id,Ie, E_t

E_t(id) gives t
---------------------------------------------------------- :: var
<E_t,E_d> |- id : t gives id,Ie,E_t

id NOTIN dom(E_t)
---------------------------------------------------------- :: wnew
<E_t,E_d> |- id : t gives id,Ie, {id |-> reg<t>}

E_t(id) gives E_k, S_N, Extern, t1 -> t {</base_effecti//i/>, wmem, </base_effect'j//j/>}
<E_t,E_d>,t1 |- exp : u1 gives exp',I,E_t1
---------------------------------------------------------- :: wmem
<E_t,E_d> |- :LEXP_memory: id(exp) : t gives :LEXP_memory: id(exp'),I u+ <S_N,{wmem}>,E_t

E,atom<ne> |- exp : u gives exp',I1,E_t
E |- lexp : vector<ne1 ne2 inc t> 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<ne> |- exp : u gives exp',I1,E_t
E |- lexp : vector<ne1 ne2 dec t> 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 </idi : ti//i/> id : t </id'j : t'j//j/>
<E_t,<E_k,E_r,E_e>> |- lexp : id'' t_args gives I,E_t
---------------------------------------------------------- :: wrecord
<E_t,<E_k,E_r,E_e>> |- 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

<E_k,E_r,E_e> |- typschm ~> t,E_k2,S_N
<E_t,<E_k u+ E_k2,E_r,E_e>> |- pat : t gives E_t1, S_N1
<E_t,<E_k u+ E_k2,E_r,E_e>> |- exp : t gives <S_N2,effect>,E_t2
------------------------------------------------------------ :: val_annot
<E_t,<E_k,E_r,E_e>> |- let typschm pat = exp gives E_t1, S_N u+ S_N1 u+ S_N2, effect, E_k2
 
<E_t,E_d> |- pat : t gives E_t1,S_N1
<(E_t u+ E_t1),E_d> |- exp : t gives <S_N2,effect>,E_t2
------------------------------------------------------------ :: val_noannot
<E_t,E_d> |- 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,{}>>

</ <E_k,E_r,E_e> |- quant_itemi ~>E_ki, S_Ni//i/>
<E_k u+ </E_ki//i/>,E_r,E_e> |- typ1 ~> t1 .. <E_k u+ </E_ki//i/>,E_r,E_e> |- typn ~> tn
{ id'1 |-> k1, .. ,id'm |-> km } = u+ </E_ki//i/>
E_r1 = { {id1:t1, .., idn:tn} |-> {id'1 |-> k1, ..,id'm |-> km}, u+</S_Ni//i/>, None, id :t_arg_typ: id'1 ..  :t_arg_typ: id'm }
E_k1' = { id |-> K_Lam (k1 .. km -> K_Typ) }
----------------------------------------------------------- :: quant_record
<E_k,E_r,E_e> |- typedef id name_scm_opt = const struct forall </quant_itemi//i/> . { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<E_k',E_r1,{}>>

E_t = { id1 |-> t1 -> :T_id: id pure Ctor {}, ..., idn |-> tn -> :T_id: id pure Ctor {} }
E_k1 = { id |-> K_Typ }
<E_k u+ E_k1,E_r,E_e> |- typ1 ~> t1 ... <E_k u+ E_k1,E_r,E_e> |- typn ~> tn
------------------------------------------------------------ :: unquant_union
<E_k,E_r,E_e> |- typedef id name_scm_opt = const union { typ1 id1 ; ... ; typn idn semi_opt } gives <E_t,<E_k1,{},{}>>

</ <E_k,E_r,E_e> |- quant_itemi ~> E_ki, S_Ni//i/>
{ id'1 |-> k1, ... , id'm |-> km } = u+ </E_ki//i/>
E_k' = { id |-> K_Lam (k1 ... km -> K_Typ) } u+ </E_ki//i/>
<E_k u+ E_k',E_r,E_e> |- typ1 ~> t1 ... <E_k u+ E_k',E_r,E_e> |- typn ~> tn
t = id :t_arg_typ: id'1 ... :t_arg_typ: id'm
E_t = { id1 |-> E_k', u+</S_Ni//i/>, Ctor, t1 -> t pure Ctor {}, ... , idn |-> E_k', u+</S_Ni//i/>, Ctor, tn -> t pure Ctor {} }
------------------------------------------------------------ :: quant_union
<E_k,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 |-> id, ..., idn |-> id}
E_e = { id |-> { num1 |-> id1 ... numn |-> idn} }
------------------------------------------------------------- :: enumerate
E_d |- typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } gives <E_t,<{id |-> 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_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 ~> t
</<E_t,E_d1> |- patj : t1 gives E_tj,S_N'''j//j/>
</<(E_t u+ E_tj),E_d1> |- expj : t gives <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''''')
------------------------------------------------------------- :: rec_function
<E_t,E_d> |- function rec forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives E_t, S_N

E_t(id) gives t1 -> t effect None S_N'
E_d |- typ ~> t
</<E_t,E_d> |- patj : t1 gives E_tj,S_N''j//j/>
</<(E_t u+ E_tj),E_d> |- expj : t gives <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_function2
<E_t,E_d> |- function rec typ effectkw effect </id patj = expj//j/> gives E_t, S_N

</<E_k,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_r,E_e> |- typ ~> t
</<E_t,<E_k',E_r,E_e>> |- patj : t1 gives E_tj,S_N''j//j/>
E_t' = (E_t u+ {id |-> t1 -> t effect None S_N'})
</<(E_t' u+ E_tj),<E_k',E_r,E_e>> |- expj : t gives <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_r,E_e>> |- function rec forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives E_t', S_N

E_d |- typ ~> t
</<E_t,E_d> |- patj : t1 gives E_tj,S_N'j//j/>
E_t' = (E_t u+ {id |-> t1 -> t effect None {}})
</<(E_t' u+ E_tj),E_d> |- expj : t gives <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 E_t', S_N

t2 = t1 -> t effect None S_N'
E_t(id) gives E_k',S_N',None, t2
</<E_k,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_r,E_e> |- typ ~> t
</<E_t,<E_k u+ E_k'',E_r,E_e>> |- patj : t1 gives E_tj,S_N''j//j/>
</<(E_t u- {id |-> t2} u+ E_tj),<E_k u+ E_k'',E_r,E_e>> |- expj : t gives <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_r,E_e>> |- function forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives E_t, S_N

E_t(id) gives t1 -> t effect None S_N1
E_d |- typ ~> t
</<E_t,E_d> |- patj : t1 gives E_tj,S_N'j//j/>
</<(E_t u- {id |-> t1 -> t effect None S_N1} u+ E_tj),E_d> |- expj : t gives <S_N''j,effect'j>,E_t'j//j/>
effect = u+ </effect'j//j/>
S_N = resolve (S_N1 u+ </S_N'j u+ S_N''j//j/>)
------------------------------------------------------------- :: function2
<E_t,E_d> |- function typ effectkw effect </id patj = expj//j/> gives E_t, S_N

</<E_k,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_r,E_e> |- typ ~> t
</<E_t,<E_k'',E_r,E_e>> |- patj : t1 gives E_tj,S_N''j//j/>
E_t' = (E_t u+ {id |-> t1 -> t effect None S_N'})
</<(E_t u+ E_tj),<E_k'',E_r,E_e>> |- expj : t gives <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_r,E_e>> |- function forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives E_t', S_N

E_d |- typ ~> t
</<E_t,E_d> |- patj : t1 gives E_tj,S_N'j//j/>
E_t' = (E_t u+ {id |-> t1 -> t effect None S_N})
</<(E_t u+ E_tj),E_d> |- expj : t gives <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 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
<E_t,E_d> |- val typschm id gives {id |-> E_k1,S_N,None,t }

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}

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_r,E_e> |- 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
<E_t,E_d>|- type_def gives <E_t,E_d> u+ E

E |- fundef gives E_t,S_N 
--------------------------------------------------------- :: fdef
E |- fundef gives E u+ <E_t,empty>

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_t,empty>

E_d |- default_spec gives E_t1, E_k1
--------------------------------------------------------- :: default
<E_t,E_d> |- default_spec  gives <(E_t u+ E_t1),E_d u+ <E_k1,{},{}>>

E_d |- typ ~> t
---------------------------------------------------------- :: register
<E_t,E_d> |- 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 |- </defi// i/> gives E2
------------------------------------------------------------ :: defs 
E |- def </defi// i/> gives E2