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.

7 files changed, 1224 insertions, 1528 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
+%% % 
+
diff --git a/src/ast.ml b/src/ast.ml
index bc4e7a5d..d280f4b8 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -109,6 +109,12 @@ quant_item =
 
 
 type 
+effects_aux =  (* effect set, of kind $_$ *)
+   Effects_var of id
+ | Effects_set of (efct) list (* effect set *)
+
+
+type 
 order_aux =  (* vector order specifications, of kind $_$ *)
    Ord_id of id (* identifier *)
  | Ord_inc (* increasing (little-endian) *)
@@ -116,25 +122,32 @@ order_aux =  (* vector order specifications, of kind $_$ *)
 
 
 type 
-effects_aux =  (* effect set, of kind $_$ *)
-   Effects_var of id
- | Effects_set of (efct) list (* effect set *)
-
-
-type 
 typquant_aux =  (* type quantifiers and constraints *)
    TypQ_tq of (quant_item) list
  | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
 
 
 type 
+effects = 
+   Effects_aux of effects_aux * l
+
+
+type 
 order = 
    Ord_aux of order_aux * l
 
 
 type 
-effects = 
-   Effects_aux of effects_aux * l
+lit_aux =  (* Literal constant *)
+   L_unit (* $() : _$ *)
+ | L_zero (* $_ : _$ *)
+ | L_one (* $_ : _$ *)
+ | L_true (* $_ : _$ *)
+ | L_false (* $_ : _$ *)
+ | L_num of int (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_string of string (* string constant *)
 
 
 type 
@@ -164,31 +177,13 @@ and typ_arg =
 
 
 type 
-lit_aux =  (* Literal constant *)
-   L_unit (* $() : _$ *)
- | L_zero (* $_ : _$ *)
- | L_one (* $_ : _$ *)
- | L_true (* $_ : _$ *)
- | L_false (* $_ : _$ *)
- | L_num of int (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_string of string (* string constant *)
-
-
-type 
-typschm_aux =  (* type scheme *)
-   TypSchm_ts of typquant * typ
-
-
-type 
 lit = 
    L_aux of lit_aux * l
 
 
 type 
-typschm = 
-   TypSchm_aux of typschm_aux * l
+typschm_aux =  (* type scheme *)
+   TypSchm_ts of typquant * typ
 
 
 type 
@@ -217,6 +212,11 @@ and 'a fpat =
 
 
 type 
+typschm = 
+   TypSchm_aux of typschm_aux * l
+
+
+type 
 'a exp_aux =  (* Expression *)
    E_block of ('a exp) list (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
@@ -281,19 +281,14 @@ and 'a letbind =
 
 
 type 
-ne =  (* internal numeric expressions *)
-   Ne_var of id
- | Ne_const of int
- | Ne_mult of ne * ne
- | Ne_add of ne * ne
- | Ne_exp of ne
- | Ne_unary of ne
+rec_opt_aux =  (* Optional recursive annotation for functions *)
+   Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
 
 
 type 
-naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
-   Name_sect_none
- | Name_sect_some of string
+'a funcl_aux =  (* Function clause *)
+   FCL_Funcl of id * 'a pat * 'a exp
 
 
 type 
@@ -302,36 +297,35 @@ type
 
 
 type 
-'a funcl_aux =  (* Function clause *)
-   FCL_Funcl of id * 'a pat * 'a exp
-
-
-type 
 'a effects_opt_aux =  (* Optional effect annotation for functions *)
    Effects_opt_pure (* sugar for empty effect set *)
  | Effects_opt_effects of effects
 
 
 type 
-rec_opt_aux =  (* Optional recursive annotation for functions *)
-   Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+naming_scheme_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+   Name_sect_none
+ | Name_sect_some of string
 
 
 type 
-k =  (* Internal kinds *)
-   Ki_typ
- | Ki_nat
- | Ki_ord
- | Ki_efct
- | Ki_val (* Representing values, for use in identifier checks *)
- | Ki_ctor of (k) list * k
- | Ki_infer (* Representing an unknown kind, inferred by context *)
+rec_opt = 
+   Rec_aux of rec_opt_aux * l
 
 
 type 
-naming_scheme_opt = 
-   Name_sect_aux of naming_scheme_opt_aux * l
+'a funcl = 
+   FCL_aux of 'a funcl_aux * 'a annot
+
+
+type 
+'a tannot_opt = 
+   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+
+
+type 
+'a effects_opt = 
+   Effects_opt_aux of 'a effects_opt_aux * 'a annot
 
 
 type 
@@ -345,23 +339,24 @@ and index_range =
 
 
 type 
-'a tannot_opt = 
-   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+naming_scheme_opt = 
+   Name_sect_aux of naming_scheme_opt_aux * l
 
 
 type 
-'a funcl = 
-   FCL_aux of 'a funcl_aux * 'a annot
+'a fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
 
 
 type 
-'a effects_opt = 
-   Effects_opt_aux of 'a effects_opt_aux * 'a annot
+'a val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
 
 
 type 
-rec_opt = 
-   Rec_aux of rec_opt_aux * l
+'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
+   DT_kind of base_kind * id
+ | DT_typ of typschm * id
 
 
 type 
@@ -374,24 +369,23 @@ type
 
 
 type 
-'a default_typing_spec_aux =  (* Default kinding or typing assumption *)
-   DT_kind of base_kind * id
- | DT_typ of typschm * id
-
-
-type 
-'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * 'a tannot_opt * 'a effects_opt * ('a funcl) list
+ne =  (* internal numeric expressions *)
+   Ne_var of id
+ | Ne_const of int
+ | Ne_mult of ne * ne
+ | Ne_add of ne * ne
+ | Ne_exp of ne
+ | Ne_unary of ne
 
 
 type 
-'a val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
+'a fundef = 
+   FD_aux of 'a fundef_aux * 'a annot
 
 
 type 
-'a type_def = 
-   TD_aux of 'a type_def_aux * 'a annot
+'a val_spec = 
+   VS_aux of 'a val_spec_aux * 'a annot
 
 
 type 
@@ -400,13 +394,19 @@ type
 
 
 type 
-'a fundef = 
-   FD_aux of 'a fundef_aux * 'a annot
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
 
 
 type 
-'a val_spec = 
-   VS_aux of 'a val_spec_aux * 'a annot
+k =  (* Internal kinds *)
+   Ki_typ
+ | Ki_nat
+ | Ki_ord
+ | Ki_efct
+ | Ki_val (* Representing values, for use in identifier checks *)
+ | Ki_ctor of (k) list * k
+ | Ki_infer (* Representing an unknown kind, inferred by context *)
 
 
 type 
@@ -466,11 +466,5 @@ type
 'a defs =  (* Definition sequence *)
    Defs of ('a def) list
 
-(** definitions *)
-(** definitions *)
-(** definitions *)
-(** definitions *)
-(** definitions *)
-(** definitions *)
 
 
diff --git a/src/ast.lem b/src/lem_interp/ast.lem
index c3305c97..aebbebc6 100644
--- a/src/ast.lem
+++ b/src/lem_interp/ast.lem
@@ -8,7 +8,7 @@ type l =
   | Trans of string * option l
   | Range of num * num
 
-val disjoint : forall 'a . set 'a -> set 'a -> bool
+ val disjoint : forall 'a . set 'a -> set 'a -> bool
 let disjoint s1 s2 = 
   let diff = s1 inter s2 in
   diff = Pervasives.empty
@@ -32,11 +32,6 @@ val subst : forall 'a. list 'a -> list 'a -> bool
 type x = string (* identifier *)
 type ix = string (* infix identifier *)
 
-type id =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
-
-
 type base_kind =  (* base kind *)
  | BK_type (* kind of types *)
  | BK_nat (* kind of natural number size expressions *)
@@ -44,6 +39,15 @@ type base_kind =  (* base kind *)
  | BK_effects (* kind of effect sets *)
 
 
+type id =  (* Identifier *)
+ | Id of x
+ | DeIid of x (* remove infix status *)
+
+
+type kind =  (* kinds *)
+ | K_kind of list base_kind
+
+
 type nexp =  (* expression of kind $Nat$, for vector sizes and origins *)
  | Nexp_id of id (* identifier *)
  | Nexp_constant of num (* constant *)
@@ -52,10 +56,6 @@ type nexp =  (* expression of kind $Nat$, for vector sizes and origins *)
  | Nexp_exp of nexp (* exponential *)
 
 
-type kind =  (* kinds *)
- | K_kind of list base_kind
-
-
 type efct =  (* effect *)
  | Effect_rreg (* read register *)
  | Effect_wreg (* write register *)
@@ -66,6 +66,11 @@ type efct =  (* effect *)
  | Effect_nondet (* nondeterminism from intra-instruction parallelism *)
 
 
+type kinded_id =  (* optionally kind-annotated identifier *)
+ | KOpt_none of id (* identifier *)
+ | KOpt_kind of kind * id (* kind-annotated variable *)
+
+
 type nexp_constraint =  (* constraint over kind $Nat$ *)
  | NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
@@ -73,11 +78,6 @@ type nexp_constraint =  (* constraint over kind $Nat$ *)
  | NC_nat_set_bounded of id * list num
 
 
-type kinded_id =  (* optionally kind-annotated identifier *)
- | KOpt_none of id (* identifier *)
- | KOpt_kind of kind * id (* kind-annotated variable *)
-
-
 type order =  (* vector order specifications, of kind $Order$ *)
  | Ord_id of id (* identifier *)
  | Ord_inc (* increasing (little-endian) *)
@@ -94,15 +94,6 @@ type quant_item =  (* Either a kinded identifier or a nexp constraint for a typq
  | QI_const of nexp_constraint (* A constraint for this type *)
 
 
-type ne =  (* internal numeric expressions *)
- | Ne_var of id
- | Ne_const of num
- | Ne_mult of ne * ne
- | Ne_add of ne * ne
- | Ne_exp of ne
- | Ne_unary of ne
-
-
 type typ =  (* Type expressions, of kind $Type$ *)
  | Typ_wild (* Unspecified type *)
  | Typ_var of id (* Type variable *)
@@ -117,6 +108,11 @@ and typ_arg =  (* Type constructor arguments of all kinds *)
  | Typ_arg_effects of effects
 
 
+type typquant =  (* type quantifiers and constraints *)
+ | TypQ_tq of list quant_item
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
 type lit =  (* Literal constant *)
  | L_unit (* $() : unit$ *)
  | L_zero (* $bitzero : bit$ *)
@@ -129,19 +125,8 @@ type lit =  (* Literal constant *)
  | L_string of string (* string constant *)
 
 
-type typquant =  (* type quantifiers and constraints *)
- | TypQ_tq of list quant_item
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
-
-
-type k =  (* Internal kinds *)
- | Ki_typ
- | Ki_nat
- | Ki_ord
- | Ki_efct
- | Ki_val (* Representing values, for use in identifier checks *)
- | Ki_ctor of list k * k
- | Ki_infer (* Representing an unknown kind, inferred by context *)
+type typschm =  (* type scheme *)
+ | TypSchm_ts of typquant * typ
 
 
 type pat =  (* Pattern *)
@@ -162,11 +147,20 @@ and fpat =  (* Field pattern *)
  | FP_Fpat of id * pat
 
 
-type typschm =  (* type scheme *)
- | TypSchm_ts of typquant * typ
+type ne =  (* internal numeric expressions *)
+ | Ne_var of id
+ | Ne_const of num
+ | Ne_mult of ne * ne
+ | Ne_add of ne * ne
+ | Ne_exp of ne
+ | Ne_unary of ne
 
 
-type exp =  (* Expression *)
+type letbind =  (* Let binding *)
+ | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
+ | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
+
+and exp =  (* Expression *)
  | E_block of list exp (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
  | E_lit of lit (* literal constant *)
@@ -206,9 +200,15 @@ and fexps =  (* Field-expression list *)
 and pexp =  (* Pattern match *)
  | Pat_exp of pat * exp
 
-and letbind =  (* Let binding *)
- | LB_val_explicit of typschm * pat * exp (* value binding, explicit type (pat must be total) *)
- | LB_val_implicit of pat * exp (* value binding, implicit type (pat must be total) *)
+
+type k =  (* Internal kinds *)
+ | Ki_typ
+ | Ki_nat
+ | Ki_ord
+ | Ki_efct
+ | Ki_val (* Representing values, for use in identifier checks *)
+ | Ki_ctor of list k * k
+ | Ki_infer (* Representing an unknown kind, inferred by context *)
 
 
 type index_range =  (* index specification, for bitfields in register types *)
@@ -227,17 +227,22 @@ type rec_opt =  (* Optional recursive annotation for functions *)
  | Rec_rec (* recursive *)
 
 
-type tannot_opt =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
+type effects_opt =  (* Optional effect annotation for functions *)
+ | Effects_opt_pure (* sugar for empty effect set *)
+ | Effects_opt_effects of effects
 
 
 type funcl =  (* Function clause *)
  | FCL_Funcl of id * pat * exp
 
 
-type effects_opt =  (* Optional effect annotation for functions *)
- | Effects_opt_pure (* sugar for empty effect set *)
- | Effects_opt_effects of effects
+type tannot_opt =  (* Optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
+
+
+type default_typing_spec =  (* Default kinding or typing assumption *)
+ | DT_kind of base_kind * id
+ | DT_typ of typschm * id
 
 
 type val_spec =  (* Value type specification *)
@@ -252,11 +257,6 @@ type type_def =  (* Type definition body *)
  | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
-type default_typing_spec =  (* Default kinding or typing assumption *)
- | DT_kind of base_kind * id
- | DT_typ of typschm * id
-
-
 type fundef =  (* Function definition *)
  | FD_function of rec_opt * tannot_opt * effects_opt * list funcl
 
@@ -275,10 +275,6 @@ type def =  (* Top-level definition *)
  | DEF_scattered_end of id (* scattered definition end *)
 
 
-type ctor_def =  (* Datatype constructor definition clause *)
- | CT_ct of id * typschm
-
-
 type typ_lib =  (* library types and syntactic sugar for them *)
  | Typ_lib_unit (* unit type with value $()$ *)
  | Typ_lib_bool (* booleans $true$ and $false$ *)
@@ -296,307 +292,12 @@ type typ_lib =  (* library types and syntactic sugar for them *)
  | Typ_lib_reg of typ (* mutable register components holding typ *)
 
 
+type ctor_def =  (* Datatype constructor definition clause *)
+ | CT_ct of id * typschm
+
+
 type defs =  (* Definition sequence *)
  | Defs of list def
 
-(** definitions *)
- (* defns translate_ast *)
-indreln
-
-(** definitions *)
- (* defns check_t *)
-indreln
-(* defn check_t *)
-
-check_t_var: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_typ )
- ==> 
-check_t E_k (T_var id)
-
-and
-check_t_varInfer: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_infer ) &&
-((Formula_update_k E_k id Ki_typ))
- ==> 
-check_t E_k (T_var id)
-
-and
-check_t_fn: forall E_k t1 t2 effects .
-(check_t E_k t1) &&
-(check_t E_k t2) &&
-(check_ef E_k effects)
- ==> 
-check_t E_k (T_fn t1 t2 effects)
-
-and
-check_t_tup: forall t_list E_k .
-((List.for_all (fun b -> b) ((List.map (fun t_ -> check_t E_k t_) t_list))))
- ==> 
-check_t E_k (T_tup (t_list))
-
-and
-check_t_app: forall t_arg_k_list E_k id .
-( Pmap.find  id   E_k  =  (Ki_ctor ((List.map (fun (t_arg_,k_) -> k_) t_arg_k_list)) Ki_typ) ) &&
-((List.for_all (fun b -> b) ((List.map (fun (t_arg_,k_) -> check_targs E_k k_ t_arg_) t_arg_k_list))))
- ==> 
-check_t E_k (T_app id (T_args ((List.map (fun (t_arg_,k_) -> t_arg_) t_arg_k_list))))
-
-
-and
-(* defn check_ef *)
-
-check_ef_var: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_efct )
- ==> 
-check_ef E_k (Effects_var id)
-
-and
-check_ef_varInfer: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_infer ) &&
-((Formula_update_k E_k id Ki_efct))
- ==> 
-check_ef E_k (Effects_var id)
-
-and
-check_ef_set: forall efct_list E_k .
-true
- ==> 
-check_ef E_k (Effects_set (efct_list))
-
-
-and
-(* defn check_n *)
-
-check_n_var: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_nat )
- ==> 
-check_n E_k (Ne_var id)
-
-and
-check_n_varInfer: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_infer ) &&
-((Formula_update_k E_k id Ki_nat))
- ==> 
-check_n E_k (Ne_var id)
-
-and
-check_n_num: forall E_k num .
-true
- ==> 
-check_n E_k (Ne_const num)
-
-and
-check_n_sum: forall E_k ne1 ne2 .
-(check_n E_k ne1) &&
-(check_n E_k ne2)
- ==> 
-check_n E_k (Ne_add ne1 ne2)
-
-and
-check_n_mult: forall E_k ne1 ne2 .
-(check_n E_k ne1) &&
-(check_n E_k ne2)
- ==> 
-check_n E_k (Ne_mult ne1 ne2)
-
-and
-check_n_exp: forall E_k ne .
-(check_n E_k ne)
- ==> 
-check_n E_k (Ne_exp ne)
-
-
-and
-(* defn check_ord *)
-
-check_ord_var: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_ord )
- ==> 
-check_ord E_k (Ord_id id)
-
-and
-check_ord_varInfer: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_infer ) &&
-((Formula_update_k E_k id Ki_ord))
- ==> 
-check_ord E_k (Ord_id id)
-
-
-and
-(* defn check_targs *)
-
-check_targs_typ: forall E_k t .
-(check_t E_k t)
- ==> 
-check_targs E_k Ki_typ (Typ t)
-
-and
-check_targs_eff: forall E_k effects .
-(check_ef E_k effects)
- ==> 
-check_targs E_k Ki_efct (Effect effects)
-
-and
-check_targs_nat: forall E_k ne .
-(check_n E_k ne)
- ==> 
-check_targs E_k Ki_nat (Nexp ne)
-
-and
-check_targs_ord: forall E_k order .
-(check_ord E_k order)
- ==> 
-check_targs E_k Ki_ord (Order order)
-
-
-(** definitions *)
- (* defns convert_typ *)
-indreln
-(* defn convert_typ *)
-
-convert_typ_var: forall E_k id .
-( Pmap.find  id   E_k  =  Ki_typ )
- ==> 
-convert_typ E_k (Typ_var id) (T_var id)
-
-and
-convert_typ_fn: forall E_k typ1 typ2 effects t1 t2 .
-(convert_typ E_k typ1 t1) &&
-(convert_typ E_k typ2 t2) &&
-(check_ef E_k effects)
- ==> 
-convert_typ E_k (Typ_fn typ1 typ2 effects) (T_fn t1 t2 effects)
-
-and
-convert_typ_tup: forall typ_t_list E_k .
-((List.for_all (fun b -> b) ((List.map (fun (typ_,t_) -> convert_typ E_k typ_ t_) typ_t_list))))
- ==> 
-convert_typ E_k (Typ_tup ((List.map (fun (typ_,t_) -> typ_) typ_t_list))) (T_tup ((List.map (fun (typ_,t_) -> t_) typ_t_list)))
-
-and
-convert_typ_app: forall typ_arg_t_arg_k_list E_k id .
-( Pmap.find  id   E_k  =  (Ki_ctor ((List.map (fun (typ_arg_,t_arg_,k_) -> k_) typ_arg_t_arg_k_list)) Ki_typ) ) &&
-((List.for_all (fun b -> b) ((List.map (fun (typ_arg_,t_arg_,k_) -> convert_targ E_k k_ typ_arg_ t_arg_) typ_arg_t_arg_k_list))))
- ==> 
-convert_typ E_k (Typ_app id ((List.map (fun (typ_arg_,t_arg_,k_) -> typ_arg_) typ_arg_t_arg_k_list))) (T_app id (T_args ((List.map (fun (typ_arg_,t_arg_,k_) -> t_arg_) typ_arg_t_arg_k_list))))
-
-and
-convert_typ_eq: forall E_k typ t2 t1 .
-(convert_typ E_k typ t1)
- ==> 
-convert_typ E_k typ t2
-
-
-and
-(* defn convert_targ *)
-
-
-(** definitions *)
- (* defns check_lit *)
-indreln
-(* defn check_lit *)
-
-check_lit_true: forall .
-true
- ==> 
-check_lit L_true (T_var  bool_id )
-
-and
-check_lit_false: forall .
-true
- ==> 
-check_lit L_false (T_var  bool_id )
-
-and
-check_lit_num: forall num .
-true
- ==> 
-check_lit (L_num num) (T_var  nat_id )
-
-and
-check_lit_string: forall string .
-true
- ==> 
-check_lit (L_string string) (T_var  string_id )
-
-and
-check_lit_hex: forall hex zero num .
-( ( (Ne_const num)  =   (hlength  hex )  ) )
- ==> 
-check_lit (L_hex hex) (T_app  vector_id  (T_args ([((Nexp (Ne_const zero)))] @ [((Nexp (Ne_const num)))] @ [((Order Ord_inc))] @ [((Typ (T_var  bit_id )))])))
-
-and
-check_lit_bin: forall bin zero num .
-( ( (Ne_const num)  =   (blength  bin )  ) )
- ==> 
-check_lit (L_bin bin) (T_app  vector_id  (T_args ([((Nexp (Ne_const zero)))] @ [((Nexp (Ne_const num)))] @ [((Order Ord_inc))] @ [((Typ (T_var  bit_id )))])))
-
-and
-check_lit_unit: forall .
-true
- ==> 
-check_lit L_unit (T_var  unit_id )
-
-and
-check_lit_bitzero: forall .
-true
- ==> 
-check_lit L_zero (T_var  bit_id )
-
-and
-check_lit_bitone: forall .
-true
- ==> 
-check_lit L_one (T_var  bit_id )
-
-
-(** definitions *)
- (* defns check_pat *)
-indreln
-(* defn check_pat *)
-
-check_pat_wild: forall E_k t .
-(check_t E_k t)
- ==> 
-(PARSE_ERROR "line 1762 - 1763" "no parses (char 16): <E_t,E_k> |- _ a***nnot : t gives {}  ")
-
-and
-check_pat_as: forall E_t E_k pat id t E_t1 .
-(check_pat  (Env  E_k   E_t )  pat t E_t1) &&
-( Pervasives.not (Pmap.mem  id   E_t1 ) )
- ==> 
-check_pat  (Env  E_k   E_t )  (P_as pat id) t  (List.fold_right union_map  ([(E_t1)] @ [( (List.fold_right (fun (x,f) m -> Pmap.add x f m)  ([(id,t)])  Pmap.empty) )])  Pmap.empty) 
-
-and
-check_pat_typ: forall E_t E_k typ pat t E_t1 .
-(convert_typ E_k typ t) &&
-(check_pat  (Env  E_k   E_t )  pat t E_t1)
- ==> 
-check_pat  (Env  E_k   E_t )  (P_typ typ pat) t E_t1
-
-and
-check_pat_ident_constr: forall pat_E_t_t_list E_t E_k id t_args .
-((List.for_all (fun b -> b) ((List.map (fun (pat_,E_t_,t_) -> check_pat  (Env  E_k   E_t )  pat_ t_ E_t_) pat_E_t_t_list))))
- ==> 
-check_pat  (Env  E_k   E_t )  (P_app id ((List.map (fun (pat_,E_t_,t_) -> pat_) pat_E_t_t_list))) (T_app id t_args)  (List.fold_right union_map  ((List.map (fun (pat_,E_t_,t_) -> E_t_) pat_E_t_t_list))  Pmap.empty) 
-
-and
-check_pat_var: forall E_t E_k id t .
-(check_t E_k t)
- ==> 
-check_pat  (Env  E_k   E_t )  (P_id id) t  (List.fold_right union_map  ([(E_t)] @ [( (List.fold_right (fun (x,f) m -> Pmap.add x f m)  ([(id,t)])  Pmap.empty) )])  Pmap.empty) 
-
-and
-check_pat_tup: forall pat_t_E_t_list E_t E_k .
-((List.for_all (fun b -> b) ((List.map (fun (pat_,t_,E_t_) -> check_pat  (Env  E_k   E_t )  pat_ t_ E_t_) pat_t_E_t_list)))) &&
-( disjoint_all (List.map Pmap.domain  ((List.map (fun (pat_,t_,E_t_) -> E_t_) pat_t_E_t_list)) ) )
- ==> 
-check_pat  (Env  E_k   E_t )  (P_tup ((List.map (fun (pat_,t_,E_t_) -> pat_) pat_t_E_t_list))) (T_tup ((List.map (fun (pat_,t_,E_t_) -> t_) pat_t_E_t_list)))  (List.fold_right union_map  ((List.map (fun (pat_,t_,E_t_) -> E_t_) pat_t_E_t_list))  Pmap.empty) 
-
-
-(** definitions *)
- (* defns check_exp *)
-indreln
-
 
 
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index d51e0c12..bcc5961d 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -340,8 +340,8 @@ let pp_defs ppf (Defs(defs)) =
 
 let pp_format_id_lem (Id_aux(i,_)) =
   match i with
