Merge branch 'interp_typed'

Conflicts:
	src/lem_interp/interp.lem
	src/lem_interp/run_interp.ml

16 files changed, 1721 insertions, 1029 deletions

diff --git a/language/Makefile b/language/Makefile
index d650f957..2076069c 100644
--- a/language/Makefile
+++ b/language/Makefile
@@ -9,7 +9,7 @@ all: l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem
 %Theory.uo: %Script.sml
 	Holmake --qof -I $(OTTLIB) $@
 
-l2.tex: l2.ott l2_rules.ott
+l2.tex: l2.ott l2_typ.ott l2_rules.ott
 	ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^
 
 %.tex: %.ott
@@ -21,12 +21,8 @@ l2.tex: l2.ott l2_rules.ott
 %Script.sml: %.ott
 	ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^
 
-%.lem: %.ott
-	# work 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.
-	ott -sort false -generate_aux_rules false -o $@ -picky_multiple_parses true $^
+l2.lem: l2.ott l2_typ.ott
+	ott -sort false -generate_aux_rules true -o $@ -picky_multiple_parses true $^
 
 clean:
 	rm -rf *~
diff --git a/language/l2.lem b/language/l2.lem
index 630c976d..30027846 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -1,4 +1,4 @@
-(* generated by Ott 0.23 from: l2.ott *)
+(* generated by Ott 0.24 from: l2_typ.ott l2.ott *)
 open import Pervasives
 
 open import Map
@@ -8,7 +8,9 @@ open import Set_extra
 type l =
   | Unknown
   | Trans of string * maybe l
-  | Range of nat * nat
+  | Range of string * nat * nat * nat * nat
+
+type annot 'a = l * 'a
 
 val duplicates : forall 'a. list 'a -> list 'a
 
@@ -20,30 +22,45 @@ val subst : forall 'a. list 'a -> list 'a -> bool
 type x = string (* identifier *)
 type ix = string (* infix identifier *)
 
-type kid =  (* variables with kind, ticked to differntiate from program variables *)
- | Var of x
-
-
-type base_kind =  (* base kind *)
+type base_kind_aux =  (* base kind *)
  | BK_type (* kind of types *)
  | BK_nat (* kind of natural number size expressions *)
  | BK_order (* kind of vector order specifications *)
  | BK_effect (* kind of effect sets *)
 
 
-type nexp =  (* expression of kind Nat, for vector sizes and origins *)
+type base_kind = 
+ | BK_aux of base_kind_aux * l
+
+
+type kid_aux =  (* variables with kind, ticked to differntiate from program variables *)
+ | Var of x
+
+
+type kind_aux =  (* kinds *)
+ | K_kind of list base_kind
+
+
+type kid = 
+ | Kid_aux of kid_aux * l
+
+
+type kind = 
+ | K_aux of kind_aux * l
+
+
+type nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
  | Nexp_var of kid (* variable *)
  | Nexp_constant of natural (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
  | Nexp_exp of nexp (* exponential *)
 
-
-type kind =  (* kinds *)
- | K_kind of list base_kind
+and nexp = 
+ | Nexp_aux of nexp_aux * l
 
 
-type base_effect =  (* effect *)
+type base_effect_aux =  (* effect *)
  | BE_rreg (* read register *)
  | BE_wreg (* write register *)
  | BE_rmem (* read memory *)
@@ -53,45 +70,78 @@ type base_effect =  (* effect *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
 
 
-type order =  (* vector order specifications, of kind Order *)
+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 *)
+
+
+type order_aux =  (* vector order specifications, of kind Order *)
  | Ord_var of kid (* variable *)
  | Ord_inc (* increasing (little-endian) *)
  | Ord_dec (* decreasing (big-endian) *)
 
 
-type effect =  (* effect set, of kind Effects *)
- | Effect_var of kid
- | Effect_set of list base_effect (* effect set *)
+type id = 
+ | Id_aux of id_aux * l
 
 
-type id =  (* Identifier *)
- | Id of x
- | DeIid of x (* remove infix status *)
+type effect = 
+ | Effect_aux of effect_aux * l
+
+
+type order = 
+ | Ord_aux of order_aux * l
 
 let effect_union e1 e2 = 
   match (e1,e2) with
-  | (Effect_set els,Effect_set els2) -> Effect_set (els++els2)
+  | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l
   end
 
 
-type n_constraint =  (* constraint over kind $Nat$ *)
+type kinded_id_aux =  (* optionally kind-annotated identifier *)
+ | KOpt_none of kid (* identifier *)
+ | KOpt_kind of kind * kid (* kind-annotated variable *)
+
+
+type n_constraint_aux =  (* constraint over kind $Nat$ *)
  | NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
  | NC_bounded_le of nexp * nexp
  | NC_nat_set_bounded of kid * list natural
 
 
-type kinded_id =  (* optionally kind-annotated identifier *)
- | KOpt_none of kid (* identifier *)
- | KOpt_kind of kind * kid (* kind-annotated variable *)
+type kinded_id = 
+ | KOpt_aux of kinded_id_aux * l
+
+
+type n_constraint = 
+ | NC_aux of n_constraint_aux * l
 
 
-type quant_item =  (* Either a kinded identifier or a nexp constraint for a typquant *)
+type quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
  | QI_id of kinded_id (* An optionally kinded identifier *)
  | QI_const of n_constraint (* A constraint for this type *)
 
 
-type lit =  (* Literal constant *)
+type quant_item = 
+ | QI_aux of quant_item_aux * l
+
+
+type typquant_aux =  (* type quantifiers and constraints *)
+ | TypQ_tq of list quant_item
+ | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+
+type lit_aux =  (* Literal constant *)
  | L_unit (* $() : unit$ *)
  | L_zero (* $bitzero : bit$ *)
  | L_one (* $bitone : bit$ *)
@@ -104,7 +154,7 @@ type lit =  (* Literal constant *)
  | L_string of string (* string constant *)
 
 
-type typ =  (* Type expressions, of kind $Type$ *)
+type typ_aux =  (* Type expressions, of kind $Type$ *)
  | Typ_wild (* Unspecified type *)
  | Typ_id of id (* Defined type *)
  | Typ_var of kid (* Type variable *)
@@ -112,164 +162,390 @@ type typ =  (* Type expressions, of kind $Type$ *)
  | Typ_tup of list typ (* Tuple type *)
  | Typ_app of id * list typ_arg (* type constructor application *)
 
-and typ_arg =  (* Type constructor arguments of all kinds *)
+and typ = 
+ | Typ_aux of typ_aux * l
+
+and typ_arg_aux =  (* Type constructor arguments of all kinds *)
  | Typ_arg_nexp of nexp
  | Typ_arg_typ of typ
  | Typ_arg_order of order
  | Typ_arg_effect of effect
 
+and typ_arg = 
+ | Typ_arg_aux of typ_arg_aux * l
 
-type typquant =  (* type quantifiers and constraints *)
- | TypQ_tq of list quant_item
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
+
+type typquant = 
+ | TypQ_aux of typquant_aux * l
+
+
+type lit = 
+ | L_aux of lit_aux * l
 
 
-type pat =  (* Pattern *)
+type typschm_aux =  (* type scheme *)
+ | TypSchm_ts of typquant * typ
+
+
+type pat_aux 'a =  (* Pattern *)
  | P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
- | P_as of pat * id (* named pattern *)
- | P_typ of typ * pat (* typed pattern *)
+ | P_as of (pat 'a) * id (* named pattern *)
+ | P_typ of typ * (pat 'a) (* typed pattern *)
  | P_id of id (* identifier *)
- | P_app of id * list pat (* union constructor pattern *)
- | P_record of list fpat * bool (* struct pattern *)
- | P_vector of list pat (* vector pattern *)
- | P_vector_indexed of list (natural * pat) (* vector pattern (with explicit indices) *)
- | P_vector_concat of list pat (* concatenated vector pattern *)
- | P_tup of list pat (* tuple pattern *)
- | P_list of list pat (* list pattern *)
+ | P_app of id * list (pat 'a) (* union constructor pattern *)
+ | P_record of list (fpat 'a) * bool (* struct pattern *)
+ | P_vector of list (pat 'a) (* vector pattern *)
+ | P_vector_indexed of list (natural * (pat 'a)) (* vector pattern (with explicit indices) *)
+ | P_vector_concat of list (pat 'a) (* concatenated vector pattern *)
+ | P_tup of list (pat 'a) (* tuple pattern *)
+ | P_list of list (pat 'a) (* list pattern *)
 
-and fpat =  (* Field pattern *)
- | FP_Fpat of id * pat
+and pat 'a = 
+ | P_aux of (pat_aux 'a) * annot 'a
 
+and fpat_aux 'a =  (* Field pattern *)
+ | FP_Fpat of id * (pat 'a)
 
-type typschm =  (* type scheme *)
- | TypSchm_ts of typquant * typ
+and fpat 'a = 
+ | FP_aux of (fpat_aux 'a) * annot 'a
 
 
-type exp =  (* Expression *)
- | E_block of list exp (* block (parsing conflict with structs?) *)
+type typschm = 
+ | TypSchm_aux of typschm_aux * l
+
+
+type exp_aux 'a =  (* Expression *)
+ | E_block of list (exp 'a) (* block (parsing conflict with structs?) *)
  | E_id of id (* identifier *)
  | E_lit of lit (* literal constant *)
- | E_cast of typ * exp (* cast *)
- | E_app of id * list exp (* function application *)
- | E_app_infix of exp * id * exp (* infix function application *)
- | E_tuple of list exp (* tuple *)
- | E_if of exp * exp * exp (* conditional *)
- | E_for of id * exp * exp * exp * order * exp (* loop *)
- | E_vector of list exp (* vector (indexed from 0) *)
- | E_vector_indexed of list (natural * exp) (* vector (indexed consecutively) *)
- | E_vector_access of exp * exp (* vector access *)
- | E_vector_subrange of exp * exp * exp (* subvector extraction *)
- | E_vector_update of exp * exp * exp (* vector functional update *)
- | E_vector_update_subrange of exp * exp * exp * exp (* vector subrange update (with vector) *)
- | E_list of list exp (* list *)
- | E_cons of exp * exp (* cons *)
- | E_record of fexps (* struct *)
- | E_record_update of exp * fexps (* functional update of struct *)
- | E_field of exp * id (* field projection from struct *)
- | E_case of exp * list pexp (* pattern matching *)
- | E_let of letbind * exp (* let expression *)
- | E_assign of lexp * exp (* imperative assignment *)
-
-and lexp =  (* lvalue expression *)
+ | E_cast of typ * (exp 'a) (* cast *)
+ | E_app of id * list (exp 'a) (* function application *)
+ | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *)
+ | E_tuple of list (exp 'a) (* tuple *)
+ | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *)
+ | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *)
+ | E_vector of list (exp 'a) (* vector (indexed from 0) *)
+ | E_vector_indexed of list (natural * (exp 'a)) (* vector (indexed consecutively) *)
+ | E_vector_access of (exp 'a) * (exp 'a) (* vector access *)
+ | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *)
+ | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *)
+ | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *)
+ | E_list of list (exp 'a) (* list *)
+ | E_cons of (exp 'a) * (exp 'a) (* cons *)
+ | E_record of (fexps 'a) (* struct *)
+ | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *)
+ | E_field of (exp 'a) * id (* field projection from struct *)
+ | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *)
+ | E_let of (letbind 'a) * (exp 'a) (* let expression *)
+ | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *)
+
+and exp 'a = 
+ | E_aux of (exp_aux 'a) * annot 'a
+
+and lexp_aux 'a =  (* lvalue expression *)
  | LEXP_id of id (* identifier *)
- | LEXP_memory of id * list exp (* memory write via function call *)
- | LEXP_vector of lexp * exp (* vector element *)
- | LEXP_vector_range of lexp * exp * exp (* subvector *)
- | LEXP_field of lexp * id (* struct field *)
+ | LEXP_memory of id * list (exp 'a) (* memory write via function call *)
+ | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *)
+ | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *)
+ | LEXP_field of (lexp 'a) * id (* struct field *)
 
-and fexp =  (* Field-expression *)
- | FE_Fexp of id * exp
+and lexp 'a = 
+ | LEXP_aux of (lexp_aux 'a) * annot 'a
 
-and fexps =  (* Field-expression list *)
- | FES_Fexps of list fexp * bool
+and fexp_aux 'a =  (* Field-expression *)
+ | FE_Fexp of id * (exp 'a)
 
-and pexp =  (* Pattern match *)
- | Pat_exp of pat * exp
+and fexp 'a = 
+ | FE_aux of (fexp_aux 'a) * annot 'a
 
-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) *)
+and fexps_aux 'a =  (* Field-expression list *)
+ | FES_Fexps of list (fexp 'a) * bool
 
+and fexps 'a = 
+ | FES_aux of (fexps_aux 'a) * annot 'a
 
-type type_union =  (* Type union constructors *)
- | Tu_id of id
- | Tu_ty_id of typ * id
+and pexp_aux 'a =  (* Pattern match *)
+ | Pat_exp of (pat 'a) * (exp 'a)
+
+and pexp 'a = 
+ | Pat_aux of (pexp_aux 'a) * annot 'a
 
+and letbind_aux 'a =  (* Let binding *)
+ | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *)
+ | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)
 
-type funcl =  (* Function clause *)
- | FCL_Funcl of id * pat * exp
+and letbind 'a = 
+ | LB_aux of (letbind_aux 'a) * annot 'a
 
 
-type effect_opt =  (* Optional effect annotation for functions *)
+type effect_opt_aux =  (* Optional effect annotation for functions *)
  | Effect_opt_pure (* sugar for empty effect set *)
  | Effect_opt_effect of effect
 
 
-type name_scm_opt =  (* Optional variable-naming-scheme specification for variables of defined type *)
+type rec_opt_aux =  (* Optional recursive annotation for functions *)
+ | Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
+
+
+type funcl_aux 'a =  (* Function clause *)
+ | FCL_Funcl of id * (pat 'a) * (exp 'a)
+
+
+type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
  | Name_sect_none
  | Name_sect_some of string
 
 
-type rec_opt =  (* Optional recursive annotation for functions *)
- | Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
+type type_union_aux =  (* Type union constructors *)
+ | Tu_id of id
+ | Tu_ty_id of typ * id
 
 
-type tannot_opt =  (* Optional type annotation for functions *)
+type tannot_opt_aux =  (* Optional type annotation for functions *)
  | Typ_annot_opt_some of typquant * typ
 
 
-type index_range =  (* index specification, for bitfields in register types *)
+type effect_opt = 
+ | Effect_opt_aux of effect_opt_aux * l
+
+
+type rec_opt = 
+ | Rec_aux of rec_opt_aux * l
+
+
+type funcl 'a = 
+ | FCL_aux of (funcl_aux 'a) * annot 'a
+
+
+type name_scm_opt = 
+ | Name_sect_aux of name_scm_opt_aux * l
+
+
+type type_union = 
+ | Tu_aux of type_union_aux * l
+
+
+type tannot_opt = 
+ | Typ_annot_opt_aux of tannot_opt_aux * l
+
+
+type index_range_aux =  (* index specification, for bitfields in register types *)
  | BF_single of natural (* single index *)
  | BF_range of natural * natural (* index range *)
  | BF_concat of index_range * index_range (* concatenation of index ranges *)
 
-
-type val_spec =  (* Value type specification *)
- | VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
+and index_range = 
+ | BF_aux of index_range_aux * l
 
 
-type scattered_def =  (* Function and type union definitions that can be spread across
+type scattered_def_aux 'a =  (* Function and type union definitions that can be spread across
          a file. Each one must end in $id$ *)
  | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
- | SD_scattered_funcl of funcl (* scattered function definition clause *)
+ | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *)
  | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
  | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
  | SD_scattered_end of id (* scattered definition end *)
 
 
-type fundef =  (* Function definition *)
- | FD_function of rec_opt * tannot_opt * effect_opt * list funcl
+type type_def_aux 'a =  (* Type definition body *)
+ | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
+ | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
+ | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
+ | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
+
+
+type fundef_aux 'a =  (* Function definition *)
+ | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
 
 
-type default_spec =  (* Default kinding or typing assumption *)
+type default_spec_aux 'a =  (* Default kinding or typing assumption *)
  | DT_kind of base_kind * kid
  | DT_typ of typschm * id
 
 
-type type_def =  (* Type definition body *)
- | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
- | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
- | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
- | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
+type val_spec_aux 'a =  (* Value type specification *)
+ | VS_val_spec of typschm * id
+ | VS_extern_no_rename of typschm * id
+ | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
+
+
+type scattered_def 'a = 
+ | SD_aux of (scattered_def_aux 'a) * annot 'a
 
 
-type 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_spec (* default kind and type assumptions *)
- | DEF_scattered of scattered_def (* scattered function and type definition *)
+type type_def 'a = 
+ | TD_aux of (type_def_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
+
+
+type val_spec 'a = 
+ | VS_aux of (val_spec_aux 'a) * annot 'a
+
+
+type def_aux '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 defs =  (* Definition sequence *)
- | Defs of list def
+type def 'a = 
+ | DEF_aux of (def_aux 'a) * annot 'a
+
+
+type defs 'a =  (* Definition sequence *)
+ | Defs of list (def 'a)
+
+
+let rec remove_one i l =
+  match l with
+  | [] -> []
+  | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2)
+end
+
+let rec remove_from l l2 =
+  match l2 with 
+  | [] -> l
+  | i::l2' -> remove_from (remove_one i l) l2'
+end
+
+let disjoint s1 s2 = Set.null (s1 inter s2)
+
+let rec disjoint_all sets =
+  match sets with
+  | [] -> true
+  | s1::[] -> true
+  | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets))
+end
+
+
+type k =  (* Internal kinds *)
+ | Ki_typ
+ | Ki_nat
+ | Ki_ord
+ | Ki_efct
+ | Ki_ctor of list k * k
+ | Ki_infer (* Representing an unknown kind, inferred by context *)
+
+
+type ne =  (* internal numeric expressions *)
+ | Ne_var of kid
+ | Ne_const of natural
+ | Ne_mult of ne * ne
+ | Ne_add of list ne
+ | Ne_exp of ne
+ | Ne_unary of ne
+
+
+type kinf =  (* Whether a kind is default or from a local binding *)
+ | Kinf_k of k
+ | Kinf_def of k
+
+
+type tid =  (* A type identifier or type variable *)
+ | Tid_id of id
+ | Tid_var of kid
+
+
+type nec =  (* Numeric expression constraints *)
+ | Nec_lteq of ne * ne
+ | Nec_eq of ne * ne
+ | Nec_gteq of ne * ne
+ | Nec_in of kid * list natural
+
+
+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 id
+ | T_var of kid
+ | T_fn of t * t * effect
+ | T_tup of list t
+ | T_app of id * t_args
+
+and t_arg =  (* Argument to type constructors *)
+ | T_arg_typ of t
+ | T_arg_nexp of ne
+ | T_arg_effect of effect
+ | T_arg_order of order
+
+and t_args =  (* Arguments to type constructors *)
+ | T_args of list t_arg
+
+
+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
+
+ type definition_env =
+   | DenvEmp
+   | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id)))
+
+
+let blength (bit) = Ne_const 8
+let hlength (bit) = Ne_const 8
+
+ type env =
+   | EnvEmp 
+   | Env of (map id tinf) * definition_env
+
+ type inf = 
+   | Iemp
+   | Inf of (list nec) * effect
+
+ val denv_union : definition_env -> definition_env -> definition_env
+ let denv_union de1 de2 = 
+  match (de1,de2) with
+   | (DenvEmp,de2) -> de2
+   | (de1,DenvEmp) -> de1
+   | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) ->
+      Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2)
+   end
+
+ val env_union : env -> env -> env
+ let env_union e1 e2 =
+   match (e1,e2) with
+    | (EnvEmp,e2) -> e2
+    | (e1,EnvEmp) -> e1
+    | ((Env te1 de1),(Env te2 de2)) ->
+      Env (te1 union te2) (denv_union de1 de2)
+ end
+
+let inf_union i1 i2 =
+  match (i1,i2) with 
+ | (Iemp,i2) -> i2
+ | (i1,Iemp) -> i1
+ | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2))
+ end
+
+let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*)
+
+
+
+type I = inf
+
+
+type E = env
 
 
 
diff --git a/language/l2.ml b/language/l2.ml
index b01a25ac..1c2a6c09 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -1,4 +1,4 @@
-(* generated by Ott 0.23 from: l2.ott *)
+(* generated by Ott 0.24 from: l2.ott *)
 
 
 type text = string
@@ -294,13 +294,13 @@ and 'a lexp_aux =  (* lvalue expression *)
 
 
 type 
-'a effect_opt_aux =  (* Optional effect annotation for functions *)
+effect_opt_aux =  (* Optional effect annotation for functions *)
    Effect_opt_pure (* sugar for empty effect set *)
  | Effect_opt_effect of effect
 
 
 type 
-'a tannot_opt_aux =  (* Optional type annotation for functions *)
+tannot_opt_aux =  (* Optional type annotation for functions *)
    Typ_annot_opt_some of typquant * typ
 
 
@@ -328,13 +328,13 @@ type_union_aux =  (* Type union constructors *)
 
 
 type 
-'a effect_opt = 
-   Effect_opt_aux of 'a effect_opt_aux * 'a annot
+effect_opt = 
+   Effect_opt_aux of effect_opt_aux * l
 
 
 type 
-'a tannot_opt = 
-   Typ_annot_opt_aux of 'a tannot_opt_aux * 'a annot
+tannot_opt = 
+   Typ_annot_opt_aux of tannot_opt_aux * l
 
 
 type 
@@ -369,13 +369,13 @@ and index_range =
 
 type 
 'a fundef_aux =  (* Function definition *)
-   FD_function of rec_opt * 'a tannot_opt * 'a effect_opt * ('a funcl) list
+   FD_function of rec_opt * tannot_opt * effect_opt * ('a funcl) list
 
 
 type 
 'a 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 * 'a tannot_opt * 'a effect_opt * id (* scattered function definition header *)
+   SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
  | SD_scattered_funcl of 'a funcl (* scattered function definition clause *)
  | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
  | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
diff --git a/language/l2.ott b/language/l2.ott
index 8cbacf0d..aa981cc7 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -58,7 +58,9 @@ open import Set_extra
 type l =
   | Unknown
   | Trans of string * maybe l
-  | Range of nat * nat
+  | Range of string * nat * nat * nat * nat
+
+type annot 'a = l * 'a
 
 val duplicates : forall 'a. list 'a -> list 'a
 
@@ -102,7 +104,7 @@ l :: '' ::=                                     {{ phantom }}
 annot :: '' ::=
                                                 {{ phantom }}
                                                 {{ ocaml 'a annot }}
-                                                {{ lem annot }}
+                                                {{ lem annot 'a }}
                                                 {{ hol unit }}
 
 id :: '' ::=
@@ -195,13 +197,13 @@ effect :: 'Effect_' ::=
  | pure                                 :: M :: pure {{ com sugar for empty effect set }} 
    {{ lem (Effect_set [])  }} {{icho [[{}]] }}
  | effect1 u+ .. u+ effectn                   :: M :: union {{ com meta operation for combining sets of effects }} {{ icho [] }}
-   {{ lem (List.foldr effect_union (Effect_set []) [[effect1..effectn]]) }}
+   {{ lem (List.foldr effect_union (Effect_aux (Effect_set []) Unknown) [[effect1..effectn]]) }}
 
 embed
 {{ lem
 let effect_union e1 e2 = 
   match (e1,e2) with
-  | (Effect_set els,Effect_set els2) -> Effect_set (els++els2)
+  | ((Effect_aux (Effect_set els) _),(Effect_aux (Effect_set els2) l)) -> Effect_aux (Effect_set (els++els2)) l
   end
 }}
 
@@ -727,7 +729,7 @@ grammar
 
 tannot_opt :: 'Typ_annot_opt_' ::=
   {{ com Optional type annotation for functions}}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ aux _ l }} 
 %  |                                             :: :: none
 % Currently not optional; one issue, do the type parameters apply over the argument types, or should this be the type of the function and not just the return
   | typquant typ                                :: :: some 
@@ -740,7 +742,7 @@ rec_opt :: 'Rec_' ::=
 
 effect_opt :: 'Effect_opt_' ::=
   {{ com Optional effect annotation for functions }}
-  {{ aux _ annot }} {{ auxparam 'a }}
+  {{ aux _ l }}
   |                                             :: :: pure {{ com sugar for empty effect set }}
   | effectkw effect                              :: :: effect
 
@@ -837,6 +839,8 @@ defs :: '' ::=
   | def1  .. defn                 :: :: Defs
 
 
+
+
 terminals :: '' ::=
   | **                                  :: :: starstar
     {{ tex \ensuremath{\mathop{\mathord{*}\mathord{*} } } }}
diff --git a/language/l2_rules.ott b/language/l2_rules.ott
index 7e3efcb7..3bade9d4 100644
--- a/language/l2_rules.ott
+++ b/language/l2_rules.ott
@@ -1,323 +1,5 @@
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% Machinery for typing rules                                   %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-embed
-{{ lem
-
-let rec remove_one i l =
-  match l with
-  | [] -> []
-  | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2)
-end
-
-let rec remove_from l l2 =
-  match l2 with 
-  | [] -> l
-  | i::l2' -> remove_from (remove_one i l) l2'
-end
-
-let disjoint s1 s2 = Set.null (s1 inter s2)
-
-let rec disjoint_all sets =
-  match sets with
-  | [] -> true
-  | s1::[] -> true
-  | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets))
-end
-}}
-
- 
-grammar 
-
-k :: 'Ki_' ::=
-{{ com Internal kinds }}
-   | K_Typ                                             :: :: typ
-   | K_Nat                                             :: :: nat
-   | K_Ord                                             :: :: ord
-   | K_Efct                                            :: :: efct
-   | K_Lam ( k0 .. kn -> k' )                          :: :: ctor
-   | K_infer                                           :: :: infer {{ com Representing an unknown kind, inferred by context }}
-   | K_Abbrev t                                        :: :: abbrev {{ com Not really a kind, but a convenient way of tracking type abbreviations }}
-
-t , u :: 'T_' ::=                                
-{{ com Internal types }}
-   | id                                           :: :: id
-   | kid                                          :: :: var
-   | t1 -> t2 effect tag S_N                      :: :: fn  {{ com [[S_N]] are constraints for the function, [[tag]] holds generation data }}
-   | ( t1 * .... * tn )                           :: :: tup
-   | id t_args                                    :: :: app 
-   | register t_args                              :: :: reg_app
-   | t [ t1 / id1 ... tn / idn ]		  :: :: subst
-
-tag :: 'Tag_' ::=                                 
-{{ com Data indicating where the identifier arises and thus information necessary in compilation }}
-   | None                                 :: :: empty 
-   | Ctor                                 :: :: ctor {{ com Data constructor from a type union }}
-   | Extern                               :: :: extern {{ com External function, specied only with a val statement }}
-   | Default                              :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }}
-   | _                                    :: :: dontcare 
-
-ne :: 'Ne_' ::=
- {{ com internal numeric expressions }}
-   | kid                                 :: :: var
-   | num                                 :: :: const
-   | ne1 * ne2                           :: :: mult
-   | ne1 + ... + nen                     :: :: add
-   | 2 ** ne				 :: :: exp
-   | ( - ne )                            :: :: unary
-   | zero   				 :: M :: zero
-     {{ lem (Ne_const 0) }}
-   | bitlength ( bin )                   :: M :: cbin
-     {{ ocaml (asssert false) }}
-     {{ hol ARB }}
-     {{ lem (blength [[bin]]) }}
-   | bitlength ( hex )                   :: M :: chex
-     {{ ocaml (assert false) }}
-     {{ hol ARB }}
-     {{ lem (hlength [[hex]]) }}
-   | length ( pat1 ... patn )            :: M :: cpat
-     {{ ocaml (assert false) }}
-     {{ hol ARB }}
-     {{ lem (Ne_const (List.length [[pat1...patn]])) }}
-   | length ( exp1 ... expn )            :: M :: cexp
-     {{ hol ARB }}
-     {{ ocaml (assert false) }}
-     {{ lem (Ne_const (List.length [[exp1...expn]])) }}
- 
- t_arg :: 't_arg_' ::=  
- {{ com Argument to type constructors }}
- | t :: :: typ
- | ne :: :: nexp
- | effect :: :: effect
- | order :: :: order
-
- t_args :: '' ::=   {{ lem list t_arg }}
-  {{ com Arguments to type constructors }}
-   | t_arg1 ... t_argn                            :: :: T_args
-
- nec :: 'Nec_' ::=
-   {{ com Numeric expression constraints }}
-   | ne <= ne'            :: :: lteq
-   | ne = ne'            :: :: eq
-   | ne >= ne'           :: :: gteq
-   | kid 'IN' { num1 , ... , numn } :: :: in
-
-S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
-                                                                    {{ hol nec list }}
-                                                                    {{ lem list nec }}
-    {{ com nexp constraint lists }}
-    | { nec1 , .. ,  necn }                              :: :: Sn_concrete
-      {{ hol [[nec1 .. necn]] }}
-      {{ lem [[nec1 .. necn]] }}
-   | S_N1 u+ .. u+ S_Nn                                                    :: M :: SN_union
-     {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }}
-     {{ lem (List.foldr (++) [] [[S_N1..S_Nn]]) }}
-     {{ ocaml (assert false) }}
-   | consistent_increase ne1 ne'1 ... nen ne'n                    :: M :: SN_increasing
-     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }}
-     {{ ocaml (assert false) }}
-     {{ ichl todo }}
-   | consistent_decrease ne1 ne'1 ... nen ne'n                      :: M :: SN_decreasing
-     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }}
-     {{ ocaml assert false }}
-     {{ ichl todo }}
-   | resolve ( S_N )                                                :: :: resolution
-     {{ lem [[S_N]] (* Write constraint solver *) }}
- 
-
- E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::=  {{ phantom }}
-                                                         {{ lem definition_env }}
- {{ com Environments storing top level information, such as defined records, enumerations, and kinds }}
- | < E_k , E_r , E_e >	     	       		    	 :: :: base
-   {{ hol arb }}
-   {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }}
- | empty       	     					 :: :: empty
-   {{ hol arb }}
-   {{ lem DenvEmp }}
- | E_d u+ E_d'						 :: :: union
-   {{ hol arb }}
-   {{ lem (denv_union [[E_d]] [[E_d']]) }}
- 
- kinf :: 'kinf_' ::=
-   {{ com Whether a kind is default or from a local binding }}
-   | k                                        :: :: k
-   | k default                                :: :: def
-
- tid :: 'tid_' ::=
-   {{ com A type identifier or type variable }}
-   | id                                      :: :: id
-   | kid                                     :: :: var
-
- E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::=             {{ phantom }}
-                                                                 {{ hol (tid-> kinf) }}
-                                                                 {{ lem (map tid kinf) }}
-   {{ com Kind environments }}
-   | { tid1 |-> kinf1 , .. , tidn |-> kinfn }    :: :: concrete
-     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }}
-     {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} 
-   | E_k1 u+ .. u+ E_kn                                          :: M :: union
-     {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} 
-     {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }}
-     {{ lem (List.foldr (union) Map.empty [[E_k1..E_kn]]) }}
-     {{ ocaml (assert false) }}
-   | E_k u- E_k1 .. E_kn                                            :: M :: multi_set_minus
-     {{ hol arb }} 
-     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]]))
-                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} 
-     {{ ocaml assert false }}
-
- 
- tinf :: 'tinf_' ::=                                                 
-    {{ com Type variables, type, and constraints, bound to an identifier }}
-    | t                                                 :: :: typ
-    | E_k , S_N , tag , t         :: :: quant_typ                                                             
-
- field_typs :: 'FT_' ::=     {{ phantom }}
-                             {{ lem list (id * t) }}
- {{ com Record fields }}
- | id1 : t1 , .. , idn : tn :: :: fields
-   {{ lem [[id1 t1..idn tn]] }}
-
- E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::=             {{ phantom }}
-                                                                 {{ hol (id*t) |-> tinf) }}
-                                                                 {{ lem map (list (id*t)) tinf }}
-   {{ com Record environments }}
-   | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn }                    :: :: concrete
-     {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }}
-     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} 
-   | E_r1 u+ .. u+ E_rn                                          :: M :: union
-     {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
-     {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }}
-     {{ ocaml (assert false) }}
-
-  enumerate_map :: '' ::=                                        {{ phantom }}
-                                                                 {{ lem (list (nat*id)) }}
-   | { num1 |-> id1 ... numn |-> idn }                           :: :: enum_map
-    {{ lem [[num1 id1...numn idn]] }}
-
-  E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::=            {{ phantom }}
-                                                                 {{ lem (map t (list (nat*id))) }}
-   {{ com Enumeration environments }}
-   | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn }     :: :: base
-     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} 
-   | E_e1 u+ .. u+ E_en                                         :: :: union
-     {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }}
-
-    
-embed
-{{ lem
- type definition_env =
-   | DenvEmp
-   | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id)))
-
-}}
-
 grammar
 
