grammar

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Machinery for typing rules                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
grammar 

k :: 'Ki_' ::=
{{ com Internal kinds }}
   | K_Typ                                             :: :: typ
   | K_Nat                                             :: :: nat
   | K_Ord                                             :: :: ord
   | K_Efct                                            :: :: efct
   | K_Lam ( k0 .. kn -> k' )                          :: :: ctor
   | K_infer                                           :: :: infer {{ com Representing an unknown kind, inferred by context }}
   | K_Abbrev t                                        :: :: abbrev {{ com Not really a kind, but a convenient way of tracking type abbreviations }}

t , u :: 'T_' ::=                                {{ phantom }}
{{ com Internal types }}
   | id                                           :: :: var
   | t1 -> t2 effects tag S_N                     :: :: fn  {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }}
   | ( t1 * .... * tn )                           :: :: tup
   | id t_args                                    :: :: app 
   | register t_args                              :: :: reg_app
   | t [ t1 / id1 ... tn / idn ]		  :: :: subst

tag :: 'Tag_' ::=                                 {{ phantom }}
{{ com Data indicating where the identifier arises and thus information necessary in compilation }}
   | None                                 :: :: empty 
   | Ctor                                 :: :: ctor {{ com Data constructor from a type union }}
   | Extern                               :: :: extern {{ com External function, specied only with a val statement }}
   | Default                              :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }}
   | _                                    :: :: dontcare 

ne :: 'Ne_' ::=
 {{ com internal numeric expressions }}
   | id                                           :: :: var
   | num                                 :: :: const
   | ne1 * ne2                           :: :: mult
   | ne1 + ... + nen                     :: :: add
   | 2 ** ne				 :: :: exp
   | ( - ne )                            :: :: unary
   | bitlength ( bin )                   :: M :: cbin
     {{ ocaml (asssert false) }}
     {{ hol ARB }}
     {{ lem (blength [[bin]]) }}
   | bitlength ( hex )                   :: M :: chex
     {{ ocaml (assert false) }}
     {{ hol ARB }}
     {{ lem (hlength [[hex]]) }}
   | length ( pat1 ... patn )            :: M :: cpat
     {{ ocaml (assert false) }}
     {{ hol ARB }}
     {{ lem (Ne_const (List.length [[pat1...patn]])) }}
   | length ( exp1 ... expn )            :: M :: cexp
     {{ hol ARB }}
     {{ ocaml (assert false) }}
     {{ lem (Ne_const (List.length [[exp1...expn]])) }}
 
 t_arg :: 't_arg_' ::=   {{ phantom }}
 {{ com Argument to type constructors }}
 | t :: :: typ
 | ne :: :: nexp
 | effects :: :: effect
 | order :: :: order

 t_args :: '' ::=   {{ phantom }}
  {{ com Arguments to type constructors }}
   | t_arg1 ... t_argn                            :: :: T_args

 nec :: 'Nec_' ::=
   {{ com Numeric expression constraints }}
   | ne <= ne'            :: :: lteq
   | ne = ne'            :: :: eq
   | ne >= ne'           :: :: gteq
   | id 'IN' { num1 , ... , numn } :: :: in

%% %% embed
%% %% {{ lem
%% %% 
%% %% val t_subst_t : list (tnv * t) -> t -> t 
%% %% val t_subst_tnv : list (tnv * t) -> tnv -> t
%% %% val ftv_t : t -> list tnv
%% %% val ftv_tm : list t -> list tnv
%% %% val ftv_s : list (p*tnv) -> list tnv
%% %% val compatible_overlap : list (x*t) -> bool
%% %% 
%% %% (*TODO Should this normalize following the implementation? And blength and hlength need a means of implementation*)
%% %% let normalize n = n
%% %% 
%% %% let blength (_,bit) = Ne_const 8
%% %% let hlength (_,bit) = Ne_const 8
%% %% 
%% %% let rec sumation_nes nes = match nes with
%% %%   | [ a; b] -> Ne_add a b 
%% %%   | x :: y -> Ne_add x (sumation_nes y)
%% %% end
%% %% 
%% %% }}
%% %% 
%% %% embed
%% %% {{ hol
%% %% load "fmaptreeTheory";
%% %% val _ = 
%% %%   Hol_datatype 
%% %%     `env_body = <| env_p : x|->p; env_f : x|->f_desc; env_v : x|->v_desc |>`;
%% %% 
%% %% val _ = Define `
%% %%   env_union e1 e2 =
%% %%     let i1 = item e1 in
%% %%     let m1 = map e1 in
%% %%     let i2 = item e2 in
%% %%     let m2 = map e2 in
%% %%       FTNode <| env_p:=FUNION i1.env_p i2.env_p; 
%% %%                 env_f:=FUNION i1.env_f i2.env_f;
%% %%                 env_v:=FUNION i1.env_v i2.env_v |>
%% %%              (FUNION m1 m2)`;
%% %% }}
%% %% {{ lem
%% %% type env =
%% %%   | EnvEmp 
%% %%   | Env of (map x env) * (map x p) * (map x f_desc) * (map x v_desc)
%% %% 
%% %% val env_union : env -> env -> env
%% %% let env_union e1 e2 =
%% %%   match (e1,e2) with
%% %%    | (EnvEmp,e2) -> e2
%% %%    | (e1,EnvEmp) -> e1
%% %%    | ((Env Em1 Ep1 Ef1 Ev1),(Env Em2 Ep2 Ef2 Ev2)) ->
%% %%      Env(union_map Em1 Em2) (union_map Ep1 Ep2) (union_map Ef1 Ef2) (union_map Ev1 Ev2)
%% %% end
%% %% 
%% %% }}
%% %% 