-  | Id(i) -> "(Id " ^ i ^ ")"
-  | DeIid(x) -> "(DeIid " ^ x ^ ")"
+  | Id(i) -> "(Id \"" ^ i ^ "\")"
+  | DeIid(x) -> "(DeIid \"" ^ x ^ "\")"
 
 let pp_lem_id ppf id = base ppf (pp_format_id_lem id)
 
@@ -352,12 +352,12 @@ let pp_format_bkind_lem (BK_aux(k,_)) =
   | BK_order -> "BK_order"
   | BK_effects -> "BK_effects"
 
-let pp_lem_bkind ppf bk = base ppf (pp_format_bkind bk)
+let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk)
 
 let pp_format_kind_lem (K_aux(K_kind(klst),_)) = 
-  "(K_kind [" ^ list_format "; " pp_format_bkind klst ^ "])"
+  "(K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "])"
 
-let pp_lem_kind ppf k = base ppf (pp_format_kind k)
+let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k)
 
 let rec pp_format_typ_lem (Typ_aux(t,_)) =
   match t with
@@ -365,7 +365,7 @@ let rec pp_format_typ_lem (Typ_aux(t,_)) =
   | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ 
                              pp_format_typ_lem ret ^ " " ^
                             (pp_format_effects_lem efct) ^ ")"