- E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::=          {{ phantom }}
-                                                                 {{ hol (id |-> tinf) }}
-                                                                 {{ lem map id tinf }}
-   {{ com Type environments }}
-   | { id1 |-> tinf1 , .. , idn |-> tinfn }                    :: :: base
-     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }}
-     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} 
-   | ( E_t1 u+ .... u+ E_tn )                                         :: M :: union
-     {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }}
-     {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }}
-     {{ ocaml (assert false) }}
-   | u+ E_t1 .. E_tn                                            :: M :: multi_union
-     {{ hol arb }}
-     {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }}
-     {{ ocaml assert false }}
-   | E_t u- E_t1 .. E_tn                                            :: M :: multi_set_minus
-     {{ hol arb }} 
-     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]]))
-                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_t1..E_tn]]))))) }} 
-     {{ ocaml assert false }}
-   | ( E_t1 inter .... inter E_tn )                                  :: M :: intersect
-     {{ hol arb }}
-     {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b)))))  Map.empty [[E_t1....E_tn]]) }} 
-     {{ ocaml (assert false) }}
-   | inter E_t1 .. E_tn                                            :: M :: multi_inter
-     {{ hol arb }}
-     {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }}
-     {{ ocaml assert false }}
-
-
-ts :: ts_ ::=                                     {{ phantom }}
-                                                  {{ lem list t }}
-  | t1 , .. , tn :: :: lst 
-
-embed
-{{ lem
-let blength (bit) = Ne_const 8
-let hlength (bit) = Ne_const 8
-
- type env =
-   | EnvEmp 
-   | Env of (map id tinf) * definition_env
-
- type inf = 
-   | Iemp
-   | Inf of (list nec) * effect
-
- val denv_union : definition_env -> definition_env -> definition_env
- let denv_union de1 de2 = 
-  match (de1,de2) with
-   | (DenvEmp,de2) -> de2
-   | (de1,DenvEmp) -> de1
-   | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) ->
-      Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2)
-   end
-
- val env_union : env -> env -> env
- let env_union e1 e2 =
-   match (e1,e2) with
-    | (EnvEmp,e2) -> e2
-    | (e1,EnvEmp) -> e1
-    | ((Env te1 de1),(Env te2 de2)) ->
-      Env (te1 union te2) (denv_union de1 de2)
- end
-
-let inf_union i1 i2 =
-  match (i1,i2) with 
- | (Iemp,i2) -> i2
- | (i1,Iemp) -> i1
- | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2))
- end
-
-let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*)
-
-}}
-
-grammar
-
- E :: '' ::=                                                     
-                                                                 {{ hol ((string,env_body) fmaptree) }}
-                                                                 {{ lem env }}
- {{ com Definition environment and lexical environment }}
- | < E_t , E_d >                                           :: :: E
-  {{ hol arb }}
-  {{ lem (Env [[E_t]] [[E_d]])  }}
- | empty                                                       :: M :: E_empty
-   {{ hol arb }}
-   {{ lem EnvEmp }}
-   {{ ocaml assert false }}
- | E u+ E'                                                      :: :: E_union
-   {{ lem (env_union [[E]] [[E']]) }}
-
- I :: '' ::=                                                     {{ lem inf }}
-  {{ com Information given by type checking an expression }}
-  | < S_N , effect >                                      :: :: I
-    {{ lem (Inf [[S_N]] [[effect]]) }}
-  | Ie                                                           :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }}
-    {{ lem Iemp }}
-  | I1 u+ .. u+ In                                               :: :: Iunion {{ com Unions the constraints and effect }}
-    {{ lem (List.foldr inf_union Iemp [[I1..In]]) }}
-
-
 formula :: formula_ ::=
   | judgement                                                   :: :: judgement
 
diff --git a/language/l2_typ.ott b/language/l2_typ.ott
new file mode 100644
index 00000000..43a3ea17
--- /dev/null
+++ b/language/l2_typ.ott
@@ -0,0 +1,326 @@
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Machinery for typing rules                                   %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+embed
+{{ lem
+
+let rec remove_one i l =
+  match l with
+  | [] -> []
+  | i2::l2 -> if i2 = i then l2 else i2::(remove_one i l2)
+end
+
+let rec remove_from l l2 =
+  match l2 with 
+  | [] -> l
+  | i::l2' -> remove_from (remove_one i l) l2'
+end
+
+let disjoint s1 s2 = Set.null (s1 inter s2)
+
+let rec disjoint_all sets =
+  match sets with
+  | [] -> true
+  | s1::[] -> true
+  | s1::s2::sets -> (disjoint s1 s2) && (disjoint_all (s2::sets))
+end
+}}
+
+ 
+grammar 
+
+k :: 'Ki_' ::=
+{{ com Internal kinds }}
+   | K_Typ                                             :: :: typ
+   | K_Nat                                             :: :: nat
+   | K_Ord                                             :: :: ord
+   | K_Efct                                             :: :: efct
+   | K_Lam ( k0 .. kn -> k' )                  :: :: ctor
+   | K_infer                                           :: :: infer {{ com Representing an unknown kind, inferred by context }}
+
+t , u :: 'T_' ::=                                
+{{ com Internal types }}
+   | id                                            :: :: id
+   | kid                                          :: :: var
+   | t1 -> t2 effect                        :: :: fn 
+   | ( t1 * .... * tn )                          :: :: tup
+   | id t_args                                  :: :: app 
+   | register t_args                         :: S :: reg_app {{ ichlo T_app "register" [[t_args]] }}
+   | t [ t1 / id1 ... tn / idn ]            :: M :: subst {{ ichlo "todo" }}
+
+optx :: '' ::= {{ phantom }} {{ lem maybe string }} {{ ocaml string option }}
+  | x                                            ::  :: optx_x
+  {{ lem (Just [[x]]) }} {{ ocaml (Some [[x]]) }}
+  |                                              :: :: optx_none
+  {{ lem Nothing }} {{ ocaml None }}
+
+
+tag :: 'Tag_' ::=                                 
+{{ com Data indicating where the identifier arises and thus information necessary in compilation }}
+   | None                                 :: :: empty 
+   | Ctor                                 :: :: ctor {{ com Data constructor from a type union }}
+   | Extern optx                              :: :: extern {{ com External function, specied only with a val statement }}
+   | Default                              :: :: default {{ com Type has come from default declaration, identifier may not be bound locally }}
+   | Spec				  :: :: spec
+   | Enum				  :: :: enum
+
+ne :: 'Ne_' ::=
+ {{ com internal numeric expressions }}
+   | kid                                 :: :: var
+   | num                                 :: :: const
+   | ne1 * ne2                           :: :: mult
+   | ne1 + ... + nen                     :: :: add
+   | 2 ** ne				 :: :: exp
+   | ( - ne )                            :: :: unary
+   | zero   				 :: S :: zero
+     {{ lem (Ne_const 0) }}
+   | bitlength ( bin )                   :: M :: cbin
+     {{ ocaml (asssert false) }}
+     {{ hol ARB }}
+     {{ lem (blength [[bin]]) }}
+   | bitlength ( hex )                   :: M :: chex
+     {{ ocaml (assert false) }}
+     {{ hol ARB }}
+     {{ lem (hlength [[hex]]) }}
+   | length ( pat1 ... patn )            :: M :: cpat
+     {{ ocaml (assert false) }}
+     {{ hol ARB }}
+     {{ lem (Ne_const (List.length [[pat1...patn]])) }}
+   | length ( exp1 ... expn )            :: M :: cexp
+     {{ hol ARB }}
+     {{ ocaml (assert false) }}
+     {{ lem (Ne_const (List.length [[exp1...expn]])) }}
+ 
+ t_arg :: 't_arg_' ::=  
+ {{ com Argument to type constructors }}
+ | t :: :: typ
+ | ne :: :: nexp
+ | effect :: :: effect
+ | order :: :: order
+
+ t_args :: '' ::=   {{ lem list t_arg }}
+  {{ com Arguments to type constructors }}
+   | t_arg1 ... t_argn                            :: :: T_args
+
+ nec :: 'Nec_' ::=
+   {{ com Numeric expression constraints }}
+   | ne <= ne'            :: :: lteq
+   | ne = ne'            :: :: eq
+   | ne >= ne'           :: :: gteq
+   | kid 'IN' { num1 , ... , numn } :: :: in
+
+S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
+                                                                    {{ hol nec list }}
+                                                                    {{ lem list nec }}
+    {{ com nexp constraint lists }}
+    | { nec1 , .. ,  necn }                              :: :: Sn_concrete
+      {{ hol [[nec1 .. necn]] }}
+      {{ lem [[nec1 .. necn]] }}
+   | S_N1 u+ .. u+ S_Nn                                                    :: M :: SN_union
+     {{ hol (FOLDR FUNION FEMPTY [[S_N1..S_Nn]]) }}
+     {{ lem (List.foldr (++) [] [[S_N1..S_Nn]]) }}
+     {{ ocaml (assert false) }}
+   | consistent_increase ne1 ne'1 ... nen ne'n                    :: M :: SN_increasing
+     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always larger than the sum of the previous pair }}
+     {{ ocaml (assert false) }}
+     {{ ichl todo }}
+   | consistent_decrease ne1 ne'1 ... nen ne'n                      :: M :: SN_decreasing
+     {{ com Generates constraints from  pairs of constraints, where the first of each pair is always smaller than the difference of the previous pair }}
+     {{ ocaml assert false }}
+     {{ ichl todo }}
+   | resolve ( S_N )                                                :: :: resolution
+     {{ lem [[S_N]] (* Write constraint solver *) }}
+ 
+
+ E_d {{ tex {\ottnt{E}^{\textsc{d} } } }} :: 'E_d_' ::=  {{ phantom }}
+                                                         {{ lem definition_env }}
+ {{ com Environments storing top level information, such as defined records, enumerations, and kinds }}
+ | < E_k , E_r , E_e >	     	       		    	 :: :: base
+   {{ hol arb }}
+   {{ lem (Denv [[E_k]] [[E_r]] [[E_e]]) }}
+ | empty       	     					 :: :: empty
+   {{ hol arb }}
+   {{ lem DenvEmp }}
+ | E_d u+ E_d'						 :: :: union
+   {{ hol arb }}
+   {{ lem (denv_union [[E_d]] [[E_d']]) }}
+ 
+ kinf :: 'kinf_' ::=
+   {{ com Whether a kind is default or from a local binding }}
+   | k                                        :: :: k
+   | k default                                :: :: def
+
+ tid :: 'tid_' ::=
+   {{ com A type identifier or type variable }}
+   | id                                      :: :: id
+   | kid                                     :: :: var
+
+ E_k {{ tex {\ottnt{E}^{\textsc{k} } } }} :: 'E_k_' ::=             {{ phantom }}
+                                                                 {{ hol (tid-> kinf) }}
+                                                                 {{ lem (map tid kinf) }}
+   {{ com Kind environments }}
+   | { tid1 |-> kinf1 , .. , tidn |-> kinfn }    :: :: concrete
+     {{ hol (FOLDR (\(k1,k2) E. E |+ (k1,k2)) FEMPTY [[tid1 kinf1 .. tidn kinfn]]) }}
+     {{ lem (List.foldr (fun (x,v) m -> Map.insert x v m) Map.empty [[tid1 kinf1 .. tidn kinfn]]) }} 
+   | E_k1 u+ .. u+ E_kn                                          :: M :: union
+     {{ com In a unioning kinf, {k default} u {k} results in {k} (i.e. the default is locally forgotten) }} 
+     {{ hol (FOLDR FUNION FEMPTY [[E_k1..E_kn]]) }}
+     {{ lem (List.foldr (union) Map.empty [[E_k1..E_kn]]) }}
+     {{ ocaml (assert false) }}
+   | E_k u- E_k1 .. E_kn                                            :: M :: multi_set_minus
+     {{ hol arb }} 
+     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_k]]))
+                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_k1..E_kn]]))))) }} 
+     {{ ocaml assert false }}
+
+ 
+ tinf :: 'tinf_' ::=                                                 
+    {{ com Type variables, type, and constraints, bound to an identifier }}
+    | t                                                 :: :: typ
+    | E_k , S_N , tag , t         :: :: quant_typ                                                             
+
+ field_typs :: 'FT_' ::=     {{ phantom }}
+                             {{ lem list (id * t) }}
+ {{ com Record fields }}
+ | id1 : t1 , .. , idn : tn :: :: fields
+   {{ lem [[id1 t1..idn tn]] }}
+
+ E_r {{ tex \ottnt{E}^{\textsc{r} } }} :: 'E_r_' ::=             {{ phantom }}
+                                                                 {{ hol (id*t) |-> tinf) }}
+                                                                 {{ lem map (list (id*t)) tinf }}
+   {{ com Record environments }}
+   | { { field_typs1 } |-> tinf1 , .. , { field_typsn } |-> tinfn }                    :: :: concrete
+     {{ hol (FOLDR (\x E. E |+ x) FEMPTY) }}
+     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[field_typs1 tinf1..field_typsn tinfn]]) }} 
+   | E_r1 u+ .. u+ E_rn                                          :: M :: union
+     {{ hol (FOLDR FUNION FEMPTY [[E_r1..E_rn]]) }}
+     {{ lem (List.foldr (union) Map.empty [[E_r1..E_rn]]) }}
+     {{ ocaml (assert false) }}
+
+  enumerate_map :: '' ::=                                        {{ phantom }}
+                                                                 {{ lem (list (nat*id)) }}
+   | { num1 |-> id1 ... numn |-> idn }                           :: :: enum_map
+    {{ lem [[num1 id1...numn idn]] }}
+
+  E_e {{ tex \ottnt{E}^{\textsc{e} } }} :: 'E_e_' ::=            {{ phantom }}
+                                                                 {{ lem (map t (list (nat*id))) }}
+   {{ com Enumeration environments }}
+   | { t1 |-> enumerate_map1 , .. , tn |-> enumerate_mapn }     :: :: base
+     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[t1 enumerate_map1..tn enumerate_mapn]]) }} 
+   | E_e1 u+ .. u+ E_en                                         :: :: union
+     {{ lem (List.foldr (union) Map.empty [[E_e1..E_en]]) }}
+
+    
+embed
+{{ lem
+ type definition_env =
+   | DenvEmp
+   | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id)))
+
+}}
+
+grammar
+
+ E_t {{ tex {\ottnt{E}^{\textsc{t} } } }} :: 'E_t_' ::=          {{ phantom }}
+                                                                 {{ hol (id |-> tinf) }}
+                                                                 {{ lem map id tinf }}
+   {{ com Type environments }}
+   | { id1 |-> tinf1 , .. , idn |-> tinfn }                    :: :: base
+     {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }}
+     {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} 
+   | ( E_t1 u+ .... u+ E_tn )                                         :: M :: union
+     {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }}
+     {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }}
+     {{ ocaml (assert false) }}
+   | u+ E_t1 .. E_tn                                            :: M :: multi_union
+     {{ hol arb }}
+     {{ lem (List.foldr (union) Map.empty [[E_t1..E_tn]]) }}
+     {{ ocaml assert false }}
+   | E_t u- E_t1 .. E_tn                                            :: M :: multi_set_minus
+     {{ hol arb }} 
+     {{ lem (Map.fromList (remove_from (Set_extra.toList (Map.toSet [[E_t]]))
+                                       (Set_extra.toList (Map.toSet (List.foldr (union) Map.empty [[E_t1..E_tn]]))))) }} 
+     {{ ocaml assert false }}
+   | ( E_t1 inter .... inter E_tn )                                  :: M :: intersect
+     {{ hol arb }}
+     {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b)))))  Map.empty [[E_t1....E_tn]]) }} 
+     {{ ocaml (assert false) }}
+   | inter E_t1 .. E_tn                                            :: M :: multi_inter
+     {{ hol arb }}
+     {{ lem (List.foldr (fun a b -> (Map.fromList (Set_extra.toList ((Map.toSet a) inter (Map.toSet b))))) Map.empty [[E_t1..E_tn]]) }}
+     {{ ocaml assert false }}
+
+
+ts :: ts_ ::=                                     {{ phantom }}
+                                                  {{ lem list t }}
+  | t1 , .. , tn :: :: lst 
+
+embed
+{{ lem
+let blength (bit) = Ne_const 8
+let hlength (bit) = Ne_const 8
+
+ type env =
+   | EnvEmp 
+   | Env of (map id tinf) * definition_env
+
+ type inf = 
+   | Iemp
+   | Inf of (list nec) * effect
+
+ val denv_union : definition_env -> definition_env -> definition_env
+ let denv_union de1 de2 = 
+  match (de1,de2) with
+   | (DenvEmp,de2) -> de2
+   | (de1,DenvEmp) -> de1
+   | ((Denv ke1 re1 ee1),(Denv ke2 re2 ee2)) ->
+      Denv (ke1 union ke2) (re1 union re2) (ee1 union ee2)
+   end
+
+ val env_union : env -> env -> env
+ let env_union e1 e2 =
+   match (e1,e2) with
+    | (EnvEmp,e2) -> e2
+    | (e1,EnvEmp) -> e1
+    | ((Env te1 de1),(Env te2 de2)) ->
+      Env (te1 union te2) (denv_union de1 de2)
+ end
+
+let inf_union i1 i2 =
+  match (i1,i2) with 
+ | (Iemp,i2) -> i2
+ | (i1,Iemp) -> i1
+ | (Inf n1 e1,Inf n2 e2) -> (Inf (n1++n2) (effect_union e1 e2))
+ end
+
+let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should actually build a fresh string*)
+
+}}
+
+grammar
+
+ E :: '' ::=                                                     
+                                                                 {{ hol ((string,env_body) fmaptree) }}
+                                                                 {{ lem env }}
+ {{ com Definition environment and lexical environment }}
+ | < E_t , E_d >                                           :: :: E
+  {{ hol arb }}
+  {{ lem (Env [[E_t]] [[E_d]])  }}
+ | empty                                                       :: M :: E_empty
+   {{ hol arb }}
+   {{ lem EnvEmp }}
+   {{ ocaml assert false }}
+ | E u+ E'                                                      :: :: E_union
+   {{ lem (env_union [[E]] [[E']]) }}
+
+ I :: '' ::=                                                     {{ lem inf }}
+  {{ com Information given by type checking an expression }}
+  | < S_N , effect >                                      :: :: I
+    {{ lem (Inf [[S_N]] [[effect]]) }}
+  | Ie                                                           :: :: Iempty {{ com Empty constraints, effect }} {{ tex {\ottnt{I}_{\epsilon} } }}
+    {{ lem Iemp }}
+  | I1 u+ .. u+ In                                               :: :: Iunion {{ com Unions the constraints and effect }}
+    {{ lem (List.foldr inf_union Iemp [[I1..In]]) }}
+
diff --git a/src/initial_check.ml b/src/initial_check.ml
index e7b92019..ed4a0208 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -530,17 +530,17 @@ let to_ast_rec (Parse_ast.Rec_aux(r,l): Parse_ast.rec_opt) : rec_opt =
   | Parse_ast.Rec_rec -> Rec_rec
   ),l)
 
-let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)) : tannot tannot_opt * kind Envmap.t * kind Envmap.t=
+let to_ast_tannot_opt (k_env : kind Envmap.t) (Parse_ast.Typ_annot_opt_aux(tp,l)) : tannot_opt * kind Envmap.t * kind Envmap.t=
   match tp with
   | Parse_ast.Typ_annot_opt_none -> raise (Reporting_basic.err_unreachable l "Parser generated typ annot opt none")
   | Parse_ast.Typ_annot_opt_some(tq,typ) ->
     let typq,k_env,k_local = to_ast_typquant k_env tq in
-    Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),(l,None)),k_env,k_local
+    Typ_annot_opt_aux(Typ_annot_opt_some(typq,to_ast_typ k_env typ),l),k_env,k_local
 
