path: root/language/l2_rules.ott

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

embed
{{ lem

let rec remove_one i l =
  match l with
  | [] -> []
  | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2)
end

let rec remove_from l l2 =
  match l2 with 
  | [] -> l
  | i::l2' -> remove_from (remove_one i l) l2'
end

let disjoint s1 s2 = Set.null (s1 inter s2)

let rec disjoint_all sets =
  match sets with
  | [] -> true
  | s1::[] -> true
  | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets))
end
}}

 
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_' ::=                                
{{ com Internal types }}
   | id                                           :: :: id
   | kid                                          :: :: var
   | t1 -> t2 effect 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_' ::=                                 
{{ 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 }}
   | kid                                 :: :: var
   | num                                 :: :: const
   | ne1 * ne2                           :: :: mult
   | ne1 + ... + nen                     :: :: add
   | 2 ** ne				 :: :: exp
   | ( - ne )                            :: :: unary
   | zero   				 :: M :: zero
     {{ lem (Ne_const 0) }}
   | 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_' ::=  
 {{ com Argument to type constructors }}
 | t :: :: typ
 | ne :: :: nexp
 | effect :: :: effect
 | order :: :: order

 t_args :: '' ::=   {{ lem list t_arg }}
  {{ 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
   | kid 'IN' { num1 , ... , numn } :: :: in

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.foldr (++) [] [[S_N1..S_Nn]]) }}
     {{ 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
     {{ lem [[S_N]] (* Write constraint solver *) }}
 

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

 tid :: 'tid_' ::=
   {{ com A type identifier or type variable }}
   | id                                      :: :: id
   | kid                                     :: :: var

 E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::=             {{ phantom }}
                                                                 {{ hol (tid-> kinf) }}
                                                                 {{ lem (map tid kinf) }}
   {{ com Kind environments }}
   | { tid1 |-> kinf1 , .. , tidn |-> kinfn }    :: :: concrete
     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }}
     {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} 
   | 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.foldr (union) Map.empty [[E_k1..E_kn]]) }}
     {{ ocaml (assert false) }}
   | E_k u- E_k1 .. E_kn                                            :: M :: multi_set_minus
     {{ hol arb }} 
     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]]))
                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} 
     {{ 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                                                             

 field_typs :: 'FT_' ::=     {{ phantom }}
                             {{ lem list (id * t) }}
 {{ com Record fields }}
 | id1 : t1 , .. , idn : tn :: :: fields
   {{ lem [[id1 t1..idn tn]] }}

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

  enumerate_map :: '' ::=                                        {{ phantom }}
                                                                 {{ lem (list (nat*id)) }}
   | { num1 |-> id1 ... numn |-> idn }                           :: :: enum_map
    {{ lem [[num1 id1...numn idn]] }}

  E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::=            {{ phantom }}
                                                                 {{ lem (map t (list (nat*id))) }}
   {{ com Enumeration environments }}
   | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn }     :: :: base
     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} 
   | E_e1 u+ .. u+ E_en                                         :: :: union
     {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }}

    
embed
{{ lem
 type definition_env =
   | DenvEmp
   | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id)))

}}

grammar

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


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

embed
{{ lem
let blength (bit) = Ne_const 8
let hlength (bit) = Ne_const 8

 type env =
   | EnvEmp 
   | Env of (map id tinf) * definition_env

 type inf = 
   | Iemp
   | Inf of (list nec) * effect

 val denv_union : definition_env -> definition_env -> definition_env
 let denv_union de1 de2 = 
  match (de1,de2) with
   | (DenvEmp,de2) -> de2
   | (de1,DenvEmp) -> de1
   | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) ->
      Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2)
   end

 val env_union : env -> env -> env
 let env_union e1 e2 =
   match (e1,e2) with
    | (EnvEmp,e2) -> e2
    | (e1,EnvEmp) -> e1
    | ((Env te1 de1),(Env te2 de2)) ->
      Env (te1 union te2) (denv_union de1 de2)
 end

let inf_union i1 i2 =
  match (i1,i2) with 
 | (Iemp,i2) -> i2
 | (i1,Iemp) -> i1
 | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2))
 end

let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*)

}}

