grammar

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 |-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_k |- t1 = t2 :: :: teq :: teq_ 
{{ com Type equality }}
by
%% % 
%% % TD |- t ok
%% % ------------------------------------------------------------ :: refl
%% % TD |- t = t
%% % 
%% % TD |- t2 = t1
%% % ------------------------------------------------------------ :: sym
%% % TD |- t1 = t2
%% % 
%% % TD |- t1 = t2
%% % TD |- t2 = t3
%% % ------------------------------------------------------------ :: trans
%% % TD |- t1 = t3
%% % 
%% % TD |- t1 = t3
%% % TD |- t2 = t4
%% % ------------------------------------------------------------ :: arrow
%% % TD |- t1 -> t2 = t3 -> t4
%% % 
%% % TD |- t1 = u1 .... TD |- tn = un
%% % ------------------------------------------------------------ :: tup
%% % TD |- t1*....*tn = u1*....*un
%% % 
%% % TD(p) gives a1..an
%% % TD |- t1 = u1 .. TD |- tn = un
%% % ------------------------------------------------------------ :: app
%% % TD |- p  t1 .. tn = p u1 .. un
%% % 
%% % TD(p) gives a1..an . u 
%% % ------------------------------------------------------------ :: expand
%% % TD |- p t1 .. tn = {a1|->t1..an|->tn}(u)
%% % 
%% % ne = normalize (ne')
%% % ----------------------------------------------------------  :: nexp
%% % TD |- ne = ne' 
%% % 
%% % 

defns
convert_typ :: '' ::=
 
defn
E_k |- typ ~> t :: :: convert_typ :: convert_typ_ 
{{ com Convert source types to internal types }}
by
 
E_k(id) gives K_Typ
------------------------------------------------------------ :: var
E_k |- :Typ_var: id ~> id

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

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

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

defn
E_k , 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
%% % |- N l ~> N
%% % 
%% % ------------------------------------------------------------ :: num
%% % |- num l ~> nat
%% % 
%% % |- nexp1 ~> ne1
%% % |- nexp2 ~> ne2
%% % ------------------------------------------------------------ :: mult
%% % |- nexp1 * nexp2 l ~> ne1 * ne2
%% % 
%% % |- nexp1 ~> ne1
%% % |- nexp2 ~> ne2
%% % ----------------------------------------------------------- :: add
%% % |- nexp1 + nexp2 l ~> :Ne_add: ne1 + ne2
%% % 
%% % defns
%% % convert_typs :: '' ::=
%% % 
%% % defn
%% % TD , E |- typs ~> t_multi :: :: convert_typs :: convert_typs_ by
%% % 
%% % TD,E |- typ1 ~> t1 .. TD,E |- typn ~> tn
%% % ------------------------------------------------------------ :: all
%% % TD,E |- typ1 * .. * typn ~> (t1 * .. * tn)
%% % 
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 num 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
%% % inst_field :: '' ::=
%% % 
%% % defn
%% % TD , E |- field id : p t_args -> t gives ( x of names ) :: :: inst_field :: inst_field_
%% % {{ com Field typing (also returns canonical field names) }} 
%% % by
%% % 
%% % E(</x_li//i/>) gives <E_m,E_p,E_f,E_x>
%% % E_f(y) gives <forall tnv1..tnvn. p -> t, (z of names)>
%% % TD |- t1 ok .. TD |- tn ok
%% % ------------------------------------------------------------ :: all
%% % TD,E |- field </x_li.//i/> y l1 l2: p t1 .. tn -> {tnv1|->t1..tnvn|->tn}(t) gives (z of names)
%% % 
%% % defns
%% % inst_ctor :: '' ::=
%% % 
%% % defn
%% % TD , E |- ctor id : t_multi -> p t_args gives ( x of names ) :: :: inst_ctor :: inst_ctor_ 
%% % {{ com Data constructor typing (also returns canonical constructor names) }} 
%% % by
%% % 
%% % E(</x_li//i/>) gives <E_m,E_p,E_f,E_x>
%% % E_x(y) gives <forall tnv1..tnvn. t_multi -> p, (z of names)>
%% % TD |- t1 ok .. TD |- tn ok
%% % ------------------------------------------------------------ :: all
%% % TD,E |- ctor </x_li.//i/> y l1 l2 : {tnv1|->t1..tnvn|->tn}(t_multi) -> p t1 .. tn gives (z of names)
%% % 
%% % defns
%% % inst_val :: '' ::=
%% % 
%% % defn
%% % TD , E |- val id : t gives S_c :: :: inst_val :: inst_val_
%% % {{ com Typing top-level bindings, collecting typeclass constraints }}
%% % by
%% % 
%% % E(</x_li//i/>) gives <E_m,E_p,E_f,E_x>
%% % E_x(y) gives <forall tnv1..tnvn. (p1 tnv'1) .. (pi tnv'i) => t,env_tag>
%% % TD |- t1 ok .. TD |- tn ok
%% % t_subst = {tnv1|->t1..tnvn|->tn}
%% % ------------------------------------------------------------ :: all
%% % TD, E |- val </x_li.//i/> y l1 l2 : t_subst(t) gives {(p1 t_subst(tnv'1)), .. , (pi t_subst(tnv'i))}
%% % 
%% % defns
%% % not_ctor :: '' ::=
%% % 
%% % defn
%% % E , E_l |- x not ctor :: :: not_ctor :: not_ctor_ 
%% % {{ com $\ottnt{v}$ is not bound to a data constructor }}
%% % by
%% % 
%% % E_l(x) gives t
%% % ------------------------------------------------------------ :: val
%% % E,E_l |- x not ctor
%% % 
%% % x NOTIN dom(E_x)
%% % ------------------------------------------------------------ :: unbound
%% % <E_m,E_p,E_f,E_x>,E_l |- x not ctor
%% % 
%% % E_x(x) gives <forall tnv1..tnvn. (p1 tnv'1)..(pi tnv'i) => t,env_tag>
%% % ------------------------------------------------------------ :: bound
%% % <E_m,E_p,E_f,E_x>,E_l |- x not ctor
%% % 
%% % defns
%% % not_shadowed :: '' ::=
%% % 
%% % defn
%% % E_l |- id not shadowed :: :: not_shadowed :: not_shadowed_ 
%% % {{ com $\ottnt{id}$ is not lexically shadowed }}
%% % by
%% % 
%% % x NOTIN dom(E_l)
%% % ------------------------------------------------------------ :: sing
%% % E_l |- x l1 l2 not shadowed
%% % 
%% % ------------------------------------------------------------ :: multi
%% % E_l |- x_l1. .. x_ln.y_l.z_l l not shadowed
%% % 
%% % 
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_r,E_k> |- _ : t gives {}, {}
% This case should perhaps indicate the generation of a type variable, with kind Typ

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

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

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

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

E_r(</idi//i/>) gives id t_args, (</ti//i/>)
</<E_t,E_r,E_k> |- pati : ti gives E_ti,S_Ni//i/>
disjoint doms(</E_ti//i/>)
------------------------------------------------------------ :: record
<E_t,E_r,E_k> |- { </idi = pati//i/> semi_opt } : id t_args gives 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_t,E_r,E_k> |- pat1 : t1 gives E_t1,S_N1 .... <E_t,E_r,E_k> |- patn : tn gives E_tn,S_Nn
disjoint doms(E_t1,....,E_tn)
------------------------------------------------------------ :: tup
<E_t,E_r,E_k> |- (pat1, ...., patn) : (t1 * .... * tn) gives E_t1 u+ .... u+ E_tn,S_N1 u+ .... u+ S_Nn 

E_k |-t t ok
<E_t,E_r,E_k> |- pat1 : t gives E_t1,S_N1 .. <E_t,E_r,E_k> |- patn : t gives E_tn,S_Nn
disjoint doms(E_t1,..,E_tn)
------------------------------------------------------------ :: list
<E_t,E_r,E_k> |- [|pat1, .., patn |] : list t gives E_t1 u+ .. u+ E_tn,S_N1 u+ .. u+ S_Nn

 
%% % 
%% % 
%% % defns
%% % id_field :: '' ::=
%% % 
%% % defn
%% % E |- id field :: :: id_field :: id_field_
%% % {{ com Check that the identifier is a permissible field identifier }}
%% % by
%% % 
%% % E_f(x) gives f_desc
%% % ------------------------------------------------------------ :: empty
%% % <E_m,E_p,E_f,E_x> |- x l1 l2 field
%% % 
%% % 
%% % E_m(x) gives E
%% % x NOTIN dom(E_f)
%% % E |- </y_li.//i/> z_l l2 field
%% % ------------------------------------------------------------ :: cons
%% % <E_m,E_p,E_f,E_x> |- x l1.</y_li.//i/> z_l l2 field
%% % 
%% % defns
%% % id_value :: '' ::=
%% % 
%% % defn
%% % E |- id value :: :: id_value :: id_value_
%% % {{ com Check that the identifier is a permissible value identifier }}
%% % by
%% % 
%% % E_x(x) gives v_desc
%% % ------------------------------------------------------------ :: empty
%% % <E_m,E_p,E_f,E_x> |- x l1 l2 value
%% % 
%% % 
%% % E_m(x) gives E
%% % x NOTIN dom(E_x)
%% % E |- </y_li.//i/> z_l l2 value
%% % ------------------------------------------------------------ :: cons
%% % <E_m,E_p,E_f,E_x> |- x l1.</y_li.//i/> z_l l2 value
%% % 

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

%% TODO::: if t is a reg, need to distinguish here between reg and ref cell access, and add to effect if reg, and maybe add to tag
 
E_t(id) gives t
------------------------------------------------------------ :: var
<E_t,E_r,E_k> |- id : t gives Ie

E_t(id) gives t' -> t effect {} Ctor {} 
<E_t,E_r,E_k> |- exp : t' gives I
------------------------------------------------------------ :: ctor
<E_t,E_r,E_k> |- id exp : t gives Ir

 
E_t(id) gives t' -> t effects tag S_N
<E_t,E_r,E_k> |- exp : t' gives <S_N1,effects',_>
------------------------------------------------------------ :: app
<E_t,E_r,E_k> |- id exp : t gives <S_N u+ S_N1,effects u+ effects',tag>
 
E_t(id) gives (t1 * t2) -> t effects tag S_N
<E_t,E_r,E_k> |- exp1 : t1 gives <S_N2,effects2,_>
<E_t,E_r,E_k> |- exp2 : t2 gives <S_N3,effects3,_>
------------------------------------------------------------ :: infix_app
<E_t,E_r,E_k> |- :E_app_infix: exp1 id exp2 : t gives <S_N u+ S_N2 u+ S_N3, effects u+ effects2 u+ effects3,tag>

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

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

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

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

E |- exp1 : vector ne ne' order t gives I1
E |- exp2 : enum ne2 ne'2 order gives I2
E |- exp3 : enum ne3 ne'3 order gives I3
------------------------------------------------------------- :: 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,None>

E |- exp : vector ne1 ne2 order t gives I
E |- exp1 : enum ne3 ne4 order gives I1
E |- exp2 : t gives I2
------------------------------------------------------------ :: 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,None>

E |- exp : vector ne1 ne2 order t gives I
E |- exp1 : enum ne3 ne4 order gives I1
E |- exp2 : enum ne5 ne6 order gives I2
E |- exp3 : vector ne7 ne8 order t gives I3
------------------------------------------------------------ :: 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,None>

E |- exp : vector ne1 ne2 order t gives I
E |- exp1 : enum ne3 ne4 order gives I1
E |- exp2 : enum ne5 ne6 order gives I2
E |- exp3 : t gives I3
------------------------------------------------------------ :: 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,None>


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

%% % </TD,E,E_l |- pati : t gives E_li//i/>
%% % </TD,E,E_l u+ E_li |- expi : u gives S_ci,S_Ni//i/>
%% % TD,E,E_l |- exp : t gives S_c',S_N'
%% % ------------------------------------------------------------ :: case
%% % TD,E,E_l |- match exp with bar_opt </pati -> expi li//i/> l end : u gives S_c' union </S_ci//i/>,S_N' union </S_Ni//i/>

<E_t,E_r,E_k> |- exp : t gives I
E_k |- typ ~> t
------------------------------------------------------------ :: typed
<E_t,E_r,E_k> |- (typ) exp : t gives Ir

%% % %KATHYCOMMENT: where does E_l1 come from?
%% % TD,E,E_l1 |- letbind gives E_l2, S_c1,S_N1
%% % TD,E,E_l1 u+ E_l2 |- exp : t gives S_c2,S_N2
%% % ------------------------------------------------------------ :: let
%% % TD,E,E_l |- let letbind in exp : t gives S_c1 union S_c2,S_N1 union S_N2
 
E |- exp1 : t1 gives I1 .... E |- expn : tn gives In
------------------------------------------------------------ :: tup
E |- (exp1, .... , expn) : (t1 * .... * tn) gives I1 u+ .... u+ In
 
E |- exp1 : t gives I1 .. E |- expn : t gives In
------------------------------------------------------------ :: list
E |- [|exp1, .., expn |] : list t gives I1 u+ .. u+ In

E |- exp1 : bool gives I1
E |- exp2 : t gives I2
E |- exp3 : t gives I3
------------------------------------------------------------ :: if
E |- if exp1 then exp2 else exp3 : t gives I1 u+ I2 u+ I3

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

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

|- lit : t
------------------------------------------------------------ :: lit
E |- lit : t gives Ie


%% % defn
%% % TD , E , E_l |- funcl gives { x |-> t } , S_c , S_N :: :: check_funcl :: check_funcl_
%% % {{ com Build the environment for a function definition clause, collecting typeclass and index constraints }}
%% % by
%% % 
%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln
%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N
%% % disjoint doms(E_l1,...,E_ln)
%% % TD,E |- typ ~> u
%% % ------------------------------------------------------------ :: annot
%% % TD,E,E_l |- x l1 pat1 ... patn : typ = exp l2 gives {x |-> curry((t1 * ... * tn), u)}, S_c,S_N
%% % 
%% % TD,E,E_l |- pat1 : t1 gives E_l1 ... TD,E,E_l |- patn : tn gives E_ln
%% % TD,E,E_l u+ E_l1 u+ ... u+ E_ln |- exp : u gives S_c,S_N
%% % disjoint doms(E_l1,...,E_ln)
%% % ------------------------------------------------------------ :: noannot
%% % TD,E,E_l |- x l1 pat1 ... patn = exp l2 gives {x |-> curry((t1 * ... * tn), u)}, S_c,S_N
%% % 
%% % 
%% % defn
%% % TD , E , E_l1 |- letbind gives E_l2 , S_c , S_N :: :: check_letbind :: check_letbind_ 
%% % {{ com Build the environment for a let binding, collecting typeclass and index constraints }}
%% % by
%% % 
%% % %TODO similar type equality issues to above ones
%% % TD,E,E_l1 |- pat : t gives E_l2
%% % TD,E,E_l1 |- exp : t gives S_c,S_N
%% % TD,E |- typ ~> t
%% % ------------------------------------------------------------ :: val_annot
%% % TD,E,E_l1 |- pat : typ = exp l gives E_l2,S_c,S_N
%% % 
%% % TD,E,E_l1 |- pat : t gives E_l2
%% % TD,E,E_l1 |- exp : t gives S_c,S_N
%% % ------------------------------------------------------------ :: val_noannot
%% % TD,E,E_l1 |- pat = exp l gives E_l2,S_c,S_N
%% % 
%% % :check_funcl:TD,E,E_l1 |- funcl_aux l gives {x|->t},S_c,S_N
%% % ------------------------------------------------------------ :: fn
%% % TD,E,E_l1 |- funcl_aux l gives {x|->t},S_c,S_N
%% % 
%% % defns
%% % check_rule :: '' ::=
%% % 
%% % defn
%% % TD , E , E_l |- rule gives { x |-> t } , S_c , S_N :: :: check_rule :: check_rule_
%% % {{ com Build the environment for an inductive relation clause, collecting typeclass and index constraints }}
%% % by
%% % 
%% % </TD |- ti ok//i/>
%% % E_l2 = {</yi|->ti//i/>} 
%% % TD,E,E_l1 u+ E_l2 |- exp' : __bool gives S_c',S_N'
%% % TD,E,E_l1 u+ E_l2 |- exp1 : u1 gives S_c1,S_N1 .. TD,E,E_l1 u+ E_l2 |- expn : un gives S_cn,S_Nn
%% % ------------------------------------------------------------ :: rule
%% % TD,E,E_l1 |- x_l_opt forall </yi li//i/> . exp' ==> x l exp1 .. expn l' gives {x|->curry((u1 * .. * un) , __bool)}, S_c' union S_c1 union .. union S_cn,S_N' union S_N1 union .. union S_Nn
%% % 
%% % defns
%% % check_texp_tc :: '' ::=
%% % 
%% % defn
%% % xs , TD1 , E |- tc td gives TD2 , E_p :: :: check_texp_tc :: check_texp_tc_
%% % {{ com Extract the type constructor information }}
%% % by
%% % 
%% % tnvars ~> tnvs
%% % TD,E |- typ ~> t
%% % duplicates(tnvs) = emptyset
%% % FV(t) SUBSET tnvs
%% % </yi.//i/>x NOTIN dom(TD)
%% % ------------------------------------------------------------ :: abbrev
%% % </yi//i/>,TD,E |- tc x l tnvars = typ gives {</yi.//i/>x|->tnvs.t},{x|-></yi.//i/>x}
%% % 
%% % tnvars ~> tnvs
%% % duplicates(tnvs) = emptyset
%% % </yi.//i/>x NOTIN dom(TD)
%% % ------------------------------------------------------------ :: abstract
%% % </yi//i/>,TD,E1 |- tc x l tnvars gives {</yi.//i/>x|->tnvs},{x|-></yi.//i/>x}
%% % 
%% % tnvars ~> tnvs
%% % duplicates(tnvs) = emptyset
%% % </yi.//i/>x NOTIN dom(TD)
%% % ------------------------------------------------------------ :: rec
%% % </yi//i/>,TD1,E |- tc x l tnvars = <| x_l1 : typ1 ; ... ; x_lj : typj semi_opt |> gives {</yi.//i/>x|->tnvs},{x|-></yi.//i/>x}
%% % 
%% % tnvars ~> tnvs
%% % duplicates(tnvs) = emptyset
%% % </yi.//i/>x NOTIN dom(TD)
%% % ------------------------------------------------------------ :: var
%% % </yi//i/>,TD1,E |- tc x l tnvars = bar_opt ctor_def1 | ... | ctor_defj gives {</yi.//i/>x|->tnvs},{x|-></yi.//i/>x}
%% % 
%% % defns
%% % check_texps_tc :: '' ::=
%% % 
%% % defn
%% % xs , TD1 , E |- tc td1 .. tdi gives TD2 , E_p :: :: check_texps_tc :: check_texps_tc_
%% % {{ com Extract the type constructor information }}
%% % by
%% % 
%% % ------------------------------------------------------------ :: empty
%% % xs,TD,E |- tc gives {},{}
%% % 
%% % :check_texp_tc: xs,TD1,E |- tc td gives TD2,E_p2
%% % xs,TD1 u+ TD2,E u+ <{},E_p2,{},{}> |- tc </tdi//i/> gives TD3,E_p3
%% % dom(E_p2) inter dom(E_p3) = emptyset
%% % ------------------------------------------------------------ :: abbrev
%% % xs,TD1,E |- tc td </tdi//i/> gives TD2 u+ TD3,E_p2 u+ E_p3
%% % 
%% % defns
%% % check_texp :: '' ::=
%% % 
%% % defn
%% % TD , E |- tnvs p = texp gives < E_f , E_x > :: :: check_texp :: check_texp_ 
%% % {{ com Check a type definition, with its path already resolved }}
%% % by
%% % 
%% % ------------------------------------------------------------ :: abbrev
%% % TD,E |- tnvs p = typ gives <{},{}>
%% % 
%% % </TD,E |- typi ~> ti//i/>
%% % names = {</xi//i/>}
%% % duplicates(</xi//i/>) = emptyset
%% % </FV(ti) SUBSET tnvs//i/>
%% % E_f = {</xi|-> <forall tnvs. p -> ti, (xi of names)>//i/>}
%% % ------------------------------------------------------------ :: rec
%% % TD,E |- tnvs p = <| </x_li:typi//i/> semi_opt |> gives <E_f,{}>
%% % 
%% % </TD,E |- typsi ~> t_multii//i/>
%% % names = {</xi//i/>}
%% % duplicates(</xi//i/>) = emptyset
%% % </FV(t_multii) SUBSET tnvs//i/>
%% % E_x = {</xi|-><forall tnvs. t_multii -> p, (xi of names)>//i/>}
%% % ------------------------------------------------------------ :: var
%% % TD,E |- tnvs p = bar_opt </x_li of typsi//i/> gives <{},E_x>
%% % 
%% % defns
%% % check_texps :: '' ::=
%% % 
%% % defn
%% % xs , TD , E |- td1 .. tdn gives < E_f , E_x > :: :: check_texps :: check_texps_ by
%% % 
%% % ------------------------------------------------------------ :: empty
%% % </yi//i/>,TD,E |- gives <{},{}>
%% % 
%% % tnvars ~> tnvs
%% % TD,E1 |- tnvs </yi.//i/>x = texp gives <E_f1,E_x1>
%% % </yi//i/>,TD,E |- </tdj//j/> gives <E_f2,E_x2>
%% % dom(E_x1) inter dom(E_x2) = emptyset
%% % dom(E_f1) inter dom(E_f2) = emptyset
%% % ------------------------------------------------------------ :: cons_concrete
%% % </yi//i/>,TD,E |- x l tnvars = texp </tdj//j/> gives <E_f1 u+ E_f2, E_x1 u+ E_x2>
%% % 
%% % </yi//i/>,TD,E |- </tdj//j/> gives <E_f,E_x>
%% % ------------------------------------------------------------ :: cons_abstract
%% % </yi//i/>,TD,E |- x l tnvars </tdj//j/> gives <E_f,E_x>
%% % 
%% % defns
%% % convert_class :: '' ::=
%% % 
%% % defn
%% % TC , E |- id ~> p :: :: convert_class :: convert_class_
%% % {{ com Lookup a type class }}
%% % by
%% % 
%% % E(id) gives p
%% % TC(p) gives xs
%% % ------------------------------------------------------------ :: all
%% % TC,E |- id ~> p
%% % 
%% % defns
%% % solve_class_constraint :: '' ::=
%% % 
%% % defn
%% % I |- ( p t ) 'IN' semC :: :: solve_class_constraint :: solve_class_constraint_
%% % {{ com Solve class constraint }}
%% % by
%% % 
%% % ------------------------------------------------------------ :: immediate
%% % I |- (p a) IN (p1 tnv1) .. (pi tnvi) (p a) (p'1 tnv'1) .. (p'j tnv'j)
%% % 
%% % (p1 tnv1)..(pn tnvn)=>(p t) IN I 
%% % I |- (p1 t_subst(tnv1)) IN semC .. I |- (pn t_subst(tnvn)) IN semC
%% % ------------------------------------------------------------ :: chain
%% % I |- (p t_subst(t)) IN semC
%% % 
%% % defns
%% % solve_class_constraints :: '' ::=
%% % 
%% % defn
%% % I |- S_c gives semC :: :: solve_class_constraints :: solve_class_constraints_
%% % {{ com Solve class constraints }}
%% % by
%% % 
%% % I |- (p1 t1) IN semC ..  I |- (pn tn) IN semC
%% % ------------------------------------------------------------ :: all
%% % I |- {(p1 t1), .., (pn tn)} gives semC
%% % 
%% % defns
%% % check_val_def :: '' ::=
%% % 
%% % defn
%% % TD , I , E |- val_def gives E_x :: :: check_val_def :: check_val_def_
%% % {{ com Check a value definition }}
%% % by
%% % 
%% % TD,E,{} |- letbind gives {</xi|->ti//i/>},S_c,S_N
%% % %TODO, check S_N constraints
%% % I |- S_c gives semC
%% % </FV(ti) SUBSET tnvs//i/>
%% % FV(semC) SUBSET tnvs
%% % ------------------------------------------------------------ :: val
%% % TD,I,E1 |- let targets_opt letbind gives {</xi |-> <forall tnvs. semC => ti, let>//i/>}
%% % 
%% % </TD,E,E_l |- funcli gives {xi|->ti},S_ci,S_Ni//i/>
%% % I |- S_c gives semC
%% % </FV(ti) SUBSET tnvs//i/>
%% % FV(semC) SUBSET tnvs
%% % compatible overlap(</xi|->ti//i/>)
%% % E_l = {</xi|->ti//i/>}
%% % ------------------------------------------------------------ :: recfun
%% % TD,I,E |- let rec targets_opt </funcli//i/> gives {</xi|-><forall tnvs. semC => ti,let>//i/>}
%% % 
%% % defns
%% % check_t_instance :: '' ::=
%% % 
%% % defn
%% % 
%% % TD , ( a1 , .. , an ) |- t instance :: :: check_t_instance :: check_t_instance_
%% % {{ com Check that $\ottnt{t}$ be a typeclass instance }}
%% % by
%% % 
%% % ------------------------------------------------------------ :: var
%% % TD , (a) |- a instance
%% % 
%% % ------------------------------------------------------------ :: tup 
%% % TD , (a1, ...., an) |- a1 * .... * an instance
%% % 
%% % ------------------------------------------------------------ :: fn
%% % TD , (a1, a2) |- a1 -> an instance
%% % 
%% % TD(p) gives a'1..a'n
%% % ------------------------------------------------------------ :: tc
%% % TD , (a1, .., an) |- p a1 .. an instance
%% % 
%% % defns
%% % check_defs :: '' ::=
%% % 
%% % defn
%% % 
%% % </ zj // j /> , D1 , E1 |- def gives D2 , E2 :: :: check_def :: check_def_ 
%% % {{ com Check a definition }}
%% % by
%% % 
%% % 
%% % </zj//j/>,TD1,E |- tc </tdi//i/> gives TD2,E_p
%% % </zj//j/>,TD1 u+ TD2,E u+ <{},E_p,{},{}> |- </tdi//i/> gives <E_f,E_x>
%% % ------------------------------------------------------------ :: type 
%% % </zj//j/>,<TD1,TC,I>,E |- type </tdi//i/> l gives <TD2,{},{}>,<{},E_p,E_f,E_x>
%% % 
%% % TD,I,E |- val_def gives E_x
%% % ------------------------------------------------------------ :: val_def
%% % </zj//j/>,<TD,TC,I>,E |- val_def l gives empty,<{},{},{},E_x>
%% % 
%% % </TD,E1,E_l |- rulei gives {xi|->ti},S_ci,S_Ni//i/>
%% % %TODO Check S_N constraints
%% % I |- </S_ci//i/> gives semC
%% % </FV(ti) SUBSET tnvs//i/>
%% % FV(semC) SUBSET tnvs
%% % compatible overlap(</xi|->ti//i/>)
%% % E_l = {</xi|->ti//i/>}
%% % E2 = <{},{},{},{</xi |-><forall tnvs. semC => ti,let>//i/>}>
%% % ------------------------------------------------------------ :: indreln
%% % </zj//j/>,<TD,TC,I>,E1 |- indreln targets_opt </rulei//i/> l gives empty,E2
%% % 
%% % </zj//j/> x,D1,E1 |- defs gives D2,E2
%% % ------------------------------------------------------------ :: module
%% % </zj//j/>,D1,E1 |- module x l1 = struct defs end l2 gives D2,<{x|->E2},{},{},{}>
%% % 
%% % E1(id) gives E2
%% % ------------------------------------------------------------ :: module_rename
%% % </zj//j/>,D,E1 |- module x l1 = id l2 gives empty,<{x|->E2},{},{},{}>
%% % 
%% % TD,E |- typ ~> t
%% % FV(t) SUBSET </ai//i/>
%% % FV(</a'k//k/>) SUBSET </ai//i/>
%% % </TC,E |- idk ~> pk//k/>
%% % E' = <{},{},{},{x|-><forall </ai//i/>. </(pk a'k)//k/> => t,val>}>
%% % ------------------------------------------------------------ :: spec
%% % </zj//j/>,<TD,TC,I>,E |- val x l1 : forall </ai l''i//i/>. </idk a'k l'k//k/> => typ l2 gives empty,E'
%% % 
%% % </TD,E1 |- typi ~> ti//i/>
%% % </FV(ti) SUBSET a//i/>
%% % :formula_p_eq: p = </zj.//j/>x
%% % E2 = <{},{x|->p},{},{</yi |-><forall a. (p a) => ti,method>//i/>}>
%% % TC2 = {p|-></yi//i/>}
%% % p NOTIN dom(TC1)
%% % ------------------------------------------------------------ :: class
%% % </zj//j/>,<TD,TC1,I>,E1 |- class (x l a l'') </val yi li : typi li//i/> end l' gives <{},TC2,{}>,E2
%% % 
%% % E = <E_m,E_p,E_f,E_x>
%% % TD,E |- typ' ~> t'
%% % TD,(</ai//i/>) |- t' instance
%% % tnvs = </ai//i/>
%% % duplicates(tnvs) = emptyset
%% % </TC,E |- idk ~> pk//k/>
%% % FV(</a'k//k/>) SUBSET tnvs
%% % E(id) gives p
%% % TC(p) gives </zj//j/>
%% % I2 = { </=> (pk a'k)//k/> }
%% % </TD,I union I2,E |- val_defn gives E_xn//n/>
%% % disjoint doms(</E_xn//n/>)
%% % </E_x(xk) gives <forall a''. (p a'') => tk,method>//k/>
%% % {</xk |-> <forall tnvs. => {a''|->t'}(tk),let>//k/>} = </E_xn//n/>
%% % :formula_xs_eq:</xk//k/> = </zj//j/>
%% % I3 = {</(pk a'k) => (p t')//k/>}
%% % (p {</ai |-> a'''i//i/>}(t')) NOTIN I
%% % ------------------------------------------------------------ :: instance_tc
%% % </zj//j/>,<TD,TC,I>,E |- instance forall </ai l'i//i/>. </idk a'k l''k//k/> => (id typ') </val_defn ln//n/> end l' gives <{},{},I3>,empty
%% % 
%% % defn
%% % </ zj // j /> , D1 , E1 |- defs gives D2 , E2 :: :: check_defs :: check_defs_ 
%% % {{ com Check definitions, given module path, definitions and environment }}
%% % by
%% % 
%% % % TODO: Check compatibility for duplicate definitions
%% % 
%% % ------------------------------------------------------------ :: empty
%% % </zj//j/>,D,E |- gives empty,empty
%% % 
%% % :check_def: </zj//j/>,D1,E1 |- def gives D2,E2
%% % </zj//j/>,D1 u+ D2,E1 u+ E2 |- </defi semisemi_opti // i/> gives D3,E3
%% % ------------------------------------------------------------ :: relevant_def 
%% % </zj//j/>,D1,E1 |- def semisemi_opt </defi semisemi_opti // i/> gives D2 u+ D3, E2 u+ E3
%% % 
%% % E1(id) gives E2
%% % </zj//j/>,D1,E1 u+ E2 |- </defi semisemi_opti // i/> gives D3,E3
%% % ------------------------------------------------------------ :: open
%% % </zj//j/>,D1,E1 |- open id l semisemi_opt </defi semisemi_opti // i/> gives D3,E3
%% %