-  | Typ_tup(typs) -> "(Typ_tup " ^ (list_format " " pp_format_typ_lem typs) ^ ")"
+  | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])"
   | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
 and pp_format_nexp_lem (Nexp_aux(n,_)) = 
   match n with
@@ -409,9 +409,9 @@ let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e)
 
 let pp_format_nexp_constraint_lem (NC_aux(nc,_)) =
   match nc with
-  | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp n2 ^ ")"
-  | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp n1 ^ " " ^ pp_format_nexp n2 ^ ")"
-  | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp n1 ^ " " ^ pp_format_nexp n2 ^ ")"
+  | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
+  | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
+  | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
   | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^ 
     pp_format_id id ^
       " [" ^
@@ -422,12 +422,12 @@ let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc)
 
 let pp_format_qi_lem (QI_aux(qi,_)) =
   match qi with
-  | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint n_const ^ ")"
+  | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint_lem n_const ^ ")"
   | QI_id(KOpt_aux(ki,_)) ->
     "(QI_id " ^
     (match ki with
-    | KOpt_none(id) -> "(KOpt_none " ^ pp_format_id id ^ ")"
-    | KOpt_kind(k,id) -> "(KOpt_kind " ^ pp_format_kind k ^ " " ^ pp_format_id id ^ ")") ^ ")"
+    | KOpt_none(id) -> "(KOpt_none " ^ pp_format_id_lem id ^ ")"
+    | KOpt_kind(k,id) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_id_lem id ^ ")") ^ ")"
 
 let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi)
 
