Reduce redundant information in AST

10 files changed, 297 insertions, 1332 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 9f500046..969a5bbf 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -75,11 +75,6 @@ type base_effect =
  | BE_aux of base_effect_aux * l
 
 
-type id_aux =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
-
-
 type effect_aux =  (* effect set, of kind Effects *)
  | Effect_var of kid
  | Effect_set of list base_effect (* effect set *)
@@ -91,8 +86,9 @@ type order_aux =  (* vector order specifications, of kind Order *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
-type id = 
- | Id_aux of id_aux * l
+type id_aux =  (* Identifier *)
+ | Id of x
+ | DeIid of x (* remove infix status *)
 
 
 type effect = 
@@ -102,6 +98,10 @@ type effect =
 type order = 
  | Ord_aux of order_aux * l
 
+
+type id = 
+ | Id_aux of id_aux * l
+
 let effect_union e1 e2 = 
   match (e1,e2) with
   | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l
@@ -320,7 +320,7 @@ type rec_opt =
 
 
 type funcl 'a = 
- | FCL_aux of (funcl_aux 'a) * annot 'a
+ | FCL_aux of (funcl_aux 'a) * l
 
 
 type name_scm_opt = 
@@ -361,6 +361,10 @@ type type_def_aux 'a =  (* Type definition body *)
  | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
+type dec_spec_aux 'a =  (* Register declarations *)
+ | DEC_reg of typ * id
+
+
 type fundef_aux 'a =  (* Function definition *)
  | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
 
@@ -384,30 +388,30 @@ type type_def 'a =
  | TD_aux of (type_def_aux 'a) * annot 'a
 
 
+type dec_spec 'a = 
+ | DEC_aux of (dec_spec_aux 'a) * annot 'a
+
+
 type fundef 'a = 
  | FD_aux of (fundef_aux 'a) * annot 'a
 
 
 type default_spec 'a = 
- | DT_aux of (default_spec_aux 'a) * annot 'a
+ | DT_aux of (default_spec_aux 'a) * l
 
 
 type val_spec 'a = 
  | VS_aux of (val_spec_aux 'a) * annot 'a
 
 
-type def_aux 'a =  (* Top-level definition *)
+type def 'a =  (* Top-level definition *)
  | DEF_type of (type_def 'a) (* type definition *)
  | DEF_fundef of (fundef 'a) (* function definition *)
  | DEF_val of (letbind 'a) (* value definition *)
  | DEF_spec of (val_spec 'a) (* top-level type constraint *)
  | DEF_default of (default_spec 'a) (* default kind and type assumptions *)
  | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *)
- | DEF_reg_dec of typ * id (* register declaration *)
-
-
-type def 'a = 
- | DEF_aux of (def_aux 'a) * annot 'a
+ | DEF_reg_dec of (dec_spec 'a) (* register declaration *)
 
 
 type defs 'a =  (* Definition sequence *)
@@ -471,15 +475,6 @@ type nec =  (* Numeric expression constraints *)
  | Nec_in of x * list integer
 
 
-type tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
- | Tag_empty
- | Tag_ctor (* Data constructor from a type union *)
- | Tag_extern of maybe string (* External function, specied only with a val statement *)
- | Tag_default (* Type has come from default declaration, identifier may not be bound locally *)
- | Tag_spec
- | Tag_enum
-
-
 type t =  (* Internal types *)
  | T_id of x
  | T_var of x
@@ -498,6 +493,15 @@ and t_args =  (* Arguments to type constructors *)
  | T_args of list t_arg
 
 
+type tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
+ | Tag_empty
+ | Tag_ctor (* Data constructor from a type union *)
+ | Tag_extern of maybe string (* External function, specied only with a val statement *)
+ | Tag_default (* Type has come from default declaration, identifier may not be bound locally *)
+ | Tag_spec
+ | Tag_enum
+
+
 type tinf =  (* Type variables, type, and constraints, bound to an identifier *)
  | Tinf_typ of t
  | Tinf_quant_typ of (map tid kinf) * list nec * tag * t
diff --git a/language/l2.ml b/language/l2.ml
index 927f702b..6501ff28 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -200,7 +200,10 @@ typschm_aux =  (* type scheme *)
 
 
 type 
-'a pat_aux =  (* Pattern *)
+'a fpat = 
+   FP_aux of 'a fpat_aux * 'a annot
+
+and 'a pat_aux =  (* Pattern *)
    P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
  | P_as of 'a pat * id (* named pattern *)
@@ -220,9 +223,6 @@ and 'a pat =
 and 'a fpat_aux =  (* Field pattern *)
    FP_Fpat of id * 'a pat
 
-and 'a fpat = 
-   FP_aux of 'a fpat_aux * 'a annot
-
 
 type 
 typschm = 
@@ -230,35 +230,7 @@ typschm =
 
 
 type 
-'a lexp = 
-   LEXP_aux of 'a lexp_aux * 'a annot
-
-and 'a fexp_aux =  (* Field-expression *)
-   FE_Fexp of id * 'a exp
-
-and 'a fexp = 
-   FE_aux of 'a fexp_aux * 'a annot
-
-and 'a fexps_aux =  (* Field-expression list *)
-   FES_Fexps of ('a fexp) list * bool
-
-and 'a fexps = 
-   FES_aux of 'a fexps_aux * 'a annot
-
-and 'a pexp_aux =  (* Pattern match *)
-   Pat_exp of 'a pat * 'a exp
-
-and 'a pexp = 
-   Pat_aux of 'a pexp_aux * 'a annot
-
-and 'a letbind_aux =  (* Let binding *)
-   LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
- | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
-
-and 'a letbind = 
-   LB_aux of 'a letbind_aux * 'a annot
-
-and 'a exp_aux =  (* Expression *)
+'a exp_aux =  (* Expression *)
    E_block of ('a exp) list (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
  | E_lit of lit (* literal constant *)
@@ -296,6 +268,34 @@ and 'a lexp_aux =  (* lvalue expression *)
  | LEXP_vector_range of 'a lexp * 'a exp * 'a exp (* subvector *)
  | LEXP_field of 'a lexp * id (* struct field *)
 
+and 'a lexp = 
+   LEXP_aux of 'a lexp_aux * 'a annot
+
+and 'a fexp_aux =  (* Field-expression *)
+   FE_Fexp of id * 'a exp
+
+and 'a fexp = 
+   FE_aux of 'a fexp_aux * 'a annot
+
+and 'a fexps_aux =  (* Field-expression list *)
+   FES_Fexps of ('a fexp) list * bool
+
+and 'a fexps = 
+   FES_aux of 'a fexps_aux * 'a annot
+
+and 'a pexp_aux =  (* Pattern match *)
+   Pat_exp of 'a pat * 'a exp
+
+and 'a pexp = 
+   Pat_aux of 'a pexp_aux * 'a annot
+
+and 'a letbind_aux =  (* Let binding *)
+   LB_val_explicit of typschm * 'a pat * 'a exp (* value binding, explicit type ('a pat must be total) *)
+ | LB_val_implicit of 'a pat * 'a exp (* value binding, implicit type ('a pat must be total) *)
+
+and 'a letbind = 
+   LB_aux of 'a letbind_aux * 'a annot
+
 
 type 
 effect_opt_aux =  (* Optional effect annotation for functions *)
@@ -348,7 +348,7 @@ rec_opt =
 
 type 
 'a funcl = 
-   FCL_aux of 'a funcl_aux * 'a annot
+   FCL_aux of 'a funcl_aux * l
 
 
 type 
@@ -387,12 +387,8 @@ type
 
 
 type 
-'a type_def_aux =  (* Type definition body *)
-   TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
- | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
- | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
- | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
+'a dec_spec_aux =  (* Register declarations *)
+   DEC_reg of typ * id
 
 
 type 
@@ -402,6 +398,15 @@ type
 
 
 type 
+'a type_def_aux =  (* Type definition body *)
+   TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
+ | TD_record of id * name_scm_opt * typquant * ((typ * id)) list * bool (* struct type definition *)
+ | TD_variant of id * name_scm_opt * typquant * (type_union) list * bool (* union type definition *)
+ | TD_enum of id * name_scm_opt * (id) list * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * ((index_range * id)) list (* register mutable bitfield type definition *)
+
+
+type 
 'a val_spec_aux =  (* Value type specification *)
    VS_val_spec of typschm * id
  | VS_extern_no_rename of typschm * id
@@ -419,13 +424,18 @@ type
 
 
 type 
-'a type_def = 
-   TD_aux of 'a type_def_aux * 'a annot
+'a dec_spec = 
+   DEC_aux of 'a dec_spec_aux * 'a annot
 
 
 type 
 'a default_spec = 
-   DT_aux of 'a default_spec_aux * 'a annot
+   DT_aux of 'a default_spec_aux * l
+
+
+type 
+'a type_def = 
+   TD_aux of 'a type_def_aux * 'a annot
 
 
 type 
@@ -434,19 +444,14 @@ type
 
 
 type 
-'a def_aux =  (* Top-level definition *)
+'a def =  (* Top-level definition *)
    DEF_type of 'a type_def (* type definition *)
  | DEF_fundef of 'a fundef (* function definition *)
  | DEF_val of 'a letbind (* value definition *)
  | DEF_spec of 'a val_spec (* top-level type constraint *)
  | DEF_default of 'a default_spec (* default kind and type assumptions *)
  | DEF_scattered of 'a scattered_def (* scattered function and type definition *)
- | DEF_reg_dec of typ * id (* register declaration *)
-
-
-type 
-'a def = 
-   DEF_aux of 'a def_aux * 'a annot
+ | DEF_reg_dec of 'a dec_spec (* register declaration *)
 
 
 type 
diff --git a/language/l2.ott b/language/l2.ott
index 87fddc49..7b619652 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -753,7 +753,7 @@ effect_opt :: 'Effect_opt_' ::=
 
 funcl :: 'FCL_' ::=
   {{ com Function clause }}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ aux _ l }} {{ auxparam 'a }}
   | id pat = exp                   :: :: Funcl
 
 
@@ -789,7 +789,7 @@ val_spec :: 'VS_' ::=
 
 default_spec :: 'DT_' ::=
   {{ com Default kinding or typing assumption }}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ aux _ l }} {{ auxparam 'a }}
   | default base_kind kid    :: :: kind
   | default typschm id      :: :: typ
 % The intended semantics of these is that if an id in binding position
@@ -815,13 +815,18 @@ scattered_def :: 'SD_' ::=
 {{ com scattered definition end }}
 
 
+dec_spec :: 'DEC_' ::=
+  {{ com Register declarations }}
+  {{ aux _ annot }} {{ auxparam 'a }}
+  | register typ id                                             :: :: reg
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Top-level definitions                                        %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 def :: 'DEF_' ::=
   {{ com Top-level definition }}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ auxparam 'a }}
   | type_def                                                    :: :: type
     {{ com type definition }}
   | fundef                                                   :: :: fundef
@@ -834,7 +839,7 @@ def :: 'DEF_' ::=
     {{ com default kind and type assumptions }}
   | scattered_def                                        :: :: scattered
     {{ com scattered function and type definition }}
-  | register typ id                                   :: :: reg_dec
+  | dec_spec                                            :: :: reg_dec
     {{ com register declaration }}
 
 
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index 741a8a94..7be33bc4 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -30,6 +30,12 @@ base_kind =
 
 
 type 
+id_aux =  (* Identifier *)
+   Id of x
+ | DeIid of x (* remove infix status *)
+
+
+type 
 kid_aux =  (* identifiers with kind, ticked to differntiate from program variables *)
    Var of x
 
@@ -46,14 +52,13 @@ base_effect_aux =  (* effect *)
 
 
 type 
-id_aux =  (* Identifier *)
-   Id of x
- | DeIid of x (* remove infix status *)
+kind_aux =  (* kinds *)
+   K_kind of (base_kind) list
 
 
 type 
-kind_aux =  (* kinds *)
-   K_kind of (base_kind) list
+id = 
+   Id_aux of id_aux * l
 
 
 type 
@@ -67,11 +72,6 @@ base_effect =
 
 
 type 
-id = 
-   Id_aux of id_aux * l
-
-
-type 
 kind = 
    K_aux of kind_aux * l
 
@@ -252,21 +252,15 @@ and letbind =
 
 
 type 
-type_union_aux =  (* Type union constructors *)
-   Tu_id of id
- | Tu_ty_id of atyp * id
-
-
-type 
 name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
    Name_sect_none
  | Name_sect_some of string
 
 
 type 
-effect_opt_aux =  (* Optional effect annotation for functions *)
-   Effect_opt_pure (* sugar for empty effect set *)
- | Effect_opt_effect of atyp
+type_union_aux =  (* Type union constructors *)
+   Tu_id of id
+ | Tu_ty_id of atyp * id
 
 
 type 
@@ -276,6 +270,12 @@ tannot_opt_aux =  (* Optional type annotation for functions *)
 
 
 type 
+effect_opt_aux =  (* Optional effect annotation for functions *)
+   Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of atyp
+
+
+type 
 rec_opt_aux =  (* Optional recursive annotation for functions *)
    Rec_nonrec (* non-recursive *)
  | Rec_rec (* recursive *)
@@ -287,6 +287,11 @@ funcl_aux =  (* Function clause *)
 
 
 type 
+name_scm_opt = 
+   Name_sect_aux of name_scm_opt_aux * l
+
+
+type 
 index_range_aux =  (* index specification, for bitfields in register types *)
    BF_single of int (* single index *)
  | BF_range of int * int (* index range *)
@@ -302,8 +307,8 @@ type_union =
 
 
 type 
-name_scm_opt = 
-   Name_sect_aux of name_scm_opt_aux * l
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 type 
@@ -312,11 +317,6 @@ effect_opt =
 
 
 type 
-tannot_opt = 
-   Typ_annot_opt_aux of tannot_opt_aux * l
-
-
-type 
 rec_opt = 
    Rec_aux of rec_opt_aux * l
 
@@ -327,6 +327,13 @@ funcl =
 
 
 type 
+val_spec_aux =  (* Value type specification *)
+   VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string
+
+
+type 
 type_def_aux =  (* Type definition body *)
    TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
  | TD_record of id * name_scm_opt * typquant * ((atyp * id)) list * bool (* struct type definition *)
@@ -336,12 +343,22 @@ type_def_aux =  (* Type definition body *)
 
 
 type 
+dec_spec_aux =  (* Register declarations *)
+   DEC_reg of atyp * id
+
+
+type 
 default_typing_spec_aux =  (* Default kinding or typing assumption *)
    DT_kind of base_kind * kid
  | DT_typ of typschm * id
 
 
 type 
+fundef_aux =  (* Function definition *)
+   FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list
+
+
+type 
 scattered_def_aux =  (* Function and type union definitions that can be spread across
          a file. Each one must end in $_$ *)
    SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
@@ -352,15 +369,8 @@ scattered_def_aux =  (* Function and type union definitions that can be spread a
 
 
 type 
-val_spec_aux =  (* Value type specification *)
-   VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string
-
-
-type 
-fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * tannot_opt * effect_opt * (funcl) list
+val_spec = 
+   VS_aux of val_spec_aux * l
 
 
 type 
@@ -369,44 +379,34 @@ type_def =
 
 
 type 
-default_typing_spec = 
-   DT_aux of default_typing_spec_aux * l
+dec_spec = 
+   DEC_aux of dec_spec_aux * l
 
 
 type 
-scattered_def = 
-   SD_aux of scattered_def_aux * l
+default_typing_spec = 
+   DT_aux of default_typing_spec_aux * l
 
 
 type 
-val_spec = 
-   VS_aux of val_spec_aux * l
+fundef = 
+   FD_aux of fundef_aux * l
 
 
 type 
-fundef = 
-   FD_aux of fundef_aux * l
+scattered_def = 
+   SD_aux of scattered_def_aux * l
 
 
 type 
-def_aux =  (* Top-level definition *)
+def =  (* Top-level definition *)
    DEF_type of type_def (* type definition *)
  | DEF_fundef of fundef (* function definition *)
  | DEF_val of letbind (* value definition *)
  | DEF_spec of val_spec (* top-level type constraint *)
  | DEF_default of default_typing_spec (* default kind and type assumptions *)
  | DEF_scattered of scattered_def (* scattered definition *)
- | DEF_reg_dec of atyp * id (* register declaration *)
-
-
-type 
-def = 
-   DEF_aux of def_aux * l
-
-
-type 
-defs =  (* Definition sequence *)
-   Defs of (def) list
+ | DEF_reg_dec of dec_spec (* register declaration *)
 
 
 type 
@@ -421,4 +421,9 @@ and lexp =
    LEXP_aux of lexp_aux * l
 
 
+type 
+defs =  (* Definition sequence *)
+   Defs of (def) list
+
+
 
diff --git a/language/l2_parse.ott b/language/l2_parse.ott
index 2e48c264..1f365a3f 100644
--- a/language/l2_parse.ott
+++ b/language/l2_parse.ott
@@ -708,6 +708,10 @@ scattered_def :: 'SD_' ::=
   | end id  :: :: scattered_end
 {{ com scattered definition end }}
 
+dec_spec :: 'DEC_' ::=
+  {{ com Register declarations }}
+  {{ aux _ l }}
+  | register atyp id                                             :: :: reg
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Top-level definitions                                        %
@@ -715,8 +719,6 @@ scattered_def :: 'SD_' ::=
 
 def :: 'DEF_' ::=
   {{ com Top-level definition }}
-  {{ aux _ l }}
-%  {{ aux _ annot }} {{ auxparam 'a }}
   | type_def                                                    :: :: type
     {{ com type definition }}
   | fundef                                                   :: :: fundef
@@ -729,12 +731,11 @@ def :: 'DEF_' ::=
     {{ com default kind and type assumptions }}
   | scattered_def					:: :: scattered
     {{ com scattered definition }} 
-  | register atyp id                                   :: :: reg_dec
+  | dec_spec                                            :: :: reg_dec
     {{ com register declaration }}
 
 defs :: '' ::=
   {{ com Definition sequence }}
-%  {{ auxparam 'a }}
   | def1  .. defn                 :: :: Defs
 
 
@@ -1361,1062 +1362,3 @@ formula :: formula_ ::=
 %% %%   | tnvs1 = tnvs2                                                       :: :: tnvs_eq
 %% %%     {{ ichl ([[tnvs1]] = [[tnvs2]]) }}
 
-% Substitutions and freevars are not correctly generated for the OCaml ast.ml
-%substitutions
-%multiple t a :: t_subst
-%
-%freevars
-%t a :: ftv
-
-%% % 
-%% % 
-%% % defns
-%% % convert_tnvars :: '' ::=
-%% % 
-%% % defn
-%% % tnvars ~> tnvs :: :: convert_tnvars :: convert_tnvars_
-%% % by
-%% % 
-%% % :convert_tnvar: tnvar1 ~> tnv1 .. :convert_tnvar: tnvarn ~> tnvn
-%% % ------------------------------------------------------------ :: none
-%% % tnvar1 .. tnvarn  ~> tnv1 .. tnvn
-%% % 
-%% % defn
-%% % tnvar ~> tnv :: :: convert_tnvar :: convert_tnvar_
-%% % by
-%% % 
-%% % ----------------------------------------------------------- :: a
-%% % a l ~> a
-%% % 
-%% % ---------------------------------------------------------- :: N
-%% % N l ~> N
-%% % 
-%% % 
-%% % defns
-%% % look_m :: '' ::=
-%% % 
-%% % defn
-%% % E1 ( x_l1 .. x_ln ) gives E2 :: :: look_m :: look_m_ 
-%% % {{ com Name path lookup }}
-%% % by
-%% % 
-%% % ------------------------------------------------------------ :: none
-%% % E() gives E
-%% % 
-%% % E_m(x) gives E1
-%% % E1(</y_li//i/>) gives E2
-%% % ------------------------------------------------------------ :: some
-%% % <E_m,E_p,E_f,E_x>(x l </y_li//i/>) gives E2
-%% % 
-%% % defns
-%% % look_m_id :: '' ::=
-%% %  
-%% % defn
-%% % E1 ( id ) gives E2 :: :: look_m_id :: look_m_id_ 
-%% % {{ com Module identifier lookup }}
-%% % by
-%% % 
-%% % E1(</y_li//i/> x l1) gives E2
-%% % ------------------------------------------------------------ :: all
-%% % E1(</y_li.//i/> x l1 l2) gives E2
-%% % 
-%% % defns
-%% % look_tc :: '' ::=
-%% % 
-%% % defn
-%% % E ( id ) gives p :: :: look_tc :: look_tc_ 
-%% % {{ com Path identifier lookup }}
-%% % by
-%% % 
-%% % E(</y_li//i/>) gives <E_m,E_p,E_f,E_x>
-%% % E_p(x) gives p
-%% % ------------------------------------------------------------ :: all
-%% % E(</y_li.//i/> x l1 l2) gives p
-%% % 
-%% % 
-%% % defns
-%% % check_t :: '' ::=
-%% % 
-%% % defn
-%% % TD |- t ok :: :: check_t :: check_t_ 
-%% % {{ com Well-formed types }}
-%% % by
-%% % 
-%% % ------------------------------------------------------------ :: var
-%% % TD |- a ok
-%% % 
-%% % TD |- t1 ok
-%% % TD |- t2 ok
-%% % ------------------------------------------------------------ :: fn
-%% % TD |- t1 -> t2 ok
-%% % 
-%% % TD |- t1 ok .... TD |- tn ok
-%% % ------------------------------------------------------------ :: tup
-%% % TD |- t1 * .... * tn ok
-%% % 
-%% % TD(p) gives tnv1..tnvn tc_abbrev
-%% % TD,tnv1 |- t1 ok .. TD,tnvn |- tn ok
-%% % ------------------------------------------------------------ :: app
-%% % TD |- p t1 .. tn ok
-%% % 
-%% % 
-%% % defn
-%% % TD , tnv |- t ok :: :: check_tlen :: check_tlen_ 
-%% % {{ com Well-formed type/nexps matching the application type variable }}
-%% % by
-%% % 
-%% % TD |- t ok
-%% % ------------------------------------------------------------ :: t
-%% % TD,a |- t ok
-%% % 
-%% % ------------------------------------------------------------ :: len
-%% % TD,N |- ne 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
-%% % TD , E |- typ ~> t :: :: convert_typ :: convert_typ_ 
-%% % {{ com Convert source types to internal types }}
-%% % by
-%% % 
-%% % % TODO : Can't allow things like type t = _, but it's useful to have things 
-%% % % like f (x : (_, int)) = snd x
-%% % %TD |- t ok
-%% % %------------------------------------------------------------ :: wild
-%% % %TD,E |- _ l ~> t
-%% % 
-%% % ------------------------------------------------------------ :: var
-%% % TD,E |- a l' l ~> a
-%% % 
-%% % TD,E |- typ1 ~> t1
-%% % TD,E |- typ2 ~> t2
-%% % ------------------------------------------------------------ :: fn
-%% % TD,E |- typ1->typ2 l ~> t1->t2
-%% % 
-%% % TD,E |- typ1 ~> t1 .... TD,E |- typn ~> tn
-%% % ------------------------------------------------------------ :: tup
-%% % TD,E |- typ1 * .... * typn l ~> t1 * .... * tn
-%% % 
-%% % TD,E |- typ1 ~> t1 .. TD,E |- typn ~> tn
-%% % E(id) gives p
-%% % TD(p) gives a1..an tc_abbrev
-%% % ------------------------------------------------------------ :: app
-%% % TD,E |- id typ1 .. typn l ~> p t1 .. tn
-%% % 
-%% % |- nexp ~> ne
-%% % ------------------------------------------------------------ :: nexp
-%% % TD,E |- nexp ~> ne
-%% % 
-%% % TD,E |- typ ~> t
-%% % ------------------------------------------------------------ :: paren
-%% % TD,E |- (typ) l ~> t
-%% % 
-%% % 
-%% % TD,E |- typ ~> t1
-%% % TD |- t1 = t2
-%% % ------------------------------------------------------------ :: eq
-%% % TD,E |- typ ~> t2
-%% % 
-%% % 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 l : __bool
-%% % 
-%% % ------------------------------------------------------------ :: false
-%% % |- false l : __bool
-%% % 
-%% % ------------------------------------------------------------ :: num
-%% % |- num l : __num
-%% % 
-%% % nat = bitlength(hex)
-%% % ------------------------------------------------------------ :: hex
-%% % |- hex l : __vector nat __bit
-%% % 
-%% % nat = bitlength(bin)
-%% % ------------------------------------------------------------ :: bin 
-%% % |- bin l : __vector nat __bit
-%% % 
-%% % ------------------------------------------------------------ :: string
-%% % |- string l : __string
-%% % 
-%% % ------------------------------------------------------------ :: unit
-%% % |- () l : __unit
-%% % 
-%% % ------------------------------------------------------------ :: bitzero
-%% % |- bitzero l : __bit
-%% % 
-%% % ------------------------------------------------------------ :: bitone
-%% % |- bitone l : __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
-%% % TD , E , E_l1 |- pat : t gives E_l2 :: :: check_pat :: check_pat_ 
-%% % {{ com Typing patterns, building their binding environment }}
-%% % by
-%% % 
-%% % :check_pat_aux: TD,E,E_l1 |- pat_aux : t gives E_l2
-%% % ------------------------------------------------------------ :: all
-%% % TD,E,E_l1 |- pat_aux l : t gives E_l2
-%% % 
-%% % defn
-%% % TD , E , E_l1 |- pat_aux : t gives E_l2 :: :: check_pat_aux :: check_pat_aux_ 
-%% % {{ com Typing patterns, building their binding environment }}
-%% % by
-%% % 
-%% % TD |- t ok
-%% % ------------------------------------------------------------ :: wild
-%% % TD,E,E_l |- _ : t gives {}
-%% % 
-%% % TD,E,E_l1 |- pat : t gives E_l2
-%% % x NOTIN dom(E_l2)
-%% % ------------------------------------------------------------ :: as
-%% % TD,E,E_l1 |- (pat as x l) : t gives E_l2 u+ {x|->t}
-%% % 
-%% % TD,E,E_l1 |- pat : t gives E_l2
-%% % TD,E |- typ ~> t
-%% % ------------------------------------------------------------ :: typ
-%% % TD,E,E_l1 |- (pat : typ) : t gives E_l2
-%% % 
-%% % TD,E |- ctor id : (t1*..*tn) -> p t_args gives (x of names)
-%% % E_l |- id not shadowed
-%% % TD,E,E_l |- pat1 : t1 gives E_l1 .. TD,E,E_l |- patn : tn gives E_ln
-%% % disjoint doms(E_l1,..,E_ln)
-%% % ------------------------------------------------------------ :: ident_constr
-%% % TD,E,E_l |- id pat1 .. patn : p t_args gives E_l1 u+ .. u+ E_ln
-%% % 
-%% % TD |- t ok
-%% % E,E_l |- x not ctor
-%% % ------------------------------------------------------------ :: var
-%% % TD,E,E_l |- x l1 l2 : t gives {x|->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
-%% % 
-%% % 
-%% % TD,E,E_l |- pat1 : t1 gives E_l1 .... TD,E,E_l |- patn : tn gives E_ln
-%% % disjoint doms(E_l1,....,E_ln)
-%% % ------------------------------------------------------------ :: tup
-%% % TD,E,E_l |- (pat1, ...., patn) : t1 * .... * tn gives E_l1 u+ .... u+ E_ln 
-%% % 
-%% % 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/initial_check.ml b/src/initial_check.ml
index 78e44bf0..709eb42b 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -434,10 +434,10 @@ let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spe
       let k,k_typ = to_ast_base_kind bk in
       let v = to_ast_var v in
       let key = var_to_string v in
-      DT_aux(DT_kind(k,v),(l,None)),(names,(Envmap.insert k_env (key,k_typ)),t_env)
+      DT_aux(DT_kind(k,v),l),(names,(Envmap.insert k_env (key,k_typ)),t_env)
     | Parse_ast.DT_typ(typschm,id) ->
       let tps,_,_ = to_ast_typschm k_env typschm in
-      DT_aux(DT_typ(tps,to_ast_id id),(l,None)),(names,k_env,t_env) (* Does t_env need to be updated here in this pass? *)
+      DT_aux(DT_typ(tps,to_ast_id id),l),(names,k_env,t_env) (* Does t_env need to be updated here in this pass? *)
     )
 
 let to_ast_spec (names,k_env,t_env) (val_:Parse_ast.val_spec) : (tannot val_spec) envs_out =
@@ -547,7 +547,7 @@ let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) :
 
 let to_ast_funcl (names,k_env,t_env) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) =
   match fcl with
-  | Parse_ast.FCL_Funcl(id,pat,exp) -> FCL_aux(FCL_Funcl(to_ast_id id, to_ast_pat k_env pat, to_ast_exp k_env exp),(l,None))
+  | Parse_ast.FCL_Funcl(id,pat,exp) -> FCL_aux(FCL_Funcl(to_ast_id id, to_ast_pat k_env pat, to_ast_exp k_env exp),l)
 
 let to_ast_fundef  (names,k_env,t_env) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (tannot fundef) envs_out = 
   match fd with
@@ -569,92 +569,93 @@ let rec def_in_progress (id : id) (partial_defs : (id * partial_def) list) : par
     (match n,id with
     | Id_aux(Id(n),_), Id_aux(Id(i),_) -> if (n = i) then Some(pd) else def_in_progress id defs
     | _,_ -> def_in_progress id defs)
+
+let to_ast_dec (names,k_env,t_env) (Parse_ast.DEC_aux(Parse_ast.DEC_reg(typ,id),l)) =
+  let t = to_ast_typ k_env typ in
+  let id = to_ast_id id in
+  (DEC_aux(DEC_reg(t,id),(l,None)))
       
 let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * (id * partial_def) list = 
   let envs = (names,k_env,t_env) in
   match def with
-  | Parse_ast.DEF_aux(d,l) ->
-    (match d with
-    | Parse_ast.DEF_type(t_def) -> 
-      let td,envs = to_ast_typedef envs t_def in
-      ((Finished(DEF_aux(DEF_type(td),(l,None)))),envs),partial_defs
-    | Parse_ast.DEF_fundef(f_def) -> 
-      let fd,envs = to_ast_fundef envs f_def in
-      ((Finished(DEF_aux(DEF_fundef(fd),(l,None)))),envs),partial_defs
-    | Parse_ast.DEF_val(lbind) -> 
-      let lb = to_ast_letbind k_env lbind in
-      ((Finished(DEF_aux(DEF_val(lb),(l,None)))),envs),partial_defs
-    | Parse_ast.DEF_spec(val_spec) -> 
-      let vs,envs = to_ast_spec envs val_spec in
-      ((Finished(DEF_aux(DEF_spec(vs),(l,None)))),envs),partial_defs
-    | Parse_ast.DEF_default(typ_spec) -> 
-      let default,envs = to_ast_default envs typ_spec in
-      ((Finished(DEF_aux(DEF_default(default),(l,None)))),envs),partial_defs
-    | Parse_ast.DEF_reg_dec(typ,id) ->
-      let t = to_ast_typ k_env typ in
+  | Parse_ast.DEF_type(t_def) -> 
+    let td,envs = to_ast_typedef envs t_def in
+    ((Finished(DEF_type(td))),envs),partial_defs
+  | Parse_ast.DEF_fundef(f_def) -> 
+    let fd,envs = to_ast_fundef envs f_def in
+    ((Finished(DEF_fundef(fd))),envs),partial_defs
+  | Parse_ast.DEF_val(lbind) -> 
+    let lb = to_ast_letbind k_env lbind in
+    ((Finished(DEF_val(lb))),envs),partial_defs
+  | Parse_ast.DEF_spec(val_spec) -> 
+    let vs,envs = to_ast_spec envs val_spec in
+    ((Finished(DEF_spec(vs))),envs),partial_defs
+  | Parse_ast.DEF_default(typ_spec) -> 
+    let default,envs = to_ast_default envs typ_spec in
+    ((Finished(DEF_default(default))),envs),partial_defs
+  | Parse_ast.DEF_reg_dec(dec) ->
+    let d = to_ast_dec envs dec in
+    ((Finished(DEF_reg_dec(d))),envs),partial_defs
+  | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,l)) ->
+    (match sd with
+    | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
+      let rec_opt = to_ast_rec rec_opt in
+      let tannot,k_env',k_local = to_ast_tannot_opt k_env tannot_opt in
+      let effects_opt = to_ast_effects_opt k_env' effects_opt in
       let id = to_ast_id id in
-      ((Finished(DEF_aux(DEF_reg_dec(t,id),(l,None)))),envs),partial_defs (*If tracking types here, update tenv and None*)
-    | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,_)) ->
-      (match sd with
-	| Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
-	  let rec_opt = to_ast_rec rec_opt in
-	  let tannot,k_env',k_local = to_ast_tannot_opt k_env tannot_opt in
-	  let effects_opt = to_ast_effects_opt k_env' effects_opt in
-	  let id = to_ast_id id in
-	  (match (def_in_progress id partial_defs) with
-	    | None -> let partial_def = ref ((DEF_aux(DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None))),(l,None))),false) in
-                      (No_def,envs),((id,(partial_def,k_local))::partial_defs)
-	    | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None)
-	| Parse_ast.SD_scattered_funcl(funcl) -> 
-	  (match funcl with
-	    | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> 
-              let id = to_ast_id id in
-              (match (def_in_progress id partial_defs) with
-		| None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None None
-		| Some(d,k) ->
-		  (match !d with
-		    | DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),dl),false -> 
-		      let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in 
-		      d:= (DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),dl),false);
-		      (No_def,envs),partial_defs
-		    | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None
-		    | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None)))
-	| Parse_ast.SD_scattered_variant(id,naming_scheme_opt,typquant) -> 
-	  let id = to_ast_id id in
-	  let name = to_ast_namescm naming_scheme_opt in
-	  let typq, k_env',_ = to_ast_typquant k_env typquant in
-	  (match (def_in_progress id partial_defs) with
-	    | None -> let partial_def = ref ((DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None))),(l,None))),false) in
-                      (Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),{k=K_Typ}),t_env)),(id,(partial_def,k_env'))::partial_defs
-	    | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
-	| Parse_ast.SD_scattered_unioncl(id,tu) -> 
-	  let id = to_ast_id id in
-	  (match (def_in_progress id partial_defs) with
-	    | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None
-	    | Some(d,k) ->
-              (match !d with
-		| (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)),dl), false) -> 
-		  d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k tu],false),tl)),dl),false);
-		  (No_def,envs),partial_defs
-		| _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None
-		| _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None))
-	| Parse_ast.SD_scattered_end(id) ->
-	  let id = to_ast_id id in
-	  (match (def_in_progress id partial_defs) with
-	    | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None
-	    | Some(d,k) ->
-              (match !d with
-		| (DEF_aux(DEF_type(_),_) as def),false ->
-		  d:= (def,true);
-		  (No_def,envs),partial_defs
-		| (DEF_aux(DEF_fundef(_),_) as def),false ->
-		  d:= (def,true);
-		  ((Finished def), envs),partial_defs
-		| _, true -> 
-		  typ_error l "Scattered definition ended multiple times" (Some id) None None
-		| _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
-    )
-
+      (match (def_in_progress id partial_defs) with
+      | None -> let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None)))),false) in
+                (No_def,envs),((id,(partial_def,k_local))::partial_defs)
+      | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None)
+    | Parse_ast.SD_scattered_funcl(funcl) -> 
+      (match funcl with
+      | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> 
+        let id = to_ast_id id in
+        (match (def_in_progress id partial_defs) with
+	| None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None None
+	| Some(d,k) ->
+	  (match !d with
+	  | DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),false -> 
+	    let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in 
+	    d:= DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),false;
+	    (No_def,envs),partial_defs
+	  | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None
+	  | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None)))
+    | Parse_ast.SD_scattered_variant(id,naming_scheme_opt,typquant) -> 
+      let id = to_ast_id id in
+      let name = to_ast_namescm naming_scheme_opt in
+      let typq, k_env',_ = to_ast_typquant k_env typquant in
+      (match (def_in_progress id partial_defs) with
+      | None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None)))),false) in
+                (Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),{k=K_Typ}),t_env)),(id,(partial_def,k_env'))::partial_defs
+      | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
+    | Parse_ast.SD_scattered_unioncl(id,tu) -> 
+      let id = to_ast_id id in
+      (match (def_in_progress id partial_defs) with
+      | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None
+      | Some(d,k) ->
+        (match !d with
+	| DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)), false -> 
+	  d:= DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k tu],false),tl)),false;
+	  (No_def,envs),partial_defs
+	| _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None
+	| _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None))
+    | Parse_ast.SD_scattered_end(id) ->
+      let id = to_ast_id id in
+      (match (def_in_progress id partial_defs) with
+      | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None
+      | Some(d,k) ->
+        (match !d with
+	| (DEF_type(_) as def),false ->
+	  d:= (def,true);
+	  (No_def,envs),partial_defs
+	| (DEF_fundef(_) as def),false ->
+	  d:= (def,true);
+	  ((Finished def), envs),partial_defs
+	| _, true -> 
+	  typ_error l "Scattered definition ended multiple times" (Some id) None None
+	| _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
+    
 let rec to_ast_defs_helper envs partial_defs = function
   | [] -> ([],envs,partial_defs)
   | d::ds  -> let ((d', envs), partial_defs) = to_ast_def envs partial_defs d in
@@ -675,7 +676,7 @@ let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (typ_env : tan
   List.iter 
     (fun (id,(d,k)) -> 
       (match !d with
-      | (DEF_aux(_,(l,_)),false) -> typ_error l "Scattered definition never ended" (Some id) None None
+      | (d,false) -> typ_error Unknown "Scattered definition never ended" (Some id) None None
       | (_, true) -> ()))
     partial_defs;
   (Defs defs),k_env
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 8e842730..64727503 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -122,7 +122,7 @@ val to_register_fields : defs tannot -> list (id * list (id * index_range))
 let rec to_register_fields (Defs defs) = 
   match defs with
   | [ ] -> [ ]
-  | (DEF_aux def (l,tannot))::defs -> 
+  | def::defs -> 
     match def with 
     | DEF_type (TD_aux (TD_register id n1 n2 indexes) l') ->
       (id,List.map (fun (a,b) -> (b,a)) indexes)::(to_register_fields (Defs defs))
@@ -134,9 +134,9 @@ val to_registers : defs tannot -> env
 let rec to_registers (Defs defs) = 
   match defs with
   | [ ] -> [ ]
-  | (DEF_aux def (l,tannot))::defs -> 
+  | def::defs -> 
     match def with 
-    | DEF_reg_dec typ id -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs))
+    | DEF_reg_dec (DEC_aux (DEC_reg typ id) (l,tannot)) -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs))
     | _ -> to_registers (Defs defs)
     end 
   end
@@ -164,7 +164,7 @@ val to_data_constructors : defs tannot -> list (id * typ)
 let rec to_data_constructors (Defs defs) =
   match defs with
   | [] -> []
-  | (DEF_aux def _) :: defs ->
+  | def :: defs ->
     match def with
     | DEF_type (TD_aux t _)->
       match t with 
@@ -426,7 +426,7 @@ let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
 let rec find_function (Defs defs) id =
   match defs with 
   | [] -> Nothing
-  | (DEF_aux def _)::defs -> 
+  | def::defs -> 
     match def with
     | DEF_fundef f -> match get_funcls id f with
       | [] -> find_function (Defs defs) id
@@ -1273,13 +1273,13 @@ let rec to_global_letbinds (Defs defs) t_level =
   let  (Env defs' lets regs ctors subregs) = t_level in
   match defs with
   | [] -> ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, emem, []),t_level)
-  | (DEF_aux def (l,_))::defs ->
+  | def::defs ->
     match def with
     | DEF_val lbind ->
       match interp_letbind t_level [] emem lbind with
       | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs)
       | ((Action a s,lm,le),_) -> 
