Many changes:

Split out specification specific memory and external functions
Reduce the presence of big_int
Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction

Also some bug fixes exposed by above and running ARM second instruction

11 files changed, 737 insertions, 708 deletions

diff --git a/src/lem_interp/extract.mllib b/src/lem_interp/extract.mllib
index e163c71b..8f7d000c 100644
--- a/src/lem_interp/extract.mllib
+++ b/src/lem_interp/extract.mllib
@@ -7,5 +7,4 @@ Interp_interface
 Interp_inter_imp
 
 Pretty_interp
-Run_interp
 Printing_functions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 50158ff6..0c30cca8 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -24,37 +24,49 @@ let val_annot typ = Just(typ,Tag_empty,[],pure)
 
 let ctor_annot typ = Just(typ,Tag_ctor,[],pure)
 
+let enum_annot typ = Just(typ,Tag_enum,[],pure)
+
 (* This is different from OCaml: it will drop elements from the longest list. *)
 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')
 
+type i_direction = IInc | IDec
+let is_inc = function | IInc -> true | _ -> false end
+
+let id_of_string s = (Id_aux (Id s) Unknown)
+
 type reg_form =
  | Reg of id * tannot
  | SubReg of id * reg_form * index_range
 
+type ctor_kind = C_Enum | C_Union
+
 type value =
  | V_boxref of nat * t  
  | V_lit of lit
  | V_tuple of list value
  | V_list of list value
- (* A full vector: integer is the first index, bool says if that's most or least significant *)
- | V_vector of integer * bool * list value 
- (* A vector with default values, second integer stores length; as above otherwise *)
- | V_vector_sparse of integer * integer * bool * list (integer * value) * value 
+ (* A full vector: int is the first index, bool says if that's most or least significant *)
+ | V_vector of nat * i_direction * list value 
+ (* A vector with default values, second int stores length; as above otherwise *)
+ | V_vector_sparse of nat * nat * i_direction * list (nat * value) * value 
  | V_record of t * list (id * value)
- | V_ctor of id * t * value
+ | V_ctor of id * t * ctor_kind * value
  | V_unknown (* Distinct from undefined, used by memory system *)
  | V_register of reg_form (* Value to store register access, when not actively reading or writing *)
  | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *)
  | V_track of value * (list reg_form) (* Used when memory system wants to track what register(s) a value came from *)
 
-let rec integerToString n acc =
+(*let rec integerToString n acc =
   if n = 0 then
     acc
   else
     integerToString (n / 10) (chr (natFromInteger (n mod 10 + 48)) :: acc)
 
-let string_of_integer i = if i = 0 then "0" else toString(integerToString i [])
+let string_of_integer i = if i = 0 then "0" else toString(integerToString i [])*)
+val string_of_integer : integer -> string
+declare ocaml target_rep function string_of_integer = `Big_int.string_of_big_int`
+
 
 let rec string_of_value v = match v with
   | V_boxref nat t -> "$#" ^ (show nat) ^ "$"
@@ -85,11 +97,11 @@ let rec string_of_value v = match v with
 	  | V_lit (L_aux L_one _) -> to_bin()
 	  | _ -> default_format() end end
   | V_vector_sparse start stop inc vals default -> 
-    "[" ^ (list_to_string (fun (i,v) -> (string_of_integer i) ^ " = " ^ (string_of_value v)) "," vals) ^ "]:" ^
-      string_of_integer start ^ "-" ^string_of_integer  stop ^ "(default of " ^ (string_of_value default) ^ ")"
+    "[" ^ (list_to_string (fun (i,v) -> (show i) ^ " = " ^ (string_of_value v)) "," vals) ^ "]:" ^
+      show start ^ "-" ^show stop ^ "(default of " ^ (string_of_value default) ^ ")"
   | V_record t vals ->
     "{" ^ (list_to_string (fun (id,v) -> (get_id id) ^ "=" ^ (string_of_value v)) ";" vals) ^ "}"
-  | V_ctor id t value -> (get_id id) ^ " " ^ string_of_value value     
+  | V_ctor id t _ value -> (get_id id) ^ " " ^ string_of_value value     
   | V_unknown -> "Unknown"
   | V_register _ -> "register_as_value"
   | V_register_alias _ _ -> "register_as_alias"
@@ -111,7 +123,7 @@ and value_eq left right =
   | (V_record t l, V_record t' l') ->
       t = t' &&
       listEqualBy id_value_eq l l'
-  | (V_ctor i t v, V_ctor i' t' v') -> t = t' && id_value_eq (i, v) (i', v')
+  | (V_ctor i t ckind v, V_ctor i' t' ckind' v') -> t = t' && ckind=ckind' && id_value_eq (i, v) (i', v')
   | (V_unknown,_) -> true
   | (_,V_unknown) -> true
   | (V_track v _, v2) -> value_eq v v2
@@ -128,7 +140,7 @@ let reg_start_pos reg =
   match reg with
     | Reg _ (Just(typ,_,_,_)) -> 
       let start_from_vec targs = match targs with
-	| T_args [T_arg_nexp (Ne_const s);_;_;_] -> s
+	| T_args [T_arg_nexp (Ne_const s);_;_;_] -> natFromInteger s
       end in
       let start_from_reg targs = match targs with
 	| T_args [T_arg_typ (T_app "vector" targs)] -> start_from_vec targs
@@ -148,7 +160,7 @@ let reg_size reg =
   match reg with
     | Reg _ (Just(typ,_,_,_)) -> 
       let end_from_vec targs = match targs with
-	| T_args [_;T_arg_nexp (Ne_const s);_;_] -> s
+	| T_args [_;T_arg_nexp (Ne_const s);_;_] -> natFromInteger s
       end in
       let end_from_reg targs = match targs with
 	| T_args [T_arg_typ (T_app "vector" targs)] -> end_from_vec targs
@@ -165,7 +177,7 @@ let reg_size reg =
 end 
 
 let vector_length v = match v with
-  | V_vector n inc vals -> integerFromNat(List.length vals)
+  | V_vector n inc vals -> List.length vals
   | V_vector_sparse n m inc vals def -> m
   | V_lit _ -> 1
   | _ -> 0
@@ -190,18 +202,19 @@ type sub_reg_map = list (id * index_range)
 (*top_level is a tuple of 
   (all definitions,
    all extracted instructions (where possible),
+   default direction
    letbound and enum values, 
    register values, 
    Typedef union constructors, 
    sub register mappings, and register aliases) *)
 type top_level = 
-  | Env of (defs tannot) * list instruction_form * env * env * list (id * typ) * list (id * sub_reg_map) * list (id * (alias_spec tannot))
+  | Env of (defs tannot) * list instruction_form * i_direction * env * env * list (id * typ) * list (id * sub_reg_map) * list (id * (alias_spec tannot))
 
 type action = 
- | Read_reg of reg_form * maybe (integer * integer)
- | Write_reg of reg_form * maybe (integer* integer) * value
- | Read_mem of id * value * maybe (integer * integer)
- | Write_mem of id * value * maybe (integer * integer) * value
+ | Read_reg of reg_form * maybe (nat * nat)
+ | Write_reg of reg_form * maybe (nat * nat) * value
+ | Read_mem of id * value * maybe (nat * nat)
+ | Write_mem of id * value * maybe (nat * nat) * value
  | Barrier of id * value
  | Write_next_IA of value (* Perhaps not needed? *)
  | Nondet of list (exp tannot)
@@ -222,13 +235,14 @@ type outcome =
  | Action of action * stack
  | Error of l * string 
 
-type interp_mode = <| eager_eval : bool; track_values : bool |>
+type interp_mode = <| eager_eval : bool; track_values : bool; |>
 
 (* Evaluates global let binds and prepares the context for individual expression evaluation in the current model *)
-val to_top_env : (outcome -> maybe value) -> defs tannot -> (maybe outcome * top_level)
+val to_top_env : (i_direction -> outcome -> maybe value) -> defs tannot -> (maybe outcome * top_level)
+val get_default_direction : top_level -> i_direction
 
 (* interprets the exp sequentially in the presence of a set of top level definitions and returns a value, a memory request, or other external action *)
-val interp :interp_mode -> (outcome -> maybe value) -> defs tannot -> exp tannot -> outcome
+val interp :interp_mode -> (i_direction -> outcome -> maybe value) -> defs tannot -> exp tannot -> outcome
 
 (* Takes a paused partially evaluated expression, puts the value into the environment, and runs again *)
 val resume : interp_mode -> stack -> maybe value -> outcome
@@ -349,8 +363,8 @@ let is_lit_vector (L_aux l _) =
   | _ -> false
 end
 
-val litV_to_vec : lit -> bool -> value
-let litV_to_vec (L_aux lit l) is_inc =
+val litV_to_vec : lit -> i_direction -> value
+let litV_to_vec (L_aux lit l) (dir: i_direction) =
   match lit with
   | L_hex s ->
     let to_v b = V_lit (L_aux b l) in
@@ -381,20 +395,17 @@ let litV_to_vec (L_aux lit l) is_inc =
 			 | #'e' -> [L_one ;L_one ;L_one ;L_zero]
 			 | #'f' -> [L_one ;L_one ;L_one ;L_one ] end)
 		       (String.toCharList s))) in
-    if is_inc 
-    then V_vector 0 true hexes
-    else V_vector (integerFromNat ((List.length hexes) -1)) false hexes
+    V_vector (if is_inc(dir) then 0 else ((List.length hexes) - 1)) dir hexes
   | L_bin s -> 
-    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) (String.toCharList s) in
-    if is_inc
-    then V_vector 0 true bits
-    else V_vector (integerFromNat ((List.length bits) -1)) false bits
+    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) (String.toCharList s) in
+    V_vector (if is_inc(dir) then 0 else ((List.length bits) -1)) dir bits
   end
 
-(* Like List_extra.nth with a integer instead of nat index -
- * using an unsafe coercion. *)
-val list_nth : forall 'a . list 'a -> integer -> 'a
-let list_nth l n = List_extra.nth l (natFromInteger n)
+val list_nth : forall 'a . list 'a -> nat -> 'a
+let list_nth l n = List_extra.nth l n
 
 val list_length : forall 'a . list 'a -> integer
 let list_length l = integerFromNat (List.length l)
@@ -432,28 +443,22 @@ let rec binary_taint thunk vall valr =
    | (vl,vr) -> thunk vl vr
 end 
 
-val access_vector : value -> integer -> value
+val access_vector : value -> nat -> value
 let access_vector v n =
   retaint v (match (detaint v) with
     | V_unknown -> V_unknown 
-    | V_vector m inc vs -> 
-      if inc then
-	list_nth vs (n - m)
-      else list_nth vs (m - n)
+    | V_vector m dir vs -> 
+      list_nth vs (if is_inc(dir) then (n - m) else (m - n))
     | V_vector_sparse _ _ _ vs d ->
       match (List.lookup n vs) with
 	| Nothing -> d
 	| Just v  -> v end 
   end )
 
-val from_n_to_n :forall 'a. integer -> integer  -> list 'a -> list 'a
-let from_n_to_n from to_ ls =
-  let from = natFromInteger from in
-  let to_ = natFromInteger to_ in
-  take (to_ - from + 1) (drop from ls)
+val from_n_to_n :forall 'a. nat -> nat  -> list 'a -> list 'a
+let from_n_to_n from to_ ls = take (to_ - from + 1) (drop from ls)
 
-val slice_sparse_list : (integer -> integer -> bool) -> (integer -> integer) -> 
-                        list (integer * value) -> integer -> integer -> ((list (integer * value)) * bool)
+val slice_sparse_list : (nat -> nat -> bool) -> (nat -> nat) -> list (nat * value) -> nat -> nat -> ((list (nat * value)) * bool)
 let rec slice_sparse_list compare update_n vals n1 n2 = 
   let sl = slice_sparse_list compare update_n in
   if (n1 = n2) && (vals = []) 
@@ -470,23 +475,23 @@ let rec slice_sparse_list compare update_n vals n1 n2 =
       else let (rest,_) = (sl vals (update_n i) n2) in ((i,v)::rest,true)
   end
 
-val slice_vector : value -> integer -> integer -> value
+val slice_vector : value -> nat -> nat -> value
 let slice_vector v n1 n2 =
   retaint v (match detaint v with
-    | V_vector m inc vs ->
-      if inc 
-      then V_vector n1 inc (from_n_to_n (n1 - m) (n2 - m) vs)
-      else V_vector (n1 - n2 + 1) inc (from_n_to_n (m - n1) (m - n2) vs)
-    | V_vector_sparse m n inc vs d -> 
+    | V_vector m dir vs ->
+      if is_inc(dir) 
+      then V_vector n1 dir (from_n_to_n (n1 - m) (n2 - m) vs)
+      else V_vector (n1 - n2 + 1) dir (from_n_to_n (m - n1) (m - n2) vs)
+    | V_vector_sparse m n dir vs d -> 
       let (slice, still_sparse) = 
-	if inc 
+	if is_inc(dir) 
 	then slice_sparse_list (>) (fun i -> i + 1) vs n1 n2
 	else slice_sparse_list (<) (fun i -> i - 1) vs n1 n2 in
-      if still_sparse && inc
-      then V_vector_sparse n1 (n2 - n1) inc slice d
-      else if inc then V_vector 0 inc (List.map snd slice)
-      else if still_sparse then V_vector_sparse (n1 - n2 +1) (n1 - n2) inc slice d
-      else V_vector (n1 - n2 +1) inc (List.map snd slice)
+      if still_sparse && is_inc(dir)
+      then V_vector_sparse n1 (n2 - n1) dir slice d
+      else if is_inc(dir) then V_vector 0 dir (List.map snd slice)
+      else if still_sparse then V_vector_sparse (n1 - n2 +1) (n1 - n2) dir slice d
+      else V_vector (n1 - n2 +1) dir (List.map snd slice)
  end )
 
 val update_field_list : list (id * value) -> list (id * value) -> list (id * value)
@@ -506,7 +511,7 @@ let fupdate_record base updates =
        end) in
   binary_taint fupdate_record_helper base updates
 
-val fupdate_sparse : (integer -> integer -> bool) -> list (integer*value) -> integer -> value -> list (integer*value)
+val fupdate_sparse : (nat -> nat -> bool) -> list (nat*value) -> nat -> value -> list (nat*value)
 let rec fupdate_sparse comes_after vs n vexp =
   match vs with
     | [] -> [(n,vexp)]
@@ -516,18 +521,18 @@ let rec fupdate_sparse comes_after vs n vexp =
       else (i,v)::(fupdate_sparse comes_after vs n vexp)
 end
 
-val fupdate_vec : value -> integer -> value -> value
+val fupdate_vec : value -> nat -> value -> value
 let fupdate_vec v n vexp =
   let tainted = binary_taint (fun v _ -> v) v vexp in
   retaint tainted
     (match detaint v with
-      | V_vector m inc vals -> 
-	V_vector m inc (List.update vals (natFromInteger (if inc then (n-m) else (m-n))) vexp)
-      | V_vector_sparse m o inc vals d ->
-	V_vector_sparse m o inc (fupdate_sparse (if inc then (>) else (<)) vals n vexp) d
+      | V_vector m dir vals -> 
+	V_vector m dir (List.update vals (if is_inc(dir) then (n-m) else (m-n)) vexp)
+      | V_vector_sparse m o dir vals d ->
+	V_vector_sparse m o dir (fupdate_sparse (if is_inc(dir) then (>) else (<)) vals n vexp) d
      end)
 
-val replace_is : forall 'a. list 'a -> list 'a -> integer -> integer -> integer -> list 'a
+val replace_is : forall 'a. list 'a -> list 'a -> nat -> nat -> nat -> list 'a
 let rec replace_is ls vs base start stop =
   match (ls,vs) with
   | ([],_) -> []
@@ -539,7 +544,7 @@ let rec replace_is ls vs base start stop =
     else l::(replace_is ls (v::vs) (base+1) start stop)
   end
 
-val replace_sparse : (integer -> integer -> bool) -> list (integer * value) -> list (integer * value) -> list (integer * value)
+val replace_sparse : (nat -> nat -> bool) -> list (nat * value) -> list (nat * value) -> list (nat * value)
 let rec replace_sparse compare vals reps =
   match (vals,reps) with
     | ([],rs) -> rs
@@ -551,73 +556,70 @@ let rec replace_sparse compare vals reps =
       else (i2,r)::(replace_sparse compare ((i1,v)::vs) rs)
 end
 