-let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : tannot effect_opt =
+let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) : effect_opt =
   match e with
-  | Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,(l,None))
-  | Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),(l,None))
+  | Parse_ast.Effect_opt_pure -> Effect_opt_aux(Effect_opt_pure,l)
+  | Parse_ast.Effect_opt_effect(typ) -> Effect_opt_aux(Effect_opt_effect(to_ast_effects k_env typ),l)
 
 let to_ast_funcl (names,k_env,t_env) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) =
   match fcl with
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 8a68f8eb..854ed202 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1,19 +1,33 @@
 open import Pervasives
 import Map
 import Map_extra
-import Maybe
 import List_extra
-import String
+open import String_extra
 
 open import Interp_ast
 
+type tannot = maybe (t * tag * list nec * effect)
+
+val pure : effect
+let pure = Effect_aux(Effect_set []) Unknown
+
+val intern_annot : tannot -> tannot
+let intern_annot annot =
+  match annot with
+    | Just (t,_,ncs,effect) ->
+      Just (t,Tag_empty,ncs,pure)
+    | Nothing -> Nothing
+  end
+
+let val_annot typ = Just(typ,Tag_empty,[],pure)
+
 (* Workaround Lem's inability to scrap my (type classes) boilerplate.
  * Implementing only Eq, and only for literals - hopefully this will
  * be enough, but we should in principle implement ordering for everything in
  * Interp_ast *)
 
 val lit_eq: lit -> lit -> bool
-let lit_eq left right =
+let lit_eq (L_aux left _) (L_aux right _) =
    match (left, right) with
    | (L_unit, L_unit) -> true
    | (L_zero, L_zero) -> true
@@ -39,16 +53,16 @@ end
 let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
 let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')
 
-let get_id id = match id with Id s -> s | DeIid s -> s end
+let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
 
 type value =
