Fixes bugs in pretty printer to generate legal lem syntax; split ott grammar and rules for lem ast generation; created a new directory for the lem interpreter and moved the Lem ast to it.

3 files changed, 1054 insertions, 1055 deletions

diff --git a/language/Makefile b/language/Makefile
index 4ac35b65..4747dc49 100644
--- a/language/Makefile
+++ b/language/Makefile
@@ -11,9 +11,9 @@ l2_parse.pdf: l2_parse.tex
 l2Theory.uo: l2Script.sml
 	Holmake --qof -I $(OTTLIB) l2Theory.uo
 
-l2.tex ../src/ast.ml ../src/ast.lem l2Script.sml: l2.ott 
-	ott -sort false -generate_aux_rules false -o l2.tex  -picky_multiple_parses true l2.ott
-	ott -sort false -generate_aux_rules false -o ../src/ast.lem -o l2Script.sml -picky_multiple_parses true l2.ott
+l2.tex ../src/ast.ml ../src/ast.lem l2Script.sml: l2.ott l2_rules.ott
+	ott -sort false -generate_aux_rules false -o l2.tex  -picky_multiple_parses true l2.ott l2_rules.ott
+	ott -sort false -generate_aux_rules false -o ../src/lem_interp/ast.lem -o l2Script.sml -picky_multiple_parses true l2.ott
 	ott -sort false -generate_aux_rules true -o ../src/ast.ml -picky_multiple_parses true l2.ott
 # the above is working around what is probably a bug in -generate_aux_rules true: when we try to generate Lem code with that turned on, we get some surprising-looking parse failures in a few rules.  Likely we're not doing the proper transform for rules generated from inductive relation syntax. 
 
diff --git a/language/l2.ott b/language/l2.ott
index ccc910c2..fdd1dadf 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -1396,1055 +1396,3 @@ formula :: formula_ ::=
 %freevars
 %t a :: ftv
 