-val fupdate_vector_slice : value -> value -> integer -> integer -> value
+val fupdate_vector_slice : value -> value -> nat -> nat -> value
 let fupdate_vector_slice vec replace start stop =
   let fupdate_vec_help vec replace = 
     (match (vec,replace) with
-    | (V_vector m inc vals,V_vector _ inc' reps) ->
-      V_vector m inc 
+    | (V_vector m dir vals,V_vector _ dir' reps) ->
+      V_vector m dir 
 	(replace_is vals 
-	   (if inc=inc' then reps else (List.reverse reps))
-	   0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
-    | (V_vector m inc vals, V_unknown) ->
-      V_vector m inc
+	   (if dir=dir' then reps else (List.reverse reps))
+	   0 (if is_inc(dir) then (start-m) else (m-start)) (if is_inc(dir) then (stop-m) else (m-stop)))
+    | (V_vector m dir vals, V_unknown) ->
+      V_vector m dir
 	(replace_is vals 
-	   (List.replicate (natFromInteger(if inc then (stop-start) else (start-stop))) V_unknown)
-	   0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
-    | (V_vector_sparse m n inc vals d,V_vector _ _ reps) ->
-      let (_,repsi) = List.foldl (fun (i,rs) r -> ((if inc then i+1 else i-1), (i,r)::rs)) (start,[]) reps in
-      (V_vector_sparse m n inc (replace_sparse (if inc then (<) else (>)) vals (List.reverse repsi)) d)
-    | (V_vector_sparse m n inc vals d, V_unknown) ->
-      let (_,repsi) = List.foldl (fun (i,rs) r -> ((if inc then i+1 else i-1), (i,r)::rs)) (start,[]) 
-	(List.replicate (natFromInteger (if inc then (stop-start) else (start-stop))) V_unknown) in
-      (V_vector_sparse m n inc (replace_sparse (if inc then (<) else (>)) vals (List.reverse repsi)) d)
+	   (List.replicate (if is_inc(dir) then (stop-start) else (start-stop)) V_unknown)
+	   0 (if is_inc(dir) then (start-m) else (m-start)) (if is_inc(dir) then (stop-m) else (m-stop)))
+    | (V_vector_sparse m n dir vals d,V_vector _ _ reps) ->
+      let (_,repsi) = List.foldl (fun (i,rs) r -> ((if is_inc(dir) then i+1 else i-1), (i,r)::rs)) (start,[]) reps in
+      (V_vector_sparse m n dir (replace_sparse (if is_inc(dir) then (<) else (>)) vals (List.reverse repsi)) d)
+    | (V_vector_sparse m n dir vals d, V_unknown) ->
+      let (_,repsi) = List.foldl (fun (i,rs) r -> ((if is_inc(dir) then i+1 else i-1), (i,r)::rs)) (start,[]) 
+	(List.replicate (if is_inc(dir) then (stop-start) else (start-stop)) V_unknown) in
+      (V_vector_sparse m n dir (replace_sparse (if is_inc(dir) then (<) else (>)) vals (List.reverse repsi)) d)
     | (V_unknown,_) -> V_unknown
      end) in
   binary_taint fupdate_vec_help vec replace
 
-val update_vector_slice : value -> value -> integer -> integer -> lmem -> lmem
+val update_vector_slice : value -> value -> nat -> nat -> lmem -> lmem
 let update_vector_slice vector value start stop mem = 
   match (detaint vector,detaint value) with
   | ((V_boxref n t), v) ->
     update_mem mem n (fupdate_vector_slice (in_mem mem n) (retaint value v) start stop)    
-  | ((V_vector m inc vs),(V_vector n inc2 vals)) ->
+  | ((V_vector m _ vs),(V_vector n _ vals)) ->
     let (V_vector m' _ vs') = slice_vector vector start stop in
     foldr2 (fun vbox v mem -> match vbox with
       | V_boxref n t -> update_mem mem n v end)
       mem vs' vals
-  | ((V_vector m inc vs),(V_vector_sparse n o inc2 vals d)) -> 
+  | ((V_vector m dir vs),(V_vector_sparse n o _ vals d)) -> 
     let (V_vector m' _ vs') = slice_vector vector start stop in
     let (_,mem) = foldr (fun vbox (i,mem) ->
                           match vbox with
 			    | V_boxref n t -> 
-			      (if inc then i+1 else i-1,
+			      (if is_inc(dir) then i+1 else i-1,
 				update_mem mem n (match List.lookup i vals with
 				  | Nothing -> d
 				  | Just v  -> v end))
                           end) (m,mem) vs' in 
     mem
-  | ((V_vector m inc vs),v) ->
+  | ((V_vector m _ vs),v) ->
     let (V_vector m' _ vs') = slice_vector vector start stop in
     List.foldr (fun vbox mem -> match vbox with
                                     | V_boxref n t -> update_mem mem n v end)
       mem vs'
 end
 
-let update_vector_start new_start expected_size v = 
+let update_vector_start default_dir new_start expected_size v = 
   retaint v
     (match detaint v with
-      | V_lit (L_aux L_zero _) ->
-	V_vector new_start true (*TODO: Check for default endianness here*) [v]
-      | V_lit (L_aux L_one _) ->
-	V_vector new_start true [v]
-      | V_vector m inc vs -> V_vector new_start inc vs
-  (*Note, may need to shrink and check if still sparse *)
-      | V_vector_sparse m n inc vals d -> V_vector_sparse new_start n inc vals d 
+      | V_lit (L_aux L_zero _) -> V_vector new_start default_dir [v]
+      | V_lit (L_aux L_one _) -> V_vector new_start default_dir [v]
+      | V_vector m inc vs -> V_vector new_start inc vs (*Note, may need to shrink and check if still sparse *)
+      | V_vector_sparse m n dir vals d -> V_vector_sparse new_start n dir vals d 
       | V_unknown -> 
-	V_vector new_start true (List.replicate (natFromInteger expected_size) V_unknown)
+	V_vector new_start default_dir (List.replicate expected_size V_unknown)
       | V_lit (L_aux L_undef _) -> 
-	V_vector new_start true (List.replicate (natFromInteger expected_size) v)
+	V_vector new_start default_dir (List.replicate expected_size v)
      end)
 
 val in_ctors : list (id * typ) -> id -> maybe typ
@@ -645,6 +647,8 @@ let top_hole stack : bool =
   | _ -> false
 end
 
+let redex_id = id_of_string "0"
+
 (*Converts a Hole_frame into a Thunk_frame, pushing to the top of the stack to insert the value at the innermost context *)
 val add_answer_to_stack : stack -> value -> stack
 let rec add_answer_to_stack stack v = 
@@ -674,9 +678,6 @@ let get_stack_state stack =
     | Thunk_frame exp top_level lenv lmem stack -> (lenv,lmem)
 end
 
-let id_of_string s = (Id_aux (Id s) Unknown)
-
-let redex_id = id_of_string "0"
 
 (*functions for converting in progress evaluation back into expression for building current continuation*)
 let rec combine_typs ts =
@@ -735,24 +736,24 @@ let rec val_typ v =
 	| L_undef -> T_var "fresh"
       end 
     | V_tuple vals -> T_tup (List.map val_typ vals)
-    | V_vector n inc vals -> 
+    | V_vector n dir vals -> 
       let ts = List.map val_typ vals in
       let t = combine_typs ts in
-      T_app "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_app "vector" (T_args [T_arg_nexp (Ne_const (integerFromNat n)); T_arg_nexp (Ne_const (list_length vals));
+			      T_arg_order (Ord_aux (if is_inc(dir) then Ord_inc else Ord_dec) Unknown);
 			      T_arg_typ t])
-    | V_vector_sparse n m inc vals d ->
+    | V_vector_sparse n m dir vals d ->
       let ts = List.map val_typ (d::(List.map snd vals)) in
       let t = combine_typs ts in
-      T_app "vector" (T_args [T_arg_nexp (Ne_const n); T_arg_nexp (Ne_const m);
-			      T_arg_order (Ord_aux (if inc then Ord_inc else Ord_dec) Unknown);
+      T_app "vector" (T_args [T_arg_nexp (Ne_const (integerFromNat n)); T_arg_nexp (Ne_const (integerFromNat m));
+			      T_arg_order (Ord_aux (if is_inc(dir) 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 "list" (T_args [T_arg_typ t])
-    | V_ctor id t vals -> t
+    | V_ctor id t _ vals -> t
     | V_register reg -> reg_to_t reg
     | V_track v _ -> val_typ v
     | V_unknown -> T_var "fresh" (*consider carrying the type along*)
@@ -760,8 +761,14 @@ let rec val_typ v =
 
 (* When mode.track_values keeps tracking on registers by extending environment *)
 let rec to_exp mode env v : (exp tannot * lenv) =
-  let mk_annot is_ctor = (Interp_ast.Unknown, if is_ctor then (ctor_annot (val_typ v)) else (val_annot (val_typ v))) in
-  let annot = mk_annot false in
+  let mk_annot is_ctor ctor_kind = 
+    (Interp_ast.Unknown, 
+     if is_ctor 
+     then match ctor_kind with
+       | Just(C_Enum) -> (enum_annot (val_typ v))
+       | _ -> (ctor_annot (val_typ v)) end
+     else (val_annot (val_typ v))) in
+  let annot = mk_annot false Nothing in
   let mapf vs ((LEnv l env) as lenv) : (list (exp tannot) * lenv) =
     let (es, env) = 
       List.foldr (fun v (es,env) -> let (e,ev) = (to_exp mode env v) in
@@ -776,21 +783,24 @@ let rec to_exp mode env v : (exp tannot * lenv) =
   | V_lit lit -> (E_aux (E_lit lit) annot, env)
   | V_tuple(vals) -> 
     let (es,env') = mapf vals env in (E_aux (E_tuple es) annot, env')
-  | V_vector n inc vals -> 
+  | V_vector n dir vals -> 
     let (es,env') = mapf vals env in
-    if (inc && n=0) 
+    if (is_inc(dir) && n=0) 
     then (E_aux (E_vector es) annot, env') 
-    else if inc 
-    then (E_aux (E_vector_indexed (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,(n,e)::acc)) (n,[]) es)))
-	                          (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env')
+    else if is_inc(dir) 
+    then (E_aux (E_vector_indexed 
+		   (List.reverse (snd (List.foldl (fun (n,acc) e -> (n+1,((integerFromNat n),e)::acc)) (n,[]) es)))
+	           (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env')
     else 
-      (E_aux (E_vector_indexed (snd (List.foldr (fun e (n,acc) -> (n+1,(n,e)::acc)) (n-(list_length es),[]) es)) 
-	                       (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env')
-  | V_vector_sparse n m inc vals d ->
+      (E_aux (E_vector_indexed 
+		(snd (List.foldr (fun e (n,acc) -> (n+1,((integerFromNat n),e)::acc)) (n-(List.length es),[]) es)) 
+	        (Def_val_aux Def_val_empty (Interp_ast.Unknown,Nothing))) annot, env')
+  | V_vector_sparse n m dir vals d ->
     let ((es : (list (exp tannot))),env') = mapf (List.map (fun (i,v) -> v) vals) env in
     let ((d : (exp tannot)),env')  = to_exp mode env' d in
     (E_aux (E_vector_indexed 
-	      ((if inc then List.reverse else (fun i -> i)) (List.map (fun ((i,v), e) -> (i, e)) (List.zip vals es)))
+	      ((if is_inc(dir) then List.reverse else (fun i -> i))
+		  (List.map (fun ((i,v), e) -> ((integerFromNat i), e)) (List.zip vals es)))
 	      (Def_val_aux (Def_val_dec d) (Interp_ast.Unknown, Nothing))) annot, env')
   | V_record t ivals -> 
     let (es,env') = mapf (List.map (fun (i,v) -> v) ivals) env in
@@ -799,23 +809,24 @@ let rec to_exp mode env v : (exp tannot * lenv) =
                                    (List.zip ivals es)) false) 
 	               (Unknown,Nothing))) annot, env')
   | V_list(vals) -> let (es,env') = mapf vals env in (E_aux (E_list es) annot, env')
-  | V_ctor id t vals -> 
+  | V_ctor id t ckind vals -> 
+    let annotation = mk_annot true (Just ckind) in
     (match vals with
-    | V_lit (L_aux L_unit _) -> (E_aux (E_id id) (mk_annot true), env)
-    | V_track (V_lit (L_aux L_unit _)) _ -> (E_aux (E_id id) (mk_annot true), env)
-    | V_tuple vals -> let (es,env') = mapf vals env in (E_aux (E_app id es) (mk_annot true), env')
-    | V_track (V_tuple vals) _ -> let (es,env') = mapf vals env in (E_aux (E_app id es) (mk_annot true), env')
+    | V_lit (L_aux L_unit _) -> (E_aux (E_id id) annotation, env)
+    | V_track (V_lit (L_aux L_unit _)) _ -> (E_aux (E_id id) annotation, env)
+    | V_tuple vals -> let (es,env') = mapf vals env in (E_aux (E_app id es) annotation, env')
+    | V_track (V_tuple vals) _ -> let (es,env') = mapf vals env in (E_aux (E_app id es) annotation, env')
     | V_track _ _ -> 
       if mode.track_values 
       then begin let (fid,env') = fresh_var env in
                  let env' = add_to_env (fid,vals) env' in
                  (E_aux 
 		    (E_app id [(E_aux (E_id fid) (Interp_ast.Unknown, (val_annot (val_typ vals))))])
-		    (mk_annot true), env')
+		    annotation, env')
       end 
-      else let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) (mk_annot true), env') 
+      else let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) annotation, env') 
     | _ -> 
-      let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) (mk_annot true),env') end)
+      let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) annotation,env') end)
   | V_register (Reg id tan) -> (E_aux (E_id id) annot, env)
   | V_track v' _ -> 
     if mode.track_values
@@ -860,11 +871,11 @@ let rec match_pattern (P_aux p _) value_whole =
   match p with 
   | P_lit(lit) -> 
     if is_lit_vector lit then
-      let (V_vector n inc bits) = litV_to_vec lit true in (*TODO use type annotation to select between increasing and decreasing*)
+      let (V_vector n inc bits) = litV_to_vec lit IInc in (*TODO use type annotation to select between increasing and decreasing*)
       match value with
       | V_lit litv -> 
         if is_lit_vector litv then 
-          let (V_vector n' inc' bits') = litV_to_vec litv true in (*TODO use type annotation to select between increasing and decreasing *)
+          let (V_vector n' inc' bits') = litV_to_vec litv IInc in (*TODO use type annotation to select between increasing and decreasing *)
           if n=n' && inc = inc' then (foldr2 (fun l r rest -> (l = r) && rest) true bits bits',false, eenv)
           else (false,false,eenv)
         else (false,false,eenv)
@@ -890,7 +901,7 @@ let rec match_pattern (P_aux p _) value_whole =
  | P_id id -> (true, false, (LEnv 0 [(id,value_whole)]))
  | P_app (Id_aux id _) pats -> 
    match value with
-   | V_ctor (Id_aux cid _) t (V_tuple vals) -> 
+   | V_ctor (Id_aux cid _) t ckind (V_tuple vals) -> 
      if (id = cid && ((List.length pats) = (List.length vals)))
      then foldr2
           (fun pat value (matched_p,used_unknown,bounds) ->
@@ -899,7 +910,7 @@ let rec match_pattern (P_aux p _) value_whole =
               (matched_p, (used_unknown || used_unknown'), (union_env new_bounds bounds))
             else (false,false,eenv)) (true,false,eenv) pats vals
      else (false,false,eenv)
-   | V_ctor (Id_aux cid _) t (V_track (V_tuple vals) r) -> 
+   | V_ctor (Id_aux cid _) t ckind (V_track (V_tuple vals) r) -> 
      if (id = cid && ((List.length pats) = (List.length vals)))
      then foldr2
           (fun pat value (matched_p,used_unknown,bounds) ->
@@ -908,7 +919,7 @@ let rec match_pattern (P_aux p _) value_whole =
               (matched_p, (used_unknown || used_unknown'), (union_env new_bounds bounds))
             else (false,false,eenv)) (true,false,eenv) pats vals
      else (false,false,eenv)
-   | V_ctor (Id_aux cid _) t v ->
+   | V_ctor (Id_aux cid _) t ckind v ->
      if id = cid
      then (match (pats,detaint v) with
      | ([],(V_lit (L_aux L_unit _))) -> (true,true,eenv)
@@ -934,7 +945,7 @@ let rec match_pattern (P_aux p _) value_whole =
    end           
  | P_vector pats ->
    match value with
-   | V_vector n inc vals ->
+   | V_vector n dir vals ->
      if ((List.length vals) = (List.length pats))
      then foldr2
        (fun pat value (matched_p,used_unknown,bounds) -> 
@@ -942,10 +953,10 @@ let rec match_pattern (P_aux p _) value_whole =
 	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat value) in
 	   (matched_p, (used_unknown||used_unknown'), (union_env new_bounds bounds))
 	 else (false,false,eenv))
-       (true,false,eenv) (if inc then pats else List.reverse pats) vals
+       (true,false,eenv) (if is_inc(dir) then pats else List.reverse pats) vals
      else (false,false,eenv)
-   | V_vector_sparse n m inc vals d ->
-     if ((natFromInteger m) = (List.length pats))
+   | V_vector_sparse n m dir vals d ->
+     if (m = (List.length pats))
      then let (_,matched_p,used_unknown,bounds) =
 	    foldr
 	      (fun pat (i,matched_p,used_unknown,bounds) ->
@@ -954,7 +965,8 @@ let rec match_pattern (P_aux p _) value_whole =
 		       match_pattern pat (match List.lookup i vals with
 			 | Nothing -> d
 			 | Just v  -> (taint_pat v) end) in
-		     ((if inc then i+1 else i-1),matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
+		     ((if is_inc(dir) then i+1 else i-1),
+		      matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
                 else (i,false,false,eenv)) (n,true,false,eenv) pats in
 	  (matched_p,used_unknown,bounds)
      else (false,false,eenv)
@@ -963,17 +975,22 @@ let rec match_pattern (P_aux p _) value_whole =
      end
  | P_vector_indexed ipats ->
    match value with
-   | V_vector n inc vals ->
-     let v_len = if inc then list_length vals + n else n - list_length vals in
+   | V_vector n dir vals ->
+     let v_len = if is_inc(dir) then List.length vals + n else n - List.length vals in
      List.foldr
-       (fun (i,pat) (matched_p,used_unknown,bounds) -> if matched_p && i < v_len then
-	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat (list_nth vals (if inc then i+n else i-n))) in
+       (fun (i,pat) (matched_p,used_unknown,bounds) -> 
+	 let i = natFromInteger i in
+	 if matched_p && i < v_len then
+	   let (matched_p,used_unknown',new_bounds) = 
+	     match_pattern pat (taint_pat (list_nth vals (if is_inc(dir) then i+n else i-n))) in
 	   (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
          else (false,false,eenv))
        (true,false,eenv) ipats
-   | V_vector_sparse n m inc vals d ->
+   | V_vector_sparse n m dir vals d ->
      List.foldr
-       (fun (i,pat) (matched_p,used_unknown,bounds) -> if matched_p && i < m then
+       (fun (i,pat) (matched_p,used_unknown,bounds) -> 
+	 let i = natFromInteger i in
+	 if matched_p && i < m then
 	   let (matched_p,used_unknown',new_bounds) = 
              match_pattern pat (match List.lookup i vals with | Nothing -> d | Just v -> (taint_pat v) end) in
 	   (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
@@ -1023,12 +1040,13 @@ let rec match_pattern (P_aux p _) value_whole =
    | _ -> (false,false,eenv) end
  end 
 
-and vec_concat_match_plev pat r_vals inc l t =
+and vec_concat_match_plev pat r_vals dir l t =
     match pat with
       | P_lit (L_aux (L_bin bin_string) l') ->
 	let bin_chars = toCharList bin_string in
 	let binpats = List.map 
-          (fun b -> P_aux (match b with | #'0' -> P_lit (L_aux L_zero l') | #'1' -> P_lit (L_aux L_one l')end) (l',Nothing)) bin_chars in
+          (fun b -> P_aux (match b with 
+	    | #'0' -> P_lit (L_aux L_zero l') | #'1' -> P_lit (L_aux L_one l')end) (l',Nothing)) bin_chars in
 	vec_concat_match binpats r_vals
       | P_vector pats -> vec_concat_match pats r_vals
       | P_id id -> (match t with
@@ -1037,7 +1055,7 @@ and vec_concat_match_plev pat r_vals inc l t =
 	    let (matched_p,used_unknown,(LEnv bi bounds),matcheds,r_vals) = vec_concat_match wilds r_vals in
 	    if matched_p 
 	    then (matched_p, used_unknown, 
-                  (LEnv bi ((id,(V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds))::bounds)),
+                  (LEnv bi ((id,(V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds))::bounds)),
                   matcheds,r_vals)
 	    else (false,false,eenv,[],[])
 	  | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
@@ -1051,13 +1069,13 @@ and vec_concat_match_plev pat r_vals inc l t =
 	    (false,false,eenv,[],[]) (*TODO see if can have some constraint bounds here*)
 	  | _ -> (false,false,eenv,[],[]) end)
       | P_as (P_aux pat (l',Just(t,_,_,_))) id -> 
-	let (matched_p, used_unknown, (LEnv bi bounds),matcheds,r_vals) = vec_concat_match_plev pat r_vals inc l t in
+	let (matched_p, used_unknown, (LEnv bi bounds),matcheds,r_vals) = vec_concat_match_plev pat r_vals dir l t in
 	if matched_p 
 	then (matched_p, used_unknown,
-              (LEnv bi ((id,V_vector (integerFromNat (if inc then 0 else (List.length matcheds))) inc matcheds)::bounds)),
+              (LEnv bi ((id,V_vector (if is_inc(dir) then 0 else (List.length matcheds)) dir matcheds)::bounds)),
               matcheds,r_vals)
 	else (false,false,eenv,[],[])	  
-      | P_typ _ (P_aux p (l',Just(t',_,_,_))) -> vec_concat_match_plev p r_vals inc l t
+      | P_typ _ (P_aux p (l',Just(t',_,_,_))) -> vec_concat_match_plev p r_vals dir l t
       | _ -> (false,false,eenv,[],[]) end 
       (*TODO Need to support indexed here, skipping intermediate numbers but consumming r_vals, and as *)
 
@@ -1138,7 +1156,7 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
   end
 
 and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
-  let (Env defs instrs lets regs ctors subregs aliases) = t_level in 
+  let (Env defs instrs default_dir lets regs ctors subregs aliases) = t_level in 
   let (typ,tag,ncs,effect) = match annot with 
     | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -1146,7 +1164,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     | E_lit lit -> 
       if is_lit_vector lit 
       then let is_inc = (match typ with 
-	| T_app "vector" (T_args [_;_;T_arg_order (Ord_aux Ord_inc _);_]) -> true | _ -> false end) in
+	| T_app "vector" (T_args [_;_;T_arg_order (Ord_aux Ord_inc _);_]) -> IInc | _ -> IDec end) in
            (Value (litV_to_vec lit is_inc),l_mem,l_env) 
       else (Value (V_lit lit), l_mem,l_env)
     | E_cast ((Typ_aux typ _) as ctyp) exp -> 
@@ -1158,9 +1176,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	  let conditional_update_vstart () =
 	    match typ with
 	      | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
+		let i = natFromInteger i in
 		match (detaint v) with 
-		  | V_vector start inc vs ->
-		    if start = i then (Value v,lm,le) else (Value (update_vector_start i 1 v),lm,le)
+		  | V_vector start dir vs ->
+		    if start = i then (Value v,lm,le) else (Value (update_vector_start dir i 1 v),lm,le)
 		  | _ -> (Value v,lm,le) end
 	      | _ -> (Value v,lm,le) end in
           (match (tag,detaint v) with 
@@ -1205,7 +1224,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	  match in_env aliases id with
 	    | Just aspec -> interp_alias_read mode t_level l_env l_mem aspec
 	    | _ -> (Error l ("Internal error: alias not found"), l_mem,l_env) end
-        | _ -> (Error l ("Internal error: tag other than empty,enum,or extern for " ^ name),l_mem,l_env)
+        | _ -> 
+	  (Error l 
+	     ("Internal error: tag " ^ (string_of_tag tag) ^ " expected empty,enum,alias,or extern for " ^ name),
+	   l_mem,l_env)
         end
     | E_if cond thn els ->
       resolve_outcome 
@@ -1369,8 +1391,25 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	      (match in_env fexps id with
                 | Just v -> (Value (retaint value_whole v),lm,l_env)
                 | Nothing -> (Error l "Internal_error: Field not found in record",lm,le) end)
+	    | V_register ((Reg _ annot) as reg_form) ->
+	      let id' = match annot with
+		| Just((T_id id'),_,_,_) -> id'
+		| Just((T_abbrev (T_id id') _),_,_,_) -> id'
+	      end in
+	      (match in_env subregs (Id_aux (Id id') Unknown) with
+		| Just(indexes) ->
+		  (match in_env indexes id with
+		    | Just ir ->
+		      let sub_reg = SubReg id reg_form ir in
+		      (Action (Read_reg sub_reg Nothing)
+			 (Hole_frame redex_id
+			    (E_aux (E_id redex_id) 
+			       (Unknown, (val_annot (reg_to_t sub_reg)))) t_level le lm Top), lm,le)
+		    | _ -> (Error l "internal error, unrecognized read, no id",lm,le) end) end)
 	    | V_unknown -> (Value (retaint value_whole V_unknown),lm,l_env)
-            | _ -> (Error l "Internal error, neither register nor record at field access",lm,le) end)
+            | _ -> 
+	      (Error l ("Internal error: neither register nor record at field access " 
+			^ (string_of_value value_whole)),lm,le) end)
         (fun a -> 
 	  match (exp,a) with
 	    | (E_aux _ (l,Just(_,Tag_extern _,_,_)),
@@ -1401,6 +1440,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	  match detaint iv with
 	    | V_unknown -> (Value iv,lm,le)
 	    | V_lit (L_aux (L_num n) ln) ->
+	      let n = natFromInteger n in
               resolve_outcome
 		(interp_main mode t_level l_env lm vec)
 		(fun vvec lm le ->
@@ -1461,13 +1501,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			      | V_tuple [v1;v2] ->
 				(match (detaint v1, detaint v2) with 
 				  | (V_lit (L_aux (L_num n1) ln1),V_lit (L_aux (L_num n2) ln2)) ->
+				    let (n1,n2) = (natFromInteger n1,natFromInteger n2) in
 				    (match vvec with
 				      | V_vector _ _ _ -> slice_vector vvec n1 n2
-				      | V_vector_sparse _ _ _ _ _ -> slice_vector vvec n1 n2
+				      | V_vector_sparse _ _ _ _ _ -> 
+					slice_vector vvec n1 n2
 				      | V_unknown -> 
 					let inc = n1 < n2 in
-					V_vector n1 inc 
-					  (List.replicate (natFromInteger ((if inc then n1-n2 else n2-n1)+1)) V_unknown)
+					V_vector n1 (if inc then IInc else IDec) 
+					  (List.replicate ((if inc then n1-n2 else n2-n1)+1) V_unknown)
 				      | _ -> Assert_extra.failwith ("Vector slice of non-vector " ^ (string_of_value vvec)) end) end)
 			      | _ -> Assert_extra.failwith("slice not a tuple of nums " ^ (string_of_value vtup)) end) in
 			  (Value (binary_taint take_slice slice vvec), lm,le))
@@ -1479,12 +1521,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			    | Action (Read_reg reg Nothing) stack ->
 			      match vec with
 				| (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> 
-				  Action (Read_reg reg (Just((get_num i1v),(get_num i2v)))) stack
+				  Action (Read_reg reg (Just((natFromInteger (get_num i1v)),(natFromInteger (get_num i2v))))) stack
 				| _ -> Action (Read_reg reg Nothing) (add_to_top_frame rebuild stack) end
 		            | Action (Read_reg reg (Just (o,p))) stack ->
 			      match vec with
 				| (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> 
-				  Action (Read_reg reg (Just((get_num i1v),(get_num i2v)))) stack
+				  Action (Read_reg reg (Just((natFromInteger (get_num i1v)),(natFromInteger (get_num i2v))))) stack
 				| _ -> Action (Read_reg reg (Just (o,p))) (add_to_top_frame rebuild stack) end
                             | _ -> update_stack a (add_to_top_frame rebuild) end)
 		 end)
@@ -1509,8 +1551,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 		     (interp_main mode t_level le lm vec)
                      (fun vec lm le ->
 		       let fvup vi vec = (match vec with
-			 | V_vector _ _ _ -> fupdate_vec vec n1 vup
-			 | V_vector_sparse _ _ _ _ _ -> fupdate_vec vec n1 vup
+			 | V_vector _ _ _ -> fupdate_vec vec (natFromInteger n1) vup
+			 | V_vector_sparse _ _ _ _ _ -> fupdate_vec vec (natFromInteger n1) vup
 			 | V_unknown -> V_unknown
                          | _ -> Assert_extra.failwith "Update of vector given non-vector" end) in
 		       (Value (binary_taint fvup vi vec),lm,le))
@@ -1549,8 +1591,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                              (fun vvec lm le ->
 			       let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) vi1 vi2 in
 			       let fup_v_slice v1 vvec = (match vvec with
-                                 | V_vector _ _ _ -> fupdate_vector_slice vvec v_rep n1 n2
-				 | V_vector_sparse _ _ _ _ _ -> fupdate_vector_slice vvec v_rep n1 n2
+                                 | V_vector _ _ _ -> 
+				   fupdate_vector_slice vvec v_rep (natFromInteger n1) (natFromInteger n2)
+				 | V_vector_sparse _ _ _ _ _ -> 
+				   fupdate_vector_slice vvec v_rep (natFromInteger n1) (natFromInteger n2)
 				 | V_unknown -> V_unknown
 				 | _ -> Assert_extra.failwith "Vector update requires vector" end) in
 			       (Value (binary_taint fup_v_slice slice vvec),lm,le))
@@ -1588,19 +1632,19 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 		 (interp_main mode t_level l_env lm e2)
                  (fun v2 lm le ->
 		   let append v1 v2 = (match (v1,v2) with
-                     | (V_vector m inc vals1, V_vector _ _ vals2) -> V_vector m inc (vals1++vals2)
-		     | (V_vector m inc vals1, V_vector_sparse _ len _ vals2 d) ->
-		       let original_len = integerFromNat (List.length vals1) in
+                     | (V_vector m dir vals1, V_vector _ _ vals2) -> V_vector m dir (vals1++vals2)
+		     | (V_vector m dir vals1, V_vector_sparse _ len _ vals2 d) ->
+		       let original_len = List.length vals1 in
 		       let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in
 		       let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in
-		       V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d
-		     | (V_vector_sparse m len inc vals1 d, V_vector _ _ vals2) ->
-		       let new_len = integerFromNat (List.length vals2) in
+		       V_vector_sparse m (len+original_len) dir (sparse_vals ++ sparse_update) d
+		     | (V_vector_sparse m len dir vals1 d, V_vector _ _ vals2) ->
+		       let new_len = List.length vals2 in
 		       let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in
-		       V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d
-		     | (V_vector_sparse m len inc vals1 d, V_vector_sparse _ new_len _ vals2 _) ->
+		       V_vector_sparse m (len+new_len) dir (vals1++sparse_vals) d
+		     | (V_vector_sparse m len dir vals1 d, V_vector_sparse _ new_len _ vals2 _) ->
 		       let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in
-		       V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d
+		       V_vector_sparse m (len+new_len) dir (vals1 ++ sparse_update) d
 		     | (V_unknown,_) -> V_unknown (*update to get length from type*)
 		     | (_,V_unknown) -> V_unknown (*see above*)
                      | _ -> Assert_extra.failwith "vector concat requires vector" end) in
@@ -1613,29 +1657,29 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     | E_tuple(exps) -> 
       exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
     | E_vector(exps) ->
-      let is_inc = (match typ with
-        | T_app "vector" (T_args [ _; _; T_arg_order (Ord_aux Ord_inc _); _]) -> true
-        | _ -> false end) in
-      let base = integerFromNat (if is_inc then 0 else (List.length exps) - 1) in
+      let (is_inc,dir) = (match typ with
+        | T_app "vector" (T_args [ _; _; T_arg_order (Ord_aux Ord_inc _); _]) -> (true,IInc)
+        | _ -> (false,IDec) end) in
+      let base = (if is_inc then 0 else (List.length exps) - 1) in
       exp_list mode t_level 
-        (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector base is_inc vals) l_env l_mem [] exps
+        (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector base dir vals) l_env l_mem [] exps
     | E_vector_indexed iexps (Def_val_aux default dannot) ->
       let (indexes,exps) = List.unzip iexps in
-      let (is_inc,base,len) = (match typ with
+      let (dir,base,len) = (match typ with
         | T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux Ord_inc _); _]) -> 
-	  (true,base,len)
+	  (IInc,base,len)
         | T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux _ _); _]) -> 
-	  (false,base,len) end) in
+	  (IDec,base,len) end) in
       (match default with
 	| Def_val_empty ->
 	  exp_list mode t_level 
 	    (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es) 
 				                (Def_val_aux default dannot)) (l,annot)))
-            (fun vals -> V_vector (if indexes=[] then 0 else (List_extra.head indexes)) is_inc vals)
+            (fun vals -> V_vector (if indexes=[] then 0 else (natFromInteger (List_extra.head indexes))) dir vals)
 	    l_env l_mem [] exps
 	| Def_val_dec default_exp ->
 	  let (b,len) = match (base,len) with
-	    | (Ne_const b,Ne_const l) -> (b,l) end in
+	    | (Ne_const b,Ne_const l) -> (natFromInteger b, natFromInteger l) end in
 	  resolve_outcome 
 	    (interp_main mode t_level l_env l_mem default_exp)
 	    (fun v lm le -> 
@@ -1645,7 +1689,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                   (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)
 			    (Def_val_aux (Def_val_dec ev) dannot))
 		     (l,annot)))
-		(fun vs -> (V_vector_sparse b len is_inc (map2 (fun i v -> (i,v)) indexes vs) v)) l_env l_mem [] exps)
+		(fun vs -> 
+		  (V_vector_sparse b len dir (map2 (fun i v -> ((natFromInteger i),v)) indexes vs) v)) l_env l_mem [] exps)
 	    (fun a -> 
 	      update_stack a 
 		(add_to_top_frame (fun e env -> 
@@ -1726,7 +1771,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	    (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)
+          | Just(_) -> (Value (V_ctor f typ C_Union v), lm, le)
           | Nothing -> (Error l (String.stringAppend "Internal error: function with ctor tag unfound " name),lm,le)
            end)
         | Tag_extern opt_name ->
@@ -1882,7 +1927,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 
 and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) 
   : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) =
-   let (Env defs instrs lets regs ctors subregs aliases) = t_level in
+   let (Env defs instrs default_dir lets regs ctors subregs aliases) = t_level in
   let (typ,tag,ncs,ef) = match annot with 
     | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -1921,7 +1966,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
           let start_pos = reg_start_pos regf in
 	  let reg_size = reg_size regf in
 	  let request = 
-            (Action (Write_reg regf Nothing (update_vector_start start_pos reg_size value))
+            (Action (Write_reg regf Nothing (update_vector_start default_dir start_pos reg_size value))
 	       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
 	     l_mem,l_env) in
           if is_top_level then (request,Nothing) 
@@ -1937,9 +1982,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 			(match in_env indexes subreg with
 			  | Just ir -> 
 			    (Action 
-			       (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing 
-				  (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value)) 
-			       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+			     (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing 
+			      (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value))
+			     (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
 				  t_level l_env l_mem Top), l_mem, l_env)
 			  | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
 		      | _ -> 
@@ -1950,9 +1995,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 			(match in_env indexes subreg with
 			  | Just ir -> 
 			    (Action 
-			       (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing 
-				  (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value))
-			       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+			     (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing 
+			      (update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value))
+			     (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
 				  t_level l_env l_mem Top), l_mem, l_env)
 			  | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
 		      | _ -> (Error l ("Internal error: alias spec has unknown register type "^id), l_mem, l_env) end)
@@ -1960,7 +2005,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		    resolve_outcome (interp_main mode t_level l_env l_mem e) 
 		      (fun v le lm -> match v with 
 			| V_lit (L_aux (L_num i) _) -> 
-			  (Action (Write_reg (Reg reg annot') (Just (i,i)) (update_vector_start i 1 value)) 
+			  let i = natFromInteger i in
+			  (Action (Write_reg (Reg reg annot') (Just (i,i)) 
+				     (update_vector_start default_dir i 1 value)) 
 			          (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
 				     t_level l_env l_mem Top), l_mem, l_env) end)
 		      (fun a -> a)
@@ -1973,8 +2020,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 			       (fun v le lm ->
 				 (match detaint v with
 				   | V_lit (L_aux (L_num stop) _) ->
+				     let (start,stop) = (natFromInteger start,natFromInteger stop) in
+				     let size = if start < stop then stop - start +1 else start -stop +1 in
 				     (Action (Write_reg (Reg reg annot') (Just (start,stop)) 
-						(update_vector_start start ((abs (start - stop)) +1) value)) 
+						(update_vector_start default_dir start size value))
 					(Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
 					   t_level l_env l_mem Top),
 				      l_mem, l_env) end))
@@ -1989,11 +2038,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
                    (match (t1,t2) with
 		      | (T_app "vector" (T_args [T_arg_nexp (Ne_const b1); T_arg_nexp (Ne_const r1); _;_]),
 			 T_app "vector" (T_args [T_arg_nexp (Ne_const b2); T_arg_nexp (Ne_const r2); _;_])) ->
-			(Action (Write_reg (Reg reg1 annot1) Nothing (slice_vector value b1 r1))
-			        (Thunk_frame (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2)
-						              (fst (to_exp <| mode with track_values =false|> eenv 
-                                                                           (slice_vector value (r1+1) r2)))) annot2)
-				              t_level l_env l_mem Top), l_mem,l_env) end) end)
+			(Action 
+			 (Write_reg (Reg reg1 annot1) Nothing (slice_vector value (natFromInteger b1) (natFromInteger r1)))
+			 (Thunk_frame (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2)
+						(fst (to_exp <| mode with track_values =false|> eenv 
+                                                    (slice_vector value (natFromInteger (r1+1)) (natFromInteger r2)))))
+					 annot2)
+			    t_level l_env l_mem Top), l_mem,l_env) end) end)
 	    | _ -> (Error l ("Internal error: alias not found for id " ^(get_id id)),l_mem,l_env) end) in
 	  (request,Nothing)
         | _ -> 
@@ -2020,13 +2071,17 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
           let name = get_id id in 
 	  (match find_function defs id with
 	    | Just(funcls) -> 
-              (match find_funcl funcls (V_tuple [v;value]) with
+	      let new_vals = match v with 
+		| V_tuple vs -> V_tuple (vs ++ [value])
+		| V_lit (L_aux L_unit _) -> value
+		| v -> V_tuple [v;value] end in
+              (match find_funcl funcls new_vals with
 		| [] -> ((Error l ("No matching pattern for function " ^ name ^
-				      " on value " ^ (string_of_value v)),l_mem,l_env),Nothing)
+				      " on value " ^ (string_of_value new_vals)),l_mem,l_env),Nothing)
 		| [(env,used_unknown,exp)] -> 
 		  (match (if mode.eager_eval 
 		          then (interp_main mode t_level env emem exp)
-		          else (debug_out (Just name) (Just v) exp t_level emem env)) with
+		          else (debug_out (Just name) (Just new_vals) exp t_level emem env)) with
 		    | (Value ret, _,_) -> ((Value ret, l_mem,l_env),Nothing)
 		    | (Action action stack,lm,le) ->
 		      (((update_stack (Action action stack) 
@@ -2073,7 +2128,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
           let start_pos = reg_start_pos regf in
 	  let reg_size = reg_size regf in
 	  let request = 
-            (Action (Write_reg regf Nothing (update_vector_start start_pos reg_size value)) 
+            (Action (Write_reg regf Nothing (update_vector_start default_dir start_pos reg_size value)) 
 	       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
 	     l_mem,l_env) in
           if is_top_level then (request,Nothing)
@@ -2092,6 +2147,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
               let (lexp,env) = le_builder e env in
               let (ie,env) = to_exp mode env i in
 	      (LEXP_aux (LEXP_vector lexp ie) (l,annot), env)) in
+	  let n = natFromInteger n in
           (match (create_write_message_or_update mode t_level value l_env lm false lexp) with
           | ((Value v_whole,lm,le),maybe_builder) ->
             let v = detaint v_whole in
@@ -2101,10 +2157,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	      | V_boxref i _ -> 
 		(match (in_mem lm i,is_top_level,maybe_builder) with
 		  | ((V_vector _ _ _ as vec),true,_) ->
-		    let new_vec = fupdate_vector_slice vec (V_vector 1 true [value]) n n in
+		    let new_vec = fupdate_vector_slice vec (V_vector 1 default_dir [value]) n n in
 		    ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm i new_vec, l_env), Nothing)
 		  | ((V_track (V_vector _ _ _ as vec) r), true,_) ->
-		    let new_vec = fupdate_vector_slice vec (V_vector 1 true [value])  n n in
+		    let new_vec = fupdate_vector_slice vec (V_vector 1 default_dir [value])  n n in
 		    ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm i (taint new_vec r),l_env),Nothing)
 		  | ((V_vector _ _ _ as vec),false, Just lexp_builder) ->
 		    ((Value (access_vector vec n), lm, l_env), Just (next_builder lexp_builder))
@@ -2115,14 +2171,14 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		  | (V_register regform,true,_) ->
 		    let start_pos = reg_start_pos regform in
 		    let reg_size = reg_size regform in
-		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
+		    ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value)) 
 		        (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
 		      l_mem,l_env),
 		     Nothing)
 		  | (V_register regform,false,Just lexp_builder) ->
 		    let start_pos = reg_start_pos regform in
 		    let reg_size = reg_size regform in
-		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
+		    ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value)) 
 		        (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
 		      l_mem,l_env),
                      Just (next_builder lexp_builder))
@@ -2137,13 +2193,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		| (V_register regform,true,_) ->
 		    let start_pos = reg_start_pos regform in 
 		    let reg_size = reg_size regform in
-		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
+		    ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value)) 
 		      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
 		      l_mem,l_env),Nothing)
 		| (V_register regform,false,Just lexp_builder) ->
 		    let start_pos = reg_start_pos regform in
 		    let reg_size = reg_size regform in
-		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
+		    ((Action (Write_reg regform Nothing (update_vector_start default_dir start_pos reg_size value)) 
 		      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
 		      l_mem,l_env),
                      Just (next_builder lexp_builder))				
@@ -2163,12 +2219,12 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
            | ((Write_reg regf Nothing value),true) -> 
 	     ((Action (Write_reg regf (Just (n,n)) 
 			 (if (vector_length value) = 1 
-			  then (update_vector_start n 1 value)
+			  then (update_vector_start default_dir n 1 value)
 			  else (access_vector value n))) s, lm,le), Nothing)
            | ((Write_reg regf Nothing value),false) -> 
 	     ((Action (Write_reg regf (Just (n,n)) 
 			 (if (vector_length value) = 1 
-			  then (update_vector_start n 1 value)
+			  then (update_vector_start default_dir n 1 value)
 			  else (access_vector value n))) 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)
@@ -2196,6 +2252,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
                   let (e2,env) = to_exp mode env i2 in
                   let (lexp,env) = le_builder e env in
                   (LEXP_aux (LEXP_vector_range lexp e1 e2) (l,annot), env)) in
+	      let (n1,n2) = (natFromInteger n1,natFromInteger n2) in
               (match (create_write_message_or_update mode t_level value l_env lm false lexp) with
               | ((Value v,lm,le), Just lexp_builder) ->
 		(match (detaint v,is_top_level) with
@@ -2208,15 +2265,15 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		| (V_unknown,_) -> 
 		  let inc =  n1 < n2 in
 		  let start = if inc then n1 else (n2-1) in
-		  let size = natFromInteger ((abs (n1-n2)) + 1) in      
-		  ((Value (V_vector start inc (List.replicate size V_unknown)),lm,l_env),Nothing)
+		  let size = if inc then n2-n1 +1 else n1 -n2 +1 in      
+		  ((Value (V_vector start (if inc then IInc else IDec) (List.replicate size V_unknown)),lm,l_env),Nothing)
                 | _ -> ((Error l "Vector required",lm,le),Nothing) end)
               | ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
-		let len = ((abs (n1-n2)) +1) in
+		let len = (if n1 < n2 then n2 -n1 else n1 - n2) +1 in
                 ((Action 
 		    (Write_reg regf (Just (n1,n2)) 
 		       (if (vector_length value) <= len 
-			then (update_vector_start n1 len value)
+			then (update_vector_start default_dir n1 len value)
 			else (slice_vector value n1 n2))) s,lm,le),
 		 Just (next_builder lexp_builder))
               | ((Action (Write_mem id a Nothing value) s,lm,le), Just lexp_builder) ->
@@ -2258,8 +2315,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	   | Just(indexes) ->
 	     match in_env indexes id with
 	       | Just ir -> 
-		 ((Action (Write_reg (SubReg id regf ir) Nothing 
-			     (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value)) s,
+		 ((Action 
+		     (Write_reg (SubReg id regf ir) Nothing 
+			(update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s,
 		   lm,le), 
 		  (if is_top_level then Nothing else next_builder))
 	       | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
@@ -2270,8 +2328,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	   | Just(indexes) ->
 	     match in_env indexes id with
 	       | Just ir -> 
-		 ((Action (Write_reg (SubReg id regf ir) Nothing 
-			     (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value)) s,
+		 ((Action 
+		     (Write_reg (SubReg id regf ir) Nothing 
+			(update_vector_start default_dir (get_first_index_range ir) (get_index_range_size ir) value)) s,
 		   lm,le), 
 		  (if is_top_level then Nothing else next_builder))
 	       | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
@@ -2303,7 +2362,7 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
 end	
 
 and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
-  let (Env defs instrs lets regs ctors subregs aliases) = t_level in 
+  let (Env defs instrs default_dir lets regs ctors subregs aliases) = t_level in 
   let stack = Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot))) t_level l_env l_mem Top in
   let get_reg_typ_name typ =
     match typ with
@@ -2323,6 +2382,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
       resolve_outcome (interp_main mode t_level l_env l_mem e) 
         (fun v le lm -> match v with 
 	  | V_lit (L_aux (L_num i) _) -> 
+	    let i = natFromInteger i in
 	    (Action (Read_reg (Reg reg annot') (Just (i,i))) stack, l_mem, l_env) end)
         (fun a -> a) (*Should not currently happen as type system enforces constants*)
     | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> 
@@ -2335,6 +2395,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
 		 (fun v le lm ->
 		   (match v with
 		     | V_lit (L_aux (L_num stop) _) ->
+		       let (start,stop) = (natFromInteger start,natFromInteger stop) in
 		       (Action (Read_reg (Reg reg annot') (Just (start,stop))) stack, l_mem, l_env) end))
 		 (fun a -> a)) end)
         (fun a -> a) (*Neither action function should occur, due to above*)
@@ -2358,7 +2419,7 @@ let rec eval_toplevel_let handle_action tlevel env mem lbind =
     | _ -> Nothing end
 
 let rec to_global_letbinds handle_action (Defs defs) t_level =
-  let  (Env defs' instrs lets regs ctors subregs aliases) = t_level in
+  let  (Env defs' instrs default_dir lets regs ctors subregs aliases) = t_level in
   match defs with
   | [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, eenv),t_level)
   | def::defs ->
@@ -2366,25 +2427,36 @@ let rec to_global_letbinds handle_action (Defs defs) t_level =
     | DEF_val lbind ->
       match eval_toplevel_let handle_action t_level eenv emem lbind with
 	| Just le -> 
-	  to_global_letbinds handle_action (Defs defs) (Env defs' instrs (lets++le) regs ctors subregs aliases)
+	  to_global_letbinds handle_action (Defs defs) (Env defs' instrs default_dir (lets++le) regs ctors subregs aliases)
 	| Nothing -> 
-	  to_global_letbinds handle_action (Defs defs) (Env defs' instrs lets regs ctors subregs aliases) end
+	  to_global_letbinds handle_action (Defs defs) (Env defs' instrs default_dir lets regs ctors subregs aliases) end
     | DEF_type (TD_aux tdef _) ->
       match tdef with
       | TD_enum id ns ids _ -> 
-        let enum_vals = map (fun eid -> (eid,V_ctor eid (T_id (get_id id)) unitv)) ids in
-        to_global_letbinds handle_action (Defs defs) (Env defs' instrs (lets++enum_vals) regs ctors subregs aliases)
+        let enum_vals = map (fun eid -> (eid,V_ctor eid (T_id (get_id id)) C_Enum unitv)) ids in
+        to_global_letbinds 
+	  handle_action (Defs defs) (Env defs' instrs default_dir (lets++enum_vals) regs ctors subregs aliases)
       | _ -> to_global_letbinds handle_action (Defs defs) t_level end
     | _ -> to_global_letbinds handle_action (Defs defs) t_level
     end
   end
 
+let rec extract_default_direction (Defs defs) = match defs with 
+  | [] -> IInc (*When lack of a declared default, go for inc*)
+  | def::defs ->
+    match def with
+      | DEF_default (DT_aux (DT_order Oinc) _) -> IInc
+      | DEF_default (DT_aux (DT_order Odec) _) -> IDec
+      | _ -> extract_default_direction (Defs defs) end end
+
 (*TODO Contemplate making decode and execute environment variables instead of these constants*)
 let to_top_env external_functions defs = 
+  let direction = (extract_default_direction defs) in
   let t_level = Env defs (extract_instructions "decode" "execute" defs) 
+                    direction
                     [] (* empty letbind and enum values, call below will fill in any *) 
 		    (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
-  let (o,t_level) = to_global_letbinds external_functions defs t_level in
+  let (o,t_level) = to_global_letbinds (external_functions direction) defs t_level in
   match o with
     | (Value _,_,_) -> (Nothing,t_level)
     | (o,_,_) -> (Just o,t_level)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index e4d12ac9..f3dad5bf 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -9,9 +9,9 @@ open import Assert_extra
 
 val intern_reg_value : register_value -> Interp.value
 val intern_mem_value : memory_value -> Interp.value
-val extern_reg_value : maybe integer -> Interp.value -> register_value
+val extern_reg_value : maybe nat -> Interp.value -> register_value
 val extern_mem_value : interp_mode -> Interp.value -> (memory_value * maybe (list reg_name))
-val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name
+val extern_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name
 
 
 let make_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values |>;;
@@ -79,21 +79,22 @@ let bits_to_word8 b =
   then natFromInteger (integerFromBoolList (false,(List.reverse (List.map to_bool b))))
   else Assert_extra.failwith "bits_to_word8 given a non-8 list or one containing ? and u"
 
-(*All but reg_value should take a mode to get direction and start correct*)
+(*!!! All but reg_value should take a mode to get direction and start correct*)
 let intern_opcode (Opcode v) =
-  Interp.V_vector 0 true
+  Interp.V_vector 0 Interp.IInc
     (List.concatMap (fun (Byte(bits)) -> (List.map bit_to_ibit bits)) v)
 		   
 let intern_reg_value v = match v with
   | <| rv_bits=[b] |> -> bitl_to_ibit b
-  | _ -> Interp.V_vector (integerFromInt v.rv_start) (v.rv_dir = D_increasing) (bitls_to_ibits v.rv_bits)
+  | _ -> Interp.V_vector v.rv_start (if v.rv_dir = D_increasing then Interp.IInc else Interp.IDec) (bitls_to_ibits v.rv_bits)
 end
 
+(*!!! Another two that need the direction *)
 let intern_mem_value v = 
-  Interp.V_vector 0 true (List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits) v)
+  Interp.V_vector 0 Interp.IInc (List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits) v)
 
 let intern_ifield_value v =
-  Interp.V_vector 0 true (bits_to_ibits v)
+  Interp.V_vector 0 Interp.IInc (bits_to_ibits v)
 
 (*let byte_list_of_integer size num = 
   if (num < 0)
@@ -134,40 +135,41 @@ let integer_of_byte_list bytes =
 let extern_reg r slice = match (r,slice) with
   | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_)),Nothing) -> 
     Reg x (Interp.reg_size r)
-  | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_)),Just(i1,i2)) -> Reg_slice x (i1,i2)
+  | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_)),Just(i1,i2)) -> Reg_slice x (intFromNat i1, intFromNat i2)
   | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> 
+    let i = intFromInteger i in
     Reg_field y x (i,i)
   | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_range i j) _), Nothing) -> 
-    Reg_field y x (i,j)
+    Reg_field y x (intFromInteger i,intFromInteger j)
   | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_range i j) _), Just(i1,j1)) ->
-    Reg_f_slice y x (i,j) (i1,j1)
+    Reg_f_slice y x (intFromInteger i,intFromInteger j) (intFromNat i1, intFromNat j1)
 end
 
 let rec extern_reg_value optional_start v = match v with
   | Interp.V_track v regs -> extern_reg_value optional_start v 
-  | Interp.V_vector fst inc bits ->
+  | Interp.V_vector fst dir bits ->
     <| rv_bits=(bitls_from_ibits bits); 
-       rv_dir=(if inc then D_increasing else D_decreasing);
-       rv_start=(intFromInteger fst)|>
+       rv_dir=(if Interp.is_inc(dir) then D_increasing else D_decreasing);
+       rv_start=fst|>
   | Interp.V_vector_sparse fst stop inc bits default ->
     extern_reg_value optional_start (Interp_lib.fill_in_sparse v)
   | Interp.V_lit (L_aux L_zero _) -> 
-    let start = match optional_start with | Nothing -> 0 | Just i -> (intFromInteger i) end in
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
     <| rv_bits=[Bitl_zero]; rv_dir=D_increasing; rv_start=start |>
   | Interp.V_lit (L_aux L_false _) ->
-    let start = match optional_start with | Nothing -> 0 | Just i -> (intFromInteger i) end in
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
     <| rv_bits=[Bitl_zero]; rv_dir=D_increasing; rv_start=start |>
   | Interp.V_lit (L_aux L_one _) -> 
-    let start = match optional_start with | Nothing -> 0 | Just i -> (intFromInteger i) end in
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
     <| rv_bits=[Bitl_one]; rv_dir=D_increasing; rv_start=start |>
   | Interp.V_lit (L_aux L_true _) ->
-    let start = match optional_start with | Nothing -> 0 | Just i -> (intFromInteger i) end in
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
     <| rv_bits=[Bitl_one]; rv_dir=D_increasing; rv_start=start |>
   | Interp.V_lit (L_aux L_undef _) -> 
-    let start = match optional_start with | Nothing -> 0 | Just i -> (intFromInteger i) end in
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
     <| rv_bits=[Bitl_undef]; rv_dir=D_increasing; rv_start=start |>
   | Interp.V_unknown -> 
-    let start = match optional_start with | Nothing -> 0 | Just i -> (intFromInteger i) end in
+    let start = match optional_start with | Nothing -> 0 | Just i -> i end in
     <| rv_bits=[Bitl_unknown]; rv_dir=D_increasing; rv_start=start |>
 end 
 
@@ -195,10 +197,8 @@ end
 
 let rec slice_reg_value v start stop = 
   let inc = v.rv_dir = D_increasing in
-  let start = intFromInteger start in
-  let stop = intFromInteger stop in
-  <| v with rv_bits = (Interp.from_n_to_n (integerFromInt (if inc then (start - v.rv_start) else (v.rv_start - start)))
-                                          (integerFromInt (if inc then (stop - v.rv_start) else (v.rv_start - stop))) v.rv_bits);
+  <| v with rv_bits = (Interp.from_n_to_n (if inc then (start - v.rv_start) else (v.rv_start - start))
+                                          (if inc then (stop - v.rv_start) else (v.rv_start - stop)) v.rv_bits);
             rv_start = (if inc then start else ((stop - start) + 1)) |> 
 
 (*
@@ -262,111 +262,16 @@ let initial_instruction_state top_level main args =
   Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) e_args) (Interp_ast.Unknown, Nothing)) 
     top_level Interp.eenv Interp.emem Interp.Top
 
-let rec countLeadingZeros_helper bits =
-  match bits with
-    | (Interp.V_lit (L_aux L_zero _))::bits -> 
-      let (Interp.V_lit (L_aux (L_num n) loc)) = countLeadingZeros_helper bits in
-      Interp.V_lit (L_aux (L_num (n+1)) loc)
-    | _ -> Interp.V_lit (L_aux (L_num 0) Interp_ast.Unknown)
-end
-let rec countLeadingZeros (Interp.V_tuple v) = match v with
-  | [Interp.V_track v r;Interp.V_track v2 r2] -> 
-    Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) (r++r2)
-  | [Interp.V_track v r;v2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r
-  | [v;Interp.V_track v2 r2] -> Interp.taint (countLeadingZeros (Interp.V_tuple [v;v2])) r2
-  | [Interp.V_unknown;_] -> Interp.V_unknown
-  | [_;Interp.V_unknown] -> Interp.V_unknown
-  | [Interp.V_vector _ _ bits;Interp.V_lit (L_aux (L_num n) _)] -> 
-    countLeadingZeros_helper (snd (List.splitAt (natFromInteger n) bits))
-end
-
-(*Power specific external functions*)
-let power_externs = [
-  ("countLeadingZeroes", countLeadingZeros);
-]
-
-(*All external functions*)
-let external_functions = Interp_lib.function_map ++ power_externs
 
-type mem_function = (string * 
-                     (maybe read_kind * maybe write_kind * 
-			(interp_mode -> Interp.value -> (memory_value * (maybe (list reg_name))))))
-type barrier_function = (string * barrier_kind)
-
-(*List of memory functions; needs to be expanded with all of the memory functions needed for PPCMem.
-  Should probably be expanded into a parameter to mode as with above
-*)
-let memory_functions =
-  [ ("MEMr", (Just(Read_plain), Nothing, 
-	     (fun mode v -> match v with
-	       | Interp.V_tuple [location;length] ->
-		 match length with
-		   | Interp.V_lit (L_aux (L_num len) _) ->
-		     let (v,regs) = extern_mem_value mode location in
-		     (v,len,regs) 
-		   | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-		     let (v,loc_regs) = extern_mem_value mode location in
-		     match loc_regs with
-		       | Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
-		       | Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
-	      end end end)));
-    ("MEMr_reserve", (Just(Read_reserve),Nothing,
-		      (fun mode v -> match v with
-			| Interp.V_tuple [location;length] ->
-			  match length with
-			    | Interp.V_lit (L_aux (L_num len) _) ->
-			      let (v,regs) = extern_mem_value mode location in
-			      (v,len,regs) 
-			    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-			      let (v,loc_regs) = extern_mem_value mode location in
-			      match loc_regs with
-				| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
-				| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
-		       end end end)));		      
-    ("MEMw", (Nothing, Just(Write_plain), 
-	      (fun mode v -> match v with
-		| Interp.V_tuple [location;length] ->
-		  match length with
-		    | Interp.V_lit (L_aux (L_num len) _) ->
-		      let (v,regs) = extern_mem_value mode location in
-		      (v,len,regs)
-		    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-		      let (v,loc_regs) = extern_mem_value mode location in
-		      match loc_regs with
-			| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
-			| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
-	       end end end)));
-    ("MEMw_conditional", (Nothing, Just(Write_conditional), 
-	      (fun mode v -> match v with
-		| Interp.V_tuple [location;length] ->
-		  match length with
-		    | Interp.V_lit (L_aux (L_num len) _) ->
-		      let (v,regs) = extern_mem_value mode location in
-		      (v,len,regs)
-		    | Interp.V_track (Interp.V_lit (L_aux (L_num len) _)) size_regs ->
-		      let (v,loc_regs) = extern_mem_value mode location in
-		      match loc_regs with
-			| Nothing -> (v,len,Just (List.map (fun r -> extern_reg r Nothing) size_regs))
-			| Just loc_regs -> (v,len,Just (loc_regs++(List.map (fun r -> extern_reg r Nothing) size_regs)))
-	      end end end)));
-  ]
-
-let barrier_functions = [
-  ("I_Sync", Isync);
-  ("H_Sync", Sync);
-  ("LW_Sync", LwSync);
-  ("EIEIO", Eieio);
-]
-
-let rec interp_to_value_helper arg instr thunk = 
+let rec interp_to_value_helper arg instr direction thunk = 
   match thunk() with
     | Interp.Value value -> (Just value,Nothing)
     | Interp.Error l msg -> (Nothing, Just (Internal_error msg))
     | Interp.Action (Interp.Call_extern i value) stack ->
-      match List.lookup i external_functions with
+      match List.lookup i (Interp_lib.library_functions direction) with
 	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
 	| Just f  -> 
-          interp_to_value_helper arg instr (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
+          interp_to_value_helper arg instr direction (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
       end 
     | Interp.Action (Interp.Exit (E_aux e _)) _ ->
       match e with
@@ -376,15 +281,19 @@ let rec interp_to_value_helper arg instr thunk =
     | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
 end
 
-let call_external_functions outcome = 
+let call_external_functions direction outcome = 
   match outcome with
     | Interp.Action (Interp.Call_extern i value) stack ->
-      match List.lookup i external_functions with
+      match List.lookup i (Interp_lib.library_functions direction) with
 	| Nothing -> Nothing
 	| Just f -> Just (f value) end
     | _ -> Nothing end
 
-let build_context defs = match Interp.to_top_env call_external_functions defs with (_,context) -> context end
+let build_context defs reads writes barriers externs = 
+  (*TODO add externs to to_top_env*)
+  match Interp.to_top_env call_external_functions defs with 
+    | (_,((Interp.Env _ _ dir _ _ _ _ _) as context)) -> 
+      Context context (if Interp.is_inc(dir) then D_increasing else D_decreasing) reads writes barriers externs end
 
 
 let rec find_instruction i = function
@@ -399,24 +308,25 @@ end
 let migrate_typ = function
   | Instruction_extractor.IBit -> Bit
   | Instruction_extractor.IBitvector len ->
-    Bvector (match len with Nothing -> Nothing | Just i -> Just (intFromInteger i) end) 
+    Bvector (match len with Nothing -> Nothing | Just i -> Just (natFromInteger i) end) 
   | Instruction_extractor.IOther -> Other
 end
 
 let decode_to_istate top_level value = 
   let mode = make_mode true false in
   let (arg,_) = Interp.to_exp mode Interp.eenv (intern_opcode value) in
-  let (Interp.Env _ instructions _ _ _ _ _) = top_level in
-  let (instr_decoded,error) = interp_to_value_helper value ("",[],[])
+  let (Context ((Interp.Env _ instructions _ _ _ _ _ _) as top_env) direction _ _ _ _) = top_level in
+  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
+  let (instr_decoded,error) = interp_to_value_helper value ("",[],[]) internal_direction
     (fun _ -> Interp.resume 
       (make_mode true false) 
       (Interp.Thunk_frame 
 	 (E_aux (E_app (Id_aux (Id "decode") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) 
-	 top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
+	 top_env Interp.eenv Interp.emem Interp.Top) Nothing) in
   match (instr_decoded,error) with
     | (Just instr, _) -> 
       let instr_external = match instr with
-	| Interp.V_ctor (Id_aux (Id i) _) _ parm ->
+	| Interp.V_ctor (Id_aux (Id i) _) _ _ parm ->
 	  match (find_instruction i instructions) with
 	    | Just(Instruction_extractor.Instr_form name parms effects) -> 
 	      match (parm,parms) with
@@ -429,20 +339,21 @@ let decode_to_istate top_level value =
 		     (p_name,(migrate_typ ie_typ),(extern_ifield_value value))) vals parms), effects)
           end end end in 
       let (arg,_) = Interp.to_exp mode Interp.eenv instr in
-      let (instr_decoded,error) = interp_to_value_helper value instr_external
+      let (instr_decoded,error) = interp_to_value_helper value instr_external internal_direction
 	(fun _ -> Interp.resume 
 	 (make_mode true false) 
 	 (Interp.Thunk_frame 
 	 (E_aux (E_app (Id_aux (Id "supported_instructions") Interp_ast.Unknown) [arg]) 
 	    (Interp_ast.Unknown, Nothing)) 
-	 top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
+	 top_env Interp.eenv Interp.emem Interp.Top) Nothing) in
       match (instr_decoded,error) with
 	| (Just instr,_) ->
 	  let (arg,_) = Interp.to_exp mode Interp.eenv instr in
 	  Instr instr_external
-	    (Interp.Thunk_frame
-		   (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
-		   top_level Interp.eenv Interp.emem Interp.Top)
+	    (IState (Interp.Thunk_frame
+		       (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
+		       top_env Interp.eenv Interp.emem Interp.Top)
+	       top_level)
 	| (Nothing, Just err) -> Decode_error err
       end 
     | (Nothing, Just err) -> Decode_error err
@@ -458,26 +369,31 @@ let decode_to_instruction (top_level:context) (value:opcode) : instruction_or_de
 val instruction_to_istate : context -> instruction -> instruction_state 
 let instruction_to_istate (top_level:context) (((name, parms, _) as instr):instruction) : instruction_state  = 
   let mode = make_mode true false in
+  let (Context top_env _ _ _ _ _) = top_level in
   let get_value (name,typ,v) = 
     let vec = intern_ifield_value v in
     let v = match vec with
       | Interp.V_vector start dir bits ->
 	match typ with
 	  | Bit -> match bits with | [b] -> b | _ -> Assert_extra.failwith "Expected a bitvector of length 1" end
-	  | Range _ -> Interp_lib.to_num Interp_lib.Signed vec
+	  | Range _ -> Interp_lib.to_num Interp_lib.Unsigned vec
 	  | _ -> vec
        end 
     end in
     let (e,_) = Interp.to_exp mode Interp.eenv v in e 
   in
-  (Interp.Thunk_frame
-       (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) 
-		 [(E_aux (E_app (Id_aux (Id name) Interp_ast.Unknown) (List.map get_value parms))
-		        (Interp_ast.Unknown,Interp.ctor_annot (T_id "ast")) (*This type shouldn't be hard-coded*))])
-	      (Interp_ast.Unknown,Nothing))
-       top_level Interp.eenv Interp.emem Interp.Top)
-
-let rec interp_to_outcome mode thunk = 
+  (IState
+     (Interp.Thunk_frame
+	(E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) 
+		  [(E_aux (E_app (Id_aux (Id name) Interp_ast.Unknown) (List.map get_value parms))
+		      (Interp_ast.Unknown,Interp.ctor_annot (T_id "ast")) (*This type shouldn't be hard-coded*))])
+	   (Interp_ast.Unknown,Nothing))
+	top_env Interp.eenv Interp.emem Interp.Top)
+     top_level)
+
+let rec interp_to_outcome mode context thunk = 
+  let (Context _ direction mem_reads mem_writes barriers spec_externs) = context in
+  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
   match thunk () with
   | Interp.Value _ -> Done
   | Interp.Error l msg -> Error msg (*Todo, add the l information the string format*)
@@ -488,59 +404,61 @@ let rec interp_to_outcome mode thunk =
                (fun v -> 
                  let v = (intern_reg_value v) in
                  let v = if mode.Interp.track_values then (Interp.V_track v [reg_form]) else v in 
-                 Interp.add_answer_to_stack next_state v)
+                 IState (Interp.add_answer_to_stack next_state v) context)
     | Interp.Write_reg reg_form slice value ->
       let optional_start = 
 	match slice with | Just (st1,st2) -> if (st1=st2) then Just st1 else Nothing | _ -> Nothing end in
-      Write_reg (extern_reg reg_form slice) (extern_reg_value optional_start value) next_state
+      Write_reg (extern_reg reg_form slice) (extern_reg_value optional_start value) (IState next_state context)
     | Interp.Read_mem (Id_aux (Id i) _) value slice ->
-      match List.lookup i memory_functions with
-      | (Just (Just read_k,_,f)) -> 
+      match List.lookup i mem_reads with
+      | (Just (MR read_k f)) -> 
         let (location, length, tracking) = (f mode value) in 
 	if (List.length location) = 8
         then Read_mem read_k (Address_lifted location) length tracking 
-	  (fun v -> Interp.add_answer_to_stack next_state (intern_mem_value v))
+	  (fun v -> IState (Interp.add_answer_to_stack next_state (intern_mem_value v)) context)
 	else Error ("Memory address on read is not 64 bits")
       | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
       end
     | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
-      match List.lookup i memory_functions with
-      | (Just (_,Just write_k,f)) -> 
+      match List.lookup i mem_writes with
+      | (Just (MW write_k f _)) -> 
         let (location, length, tracking) = (f mode loc_val) in
         let (value, v_tracking) = (extern_mem_value mode write_val) in
 	if (List.length location) = 8
-        then Write_mem write_k (Address_lifted location) length tracking value v_tracking (fun b -> next_state) 
+        then Write_mem write_k (Address_lifted location) 
+	  length tracking value v_tracking (fun b -> (IState next_state context)) 
 	(*Note, does not pass boolean on conditional write, but we're not using that yet anyway*)
 	else Error "Memory address on write is not 64 bits"
       | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
       end 
     | Interp.Barrier (Id_aux (Id i) _) lval ->
-      match List.lookup i barrier_functions with
+      match List.lookup i barriers with
 	| Just barrier -> 
-	  Barrier barrier next_state
+	  Barrier barrier (IState next_state context)
 	| _ -> Error ("Barrier " ^ i ^ " function not found") end
     | Interp.Nondet exps -> 
       let nondet_states = List.map (Interp.set_in_context next_state) exps in
-      Nondet_choice nondet_states next_state      
+      Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context)
     | Interp.Call_extern i value -> 
-      match List.lookup i external_functions with
+      match List.lookup i ((Interp_lib.library_functions internal_direction) ++ spec_externs) with
       | Nothing -> Error ("External function not available " ^ i)
       | Just f  -> 
         if (mode.Interp.eager_eval)
-        then interp_to_outcome mode (fun _ -> Interp.resume mode next_state (Just (f value))) 
+        then interp_to_outcome mode context (fun _ -> Interp.resume mode next_state (Just (f value))) 
         else let new_v = f value in
              Internal (Just i) 
                       (Just (fun _ -> (Interp.string_of_value value) ^ "=>" ^ (Interp.string_of_value new_v)))
-                      (Interp.add_answer_to_stack next_state new_v)
+                      (IState (Interp.add_answer_to_stack next_state new_v) context)
       end
-    | Interp.Step l Nothing Nothing -> Internal Nothing Nothing next_state 
-    | Interp.Step l (Just name) Nothing -> Internal (Just name) Nothing next_state
+    | Interp.Step l Nothing Nothing -> Internal Nothing Nothing (IState next_state context)
+    | Interp.Step l (Just name) Nothing -> Internal (Just name) Nothing (IState next_state context)
     | Interp.Step l (Just name) (Just value) ->
-      Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) next_state
+      Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context)
     end 
   end 
 
-let interp mode i_state = interp_to_outcome mode (fun _ -> Interp.resume mode i_state Nothing)
+let interp mode (IState interp_state context) = 
+  interp_to_outcome mode context (fun _ -> Interp.resume mode interp_state Nothing)
 
 (*TODO: Only find some sub piece matches, need to look for field/slice sub pieces*)
 let rec find_reg_name reg = function
@@ -549,13 +467,13 @@ let rec find_reg_name reg = function
     match (reg,reg_name) with
       | (Reg i size, Reg n size2) -> if i = n && size = size2 then (Just v) else find_reg_name reg registers
       | (Reg_slice i (p1,p2), Reg n _) -> 
-	if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
+	if i = n then (Just (slice_reg_value v (natFromInt p1) (natFromInt p2))) else find_reg_name reg registers
       | (Reg_field i f (p1,p2), Reg n _) -> 
-	if i = n then (Just (slice_reg_value v p1 p2)) else find_reg_name reg registers
+	if i = n then (Just (slice_reg_value v (natFromInt p1) (natFromInt p2))) else find_reg_name reg registers
       | (Reg_slice  i (p1,p2), Reg_slice n (p3,p4)) ->
 	if i=n 
 	then if p1=p3 && p2 = p4 then (Just v)
-	     else if p1>=p3 && p2<= p4 then (Just (slice_reg_value v p1 p2))
+	     else if p1>=p3 && p2<= p4 then (Just (slice_reg_value v (natFromInt p1) (natFromInt p2)))
 	     else find_reg_name reg registers
 	  else find_reg_name reg registers
       | (Reg_field i f _,Reg_field n fn _) ->
@@ -567,16 +485,19 @@ end end
 
 let reg_size = function
   | Reg i size -> size
-  | Reg_slice i (p1,p2) -> if p1 < p2 then (p2-p1 +1) else (p1-p2 +1)
-  | Reg_field i f (p1,p2) -> if p1 < p2 then (p2-p1 +1) else (p1-p2 +1)
-  | Reg_f_slice i f _ (p1,p2) -> if p1 < p2 then p2-p1 +1 else p1-p2+1
+  | Reg_slice i (p1,p2) -> natFromInt (if p1 < p2 then (p2-p1 +1) else (p1-p2 +1))
+  | Reg_field i f (p1,p2) -> natFromInt (if p1 < p2 then (p2-p1 +1) else (p1-p2 +1))
+  | Reg_f_slice i f _ (p1,p2) -> natFromInt (if p1 < p2 then p2-p1 +1 else p1-p2+1)
 end
 
-let rec ie_loop mode register_values i_state = 
+let rec ie_loop mode register_values (IState interp_state context) = 
+  let (Context _ direction externs reads writes barriers) = context in
   let unknown_reg size =  
-    <| rv_bits = (List.replicate (natFromInteger size) Bitl_unknown); rv_start = 0; rv_dir = D_increasing |> in
-  let unknown_mem size = List.replicate (natFromInteger size) (Byte_lifted (List.replicate 8 Bitl_unknown)) in
-  match (interp mode i_state) with
+    <| rv_bits = (List.replicate size Bitl_unknown);
+       rv_start = (if direction = D_increasing then 0 else (size-1));
+       rv_dir = direction |> in
+  let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in
+  match interp mode (IState interp_state context) with
     | Done -> []
     | Error msg -> [E_error msg]
     | Read_reg reg i_state_fun -> 
@@ -603,8 +524,11 @@ let interp_exhaustive register_values i_state =
   ie_loop mode register_values i_state
 
 let rec rr_ie_loop mode i_state = 
+  let (IState _ (Context _ direction _ _ _ _)) = i_state in
   let unknown_reg size =  
-    <| rv_bits = (List.replicate size Bitl_unknown); rv_start = 0; rv_dir = D_increasing |> in
+    <| rv_bits = (List.replicate size Bitl_unknown); 
+       rv_start = (if direction=D_increasing then 0 else (size-1));
+       rv_dir = direction |> in
   let unknown_mem size = List.replicate size (Byte_lifted (List.replicate 8 Bitl_unknown)) in
   match (interp mode i_state) with
     | Done -> ([],Done)
@@ -614,7 +538,7 @@ let rec rr_ie_loop mode i_state =
       let (events,outcome) = (rr_ie_loop mode i_state) in
       (((E_write_reg reg value)::events), outcome)
     | Read_mem read_k loc length tracking i_state_fun ->
-      let (events,outcome) = (rr_ie_loop mode (i_state_fun (unknown_mem (natFromInteger length)))) in 
+      let (events,outcome) = (rr_ie_loop mode (i_state_fun (unknown_mem length))) in 
       (((E_read_mem read_k loc length tracking)::events),outcome)
     | Write_mem write_k loc length tracking value v_tracking i_state_fun ->
       let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 3b83dd89..0b77909d 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -9,11 +9,6 @@ to take an opcode as defined above, instead of a value
 
 and change 
 
-  type instruction = (string * list (string * instr_parm_typ * value) * list base_effect)
-
-to 
-
-  type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect)
 *)
 
 
@@ -35,139 +30,13 @@ end
 
 type word8 = nat (* bounded at a byte, for when lem supports it*)
 
-(* Abstract types, to be accessed only through this interface *)
-type instruction_state = Interp.stack
-type context = Interp.top_level
-type interp_mode = Interp.interp_mode
+type interpreter_state = Interp.stack (*Deem abstract*)
+(* Will come from a .lem file generated by Sail, bound to a 'defs' identifier *)
+type specification = Interp_ast.defs Interp.tannot (*Deem abstract*)
+type interp_mode = Interp.interp_mode (*Deem abstract*)
 val make_mode : bool -> bool -> interp_mode
 val tracking_dependencies : interp_mode -> bool
 
-(*Concrete types*)
-type read_kind = Read_plain | Read_reserve | Read_acquire
-type write_kind = Write_plain | Write_conditional | Write_release
-type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB (* PS removed "plain" and added "Isync" and "ISB" *)
-
-(*type value = 
-| Bitvector of list bool  * bool * integer 
-(* In Bitvector bs b n:
-   - the bs are the bits (true represents 1 and false represents 0)
-   - the b specifies whether the indicies are increasing (true) or decreasing (false) along the list (for Power the Bitvector values are always increasing)    
-   - the n is the index of the head of the list
-*)
-(*To discuss:  ARM8 uses at least one abstract record form for 
-  some special registers, with no clear mapping to bits. Should
-  we permit Record of (string * Bitvector) values as well?
-*)
-| Bytevector of list word8 (* For memory accesses *)
-| Unknown
-(*To add: an abstract value representing an unknown but named memory address?*)
-
-instance (Ord bool)
-  let compare = defaultCompare
-  let (<) = defaultLess
-  let (<=) = defaultLessEq
-  let (>) = defaultGreater
-  let (>=) = defaultGreaterEq
-end
-
-let valueCompare v1 v2 = 
-  match (v1,v2) with
-  | (Bitvector bits1 inc1 start1, Bitvector bits2 inc2 start2) ->
-    tripleCompare compare compare compare (bits1,inc1,start1) (bits2,inc2,start2)
-  | (Bytevector words1, Bytevector words2) -> compare words1 words2
-  | (Unknown,Unknown) -> EQ
-  | (Bitvector _ _ _, _)  -> LT
-  | (Bytevector _, _) -> LT
-  | (_, _) -> GT
-  end
-
-instance (Ord value)
-  let compare = valueCompare
-  let (<) v1 v2 = (valueCompare v1 v2) = LT
-  let (<=) v1 v2 = (valueCompare v1 v2) <> GT
-  let (>) v1 v2 = (valueCompare v1 v2) = GT
-  let (>=) v1 v2 = (valueCompare v1 v2) <> LT
-end
-
-let valueEqual v1 v2 =
-  match (v1,v2) with
-    | (Bitvector bits1 inc1 start1, Bitvector bits2 inc2 start2) ->
-      bits1 = bits2 && inc1 = inc2 && start1 = start2
-    | (Bytevector words1, Bytevector words2) -> words1 = words2
-    | (Unknown,Unknown) -> true
-    | _ -> false
-end 
-
-instance  (Eq value)
-  let (=) = valueEqual
-  let (<>) x y = not (valueEqual x y)
-end
-*)
-type slice = (integer * integer)
-
-
-type reg_name = 
-| Reg of string * integer
-(*Name of the register, accessing the entire register, and the size of this register *)
-
-| Reg_slice of string * slice 
-(* Name of the register, accessing from the bit indexed by the first
-to the bit indexed by the second integer of the slice, inclusive. For
-Power the first will be a smaller number than or equal to the second;
-for other architectures it might be the other way round.  *)
-
-| Reg_field of string * string * slice 
-(*Name of the register and name of the field of the register
-accessed. The slice specifies where this field is in the register*)
-
-| Reg_f_slice of string * string * slice * slice 
-(* The first three components are as in Reg_field; the final slice
-specifies a part of the field, indexed w.r.t. the register as a whole *)
-
-
-(* because reg_name contains slice which currently contains Big_int.big_int, the default OCaml comparison is not sufficient and we need to define explicit type classes *)
-let slice_eq (s1l,s1r) (s2l,s2r) = (s1l = s2l) && (s1r = s2r)
-
-let reg_nameEqual r1 r2 = 
-  match (r1,r2) with
-  | (Reg s1 l1, Reg s2 l2) -> s1=s2 && l1=l2
-  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> s1=s2 && (slice_eq sl1 sl2)
-  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> s1=s2 && f1=f2 && (slice_eq sl1 sl2)
-  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> s1=s2 && f1=f2 && (slice_eq sl1 sl2) && (slice_eq sl1' sl2')
-  | _ -> false
-  end
-
-instance  (Eq reg_name)
-  let (=) = reg_nameEqual
-  let (<>) x y = not (reg_nameEqual x y)
-end
-
-let reg_nameCompare r1 r2 = 
-  match (r1,r2) with
-  | (Reg s1 l1, Reg s2 l2) -> pairCompare compare compare (s1,l1) (s2,l2)
-  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> pairCompare compare compare (s1,sl1) (s2,sl2)
-  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> 
-      tripleCompare compare compare compare (s1,f1,sl1) (s2,f2,sl2)
-  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> 
-      pairCompare compare (tripleCompare compare compare compare) (s1,(f1,sl1,sl1')) (s2,(f2,sl2,sl2'))
-  | (Reg _ _, _)  -> LT
-  | (Reg_slice _ _, _) -> LT
-  | (Reg_field _ _ _, _) -> LT
-  | (_, _) -> GT
-  end
-
-instance (SetType reg_name)
-  let setElemCompare = reg_nameCompare
-end
-
-instance (Ord reg_name)
-  let compare = reg_nameCompare
-  let (<)  r1 r2 = (reg_nameCompare r1 r2) = LT
-  let (<=) r1 r2 = (reg_nameCompare r1 r2) <> GT
-  let (>)  r1 r2 = (reg_nameCompare r1 r2) = GT
-  let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT
-end
-
 (** basic values *)
 
 type bit =
@@ -184,7 +53,7 @@ type direction =
   | D_increasing
   | D_decreasing
 
-type register_value = <| rv_bits: list bit_lifted (* MSB first, smallest index number *); rv_dir: direction; rv_start: int |>  (* beter for this to be int, not integer *)
+type register_value = <| rv_bits: list bit_lifted (* MSB first, smallest index number *); rv_dir: direction; rv_start: nat |>
 
 type byte_lifted = Byte_lifted of list bit_lifted (* of length 8 *)
 
@@ -260,12 +129,102 @@ instance (Ord address_lifted)
   let (>=) = defaultGreaterEq
 end
 
+(* Registers *)
+(*Can be nat nat, but finding out where ppcmem doens't like that is maybe not worth the effort *)
+type slice = (int * int)
+
+type reg_name = 
+| Reg of string * nat
+(*Name of the register, accessing the entire register, and the size of this register *)
+
+| Reg_slice of string * slice 
+(* Name of the register, accessing from the bit indexed by the first
+to the bit indexed by the second integer of the slice, inclusive. For
+Power the first will be a smaller number than or equal to the second;
+for other architectures it might be the other way round.  *)
+
+| Reg_field of string * string * slice 
+(*Name of the register and name of the field of the register
+accessed. The slice specifies where this field is in the register*)
+
+| Reg_f_slice of string * string * slice * slice 
+(* The first three components are as in Reg_field; the final slice
+specifies a part of the field, indexed w.r.t. the register as a whole *)
+
+
+(* because reg_name contains slice which currently contains Big_int.big_int, the default OCaml comparison is not sufficient and we need to define explicit type classes *)
+let slice_eq (s1l,s1r) (s2l,s2r) = (s1l = s2l) && (s1r = s2r)
+
+let reg_nameEqual r1 r2 = 
+  match (r1,r2) with
+  | (Reg s1 l1, Reg s2 l2) -> s1=s2 && l1=l2
+  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> s1=s2 && (slice_eq sl1 sl2)
+  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> s1=s2 && f1=f2 && (slice_eq sl1 sl2)
+  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> s1=s2 && f1=f2 && (slice_eq sl1 sl2) && (slice_eq sl1' sl2')
+  | _ -> false
+  end
+
+instance  (Eq reg_name)
+  let (=) = reg_nameEqual
+  let (<>) x y = not (reg_nameEqual x y)
+end
+
+let reg_nameCompare r1 r2 = 
+  match (r1,r2) with
+  | (Reg s1 l1, Reg s2 l2) -> pairCompare compare compare (s1,l1) (s2,l2)
+  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> pairCompare compare compare (s1,sl1) (s2,sl2)
+  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> 
+      tripleCompare compare compare compare (s1,f1,sl1) (s2,f2,sl2)
+  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> 
+      pairCompare compare (tripleCompare compare compare compare) (s1,(f1,sl1,sl1')) (s2,(f2,sl2,sl2'))
+  | (Reg _ _, _)  -> LT
+  | (Reg_slice _ _, _) -> LT
+  | (Reg_field _ _ _, _) -> LT
+  | (_, _) -> GT
+  end
+
+instance (SetType reg_name)
+  let setElemCompare = reg_nameCompare
+end
+
+instance (Ord reg_name)
+  let compare = reg_nameCompare
+  let (<)  r1 r2 = (reg_nameCompare r1 r2) = LT
+  let (<=) r1 r2 = (reg_nameCompare r1 r2) <> GT
+  let (>)  r1 r2 = (reg_nameCompare r1 r2) = GT
+  let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT
+end
+
+(* Data structures for building up instructions *)
+
+type read_kind = Read_plain | Read_reserve | Read_acquire
+type write_kind = Write_plain | Write_conditional | Write_release
+type barrier_kind = Sync | LwSync | Eieio | Isync | DMB | DMB_ST | DMB_LD | DSB | DSB_ST | DSB_LD | ISB 
+
+(*Map between external functions as preceived from a Sail spec and the actual implementation of the function *)
+type external_functions = list (string * (Interp.value -> Interp.value))
+
+(*Maps between the memory functions as preceived from a Sail spec and the values needed for actions in the memory model*)
+type barriers = list (string * barrier_kind)
+type memory_parameter_transformer = interp_mode -> Interp.value -> (memory_value * nat * maybe (list reg_name))
+type memory_read = MR of read_kind * memory_parameter_transformer
+type memory_reads  = list (string * memory_read)
+type memory_write = MW of write_kind * memory_parameter_transformer * (maybe (instruction_state -> bool -> instruction_state))
+and memory_writes = list (string * memory_write)
+
+(* Definition information needed to run an instruction *)
+and context = Context of Interp.top_level * direction * memory_reads * memory_writes * barriers * external_functions
+
+(* An instruction in flight *)
+and instruction_state = IState of interpreter_state * context
+
+
 type outcome =
 (* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values,
    integer is size to read, followed by registers that were used in computing that size *)
-| Read_mem of read_kind * address_lifted * integer * maybe (list reg_name) *  (memory_value -> instruction_state)
+| Read_mem of read_kind * address_lifted * nat * maybe (list reg_name) *  (memory_value -> instruction_state)
 (* Request to write memory, first value and dependent registers is location, second is the value to write *)
-| Write_mem of write_kind * address_lifted * integer * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state)
+| Write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name) * (bool -> instruction_state)
 (* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
 (* Request to read register, will track dependency when mode.track_values *)
@@ -282,18 +241,15 @@ type outcome =
 | Error of string
 
 type event = 
-| E_read_mem of read_kind * address_lifted * integer * maybe (list reg_name)
-| E_write_mem of write_kind * address_lifted * integer * maybe (list reg_name) * memory_value * maybe (list reg_name)
+| E_read_mem of read_kind * address_lifted * nat * maybe (list reg_name)
+| E_write_mem of write_kind * address_lifted * nat * maybe (list reg_name) * memory_value * maybe (list reg_name)
 | E_barrier of barrier_kind
 | E_read_reg of reg_name
 | E_write_reg of reg_name * register_value
 | E_escape
 | E_error of string (* Should not happen, but may if the symbolic evaluation doesn't work out*)
-(*To discuss: Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
-
 
-
-(* more explicit type classes to work around the occurrences of big_int in reg_name *)
+(* more explicit type classes to work around the occurrences of big_int in reg_name ::no longer necessary?*)
 instance (Ord read_kind)
   let compare = defaultCompare
   let (<) = defaultLess
@@ -340,18 +296,17 @@ instance (SetType event)
   let setElemCompare = eventCompare
 end
 
-
 (* Functions to build up the initial state for interpretation *)
-val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come from a .lem file generated by Sail*)
+val build_context : specification -> memory_reads -> memory_writes -> barriers -> external_functions -> context 
 val initial_instruction_state : context -> string -> list register_value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)
 
 (*Type representint the constructor parameters in instruction, other is a type not representable externally*)
 type instr_parm_typ = 
   | Bit (*A single bit, represented as a one element Bitvector as a value*)
-  | Range of maybe int (*Internall represented as a number, externally as a bitvector of length int *)
+  | Range of maybe nat (*Internall represented as a number, externally as a bitvector of length int *)
   | Other (*An unrepresentable type, will be represented as Unknown in instruciton form *)
-  | Bvector of maybe int (* A bitvector type, with length when statically known *)
+  | Bvector of maybe nat (* A bitvector type, with length when statically known *)
 
 let instr_parm_typEqual ip1 ip2 = match (ip1,ip2) with
   | (Bit,Bit) -> true
@@ -366,8 +321,9 @@ instance (Eq instr_parm_typ)
   let (<>) ip1 ip2 = not (instr_parm_typEqual ip1 ip2)
 end 
 
-(*A representation of the AST node for each instruction in the spec, with concrete values from this call, and the potential static effects from the funcl clause for this instruction 
-Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
+(*A representation of the AST node for each instruction in the spec, with concrete values from this call,
+  and the potential static effects from the funcl clause for this instruction 
+  Follows the form of the instruction in instruction_extractor, but populates the parameters with actual values
 *)
 type instruction = (string * list (string * instr_parm_typ * instruction_field_value) * list base_effect)
 
@@ -438,17 +394,17 @@ val word8_list_of_integer : integer -> integer -> list word8
 
 (* constructing values *)
 
-val register_value : bit_lifted -> direction -> int -> int -> register_value
+val register_value : bit_lifted -> direction -> nat -> nat -> register_value
 let register_value b dir width start_index = 
-  <| rv_bits = List.replicate (natFromInt width) b;
-     rv_dir = dir; (* D_increasing for Power *)
+  <| rv_bits = List.replicate width b;
+     rv_dir = dir; (* D_increasing for Power, D_decreasing for ARM *)
      rv_start = start_index; |>
 
-val register_value_zeros : direction -> int -> int -> register_value
+val register_value_zeros : direction -> nat -> nat -> register_value
 let register_value_zeros dir width start_index = 
   register_value Bitl_zero dir width start_index
 
-val register_value_ones : direction -> int -> int -> register_value
+val register_value_ones : direction -> nat -> nat -> register_value
 let register_value_ones dir width start_index = 
   register_value Bitl_one dir width start_index
 
@@ -462,8 +418,8 @@ let memory_value_unknown (width:int) : memory_value =
 
 (* lengths *)  
 
-val memory_value_length : memory_value -> integer
-let memory_value_length (mv:memory_value) = integerFromNat (List.length mv)
+val memory_value_length : memory_value -> nat
+let memory_value_length (mv:memory_value) = List.length mv
 
 
 (* aux fns *)
@@ -549,16 +505,16 @@ let integer_of_bit_list b =
   integerFromBoolList (false,(List.reverse (List.map bit_to_bool b)))
   (* integerFromBoolList takes a list with LSB first, so we reverse it *)
 
-val bit_list_of_integer : int -> integer -> list bit 
+val bit_list_of_integer : nat -> integer -> list bit 
 let bit_list_of_integer len b = 
   List.map (fun b -> if b then Bitc_one else Bitc_zero) 
-    (reverse (boolListFrombitSeq (natFromInt len) (bitSeqFromInteger Nothing b)))
+    (reverse (boolListFrombitSeq len (bitSeqFromInteger Nothing b)))
 
 val integer_of_byte_list : list byte -> integer 
 let integer_of_byte_list bytes = integer_of_bit_list (List.concatMap (fun (Byte bs) -> bs) bytes)
 
-val byte_list_of_integer : int -> integer -> list byte 
-let byte_list_of_integer (len:int) (a:integer):list byte = 
+val byte_list_of_integer : nat -> integer -> list byte 
+let byte_list_of_integer (len:nat) (a:integer):list byte = 
   let bits = bit_list_of_integer (len * 8) a in bytes_of_bits bits
 
 
@@ -620,8 +576,8 @@ let integer_of_memory_value (mv:memory_value):maybe integer =
   | Nothing -> Nothing 
   end
 
-val memory_value_of_integer : int -> integer -> memory_value 
-let memory_value_of_integer (len:int) (i:integer):memory_value =
+val memory_value_of_integer : nat -> integer -> memory_value 
+let memory_value_of_integer (len:nat) (i:integer):memory_value =
   List.map (byte_lifted_of_byte) (byte_list_of_integer len i)
 
 
@@ -633,8 +589,8 @@ let integer_of_register_value (rv:register_value):maybe integer =
   end 
 
   
-val register_value_of_integer : int -> int -> integer -> register_value 
-let register_value_of_integer (len:int) (start:int) (i:integer):register_value =
+val register_value_of_integer : nat -> nat -> integer -> register_value 
+let register_value_of_integer (len:nat) (start:nat) (i:integer):register_value =
   let bs = bit_list_of_integer len i in
   <| 
   rv_bits = List.map bit_lifted_of_bit bs;
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 82c594e5..e4de0d71 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -90,7 +90,7 @@ let rec sparse_walker update ni processed_length length ls df =
   if processed_length = length 
   then []
   else match ls with
-  | [] -> replicate (natFromInteger (length - processed_length)) df
+  | [] -> replicate (length - processed_length) df
   | (i,v)::ls -> 
     if ni = i 
     then v::(sparse_walker update (update ni) (processed_length + 1) length ls df)
@@ -99,10 +99,10 @@ end
 
 let fill_in_sparse v = 
   retaint v (match detaint v with
-    | V_vector_sparse first length inc ls df -> 
-      V_vector first inc 
+    | V_vector_sparse first length dir ls df -> 
+      V_vector first dir
 	(sparse_walker 
-	   (if inc then (fun (x: integer) -> x + onei) else (fun (x: integer) -> x - onei)) first zeroi length ls df)
+	   (if is_inc(dir) then (fun (x: nat) -> x + 1) else (fun (x: nat) -> x - 1)) first 0 length ls df)
     | V_unknown -> V_unknown
     end)
 
@@ -179,14 +179,11 @@ let to_num signed v =
   retaint v   
     (match detaint v with
       | (V_vector idx inc l) ->
-	if has_unknown v 
-	then V_unknown
-	else if l=[]
-	then V_unknown
+	if has_unknown v then V_unknown else if l=[] then V_unknown
 	else 
-      (* Word library in Lem expects bitseq with LSB first *)
+	  (* Word library in Lem expects bitseq with LSB first *)
 	  let l = reverse l in
-      (* Make sure the last bit is a zero to force unsigned numbers *)
+	  (* Make sure the last bit is a zero to force unsigned numbers *)
 	  let l = (match signed with | Signed -> l | Unsigned -> l ++ [V_lit (L_aux L_zero Unknown)] end) in
 	  V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
       | V_unknown -> V_unknown
@@ -197,11 +194,11 @@ let to_vec_inc (V_tuple[v1;v2]) =
     match (v1,v2) with
       | (V_lit(L_aux (L_num len) _), (V_lit(L_aux (L_num n) ln))) ->
 	let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
-	V_vector 0 true (map bool_to_bit (reverse l)) 
+	V_vector 0 IInc (map bool_to_bit (reverse l)) 
       | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
-	V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
+	V_vector 0 IInc (List.replicate (natFromInteger n) V_unknown)
       | ((V_lit(L_aux (L_num n) ln)),(V_lit (L_aux L_undef _))) -> 
-	V_vector 0 true (List.replicate (natFromInteger n) v2)
+	V_vector 0 IInc (List.replicate (natFromInteger n) v2)
       | (_,V_unknown) -> V_unknown
       | (V_unknown,_) -> V_unknown
       | _ -> Assert_extra.failwith ("to_vec_inc parameters were " ^ (string_of_value (V_tuple[v1;v2])))
@@ -212,12 +209,15 @@ let to_vec_dec (V_tuple([v1;v2])) =
   let tv_fun v1 v2 =
     match (v1,v2) with 
       | (V_lit(L_aux (L_num len) _), (V_lit(L_aux (L_num n) ln))) ->
-	let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
-	V_vector (len - 1) false (map bool_to_bit (reverse l)) 
+	let len = natFromInteger len in
+	let l = boolListFrombitSeq len (bitSeqFromInteger Nothing n) in
+	V_vector (len - 1) IDec (map bool_to_bit (reverse l)) 
       | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
-	V_vector (n-1) false (List.replicate (natFromInteger n) V_unknown)
+	let n = natFromInteger n in
+	V_vector (n-1) IDec (List.replicate n V_unknown)
       | ((V_lit(L_aux (L_num n) ln)),(V_lit (L_aux L_undef _))) -> 
-	V_vector (n-1) false (List.replicate (natFromInteger n) v2)
+	let n = natFromInteger n in
+	V_vector (n-1) IDec (List.replicate n v2)
       | (_,V_unknown) -> V_unknown
       | (V_unknown,_) -> V_unknown
       | _ -> Assert_extra.failwith ("to_vec_dec parameters were " ^ (string_of_value (V_tuple[v1;v2])))
@@ -225,23 +225,23 @@ let to_vec_dec (V_tuple([v1;v2])) =
   binary_taint tv_fun v1 v2
 
 let to_vec ord len n =
-  if ord
-  then to_vec_inc (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
-  else to_vec_dec (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
+  if is_inc(ord)
+  then to_vec_inc (V_tuple ([V_lit(L_aux (L_num len) Interp_ast.Unknown); n]))
+  else to_vec_dec (V_tuple ([V_lit(L_aux (L_num len) Interp_ast.Unknown); n]))
 ;;
 
-let exts (V_tuple[v1;v]) = 
+let exts direction (V_tuple[v1;v]) = 
   let exts_help v1 v = match (v1,v) with
-    | (V_lit(L_aux (L_num len) _), V_vector _ inc _)-> to_vec inc (natFromInteger len) (to_num Signed v)
-    | (V_lit(L_aux (L_num len) _), V_unknown) -> to_vec true (natFromInteger len) V_unknown
+    | (V_lit(L_aux (L_num len) _), V_vector _ inc _)-> to_vec inc len (to_num Signed v)
+    | (V_lit(L_aux (L_num len) _), V_unknown) -> to_vec direction len V_unknown
     | (V_unknown,_) -> V_unknown
   end in
   binary_taint exts_help v1 v
 
-let extz (V_tuple[v1;v]) = 
+let extz direction (V_tuple[v1;v]) = 
   let extz_help v1 v = match (v1,v) with
-    | (V_lit(L_aux (L_num len) _), V_vector _ inc _)-> to_vec inc (natFromInteger len) (to_num Unsigned v)
-    | (V_lit(L_aux (L_num len) _), V_unknown) -> to_vec true (natFromInteger len) V_unknown
+    | (V_lit(L_aux (L_num len) _), V_vector _ inc _)-> to_vec inc len (to_num Unsigned v)
+    | (V_lit(L_aux (L_num len) _), V_unknown) -> to_vec direction len V_unknown
     | (V_unknown,_) -> V_unknown
   end in
   binary_taint extz_help v1 v
@@ -282,9 +282,11 @@ let rec arith_op_vec op sign size (V_tuple [vl;vr]) =
       | ((V_vector b ord cs as l1),(V_vector _ _ _ as l2)) ->
 	let (l1',l2') = (to_num sign l1,to_num sign l2) in
 	let n = arith_op op (V_tuple [l1';l2']) in
-	to_vec ord ((List.length cs) * size) n
+	to_vec ord (integerFromNat ((List.length cs) * size)) n
       | (V_unknown,_) -> V_unknown
       | (_,V_unknown) -> V_unknown
+      | _ -> Assert_extra.failwith 
+	("arith_op_vec given (" ^ (string_of_value vl) ^ ", " ^ (string_of_value vr) ^ ")")
   end in
   binary_taint arith_op_help vl vr
 let rec arith_op_vec_vec_range op sign (V_tuple [vl;vr]) = 
@@ -305,14 +307,14 @@ let rec arith_op_overflow_vec op over_typ sign size (V_tuple [vl;vr]) =
 	let act_size = len * size in
 	let (is_l1_unknown,is_l2_unknown) = ((has_unknown vl), (has_unknown vr)) in
 	if is_l1_unknown || is_l2_unknown 
-	then (V_tuple [ (to_vec ord act_size V_unknown);V_unknown;V_unknown])
+	then (V_tuple [ (to_vec ord (integerFromNat act_size) V_unknown);V_unknown;V_unknown])
 	else 
 	  let (l1_sign,l2_sign) = (to_num sign vl,to_num sign vr) in
 	  let (l1_unsign,l2_unsign) = (to_num Unsigned vl,to_num Unsigned vr) in
 	  let n = arith_op op (V_tuple [l1_sign;l2_sign]) in
 	  let n_unsign = arith_op op (V_tuple[l1_unsign;l2_unsign]) in
-	  let correct_size_num = to_vec ord act_size n in
-	  let one_more_size_u = to_vec ord (act_size +1) n_unsign in
+	  let correct_size_num = to_vec ord (integerFromNat act_size) n in
+	  let one_more_size_u = to_vec ord (integerFromNat (act_size +1)) n_unsign in
 	  let overflow = (match n with 
 	    | V_lit (L_aux (L_num n') ln) -> 
 	      if (n' <= (get_max_representable_in sign len)) &&
@@ -336,7 +338,7 @@ let rec arith_op_overflow_vec_bit op sign size (V_tuple [vl;vr]) =
 	let act_size = (List.length cs) * size in
 	let is_v_unknown = has_unknown vl in
 	if is_v_unknown 
-	then V_tuple [(to_vec ord act_size V_unknown);V_unknown;V_unknown]
+	then V_tuple [(to_vec ord (integerFromNat act_size) V_unknown);V_unknown;V_unknown]
 	else
 	  let l1' = to_num sign vl in
 	  let l1_u = to_num Unsigned vl in
@@ -344,8 +346,8 @@ let rec arith_op_overflow_vec_bit op sign size (V_tuple [vl;vr]) =
 	    | L_one -> (arith_op op (V_tuple [l1';(V_lit (L_aux (L_num 1) li))]),
 			arith_op op (V_tuple [l1_u;(V_lit (L_aux (L_num 1) li))]), true)
 	    | L_zero -> (l1',l1_u,false) end in
-	let correct_size_num = to_vec ord act_size n in
-	let one_larger = to_vec ord (act_size +1) nu in
+	let correct_size_num = to_vec ord (integerFromNat act_size) n in
+	let one_larger = to_vec ord (integerFromNat (act_size +1)) nu in
 	let overflow = if changed 
 	  then retaint n (match detaint n with 
 	    | V_lit (L_aux (L_num n') ln) -> 
@@ -365,7 +367,7 @@ let rec arith_op_range_vec op sign size (V_tuple [vl;vr]) =
     | (V_unknown,_) -> V_unknown
     | (_,V_unknown) -> V_unknown
     | (n, V_vector _ ord cs) ->
-      arith_op_vec op sign size (V_tuple [(to_vec ord (List.length cs) n);vr])
+      arith_op_vec op sign size (V_tuple [(to_vec ord (integerFromNat (List.length cs)) n);vr])
   end in
   binary_taint arith_help vl vr
 let rec arith_op_vec_range op sign size (V_tuple [vl;vr]) = 
@@ -373,7 +375,7 @@ let rec arith_op_vec_range op sign size (V_tuple [vl;vr]) =
     | (V_unknown,_) -> V_unknown
     | (_,V_unknown) -> V_unknown
     | (V_vector _ ord cs,n) ->
-      arith_op_vec op sign size (V_tuple [vl;(to_vec ord (List.length cs) n)])
+      arith_op_vec op sign size (V_tuple [vl;(to_vec ord (integerFromNat (List.length cs)) n)])
   end in
   binary_taint arith_help vl vr
 let rec arith_op_range_vec_range op sign (V_tuple [vl;vr]) =
@@ -404,7 +406,7 @@ let rec arith_op_vec_bit op sign size (V_tuple [vl;vr]) =
 				V_lit 
 				  (L_aux (L_num (match bit with | L_one -> 1 | L_zero -> 0 end)) Unknown)])
 	in
-	to_vec ord ((List.length cs) * size) n
+	to_vec ord (integerFromNat ((List.length cs) * size)) n
       end in
    binary_taint arith_help vl vr 
 
@@ -435,7 +437,7 @@ let rec arith_op_vec_no0 op op_s sign size (V_tuple [vl;vr]) =
 	      ((n' <= (get_max_representable_in sign act_size)) && (n' >= (get_min_representable_in sign act_size)))
 	    | _ -> true end in
          if representable 
-	 then to_vec ord act_size n else to_vec ord act_size (V_lit (L_aux L_undef Unknown))
+	 then to_vec ord (integerFromNat act_size) n else to_vec ord (integerFromNat act_size) (V_lit (L_aux L_undef Unknown))
       | (V_unknown,_) -> V_unknown
       | (_,V_unknown) -> V_unknown
    end in
@@ -448,7 +450,7 @@ let rec arith_op_overflow_vec_no0 op op_s sign size (V_tuple [vl;vr]) =
 	let act_size = (List.length cs) * size in
 	let (is_l1_unknown,is_l2_unknown) = ((has_unknown vl), (has_unknown vr)) in
 	if is_l1_unknown || is_l2_unknown
-	then V_tuple [to_vec ord act_size V_unknown;V_unknown;V_unknown]
+	then V_tuple [to_vec ord (integerFromNat act_size) V_unknown;V_unknown;V_unknown]
 	else
 	  let (l1',l2') = ((to_num sign vl),(to_num sign vr)) in
 	  let (l1_u,l2_u) = (to_num Unsigned vl,to_num Unsigned vr) in
@@ -460,9 +462,9 @@ let rec arith_op_overflow_vec_no0 op op_s sign size (V_tuple [vl;vr]) =
 		((n' <= (get_max_representable_in sign rep_size)) && (n' >= (get_min_representable_in sign rep_size)))
 	      | _ -> true end in
           let (correct_size_num,one_more) = 
-	  if representable then (to_vec ord act_size n,to_vec ord (act_size+1) n_u) 
+	  if representable then (to_vec ord (integerFromNat act_size) n,to_vec ord (integerFromNat (act_size+1)) n_u) 
 	  else let udef = V_lit (L_aux L_undef Unknown) in
-	       (to_vec ord act_size udef, to_vec ord (act_size +1) udef) in
+	       (to_vec ord (integerFromNat act_size) udef, to_vec ord (integerFromNat (act_size +1)) udef) in
 	  let overflow = if representable then V_lit (L_aux L_zero Unknown) else V_lit (L_aux L_one Unknown) in
 	  let carry = match one_more with
 	    | V_vector _ _ (b::bits) -> b end in
@@ -478,7 +480,7 @@ let rec arith_op_vec_range_no0 op op_s sign size (V_tuple [vl;vr]) =
       | (V_unknown,_) -> V_unknown
       | (_,V_unknown) -> V_unknown
       | (V_vector _ ord cs,n) ->
-	arith_op_vec_no0 op op_s sign size (V_tuple [vl;(to_vec ord (List.length cs) n)])
+	arith_op_vec_no0 op op_s sign size (V_tuple [vl;(to_vec ord (integerFromNat (List.length cs)) n)])
   end in
   binary_taint arith_help vl vr
 
@@ -486,16 +488,17 @@ let rec shift_op_vec op (V_tuple [vl;vr]) =
   let arith_op_help vl vr =
     match (vl,vr) with
       | (V_vector b ord cs,V_lit (L_aux (L_num n) _)) ->
+	let n = natFromInteger n in
 	(match op with
 	  | "<<" -> 
 	    V_vector b ord 
-	      ((from_n_to_n n (integerFromNat ((length cs) - 1)) cs) ++(List.replicate (natFromInteger n) (V_lit (L_aux L_zero Unknown))))
+	      ((from_n_to_n n ((length cs) - 1) cs) ++(List.replicate n (V_lit (L_aux L_zero Unknown))))
 	  | ">>" ->
 	    V_vector b ord
-	      ((List.replicate (natFromInteger n) (V_lit (L_aux L_zero Unknown))) ++ (from_n_to_n 0 (n-1) cs))
+	      ((List.replicate n (V_lit (L_aux L_zero Unknown))) ++ (from_n_to_n 0 (n-1) cs))
 	  | "<<<" ->
 	    V_vector b ord
-	      ((from_n_to_n n (integerFromNat ((length cs) -1)) cs) ++ (from_n_to_n 0 (n-1) cs)) end)
+	      ((from_n_to_n n ((length cs) -1) cs) ++ (from_n_to_n 0 (n-1) cs)) end)
       | (V_unknown,_) -> V_unknown
       | (_,V_unknown) -> V_unknown
   end in
@@ -531,13 +534,13 @@ let rec compare_op_vec_unsigned op (V_tuple [vl;vr]) =
   end in
   binary_taint comp_help vl vr
 
-let duplicate (V_tuple [vl;vr]) = 
+let duplicate direction (V_tuple [vl;vr]) = 
   let dup_help vl vr =
     match (vl,vr) with
       | ((V_lit _ as v),(V_lit (L_aux (L_num n) _))) ->
-	V_vector 0 true (List.replicate (natFromInteger n) v)
+	V_vector 0 direction (List.replicate (natFromInteger n) v)
       | (V_unknown,(V_lit (L_aux (L_num n) _))) ->
-	V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
+	V_vector 0 direction (List.replicate (natFromInteger n) V_unknown)
       | (V_unknown,_) -> V_unknown
     end in
   binary_taint dup_help vl vr
@@ -560,7 +563,16 @@ let v_length v = retaint v (match detaint v with
   | V_unknown -> V_unknown 
   | _ -> Assert_extra.failwith ("length given unexpected " ^ (string_of_value v)) end)
 
-let function_map = [
+let mask direction (V_tuple [vsize;v]) = retaint v (match (detaint v,detaint vsize) with
+  | (V_vector s d l,V_lit (L_aux (L_num n) _)) ->
+    let n = natFromInteger n in
+    let current_size = List.length l in
+    V_vector (if is_inc(d) then 0 else (n-1)) d (drop (current_size - n) l) 
+  | (V_unknown,V_lit (L_aux (L_num n) _)) -> 
+    V_vector 0 direction (List.replicate (natFromInteger n) V_unknown)
+					  end)
+
+let library_functions direction = [
   ("ignore", ignore_sail);            
   ("length", v_length);
   ("add", arith_op (+));
@@ -621,8 +633,8 @@ let function_map = [
   ("is_one", is_one);
   ("to_num_inc", to_num Unsigned);
   ("to_num_dec", to_num Unsigned);
-  ("EXTS", exts);
-  ("EXTZ", extz);
+  ("EXTS", exts direction);
+  ("EXTZ", extz direction);
   ("to_vec_inc", to_vec_inc);
   ("to_vec_dec", to_vec_dec);
   ("bitwise_not", bitwise_not);
@@ -651,10 +663,11 @@ let function_map = [
   ("gteq_vec_unsigned", compare_op_vec (>=) Unsigned);
   ("ltu", compare_op_vec_unsigned (<));
   ("gtu", compare_op_vec_unsigned (>));
-  ("duplicate", duplicate);
+  ("duplicate", duplicate direction);
+  ("mask", mask direction);
 ] ;;
 
-let eval_external name v = match List.lookup name function_map with
+let eval_external name v = match List.lookup name (library_functions IInc) with
   | Just f -> f v
   | Nothing -> Assert_extra.failwith ("missing library function " ^ name)
   end
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index 1bfa698b..0a23e74c 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -73,6 +73,18 @@ let get_effects (Typ_aux t _) =
     | _ -> []
   end
 
+let string_of_tag tag = match tag with
+  | Tag_empty -> "empty"
+  | Tag_global -> "global"
+  | Tag_ctor -> "ctor"
+  | Tag_extern (Just n) -> "extern " ^ n
+  | Tag_extern _ -> "extern"
+  | Tag_default -> "default"
+  | Tag_spec -> "spec"
+  | Tag_enum -> "enum"
+  | Tag_alias -> "alias"
+end      
+
 val find_type_def : defs tannot -> id -> maybe (type_def tannot)
 val find_function : defs tannot -> id -> maybe (list (funcl tannot))
 
@@ -92,14 +104,14 @@ let rec find_function (Defs defs) id =
 
 
 let rec get_first_index_range (BF_aux i _) = match i with
-  | BF_single i -> i
-  | BF_range i j -> i
+  | BF_single i -> (natFromInteger i)
+  | BF_range i j -> (natFromInteger i)
   | BF_concat s _ -> get_first_index_range s
 end 
 
 let rec get_index_range_size (BF_aux i _) = match i with
   | BF_single _ -> 1
-  | BF_range i j -> (abs (i-j)) + 1
+  | BF_range i j -> (natFromInteger (abs (i-j))) + 1
   | BF_concat i j -> (get_index_range_size i) + (get_index_range_size j)
 end
 
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index a2b63f33..0366bfa9 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -233,9 +233,9 @@ let rec bit_to_hex v =
 let reg_name_to_string = function
   | Reg0(s,_) -> s
   | Reg_slice(s,(first,second)) -> 
-    s ^ "[" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
+    s ^ "[" ^ string_of_int first ^ (if (first = second) then "" else ".." ^ (string_of_int second)) ^ "]"
   | Reg_field(s,f,_) -> s ^ "." ^ f
-  | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f ^ "]" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
+  | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f ^ "]" ^ string_of_int first ^ (if (first = second) then "" else ".." ^ (string_of_int second)) ^ "]"
 
 let dependencies_to_string dependencies = String.concat ", " (List.map reg_name_to_string dependencies)
 
@@ -249,19 +249,19 @@ let rec val_to_string_internal ((Interp.LMem (_,memory)) as mem) = function
      let repr = String.concat "; " (List.map (val_to_string_internal mem) l) in
      sprintf "[||%s||]" repr
  | Interp.V_vector (first_index, inc, l) ->
-     let last_index = add_int_big_int (if inc then List.length l - 1 else 1 - List.length l) first_index  in
+     let last_index = (if (Interp.IInc = inc) then List.length l - 1 else 1 - List.length l) + first_index  in
      let repr =
        try bitvec_to_string l
        with Failure _ ->
          sprintf "[%s]" (String.concat "; " (List.map (val_to_string_internal mem) l)) in
-     sprintf "%s [%s..%s]" repr (string_of_big_int first_index) (string_of_big_int last_index)
+     sprintf "%s [%s..%s]" repr (string_of_int first_index) (string_of_int last_index)
  | (Interp.V_vector_sparse(first_index,last_index,inc,l,default) as v) -> 
    val_to_string_internal mem (Interp_lib.fill_in_sparse v)
  | Interp.V_record(_, l) ->
      let pp (id, value) = sprintf "%s = %s" (id_to_string id) (val_to_string_internal mem value) in
      let repr = String.concat "; " (List.map  pp l) in
      sprintf "{%s}" repr
- | Interp.V_ctor (id,_, value) ->
+ | Interp.V_ctor (id,_,_, value) ->
      sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value)
  | Interp.V_register _ | Interp.V_register_alias _ ->
      sprintf "reg-as-value" 
@@ -336,10 +336,10 @@ let rec format_events = function
   | (E_error s)::events ->
     "     Failed with message : " ^ s ^ " but continued on erroneously\n"
   | (E_read_mem(read_kind, (Address_lifted location), length, tracking))::events ->
-    "     Read_mem at " ^ (memory_value_to_string location) ^ " for " ^ (string_of_big_int length) ^ " bytes \n" ^
+    "     Read_mem at " ^ (memory_value_to_string location) ^ " for " ^ (string_of_int length) ^ " bytes \n" ^
     (format_events events)
   | (E_write_mem(write_kind,(Address_lifted location), length, tracking, value, v_tracking))::events ->
-    "     Write_mem at " ^ (memory_value_to_string location) ^ " writing " ^ (memory_value_to_string value) ^ " across " ^ (string_of_big_int length) ^ " bytes\n" ^
+    "     Write_mem at " ^ (memory_value_to_string location) ^ " writing " ^ (memory_value_to_string value) ^ " across " ^ (string_of_int length) ^ " bytes\n" ^
     (format_events events)
   | ((E_barrier b_kind)::events) ->
     "     Memory_barrier occurred\n" ^ 
@@ -380,11 +380,12 @@ let get_loc (E_aux(_, (l, (_ : tannot)))) = loc_to_string l
 let print_exp printer env e =
   printer ((get_loc e) ^ ": " ^ (Pretty_interp.pp_exp env red e) ^ "\n")
 
-let instruction_state_to_string stack =
+let instruction_state_to_string (IState(stack, _)) =
   let env = () in
   List.fold_right (fun (e,(env,mem)) es -> (exp_to_string env e) ^ "\n" ^ es) (compact_stack stack) ""
 
-let top_instruction_state_to_string stack = let (exp,(env,_)) = top_frame_exp_state stack in exp_to_string env exp
+let top_instruction_state_to_string (IState(stack,_)) = 
+  let (exp,(env,_)) = top_frame_exp_state stack in exp_to_string env exp
 
 let rec option_map f xs = 
   match xs with 
@@ -394,7 +395,7 @@ let rec option_map f xs =
       | None -> option_map f xs 
       | Some x -> x :: (option_map f xs) ) 
 
-let local_variables_to_string stack = 
+let local_variables_to_string (IState(stack,_)) = 
   let (_,(env,mem)) = top_frame_exp_state stack in 
   match env with
     | LEnv(_,env) -> 
@@ -423,6 +424,8 @@ let pad n s = if String.length s < n then s ^ String.make (n-String.length s) '
 let instruction_to_string (name, parms, base_effects) = 
   ((*pad 5*) (String.lowercase name)) ^ " " ^ instr_parms_to_string parms 
 
-let print_backtrace_compact printer stack = List.iter (fun (e,(env,mem)) -> print_exp printer env e) (compact_stack stack)
-let print_continuation printer stack = let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env e
+let print_backtrace_compact printer (IState(stack,_)) =
+  List.iter (fun (e,(env,mem)) -> print_exp printer env e) (compact_stack stack)
+let print_continuation printer (IState(stack,_)) = 
+  let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env e
 let print_instruction printer instr = printer (instruction_to_string instr)
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index 92deef2a..e5b285fa 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -36,7 +36,7 @@ val grey : string -> string
 
 (*Functions to modify the instruction state and expression used in printing and in run_model*)
 val compact_exp : tannot exp -> tannot exp
-val top_frame_exp_state : instruction_state -> (tannot exp * (Interp.lenv*Interp.lmem))
+val top_frame_exp_state : interpreter_state -> (tannot exp * (Interp.lenv*Interp.lmem))
 
 
 (*functions to format events and instruction_states to strings *)
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 44d219e3..afcba19b 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -20,7 +20,7 @@ let rec rewrite_nexp_to_exp program_vars l nexp =
     | Nadd (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "+",l)),rewrite n2),
 			     (l, (tag_annot typ (External (Some "add")))))
     | Nmult (n1,n2) -> E_aux (E_app_infix (rewrite n1,(Id_aux (Id "*",l)),rewrite n2),
-			      (l, tag_annot typ (External (Some "mult"))))
+			      (l, tag_annot typ (External (Some "multiply"))))
     | N2n (n, _) -> E_aux (E_app_infix (E_aux (E_lit (L_aux (L_num 2,l)), (l, simple_annot (mk_atom_typ n_two))),
 					(Id_aux (Id "**",l)),
 					rewrite n), (l, tag_annot typ (External (Some "power"))))
@@ -141,6 +141,7 @@ let rec rewrite_exp (E_aux (exp,(l,annot))) =
     | E_internal_exp_user ((l,user_spec),(_,impl)) -> 
       (match (user_spec,impl) with
 	| (Base((_,tu),_,_,_,_), Base((_,ti),_,_,_,bounds)) ->
+	  (*let _ = Printf.eprintf "E_interal_user getting rewritten two types are %s and %s\n" (t_to_string tu) (t_to_string ti) in*)
 	  match (tu.t,ti.t) with
 	    | (Tapp("implicit", [TA_nexp u]),Tapp("implicit",[TA_nexp i])) ->
 	      let vars = get_all_nvar i in
diff --git a/src/type_check.ml b/src/type_check.ml
index 1636d17f..2cb9b492 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -187,9 +187,9 @@ let into_register d_env (t : tannot) : tannot =
 
 let rec check_pattern envs emp_tag expect_t (P_aux(p,(l,annot))) : ((tannot pat) * (tannot emap) * nexp_range list * bounds_env * t)  =
   let (Env(d_env,t_env,b_env,tp_env)) = envs in
-(*  let _ = Printf.printf "checking pattern with expected type %s\n" (t_to_string expect_t) in*)
+  (*let _ = Printf.printf "checking pattern with expected type %s\n" (t_to_string expect_t) in*)
   let expect_t,cs = get_abbrev d_env expect_t in
-(*  let _ = Printf.printf "check pattern expect_t after abbrev %s\n" (t_to_string expect_t) in*)
+  (*let _ = Printf.printf "check pattern expect_t after abbrev %s\n" (t_to_string expect_t) in*)
   let expect_actual = match expect_t.t with | Tabbrev(_,t) -> t | _ -> expect_t in
   match p with
     | P_lit (L_aux(lit,l')) ->
@@ -578,7 +578,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let (e',u,t_env,cs,bounds,ef) = check_exp envs imp_param ct e in
       let t',cs2,ef',e' = type_coerce (Expr l) d_env true false u e' cast_t in
       let t',cs3,ef'',e'' = type_coerce (Expr l) d_env false false cast_t e' expect_t in 
-      (e'',t',t_env,cs_a@cs@cs3,bounds,union_effects ef' (union_effects ef'' ef))
+      (e'',t',t_env,cs_a@cs@cs2@cs3,bounds,union_effects ef' (union_effects ef'' ef))
     | E_app(id,parms) -> 
       let i = id_to_string id in
       let check_parms p_typ parms = (match parms with
@@ -603,7 +603,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let check_result ret imp tag cs ef parms =    
 	match (imp,imp_param) with
 	  | (IP_length n ,None) | (IP_user n,None) | (IP_start n,None) ->
-	    (*let _ = Printf.printf "implicit length or var required, no imp_param\n!" in*)
+	    (*let _ = Printf.eprintf "implicit length or var required, no imp_param %s\n!" (n_to_string n) in*)
 	    let internal_exp = 
 	      let implicit = {t= Tapp("implicit",[TA_nexp n])} in
 	      let annot_i = Base(([],implicit),Emp_local,[],pure_e,b_env) in
@@ -611,7 +611,8 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
             type_coerce (Expr l) 
 	      d_env false false ret (E_aux (E_app(id, internal_exp::parms),(l,(Base(([],ret),tag,cs,ef,nob))))) expect_t
 	  | (IP_length n ,Some ne) | (IP_user n,Some ne) | (IP_start n,Some ne) ->
-	    (*let _ = Printf.printf "implicit length or var required with imp_param\n" in*)
+	    (*let _ = Printf.eprintf "implicit length or var required %s with imp_param %s\n" (n_to_string n) (n_to_string ne) in
+	    let _ = Printf.eprintf "and expected type is %s and return type is %s\n" (t_to_string expect_t) (t_to_string ret) in*)
 	    let internal_exp = 
 	      let implicit_user = {t = Tapp("implicit",[TA_nexp ne])} in
 	      let implicit = {t= Tapp("implicit",[TA_nexp n])} in
@@ -635,11 +636,11 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
         let t,cs,ef,_ = subst params t cs ef in
         (match t.t with
         | Tfn(arg,ret,imp,ef') ->
-	  (*let _ = Printf.printf "Checking funcation call of %s\n" i in*)
+	  (*let _ = Printf.eprintf "Checking funcation call of %s\n" i in*)
           let parms,arg_t,cs_p,ef_p = check_parms arg parms in
 	  (*let _ = Printf.printf "Checked parms of %s\n" i in*)
           let (ret_t,cs_r,ef_r,e') = check_result ret imp tag cs ef' parms in
-	  (*let _ = Printf.printf "Checked result of %s\n" i in*)
+	  (*let _ = Printf.eprintf "Checked result of %s and constraints are %s\n" i (constraints_to_string cs_r) in*)
           (e',ret_t,t_env,cs@cs_p@cs_r, bounds,union_effects ef' (union_effects ef_p ef_r))
         | _ -> typ_error l ("Expected a function or constructor, found identifier " ^ i ^ " bound to type " ^ (t_to_string t)))
       | Some(Overload(Base((params,t),tag,cs,ef,_),overload_return,variants)) ->
@@ -1241,6 +1242,7 @@ let rec check_exp envs (imp_param:nexp option) (expect_t:t) (E_aux(e,(l,annot)):
       let (lexp',t',t_env',tag,cs,b_env',ef) = check_lexp envs imp_param true lexp in
       let (exp',t'',_,cs',_,ef') = check_exp envs imp_param t' exp in
       let (t',c') = type_consistent (Expr l) d_env false unit_t expect_t in
+      (*let _ = Printf.eprintf "Constraints for E_assign %s\n" (constraints_to_string (cs@cs'@c')) in*)
       (E_aux(E_assign(lexp',exp'),(l,(Base(([],unit_t),tag,[],ef,nob)))),unit_t,t_env',cs@cs'@c',b_env',union_effects ef ef')
     | E_exit e ->
       let (e',t',_,_,_,_) = check_exp envs imp_param (new_t ()) e in
@@ -1709,16 +1711,16 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
   let check t_env tp_env imp_param =
     List.split
       (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) ->
-	(*let _ = Printf.printf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
+	(*let _ = Printf.eprintf "checking function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
 	let (pat',t_env',cs_p,b_env',t') = check_pattern (Env(d_env,t_env,b_env,tp_env)) Emp_local param_t pat in
 	(*let _ = Printf.printf "cs_p for %s %s\n" (id_to_string id) (constraints_to_string cs_p) in*)
-(*	let _ = Printf.printf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*)
+        (*let _ = Printf.printf "about to see if %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*)
 	let t', _ = type_consistent (Patt l) d_env false param_t t' in
 	let exp',_,_,cs_e,_,ef = 
 	  check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env true) t_env t_env', 
 			 merge_bounds b_env b_env',tp_env)) imp_param ret_t exp in
-(*	let _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*)
-	(*let _ = Printf.eprintf "effects were %s\n" (e_to_string ef) in*)
+	(*let _ = Printf.eprintf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in
+	let _ = Printf.eprintf "constraints were %s\n" (constraints_to_string (cs_p@cs_e)) in*)
 	let cs = [CondCons(Fun l,cs_p,cs_e)] in
 	(FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,cs,ef,nob)))),(cs,ef))) funcls) in
   let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) = 
@@ -1730,10 +1732,10 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
   in
   match (in_env,tannot) with
     | Some(Base( (params,u),Spec,constraints,eft,_)), Base( (p',t),_,c',eft',_) ->
-(*      let _ = Printf.printf "Function %s is in env\n" id in*)
+      (*let _ = Printf.eprintf "Function %s is in env\n" id in*)
       let u,constraints,eft,t_param_env = subst params u constraints eft in
       let _,cs_decs = type_consistent (Specc l) d_env false t u in
-(*      let _ = Printf.printf "valspec consistent with declared type for %s, %s ~< %s with %i constraints \n" id (t_to_string t) (t_to_string u) (List.length cs_decs) in*)
+      (*let _ = Printf.eprintf "valspec consistent with declared type for %s, %s ~< %s with %i constraints \n" id (t_to_string t) (t_to_string u) (List.length cs_decs) in*)
       let imp_param = match u.t with 
 	| Tfn(_,_,IP_user n,_) -> Some n
 	| _ -> None in
@@ -1742,12 +1744,14 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       let cs,ef = ((fun (cses,efses) -> 
 	(List.concat cses),(List.fold_right union_effects efses pure_e)) (List.split cs_ef)) in
       let cs' = resolve_constraints (cs@cs_decs@constraints) in
-(*     let _ = Printf.printf "checking tannot for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*)
+      (*let _ = Printf.eprintf "remaining constraints are: %s\n" (constraints_to_string cs') in
+     let _ = Printf.eprintf "checking tannot for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*)
       let tannot = check_tannot l tannot imp_param cs' ef in
-(*     let _ = Printf.printf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*)
+     (*let _ = Printf.printf "check_tannot ok for %s val type %s derived type %s \n" id (t_to_string u) (t_to_string t) in*)
       let funcls = match imp_param with
-	| None | Some {nexp = Nconst _} -> funcls
-	| Some {nexp = Nvar i} -> List.map (update_pattern i) funcls in
+	| Some {nexp = Nvar i} -> List.map (update_pattern i) funcls 
+	| _ -> funcls
+      in
       (*let _ = Printf.printf "done funcheck case 1\n" in*)
       (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
       Env(d_env,Envmap.insert t_env (id,tannot),b_env,tp_env)
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 3b7392b6..bb17397c 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -181,7 +181,7 @@ and n_to_string n =
     | N2n(n,Some i) -> "2**" ^ (n_to_string n) ^ "(*" ^ (string_of_big_int i) ^ "*)"
     | Npow(n, i) -> "(" ^ (n_to_string n) ^ ")**" ^ (string_of_int i)
     | Nneg n -> "-" ^ (n_to_string n)
-    | Nuvar({nindex=i;nsubst=a}) -> if !debug_mode then "Nu_" ^ string_of_int i ^ "()" else "_"
+    | Nuvar({nindex=i;nsubst=a}) -> if !debug_mode then "Nu_" ^ string_of_int i ^ "(" ^ (match a with | None -> "None" | Some n -> n_to_string n) ^ ")" else "_"
 and ef_to_string (Ast.BE_aux(b,l)) =
     match b with
       | Ast.BE_rreg  -> "rreg"
@@ -716,19 +716,45 @@ let equate_t (t_box : t) (t : t) : unit =
        | _ -> assert false)
      | _ ->
        t_box.t <- t.t)
+
+let rec occurs_in_pending_subst n_box n : bool =
+  if n_box.nexp == n.nexp then true 
+  else match n_box.nexp with
+    | Nuvar( { nsubst= Some(n') }) -> 
+      if n'.nexp == n.nexp 
+      then true
+      else occurs_in_pending_subst n' n
+    | Nuvar( { nsubst = None } ) -> false
+    | _ -> false
+
+let rec occurs_in_nexp n_box nuvar : bool =
+  if n_box.nexp == nuvar.nexp then true
+  else match n_box.nexp with
+    | Nuvar _ -> occurs_in_pending_subst n_box nuvar
+    | Nadd (nb1,nb2) | Nmult (nb1,nb2) -> occurs_in_nexp nb1 nuvar || occurs_in_nexp nb2 nuvar
+    | Nneg nb | N2n(nb,None) | Npow(nb,_) -> occurs_in_nexp nb nuvar
+    | _ -> false
+
 let equate_n (n_box : nexp) (n : nexp) : unit =
-  let n = resolve_nsubst n in
-  if n_box == n then ()
-  else
-    (occurs_check_n n_box n;
-     match n.nexp with
-     | Nuvar(_) ->
-       (match n_box.nexp with
-       | Nuvar(u) ->
-         u.nsubst <- Some(n)
-       | _ -> assert false)
-     | _ ->
-       n_box.nexp <- n.nexp)
+  (* let _ = Printf.eprintf "equate_n given n_box %s and n %s\n" (n_to_string n_box) (n_to_string n) in*)
+  if n_box.nexp == n.nexp then ()
+  else 
+    let n = resolve_nsubst n in
+    if occurs_in_pending_subst n_box n || occurs_in_pending_subst n n_box then ()
+    else 
+      (* let _ = Printf.eprintf "equate_n has does not occur in %s and %s\n" (n_to_string n_box) (n_to_string n)) in *)
+      match n.nexp with
+	| Nuvar(_) ->
+	  (match n_box.nexp with
+	    | Nuvar(u) ->
+	      let rec set_bottom_nsubst u =
+		match u.nsubst with	       
+		  | None -> u.nsubst <- Some(n);
+		  | Some(({nexp = Nuvar(u)} as n1)) -> set_bottom_nsubst u in
+	      set_bottom_nsubst u; 
+	    | _ -> assert false)
+	| _ ->
+	  n_box.nexp <- n.nexp
 let equate_o (o_box : order) (o : order) : unit =
   let o = resolve_osubst o in
   if o_box == o then ()
@@ -775,12 +801,13 @@ let rec fresh_tvar bindings t =
     None
   | _ -> None
 let rec fresh_nvar bindings n =
+  (*let _ = Printf.printf "fresh_nvar for %s\n" (n_to_string n) in*)
   match n.nexp with
     | Nuvar { nindex = i;nsubst = None } -> 
-      fresh_var i (fun v -> equate_n n {nexp = (Nvar v)}; Some(v,{k=K_Nat})) bindings
+      fresh_var i (fun v -> n.nexp <- (Nvar v); Some(v,{k=K_Nat})) bindings
     | Nuvar { nindex = i; nsubst = Some({nexp=Nuvar _} as n')} ->
       let kv = fresh_nvar bindings n' in
-      equate_n n n';
+      n.nexp <- n'.nexp;
       kv
     | Nuvar { nindex = i; nsubst = Some n' } ->
       n.nexp <- n'.nexp;
@@ -1599,14 +1626,16 @@ and ta_remove_unifications s_env ta =
   | TA_eft e -> (e_remove_unifications s_env e)
   | TA_ord o -> (o_remove_unifications s_env o)
 and n_remove_unifications s_env n =
+  (*let _ = Printf.eprintf "n_remove_unifications %s\n" (n_to_string n) in*)
   match n.nexp with
   | Nvar _ | Nconst _ | Npos_inf | Nneg_inf -> s_env
   | Nuvar nu -> 
     let n' = match nu.nsubst with
       | None -> n
       | _ -> resolve_nsubst n; n in
-    (match n.nexp with
+    (match n'.nexp with
       | Nuvar _ -> 
+	(*let _ = Printf.eprintf "nuvar is before turning into var %s\n" (n_to_string n') in*)
 	(match fresh_nvar s_env n with
 	  | Some ks -> Envmap.insert s_env ks
 	  | None -> s_env)
@@ -1995,18 +2024,25 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 =
   let t2_actual = match t2.t with | Tabbrev(_,t2) -> t2 | _ -> t2 in
   let cs1,cs2 = cs1@cs1',cs2@cs2' in
   let csp = cs1@cs2 in
+  (*let _ = Printf.eprintf "called type_coerce_internal is_explicit %b, turning %s into %s\n" is_explicit (t_to_string t1) (t_to_string t2) in*)
   match t1_actual.t,t2_actual.t with
   | Toptions(to1,Some to2),_ -> 
     if (conforms_to_t d_env false true to1 t2_actual || conforms_to_t d_env false true to2 t2_actual)
     then begin t1_actual.t <- t2_actual.t; (t2,csp,pure_e,e) end
     else eq_error l ("Neither " ^ (t_to_string to1) ^
 		     " nor " ^ (t_to_string to2) ^ " can match expected type " ^ (t_to_string t2))
-  | Toptions(to1,None),_ -> (t2,csp,pure_e,e)
+  | Toptions(to1,None),_ -> 
+    if is_explicit 
+    then type_coerce_internal co d_env is_explicit widen to1 cs1 e t2 cs2
+    else (t2,csp,pure_e,e)
   | _,Toptions(to1,Some to2) -> 
     if (conforms_to_t d_env false true to1 t1_actual || conforms_to_t d_env false true to2 t1_actual)
     then begin t2_actual.t <- t1_actual.t; (t1,csp,pure_e,e) end
     else eq_error l ((t_to_string t1) ^ " can match neither expexted type " ^ (t_to_string to1) ^ " nor " ^ (t_to_string to2))
-  | _,Toptions(to1,None) -> (t1,csp,pure_e,e)
+  | _,Toptions(to1,None) -> 
+    if is_explicit
+    then type_coerce_internal co d_env is_explicit widen t1_actual cs1 e to1 cs2
+    else (t1,csp,pure_e,e)
   | Ttup t1s, Ttup t2s ->
     let tl1,tl2 = List.length t1s,List.length t2s in
     if tl1=tl2 then 
@@ -2053,7 +2089,7 @@ let rec type_coerce_internal co d_env is_explicit widen t1 cs1 e t2 cs2 =
         let cs = csp@[Eq(co,r1,r2)] in
         let t',cs' = type_consistent co d_env widen t1i t2i in
         let tannot = Base(([],t2),Emp_local,cs@cs',pure_e,nob) in
-	(*let _ = Printf.printf "looking at vector vector coerce, t1 %s, t2 %s\n" (t_to_string t1) (t_to_string t2) in*)
+	(*let _ = Printf.eprintf "looking at vector vector coerce, t1 %s, t2 %s\n" (t_to_string t1) (t_to_string t2) in*)
         let e' = E_aux(E_internal_cast ((l,(Base(([],t2),Emp_local,[],pure_e,nob))),e),(l,tannot)) in
         (t2,cs@cs',pure_e,e')
       | _ -> raise (Reporting_basic.err_unreachable l "vector is not properly kinded"))
@@ -2292,14 +2328,30 @@ let freshen n =
 
 let rec simple_constraint_check in_env cs = 
   let check = simple_constraint_check in_env in
-  (*let _ = Printf.printf "simple_constraint_check\n" in *)
+  (*let _ = Printf.eprintf "simple_constraint_check of %s\n" (constraints_to_string cs) in *)
   match cs with 
   | [] -> []
   | Eq(co,n1,n2)::cs -> 
+    let eq_to_zero ok_to_set n1 n2 = 	
+      let new_n = normalize_nexp (mk_sub n1 n2) in
+      (match new_n.nexp with
+	| Nconst i -> 
+	  if eq_big_int i zero
+	  then None
+	  else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires "
+					^ n_to_string new_n ^ " to equal 0, not " ^ string_of_big_int i)
+	| Nuvar u1 ->
+	  if ok_to_set
+	  then begin ignore(resolve_nsubst new_n); equate_n new_n n_zero; None end
+	  else Some(Eq(co,new_n,n_zero))
+	| Nadd(new_n1,new_n2) ->
+	  (match new_n1.nexp, new_n2.nexp with
+	    | _ -> Some(Eq(co,n1,n2)))
+	| _ -> Some(Eq(co,n1,n2))) in
     let check_eq ok_to_set n1 n2 = 
-      (*let _ = Printf.printf "eq check, about to normalize_nexp of %s, %s arising from %s \n" (n_to_string n1) (n_to_string n2) (co_to_string co) in *)
+      (*let _ = Printf.eprintf "eq check, about to normalize_nexp of %s, %s arising from %s \n" (n_to_string n1) (n_to_string n2) (co_to_string co) in *)
       let n1',n2' = normalize_nexp n1,normalize_nexp n2 in
-      (*let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *)
+      (*let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *)
       (match n1'.nexp,n2'.nexp with
       | Ninexact,nok | nok,Ninexact -> 
 	eq_error (get_c_loc co) ("Type constraint arising from here requires " ^ n_to_string {nexp = nok} ^ " to be equal to +inf + -inf")
@@ -2307,38 +2359,30 @@ let rec simple_constraint_check in_env cs =
       | Nconst i1, Nconst i2 | Nconst i1,N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst(i2) -> 
         if eq_big_int i1 i2 then None
         else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires " ^ n_to_string n1 ^ " to equal " ^ n_to_string n2 )
-      | Nconst i, Nuvar u ->
-        if not(u.nin) && ok_to_set 
-        then begin equate_n n2' n1'; None end
-        else Some (Eq(co,n1',n2')) 
-      | Nuvar u, Nconst i ->
-        if not(u.nin) && ok_to_set
-        then begin equate_n n1' n2'; None end
-        else Some (Eq(co,n1',n2'))
       | Nuvar u1, Nuvar u2 ->
-	(*let _ = Printf.printf "setting two nuvars, %s and %s, it is ok_to_set %b\n" (n_to_string n1) (n_to_string n2) ok_to_set in*)
+	(*let _ = Printf.eprintf "setting two nuvars, %s and %s, it is ok_to_set %b\n" (n_to_string n1) (n_to_string n2) ok_to_set in*)
         if ok_to_set
-        then begin ignore(resolve_nsubst n1); ignore(resolve_nsubst n2); equate_n n1' n2'; None end
+        then begin equate_n n1' n2'; None end
         else Some(Eq(co,n1',n2'))
+      | _, Nuvar u ->
+	let occurs = occurs_in_nexp n1' n2' in
+        if not(u.nin) && ok_to_set && not(occurs)
+        then begin equate_n n2' n1'; None end
+        else if occurs 
+	then eq_to_zero ok_to_set n1' n2'
+	else Some (Eq(co,n1',n2')) 
+      | Nuvar u, _ ->
+	let occurs = occurs_in_nexp n2' n1' in
+        if not(u.nin) && ok_to_set && not(occurs)
+        then begin equate_n n1' n2'; None end
+        else if occurs
+	then eq_to_zero ok_to_set n1' n2'
+	else Some (Eq(co,n1',n2'))
       | _,_ -> 
 	if nexp_eq_check n1' n2'
 	then None
-	else
-	let new_n = normalize_nexp (mk_sub n1' n2') in
-	(match new_n.nexp with
-	  | Nconst i -> 
-	    if eq_big_int i zero
-	    then None
-	    else eq_error (get_c_loc co) ("Type constraint mismatch: constraint arising from here requires "
-					     ^ n_to_string new_n ^ " to equal 0, not " ^ string_of_big_int i)
-	  | Nuvar u1 ->
-	    if ok_to_set
-	    then begin ignore(resolve_nsubst new_n); equate_n new_n n_zero; None end
-	    else Some(Eq(co,new_n,n_zero))
-	  | Nadd(new_n1,new_n2) ->
-	    (match new_n1.nexp, new_n2.nexp with
-	      | _ -> Some(Eq(co,n1',n2')))
-	  | _ -> Some(Eq(co,n1',n2')))) in
+	else eq_to_zero ok_to_set n1' n2')
+    in
     (match contains_in_vars in_env n1, contains_in_vars in_env n2 with
       | _,_ ->	
 	(match check_eq true n1 n2 with
@@ -2346,7 +2390,7 @@ let rec simple_constraint_check in_env cs =
 	  | Some(c) -> c::(check cs))
       | _ -> (Eq(co,n1,n2)::(check cs)))
   | GtEq(co,n1,n2)::cs -> 
-    (*let _ = Printf.printf ">= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
+    (*let _ = Printf.eprintf ">= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
     let n1',n2' = normalize_nexp n1,normalize_nexp n2 in
     (*let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in*)
     (match n1'.nexp,n2'.nexp with
@@ -2369,9 +2413,9 @@ let rec simple_constraint_check in_env cs =
 					     ^ n_to_string new_n ^ " to be greater than or equal to 0, not " ^ string_of_big_int i)
 	  | _ -> GtEq(co,n1',n2')::(check cs)))
   | LtEq(co,n1,n2)::cs -> 
-    (*let _ = Printf.printf "<= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
+    (*let _ = Printf.eprintf "<= check, about to normalize_nexp of %s, %s\n" (n_to_string n1) (n_to_string n2) in *)
     let n1',n2' = normalize_nexp n1,normalize_nexp n2 in
-    (*let _ = Printf.printf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *)
+    (*let _ = Printf.eprintf "finished evaled to %s, %s\n" (n_to_string n1') (n_to_string n2') in *)
     (match n1'.nexp,n2'.nexp with
     | Nconst i1, Nconst i2 | Nconst i1, N2n(_,Some(i2)) | N2n(_,Some(i1)),Nconst i2 -> 
       if le_big_int i1 i2 
@@ -2383,15 +2427,15 @@ let rec simple_constraint_check in_env cs =
                                                         ^ (n_to_string n2'))
     | _,_ -> LtEq(co,n1',n2')::(check cs))
   | CondCons(co,pats,exps):: cs ->
-    (*let _ = Printf.printf "Condcons check length pats %i, length exps %i\n" (List.length pats) (List.length exps) in*)
+    (*let _ = Printf.eprintf "Condcons check length pats %i, length exps %i\n" (List.length pats) (List.length exps) in*)
     let pats' = check pats in
     let exps' = check exps in
-    (*let _ = Printf.printf "Condcons after check length pats' %i, length exps' %i\n" (List.length pats') (List.length exps') in*)
+    (*let _ = Printf.eprintf "Condcons after check length pats' %i, length exps' %i\n" (List.length pats') (List.length exps') in*)
     (match pats',exps' with
       | [],[] -> check cs
       | _     -> CondCons(co,pats',exps')::(check cs))
   | BranchCons(co,branches)::cs ->
-    (*let _ = Printf.printf "Branchcons check length branches %i\n" (List.length branches) in*)
+    (*let _ = Printf.eprintf "Branchcons check length branches %i\n" (List.length branches) in*)
     let b' = check branches in
     if [] = b' 
     then check cs
@@ -2411,17 +2455,18 @@ let rec constraint_size = function
 let do_resolve_constraints = ref true
 
 let resolve_constraints cs = 
-  (*let _ = Printf.printf "called resolve constraints with %i constraints\n" (constraint_size cs) in*)
+  (*let _ = Printf.eprintf "called resolve constraints with %i constraints\n" (constraint_size cs) in*)
   if not !do_resolve_constraints
   then cs
   else
     let rec fix len cs =
-      (*let _ = Printf.printf "Calling simple constraint check, fix check point is %i\n" len in *)
+      (*let _ = Printf.eprintf "Calling simple constraint check, fix check point is %i\n" len in *)
       let cs' = simple_constraint_check (in_constraint_env cs) cs in
       let len' = constraint_size cs' in
       if len > len' then fix len' cs'
       else cs' in
     let complex_constraints = fix (constraint_size cs) cs in
+    (*let _ = Printf.eprintf "Resolved as many constraints as possible, leaving %i\n" (constraint_size complex_constraints) in*)
     complex_constraints