- | V_boxref of nat 
+ | V_boxref of nat * t  
  | V_lit of lit
  | V_tuple of list value
  | V_list of list value
  | V_vector of natural * bool * list value (* The nat stores the first index, the bool whether that's most or least significant *)
- | V_record of list (id * value)
- | V_ctor of id * value
+ | V_record of t * list (id * value)
+ | V_ctor of id * t * value
 
  (* seems useless currently:
 let rec id_value_eq (i, v) (i', v') = i = i' && value_eq v v'
@@ -78,7 +92,7 @@ type env = list (id * value)
 let emem = Mem 1 Map.empty
 
 type reg_form =
- | Reg of id * typ
+ | Reg of id * t
  | SubReg of id * reg_form * index_range
 
 (* These may need to be refined or expanded based on memory requirement *)
@@ -92,34 +106,35 @@ type action =
 (* Inverted call stack, where top item on the stack is waiting for an action and all other frames for the right stack *)
 type stack = 
  | Top
- | Frame of id * exp * env * mem * stack
+ | Frame of id * exp tannot * env * mem * stack
 
 (* Either a case must be added for parallel options or action must be tied to a list *)
 type outcome =
  | Value of value
  | Action of action * stack
- | Error of string (* When we store location information, it should be added here *)
+ | Error of l * string 
 
 (* interprets the exp sequentially in the presence of a set of top level definitions and returns a value or a memory request *)
-val interp : defs -> exp -> outcome
+val interp : defs tannot -> exp tannot -> outcome
 
-val to_registers : defs -> list (id * reg_form)
-let rec to_registers (Defs defs) =
-  match defs with
+val to_registers : defs tannot -> list (id * reg_form)
+let rec to_registers (Defs defs) = []
+(*  match defs with
   | [ ] -> [ ]
-  | def::defs -> 
+  | (DEF_aux def _)::defs -> 
     match def with 
     | DEF_spec valsp -> 
       match valsp with
-      | VS_val_spec (TypSchm_ts tq ((Typ_app (Id "reg") _) as t)) id -> (id, Reg id t):: (to_registers (Defs defs))
+      | (VS_aux (VS_val_spec (TypSchm_aux (TypSchm_ts tq ((Typ_aux (Typ_app (Id_aux (Id "reg") _) _) _) as t)) _) id) _) -> 
+	(id, Reg id t):: (to_registers (Defs defs))
       | _ -> to_registers (Defs defs)
       end
     | DEF_reg_dec typ id -> (id, Reg id typ) :: (to_registers (Defs defs))
     | DEF_type tdef ->
       match tdef with 
-      | TD_register id n1 n2 ranges -> 
-	(id,Reg id (Typ_app (Id "vector")[]))::
-	((to_reg_ranges id (Reg id (Typ_app (Id "vector")[])) ranges) ++ (to_registers (Defs defs)))
+      | (TD_aux (TD_register id n1 n2 ranges) _) -> 
+	(id,Reg id (Typ_aux (Typ_app (Id_aux (Id "vector") Unknown) []) Unknown))::
+	((to_reg_ranges id (Reg id (Typ_aux (Typ_app (Id_aux (Id "vector") Unknown) []) Unknown)) ranges) ++ (to_registers (Defs defs)))
       | _ -> to_registers (Defs defs)
       end
     | _ -> to_registers (Defs defs)
@@ -129,13 +144,13 @@ and to_reg_ranges base_id base_reg ranges =
   match ranges with
   | [ ] -> [ ]
   | (irange,id)::ranges -> (id,(SubReg base_id base_reg irange))::(to_reg_ranges base_id base_reg ranges)
-  end
+  end*)
 
 val has_memory_effect : list base_effect -> bool
 let rec has_memory_effect efcts =
   match efcts with
   | [] -> false
-  | e::efcts ->
+  | (BE_aux e _)::efcts ->
     match e with
     | BE_wreg -> true
     | BE_wmem -> true
@@ -143,53 +158,66 @@ let rec has_memory_effect efcts =
     end 
   end
 
+let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
+let get_effects (Typ_aux t _) =
+  match t with
+    | Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff
+    | _ -> []
+  end
+
 (*Look for externs as well*)
-val to_memory_ops : defs -> list (id * typ)
-let rec to_memory_ops (Defs defs) =
-  match defs with
+val to_memory_ops : defs tannot -> list (id * typ)
+let rec to_memory_ops (Defs defs) = []
+(*  match defs with
   | [] -> []
-  | def ::defs ->
+  | (DEF_aux def _) ::defs ->
     match def with
-    | DEF_spec valsp ->
+    | DEF_spec (VS_aux valsp _) ->
       match valsp with
-      | VS_val_spec (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id ->
+      | VS_val_spec ts id ->
+	let t = get_typ ts in
+	let eff = get_effects t in
         if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
-      | VS_extern_spec (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id _ ->
+      | VS_extern_spec ts id _ ->
+	let t = get_typ ts in
+	let eff = get_effects t in
         if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
-      | VS_extern_no_rename (TypSchm_ts tq ((Typ_fn a r (Effect_set eff)) as t)) id ->
+      | VS_extern_no_rename ts id ->
+	let t = get_typ ts in
+	let eff = get_effects t in
         if has_memory_effect eff then (id,t)::(to_memory_ops (Defs defs)) else (to_memory_ops (Defs defs))
       | _ -> to_memory_ops (Defs defs) end
     | _ -> to_memory_ops (Defs defs) end
-  end
+  end*)
 
-val to_externs : defs -> list (id * string)
-let rec to_externs (Defs defs) =
-  match defs with
+val to_externs : defs tannot -> list (id * string)
+let rec to_externs (Defs defs) = []
+(*  match defs with
   | [] -> []
-  | def ::defs ->
+  | (DEF_aux def _) ::defs ->
     match def with
-    | DEF_spec valsp ->
+    | DEF_spec (VS_aux valsp _) ->
       match valsp with
-      | VS_extern_spec (TypSchm_ts tq ((Typ_fn a r e) as t)) id s ->
+      | VS_extern_spec (TypSchm_aux (TypSchm_ts tq (Typ_aux (Typ_fn a r e) _)) _) id s ->
         (id,s)::(to_externs (Defs defs))
       | _ -> to_externs (Defs defs) end
     | _ -> to_externs (Defs defs) end
-  end
+  end*)
 
-val to_data_constructors : defs -> list (id * typ)
+val to_data_constructors : defs tannot -> list (id * typ)
 let rec to_data_constructors (Defs defs) =
   match defs with
   | [] -> []
-  | def :: defs ->
+  | (DEF_aux def _) :: defs ->
     match def with
-    | DEF_type t ->
+    | DEF_type (TD_aux t _)->
       match t with 
       | TD_variant id _ tq tid_list _ ->
         (List.map 
-	   (fun t ->
+	   (fun (Tu_aux t _) ->
 	     match t with
 	    | (Tu_ty_id x y) -> (y,x)
-	    | Tu_id x -> (id,Typ_app (Id "unit") []) end) tid_list)++(to_data_constructors (Defs defs))
+	    | Tu_id x -> (id,Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown) end) tid_list)++(to_data_constructors (Defs defs))
       | _ -> to_data_constructors (Defs defs) end
     | _ -> to_data_constructors (Defs defs) end
    end
@@ -198,7 +226,7 @@ val in_env : env -> id -> maybe value
 let rec in_env env id =
  match env with
  | [] -> Nothing
- | (eid,value)::env -> if eid = id then Just value else in_env env id
+ | (eid,value)::env -> if (get_id eid) = (get_id id) then Just value else in_env env id
  end 
 
 val in_mem : mem -> nat -> value
@@ -213,7 +241,7 @@ let update_mem (Mem c m) loc value =
   Mem c m'
 
 val is_lit_vector : lit -> bool
-let is_lit_vector l = 
+let is_lit_vector (L_aux l _) = 
   match l with
   | L_bin _ -> true 
   | L_hex _ -> true
@@ -221,16 +249,16 @@ let is_lit_vector l =
 end
 
 val litV_to_vec : lit -> value
-let litV_to_vec l =
-  match l with
+let litV_to_vec (L_aux lit l) =
+  match lit with
   | L_hex s ->
     let hexes = String.toCharList s in
     (* XXX unimplemented *)
     V_vector 0 true []
   | L_bin s -> 
     let bits = String.toCharList s in
-    let exploded_bits = List.map (fun c -> String.toString [c]) bits in
-    let bits = List.map (fun s -> match s with | "0" -> (V_lit L_zero) | "1" -> (V_lit L_one) end) exploded_bits in
+    let exploded_bits = bits in (*List.map (fun c -> String.toString [c]) bits in*)
+    let bits = List.map (fun s -> match s with | #'0' -> (V_lit (L_aux L_zero l)) | #'1' -> (V_lit (L_aux L_one l)) end) exploded_bits in
     (* XXX assume binary constants are written in big-endian, convert them to
      * little-endian by default - we might need syntax to change both of those
      * assumptions. *)
@@ -281,18 +309,18 @@ end
 val fupdate_record : value -> value -> value
 let fupdate_record base updates = 
   match (base,updates) with
-  | (V_record bs,V_record us) -> V_record (update_field_list bs us) end
+  | (V_record t bs,V_record _ us) -> V_record t (update_field_list bs us) end
 
 val update_vector_slice : value -> value -> mem -> mem
 let rec update_vector_slice vector value mem = 
   match (vector,value) with
   | ((V_vector m inc vs),(V_vector n inc2 vals)) ->
     foldr2 (fun vbox v mem -> match vbox with
-                                       | V_boxref n -> update_mem mem n v end)
+                                       | V_boxref n t -> update_mem mem n v end)
       mem vs vals
   | ((V_vector m inc vs),v) ->
     List.foldr (fun vbox mem -> match vbox with
-                                    | V_boxref n -> update_mem mem n v end)
+                                    | V_boxref n t -> update_mem mem n v end)
       mem vs
 end
 
@@ -326,13 +354,13 @@ val in_reg : list (id * reg_form) -> id -> maybe reg_form
 let rec in_reg regs id =
   match regs with
   | [] -> Nothing
-  | (eid,regf)::regs -> if eid = id then Just regf else in_reg regs id
+  | (eid,regf)::regs -> if (get_id eid) = (get_id id) then Just regf else in_reg regs id
 end
 val in_ctors : list (id * typ) -> id -> maybe typ
 let rec in_ctors ctors id =
   match ctors with
   | [] -> Nothing
-  | (cid,typ)::ctors -> if cid = id then Just typ else in_ctors ctors id
+  | (cid,typ)::ctors -> if (get_id cid) = (get_id id) then Just typ else in_ctors ctors id
 end
 
 let add_to_top_frame e_builder stack =
@@ -340,33 +368,105 @@ let add_to_top_frame e_builder stack =
   | Frame id e env mem stack -> Frame id (e_builder e) env mem stack
   end
 
-let rec to_exp v =
-    match v with
-    | V_boxref n -> E_id (Id ("XXX string_of_num n"))
-    | V_lit lit -> E_lit lit
-    | V_tuple(vals) -> E_tuple (List.map to_exp vals)
-    | V_vector n inc vals -> 
-      if (inc && n=0) 
-      then E_vector (List.map to_exp vals) 
-      else if inc then
-        E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
-      else 
-        E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals))
-    | V_record(ivals) -> E_record(FES_Fexps (List.map (fun (id,value) -> (FE_Fexp id (to_exp value))) ivals) false)
-    | V_list(vals) -> E_list (List.map to_exp vals)
-    | V_ctor id vals -> E_app id [to_exp vals]
-    end
+let id_of_string s = (Id_aux (Id s) Unknown)
+
+let rec combine_typs ts =
+  match ts with
+  | [] -> T_var (Kid_aux (Var "fresh") Unknown)
+  | [t] -> t
+  | t::ts ->
+    let t' = combine_typs ts in
+    match (t,t') with 
+      | (_,T_var _) -> t
+      | ((T_app (Id_aux (Id "enum") _) (T_args [T_arg_nexp (Ne_const n1); T_arg_nexp (Ne_const r1)])),
+	 (T_app (Id_aux (Id "enum") _) (T_args [T_arg_nexp (Ne_const n2); T_arg_nexp (Ne_const r2)]))) ->
+	let (smaller,larger,larger_r) = if n1 < n2 then (n1,n2,r2) else (n2,n1,r1) in
+	let r = (larger + larger_r) - smaller in
+	T_app (id_of_string "enum") (T_args [T_arg_nexp (Ne_const smaller); T_arg_nexp (Ne_const r)])
+      | ((T_app (Id_aux (Id "vector") _) (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); 
+						  T_arg_order (Ord_aux o1 _); T_arg_typ t1])),
+	 (T_app (Id_aux (Id "vector") _) (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); 
+						  T_arg_order (Ord_aux o2 _); T_arg_typ t2]))) ->
+	let t = combine_typs [t1;t2] in
+	match (o1,o2) with
+	  | (Ord_inc,Ord_inc) ->
+	    let larger_start = if b1 < b2 then b2 else b1 in
+	    let smaller_rise = if r1 < r2 then r1 else r2 in
+	    (T_app (id_of_string "vector") (T_args [T_arg_nexp (Ne_const larger_start); T_arg_nexp (Ne_const smaller_rise);
+						    (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
+	  | (Ord_dec,Ord_dec) ->
+	    let smaller_start = if b1 < b2 then b1 else b2 in
+	    let smaller_fall = if r1 < r2 then r2 else r2 in
+	    (T_app (id_of_string "vector") (T_args [T_arg_nexp (Ne_const smaller_start); T_arg_nexp (Ne_const smaller_fall);
+						    (T_arg_order (Ord_aux o1 Unknown)); T_arg_typ t]))
+	  | _ -> T_var (Kid_aux (Var "fresh") Unknown)
+	 end 
+      | _ -> t'
+     end 
+   end
 
-val find_type_def : defs -> id -> maybe type_def
-val find_function : defs -> id -> maybe (list funcl)
 
-let get_funcls id (FD_function _ _ _ fcls) =
-  List.filter (fun (FCL_Funcl name pat exp) -> id = name) fcls
+let rec val_typ v =
+  match v with
+    | V_boxref n t -> T_app (id_of_string "reg") (T_args [T_arg_typ t])
+    | V_lit (L_aux lit _) ->
+      match lit with
+	| L_unit -> T_id (id_of_string "unit")
+	| L_true -> T_id (id_of_string "bool")
+	| L_false -> T_id (id_of_string "bool")
+	| L_one -> T_id (id_of_string "bit")
+	| L_zero -> T_id (id_of_string "bit")
+	| L_string _ -> T_id (id_of_string "string")
+	| L_num n -> T_app (id_of_string "enum") (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const 0)])
+	| L_undef -> T_var (Kid_aux (Var "fresh") Unknown)
+      end 
+    | V_tuple vals -> T_tup (List.map val_typ vals)
+    | V_vector n inc vals -> 
+      let ts = List.map val_typ vals in
+      let t = combine_typs ts in
+      T_app (id_of_string "vector") (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const (list_length vals));
+					     T_arg_order (Ord_aux (if inc then Ord_inc else Ord_dec) Unknown);
+					     T_arg_typ t])
+    | V_record t ivals -> t
+    | V_list vals -> 
+      let ts = List.map val_typ vals in
+      let t = combine_typs ts in
+      T_app (id_of_string "list") (T_args [T_arg_typ t])
+    | V_ctor id t vals -> t
+  end
+
+let rec to_exp v =
+  E_aux
+    (match v with
+      | V_boxref n t -> E_id (Id_aux (Id (show n)) Unknown)
+      | V_lit lit -> E_lit lit
+      | V_tuple(vals) -> E_tuple (List.map to_exp vals)
+      | V_vector n inc vals -> 
+	if (inc && n=0) 
+	then E_vector (List.map to_exp vals) 
+	else if inc then
+          E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n, to_exp e)::acc)) (n,[]) vals)))
+	else 
+          E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n, to_exp e)::acc)) (n-(list_length vals),[]) vals))
+      | V_record t ivals -> 
+	E_record(FES_aux (FES_Fexps
+			    (List.map (fun (id,value) -> (FE_aux (FE_Fexp id (to_exp value)) (Unknown,Nothing))) ivals) false) 
+		   (Unknown,Nothing))
+      | V_list(vals) -> E_list (List.map to_exp vals)
+      | V_ctor id t vals -> E_app id [to_exp vals]
+     end)
+    (Unknown,(val_annot (val_typ v)))
+
+val find_type_def : defs tannot -> id -> maybe (type_def tannot)
+val find_function : defs tannot -> id -> maybe (list (funcl tannot))
+
+let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
+  List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls
 
 let rec find_function (Defs defs) id =
   match defs with 
   | [] -> Nothing
-  | def::defs -> 
+  | (DEF_aux def _)::defs -> 
     match def with
     | DEF_fundef f -> match get_funcls id f with
       | [] -> find_function (Defs defs) id
@@ -380,8 +480,8 @@ let find_memory mems id = List.lookup id mems
 val find_extern : list ( id * string ) -> id -> maybe string
 let find_extern externs id = List.lookup id externs
 
-val match_pattern : pat -> value -> bool * list (id * value)
-let rec match_pattern p value =
+val match_pattern : pat tannot -> value -> bool * list (id * value)
+let rec match_pattern (P_aux p _) value =
   match p with 
   | P_lit(lit) -> 
     if is_lit_vector lit then
@@ -411,7 +511,7 @@ let rec match_pattern p value =
  | P_id id -> (true, [(id,value)])
  | P_app id pats -> 
    match value with
-   | V_ctor cid (V_tuple vals) -> 
+   | V_ctor cid t (V_tuple vals) -> 
      if (id = cid && ((List.length pats) = (List.length vals)))
      then foldr2
           (fun pat value (matched_p,bounds) ->
@@ -423,9 +523,9 @@ let rec match_pattern p value =
    | _ -> (false,[]) end
  | P_record fpats _ ->
    match value with
-   | V_record fvals ->
+   | V_record t fvals ->
      List.foldr
-       (fun (FP_Fpat id pat) (matched_p,bounds) ->
+       (fun (FP_aux (FP_Fpat id pat) _) (matched_p,bounds) ->
          if matched_p then
            let (matched_p,new_bounds) = match in_env fvals id with
                                        | Nothing -> (false,[])
@@ -465,7 +565,7 @@ let rec match_pattern p value =
    | V_vector n inc vals ->
      let (matched_p,bounds,remaining_vals) =
        List.foldl 
-         (fun (matched_p,bounds,r_vals) pat ->
+         (fun (matched_p,bounds,r_vals) (P_aux pat _) ->
            match pat with
            | P_vector pats -> vec_concat_match pats r_vals
            | P_id id -> (false,[],[]) (*Need to have at least a guess of how many to consume*)
@@ -512,37 +612,37 @@ and vec_concat_match pats r_vals =
     end
 
 
-val find_funcl : list funcl -> value -> maybe (env * exp)
+val find_funcl : list (funcl tannot) -> value -> maybe (env * (exp tannot))
 let rec find_funcl funcls value =
   match funcls with
   | [] -> Nothing
-  | (FCL_Funcl id pat exp)::funcls ->
+  | (FCL_aux (FCL_Funcl id pat exp) _)::funcls ->
     let (is_matching,env) = match_pattern pat value in
     if is_matching then Just (env,exp) else find_funcl funcls value
   end
 
-val find_case : list pexp -> value -> maybe (env * exp)
+val find_case : list (pexp tannot) -> value -> maybe (env * (exp tannot))
 let rec find_case pexps value =
   match pexps with
   | [] -> Nothing
-  | (Pat_exp p e)::pexps -> 
+  | (Pat_aux (Pat_exp p e) _)::pexps -> 
     let (is_matching,env) = match_pattern p value in
     if is_matching then Just(env,e) else find_case pexps value
   end
 
 (*top_level is a tuple of 
   (all definitions, external functions, letbound values, declared registers, memory functions (typ expected to be num -> num -> a), and Typedef union constructors) *)
-type top_level = Env of defs * list (id * string) * env * list (id*reg_form) * list (id * typ) * list (id * typ)
+type top_level = Env of (defs tannot) * list (id * string) * env * list (id*reg_form) * list (id * typ) * list (id * typ)
 
-val interp_main : top_level -> env -> mem -> exp -> (outcome * mem * env)
-val exp_list : top_level -> (list exp -> exp) -> (list value -> value) -> env -> mem -> list value -> list exp -> (outcome * mem * env)
-val interp_lbind : top_level -> env -> mem -> letbind -> ((outcome * mem * env) * (maybe (exp -> letbind)))
+val interp_main : top_level -> env -> mem -> (exp tannot) -> (outcome * mem * env)
+val exp_list : top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> env -> mem -> list value -> list (exp tannot) -> (outcome * mem * env)
+val interp_lbind : top_level -> env -> mem -> (letbind tannot) -> ((outcome * mem * env) * (maybe ((exp tannot) -> (letbind tannot))))
 
 let resolve_outcome to_match value_thunk action_thunk =
   match to_match with
   | (Value v,lm,le) -> value_thunk v lm le
   | (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le)
-  | (Error s,lm,le) -> (Error s,lm,le)
+  | (Error l s,lm,le) -> (Error l s,lm,le)
   end
 
 let update_stack (Action act stack) fn = Action act (fn stack)  
@@ -557,166 +657,232 @@ let rec exp_list t_level build_e build_v l_env l_mem vals exps =
                     (fun a -> update_stack a (add_to_top_frame (fun e -> (build_e ((List.map to_exp vals)++(e::exps))))))
   end
 
-and interp_main t_level l_env l_mem exp =
-    match exp with
-    | E_lit lit -> if is_lit_vector lit then (Value (litV_to_vec lit),l_mem,l_env) else (Value (V_lit lit), l_mem,l_env)
+and interp_main t_level l_env l_mem (E_aux exp (l,annot)) =
+  let (Env defs externs lets regs mems ctors) = t_level in 
+  let (typ,tag,ncs,effect) = match annot with 
+    | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown),
+		  Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
+    | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
+  match exp with
+    | E_lit lit -> 
+      if is_lit_vector lit then (Value (litV_to_vec lit),l_mem,l_env) else (Value (V_lit lit), l_mem,l_env)
     | E_cast typ exp -> interp_main t_level l_env l_mem exp (* Potentially introduce coercions ie vectors and numbers *)
-    | E_id id -> match in_env l_env id with
-                 | Just(value) -> match value with
-		                  | V_boxref n ->(Value (in_mem l_mem n),l_mem,l_env)
-		                  | _ -> (Value value,l_mem,l_env) end
-		 | Nothing -> match t_level with
-		           | (Env defs externs lets regs mems ctors) ->
-                             match in_env lets id with
-                             | Just(value) -> (Value value,l_mem,l_env) 
-                             | Nothing -> 
-			       match in_reg regs id with
-			       | Just(regf) -> 
-			         (Action (Read_reg regf Nothing) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top), l_mem, l_env) 
-			       | Nothing ->                                  
-                                 let name = get_id id in
-			         (Error (String.stringAppend "unbound identifier " name ),l_mem,l_env)
-			        end 
-                              end 
-                            end
-		end
+    | E_id id -> 
+      let name = get_id id in
+      match tag with
+	| Tag_empty -> 
+	  match in_env l_env id with
+	    | Just(value) -> match value with
+		             | V_boxref n t -> (Value (in_mem l_mem n),l_mem,l_env)
+			     | _ -> (Value value,l_mem,l_env) end
+            | Nothing -> 
+              match in_env lets id with
+              | Just(value) -> (Value value,l_mem,l_env) 
+              | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_none " name), l_mem,l_env)
+          end end
+        | Tag_enum ->
+          match in_env lets id with
+            | Just(value) -> (Value value,l_mem,l_env)
+	    | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_enum " name), l_mem,l_env)
+	    end 
+        | Tag_extern _ -> (* Need to change from "register" to which register where different from id *)
+	  let regf = Reg id typ in
+	  (Action (Read_reg regf Nothing)
+	          (Frame (Id_aux (Id "0") Unknown)
+		         (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),
+           l_mem,l_env)
+        | _ -> (Error l (String.stringAppend "Internal error: tag other than empty,enum,or extern " name),l_mem,l_env)
+        end
     | E_if cond thn els ->
       resolve_outcome (interp_main t_level l_env l_mem cond)
                       (fun value lm le -> 
                         match value with
-                        | V_lit(L_true) -> interp_main t_level l_env lm thn
-                        | V_lit(L_false) -> interp_main t_level l_env lm els
-                        | _ -> (Error "Type error, not provided boolean for if",lm,l_env) end)
-                      (fun a -> update_stack a (add_to_top_frame (fun c -> (E_if c thn els))))
-    | E_for id from to_ by order exp ->
+                        | V_lit(L_aux L_true _) -> interp_main t_level l_env lm thn
+                        | V_lit(L_aux L_false _) -> interp_main t_level l_env lm els end)
+                      (fun a -> update_stack a (add_to_top_frame (fun c -> (E_aux (E_if c thn els) (l,annot)))))
+    | E_for id from to_ by ((Ord_aux o _) as order) exp ->
+      let is_inc = match o with
+        | Ord_inc -> true
+        | _ -> false end in
       resolve_outcome (interp_main t_level l_env l_mem from)
                       (fun from_val lm le ->
                         match from_val with
-                        | V_lit(L_num from_num) -> 
+                        | (V_lit(L_aux(L_num from_num) fl) as fval) -> 
                           resolve_outcome (interp_main t_level le lm to_)
                                           (fun to_val lm le ->
                                             match to_val with
-                                            | V_lit(L_num to_num) ->
+                                            | (V_lit(L_aux (L_num to_num) tl) as tval) ->
                                               resolve_outcome 
                                                 (interp_main t_level le lm by)
                                                 (fun by_val lm le ->
                                                   match by_val with 
-                                                  | V_lit (L_num by_num) ->
+                                                  | (V_lit (L_aux (L_num by_num) bl) as bval) ->
                                                     if (from_num = to_num) 
-                                                    then (Value(V_lit L_unit),lm,le)
-                                                    else interp_main t_level le lm 
-                                                      (E_block [(E_let (LB_val_implicit (P_id id) (E_lit (L_num from_num))) exp);
-                                                                (E_for id (E_lit (L_num (from_num + by_num))) (E_lit (L_num to_num)) (E_lit (L_num by_num)) order exp)])
-                                                  | _ -> (Error "by must be a number",lm,le) end)
-                                                (fun a -> update_stack a (add_to_top_frame (fun b -> (E_for id (E_lit (L_num from_num)) (E_lit (L_num to_num)) b order exp))))
-                                            | _ -> (Error "to must be a number",lm,le) end)
-                                           (fun a -> update_stack a (add_to_top_frame (fun t -> (E_for id (E_lit (L_num from_num)) t by order exp))))
-                        | _ -> (Error "from must be a number",lm,le) end)
-                       (fun a -> update_stack a (add_to_top_frame (fun f -> (E_for id f to_ by order exp))))
+                                                    then (Value(V_lit (L_aux L_unit l)),lm,le)
+                                                    else
+                                                      let (ftyp,ttyp,btyp) = (val_typ fval,val_typ tval,val_typ bval) in
+                                                      interp_main t_level le lm 
+                                                        (E_aux 
+							   (E_block 
+							      [(E_aux (E_let 
+								         (LB_aux (LB_val_implicit 
+									            (P_aux (P_id id) (fl,val_annot ftyp))
+									            (E_aux (E_lit(L_aux(L_num from_num) fl)) (fl,val_annot ftyp)))
+								            (Unknown,val_annot ftyp))
+								         exp) (l,annot));
+                                                               (E_aux (E_for id 
+                                                                         (if is_inc 
+                                                                          then (E_aux (E_lit (L_aux (L_num (from_num + by_num)) fl)) (fl,val_annot (combine_typs [ftyp;ttyp])))
+                                                                          else (E_aux (E_lit (L_aux (L_num (from_num - by_num)) fl)) (fl,val_annot (combine_typs [ttyp;ftyp]))))
+								         (E_aux (E_lit (L_aux (L_num to_num) tl)) (tl,val_annot ttyp))
+								         (E_aux (E_lit (L_aux (L_num by_num) bl)) (bl,val_annot btyp))
+								         order exp) (l,annot))])
+							   (l,annot))
+                                                  | _ -> (Error l "internal error: by must be a number",lm,le) end)
+                                                (fun a -> update_stack a 
+						  (add_to_top_frame (fun b -> 
+						    (E_aux (E_for id 
+							      (E_aux (E_lit (L_aux (L_num from_num) fl)) (fl,(val_annot (val_typ fval))))
+							      (E_aux (E_lit (L_aux (L_num to_num) tl)) (tl,(val_annot (val_typ tval))))
+							      b order exp) (l,annot)))))
+                                            | _ -> (Error l "internal error: to must be a number",lm,le) end)
+                                           (fun a -> update_stack a 
+					     (add_to_top_frame (fun t -> 
+					       (E_aux (E_for id (E_aux (E_lit (L_aux (L_num from_num) fl)) (fl,val_annot (val_typ fval)))
+							 t by order exp) (l,annot)))))
+                        | _ -> (Error l "internal error: from must be a number",lm,le) end)
+                       (fun a -> update_stack a (add_to_top_frame (fun f -> (E_aux (E_for id f to_ by order exp) (l,annot)))))
     | E_case exp pats ->
       resolve_outcome (interp_main t_level l_env l_mem exp)
                       (fun v lm le ->
                         match find_case pats v with
-                        | Nothing -> (Error "No matching patterns in case",lm,le)
+                        | Nothing -> (Error l "No matching patterns in case",lm,le)
                         | Just (env,exp) -> interp_main t_level (env++l_env) lm exp end)