@@ -435,9 +435,9 @@ let pp_format_typquant_lem (TypQ_aux(tq,_)) =
   match tq with
   | TypQ_no_forall -> "TypQ_no_forall"
   | TypQ_tq(qlist) ->
-    "(TypQ_tq " ^ 
-    (list_format " " pp_format_qi qlist) ^
-    ")"
+    "(TypQ_tq [" ^ 
+    (list_format "; " pp_format_qi_lem qlist) ^
+    "])"
 
 let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq)
 
@@ -548,8 +548,8 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,_)) =
 
 let pp_lem_default ppf (DT_aux(df,_)) =
   match df with
-  | DT_kind(bk,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "DT_kind" pp_lem_bkind bk pp_lem_id id
-  | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
+  | DT_kind(bk,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_id id
+  | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
 
 let pp_lem_spec ppf (VS_aux(VS_val_spec(ts,id),_)) =
   fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
@@ -568,25 +568,25 @@ let rec pp_lem_range ppf (BF_aux(r,_)) =
 let pp_lem_typdef ppf (TD_aux(td,_)) =
   match td with
   | TD_abbrev(id,namescm,typschm) -> 
-    fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
+    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
   | TD_record(id,nm,typq,fs,_) -> 
     let f_pp ppf (typ,id) =
       fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
-    fprintf ppf "@[<0>(%a %a %a %a [%a])]@\n" 
+    fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" 
       kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
   | TD_variant(id,nm,typq,ar,_) ->
     let a_pp ppf (typ,id) = 
       fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
-    fprintf ppf "@[<0>(%a %a %a %a [%a])]@\n" 
+    fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" 
       kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar 
   | TD_enum(id,ns,enums,_) ->
     let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
-    fprintf ppf "@[<0>(%a %a %a [%a])@]@\n"
+    fprintf ppf "@[<0>(%a %a %a [%a] false)@]"
       kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
   | TD_register(id,n1,n2,rs) -> 
     let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
     let pp_rids = (list_pp pp_rid pp_rid) in
-    fprintf ppf "@[<0>(%a %a %a %a [%a])@]@\n"
+    fprintf ppf "@[<0>(%a %a %a %a [%a])@]"
      kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
 
 let pp_lem_rec ppf (Rec_aux(r,_)) =
@@ -608,17 +608,17 @@ let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
 
 let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   let pp_funcls ppf funcl = fprintf ppf "%a %a" kwd ";" pp_lem_funcl funcl in
-  fprintf ppf "@[<0>(%a %a %a %a [%a]@]@\n" 
+  fprintf ppf "@[<0>(%a %a %a %a [%a]@]" 
     kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls
 
 let pp_lem_def ppf (DEF_aux(d,(l,_))) =
   match d with
-  | DEF_default(df) -> fprintf ppf "(DEF_default %a)" pp_lem_default df
-  | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a)" pp_lem_spec v_spec
-  | DEF_type(t_def) -> fprintf ppf "(DEF_type %a)" pp_lem_typdef t_def
-  | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a)" pp_lem_fundef f_def
-  | DEF_val(lbind) -> fprintf ppf "(DEF_val %a)" pp_lem_let lbind
-  | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id
+  | DEF_default(df) -> fprintf ppf "(DEF_default %a);@\n" pp_lem_default df
+  | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);@\n" pp_lem_spec v_spec
+  | DEF_type(t_def) -> fprintf ppf "(DEF_type %a);@\n" pp_lem_typdef t_def
+  | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);@\n" pp_lem_fundef f_def
+  | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind
+  | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@];@\n" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id
   | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs")
 
 let pp_lem_defs ppf (Defs(defs)) =
diff --git a/src/process_file.ml b/src/process_file.ml
index a73eeac3..ce99f037 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -77,7 +77,7 @@ let convert_ast (defs : Parse_ast.defs) : Type_internal.tannot Ast.defs =
   Initial_check.to_ast Nameset.empty Type_internal.initial_kind_env Envmap.empty defs
 
 let open_output_with_check file_name =
-  let (temp_file_name, o) = Filename.open_temp_file "lem_temp" "" in
+  let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
   let o' = Format.formatter_of_out_channel o in
   (o', (o, temp_file_name, file_name))
 
@@ -136,7 +136,9 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
       | Lem_ast_out ->
 	begin
 	  let (o, ext_o) = open_output_with_check (f' ^ ".lem") in
-	  Format.fprintf o "(* %s *)" (generated_line filename);
+	  Format.fprintf o "(* %s *)@\n" (generated_line filename);
+          Format.fprintf o "open Ast@\n";
+          Format.fprintf o "let defs = ";
 	  Pretty_print.pp_lem_defs o defs;
 	  close_output_with_check ext_o
 	end