S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
                                                                    {{ hol nec list }}
                                                                    {{ lem list nec }}
    {{ com nexp constraint lists }}
    | { nec1 , .. ,  necn }                              :: :: Sn_concrete
      {{ hol [[nec1 .. necn]] }}
      {{ lem [[nec1 .. necn]] }}
   | S_N1 u+ .. u+ S_Nn                                                    :: M :: SN_union
     {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }}
     {{ lem (List.fold_right union_map [[S_N1..S_Nn]] Map.empty) }}
     {{ ocaml (assert false) }}
   | consistent_increase ne1 ne'1 ... nen ne'n                    :: M :: SN_increasing
     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }}
     {{ ocaml (assert false) }}
     {{ ichl todo }}
   | consistent_decrease ne1 ne'1 ... nen ne'n                      :: M :: SN_decreasing
     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }}
     {{ ocaml assert false }}
     {{ ichl todo }}
   | resolve ( S_N )                                                :: :: resolution
 
 I :: '' ::=                                                     {{ phantom }}
  {{ com Information given by type checking an expression }}
  | < S_N , effects >                                      :: :: I
  | Ie                                                           :: :: Iempty {{ com Empty constraints, effects }} {{ tex {\ottnt{I}_{\epsilon} } }}
  | I1 u+ .. u+ In                                               :: :: Iunion {{ com Unions the constraints and effects }}

 E :: '' ::=                                                     
                                                                 {{ hol ((string,env_body) fmaptree) }}
                                                                 {{ lem env }}
 {{ com Definition environment and lexical environment }}
 | < E_t , E_d >                                           :: :: E
  {{ hol arb }}
  {{ lem (Env [[E_t]] [[E_d]]  }}
 | empty                                                       :: M :: E_empty
   {{ hol arb }}
   {{ lem EnvEmp }}
   {{ ocaml assert false }}
 | E u+ E'                                                      :: :: E_union

 E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::=
 {{ com Environments storing top level information, such as defined records, enumerations, and kinds }}
 | < E_k , E_r , E_e >	     	       		    	 :: :: base
 | empty       	     					 :: :: empty
 | E_d u+ E_d'						 :: :: union
 
 kinf :: 'kinf_' ::=
   {{ com Whether a kind is default or from a local binding }}
   | k                                        :: :: k
   | k default                                :: :: def

 E_k {{ tex \ottnt{E}^{\textsc{k} } }} :: 'E_k_' ::=             {{ phantom }}
                                                                 {{ hol (id-> k) }}
                                                                 {{ lem map id k }}
   {{ com Kind environments }}
   | { id1 |-> kinf1 , .. , idn |-> kinfn }    :: :: concrete
     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[id1 kinf1 .. idn kinfn]]) }}
     {{ lem (List.fold_right (fun (x,v) m -> Map.insert x v m) [[id1 kinf1 .. idn kinfn]] Map.empty) }} 
   | E_k1 u+ .. u+ E_kn                                          :: M :: union
     {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} 
     {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }}
     {{ lem (List.fold_right union_map [[E_k1..E_kn]] Map.empty) }}
     {{ ocaml (assert false) }}
   | E_k u- E_k1 .. E_kn                                            :: M :: multi_set_minus
     {{ hol arb }} {{ lem arb }} {{ ocaml assert false }}

 
 tinf :: 'tinf_' ::=                                                 
    {{ com Type variables, type, and constraints, bound to an identifier }}
    | t                                                 :: :: typ
    | E_k , S_N , tag , t         :: :: quant_typ                                                                 

 E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::=             {{ phantom }}
                                                                 {{ hol (id |-> tinf) }}
                                                                 {{ lem map x f_desc }}
   {{ com Type environments }}
   | { id1 |-> tinf1 , .. , idn |-> tinfn }                    :: :: base
     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }}
     {{ lem (List.fold_right (fun (x,f) m -> Map.insert x f m) [[id1 tinf1 .. idn tinfn]] Map.empty) }} 
   | ( E_t1 u+ .... u+ E_tn )                                         :: M :: union
     {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }}
     {{ lem (List.fold_right union_map [[E_t1....E_tn]] Map.empty) }}
     {{ ocaml (assert false) }}
   | u+ E_t1 .. E_tn                                            :: M :: multi_union
     {{ hol arb }}
     {{ lem arb }}
     {{ ocaml assert false }}
   | E_t u- E_t1 .. E_tn                                            :: M :: multi_set_minus
     {{ hol arb }} {{ lem arb }} {{ ocaml assert false }}
   | ( E_t1 inter .... inter E_tn )                                  :: M :: intersect
     {{ hol arb }}
     {{ lem syntax error }}
     {{ ocaml (assert false) }}
   | inter E_t1 .. E_tn                                            :: M :: multi_inter
     {{ hol arb }}
     {{ lem arb }}
     {{ ocaml assert false }}


 field_typs :: 'FT_' ::=     {{ phantom }}
 {{ com Record fields }}
 | id1 : t1 , .. , idn : tn :: :: fields

 E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::=             {{ phantom }}
                                                                 {{ hol (id |-> t) }}
                                                                 {{ lem map x f_desc }}
   {{ com Record environments }}
   | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn }                    :: :: concrete
     {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }}
     {{ lem (List.fold_right (fun (x,f) m -> Map.insert x f m)  Map.empty) }} 
   | E_r1 u+ .. u+ E_rn                                          :: M :: union
     {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
     {{ lem (List.fold_right union_map [[E_r1..E_rn]] Map.empty) }}
     {{ ocaml (assert false) }}

  enumerate_map :: '' ::=
   | { num1 |-> id1 ... numn |-> idn }                           :: :: enum_map

  E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::=
   {{ com Enumeration environments }}
   | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn }     :: :: base
   | E_e1 u+ .. u+ E_en                                         :: :: union