-                      (fun a -> update_stack a (add_to_top_frame (fun e -> E_case e pats)))
-    | E_record(FES_Fexps fexps _) -> 
-      let (fields,exps) = List.unzip (List.map (fun (FE_Fexp id exp) -> (id,exp)) fexps) in
-      exp_list t_level (fun es -> (E_record(FES_Fexps (map2 (fun id exp -> FE_Fexp id exp) fields es) false)))
-	               (fun vs -> (V_record (List.zip fields vs))) l_env l_mem [] exps
-    | E_record_update exp (FES_Fexps fexps _) ->
+                      (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_case e pats) (l,annot)))))
+    | E_record(FES_aux (FES_Fexps fexps _) fes_annot) -> 
+      let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
+      exp_list t_level 
+	(fun es -> 
+	  (E_aux (E_record 
+		    (FES_aux (FES_Fexps (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing))) fields es) false) fes_annot))
+	          (l,annot)))
+	(fun vs -> (V_record typ (List.zip fields vs))) l_env l_mem [] exps
+    | E_record_update exp (FES_aux (FES_Fexps fexps _) fes_annot) ->
       resolve_outcome (interp_main t_level l_env l_mem exp)
                       (fun rv lm le -> 
                         match rv with
-                        | V_record fvs ->
-                          let (fields,exps) = List.unzip (List.map (fun (FE_Fexp id exp) -> (id,exp)) fexps) in
-                          resolve_outcome (exp_list t_level (fun es -> (E_record_update (to_exp rv) (FES_Fexps (map2 (fun id exp -> FE_Fexp id exp) fields es) false)))
-                                                            (fun vs -> (V_record (List.zip fields vs))) l_env l_mem [] exps)
+                        | V_record t fvs ->
+                          let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
+                          resolve_outcome (exp_list t_level 
+					     (fun es -> 
+					       (E_aux (E_record_update (to_exp rv) 
+							 (FES_aux (FES_Fexps 
+								     (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing)))
+									fields es) false) fes_annot))
+						      (l,annot)))					     
+                                             (fun vs -> (V_record t (List.zip fields vs))) l_env l_mem [] exps)
                                           (fun vs lm le ->
                                             (Value (fupdate_record rv vs), lm, le))
                                           (fun a -> a)
-                        | _ -> (Error "record upate requires record",lm,le) end)
-                      (fun a -> update_stack a (add_to_top_frame (fun e -> E_record_update e (FES_Fexps fexps false))))
+                        | _ -> (Error l "record upate requires record",lm,le) end)
+                      (fun a -> update_stack a (add_to_top_frame 
+						  (fun e -> E_aux(E_record_update e (FES_aux(FES_Fexps fexps false) fes_annot)) (l,annot))))
     | E_list(exps) ->
-      exp_list t_level E_list V_list l_env l_mem [] exps
+      exp_list t_level (fun exps -> E_aux (E_list exps) (l,annot)) V_list l_env l_mem [] exps
     | E_cons hd tl ->
       resolve_outcome (interp_main t_level l_env l_mem hd)
                       (fun hdv lm le -> resolve_outcome
                                         (interp_main t_level l_env lm tl)
                                         (fun tlv lm le -> match tlv with 
                                                    | V_list t -> (Value(V_list (hdv::t)),lm,le)
-                                                   | _ -> (Error ":: of non-list value",lm,le) end)
-                                        (fun a -> update_stack a (add_to_top_frame (fun t -> E_cons (to_exp hdv) t))))
-                      (fun a -> update_stack a (add_to_top_frame (fun h -> E_cons h tl)))
+                                                   | _ -> (Error l ":: of non-list value",lm,le) end)
+                                        (fun a -> update_stack a (add_to_top_frame (fun t ->E_aux (E_cons (to_exp hdv) t) (l,annot)))))
+                      (fun a -> update_stack a (add_to_top_frame (fun h -> E_aux (E_cons h tl) (l,annot))))
     | E_field exp id -> 
       resolve_outcome (interp_main t_level l_env l_mem exp)
                       (fun value lm le -> 
                         match value with 
-                        | V_record fexps -> match in_env fexps id with
+                        | V_record t fexps -> match in_env fexps id with
                                             | Just v -> (Value v,lm,l_env)
-                                            | Nothing -> (Error "Field not found in record",lm,le) end
-                        | _ -> (Error "Field access requires a record",lm,le)
+                                            | Nothing -> (Error l "Field not found in record",lm,le) end
+                        | _ -> (Error l "Field access requires a record",lm,le)
                         end )
-                      (fun a -> update_stack a (add_to_top_frame (fun e -> E_field e id)))
+                      (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux(E_field e id) (l,annot))))
     | E_vector_access vec i ->
       resolve_outcome (interp_main t_level l_env l_mem i)
                       (fun iv lm le -> 
                         match iv with
-                        | V_lit (L_num n) -> 
+                        | V_lit (L_aux (L_num n) ln) -> 
                           resolve_outcome (interp_main t_level l_env lm vec)
                                           (fun vvec lm le ->
                                             match vvec with
                                             | V_vector base inc vals -> (Value (access_vector vvec n),lm,le)
-                                            | _ -> (Error "Vector access of non-vector",lm,le)end)
-                                          (fun a -> update_stack a (add_to_top_frame (fun v -> (E_vector_access v (E_lit (L_num n))))))
-                        | _ -> (Error "Vector access not given a number for index",lm,l_env) end)
-                      (fun a -> update_stack a (add_to_top_frame (fun i -> E_vector_access vec i)))
+                                            | _ -> (Error l "Vector access of non-vector",lm,le)end)
+                                          (fun a -> update_stack a 
+					    (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)))))
+                        | _ -> (Error l "Vector access not given a number for index",lm,l_env) end)
+                      (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_access vec i) (l,annot))))
     | E_vector_subrange vec i1 i2 ->
       resolve_outcome (interp_main t_level l_env l_mem i1)
                       (fun i1v lm le ->
                         match i1v with
-                        | V_lit (L_num n1) ->
+                        | V_lit (L_aux (L_num n1) ln1) ->
                           resolve_outcome (interp_main t_level l_env lm i2)
                                           (fun i2v lm le ->
                                             match i2v with
-                                            | V_lit (L_num n2) ->
+                                            | V_lit (L_aux (L_num n2) ln2) ->
                                               resolve_outcome (interp_main t_level l_env lm vec)
                                                               (fun vvec lm le ->
                                                                 match vvec with
                                                                 | V_vector base inc vals -> (Value (slice_vector vvec n1 n2),lm,le)
-                                                                | _ -> (Error "Vector slice of non-vector",lm,le)end)
+                                                                | _ -> (Error l "Vector slice of non-vector",lm,le)end)
                                                               (fun a -> update_stack a 
-                                                                (add_to_top_frame (fun v -> (E_vector_subrange v (E_lit (L_num n1)) (E_lit (L_num n2))))))
-                                            | _ -> (Error "vector slice given non number for last index",lm,le) end)
-                                          (fun a -> update_stack a (add_to_top_frame (fun i2 -> (E_vector_subrange vec (E_lit (L_num n1)) i2))))
-                        | _ -> (Error "Vector slice given non-number for first index",lm,le) end)
-                       (fun a -> update_stack a (add_to_top_frame (fun i1 -> (E_vector_subrange vec i1 i2))))
+                                                                (add_to_top_frame 
+								   (fun v -> (E_aux (E_vector_subrange v 
+										       (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+										       (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)))
+										(l,annot)))))
+                                            | _ -> (Error l "vector slice given non number for last index",lm,le) end)
+                                          (fun a -> update_stack a 
+					    (add_to_top_frame 
+					       (fun i2 -> (E_aux (E_vector_subrange vec 
+								    (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+								    i2) (l,annot)))))
+                        | _ -> (Error l "Vector slice given non-number for first index",lm,le) end)
+                       (fun a -> update_stack a (add_to_top_frame (fun i1 -> (E_aux (E_vector_subrange vec i1 i2) (l,annot)))))
     | E_vector_update vec i exp ->
       resolve_outcome (interp_main t_level l_env l_mem i)
                       (fun vi lm le ->
                         match vi with
-                        | V_lit (L_num n1) ->
+                        | V_lit (L_aux (L_num n1) ln1) ->
                           resolve_outcome (interp_main t_level le lm exp)
                                           (fun vup lm le ->
                                             resolve_outcome (interp_main t_level le lm vec)
                                                             (fun vec lm le ->
                                                               match vec with
                                                               | V_vector base inc vals -> (Value (fupdate_vec vec n1 vup), lm,le)
-                                                              | _ -> (Error "Update of vector given non-vector",lm,le) end)
-                                                            (fun a -> update_stack a (add_to_top_frame (fun v -> E_vector_update v (E_lit (L_num n1)) (to_exp vup)))))
-                                          (fun a -> update_stack a (add_to_top_frame (fun e -> E_vector_update vec (E_lit (L_num n1)) e)))
-                        | _ -> (Error "Update of vector requires number for access",lm,le) end)
-                      (fun a -> update_stack a (add_to_top_frame (fun i -> E_vector_update vec i exp)))                            
+                                                              | _ -> (Error l "Update of vector given non-vector",lm,le) end)
+                                                            (fun a -> update_stack a 
+							      (add_to_top_frame 
+								 (fun v -> E_aux (E_vector_update v 
+										    (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) 
+										    (to_exp vup)) (l,annot)))))
+                                          (fun a -> update_stack a 
+					    (add_to_top_frame (fun e -> E_aux (E_vector_update vec 
+										 (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+										 e) (l,annot))))
+                        | _ -> (Error l "Update of vector requires number for access",lm,le) end)
+                      (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_update vec i exp) (l,annot))))
     | E_vector_update_subrange vec i1 i2 exp ->
       resolve_outcome (interp_main t_level l_env l_mem i1)
                       (fun vi1 lm le ->
                         match vi1 with
-                        | V_lit (L_num n1) ->
+                        | V_lit (L_aux (L_num n1) ln1) ->
                           resolve_outcome 
                             (interp_main t_level l_env lm i2) 
                             (fun vi2 lm le ->
                               match vi2 with
-                              | V_lit (L_num n2) ->
+                              | V_lit (L_aux (L_num n2) ln2) ->
                                 resolve_outcome (interp_main t_level l_env lm exp)
                                   (fun v_rep lm le ->
                                     (resolve_outcome 
@@ -724,90 +890,131 @@ and interp_main t_level l_env l_mem exp =
                                        (fun vvec lm le ->
                                          match vvec with
                                          | V_vector m inc vals -> (Value (fupdate_vector_slice vvec v_rep n1 n2),lm,le)
-                                         | _ -> (Error "Vector update requires vector",lm,le) end)
+                                         | _ -> (Error l "Vector update requires vector",lm,le) end)
                                        (fun a -> update_stack a 
-                                         (add_to_top_frame (fun v -> E_vector_update_subrange v (E_lit (L_num n1)) (E_lit (L_num n2)) (to_exp v_rep))))))
+                                         (add_to_top_frame 
+					    (fun v -> E_aux (E_vector_update_subrange v 
+							       (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+							       (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)) 
+							       (to_exp v_rep)) (l,annot))))))
                                   (fun a -> update_stack a 
-                                    (add_to_top_frame (fun e -> E_vector_update_subrange vec (to_exp vi1) (to_exp vi2) e)))
-                              | _ -> (Error "vector update requires number",lm,le) end)
-                            (fun a -> update_stack a (add_to_top_frame (fun i2 -> E_vector_update_subrange vec (to_exp vi1) i2 exp)))
-                        | _ -> (Error "vector update requires number",lm,le) end)
-                      (fun a -> update_stack a (add_to_top_frame (fun i1 -> E_vector_update_subrange vec i1 i2 exp)))
+                                    (add_to_top_frame 
+				       (fun e -> E_aux (E_vector_update_subrange vec (to_exp vi1) (to_exp vi2) e) (l,annot))))
+                              | _ -> (Error l "vector update requires number",lm,le) end)
+                            (fun a -> 
+			      update_stack a (add_to_top_frame (fun i2 -> E_aux (E_vector_update_subrange vec (to_exp vi1) i2 exp) (l,annot))))
+                        | _ -> (Error l "vector update requires number",lm,le) end)
+                      (fun a -> update_stack a (add_to_top_frame (fun i1 -> E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot))))
     | E_tuple(exps) -> 
-      exp_list t_level E_tuple V_tuple l_env l_mem [] exps
+      exp_list t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
     | E_vector(exps) ->
-      exp_list t_level E_vector (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
+      exp_list t_level (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps
     | E_vector_indexed(iexps) ->
       let (indexes,exps) = List.unzip iexps in
-      exp_list t_level (fun es -> (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es))) 
-                       (fun vals -> V_vector (List_extra.head indexes) true vals) (*Need to see increasing or not, can look at types later*) l_env l_mem [] exps
+      let is_inc = match typ with
+        | T_app (Id_aux (Id "vector") _) (T_args [T_arg_nexp _;T_arg_nexp _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
+        | _ -> false end in
+      exp_list t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)) (l,annot))) 
+                       (fun vals -> V_vector (List_extra.head indexes) is_inc vals) l_env l_mem [] exps
     | E_block(exps) -> interp_block t_level l_env l_env l_mem exps
     | E_app f args ->
-      (match (exp_list t_level (fun es -> E_app f es) (fun vs -> match vs with | [] -> V_lit L_unit | [v] -> v | vs -> V_tuple vs end) l_env l_mem [] args) with
+      (match (exp_list t_level (fun es -> E_aux (E_app f es) (l,annot)) 
+		               (fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end) 
+			       l_env l_mem [] args) with
       | (Value v,lm,le) -> 
-         (match (f,t_level) with
-      	 | (id,(Env defs externs lets regs mems ctors)) -> 
-	   (match find_function defs id with
-	   | Just(funcls) -> 
-             (match find_funcl funcls v with
-	     | Nothing -> 
-               let name = get_id id in
-               (Error (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
-	     | Just(env,exp) -> 
-               resolve_outcome (interp_main t_level env l_mem exp)
-	                       (fun ret lm le -> (Value ret, lm,l_env))
-                               (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack)))
+        let name = get_id f in 
+        (match tag with
+        | Tag_empty -> 
+	  (match find_function defs f with
+	  | Just(funcls) -> 
+            (match find_funcl funcls v with
+	    | Nothing -> 
+              (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
+	    | Just(env,exp) -> 
+              resolve_outcome (interp_main t_level env l_mem exp)
+	                      (fun ret lm le -> (Value ret, lm,l_env))
+                              (fun a -> update_stack a 
+				(fun stack -> (Frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
              end)
-          | Nothing -> 
-            (match in_ctors ctors id with
-            | Just(typ) -> (Value (V_ctor id v), lm, le)
-            | Nothing -> 
-              (match find_memory mems id with
-              | Just(typ) -> 
-                (Action (Read_mem id v Nothing) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)
-              | Nothing -> 
-                (match find_extern externs id with
-                | Just(str) -> 
-                  (Action (Call_extern str v) (Frame (Id "0") (E_id (Id "0")) le lm Top), lm, le)
-                | Nothing -> (Error (String.stringAppend "Unknown function call " (get_id id)),lm,le) end)
-	       end) end) end) end)
-         | out -> out end)
-    | E_app_infix l op r -> 
+          | Nothing -> (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
+	| Tag_spec ->  
+          (match find_function defs f with
+	  | Just(funcls) -> 
+            (match find_funcl funcls v with
+	    | Nothing -> 
+              (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
+	    | Just(env,exp) -> 
+              resolve_outcome (interp_main t_level env l_mem exp)
+	                      (fun ret lm le -> (Value ret, lm,l_env))
+                              (fun a -> update_stack a 
+				(fun stack -> (Frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
+             end)
+          | Nothing -> (Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end)
+        | Tag_ctor ->
+          (match in_ctors ctors f with
+          | Just(_) -> (Value (V_ctor f typ v), lm, le)
+          | Nothing -> (Error l (String.stringAppend "Internal error: function with ctor tag unfound " name),lm,le)
+           end)
+        | Tag_extern opt_name ->
+          let name_ext = match opt_name with | Just s -> s | Nothing -> name end in
+          if has_memory_effect (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end) 
+          then
+            (Action (Read_mem (id_of_string name_ext) v Nothing) 
+	            (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) le lm Top), lm, le)
+          else
+            (Action (Call_extern name_ext v) 
+	            (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) le lm Top), lm, le)
+        | _ -> (Error l (String.stringAppend "Tag other than empty, spec, ctor, or extern on function call " name),lm,le) end)
+      | out -> out end)
+    | E_app_infix lft op r -> 
        let op = match op with
-       | Id x -> DeIid x
-       | DeIid _ -> op
+       | Id_aux (Id x) il -> Id_aux (DeIid x) il
+       | _ -> op
        end in
-      resolve_outcome (interp_main t_level l_env l_mem l)
+      let name = get_id op in
+      resolve_outcome (interp_main t_level l_env l_mem lft)
                       (fun lv lm le -> 
                          resolve_outcome (interp_main t_level l_env lm r)
                                          (fun rv lm le -> 
-			                   (match t_level with
-			                   | (Env defs externs lets regs mems ctors) ->
+                                           match tag with
+                                           | Tag_empty -> 
 				             (match find_function defs op with
-				             | Nothing -> 
-                                               (match find_extern externs op with
-                                               | Just(str) ->
-                                                 (Action (Call_extern str (V_tuple [lv;rv])) (Frame (Id "0") (E_id (Id "0")) le lm Top),lm,le)
-                                               | Nothing ->
-                                                   (Error (String.stringAppend
-                                                   "No matching function "
-                                                   (get_id op)),lm,l_env) end)
-				             | Just (funcls) ->
+				             | Nothing -> (Error l (String.stringAppend "Internal error, no function def for " name),lm,le)
+                                             | Just (funcls) ->
 				               (match find_funcl funcls (V_tuple [lv;rv]) with 
-				               | Nothing -> (Error "No matching pattern for function",lm,l_env)
+				               | Nothing -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
 				               | Just(env,exp) ->
 				                 resolve_outcome (interp_main t_level env emem exp)
-				                 (fun ret lm le -> (Value ret,l_mem,l_env))
-                                                 (fun a -> update_stack a (fun stack -> (Frame (Id "0") (E_id (Id "0")) l_env l_mem stack)))
-				                end)
-				              end)
-			                    end))
-                                         (fun a -> update_stack a (add_to_top_frame (fun r -> (E_app_infix (to_exp lv) op r)))))
-                       (fun a -> update_stack a (add_to_top_frame (fun l -> (E_app_infix l op r))))
-  | E_let lbind exp -> 
+				                   (fun ret lm le -> (Value ret,l_mem,l_env))
+                                                   (fun a -> update_stack a 
+						     (fun stack -> (Frame (Id_aux (Id "0") l)
+								          (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
+				                end)end)
+                                           | Tag_spec ->
+                                             (match find_function defs op with
+				             | Nothing -> (Error l (String.stringAppend "No function definition found for " name),lm,le)
+                                             | Just (funcls) ->
+				               (match find_funcl funcls (V_tuple [lv;rv]) with 
+				               | Nothing -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
+				               | Just(env,exp) ->
+				                 resolve_outcome (interp_main t_level env emem exp)
+				                   (fun ret lm le -> (Value ret,l_mem,l_env))
+                                                   (fun a -> update_stack a 
+						     (fun stack -> (Frame (Id_aux (Id "0") l)
+								          (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack)))
+				                end)end)
+                                           | Tag_extern ext_name ->
+                                             let ext_name = match ext_name with Just s -> s | Nothing -> name end in
+                                             (Action (Call_extern ext_name (V_tuple [lv;rv])) 
+						     (Frame (Id_aux (Id "0") l) 
+							    (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) le lm Top),lm,le) end)
+                                         (fun a -> update_stack a (add_to_top_frame (fun r ->E_aux (E_app_infix (to_exp lv) op r) (l,annot)))))
+                       (fun a -> update_stack a (add_to_top_frame (fun lft -> (E_aux (E_app_infix lft op r) (l,annot)))))
+  | E_let (lbind : letbind tannot) exp -> 
     match (interp_letbind t_level l_env l_mem lbind) with
     | ((Value v,lm,le),_) -> interp_main t_level le lm exp
-    | (((Action a s as o),lm,le),Just lbuild) ->  ((update_stack o (add_to_top_frame (fun e -> (E_let (lbuild e) exp)))),lm,le)
+    | (((Action a s as o),lm,le),Just lbuild) ->  
+      ((update_stack o (add_to_top_frame (fun e -> (E_aux (E_let (lbuild e) exp) (l,annot))))),lm,le)
     | (e,_) -> e end
   | E_assign lexp exp ->
     resolve_outcome (interp_main t_level l_env l_mem exp)
@@ -823,98 +1030,123 @@ and interp_main t_level l_env l_mem exp =
 					      (Action (Write_reg regf range value) stack)
 					    | (Action (Write_mem id a range value) stack) -> 
 					      (Action (Write_mem id a range value) stack)
-					    | _ -> update_stack a (add_to_top_frame (fun e -> (E_assign (lexp_builder e) (to_exp v)))) end))
+					    | _ -> update_stack a (add_to_top_frame 
+								     (fun e -> (E_aux (E_assign (lexp_builder e) (to_exp v)) (l,annot)) )) end))
 		       end))
-                    (fun a -> update_stack a (add_to_top_frame (fun v -> (E_assign lexp v))))
+                    (fun a -> update_stack a (add_to_top_frame (fun v -> (E_aux (E_assign lexp v) (l,annot)))))
   end
 
  and interp_block t_level init_env local_env local_mem exps =
    match exps with
-    | [ ] -> (Value (V_lit (L_unit)), local_mem, init_env)
+    | [ ] -> (Value (V_lit (L_aux (L_unit) Unknown)), local_mem, init_env)
     | [ exp ] -> interp_main t_level local_env local_mem exp
     | exp:: exps ->
       resolve_outcome (interp_main t_level local_env local_mem exp)
                       (fun _ lm le -> interp_block t_level init_env le lm exps)
-                      (fun a -> update_stack a (add_to_top_frame (fun e -> E_block(e::exps))))
+                      (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_block(e::exps)) (Unknown,Nothing)))))
     end
 
-and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
+and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) =
    let (Env defs externs lets regs mems ctors) = t_level in
