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]]) }}

   | 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
----------------------------------------------------------- :: 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; }}
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


------------------------------------------------------------ :: inc
E_k |-o inc ok

------------------------------------------------------------ :: 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

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

------------------------------------------------------------- :: id
|- x ~> x

------------------------------------------------------------ :: var
|- 'x ~> 'x

------------------------------------------------------------ :: num
|- num ~> num

|- nexp1 ~> ne1
|- nexp2 ~> ne2
------------------------------------------------------------ :: mult
|- nexp1 * nexp2 ~> ne1 * ne2

|- nexp1 ~> ne1
|- nexp2 ~> ne2
----------------------------------------------------------- :: add
|- nexp1 + nexp2 ~> ne1 + ne2

|- nexp1 ~> ne1
|- nexp2 ~> ne2
----------------------------------------------------------- :: sub
|- nexp1 - nexp2 ~> ne1 - ne2

|- 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

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' 

: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 }}
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>


------------------------------------------------------------ :: atom
E_d |- atom<ne> ~= range<ne1 ne2>

------------------------------------------------------------ :: 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>

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

E_d |- t ~= u
------------------------------------------------------------ :: reg
E_d |- reg<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'

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

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

------------------------------------------------------------- :: vecToAtom
E_d |-c vector<ne ne2 order bit> ~= atom<ne3>

------------------------------------------------------------- :: vecToRange
E_d |-c vector<ne ne2 order bit> ~= range<ne3 ne4>

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

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

E_d |-c t1 ~= u1 .... E_d |-c tn ~= un
------------------------------------------------------------ :: tup
E_d |-c (t1,....,tn) ~= (u1,....,un)

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>


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>

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_
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'


defn
E_d |- select ( conformsto ( t , t' ) ) of tinflist gives tinflist' :: :: selectoverload :: so_
{{ tex [[select]]_{[[conformsto]] ([[t]],[[t']])} ([[tinflist]]) [[gives]] [[tinflist']] }}
by

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

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


----------------------------------------------------------- :: range
E_d,widening |- range <ne1 ne2> ~< range<ne3 ne4>: range<ne3 ne4>, { ne3 <= ne1, ne2 <= ne4 }

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


---------------------------------------------------------- :: atom
E_d,(none,_) |- atom <ne1> ~< atom<ne2>: atom<ne2>, { ne1 = ne2 }

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

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

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

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

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


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' }

 ------------------------------------------------------------ :: numbitzero
widening, bit  |- numZero : atom < zero > => bitzero, {}

 ------------------------------------------------------------ :: numbitone
widening, bit  |- numOne : atom < one > => bitone, {}
 
 ------------------------------------------------------------- :: string
widening, string |- :L_string: string : :T_string_typ: string => :E_lit: string, {}

 ne == bitlength(hex)
 ------------------------------------------------------------ :: hex
widening, vector<ne1 ne2 order bit> |- hex : vector< ne1 ne order bit> => hex, {ne=ne2}

ne == bitlength(bin)
 ------------------------------------------------------------ :: bin 
widening,vector<ne1 ne2 order bit> |- bin : vector< ne1 ne order bit> => bin, {ne=ne2}

 ------------------------------------------------------------ :: unit
widening, unit |- () : unit => unit, {}

 ------------------------------------------------------------ :: bitzero
widening, bit |- bitzero : bit => bitzero, {}

 ------------------------------------------------------------ :: bitone
widening, bit  |- bitone : bit => bitzero, {}

------------------------------------------------------------ :: 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

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'


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

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

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,{}

defns
check_defs :: '' ::=

defn
E_d |- type_def gives E :: :: check_td :: check_td_
{{ com Check a type definition }}
by

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

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


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 }

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_a,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 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>

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