-	((Error l "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
+	((Error Unknown "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
       | (e,_) -> (e,t_level) end
     | _ -> to_global_letbinds (Defs defs) t_level
     end
diff --git a/src/parser.mly b/src/parser.mly
index 60f50737..06b26765 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -80,7 +80,7 @@ let tdloc td = TD_aux(td, loc())
 let funloc fn = FD_aux(fn, loc())
 let vloc v = VS_aux(v, loc ())
 let sdloc sd = SD_aux(sd, loc ())
-let dloc d = DEF_aux(d,loc ())
+let dloc d = d
 
 let mk_typschm tq t s e = TypSchm_aux((TypSchm_ts(tq,t)),(locn s e))
 let mk_rec i = (Rec_aux((Rec_rec), locn i i))
@@ -1138,7 +1138,7 @@ def:
   | default_typ
     { dloc (DEF_default($1)) }
   | Register atomic_typ id
-    { dloc (DEF_reg_dec($2,$3)) }
+    { dloc (DEF_reg_dec(DEC_aux(DEC_reg($2,$3),loc ()))) }
   | Scattered scattered_def
     { dloc (DEF_scattered $2) }
   | Function_ Clause funcl
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 153147d3..5f86b2ed 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -346,15 +346,18 @@ let pp_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   fprintf ppf "@[<0>%a %a%a%a @[<1>%a@] @[<1>%a@] @]@\n"
     kwd "function" pp_rec r pp_tannot_opt typa pp_effects_opt efa pp_funcl (List.hd fcls) (list_pp pp_funcls pp_funcls) (List.tl fcls)
 
-let pp_def ppf (DEF_aux(d,(l,_))) =
+let pp_dec ppf (DEC_aux(DEC_reg(typ,id),_)) =
+  fprintf ppf "@[<0>register %a %a@]@\n" pp_typ typ pp_id id
+
+let pp_def ppf d =
   match d with
   | DEF_default(df) -> pp_default ppf df
   | DEF_spec(v_spec) -> pp_spec ppf v_spec
   | DEF_type(t_def) -> pp_typdef ppf t_def
   | DEF_fundef(f_def) -> pp_fundef ppf f_def
   | DEF_val(lbind) -> fprintf ppf "@[<0>%a@]@\n" pp_let lbind
-  | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "register" pp_typ typ pp_id id
-  | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs")
+  | DEF_reg_dec(dec) -> pp_dec ppf dec
+  | _ -> raise (Reporting_basic.err_unreachable Unknown "initial_check didn't remove all scattered Defs")
 
 let pp_defs ppf (Defs(defs)) =
   fprintf ppf "@[%a@]@\n" (list_pp pp_def pp_def) defs
@@ -712,13 +715,13 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) =
   in
   fprintf ppf "@[(LEXP_aux %a (%a, %a))@]" print_le lexp pp_lem_l l pp_annot annot
 
-let pp_lem_default ppf (DT_aux(df,(l,annot))) =
+let pp_lem_default ppf (DT_aux(df,l)) =
   let print_de ppf df =
     match df with
       | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var
       | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
   in
-  fprintf ppf "@[<0>(DT_aux %a (%a, %a))@]" print_de df pp_lem_l l pp_annot annot
+  fprintf ppf "@[<0>(DT_aux %a %a)@]" print_de df pp_lem_l l
 
 let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
   let print_spec ppf v =
@@ -786,9 +789,9 @@ let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) =
   | Effect_opt_pure -> fprintf ppf "(Effect_opt_aux Effect_opt_pure %a)" pp_lem_l l
   | Effect_opt_effect e -> fprintf ppf "(Effect_opt_aux (Effect_opt_effect %a) %a)" pp_lem_effects e pp_lem_l l
 
-let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),(l,annot))) =
-  fprintf ppf "@[<0>(FCL_aux (%a %a %a %a) (%a, %a))@]@\n" 
-    kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot
+let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),l)) =
+  fprintf ppf "@[<0>(FCL_aux (%a %a %a %a) %a)@]@\n" 
+    kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp pp_lem_l l
 
 let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) =
   let pp_funcls ppf funcl = fprintf ppf "%a %a" pp_lem_funcl funcl kwd ";" in