+  let (typ,tag,ncs,ef) = match annot with 
+    | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown), Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
+    | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
    match lexp with
     | LEXP_id id -> 
-      match in_env l_env id with
-      | Just (V_boxref n) -> 
-	if is_top_level 
-	then ((Value (V_lit L_unit), update_mem l_mem n value, l_env),Nothing)
-	else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_id id))
-      | Just v -> if is_top_level then ((Error "Writes must be to reg values",l_mem,l_env),Nothing) else ((Value v,l_mem,l_env),Just (fun e -> LEXP_id id))
-      | Nothing -> 
-	match in_reg regs id with
-	| Just regf -> let request = (Action (Write_reg regf Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env l_mem Top),l_mem,l_env) in
-                       if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_id id))
-	| Nothing -> 
-	  if is_top_level 
-          then begin
-	    let (Mem c m) = l_mem in
-	    let l_mem = (Mem (c+1) m) in
-	    ((Value (V_lit L_unit), update_mem l_mem c value, (id,(V_boxref c))::l_env),Nothing)
-          end
-          else ((Error "Undefined id",l_mem,l_env),Nothing)
-        end
+      match tag with
+	| Tag_empty ->
+	  match in_env l_env id with
+	    | Just (V_boxref n t) -> 
+	      if is_top_level 
+	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
+	      else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_id id) (l,annot)))
+	    | Just v -> 
+	      if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) 
+	      else ((Value v,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_id id) (l,annot)))
+	    | Nothing -> 	  
+	      if is_top_level 
+              then begin
+		let (Mem c m) = l_mem in
+		let l_mem = (Mem (c+1) m) in
+		((Value (V_lit (L_aux L_unit l)), update_mem l_mem c value, (id,(V_boxref c typ))::l_env),Nothing)
+              end
+              else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing)
+          end 
+        | Tag_extern _ ->
+	  let regf = Reg id typ in
+	  let request = (Action (Write_reg regf Nothing value) 
+			        (Frame (Id_aux (Id "0") l) 
+				       (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env l_mem Top),l_mem,l_env) in
+          if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_aux (LEXP_id id) (l,annot)))
+        | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern or empty " (get_id id)),l_mem,l_env),Nothing)
       end 
     | LEXP_memory id exps -> 
-      match (exp_list t_level E_tuple (fun vs -> match vs with | [] -> V_lit L_unit | [v] -> v | vs -> V_tuple vs end) l_env l_mem [] exps) with
+      match (exp_list t_level (fun exps -> E_aux (E_tuple exps) (Unknown,Nothing)) 
+	              (fun vs -> match vs with | [] -> V_lit (L_aux L_unit Unknown) | [v] -> v | vs -> V_tuple vs end)
+		      l_env l_mem [] exps) with
       | (Value v,lm,le) ->
-        let request = (Action (Write_mem id v Nothing value) (Frame (Id "0") (E_id (Id "0")) l_env lm Top),lm,l_env) in
-        if is_top_level then (request,Nothing) else (request,Just (fun e -> (LEXP_memory id (match v with | V_tuple vs -> (List.map to_exp vs) | v -> [to_exp v]end))))
-      | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_tuple es) -> (LEXP_memory id es)))
+        (match tag with
+        | Tag_extern ->
+          let request = (Action (Write_mem id v Nothing value) 
+                                (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) l_env lm Top),lm,l_env) in
+          if is_top_level then (request,Nothing) 
+	  else (request,Just (fun e -> 
+	                       (LEXP_aux (LEXP_memory id (match v with | V_tuple vs -> (List.map to_exp vs) | v -> [to_exp v]end)) (l,annot))))
+         end)
+      | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) -> (LEXP_aux (LEXP_memory id es) (l,annot))))
       | e -> (e,Nothing) end
     | LEXP_vector lexp exp -> 
       match (interp_main t_level l_env l_mem exp) with
       | (Value i,lm,le) ->
         (match i with 
-        | V_lit (L_num n) -> 
-          let next_builder le_builder = (fun e -> LEXP_vector (le_builder e) (E_lit (L_num n))) in
+        | V_lit (L_aux (L_num n) ln) -> 
+          let next_builder le_builder = (fun e -> 
+	                                  LEXP_aux (LEXP_vector (le_builder e) (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)) in
           (match (create_write_message_or_update t_level value l_env lm false lexp) with
           | ((Value v,lm,le),maybe_builder) ->
             (match v with 
             | V_vector inc m vs -> 
               let nth = access_vector v n in
               (match (nth,is_top_level,maybe_builder) with
-              | (V_boxref n,true,_) -> ((Value (V_lit L_unit), update_mem lm n value, l_env),Nothing)
-              | (v,true,_) -> ((Error "Vector does not contain reg values",lm,l_env),Nothing)
-              | ((V_boxref n),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
+              | (V_boxref n t,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
+              | (v,true,_) -> ((Error l "Vector does not contain reg values",lm,l_env),Nothing)
+              | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
               | (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
-            | _ -> ((Error "Vector access of non-vector",lm,l_env),Nothing) end)
+            | _ -> ((Error l "Vector access of non-vector",lm,l_env),Nothing) end)
          | ((Action a s,lm,le),Just lexp_builder) ->
            (match (a,is_top_level) with
            | ((Write_reg regf Nothing value),true) -> ((Action (Write_reg regf (Just (n,n)) value) s, lm,le), Nothing)
-           | ((Write_reg regf Nothing value),false) -> ((Action (Write_reg regf (Just (n,n)) value) s,lm,le), Just  (next_builder lexp_builder))
+           | ((Write_reg regf Nothing value),false) -> 
+	     ((Action (Write_reg regf (Just (n,n)) value) s,lm,le), Just  (next_builder lexp_builder))
            | ((Write_mem id a Nothing value),true) -> ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing)
-           | ((Write_mem id a Nothing value),false) -> ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
+           | ((Write_mem id a Nothing value),false) -> 
+	     ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
            | _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end)
          | e -> e end)
-        | _ -> ((Error "Vector access must be a number",lm,le),Nothing) end)
-      | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_vector lexp e)))
+        | _ -> ((Error l "Vector access must be a number",lm,le),Nothing) end)
+      | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_aux (LEXP_vector lexp e) (l,annot))))
       | e -> (e,Nothing) end
     | LEXP_vector_range lexp exp1 exp2  ->
       match (interp_main t_level l_env l_mem exp1) with
       | (Value i1, lm, le) ->
         (match i1 with
-        | V_lit (L_num n1) ->
+        | V_lit (L_aux (L_num n1) ln1) ->
           (match (interp_main t_level l_env l_mem exp2) with
           | (Value i2,lm,le) ->
             (match i2 with
-            | V_lit (L_num n2) ->
-              let next_builder le_builder = (fun e -> LEXP_vector_range (le_builder e) (E_lit (L_num n1)) (E_lit (L_num n2))) in
+            | V_lit (L_aux (L_num n2) ln2) ->
+              let next_builder le_builder = 
+		(fun e -> LEXP_aux (LEXP_vector_range (le_builder e) 
+				                      (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
+						      (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))) (l,annot)) in
               (match (create_write_message_or_update t_level value l_env lm false lexp) with
               | ((Value v,lm,le), Just lexp_builder) ->
                 (match (v,is_top_level) with
                 | (V_vector m inc vs,true) -> 
-                  ((Value (V_lit L_unit), update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing)
+                  ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing)
                 | (V_vector m inc vs,false) ->
                   ((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder))
-                | _ -> ((Error "Vector required",lm,le),Nothing) end)
+                | _ -> ((Error l "Vector required",lm,le),Nothing) end)
               | ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
                 ((Action (Write_reg regf (Just (n1,n2)) value) s,lm,le), Just (next_builder lexp_builder))
               | ((Action (Write_mem id a Nothing value) s,lm,le), Just lexp_builder) ->
@@ -922,63 +1154,66 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level lexp =
               | ((Action a s,lm,le), Just lexp_builder) ->
                 ((Action a s,lm,le), Just (next_builder lexp_builder))
               | e -> e end)
-            | _ -> ((Error "Vector slice requires a number", lm, le),Nothing) end)
+            | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end)
           | (Action a s,lm,le) ->
-            ((Action a s,lm, le), Just (fun e -> LEXP_vector_range lexp (E_lit (L_num  n1)) e))
+            ((Action a s,lm, le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp 
+							                     (E_aux (E_lit (L_aux (L_num  n1) ln1)) (ln1,Nothing))
+									     e) (l,annot)))
           | e -> (e,Nothing) end)
-        | _ -> ((Error "Vector slice requires a number", lm, le),Nothing) end)
+        | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end)
       | (Action a s,lm,le) ->
-        ((Action a s, lm,le), Just (fun e -> LEXP_vector_range lexp e exp2))
+        ((Action a s, lm,le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot)))
       | e -> (e,Nothing) end
    | LEXP_field lexp id ->
      (match (create_write_message_or_update t_level value l_env l_mem false lexp) with
-     | ((Value (V_record fexps),lm,le),Just lexp_builder) ->
+     | ((Value (V_record t fexps),lm,le),Just lexp_builder) ->
        match (in_env fexps id,is_top_level) with
-       | (Just (V_boxref n),true) -> ((Value (V_lit L_unit), update_mem lm n value, l_env),Nothing)
-       | (Just (V_boxref n),false) -> ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_field (lexp_builder e) id))
-       | (Just v, true) -> ((Error "Field access requires record",lm,le),Nothing)
-       | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_field (lexp_builder e) id))
-       | (Nothing,_) -> ((Error "Field not found in specified record",lm,le),Nothing) end
+       | (Just (V_boxref n t),true) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
+       | (Just (V_boxref n t),false) -> 
+	 ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+       | (Just v, true) -> ((Error l "Field access requires record",lm,le),Nothing)
+       | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+       | (Nothing,_) -> ((Error l "Field not found in specified record",lm,le),Nothing) end
      | ((Action a s,lm,le), Just lexp_builder) ->  
        match a with
-       | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
-       | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
-       | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_field (lexp_builder e) id))
-       | _ -> ((Error "Unimplemented feature, writing to a field in a register or memory",lm,le),Nothing)
+       | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+       | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+       | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+       | _ -> ((Error l "Unimplemented feature, writing to a field in a register or memory",lm,le),Nothing)
        end 
      | e -> e end)
      end	
 
-and interp_letbind t_level l_env l_mem lbind =
+and interp_letbind t_level l_env l_mem (LB_aux lbind (l,annot)) =
   match lbind with
   | LB_val_explicit t pat exp ->
     match (interp_main t_level l_env l_mem exp) with
     | (Value v,lm,le) ->
       (match match_pattern pat v with
-      | (true,env) -> ((Value (V_lit L_unit), lm, env++l_env),Nothing)
-      | _ -> ((Error "Pattern in letbind did not match value",lm,le),Nothing) end)
-    | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> LB_val_explicit t pat e)))
+      | (true,env) -> ((Value (V_lit (L_aux L_unit l)), lm, env++l_env),Nothing)
+      | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
+    | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e ->(LB_aux (LB_val_explicit t pat e) (l,annot)))))
     | e -> (e,Nothing) end
   | LB_val_implicit pat exp ->
     match (interp_main t_level l_env l_mem exp) with
     | (Value v,lm,le) ->
       (match match_pattern pat v with
-      | (true,env) -> ((Value (V_lit L_unit), lm, env++l_env),Nothing)
-      | _ -> ((Error "Pattern in letbind did not match value",lm,le),Nothing) end)
-    | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> LB_val_implicit pat e)))
+      | (true,env) -> ((Value (V_lit (L_aux L_unit l)), lm, env++l_env),Nothing)
+      | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
+    | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) (l,annot)))))
     | e -> (e,Nothing) end
 end	
 
 let rec to_global_letbinds (Defs defs) t_level =
   let  (Env defs' externs lets regs mems ctors) = t_level in
   match defs with
-  | [] -> ((Value (V_lit L_unit), emem, []),t_level)
-  | def ::defs ->
+  | [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, []),t_level)
+  | (DEF_aux def (l,_))::defs ->
     match def with
     | DEF_val lbind ->
       match interp_letbind t_level [] emem lbind with
       | ((Value v,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' externs (lets++le) regs mems ctors)
-      | ((Action a s,lm,le),_) -> ((Error "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
+      | ((Action a s,lm,le),_) -> ((Error l "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
@@ -998,7 +1233,7 @@ let interp defs exp =
 
 let rec resume_main t_level stack value =
   match stack with
-  | Top -> Error "Top hit without place to put value"
+  | Top -> Error Unknown "Top hit without place to put value"
   | Frame id exp env mem Top -> 
     match interp_main t_level ((id,value)::env) mem exp with | (o,_,_) -> o end 
   | Frame id exp env mem stack ->
@@ -1006,7 +1241,7 @@ let rec resume_main t_level stack value =
     | Value v -> 
       match interp_main t_level ((id,v)::env) mem exp with | (o,_,_) -> o end 
     | Action action stack -> Action action (Frame id exp env mem stack)
-    | Error s -> Error s
+    | Error l s -> Error l s
     end  
   end
 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index aeb81085..b18d031e 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -8,51 +8,51 @@ open import Word
 
 let compose f g x = f (V_tuple [g x]) ;;
 
-let is_one (V_lit b) = V_lit (if b = L_one then L_true else L_false) ;;
+let is_one (V_lit (L_aux b lb)) = V_lit (L_aux (if b = L_one then L_true else L_false) lb) ;;
 
-let eq (V_tuple [x; y]) = V_lit (if x = y then L_true else L_false) ;;
+let eq (V_tuple [x; y]) = V_lit (L_aux (if x = y then L_true else L_false) Unknown) ;;
 
-let neg (V_tuple [V_lit arg]) = V_lit (match arg with
+let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
   | L_true -> L_false
-  | L_false -> L_true end) ;;
+  | L_false -> L_true end) la) ;;
 
 let neq = compose neg eq ;;
 
 let bit_to_bool b = match b with
-    V_lit L_zero -> false
-  | V_lit L_one -> true
+    V_lit (L_aux L_zero _) -> false
+  | V_lit (L_aux L_one _) -> true
   end ;;
 let bool_to_bit b = match b with
-    false -> V_lit L_zero
-  | true -> V_lit L_one
+    false -> V_lit (L_aux L_zero Unknown)
+  | true -> V_lit (L_aux L_one Unknown)
   end ;;
 
 (* XXX always interpret as positive ? *)
 let to_num_dec (V_vector idx false l) =
-  V_lit(L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool (reverse l)))));;
+  V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool (reverse l))))) Unknown);;
 let to_num_inc (V_vector idx true l) =
-  V_lit(L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool l))));;
+  V_lit(L_aux (L_num(naturalFromBitSeq (BitSeq Nothing false (map bit_to_bool l)))) Unknown);;
 
 (* XXX not quite sure about list reversal here - what is the convention for
  * V_vector? cf. above too *)
-let to_vec_dec len (V_lit(L_num n)) =
-  let BitSeq _ false l = bitSeqFromNatural len n in
+let to_vec_dec len (V_lit(L_aux (L_num n) ln)) =
+  let (BitSeq _ false l) = bitSeqFromNatural len n in
   V_vector 0 false (map bool_to_bit (reverse l)) ;;