ts :: ts_ ::=                                     {{ phantom }}
  | t1 , .. , tn :: :: lst 

formula :: formula_ ::=
  | judgement                                                   :: :: judgement

  | formula1 .. formulan                                        :: :: dots

   | E_k ( id ) gives kinf                                      :: :: lookup_k
     {{ com Kind lookup }}
     {{ hol (FLOOKUP [[E_k]] [[id]] = SOME [[k]]) }}
     {{ lem Map.lookup [[id]] [[E_k]] = Just [[k]] }} 

   | E_t ( id ) gives tinf                                      :: :: lookup_t
     {{ com Type lookup }}
     {{ hol (FLOOKUP [[E_t]] [[id]] = SOME [[t]]) }}
     {{ lem Map.lookup [[id]] [[E_t]] = Just [[t]] }} 

  | E_k ( id ) <-| k						:: :: update_k
     {{ com Update the kind associated with id to k }}        

  | E_r ( id0 .. idn ) gives t , ts                      :: :: lookup_r
     {{ com Record lookup }}

  | E_r ( t ) gives id0 : t0 .. idn : tn                 :: :: lookup_rt
    {{ com Record looup by type }}

  | E_e ( t ) gives enumerate_map			:: :: lookup_e
    {{ com Enumeration lookup by type }}

   | 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

   | num1 lt ... lt numn                                         :: :: increasing

   | num1 gt ... gt numn                                         :: :: decreasing

   | E_k1 = E_k2                                                 :: :: E_k_eqn
     {{ ichl ([[E_k1]] = [[E_k2]]) }}

   | E_k1 ~= E_k2                                                :: :: E_k_approx
     {{ ichl 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]]) }}
 
   | I1 = I2                                                     :: :: I_eqn
     {{ ichl ([[I1]] = [[I2]]) }}

   | effects1 = effects2                                        :: :: Ef_eqn
     {{ ichl ([[effects1]] = [[effects2]]) }}

   | t1 = t2                                                     :: :: t_eq
     {{ ichl ([[t1]] = [[t2]]) }}
   | ne1 = ne2							:: :: ne_eq
     {{ ichl ([[ne1]] = [[ne2]]) }}


defns
check_t :: '' ::=

defn
E_k |-t t ok :: :: check_t :: check_t_ 
 {{ com Well-formed types }}
 by

 E_k(id) gives K_Typ
 ------------------------------------------------------------ :: var
 E_k |-t id ok

 E_k(id) gives K_infer
 E_k(id) <-| K_Typ
 ------------------------------------------------------------ :: varInfer
 E_k |-t id ok

 E_k(id) gives K_Abbrev t
 E_k u- {id |-> K_Abbrev t} |-t t ok
 ------------------------------------------------------------ :: varAbbrev
 E_k |-t id ok 

 E_k |-t t1 ok
 E_k |-t t2 ok
 E_k |-e effects ok
 ------------------------------------------------------------ :: fn
 E_k |-t t1 -> t2 effects tag S_N ok

 E_k |-t t1 ok .... E_k |-t tn ok
 ------------------------------------------------------------ :: tup
 E_k |-t (t1 * .... * tn) ok

 E_k(id) gives K_Lam(k1..kn -> K_Typ)
 E_k,k1 |- t_arg1 ok .. E_k,kn |- t_argn ok
 ------------------------------------------------------------ :: app
 E_k |-t id t_arg1 .. t_argn ok

defn 
E_k |-e effects ok :: :: check_ef :: check_ef_
{{ com Well-formed effects }}
by

E_k(id) gives K_Efct
----------------------------------------------------------- :: var
E_k |-e effect id ok

E_k(id) gives K_infer
E_k(id) <-| K_Efct
------------------------------------------------------------ :: varInfer
E_k |-e effect id ok

------------------------------------------------------------- :: set
E_k |-e effect { efct1 , .. , efctn } ok

defn 
E_k |-n ne ok :: :: check_n :: check_n_
{{ com Well-formed numeric expressions }}
by

E_k(id) gives K_Nat
----------------------------------------------------------- :: var
E_k |-n id ok

E_k(id) gives K_infer
E_k(id) <-| K_Nat
------------------------------------------------------------ :: varInfer
E_k |-n id 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 }}
by

E_k(id) gives K_Ord
----------------------------------------------------------- :: var
E_k |-o id ok

E_k(id) gives K_infer
E_k(id) <-| K_Ord
------------------------------------------------------------ :: varInfer
E_k |-o id ok


defn
E_k , k |- t_arg ok :: :: check_targs :: check_targs_ 
{{ com Well-formed type arguments kind check matching the application type variable }}
by

E_k |-t t ok
--------------------------------------------------------- :: typ
E_k , K_Typ |- t ok

E_k |-e effects ok
--------------------------------------------------------- :: eff
E_k , K_Efct |- effects 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


%% % 
%% % %TODO type equality isn't right; neither is type conversion
%% % 
defns
teq :: '' ::=

defn
E_d |- t1 = t2 :: :: teq :: teq_ 
{{ com Type equality }}
by

E_k |-t t ok
------------------------------------------------------------ :: refl
<E_k,E_r,E_e> |- t = t
 
E_d |- t2 = t1
------------------------------------------------------------ :: sym
E_d |- t1 = t2
 
E_d |- t1 = t2
E_d |- t2 = t3
------------------------------------------------------------ :: trans
E_d |- t1 = t3

E_k(id) gives K_Abbrev u
<E_k,E_r,E_e> |- u = t
------------------------------------------------------------ :: abbrev
<E_k,E_r,E_e> |- id = t 
 