@@ -796,18 +799,18 @@ let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) =
     kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls
     pp_lem_l l pp_annot annot
 
-let pp_lem_def ppf (DEF_aux(d,(l,annot))) =
-  let print_d ppf d = 
-    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)@]" 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")
-  in
-  fprintf ppf "@[<0>(DEF_aux %a (%a, %a))@];@\n" print_d d pp_lem_l l pp_annot annot
+let pp_lem_dec ppf (DEC_aux(DEC_reg(typ,id),(l,annot))) =
+  fprintf ppf "@[<0>(DEC_aux (DEC_reg %a %a) (%a,%a))@]" pp_lem_typ typ pp_lem_id id pp_lem_l l pp_annot annot
+
+let pp_lem_def ppf d =
+  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(dec) -> fprintf ppf "(DEF_reg_dec %a);" pp_lem_dec dec
+  | _ -> raise (Reporting_basic.err_unreachable Unknown "initial_check didn't remove all scattered Defs")
 
 let pp_lem_defs ppf (Defs(defs)) =
   fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs
diff --git a/src/type_check.ml b/src/type_check.ml
index be944d31..2bb5700d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1208,13 +1208,13 @@ let check_val_spec envs (VS_aux(vs,(l,annot))) =
       (VS_aux(vs,(l,tannot)),
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
 
-let check_default envs (DT_aux(ds,(l,annot))) =
+let check_default envs (DT_aux(ds,l)) =
   let (Env(d_env,t_env)) = envs in
   match ds with
-    | DT_kind _ -> ((DT_aux(ds,(l,annot))),envs)
+    | DT_kind _ -> ((DT_aux(ds,l)),envs)
     | DT_typ(typs,id) ->
       let tannot = typschm_to_tannot envs typs Default in
-      (DT_aux(ds,(l,tannot)),
+      (DT_aux(ds,l),
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
 
 let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,annot))) =