-let to_vec_inc len (V_lit(L_num n)) =
-  let BitSeq _ false l = bitSeqFromNatural len n in
+let to_vec_inc len (V_lit(L_aux (L_num n) ln)) =
+  let (BitSeq _ false l) = bitSeqFromNatural len n in
   V_vector 0 true (map bool_to_bit l) ;;
 
 let rec add (V_tuple args) = match args with
   (* vector case *)
   | [(V_vector _ d l as v); (V_vector _ d' l' as v')] ->
-      let V_lit (L_num x) = (if d then to_num_inc else to_num_dec) v in
-      let V_lit (L_num y) = (if d' then to_num_inc else to_num_dec) v' in
+      let (V_lit (L_aux (L_num x) lx)) = (if d then to_num_inc else to_num_dec) v in
+      let (V_lit (L_aux (L_num y) ly)) = (if d' then to_num_inc else to_num_dec) v' in
       (* XXX how shall I decide this? max? max+1? *)
       let len = max (List.length l) (List.length l') in
       (* XXX assume d = d' *)
-      (if d then to_vec_inc else to_vec_dec) (Just len) (V_lit (L_num (x+y)))
+      (if d then to_vec_inc else to_vec_dec) (Just len) (V_lit (L_aux (L_num (x+y)) lx))
   (* integer case *)
-  | [V_lit(L_num x); V_lit(L_num y)] -> V_lit(L_num (x+y))
+  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (x+y)) lx)
   (* assume other literals are L_bin or L_hex, ie. vectors *)
   | [V_lit l; x ] -> add (V_tuple [litV_to_vec l; x])
   | [ x ; V_lit l ] -> add (V_tuple [x; litV_to_vec l])
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 98b8e6fe..19c27b56 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -19,18 +19,26 @@ let lit_to_string = function
 ;;
 
 let id_to_string = function
-  | Id s | DeIid s -> s
+  | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s
+;;
+
+let loc_to_string = function
+  | Unknown -> "Unknown"
+  | Trans(s,_) -> s
+  | Range(s,fline,fchar,tline,tchar) -> 
+    "in " ^ s ^ " from line " ^  (string_of_int fline) ^ " character " ^ (string_of_int fchar) ^ 
+      " to line " ^ (string_of_int tline) ^ " character " ^ (string_of_int tchar)
 ;;
 
 let bitvec_to_string l = "0b" ^ (String.concat "" (List.map (function
-  | V_lit(L_zero) -> "0"
-  | V_lit(L_one) -> "1"
+  | V_lit(L_aux(L_zero, _)) -> "0"
+  | V_lit(L_aux(L_one, _)) -> "1"
   | _ -> assert false) l))
 ;;
 
 let rec val_to_string = function
- | V_boxref n -> sprintf "boxref %d" n
- | V_lit l -> sprintf (*"literal %s" *) "%s" (lit_to_string l)
+ | V_boxref(n, t) -> sprintf "boxref %d" n
+ | V_lit (L_aux(l,_)) -> sprintf (*"literal %s" *) "%s" (lit_to_string l)
  | V_tuple l ->
      let repr = String.concat ", " (List.map val_to_string l) in
      sprintf "tuple <%s>" repr
@@ -43,11 +51,11 @@ let rec val_to_string = function
        try bitvec_to_string l
        with Failure _ -> String.concat "; " (List.map val_to_string l) in
      sprintf "vector [%s] (%s, from %s)" repr order (string_of_big_int first_index)
- | V_record l ->
+ | V_record(_, l) ->
      let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string value) in
      let repr = String.concat "; " (List.map  pp l) in
      sprintf "record {%s}" repr
- | V_ctor (id, value) ->
+ | V_ctor (id,_, value) ->
      sprintf "constructor %s %s" (id_to_string id) (val_to_string value)
 ;;
 
@@ -82,15 +90,22 @@ let act_to_string = function
      sprintf "extern call %s applied to %s" name (val_to_string arg)
 ;;
 
+let id_compare i1 i2 = 
+  match (i1, i2) with 
+    | (Id_aux(Id(i1),_),Id_aux(Id(i2),_)) 
+    | (Id_aux(Id(i1),_),Id_aux(DeIid(i2),_)) 
+    | (Id_aux(DeIid(i1),_),Id_aux(Id(i2),_))
+    | (Id_aux(DeIid(i1),_),Id_aux(DeIid(i2),_)) -> compare i1 i2
+
 module Reg = struct
-  include Map.Make(struct type t = id let compare = compare end)
+  include Map.Make(struct type t = id let compare = id_compare end)
 end ;;
 
 module Mem = struct
   include Map.Make(struct
     type t = (id * big_int)
     let compare (i1, v1) (i2, v2) =
-      match compare i1 i2 with
+      match id_compare i1 i2 with
       | 0 -> compare_big_int v1 v2
       | n -> n
     end)
@@ -114,22 +129,22 @@ let vconcat v v' = vec_concat (V_tuple [v; v']) ;;
 let perform_action ((reg, mem) as env) = function
  | Read_reg ((Reg (id, _) | SubReg (id, _, _)), sub) ->
      slice (Reg.find id reg) sub, env
- | Read_mem (id, V_lit(L_num n), sub) ->
+ | Read_mem (id, V_lit(L_aux((L_num n),_)), sub) ->
      slice (Mem.find (id, n) mem) sub, env
  | Write_reg ((Reg (id, _) | SubReg (id, _, _)), None, value) ->
-     V_lit L_unit, (Reg.add id value reg, mem)
+     V_lit (L_aux(L_unit,Interp_ast.Unknown)), (Reg.add id value reg, mem)
  | Write_reg ((Reg (id, _) | SubReg (id, _, _)), Some (start, stop), value) ->
      (* XXX if updating a single element, wrap value into a vector -
       * should the typechecker do that coercion for us automatically? *)
      let value = if eq_big_int start stop then V_vector (zero_big_int, true, [value]) else value in
      let old_val = Reg.find id reg in
      let new_val = fupdate_vector_slice old_val value start stop in
-     V_lit L_unit, (Reg.add id new_val reg, mem)
- | Write_mem (id, V_lit(L_num n), None, value) ->
-     V_lit L_unit, (reg, Mem.add (id, n) value mem)
+     V_lit (L_aux(L_unit,Interp_ast.Unknown)), (Reg.add id new_val reg, mem)
+ | Write_mem (id, V_lit(L_aux(L_num n,_)), None, value) ->
+     V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, Mem.add (id, n) value mem)
  (* multi-byte accesses to memory *)
  (* XXX this doesn't deal with endianess at all *)
- | Read_mem (id, V_tuple [V_lit(L_num n); V_lit(L_num size)], sub) ->
+ | Read_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], sub) ->
      let rec fetch k acc =
        if eq_big_int k size then slice acc sub else
          let slice = Mem.find (id, add_big_int n k) mem in
@@ -139,7 +154,7 @@ let perform_action ((reg, mem) as env) = function
  (* XXX no support for multi-byte slice write at the moment - not hard to add,
   * but we need a function basic read/write first since slice access involves
   * read, fupdate, write. *)
- | Write_mem (id, V_tuple [V_lit(L_num n); V_lit(L_num size)], None, V_vector (m, inc, vs)) ->
+ | Write_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], None, V_vector (m, inc, vs)) ->
      (* normalize input vector so that it is indexed from 0 - for slices *)
      let value = V_vector (zero_big_int, inc, vs) in
      (* assumes smallest unit of memory is 8 bit *)
@@ -151,15 +166,15 @@ let perform_action ((reg, mem) as env) = function
          let slice = slice_vector value n1 n2 in
          let mem' = Mem.add (id, add_big_int n k) slice mem in
          update (succ_big_int k) mem'
-     in V_lit L_unit, (reg, update zero_big_int mem)
+     in V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, update zero_big_int mem)
  (* This case probably never happens in the POWER spec anyway *)
- | Write_mem (id, V_lit(L_num n), Some (start, stop), value) ->
+ | Write_mem (id, V_lit(L_aux(L_num n,_)), Some (start, stop), value) ->
      (* XXX if updating a single element, wrap value into a vector -
       * should the typechecker do that coercion for us automatically? *)
      let value = if eq_big_int start stop then V_vector (zero_big_int, true, [value]) else value in
      let old_val = Mem.find (id, n) mem in
      let new_val = fupdate_vector_slice old_val value start stop in
-     V_lit L_unit, (reg, Mem.add (id, n) new_val mem)
+     V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, Mem.add (id, n) new_val mem)
  | Call_extern (name, arg) -> eval_external name arg, env
  | _ -> assert false
 ;;
@@ -174,8 +189,8 @@ let run (name, test) =
       let return, env' = perform_action env a in
       eprintf "%s: action returned %s\n" name (val_to_string return);
       loop env' (resume test s return)
-  | Error e -> eprintf "%s: error: %s\n" name e; false in
-  let entry = E_app((Id "main"), [E_lit L_unit]) in
+  | Error(l, e) -> eprintf "%s: %s: error: %s\n" name (loc_to_string l) e; false in
+  let entry = E_aux(E_app(Id_aux((Id "main"),Unknown), [E_aux(E_lit (L_aux(L_unit,Unknown)),(Unknown,None))]),(Unknown,None)) in
   eprintf "%s: starting\n" name;
   try
     Printexc.record_backtrace true;
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 236bfc91..4190ad9b 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1,3 +1,4 @@
+open Type_internal
 open Ast
 open Format
 
@@ -349,86 +350,115 @@ let pp_defs ppf (Defs(defs)) =
 
 
 (****************************************************************************
- * source to Lem ast pretty printer
+ * annotated source to Lem ast pretty printer
 ****************************************************************************)
 
-let pp_format_id_lem (Id_aux(i,_)) =
-  match i with
-  | Id(i) -> "(Id \"" ^ i ^ "\")"
-  | DeIid(x) -> "(DeIid \"" ^ x ^ "\")"
+let rec pp_format_l_lem = function
+  | Parse_ast.Unknown -> "Unknown"
+  | Parse_ast.Trans(s,None) -> "(Trans \"" ^ s ^ "\" Nothing)"
+  | Parse_ast.Trans(s,(Some l)) -> "(Trans \"" ^  s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))"
+  | Parse_ast.Range(p1,p2) -> "(Range \"" ^ p1.Lexing.pos_fname ^ "\" " ^
+                               (string_of_int p1.Lexing.pos_lnum) ^ " " ^ 
+                               (string_of_int (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) ^ " " ^
+                               (string_of_int p2.Lexing.pos_lnum) ^ " " ^
+                               (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")"
+
+let pp_lem_l ppf l = base ppf (pp_format_l_lem l)
+
+let pp_format_id_lem (Id_aux(i,l)) =
+  "(Id_aux " ^
+    (match i with
+      | Id(i) -> "(Id \"" ^ i ^ "\")"
+      | DeIid(x) -> "(DeIid \"" ^ x ^ "\")") ^ " " ^
+   (pp_format_l_lem l) ^ ")"
 
 let pp_lem_id ppf id = base ppf (pp_format_id_lem id)
 
-let pp_format_var_lem (Kid_aux(Var v,_)) = "(Var \"" ^ v ^ "\")"
+let pp_format_var_lem (Kid_aux(Var v,l)) = "(Kid_aux (Var \"" ^ v ^ "\") " ^ (pp_format_l_lem l) ^ ")"
 
 let pp_lem_var ppf var = base ppf (pp_format_var_lem var)
 
-let pp_format_bkind_lem (BK_aux(k,_)) =
-  match k with
-  | BK_type -> "BK_type"
-  | BK_nat -> "BK_nat"
-  | BK_order -> "BK_order"
-  | BK_effect -> "BK_effect"
+let pp_format_bkind_lem (BK_aux(k,l)) =
+  "(BK_aux " ^
+  (match k with
+    | BK_type -> "BK_type"
+    | BK_nat -> "BK_nat"
+    | BK_order -> "BK_order"
+    | BK_effect -> "BK_effect") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
 
 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_lem klst ^ "])"
+let pp_format_kind_lem (K_aux(K_kind(klst),l)) = 
+  "(K_aux (K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "]) " ^ (pp_format_l_lem l) ^ ")"
 
 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
-  | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")"
-  | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")"
-  | 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_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
-  | Typ_wild -> "Typ_wild"
-and pp_format_nexp_lem (Nexp_aux(n,_)) = 
-  match n with
-  | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
-  | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
-  | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
-  | Nexp_times(n1,n2) -> "(Nexp_times " ^  (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
-  | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")"
-and pp_format_ord_lem (Ord_aux(o,_)) = 
-  match o with
-  | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")"
-  | Ord_inc -> "Ord_inc"
-  | Ord_dec -> "Ord_dec"  
-and pp_format_effects_lem (Effect_aux(e,_)) =
-  match e with
+let rec pp_format_typ_lem (Typ_aux(t,l)) =
+  "(Typ_aux " ^
+  (match t with
+    | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")"
+    | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")"
+    | 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_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
+    | Typ_wild -> "Typ_wild") ^ " " ^
+    (pp_format_l_lem l) ^ ")"
+and pp_format_nexp_lem (Nexp_aux(n,l)) = 
+  "(Nexp_aux " ^
+  (match n with
+    | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
+    | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
+    | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+    | Nexp_times(n1,n2) -> "(Nexp_times " ^  (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+    | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^
+    (pp_format_l_lem l) ^ ")"
+and pp_format_ord_lem (Ord_aux(o,l)) = 
+  "(Ord_aux " ^ 
+  (match o with
+    | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")"
+    | Ord_inc -> "Ord_inc"
+    | Ord_dec -> "Ord_dec") ^ " " ^
+   (pp_format_l_lem l) ^ ")"
+and pp_format_base_effect_lem (BE_aux(e,l)) =
+  "(BE_aux " ^
+  (match e with
+    | BE_rreg -> "BE_rreg"
+    | BE_wreg -> "BE_wreg"
+    | BE_rmem -> "BE_rmem"
+    | BE_wmem -> "BE_wmem"
+    | BE_undef -> "BE_undef"
+    | BE_unspec -> "BE_unspec"
+    | BE_nondet -> "BE_nondet") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
+and pp_format_effects_lem (Effect_aux(e,l)) =
+  "(Effect_aux " ^
+  (match e with
   | Effect_var(v) -> "(Effect_var " ^ pp_format_var v ^ ")"
   | Effect_set(efcts) ->
     "(Effect_set [" ^
-      (list_format "; " 
-         (fun (BE_aux(e,l)) ->
-	   match e with
-	   | BE_rreg -> "BE_rreg"
-	   | BE_wreg -> "BE_wreg"
-	   | BE_rmem -> "BE_rmem"
-	   | BE_wmem -> "BE_wmem"
-	   | BE_undef -> "BE_undef"
-	   | BE_unspec -> "BE_unspec"
-	   | BE_nondet -> "BE_nondet")
-	 efcts) ^ " ])"
-and pp_format_typ_arg_lem (Typ_arg_aux(t,_)) = 
-  match t with
+      (list_format "; " pp_format_base_effect_lem efcts) ^ " ])") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
+and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) = 
+  "(Typ_arg_aux " ^
+  (match t with
   | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
   | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
   | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")"
-  | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")"
+  | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
 
 let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t)
 let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n)
 let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o)
 let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e)
+let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be)
 
-let pp_format_nexp_constraint_lem (NC_aux(nc,_)) =
-  match nc with
+let pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
+  "(NC_aux " ^
+  (match nc with
   | 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 ^ ")"
@@ -436,38 +466,46 @@ let pp_format_nexp_constraint_lem (NC_aux(nc,_)) =
     pp_format_var_lem id ^
       " [" ^
       list_format "; " string_of_int bounds ^
-      "])"
+      "])") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
 
 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
+let pp_format_qi_lem (QI_aux(qi,lq)) =
+  "(QI_aux " ^ 
+  (match qi with
   | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint_lem n_const ^ ")"
-  | QI_id(KOpt_aux(ki,_)) ->
-    "(QI_id " ^
+  | QI_id(KOpt_aux(ki,lk)) ->
+    "(QI_id (KOpt_aux " ^
     (match ki with
     | KOpt_none(var) -> "(KOpt_none " ^ pp_format_var_lem var ^ ")"
-    | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ ")"
+    | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ " " ^
+      (pp_format_l_lem lk) ^ "))") ^ " " ^ 
+  (pp_format_l_lem lq) ^ ")"
 
 let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi)
 
-let pp_format_typquant_lem (TypQ_aux(tq,_)) =
-  match tq with
+let pp_format_typquant_lem (TypQ_aux(tq,l)) =
+  "(TypQ_aux " ^ 
+  (match tq with
   | TypQ_no_forall -> "TypQ_no_forall"
   | TypQ_tq(qlist) ->
     "(TypQ_tq [" ^ 
     (list_format "; " pp_format_qi_lem qlist) ^
-    "])"
+    "])") ^ " " ^ 
+  (pp_format_l_lem l) ^ ")"
 
 let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq)
 
-let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  "(TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ")"
+let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),l)) =
+  "(TypSchm_aux (TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ") " ^
+                (pp_format_l_lem l) ^ ")"
  
 let pp_lem_typscm ppf ts = base ppf (pp_format_typscm_lem ts)
 
-let pp_format_lit_lem (L_aux(l,_)) =
-  match l with
+let pp_format_lit_lem (L_aux(lit,l)) =
+  "(L_aux " ^
+  (match lit with
   | L_unit -> "L_unit"
   | L_zero -> "L_zero"
   | L_one -> "L_one"
@@ -477,12 +515,81 @@ let pp_format_lit_lem (L_aux(l,_)) =
   | L_hex(n) -> "(L_hex \"" ^ n ^ "\")"
   | L_bin(n) -> "(L_bin \"" ^ n ^ "\")"
   | L_undef -> "L_undef"
-  | L_string(s) -> "(L_string \"" ^ s ^ "\")" 
+  | L_string(s) -> "(L_string \"" ^ s ^ "\")") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
 
 let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l)
 
-let rec pp_format_pat_lem (P_aux(p,l)) =
-  match p with
+
+let rec pp_format_t t =
+  match t.t with
+    | Tid i -> "(T_id (Id_aux (Id \"" ^ i ^ "\") Unknown))"
+    | Tvar i -> "(T_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+    | Tfn(t1,t2,e) -> "(T_fn " ^ (pp_format_t t1) ^ " " ^ (pp_format_t t2) ^ " " ^ pp_format_e e ^ ")"
+    | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])"
+    | Tapp(i,args) -> "(T_app (Id_aux (Id \"" ^ i ^ "\") Unknown) (T_args [" ^  list_format "; " pp_format_targ args ^ "]))"
+    | Tuvar(_) -> "(T_var (Kid_aux (Var \"fresh_v\") Unknown))"
+and pp_format_targ = function
+  | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")"
+  | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")"
+  | TA_eft e -> "(T_arg_effect " ^ pp_format_e e ^ ")"
+  | TA_ord o -> "(T_arg_order " ^ pp_format_o o ^ ")"
+and pp_format_n n =
+  match n.nexp with
+    | Nvar i -> "(Ne_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+    | Nconst i -> "(Ne_const " ^ string_of_int i ^ ")"
+    | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])"
+    | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
+    | N2n n -> "(Ne_exp " ^ (pp_format_n n) ^ ")"
+    | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")"
+    | Nuvar(_) -> "(Ne_var (Kid_aux (Var \"fresh_v\") Unknown))"
+and pp_format_e e = 
+  "(Effect_aux " ^
+  (match e.effect with
+  | Evar i -> "(Effect_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+  | Eset es -> "(Effect_set [" ^
+                  (list_format "; " pp_format_base_effect_lem es) ^ " ])"
+  | Euvar(_) -> "(Effect_var (Kid_aux (Var \"fresh_v\") Unknown))")
+  ^ " Unknown)"
+and pp_format_o o = 
+  "(Ord_aux " ^ 
+  (match o.order with
+  | Ovar i -> "(Ord_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+  | Oinc -> "Ord_inc"
+  | Odec -> "Ord_dec"
+  | Ouvar(_) -> "(Ord_var (Kid_aux (Var \"fresh_v\") Unknown))")
+  ^ " Unknown)"
+
+let pp_format_tag = function
+  | Emp -> "Tag_empty"
+  | External (Some s) -> "(Tag_extern (Just \""^s^"\"))"
+  | External None -> "(Tag_extern Nothing)"
+  | Default -> "Tag_default"
+  | Constructor -> "Tag_ctor"
+  | Enum -> "Tag_enum"
+  | Spec -> "Tag_spec"
+
+let pp_format_nes nes = 
+  "[" ^ 
+  (list_format "; "
+     (fun ne -> match ne with
+       | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
+       | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
+       | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
+       | In(_,i,ns) -> "(Nec_in (Kid_aux (Var \"" ^ i ^ "\") Unknown) [" ^ (list_format "; " string_of_int ns)^ "])")
+     nes) ^ "]"
+
+let pp_format_annot = function
+  | None -> "Nothing"
+  | Some((_,t),tag,nes,efct) -> 
+    "(Just (" ^ pp_format_t t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ pp_format_e efct ^ "))"
+
+let pp_annot ppf ant = base ppf (pp_format_annot ant)
+
+
+let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
+  "(P_aux " ^
+  (match p with
   | P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")"
   | P_wild -> "P_wild"
   | P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")"
@@ -499,156 +606,182 @@ let rec pp_format_pat_lem (P_aux(p,l)) =
     "(P_vector_indexed [" ^ list_format "; " (fun (i,p) -> Printf.sprintf "(%d, %s)" i (pp_format_pat_lem p)) ipats ^ "])"
   | P_vector_concat(pats) -> "(P_vector_concat [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
   | P_tup(pats) -> "(P_tup [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
-  | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
+  | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])") ^ 
+  " (" ^ pp_format_l_lem l ^ ", " ^ pp_format_annot annot ^ "))"
 
 let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p)
 
-let rec pp_lem_let ppf (LB_aux(lb,_)) =
-  match lb with
-  | LB_val_explicit(ts,pat,exp) -> 
-    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp
-  | LB_val_implicit(pat,exp) -> 
-    fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat  pp_lem_exp exp
-
-and pp_lem_exp ppf (E_aux(e,_)) = 
-  match e with
-  | E_block(exps) -> fprintf ppf "@[<0>%a [%a] %a@]"
+let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) =
+  let print_lb ppf lb = 
+    match lb with
+      | LB_val_explicit(ts,pat,exp) -> 
+	fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp
+      | LB_val_implicit(pat,exp) -> 
+	fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat  pp_lem_exp exp in
+  fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot
+
+and pp_lem_exp ppf (E_aux(e,(l,annot))) = 
+  let print_e ppf e = 
+    match e with
+      | E_block(exps) -> fprintf ppf "@[<0>%a [%a] %a@]"
                                  kwd "(E_block" 
                                  (list_pp pp_semi_lem_exp pp_lem_exp) exps
                                  kwd ")"