E_d |- t1 = t3
E_d |- t2 = t4
------------------------------------------------------------ :: arrow
E_d |- t1 -> t2 effects tag = t3 -> t4 effects tag
 
E_d |- t1 = u1 .... E_d |- tn = un
------------------------------------------------------------ :: tup
E_d |- (t1*....*tn) = (u1*....*un)

E_k(id) gives K_Lam (k1 .. kn -> K_Typ)
<E_k,E_r,E_e>,k1 |- t_arg1 = t_arg'1 .. <E_k,E_r,E_e>,kn |- t_argn = t_arg'n
------------------------------------------------------------ :: app
<E_k,E_r,E_e> |- id t_arg1 .. t_argn = id t_arg'1 .. t_arg'n

defn
E_d , k |- t_arg = t_arg' :: :: targeq :: targeq_ by

defns
convert_kind :: '' ::=

defn
E_k |- kind ~> k :: :: convert_kind :: convert_kind_ by

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

E_k |- kind ~> k
----------------------------------------------------------- :: kind
<E_k,E_r,E_e> |- kind id ~> {id |-> k}, {}

E_k(id) gives k
----------------------------------------------------------- :: nokind
<E_k,E_r,E_e> |- id ~> {id |-> 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 |- id IN {num1 , ... , numn} ~> {}, {id IN {num1 , ..., numn}}

defn 
E_d |- typschm ~> t , E_k2 , S_N :: :: convert_typschm :: convert_typschm_
{{ com Convert source types with typeschemes to internal types and kind environments }}
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 }}
by
 
E_k(id) gives K_Typ
------------------------------------------------------------ :: var
<E_k,E_r,E_e> |- :Typ_var: id ~> id

E_d |- typ1 ~> t1
E_d |- typ2 ~> t2
------------------------------------------------------------ :: fn
E_d |- typ1->typ2 effects ~> t1->t2 effects None
 
E_d |- typ1 ~> t1 .... E_d |- typn ~> tn
------------------------------------------------------------ :: tup
E_d |- typ1 * .... * typn ~> (t1 * .... * tn)

E_k(id) gives K_Lam (k1..kn -> K_Typ)
<E_k,E_r,E_e>,k1 |- typ_arg1 ~> t_arg1 .. <E_k,E_r,E_e>,kn |- typ_argn ~> t_argn
------------------------------------------------------------ :: app
<E_k,E_r,E_e> |- id typ_arg1 .. typ_argn ~> id t_arg1 .. t_argn

E_d |- typ ~> t1
E_d |- t1 = t2
------------------------------------------------------------ :: eq
E_d |- typ ~> t2

defn
E_d , k |- typ_arg ~> t_arg :: :: convert_targ :: convert_targ_
{{ com Convert source type arguments to internals }}
by
 
defn 
|- nexp ~> ne :: :: convert_nexp :: convert_nexp_ 
{{ com Convert and normalize numeric expressions }}
by
 
------------------------------------------------------------ :: var
|- id ~> id

------------------------------------------------------------ :: 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' , S_N :: :: coerce_typ :: coerce_typ_ by

E_d |- t = u
-------------------------------------- :: eq
E_d |- t :> u, {}

E_d |- t1 :> u1, S_N1 .. E_d |- tn :> un, S_Nn
-------------------------------------- :: tuple
E_d |- (t1 * .. * tn) :> (u1 * .. * un), S_N1 u+ .. u+ S_Nn

-------------------------------------- :: enum
E_d |- enum ne1 ne2 order :> enum ne3 ne4 order, {ne3 <= ne1, ne3+ne4 >= ne1 + ne2}