-defns 
-translate_ast :: '' ::=
-
-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 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
-%% % TD |- 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
- 
-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 : nat
- 
- ------------------------------------------------------------- :: 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 :: :: check_pat :: check_pat_ 
-{{ com Typing patterns, building their binding environment }}
-by
-
-E_k |-t t ok
------------------------------------------------------------- :: wild
-<E_t,E_k> |- _ annot : t gives {} 
-% This case should perhaps indicate the generation of a type variable, with kind Typ
-
-<E_t,E_k> |- pat : t gives E_t1
-id NOTIN dom(E_t1)
------------------------------------------------------------- :: as
-<E_t,E_k> |- (pat as id) : t gives E_t1 u+ {id|->t}
-
-E_k |- typ ~> t
-<E_t,E_k> |- pat : t gives E_t1
------------------------------------------------------------- :: typ
-<E_t,E_k> |- (<typ> pat) : t gives E_t1
-
-%% % TD,E |- ctor id : (t1*..*tn) -> p t_args gives (x of names)
-<E_t,E_k> |- pat1 : t1 gives E_t1 .. <E_t,E_k> |- patn : tn gives E_tn
-%% % disjoint doms(E_l1,..,E_ln)
------------------------------------------------------------- :: ident_constr
-<E_t,E_k> |- id pat1 .. patn : id t_args gives E_t1 u+ .. u+ E_tn
-
-E_k |-t t ok
- ------------------------------------------------------------ :: var
-<E_t,E_k> |- :P_id: id : t gives E_t u+ {id|->t}
-
-%% % 
-%% % </TD,E |- field idi : p t_args -> ti gives (xi of names) // i />
-%% % </TD,E,E_l |- pati : ti gives E_li//i/>
-%% % disjoint doms(</E_li//i/>)
-%% % duplicates(</xi//i/>) = emptyset
-%% % ------------------------------------------------------------ :: record
-%% % TD,E,E_l |- <| </idi = pati li//i/> semi_opt |> : p t_args gives u+ </E_li//i/>
-%% % 
-%% % TD,E,E_l |- pat1 : t gives E_l1 ... TD,E,E_l |- patn : t gives E_ln
-%% % disjoint doms(E_l1 , ... , E_ln)
-%% % length(pat1 ... patn) = nat
-%% % ----------------------------------------------------------- :: vector
-%% % TD,E,E_l |- [| pat1 ; ... ; patn semi_opt |] : __vector nat t gives E_l1 u+ ... u+ E_ln
-%% % 
-%% % TD,E,E_l |- pat1 : __vector ne1 t gives E_l1 ... TD,E,E_l |- patn : __vector nen t gives E_ln
-%% % disjoint doms(E_l1 , ... , E_ln)
-%% % ne' = ne1 + ... + nen
-%% % ----------------------------------------------------------- :: vectorConcat
-%% % TD,E,E_l |- [| pat1 ... patn  |] : __vector ne' t gives E_l1 u+ ... u+ E_ln
-%% % 
-
-<E_t,E_k> |- pat1 : t1 gives E_t1 .... <E_t,E_k> |- patn : tn gives E_tn
-disjoint doms(E_t1,....,E_tn)
------------------------------------------------------------- :: tup
-<E_t,E_k> |- (pat1, ...., patn) : t1 * .... * tn gives E_t1 u+ .... u+ E_tn 
-
-%% % TD |- t ok
-%% % TD,E,E_l |- pat1 : t gives E_l1 .. TD,E,E_l |- patn : t gives E_ln
-%% % disjoint doms(E_l1,..,E_ln)
-%% % ------------------------------------------------------------ :: list
-%% % TD,E,E_l |- [pat1; ..; patn semi_opt] : __list t gives E_l1 u+ .. u+ E_ln 
-%% % 
-%% % TD,E,E_l1 |- pat : t gives E_l2
-%% % ------------------------------------------------------------ :: paren
-%% % TD,E,E_l1 |- (pat) : t gives E_l2
-%% % 
-%% % TD,E,E_l1 |- pat1 : t gives E_l2
-%% % TD,E,E_l1 |- pat2 : __list t gives E_l3
-%% % disjoint doms(E_l2,E_l3)
-%% % ------------------------------------------------------------ :: cons
-%% % TD,E,E_l1 |- pat1 :: pat2 : __list t gives E_l2 u+ E_l3
-%% % 
-%% % |- lit : t
-%% % ------------------------------------------------------------ :: lit
-%% % TD,E,E_l |- lit : t gives {}
-%% % 
-%% % E,E_l |- x not ctor
-%% % ------------------------------------------------------------ :: num_add
-%% % TD,E,E_l |- x l + num : __num gives {x|->__num}
-%% % 
-%% % 
-%% % 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
-%% % TD , E , E_l |- exp : t gives S_c , S_N :: :: check_exp :: check_exp_ 
-%% % {{ com Typing expressions, collecting typeclass and index constraints }}
-%% % by
-%% % 
-%% % :check_exp_aux: TD,E,E_l |- exp_aux : t gives S_c,S_N
-%% % ------------------------------------------------------------ :: all
-%% % TD,E,E_l  |- exp_aux l : t gives S_c,S_N
-%% % 
-%% % defn
-%% % TD , E , E_l |- exp_aux : t gives S_c , S_N :: :: check_exp_aux :: check_exp_aux_
-%% % {{ com Typing expressions, collecting typeclass and index constraints }}
-%% % by
-%% % 
-%% % E_l(x) gives t
-%% % ------------------------------------------------------------ :: var
-%% % TD,E,E_l |- x l1 l2 : t gives {},{}
-%% % 
-%% % %TODO KG Add check that N is in scope
-%% % ------------------------------------------------------------ :: nvar
-%% % TD,E,E_l |- N : __num gives {},{}
-%% % 
-%% % E_l |- id not shadowed
-%% % E |- id value
-%% % TD,E |- ctor id : t_multi -> p t_args gives (x of names)
-%% % ------------------------------------------------------------ :: ctor
-%% % TD,E,E_l |- id : curry(t_multi, p t_args) gives {},{}
-%% % 
-%% % E_l |- id not shadowed
-%% % E |- id value
-%% % TD, E |- val id : t gives S_c
-%% % ------------------------------------------------------------ :: val
-%% % TD,E,E_l |- id : t gives S_c,{}
-%% % 
-%% % 
-%% % 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)
-%% % ------------------------------------------------------------ :: fn
-%% % TD,E,E_l |- fun pat1 ... patn -> exp l : curry((t1*...*tn), u) gives S_c,S_N
-%% % 
-%% % %TODO: the various patterns might want to use different specifications for vector length (i.e. 32 in one and 8+n+8 in another)
-%% % % So should be pati : t gives E_li,S_Ni
-%% % </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/>
-%% % ------------------------------------------------------------ :: function
-%% % TD,E,E_l |- function bar_opt </pati -> expi li//i/> end : t -> u gives </S_ci//i/> , </S_Ni//i/>
-%% % 
-%% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N
-%% % TD,E,E_l |- exp1 : t1 -> t2 gives S_c1,S_N1
-%% % TD,E,E_l |- exp2 : t1 gives S_c2,S_N2
-%% % ------------------------------------------------------------ :: app
-%% % TD,E,E_l |- exp1 exp2 : t2 gives S_c1 union S_c2, S_N1 union S_N2
-%% % 
-%% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N
-%% % %          Same for t2
-%% % :check_exp_aux: TD,E,E_l |- (ix) : t1 -> t2 -> t3 gives S_c1,S_N1
-%% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2
-%% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3
-%% % ------------------------------------------------------------ :: infix_app1
-%% % TD,E,E_l |- exp1 ix l exp2 : t3 gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3
-%% % 
-%% % %TODO, see above todo
-%% % :check_exp_aux: TD,E,E_l |- x : t1 -> t2 -> t3 gives S_c1,S_N1
-%% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2
-%% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3
-%% % ------------------------------------------------------------ :: infix_app2
-%% % TD,E,E_l |- exp1 `x` l exp2 : t3 gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3
-%% % 
-%% % %TODO, see above todo, with regard to t_args
-%% % </TD,E |- field idi : p t_args -> ti gives (xi of names)//i/>
-%% % </TD,E,E_l |- expi : ti gives S_ci,S_Ni//i/>
-%% % duplicates(</xi//i/>) = emptyset
-%% % names = {</xi//i/>}
-%% % ------------------------------------------------------------ :: record
-%% % TD,E,E_l |- <| </idi = expi li//i/> semi_opt l |> : p t_args gives </S_ci//i/>,</S_Ni//i/>
-%% % 
-%% % %TODO, see above todo, with regard to t_args
-%% % </TD,E |- field idi : p t_args -> ti gives (xi of names)//i/>
-%% % </TD,E,E_l |- expi : ti gives S_ci,S_Ni//i/>
-%% % duplicates(</xi//i/>) = emptyset
-%% % TD,E,E_l |- exp : p t_args gives S_c',S_N'
-%% % ------------------------------------------------------------ :: recup
-%% % TD,E,E_l |- <| exp with </idi = expi li//i/> semi_opt l |> : p t_args gives S_c' union </S_ci//i/>,S_N' union </S_Ni//i/>
-%% % 
-%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 ... TD,E,E_l |- expn : t gives S_cn,S_Nn
-%% % length(exp1 ... expn) = nat
-%% % ------------------------------------------------------------ :: vector
-%% % TD,E,E_l |- [| exp1 ; ... ; expn semi_opt |] : __vector nat t gives S_c1 union ... union S_cn, S_N1 union ... union S_Nn
-%% % 
-%% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N
-%% % |- nexp ~> ne
-%% % ------------------------------------------------------------- :: vectorget
-%% % TD,E,E_l |- exp .( nexp ) : t gives S_c,S_N union {ne<ne'}
-%% % 
-%% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N
-%% % |- nexp1 ~> ne1
-%% % |- nexp2 ~> ne2
-%% % ne = :Ne_add: ne2 + (- ne1)
-%% % ------------------------------------------------------------- :: vectorsub
-%% % TD,E,E_l |- exp .( nexp1 .. nexp2 ) : __vector ne t gives S_c,S_N union {ne1 < ne2 < ne'}
-%% % 
-%% % E |- id field
-%% % TD,E |- field id : p t_args -> t gives (x of names)
-%% % TD,E,E_l |- exp : p t_args gives S_c,S_N
-%% % ------------------------------------------------------------ :: field
-%% % TD,E,E_l |- exp.id : t gives S_c,S_N
-%% % 
-%% % </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/>
-%% % 
-%% % TD,E,E_l |- exp : t gives S_c,S_N
-%% % TD,E |- typ ~> t
-%% % ------------------------------------------------------------ :: typed
-%% % TD,E,E_l |- (exp : typ) : t gives S_c,S_N
-%% % 
-%% % %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
-%% % 
-%% % TD,E,E_l |- exp1 : t1 gives S_c1,S_N1 .... TD,E,E_l |- expn : tn gives S_cn,S_Nn
-%% % ------------------------------------------------------------ :: tup
-%% % TD,E,E_l |- (exp1, ...., expn) : t1 * .... * tn gives S_c1 union .... union S_cn,S_N1 union .... union S_Nn
-%% % 
-%% % TD |- t ok
-%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 .. TD,E,E_l |- expn : t gives S_cn,S_Nn
-%% % ------------------------------------------------------------ :: list
-%% % TD,E,E_l |- [exp1; ..; expn semi_opt] : __list t gives S_c1 union .. union S_cn, S_N1 union .. union S_Nn
-%% % 
-%% % TD,E,E_l |- exp : t gives S_c,S_N
-%% % ------------------------------------------------------------ :: paren
-%% % TD,E,E_l |- (exp) : t gives S_c,S_N
-%% % 
-%% % TD,E,E_l |- exp : t gives S_c,S_N
-%% % ------------------------------------------------------------ :: begin
-%% % TD,E,E_l |- begin exp end : t gives S_c,S_N
-%% % 
-%% % %TODO t might need different index constraints
-%% % TD,E,E_l |- exp1 : __bool gives S_c1,S_N1
-%% % TD,E,E_l |- exp2 : t gives S_c2,S_N2
-%% % TD,E,E_l |- exp3 : t gives S_c3,S_N3
-%% % ------------------------------------------------------------ :: if
-%% % TD,E,E_l |- if exp1 then exp2 else exp3 : t gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3
-%% % 
-%% % %TODO t might need different index constraints
-%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1
-%% % TD,E,E_l |- exp2 : __list t gives S_c2,S_N2
-%% % ------------------------------------------------------------ :: cons
-%% % TD,E,E_l |- exp1 :: exp2 : __list t gives S_c1 union S_c2,S_N1 union S_N2
-%% % 
-%% % |- lit : t
-%% % ------------------------------------------------------------ :: lit
-%% % TD,E,E_l |- lit : t gives {},{}
-%% % 
-%% % % TODO: should require that each xi actually appears free in exp1
-%% % </TD |- ti ok//i/>
-%% % TD,E,E_l u+ {</xi|->ti//i/>} |- exp1 : t gives S_c1,S_N1
-%% % TD,E,E_l u+ {</xi|->ti//i/>} |- exp2 : __bool gives S_c2,S_N2
-%% % disjoint doms(E_l, {</xi|->ti//i/>})
-%% % E = <E_m,E_p,E_f,E_x>
-%% % </xi NOTIN dom(E_x)//i/>
-%% % ------------------------------------------------------------ :: set_comp
-%% % TD,E,E_l |- { exp1 | exp2 } : __set t gives S_c1 union S_c2,S_N1 union S_N2
-%% % 
-%% % TD,E,E_l1 |- </qbindi//i/> gives E_l2,S_c1
-%% % TD,E,E_l1 u+ E_l2 |- exp1 : t gives S_c2,S_N2
-%% % TD,E,E_l1 u+ E_l2 |- exp2 :  __bool gives S_c3,S_N3
-%% % ------------------------------------------------------------ :: set_comp_binding
-%% % TD,E,E_l1 |- { exp1 | forall </qbindi//i/> | exp2 } : __set t gives S_c1 union S_c2 union S_c3,S_N2 union S_N3
-%% % 
-%% % TD |- t ok
-%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 .. TD,E,E_l |- expn : t gives S_cn,S_Nn
-%% % ------------------------------------------------------------ :: set
-%% % TD,E,E_l |- { exp1; ..; expn semi_opt } : __set t gives S_c1 union .. union S_cn,S_N1 union .. union S_Nn
-%% % 
-%% % TD,E,E_l1 |- </qbindi//i/> gives E_l2,S_c1
-%% % TD,E,E_l1 u+ E_l2 |- exp : __bool gives S_c2,S_N2
-%% % ------------------------------------------------------------ :: quant
-%% % TD,E,E_l1 |- q </qbindi//i/> . exp : __bool gives S_c1 union S_c2,S_N2
-%% % 
-%% % TD,E,E_l1 |- list </qbindi//i/> gives E_l2,S_c1
-%% % TD,E,E_l1 u+ E_l2 |- exp1 : t gives S_c2,S_N2
-%% % TD,E,E_l1 u+ E_l2 |- exp2 : __bool gives S_c3,S_N3
-%% % ------------------------------------------------------------ :: list_comp_binding
-%% % TD,E,E_l1 |- [ exp1 | forall </qbindi//i/> | exp2 ] : __list t gives S_c1 union S_c2 union S_c3,S_N2 union S_N3
-%% % 
-%% % defn
-%% % TD , E , E_l1 |- qbind1 .. qbindn gives E_l2 , S_c :: :: check_listquant_binding
-%% % :: check_listquant_binding_
-%% % {{ com Build the environment for quantifier bindings, collecting typeclass constraints }}
-%% %  by
-%% % 
-%% % ------------------------------------------------------------ :: empty
-%% % TD,E,E_l |- gives {},{}
-%% % 
-%% % TD |- t ok
-%% % TD,E,E_l1 u+ {x |-> t} |- </qbindi//i/> gives E_l2,S_c1
-%% % disjoint doms({x |-> t}, E_l2)
-%% % ------------------------------------------------------------ :: var
-%% % TD,E,E_l1 |- x l </qbindi//i/> gives {x |-> t} u+ E_l2,S_c1
-%% % 
-%% % TD,E,E_l1 |- pat : t gives E_l3
-%% % TD,E,E_l1 |- exp : __set t gives S_c1,S_N1
-%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2
-%% % disjoint doms(E_l3, E_l2)
-%% % ------------------------------------------------------------ :: restr
-%% % TD,E,E_l1 |- (pat IN exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2
-%% % 
-%% % TD,E,E_l1 |- pat : t gives E_l3
-%% % TD,E,E_l1 |- exp : __list t gives S_c1,S_N1
-%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2
-%% % disjoint doms(E_l3, E_l2)
-%% % ------------------------------------------------------------ :: list_restr
-%% % TD,E,E_l1 |- (pat MEM exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2
-%% % 
-%% % defn
-%% % TD , E , E_l1 |- list qbind1 .. qbindn gives E_l2 , S_c :: :: check_quant_binding :: check_quant_binding_
-%% % {{ com Build the environment for quantifier bindings, collecting typeclass constraints }}
-%% %  by
-%% % 
-%% % ------------------------------------------------------------ :: empty
-%% % TD,E,E_l |- list gives {},{}
-%% % 
-%% % TD,E,E_l1 |- pat : t gives E_l3
-%% % TD,E,E_l1 |- exp : __list t gives S_c1,S_N1
-%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2
-%% % disjoint doms(E_l3, E_l2)
-%% % ------------------------------------------------------------ :: restr
-%% % TD,E,E_l1 |- list (pat MEM exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2
-%% % 
-%% % 
-%% % 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
-%% % 
-
diff --git a/language/l2_rules.ott b/language/l2_rules.ott
new file mode 100644
index 00000000..7359c1c6
--- /dev/null
+++ b/language/l2_rules.ott
@@ -0,0 +1,1051 @@
+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 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
+%% % TD |- 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
+ 
+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 : nat
+ 
+ ------------------------------------------------------------- :: 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 :: :: check_pat :: check_pat_ 
+{{ com Typing patterns, building their binding environment }}
+by
+
+E_k |-t t ok
+------------------------------------------------------------ :: wild
+<E_t,E_k> |- _ annot : t gives {} 
+% This case should perhaps indicate the generation of a type variable, with kind Typ
+
+<E_t,E_k> |- pat : t gives E_t1
+id NOTIN dom(E_t1)
+------------------------------------------------------------ :: as
+<E_t,E_k> |- (pat as id) : t gives E_t1 u+ {id|->t}
+
+E_k |- typ ~> t
+<E_t,E_k> |- pat : t gives E_t1
+------------------------------------------------------------ :: typ
+<E_t,E_k> |- (<typ> pat) : t gives E_t1
+
+%% % TD,E |- ctor id : (t1*..*tn) -> p t_args gives (x of names)
+<E_t,E_k> |- pat1 : t1 gives E_t1 .. <E_t,E_k> |- patn : tn gives E_tn
+%% % disjoint doms(E_l1,..,E_ln)
+------------------------------------------------------------ :: ident_constr
+<E_t,E_k> |- id pat1 .. patn : id t_args gives E_t1 u+ .. u+ E_tn
+
+E_k |-t t ok
+ ------------------------------------------------------------ :: var
+<E_t,E_k> |- :P_id: id : t gives E_t u+ {id|->t}
+
+%% % 
+%% % </TD,E |- field idi : p t_args -> ti gives (xi of names) // i />
+%% % </TD,E,E_l |- pati : ti gives E_li//i/>
+%% % disjoint doms(</E_li//i/>)
+%% % duplicates(</xi//i/>) = emptyset
+%% % ------------------------------------------------------------ :: record
+%% % TD,E,E_l |- <| </idi = pati li//i/> semi_opt |> : p t_args gives u+ </E_li//i/>
+%% % 
+%% % TD,E,E_l |- pat1 : t gives E_l1 ... TD,E,E_l |- patn : t gives E_ln
+%% % disjoint doms(E_l1 , ... , E_ln)
+%% % length(pat1 ... patn) = nat
+%% % ----------------------------------------------------------- :: vector
+%% % TD,E,E_l |- [| pat1 ; ... ; patn semi_opt |] : __vector nat t gives E_l1 u+ ... u+ E_ln
+%% % 
+%% % TD,E,E_l |- pat1 : __vector ne1 t gives E_l1 ... TD,E,E_l |- patn : __vector nen t gives E_ln
+%% % disjoint doms(E_l1 , ... , E_ln)
+%% % ne' = ne1 + ... + nen
+%% % ----------------------------------------------------------- :: vectorConcat
+%% % TD,E,E_l |- [| pat1 ... patn  |] : __vector ne' t gives E_l1 u+ ... u+ E_ln
+%% % 
+
+<E_t,E_k> |- pat1 : t1 gives E_t1 .... <E_t,E_k> |- patn : tn gives E_tn
+disjoint doms(E_t1,....,E_tn)
+------------------------------------------------------------ :: tup
+<E_t,E_k> |- (pat1, ...., patn) : t1 * .... * tn gives E_t1 u+ .... u+ E_tn 
+
+%% % TD |- t ok
+%% % TD,E,E_l |- pat1 : t gives E_l1 .. TD,E,E_l |- patn : t gives E_ln
+%% % disjoint doms(E_l1,..,E_ln)
+%% % ------------------------------------------------------------ :: list
+%% % TD,E,E_l |- [pat1; ..; patn semi_opt] : __list t gives E_l1 u+ .. u+ E_ln 
+%% % 
+%% % TD,E,E_l1 |- pat : t gives E_l2
+%% % ------------------------------------------------------------ :: paren
+%% % TD,E,E_l1 |- (pat) : t gives E_l2
+%% % 
+%% % TD,E,E_l1 |- pat1 : t gives E_l2
+%% % TD,E,E_l1 |- pat2 : __list t gives E_l3
+%% % disjoint doms(E_l2,E_l3)
+%% % ------------------------------------------------------------ :: cons
+%% % TD,E,E_l1 |- pat1 :: pat2 : __list t gives E_l2 u+ E_l3
+%% % 
+%% % |- lit : t
+%% % ------------------------------------------------------------ :: lit
+%% % TD,E,E_l |- lit : t gives {}
+%% % 
+%% % E,E_l |- x not ctor
+%% % ------------------------------------------------------------ :: num_add
+%% % TD,E,E_l |- x l + num : __num gives {x|->__num}
+%% % 
+%% % 
+%% % 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
+%% % TD , E , E_l |- exp : t gives S_c , S_N :: :: check_exp :: check_exp_ 
+%% % {{ com Typing expressions, collecting typeclass and index constraints }}
+%% % by
+%% % 
+%% % :check_exp_aux: TD,E,E_l |- exp_aux : t gives S_c,S_N
+%% % ------------------------------------------------------------ :: all
+%% % TD,E,E_l  |- exp_aux l : t gives S_c,S_N
+%% % 
+%% % defn
+%% % TD , E , E_l |- exp_aux : t gives S_c , S_N :: :: check_exp_aux :: check_exp_aux_
+%% % {{ com Typing expressions, collecting typeclass and index constraints }}
+%% % by
+%% % 
+%% % E_l(x) gives t
+%% % ------------------------------------------------------------ :: var
+%% % TD,E,E_l |- x l1 l2 : t gives {},{}
+%% % 
+%% % %TODO KG Add check that N is in scope
+%% % ------------------------------------------------------------ :: nvar
+%% % TD,E,E_l |- N : __num gives {},{}
+%% % 
+%% % E_l |- id not shadowed
+%% % E |- id value
+%% % TD,E |- ctor id : t_multi -> p t_args gives (x of names)
+%% % ------------------------------------------------------------ :: ctor
+%% % TD,E,E_l |- id : curry(t_multi, p t_args) gives {},{}
+%% % 
+%% % E_l |- id not shadowed
+%% % E |- id value
+%% % TD, E |- val id : t gives S_c
+%% % ------------------------------------------------------------ :: val
+%% % TD,E,E_l |- id : t gives S_c,{}
+%% % 
+%% % 
+%% % 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)
+%% % ------------------------------------------------------------ :: fn
+%% % TD,E,E_l |- fun pat1 ... patn -> exp l : curry((t1*...*tn), u) gives S_c,S_N
+%% % 
+%% % %TODO: the various patterns might want to use different specifications for vector length (i.e. 32 in one and 8+n+8 in another)
+%% % % So should be pati : t gives E_li,S_Ni
+%% % </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/>
+%% % ------------------------------------------------------------ :: function
+%% % TD,E,E_l |- function bar_opt </pati -> expi li//i/> end : t -> u gives </S_ci//i/> , </S_Ni//i/>
+%% % 
+%% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N
+%% % TD,E,E_l |- exp1 : t1 -> t2 gives S_c1,S_N1
+%% % TD,E,E_l |- exp2 : t1 gives S_c2,S_N2
+%% % ------------------------------------------------------------ :: app
+%% % TD,E,E_l |- exp1 exp2 : t2 gives S_c1 union S_c2, S_N1 union S_N2
+%% % 
+%% % %TODO t1 and t1 should be t1 and t'1 so that constraints from any vectors can be extracted and added to S_N
+%% % %          Same for t2
+%% % :check_exp_aux: TD,E,E_l |- (ix) : t1 -> t2 -> t3 gives S_c1,S_N1
+%% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2
+%% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3
+%% % ------------------------------------------------------------ :: infix_app1
+%% % TD,E,E_l |- exp1 ix l exp2 : t3 gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3
+%% % 
+%% % %TODO, see above todo
+%% % :check_exp_aux: TD,E,E_l |- x : t1 -> t2 -> t3 gives S_c1,S_N1
+%% % TD,E,E_l |- exp1 : t1 gives S_c2,S_N2
+%% % TD,E,E_l |- exp2 : t2 gives S_c3,S_N3
+%% % ------------------------------------------------------------ :: infix_app2
+%% % TD,E,E_l |- exp1 `x` l exp2 : t3 gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3
+%% % 
+%% % %TODO, see above todo, with regard to t_args
+%% % </TD,E |- field idi : p t_args -> ti gives (xi of names)//i/>
+%% % </TD,E,E_l |- expi : ti gives S_ci,S_Ni//i/>
+%% % duplicates(</xi//i/>) = emptyset
+%% % names = {</xi//i/>}
+%% % ------------------------------------------------------------ :: record
+%% % TD,E,E_l |- <| </idi = expi li//i/> semi_opt l |> : p t_args gives </S_ci//i/>,</S_Ni//i/>
+%% % 
+%% % %TODO, see above todo, with regard to t_args
+%% % </TD,E |- field idi : p t_args -> ti gives (xi of names)//i/>
+%% % </TD,E,E_l |- expi : ti gives S_ci,S_Ni//i/>
+%% % duplicates(</xi//i/>) = emptyset
+%% % TD,E,E_l |- exp : p t_args gives S_c',S_N'
+%% % ------------------------------------------------------------ :: recup
+%% % TD,E,E_l |- <| exp with </idi = expi li//i/> semi_opt l |> : p t_args gives S_c' union </S_ci//i/>,S_N' union </S_Ni//i/>
+%% % 
+%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 ... TD,E,E_l |- expn : t gives S_cn,S_Nn
+%% % length(exp1 ... expn) = nat
+%% % ------------------------------------------------------------ :: vector
+%% % TD,E,E_l |- [| exp1 ; ... ; expn semi_opt |] : __vector nat t gives S_c1 union ... union S_cn, S_N1 union ... union S_Nn
+%% % 
+%% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N
+%% % |- nexp ~> ne
+%% % ------------------------------------------------------------- :: vectorget
+%% % TD,E,E_l |- exp .( nexp ) : t gives S_c,S_N union {ne<ne'}
+%% % 
+%% % TD,E,E_l |- exp : __vector ne' t gives S_c,S_N
+%% % |- nexp1 ~> ne1
+%% % |- nexp2 ~> ne2
+%% % ne = :Ne_add: ne2 + (- ne1)
+%% % ------------------------------------------------------------- :: vectorsub
+%% % TD,E,E_l |- exp .( nexp1 .. nexp2 ) : __vector ne t gives S_c,S_N union {ne1 < ne2 < ne'}
+%% % 
+%% % E |- id field
+%% % TD,E |- field id : p t_args -> t gives (x of names)
+%% % TD,E,E_l |- exp : p t_args gives S_c,S_N
+%% % ------------------------------------------------------------ :: field
+%% % TD,E,E_l |- exp.id : t gives S_c,S_N
+%% % 
+%% % </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/>
+%% % 
+%% % TD,E,E_l |- exp : t gives S_c,S_N
+%% % TD,E |- typ ~> t
+%% % ------------------------------------------------------------ :: typed
+%% % TD,E,E_l |- (exp : typ) : t gives S_c,S_N
+%% % 
+%% % %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
+%% % 
+%% % TD,E,E_l |- exp1 : t1 gives S_c1,S_N1 .... TD,E,E_l |- expn : tn gives S_cn,S_Nn
+%% % ------------------------------------------------------------ :: tup
+%% % TD,E,E_l |- (exp1, ...., expn) : t1 * .... * tn gives S_c1 union .... union S_cn,S_N1 union .... union S_Nn
+%% % 
+%% % TD |- t ok
+%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 .. TD,E,E_l |- expn : t gives S_cn,S_Nn
+%% % ------------------------------------------------------------ :: list
+%% % TD,E,E_l |- [exp1; ..; expn semi_opt] : __list t gives S_c1 union .. union S_cn, S_N1 union .. union S_Nn
+%% % 
+%% % TD,E,E_l |- exp : t gives S_c,S_N
+%% % ------------------------------------------------------------ :: paren
+%% % TD,E,E_l |- (exp) : t gives S_c,S_N
+%% % 
+%% % TD,E,E_l |- exp : t gives S_c,S_N
+%% % ------------------------------------------------------------ :: begin
+%% % TD,E,E_l |- begin exp end : t gives S_c,S_N
+%% % 
+%% % %TODO t might need different index constraints
+%% % TD,E,E_l |- exp1 : __bool gives S_c1,S_N1
+%% % TD,E,E_l |- exp2 : t gives S_c2,S_N2
+%% % TD,E,E_l |- exp3 : t gives S_c3,S_N3
+%% % ------------------------------------------------------------ :: if
+%% % TD,E,E_l |- if exp1 then exp2 else exp3 : t gives S_c1 union S_c2 union S_c3,S_N1 union S_N2 union S_N3
+%% % 
+%% % %TODO t might need different index constraints
+%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1
+%% % TD,E,E_l |- exp2 : __list t gives S_c2,S_N2
+%% % ------------------------------------------------------------ :: cons
+%% % TD,E,E_l |- exp1 :: exp2 : __list t gives S_c1 union S_c2,S_N1 union S_N2
+%% % 
+%% % |- lit : t
+%% % ------------------------------------------------------------ :: lit
+%% % TD,E,E_l |- lit : t gives {},{}
+%% % 
+%% % % TODO: should require that each xi actually appears free in exp1
+%% % </TD |- ti ok//i/>
+%% % TD,E,E_l u+ {</xi|->ti//i/>} |- exp1 : t gives S_c1,S_N1
+%% % TD,E,E_l u+ {</xi|->ti//i/>} |- exp2 : __bool gives S_c2,S_N2
+%% % disjoint doms(E_l, {</xi|->ti//i/>})
+%% % E = <E_m,E_p,E_f,E_x>
+%% % </xi NOTIN dom(E_x)//i/>
+%% % ------------------------------------------------------------ :: set_comp
+%% % TD,E,E_l |- { exp1 | exp2 } : __set t gives S_c1 union S_c2,S_N1 union S_N2
+%% % 
+%% % TD,E,E_l1 |- </qbindi//i/> gives E_l2,S_c1
+%% % TD,E,E_l1 u+ E_l2 |- exp1 : t gives S_c2,S_N2
+%% % TD,E,E_l1 u+ E_l2 |- exp2 :  __bool gives S_c3,S_N3
+%% % ------------------------------------------------------------ :: set_comp_binding
+%% % TD,E,E_l1 |- { exp1 | forall </qbindi//i/> | exp2 } : __set t gives S_c1 union S_c2 union S_c3,S_N2 union S_N3
+%% % 
+%% % TD |- t ok
+%% % TD,E,E_l |- exp1 : t gives S_c1,S_N1 .. TD,E,E_l |- expn : t gives S_cn,S_Nn
+%% % ------------------------------------------------------------ :: set
+%% % TD,E,E_l |- { exp1; ..; expn semi_opt } : __set t gives S_c1 union .. union S_cn,S_N1 union .. union S_Nn
+%% % 
+%% % TD,E,E_l1 |- </qbindi//i/> gives E_l2,S_c1
+%% % TD,E,E_l1 u+ E_l2 |- exp : __bool gives S_c2,S_N2
+%% % ------------------------------------------------------------ :: quant
+%% % TD,E,E_l1 |- q </qbindi//i/> . exp : __bool gives S_c1 union S_c2,S_N2
+%% % 
+%% % TD,E,E_l1 |- list </qbindi//i/> gives E_l2,S_c1
+%% % TD,E,E_l1 u+ E_l2 |- exp1 : t gives S_c2,S_N2
+%% % TD,E,E_l1 u+ E_l2 |- exp2 : __bool gives S_c3,S_N3
+%% % ------------------------------------------------------------ :: list_comp_binding
+%% % TD,E,E_l1 |- [ exp1 | forall </qbindi//i/> | exp2 ] : __list t gives S_c1 union S_c2 union S_c3,S_N2 union S_N3
+%% % 
+%% % defn
+%% % TD , E , E_l1 |- qbind1 .. qbindn gives E_l2 , S_c :: :: check_listquant_binding
+%% % :: check_listquant_binding_
+%% % {{ com Build the environment for quantifier bindings, collecting typeclass constraints }}
+%% %  by
+%% % 
+%% % ------------------------------------------------------------ :: empty
+%% % TD,E,E_l |- gives {},{}
+%% % 
+%% % TD |- t ok
+%% % TD,E,E_l1 u+ {x |-> t} |- </qbindi//i/> gives E_l2,S_c1
+%% % disjoint doms({x |-> t}, E_l2)
+%% % ------------------------------------------------------------ :: var
+%% % TD,E,E_l1 |- x l </qbindi//i/> gives {x |-> t} u+ E_l2,S_c1
+%% % 
+%% % TD,E,E_l1 |- pat : t gives E_l3
+%% % TD,E,E_l1 |- exp : __set t gives S_c1,S_N1
+%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2
+%% % disjoint doms(E_l3, E_l2)
+%% % ------------------------------------------------------------ :: restr
+%% % TD,E,E_l1 |- (pat IN exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2
+%% % 
+%% % TD,E,E_l1 |- pat : t gives E_l3
+%% % TD,E,E_l1 |- exp : __list t gives S_c1,S_N1
+%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2
+%% % disjoint doms(E_l3, E_l2)
+%% % ------------------------------------------------------------ :: list_restr
+%% % TD,E,E_l1 |- (pat MEM exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2
+%% % 
+%% % defn
+%% % TD , E , E_l1 |- list qbind1 .. qbindn gives E_l2 , S_c :: :: check_quant_binding :: check_quant_binding_
+%% % {{ com Build the environment for quantifier bindings, collecting typeclass constraints }}
+%% %  by
+%% % 
+%% % ------------------------------------------------------------ :: empty
+%% % TD,E,E_l |- list gives {},{}
+%% % 
+%% % TD,E,E_l1 |- pat : t gives E_l3
+%% % TD,E,E_l1 |- exp : __list t gives S_c1,S_N1
+%% % TD,E,E_l1 u+ E_l3 |- </qbindi//i/> gives E_l2,S_c2
+%% % disjoint doms(E_l3, E_l2)
+%% % ------------------------------------------------------------ :: restr
+%% % TD,E,E_l1 |- list (pat MEM exp) </qbindi//i/> gives E_l2 u+ E_l3,S_c1 union S_c2
+%% % 
+%% % 
+%% % 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
+%% % 
+