-  | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
-  | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
-  | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp 
-  | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
-  | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
-  | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
-  | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
-  | E_for(id,exp1,exp2,exp3,order,exp4) ->
-    fprintf ppf "@[<0>(%a %a %a %a %a %a @ @[<1> %a @])@]" 
-      kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4
-  | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps
-  | E_vector_indexed(iexps) -> 
-    let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
-    let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
-    fprintf ppf "@[<0>(%a [%a]) @]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps
-  | E_vector_access(v,e) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e
-  | E_vector_subrange(v,e1,e2) -> 
-    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e1 
-  | E_vector_update(v,e1,e2) -> 
-    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2
-  | E_vector_update_subrange(v,e1,e2,e3) -> 
-    fprintf ppf "@[<0>(%a %a %a %a %a)@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 
-  | E_list(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps
-  | E_cons(e1,e2) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2
-  | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> 
-    fprintf ppf "@[<0>(%a [%a]))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
-  | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) ->
-    fprintf ppf "@[<0>(%a %a (%a [%a]))@]" 
-      kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps 
-  | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id
-  | E_case(exp,pexps) -> 
-    fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps
-  | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp
-  | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp
+      | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
+      | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
+      | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp 
+      | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
+      | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
+      | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
+      | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
+      | E_for(id,exp1,exp2,exp3,order,exp4) ->
+	fprintf ppf "@[<0>(%a %a %a %a %a %a @ @[<1> %a @])@]" 
+	  kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4
+      | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps
+      | E_vector_indexed(iexps) -> 
+	let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
+	let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
+	fprintf ppf "@[<0>(%a [%a]) @]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps
+      | E_vector_access(v,e) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e
+      | E_vector_subrange(v,e1,e2) -> 
+	fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e1 
+      | E_vector_update(v,e1,e2) -> 
+	fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2
+      | E_vector_update_subrange(v,e1,e2,e3) -> 
+	fprintf ppf "@[<0>(%a %a %a %a %a)@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 
+      | E_list(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps
+      | E_cons(e1,e2) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2
+      | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> 
+	fprintf ppf "@[<0>(%a [%a]))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
+      | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) ->
+	fprintf ppf "@[<0>(%a %a (%a [%a]))@]" 
+	  kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps 
+      | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id
+      | E_case(exp,pexps) -> 
+	fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps
+      | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp
+      | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp
+  in
+  fprintf ppf "@[<0>(E_aux %a (%a, %a))@]" print_e e pp_lem_l l pp_annot annot
 
 and pp_semi_lem_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_lem_exp e kwd ";"
 
-and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),_)) = fprintf ppf "@[<1>(%a %a %a)@]" kwd "FE_Fexp" pp_lem_id id pp_lem_exp exp
+and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),(l,annot))) = 
+  fprintf ppf "@[<1>(FE_aux (%a %a %a) (%a, %a))@]" kwd "FE_Fexp" pp_lem_id id pp_lem_exp exp pp_lem_l l pp_annot annot
 and pp_semi_lem_fexp ppf fexp = fprintf ppf "@[<1>%a %a@]" pp_lem_fexp fexp kwd ";"
 
-and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),_)) = 
-  fprintf ppf "@[<1>(%a %a@ %a)@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp
+and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),(l,annot))) = 
+  fprintf ppf "@[<1>(Pat_aux (%a %a@ %a) (%a, %a))@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot
 and pp_semi_lem_case ppf case = fprintf ppf "@[<1>%a %a@]" pp_lem_case case kwd ";"
 
-and pp_lem_lexp ppf (LEXP_aux(lexp,_)) =
-  match lexp with
-  | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
-  | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
-  | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
-  | LEXP_vector_range(v,e1,e2) -> 
-    fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v  pp_lem_exp e1 pp_lem_exp e2
-  | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id
-
-let pp_lem_default ppf (DT_aux(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
-
-let pp_lem_spec ppf (VS_aux(v,_)) =
-  match v with
-  | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
-  | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s
-  | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id
-
-let pp_lem_namescm ppf (Name_sect_aux(ns,_)) =
+and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) =
+  let print_le ppf lexp = 
+    match lexp with
+      | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
+      | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
+      | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
+      | LEXP_vector_range(v,e1,e2) -> 
+	fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v  pp_lem_exp e1 pp_lem_exp e2
+      | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id
+  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 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
+
+let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
+  let print_spec ppf v =
+    match v with
+      | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
+      | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s
+      | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id
+  in
+  fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot
+
+let pp_lem_namescm ppf (Name_sect_aux(ns,l)) =
   match ns with
-  | Name_sect_none -> fprintf ppf "Name_sect_none"
-  | Name_sect_some(s) -> fprintf ppf "(%a \"%s\")" kwd "Name_sect_some" s
+  | Name_sect_none -> fprintf ppf "(Name_sect_aux Name_sect_none %a)" pp_lem_l l
+  | Name_sect_some(s) -> fprintf ppf "(Name_sect_aux (Name_sect_some \"%s\") %a)" s pp_lem_l l
 
-let rec pp_lem_range ppf (BF_aux(r,_)) =
+let rec pp_lem_range ppf (BF_aux(r,l)) =
   match r with 
-  | BF_single(i) -> fprintf ppf "(BF_single %i)" i
-  | BF_range(i1,i2) -> fprintf ppf "(BF_range %i %i)" i1 i2
-  | BF_concat(ir1,ir2) -> fprintf ppf "(%a %a %a)" kwd "BF_concat" pp_lem_range ir1 pp_lem_range ir2
-
-let pp_lem_typdef ppf (TD_aux(td,_)) =
-  match td with
-  | TD_abbrev(id,namescm,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] 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 (Tu_aux(typ_u,_)) = 
-      match typ_u with
-      | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_ty_id %a %a);@]" pp_lem_typ typ pp_lem_id id 
-      | Tu_id(id) -> fprintf ppf "@[<1>(Tu_id %a);@]" pp_lem_id id
-    in
-    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] 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])@]"
-     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,_)) =
+  | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" i pp_lem_l l
+  | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" i1 i2 pp_lem_l l
+  | BF_concat(ir1,ir2) -> fprintf ppf "(BF_aux (BF_concat %a %a) %a)" pp_lem_range ir1 pp_lem_range ir2 pp_lem_l l
+
+let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
+  let print_td ppf td = 
+    match td with
+      | TD_abbrev(id,namescm,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] 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 (Tu_aux(typ_u,l)) = 
+	  match typ_u with
+	    | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]" 
+	                          pp_lem_typ typ pp_lem_id id pp_lem_l l
+	    | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l
+	in
+	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] 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])@]"
+	  kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
+  in
+  fprintf ppf "@[<0>(TD_aux %a (%a, %a))@]" print_td td pp_lem_l l pp_annot annot
+
+let pp_lem_rec ppf (Rec_aux(r,l)) =
   match r with
-  | Rec_nonrec -> fprintf ppf "Rec_nonrec"
-  | Rec_rec -> fprintf ppf "Rec_rec"
-
-let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,_)) =
+  | Rec_nonrec -> fprintf ppf "(Rec_aux Rec_nonrec %a)" pp_lem_l l
+  | Rec_rec -> fprintf ppf "(Rec_aux Rec_rec %a)" pp_lem_l l
+  
+let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,l)) =
   match t with
-  | Typ_annot_opt_some(tq,typ) -> fprintf ppf "(Typ_annot_opt_some %a %a)" pp_lem_typquant tq pp_lem_typ typ
+  | Typ_annot_opt_some(tq,typ) -> 
+    fprintf ppf "(Typ_annot_opt_aux (Typ_annot_opt_some %a %a) %a)" pp_lem_typquant tq pp_lem_typ typ pp_lem_l l
 
-let pp_lem_effects_opt ppf (Effect_opt_aux(e,_)) =
+let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) =
   match e with
-  | Effect_opt_pure -> fprintf ppf "Effect_opt_pure"
-  | Effect_opt_effect e -> fprintf ppf "(Effect_opt_effect %a)" pp_lem_effects e
+  | 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),_)) =
-  fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp 
+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_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) =
+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
-  fprintf ppf "@[<0>(%a %a %a %a [%a])@]" 
+  fprintf ppf "@[<0>(FD_aux (%a %a %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);@\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")
+    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_defs ppf (Defs(defs)) =
   fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs
diff --git a/src/process_file.ml b/src/process_file.ml
index 25fbe49b..592c8cf5 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -159,6 +159,7 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
 	  let (o, ext_o) = open_output_with_check (f' ^ ".lem") in
 	  Format.fprintf o "(* %s *)@\n" (generated_line filename);
           Format.fprintf o "open import Interp_ast@\n";
+	  Format.fprintf o "open import Pervasives@\n";
           Format.fprintf o "let defs = ";
 	  Pretty_print.pp_lem_defs o defs;
 	  close_output_with_check ext_o
diff --git a/src/test/vectors.sail b/src/test/vectors.sail
index 70cc5973..482ef902 100644
--- a/src/test/vectors.sail
+++ b/src/test/vectors.sail
@@ -2,6 +2,9 @@ let (bit[32]) v = 0b101
 let (bit[4]) v2 = [0,1,0,0]
 register (bit[32]) i
 
+let (bit[10]) v3 = 0b0101010111
+register (bit[5]) slice_check
+
 register nat match_success
 
 function unit decode ([bitzero, bitzero, bitone, bitzero]) = match_success := 1
@@ -9,6 +12,10 @@ and decode x = match_success := x
 
 function bit main _ = {
 
+  slice_check := v3;
+  slice_check := v3[1..10];
+  slice_check := v3[5..10];
+
   i := [bitzero, bitzero, bitone, bitzero];
 
   (* literal match *)
diff --git a/src/type_check.ml b/src/type_check.ml
index a75c690f..e5211d72 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -377,12 +377,12 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
         (match t.t,expect_t.t with 
         | Tfn _,_ -> typ_error l ("Identifier " ^ (id_to_string id) ^ " is bound to a function and cannot be used as a value")
         | Tapp("register",[TA_typ(t')]),Tapp("register",[TA_typ(expect_t')]) -> 
-          let tannot = Some(([],t),External,cs,ef) in
+          let tannot = Some(([],t),External (Some "register"),cs,ef) in
           let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t' in
           (e',t',t_env,cs@cs',ef)
         | Tapp("register",[TA_typ(t')]),_ ->
 	  let ef' = add_effect (BE_aux(BE_rreg,l)) ef in
-          let tannot = Some(([],t),External,cs,ef') in
+          let tannot = Some(([],t),External (Some "register"),cs,ef') in
           let t',cs',e' = type_coerce l d_env t' (rebuild tannot) expect_t in
           (e',t',t_env,cs@cs',ef)
         | Tapp("reg",[TA_typ(t)]),_ ->
@@ -456,13 +456,13 @@ let rec check_exp envs expect_t (E_aux(e,(l,annot)) : tannot exp) : (tannot exp
             let (ret_t,cs_r,e') = type_coerce l d_env ret (rebuild (Some(([],ret),tag,cs@cs',ef))) expect_t in
             (e',ret_t,t_env,cs@cs'@cs_r,ef)
           | [parm] ->
-            let (parm',arg_t,t_env,cs',ef') = check_exp envs arg parm in
-            let (ret_t,cs_r',e') = type_coerce l d_env ret (E_aux(E_app(id,[parm']),(l,(Some(([],ret),tag,cs,ef))))) expect_t in
-            (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef ef')
+            let (parm',arg_t,t_env,cs',ef_p) = check_exp envs arg parm in
+            let (ret_t,cs_r',e') = type_coerce l d_env ret (E_aux(E_app(id,[parm']),(l,(Some(([],ret),tag,cs,ef'))))) expect_t in
+            (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef_p ef')
           | parms -> 
-            let ((E_aux(E_tuple parms',tannot')),arg_t,t_env,cs',ef') = check_exp envs arg (E_aux(E_tuple parms,(l,None))) in
-            let (ret_t,cs_r',e') = type_coerce l d_env ret (E_aux(E_app(id, parms'),(l,(Some(([],ret),tag,cs,ef))))) expect_t in
-            (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef ef'))
+            let ((E_aux(E_tuple parms',tannot')),arg_t,t_env,cs',ef_p) = check_exp envs arg (E_aux(E_tuple parms,(l,None))) in
+            let (ret_t,cs_r',e') = type_coerce l d_env ret (E_aux(E_app(id, parms'),(l,(Some(([],ret),tag,cs,ef'))))) expect_t in
+            (e',ret_t,t_env,cs@cs'@cs_r',union_effects ef_p ef'))
         | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
       | _ -> typ_error l ("Unbound function " ^ i)) 
     | E_app_infix(lft,op,rht) -> 
@@ -866,7 +866,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
 	  (match t.t with
 	    | Tapp("register",[TA_typ u]) ->
 	      let ef = {effect=Eset[BE_aux(BE_wreg,l)]} in
-	      (LEXP_aux(lexp,(l,(Some(([],t),External,cs,ef)))),u,Envmap.empty,External,[],ef)
+	      (LEXP_aux(lexp,(l,(Some(([],t),External (Some "register"),cs,ef)))),u,Envmap.empty,External (Some "register"),[],ef)
 	    | Tapp("reg",[TA_typ u]) ->
 	      (LEXP_aux(lexp,(l,(Some(([],t),Emp,cs,pure_e)))),u,Envmap.empty,Emp,[],pure_e)
 	    | _ -> 
@@ -881,7 +881,7 @@ and check_lexp envs (LEXP_aux(lexp,(l,annot))) : (tannot lexp * typ * tannot ema
       let i = id_to_string id in
       (match Envmap.apply t_env i with
 	| Some(Some((parms,t),tag,cs,ef)) ->
-	  let is_external = match tag with | External -> true | _ -> false in
+	  let is_external = match tag with | External any -> true | _ -> false in
 	  let t,cs,ef = subst parms t cs ef in
 	  let t,cs,ef = match get_abbrev d_env t with
 	    | None -> t,cs,ef
@@ -1109,11 +1109,11 @@ 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))))
     | VS_extern_no_rename(typs,id) ->
-      let tannot = typschm_to_tannot envs typs External in
+      let tannot = typschm_to_tannot envs typs (External None) in
       (VS_aux(vs,(l,tannot)),
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
     | VS_extern_spec(typs,id,s) ->
-      let tannot = typschm_to_tannot envs typs External in
+      let tannot = typschm_to_tannot envs typs (External (Some s)) in
       (VS_aux(vs,(l,tannot)),
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
 
@@ -1141,7 +1141,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
 	| None -> Some(id_to_string id)) funcls None in
   let in_env = Envmap.apply t_env id in 
   let ret_t,param_t,tannot = match tannotopt with
-    | Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),(l',annot')) ->
+    | Typ_annot_opt_aux(Typ_annot_opt_some(typq,typ),l') ->
       let (ids,constraints) = typq_to_params envs typq in
       let t = typ_to_t typ in
       let p_t = new_t () in
@@ -1190,8 +1190,9 @@ let check_def envs (DEF_aux(def,(l,annot))) =
 			     (DEF_aux((DEF_default(ds)),(l,annot)),envs)
     | DEF_reg_dec(typ,id) -> 
       let t = (typ_to_t typ) in
-      let tannot = into_register (Some(([],t),External,[],pure_e)) in 
-      (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env ((id_to_string id),tannot))))
+      let i = id_to_string id in
+      let tannot = into_register (Some(([],t),External (Some i),[],pure_e)) in 
+      (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env (i,tannot))))
 
 
 (*val check : envs ->  tannot defs -> tannot defs*)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index f43b797c..73bd5bc4 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -59,7 +59,7 @@ and t_arg =
 
 type tag =
   | Emp
-  | External
+  | External of string option
   | Default
   | Constructor
   | Enum
@@ -198,11 +198,11 @@ let nat_typ = {t=Tid "nat"}
 let pure_e = {effect=Eset []}
 let initial_typ_env =
   Envmap.from_list [
-    ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,{effect=Evar "b"})}),External,[],pure_e));
-    ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e));
-    ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e));
-    ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External,[],pure_e));
-    ("|",Some(([],{t= Tfn ({t=Ttup([bit_t;bit_t])},bit_t,pure_e)}),External,[],pure_e));
+    ("ignore",Some(([("a",{k=K_Typ});("b",{k=K_Efct})],{t=Tfn ({t=Tvar "a"},unit_t,{effect=Evar "b"})}),External None,[],pure_e));
+    ("+",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "add"),[],pure_e));
+    ("*",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "multiply"),[],pure_e));
+    ("-",Some(([],{t= Tfn ({t=Ttup([nat_typ;nat_typ])},nat_typ,pure_e)}),External (Some "minus"),[],pure_e));
+    ("|",Some(([],{t= Tfn ({t=Ttup([bit_t;bit_t])},bit_t,pure_e)}),External (Some "bitwise_or"),[],pure_e));
   ]
 
 let initial_abbrev_env =
@@ -308,6 +308,21 @@ and o_to_string o =
   | Odec -> "dec"
   | Ouvar({oindex=i;osubst=a}) -> string_of_int i ^ "()"
 
+let tag_to_string = function
+  | Emp -> "Emp"
+  | External None -> "External" 
+  | External (Some s) -> "External " ^ s
+  | Default -> "Default"
+  | Constructor -> "Constructor"
+  | Enum -> "Enum"
+  | Spec -> "Spec"
+
+
+let tannot_to_string = function
+  | None -> "No tannot"
+  | Some((vars,t),tag,ncs,ef) ->
+    "Tannot: type = " ^ (t_to_string t) ^ " tag = " ^ tag_to_string tag ^ " constraints = not printing effect = " ^ e_to_string ef
+
 let get_abbrev d_env t =
   match t.t with
     | Tid i ->
@@ -479,11 +494,11 @@ let rec type_coerce l d_env t1 e t2 =
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
 	let cs = [Eq(l,b2,{nexp=Nconst 0});Eq(l,r2,{nexp=N2n({nexp=Nadd(b1,r1)})})] in
-	(t2,cs,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Some(([],t2),Emp,cs,pure_e))))
+	(t2,cs,E_aux(E_app((Id_aux(Id "to_num_inc",l)),[e]),(l,Some(([],t2),External None,cs,pure_e))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
 	let cs = [Eq(l,b2,{nexp=Nconst 0});Eq(l,r2,{nexp=N2n({nexp=Nadd({nexp=Nneg b1},r1)})})] in
-	(t2,cs,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Some(([],t2),Emp,cs,pure_e))))
+	(t2,cs,E_aux(E_app((Id_aux(Id "to_num_dec",l)),[e]),(l,Some(([],t2),External None,cs,pure_e))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
 	eq_error l "Cannot convert a vector to an enum without an order"
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
@@ -494,12 +509,12 @@ let rec type_coerce l d_env t1 e t2 =
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Oinc};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
 	let cs = [Eq(l,b1,{nexp=Nconst 0});Eq(l,{nexp=Nadd(b2,r2)},{nexp=N2n r1})] in
-	(t2,cs,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),[e]),(l,Some(([],t2),Emp,cs,pure_e))))
+	(t2,cs,E_aux(E_app((Id_aux(Id "to_vec_inc",l)),[e]),(l,Some(([],t2),External None,cs,pure_e))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Odec};TA_typ {t=Tid "bit"}],
         [TA_nexp b2;TA_nexp r2;] -> 
 	let cs = [Eq(l,b1,{nexp=N2n{nexp=Nadd(b2,{nexp=Nneg r2})}});
 		  Eq(l,r1,b1)] in
-	(t2,cs,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),[e]),(l,Some(([],t2),Emp,cs,pure_e))))
+	(t2,cs,E_aux(E_app((Id_aux(Id "to_vec_dec",l)),[e]),(l,Some(([],t2),External None,cs,pure_e))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
 	eq_error l "Cannot convert an enum to a vector without an order"
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
@@ -542,7 +557,7 @@ let rec type_coerce l d_env t1 e t2 =
 		   (l,Some(([],t2),Emp,[],pure_e))))
 	  | None -> eq_error l ("Type mismatch: found a " ^ (t_to_string t1) ^ " but expected " ^ (t_to_string t2))))
   | Tid("bit"),Tid("bool") ->
-    let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Some(([],bool_t),External,[],pure_e))) in
+    let e' = E_aux(E_app((Id_aux(Id "is_one",l)),[e]),(l,Some(([],bool_t),External None,[],pure_e))) in
     (t2,[],e')
   | Tid(i),Tapp("enum",[TA_nexp b1;TA_nexp r1;]) -> 
     (match get_abbrev d_env t1 with
diff --git a/src/type_internal.mli b/src/type_internal.mli
index 13cb56ea..63583d28 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -54,7 +54,7 @@ and t_arg =
 
 type tag =
   | Emp
-  | External
+  | External of string option
   | Default
   | Constructor
   | Enum
@@ -102,6 +102,7 @@ val bit_t : t
 val pure_e : effect
 
 val t_to_string : t -> string
+val tannot_to_string : tannot -> string
 
 val reset_fresh : unit -> unit
 val new_t : unit -> t