E_e(t) gives { </numi |-> idi//i/> num |-> id </num'j |-> id'j//j/> }
------------------------------------------------ :: to_enumerate
<E_k,E_r,E_e> |- enum num zero order :> t, {}

E_e(t) gives { num1 |-> id1 ... numn |-> idn }
------------------------------------------------ :: from_enumerate
<E_k,E_r,E_e> |- t :> enum num1 numn + (- num1) inc, {}

-------------------------------------- :: to_num
E_d |- vector ne1 ne2 order :t_arg_typ: bit :> enum ne3 ne4 order, { ne3 = zero, ne4 = 2** ne2}

-------------------------------------- :: from_num
E_d |- enum ne1 ne2 order :> vector ne3 ne4 order :t_arg_typ: bit, {ne3 = zero, id = ne1 + ne2, ne4 = 2** id}


defns
check_lit :: '' ::=
 
defn
|- lit : t :: :: check_lit :: check_lit_ 
{{ com Typing literal constants }}
by

 ------------------------------------------------------------ :: true
 |- true : bool

 ------------------------------------------------------------ :: false
 |- false : bool
 
 ------------------------------------------------------------ :: num
 |- num : enum num zero inc
 
 ------------------------------------------------------------- :: string
 |- string : string

 num = bitlength(hex)
 ------------------------------------------------------------ :: hex
 |- hex : vector zero num inc :T_var: bit

 num = bitlength(bin)
 ------------------------------------------------------------ :: bin 
 |- bin  : vector zero num inc :T_var: bit

 ------------------------------------------------------------ :: unit
 |- () : unit

 ------------------------------------------------------------ :: bitzero
 |- bitzero : bit

 ------------------------------------------------------------ :: bitone
 |- bitone : bit


defns
check_pat :: '' ::=
 
defn
E |- pat : t gives E_t , S_N :: :: check_pat :: check_pat_ 
{{ com Typing patterns, building their binding environment }}
by

|- lit : t
------------------------------------------------------------ :: lit
E |- lit : t gives {}, {}

E_k |-t t ok
------------------------------------------------------------ :: wild
<E_t,<E_k,E_r,E_e>> |- _ : t gives {}, {}

E |- pat : t gives E_t1,S_N
id NOTIN dom(E_t1)
------------------------------------------------------------ :: as
E |- (pat as id) : t gives (E_t1 u+ {id|->t}),S_N

<E_t,E_d> |- pat : t gives E_t1,S_N
E_t(id) gives {}, {}, Default, t
------------------------------------------------------------ :: as_default
<E_t,E_d> |- (pat as id) : t gives (E_t1 u+ {id|->t}),S_N

E_d |- typ ~> t
<E_t,E_d> |- pat : t gives E_t1,S_N
------------------------------------------------------------ :: typ
<E_t,E_d> |- (<typ> pat) : t gives E_t1,S_N

E_t(id) gives (t1*..*tn) -> id t_args effect { } Ctor
<E_t,E_d> |- pat1 : t1 gives E_t1,S_N1 .. <E_t,E_d> |- patn : tn gives E_tn,S_Nn
disjoint doms(E_t1,..,E_tn)
------------------------------------------------------------ :: ident_constr
<E_t,E_d> |- id pat1 .. patn : id t_args gives u+ E_t1 .. E_tn, S_N1 u+ .. u+ S_Nn

E_k |-t t ok
------------------------------------------------------------ :: var
<E_t,<E_k,E_r,E_e>> |- :P_id: id : t gives (E_t u+ {id|->t}),{}

E_t(id) gives {},{},Default,t
------------------------------------------------------------ :: var_default
<E_t,E_d> |- :P_id: id : t gives (E_t u+ {id|->t}),{}

E_r(</idi//i/>) gives id t_args, (</ti//i/>)
</<E_t,<E_k,E_r,E_e>> |- pati : ti gives E_ti,S_Ni//i/>
disjoint doms(</E_ti//i/>)
------------------------------------------------------------ :: record
<E_t,<E_k,E_r,E_e>> |- { </idi = pati//i/> semi_opt } : id t_args gives :E_t_multi_union: u+ </E_ti//i/>, u+ </S_Ni//i/>
 
E |- pat1 : t gives E_t1,S_N1 .. E |- patn : t gives E_tn,S_Nn
disjoint doms(E_t1 , .. , E_tn)
length(pat1 .. patn) = num
----------------------------------------------------------- :: vector
E |- [ pat1 , .. , patn ] : vector :t_arg_nexp: id num+id inc t gives (E_t1 u+ .. u+ E_tn),S_N1 u+ .. u+ S_Nn

E |- pat1 : t gives E_t1,S_N1 ... E |- patn : t gives E_tn,S_Nn
disjoint doms(E_t1 , ... , E_tn)
num1 lt ... lt numn
----------------------------------------------------------- :: indexedVectorInc
E |- [ num1 = pat1 , ... , numn = patn ] : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives (E_t1 u+ ... u+ E_tn), {id<=num1, id' >= numn + (- num1)} u+ S_N1 u+ ... u+ S_Nn

E |- pat1 : t gives E_t1,S_N1 ... E |- patn : t gives E_tn,S_Nn
disjoint doms(E_t1 , ... , E_tn)
num1 gt ... gt numn
----------------------------------------------------------- :: indexedVectorDec
E |- [ num1 = pat1 , ... , numn = patn ] : vector :t_arg_nexp: id :t_arg_nexp: id' dec t gives (E_t1 u+ ... u+ E_tn), {id>=num1,id'<=num1 +(-numn)} u+ S_N1 u+ ... u+ S_Nn

E |- pat1 : vector ne1 ne'1 inc t gives E_t1,S_N1 ... E |- patn : vector nen ne'n inc t gives E_tn,S_Nn
disjoint doms(E_t1 , ... , E_tn)
S_N0 = consistent_increase ne1 ne'1 ... nen ne'n
----------------------------------------------------------- :: vectorConcatInc
E |- pat1 : ... : patn : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives (E_t1 u+ ... u+ E_tn),{id<=ne1,id'>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ S_Nn

E |- pat1 : vector ne1 ne'1 dec t gives E_t1,S_N1 ... E |- patn : vector nen ne'n dec t gives E_tn,S_Nn
disjoint doms(E_t1 , ... , E_tn)
S_N0 = consistent_decrease ne1 ne'1 ... nen ne'n
----------------------------------------------------------- :: vectorConcatDec
E |- pat1 : ... : patn : vector :t_arg_nexp: id :t_arg_nexp: id' inc t gives (E_t1 u+ ... u+ E_tn),{id>=ne1,id'>= ne'1 + ... + ne'n} u+ S_N0 u+ S_N1 u+ ... u+ S_Nn

E |- pat1 : t1 gives E_t1,S_N1 .... E |- patn : tn gives E_tn,S_Nn
disjoint doms(E_t1,....,E_tn)
------------------------------------------------------------ :: tup
E |- (pat1, ...., patn) : (t1 * .... * tn) gives (E_t1 u+ .... u+ E_tn),S_N1 u+ .... u+ S_Nn 

E |- pat1 : t gives E_t1,S_N1 .. E |- patn : t gives E_tn,S_Nn
disjoint doms(E_t1,..,E_tn)
------------------------------------------------------------ :: list
E |- [|pat1, .., patn |] : list t gives (E_t1 u+ .. u+ E_tn),S_N1 u+ .. u+ S_Nn


defns
check_exp :: '' ::=
 
defn
E |- exp : t gives I , E_t :: :: check_exp :: check_exp_ 
{{ com Typing expressions, collecting nexp constraints, effects, and new bindings }}
by

<E_t,E_d> |- exp : u gives <S_N,effects>,E_t1
E_d |- u :> t, S_N2
------------------------------------------------------------ :: coerce
<E_t,E_d> |- exp : t gives <S_N u+ S_N2,effects>,E_t1
 
E_t(id) gives t
------------------------------------------------------------ :: var
<E_t,E_d> |- id : t gives Ie,E_t

E_t(id) gives register t
------------------------------------------------------------ :: reg
<E_t,E_d> |- id : t gives <{},effect {rreg}>,E_t

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

E_t(id) gives {</idi |-> ki//i/>},S_N,tag,u
t = u [</ui/idi//i/>]
----------------------------------------------------------- :: ty_app
<E_t,E_d> |- id : t gives <S_N,pure>,E_t

% Need to take into account possible type variables here
E_t(id) gives t' -> t effect {} Ctor {} 
<E_t,E_d> |- exp : t' gives I,E_t
------------------------------------------------------------ :: ctor
<E_t,E_d> |- id exp : t gives I,E_t

% Need to take into account possible type variables on result of id
E_t(id) gives t' -> t effects tag S_N
<E_t,E_d> |- exp : t' gives I,E_t
------------------------------------------------------------ :: app
<E_t,E_d> |- id exp : t gives I u+ <S_N,effects>, E_t

E_t(id) gives t' -> t effects tag S_N
<E_t,E_d> |- (exp1,exp2) : t' gives I,E_t
------------------------------------------------------------ :: infix_app
<E_t,E_d> |- :E_app_infix: exp1 id exp2 : t gives I u+ <S_N, effects>, E_t

E_r(</idi//i/>) gives id t_args, </ti//i/>
</ <E_t,<E_k,E_r,E_e>> |- expi : ti gives Ii,E_t//i/>
------------------------------------------------------------ :: record
<E_t,<E_k,E_r,E_e>> |- { </idi = expi//i/> semi_opt} : id t_args gives u+ </Ii//i/>, E_t

<E_t,<E_k,E_r,E_e>> |- exp : id t_args gives I,E_t
E_r(id t_args) gives </ id'n:t'n//n/>
</ <E_t,<E_k,E_r,E_e>> |- expi : ti gives Ii,E_t//i/>
</idi:ti//i/> SUBSET </id'n : t'n//n/>
------------------------------------------------------------ :: recup
<E_t,<E_k,E_r,E_e>> |- { exp with </idi = expi//i/> semi_opt } : id t_args gives I u+ </Ii//i/>, E_t

E |- exp1 : t gives I1,E_t ... E |- expn : t gives In,E_t
length(exp1 ... expn) = num
------------------------------------------------------------ :: vector
E |- [ exp1 , ... , expn ] : vector zero num inc t gives I1 u+ ... u+ In, E_t
 
E |- exp1 : vector ne ne' inc t gives I1,E_t
E |- exp2 : enum ne2 ne2' inc gives I2,E_t
------------------------------------------------------------- :: vectorgetInc
E |- :E_vector_access: exp1 [ exp2 ] : t gives I1 u+ I2 u+ <{ne<=ne2,ne2+ne2'<=ne+ne'},pure>,E_t

E |- exp1 : vector ne ne' dec t gives I1,E_t
E |- exp2 : enum ne2 ne'2 dec gives I2,E_t
------------------------------------------------------------- :: vectorgetDec
E |- :E_vector_access: exp1 [ exp2 ] : t gives I1 u+ I2 u+ <{ne>=ne2,ne2+(-ne2')<=ne+(-ne')},pure>,E_t

E |- exp1 : vector ne ne' order t gives I1,E_t
E |- exp2 : enum ne2 ne'2 order gives I2,E_t
E |- exp3 : enum ne3 ne'3 order gives I3,E_t
------------------------------------------------------------- :: vectorsub
E |- :E_vector_subrange: exp1[ exp2 : exp3 ] : vector :t_arg_nexp: id :t_arg_nexp: id' order t gives I1 u+ I2 u+ I3 u+ <{ne <= ne2, id >= ne2 , id <= ne2+ne2', ne2+ne'2<=ne3, ne+ne'>=ne3+ne'3, id' <=ne3 + ne'3},pure>,E_t

E |- exp : vector ne1 ne2 order t gives I,E_t
E |- exp1 : enum ne3 ne4 order gives I1,E_t
E |- exp2 : t gives I2,E_t
------------------------------------------------------------ :: vectorup
E |- [ exp with exp1 = exp2 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ <{ne1 <= ne3, ne1 + ne2 >= ne3 + ne4},pure>,E_t

E |- exp : vector ne1 ne2 order t gives I,E_t
E |- exp1 : enum ne3 ne4 order gives I1,E_t
E |- exp2 : enum ne5 ne6 order gives I2,E_t
E |- exp3 : vector ne7 ne8 order t gives I3,E_t
------------------------------------------------------------ :: vecrangeup
E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ I3 u+ <{ne1 <= ne3, ne1 <= ne5,ne3+ne4 <= ne5, ne1 + ne2 <= ne5 + ne6 + (- ne3) + (- ne4), ne7 + ne8 = ne1 + ne2 + (- ne3) + (- ne4)},pure>,E_t

E |- exp : vector ne1 ne2 order t gives I,E_t
E |- exp1 : enum ne3 ne4 order gives I1,E_t
E |- exp2 : enum ne5 ne6 order gives I2,E_t
E |- exp3 : t gives I3,E_t
------------------------------------------------------------ :: vecrangeupvalue
E |- [ exp with exp1 : exp2 = exp3 ] : vector ne1 ne2 order t gives I u+ I1 u+ I2 u+ I3 u+ <{ne1 <= ne3, ne1 <= ne5,ne3+ne4 <= ne5, ne1 + ne2 <= ne5 + ne6 + (- ne3) + (- ne4)},pure>,E_t


E_r (id t_args) gives </idi : ti//i/> id : t </id'j : t'j//j/>
<E_t,<E_k,E_r,E_e>> |- exp : id t_args gives I,E_t
------------------------------------------------------------ :: field
<E_t,<E_k,E_r,E_e>> |- exp.id : t gives I,E_t

</<E_t,E_d> |- pati : t gives E_ti,S_Ni//i/>
</<(E_t u+ E_ti),E_d> |- expi : u gives Ii,E_t'i//i/>
<E_t,E_d> |- exp : t gives I,E_t
------------------------------------------------------------ :: case
<E_t,E_d> |- switch exp { </case pati -> expi//i/> }: u gives I u+ </Ii u+ <S_Ni,pure>//i/>, inter </E_t'i//i/> u- </E_ti//i/>

<E_t,E_d> |- exp : t gives I,E_t
------------------------------------------------------------ :: typed
<E_t,E_d> |- (typ) exp : t gives I,E_t

<E_t,E_d> |- letbind gives E_t1, S_N, effects, {}
<(E_t u+ E_t1),E_d> |- exp : t gives I2, E_t2
------------------------------------------------------------ :: let
<E_t,E_d> |- letbind in exp : t gives <S_N,effects> u+ I2, E_t
 
E |- exp1 : t1 gives I1,E_t .... E |- expn : tn gives In,E_t
------------------------------------------------------------ :: tup
E |- (exp1, .... , expn) : (t1 * .... * tn) gives I1 u+ .... u+ In,E_t
 
E |- exp1 : t gives I1,E_t .. E |- expn : t gives In,E_t
------------------------------------------------------------ :: list
E |- [|exp1, .., expn |] : list t gives I1 u+ .. u+ In,E_t

E |- exp1 : bool gives I1,E_t
E |- exp2 : t gives I2,E_t2
E |- exp3 : t gives I3,E_t3
------------------------------------------------------------ :: if
E |- if exp1 then exp2 else exp3 : t gives I1 u+ I2 u+ I3,(E_t2 inter E_t3)

<E_t,E_d> |- exp1 : enum ne1 ne2 order gives I1,E_t
<E_t,E_d> |- exp2 : enum ne3 ne4 order gives I2,E_t
<E_t,E_d> |- exp3 : enum ne5 ne6 order gives I3,E_t
<(E_t u+ {id |-> enum ne1 ne3+ne4 order}),E_d> |- exp4 : t gives I4,(E_t u+ {id |-> enum ne1 ne3+ne4 order})
----------------------------------------------------------- :: for
<E_t,E_d> |- foreach id from exp1 to exp2 by exp3 exp4 : t gives I1 u+ I2 u+ I3 u+ I4 u+ <{ne1 <= ne3+ne4},pure>,E_t

E |- exp1 : t gives I1,E_t
E |- exp2 : list t gives I2,E_t
------------------------------------------------------------ :: cons
E |- exp1 :: exp2 : list t gives I1 u+ I2,E_t

|- lit : t
------------------------------------------------------------ :: lit
<E_t,E_d> |- lit : t gives Ie,E_t

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

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

E |- exp:t gives I1, E_t1
E |- lexp:t gives I2, E_t2
------------------------------------------------------------ :: assign
E |- lexp := exp : unit gives I u+ I2, E_t2

defn
E |- lexp : t gives I , E_t :: :: check_lexp :: check_lexp_
{{ com Check the left hand side of an assignment }}
by

E_t(id) gives register t
---------------------------------------------------------- :: wreg
<E_t,E_d> |- id : t gives <{},effect{ wreg }>, E_t

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

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

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

E_t(id) gives t1 -> t effect {</efcti//i/>, wmem, </efct'j//j/>} Extern {}
<E_t,E_d> |- exp : t1 gives I,E_t1
---------------------------------------------------------- :: wmem
<E_t,E_d> |- id exp : t gives I u+ <{},effect{wmem}>,E_t

E |- exp : enum ne1 ne2 order gives I1,E_t
E |- lexp : vector ne3 ne4 order t gives I2,E_t
---------------------------------------------------------- :: wbit
E |- lexp [exp] : t gives I1 u+ I2 u+ <{ne3 <= ne1, ne1 + ne2 <= ne3 + ne4},pure>,E_t

E |- exp1 : enum ne1 ne2 order gives I1,E_t
E |- exp2 : enum ne3 ne4 order gives I2,E_t
E |- lexp : vector ne5 ne6 order t gives I3,E_t
---------------------------------------------------------- :: wslice
E |- lexp [exp1 : exp2] : vector :Ne_var: id1 :Ne_var: id2 order t gives I1 u+ I2 u+ I3 u+ <{ne5<=ne1, ne1+ne2 <= ne3, ne3+ne4<= ne5+ne6, id1 <= ne1, id2 <= 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 (id1 t_args) gives </idi : ti//i/> id : t </id'j : t'j//j/>
<E_t,<E_k,E_r,E_e>> |- lexp : id1 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 , effects , 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,effects>,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, effects, 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,effects>,E_t2
------------------------------------------------------------ :: val_noannot
<E_t,E_d> |- let pat = exp gives E_t1, S_N1 u+ S_N2, effects,{}

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 naming_scheme_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 naming_scheme_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 naming_scheme_opt = const struct forall </quant_itemi//i/> . { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<E_k1,E_r1,{}>>

E_t = { id1 |-> t1 -> :T_var: id pure Ctor {}, ..., idn |-> tn -> :T_var: 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 naming_scheme_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_k1 = { id |-> K_Lam (k1 ... km -> K_Typ) } u+ </E_ki//i/>
<E_k u+ E_k1,E_r,E_e> |- typ1 ~> t1 ... <E_k u+ E_k1,E_r,E_e> |- typn ~> tn
t = id :t_arg_typ: id'1 ... :t_arg_typ: id'm
E_t = { id1 |-> E_k1, u+</S_Ni//i/>, Ctor, t1 -> t pure Ctor {}, ... , idn |-> E_k1, u+</S_Ni//i/>, Ctor, tn -> t pure Ctor {} }
------------------------------------------------------------ :: quant_union
<E_k,E_r,E_e> |- typedef id naming_scheme_opt = const union forall </quant_itemi//i/> . { typ1 id1 ; ... ; typn idn semi_opt } gives <E_t,<E_k1,{},{}>>

% Save these as enumerations for coercion
E_t = {id1 |-> id, ..., idn |-> id}
E_e = { id |-> { num1 |-> id1 ... numn |-> idn} }
------------------------------------------------------------- :: enumerate
E_d |- typedef id naming_scheme_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_k1,S_N1,None, t1 -> t effects None S_N1
</E_d |- quant_itemi ~> E_ki,S_Ni//i/>
S_N2 = u+ </S_Ni//i/>
E_k1 ~= </E_ki//i/>
E_d1 = <E_k1,{},{}> 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,effects'j>,E_t'j//j/>
S_N3 = u+ </S_N'j u+ S_N''j//j/>
effects = u+ </effects'j//j/>
S_N = resolve ( S_N1 u+ S_N2 u+ S_N3)
------------------------------------------------------------- :: rec_function
<E_t,E_d> |- function rec forall </quant_itemi//i/> . typ effects </id patj = expj//j/> gives E_t, S_N

E_t(id) gives t1 -> t effects None S_N1
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,effects'j>,E_t'j//j/>
effects = u+ </effects'j//j/>
S_N = resolve (S_N1 u+ </S_N'j u+ S_N''j//j/>)
------------------------------------------------------------- :: rec_function2
<E_t,E_d> |- function rec typ effects </id patj = expj//j/> gives E_t, S_N

</<E_k,E_r,E_e> |- quant_itemi ~> E_ki,S_Ni//i/>
S_N1 = u+ </S_Ni//i/>
E_k2 = E_k u+ </E_ki//i/>
<E_k2,E_r,E_e> |- typ ~> t
</<E_t,<E_k2,E_r,E_e>> |- patj : t1 gives E_tj,S_N'j//j/>
E_t2 = (E_t u+ {id |-> t1 -> t effects None S_N1})
</<(E_t2 u+ E_tj),<E_k2,E_r,E_e>> |- expj : t gives <S_N'j,effects'j>,E_t'j//j/>
effects = u+ </effects'j//j/>
S_N = resolve (S_N1 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 effects </id patj = expj//j/> gives E_t2, S_N

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

t2 = t1 -> t effects None S_N1
E_t(id) gives E_k1,S_N1,None, t2
</<E_k,E_r,E_e> |- quant_itemi ~> E_ki,S_Ni//i/>
S_N2 = u+ </S_Ni//i/>
E_k1 ~= </E_ki//i/>
<E_k1 u+ E_k,E_r,E_e> |- typ ~> t
</<E_t,<E_k u+ E_k1,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_k1,E_r,E_e>> |- expj : t gives <S_N''j,effects'j>,E_t'j//j/>
S_N3 = u+ </S_N'j u+ S_N''j//j/>
effects = u+ </effects'j//j/>
S_N = resolve ( S_N1 u+ S_N2 u+ S_N3)
------------------------------------------------------------- :: function
<E_t,<E_k,E_r,E_e>> |- function forall </quant_itemi//i/> . typ effects </id patj = expj//j/> gives E_t, S_N

E_t(id) gives t1 -> t effects 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 effects None S_N1} u+ E_tj),E_d> |- expj : t gives <S_N''j,effects'j>,E_t'j//j/>
effects = u+ </effects'j//j/>
S_N = resolve (S_N1 u+ </S_N'j u+ S_N''j//j/>)
------------------------------------------------------------- :: function2
<E_t,E_d> |- function typ effects </id patj = expj//j/> gives E_t, S_N

</<E_k,E_r,E_e> |- quant_itemi ~> E_ki,S_Ni//i/>
S_N1 = u+ </S_Ni//i/>
E_k2 = E_k u+ </E_ki//i/>
<E_k2,E_r,E_e> |- typ ~> t
</<E_t,<E_k2,E_r,E_e>> |- patj : t1 gives E_tj,S_N'j//j/>
E_t2 = (E_t u+ {id |-> t1 -> t effects None S_N1})
</<(E_t u+ E_tj),<E_k2,E_r,E_e>> |- expj : t gives <S_N'j,effects'j>,E_t'j//j/>
effects = u+ </effects'j//j/>
S_N = resolve (S_N1 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 effects </id patj = expj//j/> gives E_t2, S_N

E_d |- typ ~> t
</<E_t,E_d> |- patj : t1 gives E_tj,S_N'j//j/>
E_t2 = (E_t u+ {id |-> t1 -> t effects None S_N})
</<(E_t u+ E_tj),E_d> |- expj : t gives <S_N'j,effects'j>,E_t'j//j/>
effects = u+ </effects'j//j/>
S_N = resolve (u+ </S_N'j u+ S_N''j//j/>)
------------------------------------------------------------- :: function_no_spec2
<E_t,E_d> |- function typ effects </id patj = expj//j/> gives E_t2, 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_typing_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 id gives {}, {id |-> 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 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_typing_spec gives E_t1, E_k1
--------------------------------------------------------- :: default
<E_t,E_d> |- default_typing_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