@@ -1224,7 +1224,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
               | Rec_aux(Rec_nonrec,_) -> false
 	      | Rec_aux(Rec_rec,_) -> true in
   let Some(id) = List.fold_right 
-    (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) id' ->
+    (fun (FCL_aux((FCL_Funcl(id,pat,exp)),l)) id' ->
       match id' with
 	| Some(id') -> if id' = id_to_string id then Some(id') 
 	  else typ_error l ("Function declaration expects all definitions to have the same name, " 
@@ -1241,13 +1241,13 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       t,p_t,Some((ids,{t=Tfn(p_t,t,ef)}),Emp_global,constraints,ef) in
   let check t_env =
     List.split
-      (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) ->
+      (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),l)) ->
 	let (pat',t_env',constraints',t') = check_pattern (Env(d_env,t_env)) Emp_local param_t pat in
         (*let _ = Printf.printf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*)
 	let exp',_,_,constraints,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env t_env')) ret_t exp in
         (*let _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) 
 	(*let _ = (Pretty_print.pp_exp Format.std_formatter) exp' in*)
-	(FCL_aux((FCL_Funcl(id,pat',exp')),(l,tannot)),((constraints'@constraints),ef))) funcls) in
+	(FCL_aux((FCL_Funcl(id,pat',exp')),l),((constraints'@constraints),ef))) funcls) in
   match (in_env,tannot) with
     | Some(Some( (params,u),Spec,constraints,eft)), Some( (p',t),_,c',eft') ->
       (*let _ = Printf.printf "Function %s is in env\n" id in*)
@@ -1270,24 +1270,24 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)))
 
 (*val check_def : envs -> tannot def -> (tannot def) envs_out*)
-let check_def envs (DEF_aux(def,(l,annot))) = 
+let check_def envs def = 
   let (Env(d_env,t_env)) = envs in
   match def with
-    | DEF_type tdef -> let td,envs = check_type_def envs tdef in
-		       (DEF_aux((DEF_type td),(l,annot)),envs)
-    | DEF_fundef fdef -> let fd,envs = check_fundef envs fdef in
-			 (DEF_aux(DEF_fundef(fd),(l,annot)),envs)
-    | DEF_val letdef -> let (letbind,t_env_let,_,eft) = check_lbind envs true Emp_global letdef in
-                        (DEF_aux(DEF_val letbind,(l,annot)),Env(d_env,Envmap.union t_env t_env_let))
-    | DEF_spec spec -> let vs,envs = check_val_spec envs spec in
-		       (DEF_aux(DEF_spec(vs),(l,annot)),envs)
-    | DEF_default default -> let ds,envs = check_default envs default in
-			     (DEF_aux((DEF_default(ds)),(l,annot)),envs)
-    | DEF_reg_dec(typ,id) -> 
-      let t = (typ_to_t typ) in
-      let i = id_to_string id in
-      let tannot = into_register d_env (Some(([],t),External (Some i),[],pure_e)) in
-      (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env (i,tannot))))
+  | DEF_type tdef -> let td,envs = check_type_def envs tdef in
+		     (DEF_type td,envs)
+  | DEF_fundef fdef -> let fd,envs = check_fundef envs fdef in
+		       (DEF_fundef fd,envs)
+  | DEF_val letdef -> let (letbind,t_env_let,_,eft) = check_lbind envs true Emp_global letdef in
+                      (DEF_val letbind,Env(d_env,Envmap.union t_env t_env_let))
+  | DEF_spec spec -> let vs,envs = check_val_spec envs spec in
+		     (DEF_spec vs, envs)
+  | DEF_default default -> let ds,envs = check_default envs default in
+			   (DEF_default ds,envs)
+  | DEF_reg_dec(DEC_aux(DEC_reg(typ,id), (l,annot))) -> 
+    let t = (typ_to_t typ) in
+    let i = id_to_string id in
+    let tannot = into_register d_env (Some(([],t),External (Some i),[],pure_e)) in
+    (DEF_reg_dec(DEC_aux(DEC_reg(typ,id),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot))))
 
 
 (*val check : envs ->  tannot defs -> tannot defs*)