grammar

 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
   {{ lem (env_union [[E]] [[E']]) }}

 I :: '' ::=                                                     {{ lem inf }}
  {{ com Information given by type checking an expression }}
  | < S_N , effect >                                      :: :: I
    {{ lem (Inf [[S_N]] [[effect]]) }}
  | Ie                                                           :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }}
    {{ lem Iemp }}
  | I1 u+ .. u+ In                                               :: :: Iunion {{ com Unions the constraints and effect }}
    {{ lem (List.foldr inf_union Iemp [[I1..In]]) }}


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

   | effect1 = effect2                                        :: :: Ef_eqn
     {{ ichl ([[effect1]] = [[effect2]]) }}

   | t1 = t2                                                     :: :: t_eq
     {{ ichl ([[t1]] = [[t2]]) }}
   | ne1 = ne2							:: :: ne_eq
     {{ ichl ([[ne1]] = [[ne2]]) }}
   | 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(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 effect ok
 ------------------------------------------------------------ :: fn
 E_k |-t t1 -> t2 effect 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 effect ok :: :: check_ef :: check_ef_
{{ com Well-formed effects }}
{{ lemwcf  witness type check_ef_witness; check check_ef_w_check; }}
by

E_k('x) gives K_Efct
----------------------------------------------------------- :: var
E_k |-e 'x ok

E_k('x) gives K_infer
E_k('x) <-| K_Efct
------------------------------------------------------------ :: varInfer
E_k |-e 'x ok

------------------------------------------------------------- :: set
E_k |-e { base_effect1 , .. , base_effectn } ok

defn 
E_k |-n ne ok :: :: check_n :: check_n_
{{ com Well-formed numeric expressions }}
{{ lemwcf  witness type check_n_witness; check check_n_w_check; }}
by

E_k('x) gives K_Nat
----------------------------------------------------------- :: var
E_k |-n 'x ok

E_k('x) gives K_infer
E_k('x) <-| K_Nat
------------------------------------------------------------ :: varInfer
E_k |-n 'x ok

----------------------------------------------------------- :: num
E_k |-n num ok

E_k |-n ne1 ok
E_k |-n ne2 ok
----------------------------------------------------------- :: sum
E_k |-n ne1 + ne2 ok

E_k |-n ne1 ok
E_k |-n ne2 ok
------------------------------------------------------------ :: mult
E_k |-n ne1 * ne2 ok

E_k |-n ne ok
------------------------------------------------------------ :: exp
E_k |-n 2 ** ne ok

defn 
E_k |-o order ok :: :: check_ord :: check_ord_
{{ com Well-formed numeric expressions }}
{{ lemwcf  witness type check_ord_witness; check check_ord_w_check; }}
by

E_k('x) gives K_Ord
----------------------------------------------------------- :: var
E_k |-o 'x ok

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


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

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

E_k |-e effect ok
--------------------------------------------------------- :: eff
E_k , K_Efct |- effect ok

E_k |-n ne ok
--------------------------------------------------------- :: nat
E_k , K_Nat |- ne ok

E_k |-o order ok
--------------------------------------------------------- :: ord
E_k, K_Ord |- order ok


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

defn
E_d |- t1 = t2 :: :: teq :: teq_ 
{{ com Type equality }}
{{ lemwcf  witness type check_teq_witness; check check_teq_w_check; }}
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 effect tag S_N = t3 -> t4 effect tag S_N
 
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_
{{ lemwcf  witness type check_targeq_witness; check check_targeq_w_check; }}
by

E_d |- t = t'
------------------------------------------------------------ :: typ
E_d, K_Typ |- t = t'

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

E_k('x) gives k
----------------------------------------------------------- :: nokind
<E_k,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_k2 , 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_r,E_e> |- 'x ~> 'x

E_k(id) gives K_Typ
------------------------------------------------------------ :: id
<E_k,E_r,E_e> |- id ~> id

E_d |- typ1 ~> t1
E_d |- typ2 ~> t2
------------------------------------------------------------ :: fn
E_d |- typ1->typ2 effectkw effect ~> t1->t2 effect 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 }}
{{ lemwcf  witness type convert_targ_witness; check convert_targ_w_check; }}
by
 
E_d |- typ ~> t
------------------------------------- :: typ
E_d, K_Typ |- typ ~> t

defn 
|- nexp ~> ne :: :: convert_nexp :: convert_nexp_ 
{{ com Convert and normalize numeric expressions }}
{{ lemwcf  witness type convert_nexp_witness; check convert_nexp_w_check; }}
by
 
------------------------------------------------------------ :: var
|- 'x ~> 'x

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

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

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

|- nexp ~> ne
------------------------------------------------------------ :: exp
|- 2** nexp ~> 2 ** ne

defn 
E_d |- exp : t :> t' , exp' , S_N :: :: coerce_typ :: coerce_typ_
{{ lemwcf  witness type coerce_typ_witness; check coerce_typ_w_check; }}
by

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

E_d |- id1 : t1 :> u1, exp1, S_N1 .. E_d |- idn: tn :> un,expn, S_Nn
exp' = switch exp { case (id1, .., idn) -> (exp1,..,expn) }
-------------------------------------- :: tuple
E_d |- exp : (t1 * .. * tn) :> (u1 * .. * un), exp', S_N1 u+ .. u+ S_Nn

-------------------------------------- :: enum
E_d |- exp: enum ne1 ne2 order :> enum ne3 ne4 order, exp, {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> |- exp: enum num zero order :> t,id, {}

E_e(t) gives { num |-> id </num''i |-> id''i//i/> num' |-> id' }
exp' = switch exp { case id -> num </case id''i -> num''i//i/> case id' -> num' }
------------------------------------------------ :: from_enumerate
<E_k,E_r,E_e> |- exp: t :> enum num num' + (- num) inc, exp', {}

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

exp' = :E_app: to_vec(exp)
'x = fresh_kid(E_d)
-------------------------------------- :: from_num
E_d |- exp: enum ne1 ne2 order :> vector ne3 ne4 order :t_arg_typ: bit,exp', {ne3 = zero, 'x = ne1 + ne2, ne4 = 2** 'x}


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

 num = bitlength(bin)
 ------------------------------------------------------------ :: bin 
 |- bin  : vector zero num inc :T_id: 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 { } 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: 'x num+'x 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: 'x :t_arg_nexp: 'x2 inc t gives (E_t1 u+ ... u+ E_tn), {'x<=num1, 'x2 >= 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: 'x :t_arg_nexp: 'x2 dec t gives (E_t1 u+ ... u+ E_tn), {'x>=num1,'x2<=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: 'x :t_arg_nexp: 'x2 inc t gives (E_t1 u+ ... u+ E_tn),{'x<=ne1,'x2>= 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: 'x :t_arg_nexp: 'x2 inc t gives (E_t1 u+ ... u+ E_tn),{'x>=ne1,'x2>= 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,effect>,E_t1
E_d |- exp : u :> t,exp', S_N2
------------------------------------------------------------ :: coerce
<E_t,E_d> |- exp : t gives <S_N u+ S_N2,effect>,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 <{},{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 {} Ctor {} 
<E_t,E_d> |- exp : t' gives I,E_t
------------------------------------------------------------ :: ctor
<E_t,E_d> |- :E_app: 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 effect tag S_N
<E_t,E_d> |- exp : t' gives I,E_t
------------------------------------------------------------ :: app
<E_t,E_d> |- :E_app: id(exp) : t gives I u+ <S_N,effect>, E_t

E_t(id) gives t' -> t effect 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, effect>, 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: 'x :t_arg_nexp: 'x2 order t gives I1 u+ I2 u+ I3 u+ <{ne <= ne2, 'x >= ne2 , 'x <= ne2+ne2', ne2+ne'2<=ne3, ne+ne'>=ne3+ne'3, 'x2 <=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, effect, {}
<(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,effect> 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 <{},{ 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 {</base_effecti//i/>, wmem, </base_effect'j//j/>} Extern {}
<E_t,E_d> |- exp : t1 gives I,E_t1
---------------------------------------------------------- :: wmem
<E_t,E_d> |- :LEXP_memory: id(exp) : t gives I u+ <{},{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: 'x :Ne_var: 'x2 order t gives I1 u+ I2 u+ I3 u+ <{ne5<=ne1, ne1+ne2 <= ne3, ne3+ne4<= ne5+ne6, 'x <= ne1, 'x2 <= ne2+ne3+ne4},pure> ,E_t

E |- exp1 : enum ne1 ne2 order gives I1,E_t
E |- exp2 : enum ne3 ne4 order gives I2,E_t
E |- lexp : vector ne5 ne6 order t gives I3,E_t
---------------------------------------------------------- :: wslice_spread
E |- lexp [exp1 : exp2] : t gives I1 u+ I2 u+ I3 u+ <{ne5<=ne1, ne1+ne2 <= ne3, ne3+ne4<= ne5+ne6},pure> ,E_t

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

defn
E |- letbind gives E_t , S_N , effect , E_k :: :: check_letbind :: check_letbind_ 
{{ com Build the environment for a let binding, collecting index constraints }}
by

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

defns
check_defs :: '' ::=

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

%Does abbrev need a type environment? Ouch if yes
E_d |- typschm ~> t,E_k1,S_N 
----------------------------------------------------------- :: abbrev
E_d |- typedef id name_scm_opt = typschm gives <{},<{id |-> K_Abbrev t},{},{}>>

E_d |- typ1 ~> t1 .. E_d |- typn ~> tn
E_r = { {id1:t1, .., idn:tn} |-> id } 
----------------------------------------------------------- :: unquant_record
E_d |- typedef id name_scm_opt = const struct { typ1 id1 ; .. ; typn idn semi_opt } gives <{},<{id |-> K_Typ},E_r,{}>>

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

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

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

% Save these as enumerations for coercion
E_t = {id1 |-> id, ..., idn |-> id}
E_e = { id |-> { num1 |-> id1 ... numn |-> idn} }
------------------------------------------------------------- :: enumerate
E_d |- typedef id name_scm_opt = enumerate { id1 ; ... ; idn semi_opt } gives <E_t,<{id |-> K_Typ},{},E_e>>

defn
E |- fundef gives E_t , S_N :: :: check_fd :: check_fd_
{{ com Check a function definition }}
by

E_t(id) gives E_k',S_N',None, t1 -> t effect None S_N'
</E_d |- quant_itemi ~> E_ki,S_Ni//i/>
S_N'' = u+ </S_Ni//i/>
E_k' ~= </E_ki//i/>
E_d1 = <E_k',{},{}> u+ E_d
E_d1 |- typ ~> t
</<E_t,E_d1> |- patj : t1 gives E_tj,S_N'''j//j/>
</<(E_t u+ E_tj),E_d1> |- expj : t gives <S_N''''j,effect'j>,E_t'j//j/>
S_N''''' = u+ </S_N'''j u+ S_N''''j//j/>
effect = u+ </effect'j//j/>
S_N = resolve ( S_N' u+ S_N'' u+ S_N''''')
------------------------------------------------------------- :: rec_function
<E_t,E_d> |- function rec forall </quant_itemi//i/> . typ effectkw effect </id patj = expj//j/> gives E_t, S_N

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

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

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

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

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

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

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


defn
E |- val_spec gives E_t :: :: check_spec :: check_spec_
{{ com Check a value specification }}
by

E_d |- typschm ~> t, E_k1, S_N
-------------------------------------------------------- :: val_spec
<E_t,E_d> |- val typschm id gives {id |-> E_k1,S_N,None,t }

E_d |- typschm ~> t, E_k1, S_N
-------------------------------------------------------- :: extern
<E_t,E_d> |- val extern typschm id = string gives {id |-> E_k1,S_N,Extern,t}

defn
E_d |- default_spec gives E_t , E_k1 :: :: check_default :: check_default_
{{ com Check a default typing specification }}
by

E_k |- base_kind ~> k
------------------------------------------------------------ :: kind
<E_k,E_r,E_e> |- default base_kind 'x gives {}, {'x |-> k default }

E_d |- typschm ~> t,E_k1,S_N 
------------------------------------------------------------ :: typ
E_d |- default typschm id gives {id |-> E_k1,S_N,Default,t},{}

defn
 
E |- def gives E' :: :: check_def :: check_def_ 
{{ com Check a definition }}
by

E_d |- type_def gives E
--------------------------------------------------------- :: tdef
<E_t,E_d>|- type_def gives <E_t,E_d> u+ E

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

E |- letbind gives {id1 |-> t1 , .. , idn |-> tn},S_N,pure,E_k 
S_N1 = resolve(S_N)
--------------------------------------------------------- :: vdef
E |- letbind gives E u+ <{id1 |-> E_k,S_N,None,t1 , .. , idn |-> E_k,S_N,None,tn},empty>

E |- val_spec gives E_t
--------------------------------------------------------- :: vspec
E |- val_spec gives E u+ <E_t,empty>

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

E_d |- typ ~> t
---------------------------------------------------------- :: register
<E_t,E_d> |- register typ id gives <(E_t u+ {id |-> register t}),E_d>

defn
E |- defs gives E' :: :: check_defs :: check_defs_ 
{{ com Check definitions, potentially given default environment of built-in library }}
by

------------------------------------------------------------ :: empty
E |- gives E

:check_def: E |- def gives E1
E u+ E1 |- </defi// i/> gives E2
------------------------------------------------------------ :: defs 
E |- def </defi// i/> gives E2