Merge remote-tracking branch 'origin/master' into sail_new_tc

1 files changed, 606 insertions, 390 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 9c88eec7..58874fa6 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -45,6 +45,7 @@ import Map
 import Map_extra (* For 'find' instead of using lookup and maybe types, as we know it cannot fail *)
 import Set_extra (* For 'to_list' because map only goes to set *)
 import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
+open import Show
 open import Show_extra (* for 'show' to convert nat to string) *)
 open import String_extra (* for chr *)
 import Assert_extra (*For failwith when partiality is known to be unreachable*)
@@ -54,7 +55,14 @@ open import Interp_ast
 open import Interp_utilities
 open import Instruction_extractor
 
-type tannot = Interp_utilities.tannot
+(* TODO: upstream into Lem *)
+val stringFromTriple : forall 'a 'b 'c. ('a -> string) -> ('b -> string) -> ('c -> string) -> ('a * 'b * 'c) -> string
+let stringFromTriple showX showY showZ (x,y,z) =
+  "(" ^ showX x ^ ", " ^ showY y ^ ", " ^ showZ z ^ ")"
+
+instance forall 'a 'b 'c. Show 'a, Show 'b, Show 'c => (Show ('a * 'b * 'c))
+  let show = stringFromTriple show show show
+end
 
 val debug_print : string -> unit
 declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s
@@ -78,36 +86,14 @@ let non_det_annot annot maybe_id = match annot with
   | _ -> Nothing
 end
 
-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 * i_direction
- | SubReg of id * reg_form * index_range
-
-type ctor_kind = C_Enum of nat | 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: 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 * 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 * (set reg_form) (* Used when memory system wants to track what register(s) a value came from *)
 
 let rec {ocaml} string_of_reg_form r = match r with
-  | Reg id _ _ -> get_id id
-  | SubReg id reg_form _ -> (string_of_reg_form reg_form) ^ "." ^ (get_id id)
+  | Form_Reg id _ _ -> get_id id
+  | Form_SubReg id reg_form _ -> (string_of_reg_form reg_form) ^ "." ^ (get_id id)
 end
 
 let rec {ocaml} string_of_value v = match v with
@@ -196,18 +182,21 @@ let rec debug_print_value v = match v with
   | V_record t vals ->
      let ppidval (id,v) = "(" ^ (get_id id) ^ "," ^ debug_print_value v ^ ")" in
      "V_record t [" ^ debug_print_value_list (List.map ppidval vals) ^ "]"
-  | V_ctor id t k vals ->
+  | V_ctor id t k v' ->
      "V_ctor " ^ (get_id id) ^ " t " ^
        (match k with | C_Enum n -> "(C_Enum " ^ show n ^ ")"
                      | C_Union -> "C_Union" end) ^
-         "(" ^ debug_print_value v ^ ")"
+         "(" ^ debug_print_value v' ^ ")"
   | V_unknown -> "V_unknown"
   | V_register r -> "V_register (" ^ string_of_reg_form r ^ ")"
   | V_register_alias _ _ -> "V_register_alias _ _"
   | V_track v rs -> "V_track (" ^ debug_print_value v ^ ") _"
   end
-                                   
-                                   
+
+instance (Show value)
+  let show v = debug_print_value v
+end
+
 let rec {coq;ocaml} id_value_eq strict (i, v) (i', v') = i = i' && value_eq strict v v'
 and value_eq strict left right =
   match (left, right) with
@@ -249,7 +238,7 @@ end
 
 let reg_start_pos reg = 
   match reg with
-    | Reg _ (Just(typ,_,_,_,_)) _ -> 
+    | Form_Reg _ (Just(typ,_,_,_,_)) _ -> 
       let start_from_vec targs = match targs with
         | T_args [T_arg_nexp (Ne_const s);_;_;_] -> natFromInteger s
         | T_args [T_arg_nexp _; T_arg_nexp (Ne_const s); T_arg_order Odec; _] -> (natFromInteger s) - 1
@@ -277,7 +266,7 @@ end
 
 let reg_size reg = 
   match reg with
-    | Reg _ (Just(typ,_,_,_,_)) _ -> 
+    | Form_Reg _ (Just(typ,_,_,_,_)) _ -> 
       let end_from_vec targs = match targs with
         | T_args [_;T_arg_nexp (Ne_const s);_;_] -> natFromInteger s
         | _ -> Assert_extra.failwith "register vector type not well formed"
@@ -326,12 +315,20 @@ end
 let env_to_string (LEnv c env) =
   "(LEnv " ^ show c ^ " [" ^
   (list_to_string ", " (fun (k,v) -> k ^ " -> " ^ (string_of_value v)) (Map_extra.toList env)) ^
-  "])"
+    "])"
+
+instance (Show lenv)
+  let show env = env_to_string env
+end
 
 let mem_to_string (LMem f c mem _) =
   "(LMem " ^ f ^ " " ^ show c ^
   " [" ^ (list_to_string ", " (fun (k,v) -> show k ^ " -> " ^ (string_of_value v)) (Map_extra.toList mem)) ^ "])"
 
+instance (Show lmem)
+  let show mem = mem_to_string mem
+end
+
 type sub_reg_map = map string index_range
 
 (*top_level is a tuple of 
@@ -351,6 +348,7 @@ type top_level =
         * map string typ (*typedef union constructors *)
         * map string sub_reg_map (*sub register mappings*)
         * map string (alias_spec tannot) (*register aliases*)
+        * bool (* debug? *)
 
 type action = 
  | Read_reg of reg_form * maybe (nat * nat)
@@ -387,10 +385,246 @@ type outcome =
  | Action of action * stack
  | Error of l * string 
 
-type interp_mode = <| eager_eval : bool; track_values : bool; track_lmem : bool|>
+let string_of_id id' =
+  (match id' with
+   | Id_aux id _ ->
+      (match id with
+       | Id s -> s
+       | DeIid s -> s
+       end)
+   end)
+
+instance (Show id)
+  let show = string_of_id
+end
+
+let string_of_kid kid' =
+  (match kid' with
+   | Kid_aux kid _ ->
+     (match kid with
+      | Var s -> s
+      end)
+   end)
+
+instance (Show kid)
+  let show = string_of_kid
+end
+
+let string_of_reg_id (RI_aux (RI_id id ) _) = string_of_id id
+
+instance forall 'a. (Show reg_id 'a)
+  let show = string_of_reg_id
+end
+
+let rec string_of_typ typ' =
+  (match typ' with
+   | Typ_aux typ _ ->
+      (match typ with
+       | Typ_wild -> "(Typ_wild)"
+       | Typ_id id -> "(Typ_id " ^ (string_of_id id) ^ ")"
+       | Typ_var kid -> "(Typ_var " ^ (string_of_kid kid) ^ ")"
+       | Typ_fn typ1 typ2 eff -> "(Typ_fn _ _ _)"
+       | Typ_tup typs -> "(Typ_tup [" ^ String.concat "; " (List.map string_of_typ typs) ^ "])"
+       | Typ_app id args -> "(Typ_app " ^ string_of_id id ^ " _)"
+       end)
+   end)
+
+instance (Show typ)
+  let show = string_of_typ
+end
+
+let rec string_of_lexp l' =
+  (match l' with
+   | LEXP_aux l _ ->
+      (match l with
+       | LEXP_id id -> "(LEXP_id " ^ string_of_id id ^ ")"
+       | LEXP_memory id exps -> "(LEXP_memory " ^ string_of_id id ^ " _)"
+       | LEXP_cast typ id -> "(LEXP_cast " ^ string_of_typ typ ^ " " ^ string_of_id id ^ ")"
+       | LEXP_tup lexps -> "(LEXP_tup [" ^ String.concat "; " (List.map string_of_lexp lexps) ^ "])"
+       | LEXP_vector lexps exps -> "(LEXP_vector _ _)"
+       | LEXP_vector_range lexp exp1 exp2 -> "(LEXP_vector_range _ _ _)"
+       | LEXP_field lexp id -> "(LEXP_field " ^ string_of_lexp lexp ^ "." ^ string_of_id id ^ ")"
+       end)
+   end)
+
+instance forall 'a. (Show lexp 'a)
+  let show = string_of_lexp
+end
+
+let string_of_lit l' =
+  (match l' with
+   | L_aux l _ ->
+      (match l with
+       | L_unit -> "()"
+       | L_zero -> "0"
+       | L_one -> "1"
+       | L_true -> "true"
+       | L_false -> "false"
+       | L_num n -> "0d" ^ (show n)
+       | L_hex s -> "0x" ^ s
+       | L_bin s -> "0b" ^ s
+       | L_undef -> "undef"
+       | L_string s -> "\"" ^ s ^ "\""
+       end)
+   end)
+
+instance (Show lit)
+  let show = string_of_lit
+end
+
+let string_of_order o' =
+  (match o' with
+   | Ord_aux o _ ->
+      (match o with
+       | Ord_var kid -> string_of_kid kid
+       | Ord_inc -> "inc"
+       | Ord_dec -> "dec"
+       end)
+   end)
+
+instance (Show order)
+  let show = string_of_order
+end
+
+let rec string_of_exp e' =
+  (match e' with
+   | E_aux e _ ->
+      (match e with
+       | E_block exps -> "(E_block [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_nondet exps -> "(E_nondet [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_id id -> "(E_id \"" ^ string_of_id id ^ "\")"
+       | E_lit lit -> "(E_lit " ^ string_of_lit lit ^ ")"
+       | E_cast typ exp -> "(E_cast " ^ string_of_typ typ ^ " " ^ string_of_exp exp ^ ")"
+       | E_app id exps -> "(E_app " ^ string_of_id id ^ " [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_app_infix exp1 id exp2 -> "(E_app_infix " ^ string_of_exp exp1 ^ " " ^ string_of_id id ^ " " ^ string_of_exp exp2 ^ ")"
+       | E_tuple exps -> "(E_tuple [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_if cond thn els -> "(E_if " ^ (string_of_exp cond) ^ " ? " ^ (string_of_exp thn) ^ " : " ^ (string_of_exp els) ^ ")"
+       | E_for id from to_ by order exp -> "(E_for " ^ string_of_id id ^ " " ^ string_of_exp from ^ " " ^ string_of_exp to_ ^ " " ^ string_of_exp by ^ " " ^ string_of_order order ^ " " ^ string_of_exp exp ^ ")"
+       | E_vector exps -> "(E_vector [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_vector_indexed _ _ -> "(E_vector_indexed)"
+       | E_vector_access exp1 exp2 -> "(E_vector_access " ^ string_of_exp exp1 ^ " " ^ string_of_exp exp2 ^ ")"
+       | E_vector_subrange exp1 exp2 exp3 -> "(E_vector_subrange " ^ string_of_exp exp1 ^ " " ^ string_of_exp exp2 ^ " " ^ string_of_exp exp3 ^ ")"
+       | E_vector_update _ _ _ -> "(E_vector_update)"
+       | E_vector_update_subrange _ _ _ _ -> "(E_vector_update_subrange)"
+       | E_vector_append exp1 exp2 -> "(E_vector_append " ^ string_of_exp exp1 ^ " " ^ string_of_exp exp2 ^ ")"
+       | E_list exps -> "(E_list [" ^ String.concat "; " (List.map string_of_exp exps) ^ "])"
+       | E_cons exp1 exp2 -> "(E_cons " ^ string_of_exp exp1 ^ " :: " ^ string_of_exp exp2 ^ ")"
+       | E_record _ -> "(E_record)"
+       | E_record_update _ _ -> "(E_record_update)"
+       | E_field _ _ -> "(E_field)"
+       | E_case _ _ -> "(E_case)"
+       | E_let _ _ -> "(E_let)"
+       | E_assign lexp exp -> "(E_assign " ^ string_of_lexp lexp ^ " := " ^ string_of_exp exp ^ ")"
+       | E_sizeof _ -> "(E_sizeof _)"
+       | E_exit exp -> "(E_exit " ^ string_of_exp exp ^ ")"
+       | E_return exp -> "(E_return " ^ string_of_exp exp ^ ")"
+       | E_assert cond msg -> "(E_assert " ^ string_of_exp cond ^ " " ^ string_of_exp msg ^ ")"
+       | E_internal_cast _ _ -> "(E_internal_cast _ _)"
+       | E_internal_exp _ -> "(E_internal_exp _)"
+       | E_sizeof_internal _ -> "(E_size _)"
+       | E_internal_exp_user _ _ -> "(E_internal_exp_user _ _)"
+       | E_comment _ -> "(E_comment _)"
+       | E_comment_struc _ -> "(E_comment_struc _)"
+       | E_internal_let _ _ _ -> "(E_internal_let _ _ _)"
+       | E_internal_plet _ _ _ -> "(E_internal_plet _ _ _)"
+       | E_internal_return _ -> "(E_internal_return _)"
+       | E_internal_value value -> "(E_internal_value " ^ debug_print_value value ^ ")"
+       end)
+   end)
+
+instance forall 'a. (Show (exp 'a))
+  let show = string_of_exp
+end
+
+let string_of_alias_spec (AL_aux _as _) =
+  (match _as with
+   | AL_subreg reg_id id -> "(AL_subreg " ^ (show reg_id) ^ " " ^ (show id) ^ ")"
+   | AL_bit reg_id exp -> "(AL_bit " ^ (show reg_id) ^ " " ^ (show exp) ^ ")"
+   | AL_slice reg_id exp1 exp2 -> "(AL_slice " ^ (show reg_id) ^ " " ^ (show exp1) ^ " " ^ (show exp2) ^ ")"
+   | AL_concat reg_id1 reg_id2 -> "(AL_concat " ^ (show reg_id1) ^ " " ^ (show reg_id2) ^ ")"
+   end)
+
+instance forall 'a. (Show alias_spec 'a)
+  let show = string_of_alias_spec
+end
+
+let string_of_quant_item (QI_aux qi _) =
+  (match qi with
+   | QI_id kinded_id -> "(QI_id _)"
+   | QI_const nc -> "(QI_const _)"
+   end)
+
+instance (Show quant_item)
+  let show = string_of_quant_item
+end
+
+let string_of_typquant (TypQ_aux tq _) =
+  (match tq with
+   | TypQ_tq qis -> "(TypQ_tq [" ^ (String.concat "; " (List.map show qis)) ^ "]"
+   | TypQ_no_forall -> "TypQ_no_forall"
+   end)
+
+instance (Show typquant)
+  let show = string_of_typquant
+end
+
+let string_of_typschm (TypSchm_aux (TypSchm_ts typquant typ) _) =
+  "(TypSchm " ^ (show typquant) ^ " " ^ (show typ) ^ ")"
+
+instance (Show typschm)
+  let show = string_of_typschm
+end
+
+let rec string_of_pat (P_aux pat _) =
+  (match pat with
+   | P_lit lit -> "(P_lit " ^ show lit ^ ")"
+   | P_wild -> "P_wild"
+   | P_as pat' id -> "(P_as " ^ string_of_pat pat' ^ " " ^ show id ^ ")"
+   | P_typ typ pat' -> "(P_typ" ^ show typ ^ " " ^ string_of_pat pat' ^ ")"
+   | P_id id -> "(P_id " ^ show id ^ ")"
+   | P_app id pats -> "(P_app " ^ show id ^ " [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])"
+   | P_record _ _ -> "(P_record _ _)"
+   | P_vector pats -> "(P_vector [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])"
+   | P_vector_indexed _ -> "(P_vector_indexed _)"
+   | P_vector_concat pats -> "(P_vector_concat [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])"
+   | P_tup pats -> "(P_tup [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])"
+   | P_list pats -> "(P_list [" ^ String.concat "; " (List.map string_of_pat pats) ^ "])"
+   end)
+
+instance forall 'a. (Show pat 'a)
+  let show = string_of_pat
+end
+
+let string_of_letbind (LB_aux lb _) =
+  (match lb with
+   | LB_val_explicit ts pat exp -> "(LB_val_explicit " ^ (show ts) ^ " " ^ (show pat) ^ " " ^ (show exp) ^ ")"
+   | LB_val_implicit pat exp -> "(LB_val_implicit " ^ (show pat) ^ " " ^ (show exp) ^ ")"
+   end)
+
+instance forall 'a. (Show letbind 'a)
+  let show = string_of_letbind
+end
+
+type interp_mode = <| eager_eval : bool; track_values : bool; track_lmem : bool; debug : bool; debug_indent : string |>
+
+let indent_mode mode = if mode.debug then <| mode with debug_indent = "  " ^ mode.debug_indent |> else mode
+
+val debug_fun_enter : interp_mode -> string -> list string -> unit
+let debug_fun_enter mode name args =
+  if mode.debug then
+    debug_print (mode.debug_indent ^ ":: " ^ name ^ " args: [" ^ (String.concat "; " args) ^ "]\n")
+  else
+    ()
+
+val debug_fun_exit : forall 'a. Show 'a => interp_mode -> string -> 'a -> unit
+let debug_fun_exit mode name retval =
+  if mode.debug then
+    debug_print (mode.debug_indent ^ "=> " ^ name ^ " returns: " ^ (show retval) ^ "\n")
+  else
+    ()
 
 (* Evaluates global let binds and prepares the context for individual expression evaluation in the current model *)
-val to_top_env : (i_direction -> outcome -> maybe value) -> defs tannot -> (maybe outcome * top_level)
+val to_top_env : bool -> (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 *)
@@ -439,7 +673,7 @@ let rec to_registers dd (Defs defs) =
         | Nothing -> dd
         | Just(t, _, _, _,_) -> dd (*TODO, lets pull the direction out properly*)
       end in
-      Map.insert (get_id id) (V_register(Reg id tannot dir)) (to_registers dd (Defs defs))
+      Map.insert (get_id id) (V_register(Form_Reg id tannot dir)) (to_registers dd (Defs defs))
     | DEF_reg_dec (DEC_aux (DEC_alias id aspec) (l,tannot)) -> 
       Map.insert (get_id id) (V_register_alias aspec tannot) (to_registers dd (Defs defs))
     | _ -> to_registers dd (Defs defs)
@@ -1039,7 +1273,7 @@ let rec combine_typs ts =
 
 let reg_to_t r =
   match r with
-    | Reg _ (Just (t,_,_,_,_)) _ -> t
+    | Form_Reg _ (Just (t,_,_,_,_)) _ -> t
     | _ -> T_var "fresh"
  end
 
@@ -1084,89 +1318,8 @@ let rec val_typ v =
     | V_register_alias _ _ -> T_var "fresh_alias"
   end
 
-(* 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 ctor_kind = 
-    (Interp_ast.Unknown, 
-     if is_ctor 
-     then match ctor_kind with
-       | Just(C_Enum i) -> (enum_annot (val_typ v) (integerFromNat i))
-       | _ -> (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
-                                    if mode.track_values 
-                                    then ((e::es), union_env ev env)
-                                    else ((e::es), env))
-                  ([],(LEnv l Map.empty)) vs in
-    (es, union_env env lenv)
-  in
-  match v with
-  | V_boxref n t -> (E_aux (E_id (Id_aux (Id (show n)) Unknown)) annot, env)
-  | 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 dir vals -> 
-    let (es,env') = mapf vals env in
-    if (is_inc(dir) && n=0) 
-    then (E_aux (E_vector es) 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 if (n+1)= List.length vals
-    then (E_aux (E_vector es) annot, env')
-    else     
-      (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 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
-    (E_aux (E_record(FES_aux (FES_Fexps
-                                (List.map (fun ((id,value), e) -> (FE_aux (FE_Fexp id e) (Unknown,Nothing)))
-                                   (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 ckind vals -> 
-    let annotation = mk_annot true (Just ckind) in
-    (match (vals,ckind) with
-    | (V_lit (L_aux L_unit _), C_Union) -> (E_aux (E_app id []) annotation, env)
-    | (V_lit (L_aux L_unit _), C_Enum _) -> (E_aux (E_id id) annotation, env)
-    | (V_track (V_lit (L_aux L_unit _)) _, C_Union) -> (E_aux (E_app id []) annotation, env)
-    | (V_track (V_lit (L_aux L_unit _)) _, C_Enum _) -> (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))))])
-                    annotation, env')
-      end 
-      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]) annotation,env') end)
-  | V_register (Reg id tan dir) -> (E_aux (E_id id) annot, env)
-  | V_register _ -> Assert_extra.failwith "V_register contains subreg"
-  | V_register_alias _ _ -> (E_aux (E_id (id_of_string "dummy_register")) annot, env) (*If this persists, then alias spec must change*)
-  | V_track v' _ -> 
-    if mode.track_values
-    then begin let (fid,env') = fresh_var env in
-               let env' = add_to_env (fid,v) env' in
-               (E_aux (E_id fid) annot, env') end
-    else to_exp mode env v'
-  | V_unknown -> (E_aux (E_id (id_of_string "-100")) annot, env)
-end
+  ((E_aux (E_internal_value v) (Interp_ast.Unknown, (val_annot (val_typ v)))), env)
 
 val env_to_let : interp_mode -> lenv -> (exp tannot) -> lenv -> ((exp tannot) * lenv)
 let rec env_to_let_help mode env taint_env = match env with
@@ -1208,7 +1361,7 @@ end
 (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
 val match_pattern : top_level -> pat tannot -> value -> bool * bool * lenv
 let rec match_pattern t_level (P_aux p (_, annot)) value_whole =
-  let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in 
+  let (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in
   let (t,tag,cs) = match annot with
     | Just(t,tag,cs,e,_) -> (t,tag,cs)
     | Nothing -> (T_var "fresh",Tag_empty,[]) end in
@@ -1535,7 +1688,43 @@ let resolve_outcome to_match value_thunk action_thunk =
     | (Value v,lm,le) -> value_thunk v lm le
     | (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le)
     | (Error l s,lm,le) -> (Error l s,lm,le)
-  end
+end
+
+let string_of_action a =
+  (match a with
+  | Read_reg r _ -> "(Read_reg " ^ string_of_reg_form r ^ " _)"
+  | Write_reg r _ _ -> "(Write_reg " ^ string_of_reg_form r ^ " _ _)"
+  | Read_mem id v _ -> "(Read_mem " ^ string_of_id id ^ " " ^ debug_print_value v ^ " _)"
+  | Read_mem_tagged id v _ -> "(Read_mem_tagged " ^ string_of_id id ^ " " ^ debug_print_value v ^ " _)"
+  | Write_mem _ _ _ _ -> "(Write_mem _ _ _ _)"
+  | Write_ea id v -> "(Write_ea " ^ string_of_id id ^ " " ^ debug_print_value v ^ " _)"
+  | Write_memv _ _ _ -> "(Write_memv _ _ _)"
+  | Excl_res id -> "(Excl_res " ^ string_of_id id ^ ")"
+  | Write_memv_tagged _ _ _ _ -> "(Write_memv_tagged _ _ _ _)"
+  | Barrier id v -> "(Barrier " ^ string_of_id id ^ " " ^ debug_print_value v ^ ")"
+  | Footprint id v -> "(Footprint " ^ string_of_id id ^ " " ^ debug_print_value v ^ ")"
+  | Nondet exps _ -> "(Nondet [" ^ String.concat "; " (List.map string_of_exp exps) ^ "] _)"
+  | Call_extern s v -> "(Call_extern \"" ^ s ^ "\" " ^ debug_print_value v ^ ")"
+  | Return v -> "(Return " ^ debug_print_value v ^ ")"
+  | Exit exp -> "(Exit " ^ string_of_exp exp ^ ")"
+  | Fail v -> "(Fail " ^ debug_print_value v ^ ")"
+  | Step _ _ _ -> "(Step _ _ _)"
+  end)
+
+instance (Show action)
+  let show action = string_of_action action
+end
+
+let string_of_outcome outcome =
+  (match outcome with
+  | Value v -> "(Value " ^ debug_print_value v ^ ")"
+  | Action a _ -> "(Action " ^ string_of_action a ^ " _)"
+  | Error _ s -> "(Error _ \"" ^ s ^ "\")"
+  end)
+
+instance (Show outcome)
+  let show outcome = string_of_outcome outcome
+end
 
 let update_stack o fn = match o  with
   | Action act stack -> Action act (fn stack)
@@ -1553,7 +1742,7 @@ let get_num v = match v with
   | _ -> 0 end
 
 (*Interpret a list of expressions, tracking local state but evaluating in the same scope (i.e. not tracking env) *)
-let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
+let rec __exp_list mode t_level build_e build_v l_env l_mem vals exps =
   match exps with
   | [ ] -> (Value (build_v vals), l_mem, l_env)
   | e::exps -> 
@@ -1566,13 +1755,20 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
                                                   (e,env''))))
   end
 
-and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
-  let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in 
+and exp_list mode t_level build_e build_v l_env l_mem vals exps =
+  let _ = debug_fun_enter mode "exp_list" [show vals; show exps] in
+  let retval = __exp_list (indent_mode mode) t_level build_e build_v l_env l_mem vals exps in
+  let _ = debug_fun_exit mode "exp_list" retval in
+  retval
+
+and __interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
+  let (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in
   let (typ,tag,ncs,effect,reffect) = match annot with 
     | Nothing ->
       (T_var "fresh_v", Tag_empty,[],(Effect_aux (Effect_set []) Unknown),(Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef,efr) -> (t,tag,ncs,ef,efr) end in
   match exp with
+    | E_internal_value v -> (Value v, l_mem, l_env)
     | E_lit lit -> 
       if is_lit_vector lit 
       then let is_inc = (match typ with 
@@ -1637,7 +1833,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
             | _ -> 
               match in_env regs name with (* Register isn't a local value, so pull from global environment *)
                 | Just(V_register regform) -> regform
-                | _ -> Reg id annot default_dir end end in
+                | _ -> Form_Reg id annot default_dir end end in
           (Action (Read_reg regf Nothing) (mk_hole l annot t_level l_env l_mem), l_mem, l_env)
         | Tag_alias -> 
           match in_env aliases name with
@@ -1823,7 +2019,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
               (match in_env (env_from_list fexps) (get_id 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) ->
+            | V_register ((Form_Reg _ annot _) as reg_form) ->
               let id' = match annot with
                 | Just((T_id id'),_,_,_,_) -> id'
                 | Just((T_abbrev (T_id id') _),_,_,_,_) -> id'
@@ -1833,7 +2029,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                 | Just(indexes) ->
                   (match in_env indexes (get_id id) with
                     | Just ir ->
-                      let sub_reg = SubReg id reg_form ir in
+                      let sub_reg = Form_SubReg id reg_form ir in
                       (Action (Read_reg sub_reg Nothing)
                               (mk_hole l (val_annot (reg_to_t sub_reg)) t_level le lm),lm,le)
                     | _ -> (Error l "Internal error: unrecognized read, no id",lm,le) end)
@@ -1845,254 +2041,226 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
         (fun a -> 
           match (exp,a) with
             | (E_aux _ (l,Just(_,Tag_extern _,_,_,_)),
-               (Action (Read_reg ((Reg _ (Just((T_id id'),_,_,_,_)) _) as regf) Nothing) s)) ->
+               (Action (Read_reg ((Form_Reg _ (Just((T_id id'),_,_,_,_)) _) as regf) Nothing) s)) ->
               match in_env subregs id' with
                 | Just(indexes) ->
                   (match in_env indexes (get_id id) with
                     | Just ir -> 
-                      (Action (Read_reg (SubReg id regf ir) Nothing) s)
+                      (Action (Read_reg (Form_SubReg id regf ir) Nothing) s)
                     | _ -> Error l "Internal error, unrecognized read, no id"
                    end) 
                 | Nothing -> Error l "Internal error, unrecognized read, no reg" end
             | (E_aux _ (l,Just(_,Tag_extern _,_,_,_)),
-               (Action (Read_reg ((Reg _ (Just((T_abbrev (T_id id') _),_,_,_,_)) _) as regf) Nothing) s))->
+               (Action (Read_reg ((Form_Reg _ (Just((T_abbrev (T_id id') _),_,_,_,_)) _) as regf) Nothing) s))->
               match in_env subregs id' with
                 | Just(indexes) ->
                   match in_env indexes (get_id id) with
                     | Just ir -> 
-                      (Action (Read_reg (SubReg id regf ir) Nothing) s)
+                      (Action (Read_reg (Form_SubReg id regf ir) Nothing) s)
                     | _ -> Error l "Internal error, unrecognized read, no id"
                                 end 
                 | Nothing -> Error l "Internal error, unrecognized read, no reg" end
              | _ -> update_stack a (add_to_top_frame (fun e env -> (E_aux(E_field e id) (l,annot),env))) end)
     | E_vector_access vec i ->
-      resolve_outcome 
-        (interp_main mode t_level l_env l_mem i)
-        (fun iv lm le -> 
-          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 ->
-                  let v_access vvec num = (match (detaint vvec, detaint num) with
-                    | (V_vector _ _ _,V_lit _) -> Value (access_vector vvec n)
-                    | (V_vector_sparse _ _ _ _ _,V_lit _) -> Value (access_vector vvec n)
-                    | (V_register reg, V_lit _) ->
-                      Action (Read_reg reg (Just (n,n))) (mk_hole l annot t_level l_env lm) 
-                    | (V_unknown,_) -> Value V_unknown 
-                    | _ -> Assert_extra.failwith 
-                      ("Vector access error: " ^ (string_of_value vvec) ^ "[" ^ (show n) ^ "]") end) in
-                  (v_access (retaint iv vvec) iv,lm,le))
-                (fun a ->
-                 (*TODO I think this pattern match is no longer necessary *)
-                  match a with
-                    | Action (Read_reg reg Nothing) stack -> 
-                      (match vec with
-                        | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
-                        | _ -> Action (Read_reg reg Nothing) 
-                          (add_to_top_frame 
-                             (fun v env -> 
-                               let (iv_e, env) = to_exp mode env iv in
-                               (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end)
-                    | Action (Read_reg reg (Just (o,p))) stack ->
-                      (match vec with
-                        | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
-                        | _ -> Action (Read_reg reg (Just (o,p))) 
-                          (add_to_top_frame 
-                             (fun v env -> 
-                               let (iv_e, env) = to_exp mode env iv in
-                               (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end)
-                    | _ -> 
-                      update_stack a 
-                        (add_to_top_frame 
-                           (fun v env -> 
-                             let (iv_e, env) = to_exp mode env iv in
-                             (E_aux (E_vector_access v iv_e) (l,annot), env))) end)
-            | _ -> (Error l "Vector access not given a number for index",lm,l_env) end)
-        (fun a -> update_stack a (add_to_top_frame (fun i env -> (E_aux (E_vector_access vec i) (l,annot), env))))
-    | E_vector_subrange vec i1 i2 ->
-      resolve_outcome 
-        (interp_main mode t_level l_env l_mem i1)
-        (fun i1v lm le ->
-          match detaint i1v with
-            | V_unknown -> (Value i1v,lm,le)
-            | V_lit (L_aux (L_num n1) nl1) -> 
-              resolve_outcome 
-                (interp_main mode t_level l_env lm i2)
-                (fun i2v lm le ->
-                  match detaint i2v with
-                    | V_unknown -> (Value i2v,lm,le)
-                    | V_lit (L_aux (L_num n2) nl2) ->
-                      resolve_outcome 
-                        (interp_main mode t_level l_env lm vec)
-                        (fun vvec lm le ->
-                          let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) i1v i2v in
-                          let take_slice vvec =
-                            let (n1,n2) = (natFromInteger n1,natFromInteger n2) in
-                            (match detaint vvec with
-                             | V_vector _ _ _ -> Value (slice_vector vvec n1 n2)
-                             | V_vector_sparse _ _ _ _ _ -> Value (slice_vector vvec n1 n2)
-                             | V_unknown -> 
-                               let inc = n1 < n2 in
-                               Value (retaint vvec (V_vector n1 (if inc then IInc else IDec) 
-                                                      (List.replicate ((if inc then n1-n2 else n2-n1)+1) V_unknown)))
-                             | V_register reg ->
-                               Action (Read_reg reg (Just (n1,n2))) (mk_hole l annot t_level le lm)
-                             | _ -> (Error l ("Vector slice of non-vector " ^ (string_of_value vvec))) end) in
-                          ((take_slice (retaint slice vvec)), lm,le))
-                        (fun a -> 
-                          let rebuild v env = let (ie1,env) = to_exp mode env i1v in
-                                              let (ie2,env) = to_exp mode env i2v in
-                           (E_aux (E_vector_subrange v ie1 ie2) (l,annot), env) in
-                          (*TODO this pattern match should no longer be needed*)
-                          match a with 
-                            | Action (Read_reg reg Nothing) stack ->
-                              match vec with
-                                | (E_aux _ (l,Just(_,Tag_extern _,_,_,_))) -> 
-                                  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((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)
-                | _ -> (Error l "vector subrange did not receive a range value", l_mem, l_env)
-                 end)
-                (fun a -> update_stack a 
-                  (add_to_top_frame 
-                     (fun i2 env -> 
-                       let (ie1,env) = to_exp mode env i1v in
-                       (E_aux (E_vector_subrange vec ie1 i2) (l,annot), env))))
-        | _ -> (Error l "vector subrange did not receive a range value", l_mem, l_env) end) 
-        (fun a -> 
-          update_stack a (add_to_top_frame (fun i1 env -> (E_aux (E_vector_subrange vec i1 i2) (l,annot), env))))
-    | E_vector_update vec i exp ->
-      resolve_outcome 
-        (interp_main mode t_level l_env l_mem i)
-        (fun vi lm le ->
-          (match (detaint vi) with
-            | V_lit (L_aux (L_num n1) ln1) ->
-              (resolve_outcome 
-                 (interp_main mode t_level le lm exp)
-                 (fun vup lm le ->
-                   resolve_outcome 
-                     (interp_main mode t_level le lm vec)
-                     (fun vec lm le ->
-                       let fvup vi vec = (match vec with
-                         | 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))
-                     (fun a -> update_stack a 
-                       (add_to_top_frame 
-                          (fun v env ->
-                            let (eup,env') = (to_exp mode env vup) in 
-                            let (ei, env') = (to_exp mode env' vi) in
-                            (E_aux (E_vector_update v ei eup) (l,annot), env')))))
-                 (fun a -> update_stack a 
-                   (add_to_top_frame 
-                      (fun e env -> 
-                        let (ei, env) = to_exp mode env vi in
-                        (E_aux (E_vector_update vec ei e) (l,annot), env)))))
-            | V_unknown -> (Value vi,lm,l_env)
-            | _ -> Assert_extra.failwith "Update of vector requires number for access" end))
-        (fun a -> update_stack a (add_to_top_frame (fun i env -> (E_aux (E_vector_update vec i exp) (l,annot), env))))
-    | E_vector_update_subrange vec i1 i2 exp ->
-      resolve_outcome 
-        (interp_main mode t_level l_env l_mem i1)
-        (fun vi1 lm le ->
-          match detaint vi1 with
-            | V_unknown -> (Value vi1,lm,le)
-            | V_lit (L_aux (L_num n1) ln1) ->
-              resolve_outcome 
-                (interp_main mode t_level l_env lm i2) 
-                (fun vi2 lm le ->
-                  match detaint vi2 with
-                    | V_unknown -> (Value vi2,lm,le)
-                    | V_lit (L_aux (L_num n2) ln2) ->
-                      resolve_outcome 
-                        (interp_main mode t_level l_env lm exp)
-                        (fun v_rep lm le ->
-                          (resolve_outcome 
-                             (interp_main mode t_level l_env lm vec)
-                             (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 (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))
-                             (fun a -> update_stack a 
-                               (add_to_top_frame 
-                                  (fun v env -> 
-                                    let (e_rep,env') = to_exp mode env v_rep in
-                                    let (ei1, env') = to_exp mode env' vi1 in
-                                    let (ei2, env') = to_exp mode env' vi2 in
-                                    (E_aux (E_vector_update_subrange v ei1 ei2 e_rep) (l,annot), env'))))))
-                        (fun a -> update_stack a 
-                          (add_to_top_frame 
-                             (fun e env -> 
-                               let (ei1,env') = to_exp mode env vi1 in
-                               let (ei2,env') = to_exp mode env' vi2 in
-                               (E_aux (E_vector_update_subrange vec ei1 ei2 e) (l,annot),env'))))
-                    | _ -> Assert_extra.failwith "vector update requires number" end)
-                (fun a -> 
-                  update_stack a (add_to_top_frame 
-                                    (fun i2 env -> 
-                                      let (ei1, env') = to_exp mode env vi1 in
-                                      (E_aux (E_vector_update_subrange vec ei1 i2 exp) (l,annot), env'))))
-            | _ -> Assert_extra.failwith "vector update requires number" end)
-        (fun a -> 
-          update_stack a 
-            (add_to_top_frame (fun i1 env -> (E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot), env))))
-    | E_vector_append e1 e2 ->
-      resolve_outcome 
-        (interp_main mode t_level l_env l_mem e1)
-        (fun v1 lm le ->
-         match detaint v1 with
-            | V_unknown -> (Value v1,lm,l_env)
-            | _ ->
-              (resolve_outcome 
-                 (interp_main mode t_level l_env lm e2)
-                 (fun v2 lm le ->
-                   let append v1 v2 = (match (v1,v2) with
-                     | (V_vector _ dir vals1, V_vector _ _ vals2) -> 
-                       let vals = vals1++vals2 in
-                       let len = List.length vals in
-                       if is_inc(dir) 
-                       then V_vector 0 dir vals
-                       else V_vector (len-1) dir vals
-                     | (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) 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) 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) 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 two vectors but given "
-                                                   ^ (string_of_value v1) ^ " " ^ (string_of_value v2)) end) in
-                   (Value (binary_taint append v1 v2),lm,le))
-                 (fun a -> update_stack a (add_to_top_frame 
-                                             (fun e env -> 
-                                               let (e1,env') = to_exp mode env v1 in
-                                               (E_aux (E_vector_append e1 e) (l,annot),env'))))) end)
-        (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_vector_append e e2) (l,annot),env))))
+       resolve_outcome
+         (interp_main mode t_level l_env l_mem vec)
+         (fun vvec lm le ->
+           resolve_outcome
+             (interp_main mode t_level l_env lm i)
+             (fun iv lm le ->
+               (match detaint iv with
+                | V_unknown -> (Value iv,lm,le)
+                | V_lit (L_aux (L_num n) ln) ->
+                   let n = natFromInteger n in
+                   let v_access vvec num =
+                     (match (detaint vvec, detaint num) with
+                      | (V_vector _ _ _,V_lit _) -> Value (access_vector vvec n)
+                      | (V_vector_sparse _ _ _ _ _,V_lit _) -> Value (access_vector vvec n)
+                      | (V_register reg, V_lit _) ->
+                         Action (Read_reg reg (Just (n,n))) (mk_hole l annot t_level l_env lm)
+                      | (V_unknown,_) -> Value V_unknown
+                      | _ -> Assert_extra.failwith
+                               ("Vector access error: " ^ (string_of_value vvec) ^ "[" ^ (show n) ^ "]")
+                      end)
+                   in
+                   (v_access (retaint iv vvec) iv,lm,le)
+                | _ -> (Error l "Vector access not given a number for index",lm,l_env)
+                end))
+                 (fun a -> update_stack a (add_to_top_frame(fun i' env ->
+                                               let (vec_e, env') = to_exp mode env vvec in
+                                               (E_aux (E_vector_access vec_e i') (l,annot), env')))))
+             (fun a ->
+               update_stack a (add_to_top_frame (fun vec' env ->
+                                   (E_aux (E_vector_access vec' i) (l,annot), env))))
+         | E_vector_subrange vec i1 i2 ->
+            resolve_outcome
+              (interp_main mode t_level l_env l_mem vec)
+              (fun vvec lm le ->
+                resolve_outcome
+                  (interp_main mode t_level l_env lm i1)
+                  (fun i1v lm le ->
+                    resolve_outcome
+                      (interp_main mode t_level l_env lm i2)
+                      (fun i2v lm le ->
+                        match detaint i1v with
+                        | V_unknown -> (Value i1v,lm,le)
+                        | V_lit (L_aux (L_num n1) nl1) ->
+                           match detaint i2v with
+                           | V_unknown -> (Value i2v,lm,le)
+                           | V_lit (L_aux (L_num n2) nl2) ->
+                              let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) i1v i2v in
+                              let take_slice vvec =
+                                let (n1,n2) = (natFromInteger n1,natFromInteger n2) in
+                                (match detaint vvec with
+                                 | V_vector _ _ _ -> Value (slice_vector vvec n1 n2)
+                                 | V_vector_sparse _ _ _ _ _ -> Value (slice_vector vvec n1 n2)
+                                 | V_unknown ->
+                                    let inc = n1 < n2 in
+                                    Value (retaint vvec (V_vector n1 (if inc then IInc else IDec)
+                                                                  (List.replicate ((if inc then n1-n2 else n2-n1)+1) V_unknown)))
+                                 | V_register reg ->
+                                    Action (Read_reg reg (Just (n1,n2))) (mk_hole l annot t_level le lm)
+                                 | _ -> (Error l ("Vector slice of non-vector " ^ (string_of_value vvec))) end) in
+                              ((take_slice (retaint slice vvec)), lm,le)
+                           | _ -> (Error l "vector subrange did not receive a range value", l_mem, l_env)
+                       end
+                      | _ -> (Error l "vector subrange did not receive a range value", l_mem, l_env)
+                       end)
+                      (fun a -> update_stack a (add_to_top_frame (fun i2' env ->
+                                                    let (vec_e, env') = to_exp mode env vvec in
+                                                    let (i1_e, env'') = to_exp mode env' i1v in
+                                                    (E_aux (E_vector_subrange vec_e i1_e i2') (l,annot), env'')))))
+                  (fun a ->
+                    update_stack a (add_to_top_frame (fun i1' env ->
+                                        let (vec_e, env') = to_exp mode env vvec in
+                                        (E_aux (E_vector_subrange vec_e i1' i2) (l,annot), env')))))
+              (fun a ->
+                update_stack a (add_to_top_frame (fun vec' env ->
+                                    (E_aux (E_vector_subrange vec' i1 i2) (l,annot), env))))
+         | E_vector_update vec i exp ->
+            resolve_outcome
+              (interp_main mode t_level l_env l_mem vec)
+              (fun vvec lm le ->
+                resolve_outcome
+                  (interp_main mode t_level l_env lm i)
+                  (fun vi lm le ->
+                    resolve_outcome
+                      (interp_main mode t_level l_env lm exp)
+                      (fun vup lm le ->
+                        (match (detaint vi) with
+                         | V_lit (L_aux (L_num n1) ln1) ->
+                            let fvup vi vvec =
+                              (match vvec with
+                               | V_vector _ _ _ -> fupdate_vec vvec (natFromInteger n1) vup
+                               | V_vector_sparse _ _ _ _ _ -> fupdate_vec vvec (natFromInteger n1) vup
+                               | V_unknown -> V_unknown
+                               | _ -> Assert_extra.failwith "Update of vector given non-vector"
+                               end)
+                            in
+                            (Value (binary_taint fvup vi vvec),lm,le)
+                         | V_unknown -> (Value vi,lm,le)
+                         | _ -> Assert_extra.failwith "Update of vector requires number for access"
+                         end))
+                      (fun a -> update_stack a (add_to_top_frame (fun exp' env ->
+                                                    let (vec_e, env') = to_exp mode env vvec in
+                                                    let (i_e, env'') = to_exp mode env' vi in
+                                                    (E_aux (E_vector_update vec_e i_e exp') (l,annot), env'')))))
+                  (fun a -> update_stack a (add_to_top_frame (fun i' env ->
+                                                let (vec_e, env') = to_exp mode env vvec in
+                                                (E_aux (E_vector_update vec_e i' exp) (l,annot), env')))))
+              (fun a -> update_stack a (add_to_top_frame (fun vec' env ->
+                                            (E_aux (E_vector_update vec' i exp) (l,annot), env))))
+         | E_vector_update_subrange vec i1 i2 exp ->
+            resolve_outcome
+              (interp_main mode t_level l_env l_mem vec)
+              (fun vvec lm le ->
+                resolve_outcome
+                  (interp_main mode t_level l_env lm i1)
+                  (fun vi1 lm le ->
+                    resolve_outcome
+                      (interp_main mode t_level l_env lm i2)
+                      (fun vi2 lm le ->
+                        resolve_outcome
+                          (interp_main mode t_level l_env lm exp)
+                          (fun v_rep lm le ->
+                            (match detaint vi1 with
+                             | V_unknown -> (Value vi1,lm,le)
+                             | V_lit (L_aux (L_num n1) ln1) ->
+                                (match detaint vi2 with
+                                 | V_unknown -> (Value vi2,lm,le)
+                                 | V_lit (L_aux (L_num n2) ln2) ->
+                                    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 (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)
+                                 | _ -> Assert_extra.failwith "vector update requires number"
+                                 end)
+                             | _ -> Assert_extra.failwith "vector update requires number"
+                             end))
+                          (fun a -> update_stack a (add_to_top_frame (fun exp' env ->
+                                                        let (vec_e, env') = to_exp mode env vvec  in
+                                                        let (i1_e, env'') = to_exp mode env' vi1  in
+                                                        let (i2_e, env''') = to_exp mode env'' vi1  in
+                                                        (E_aux (E_vector_update_subrange vec_e i1_e i2_e exp') (l,annot), env''')))))
+                      (fun a -> update_stack a (add_to_top_frame (fun i2' env ->
+                                                    let (vec_e, env') = to_exp mode env vvec  in
+                                                    let (i1_e, env'') = to_exp mode env' vi1  in
+                                                    (E_aux (E_vector_update_subrange vec_e i1_e i2' exp) (l,annot), env'')))))
+                  (fun a -> update_stack a (add_to_top_frame (fun i1' env ->
+                                                let (vec_e, env') = to_exp mode env vvec  in
+                                                (E_aux (E_vector_update_subrange vec_e i1' i2 exp) (l,annot), env')))))
+              (fun a -> update_stack a (add_to_top_frame (fun vec' env ->
+                                            (E_aux (E_vector_update_subrange vec' i1 i2 exp) (l,annot), env))))
+         | E_vector_append e1 e2 ->
+            resolve_outcome
+              (interp_main mode t_level l_env l_mem e1)
+              (fun v1 lm le ->
+                resolve_outcome
+                  (interp_main mode t_level l_env lm e2)
+                  (fun v2 lm le ->
+                    (match detaint v1 with
+                     | V_unknown -> (Value v1,lm,le)
+                     | _ ->
+                        let append v1 v2 =
+                          (match (v1,v2) with
+                           | (V_vector _ dir vals1, V_vector _ _ vals2) ->
+                              let vals = vals1++vals2 in
+                              let len = List.length vals in
+                              if is_inc(dir)
+                              then V_vector 0 dir vals
+                              else V_vector (len-1) dir vals
+                           | (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) 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) 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) 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 two vectors but given "
+                                                         ^ (string_of_value v1) ^ " " ^ (string_of_value v2))
+                           end)
+                        in
+                        (Value (binary_taint append v1 v2),lm,le)
+                     end))
+                  (fun a -> update_stack a (add_to_top_frame (fun e2' env ->
+                                                let (e1_e, env') = to_exp mode env v1  in
+                                                (E_aux (E_vector_append e1_e e2') (l,annot), env')))))
+              (fun a -> update_stack a (add_to_top_frame (fun e1' env ->
+                                            (E_aux (E_vector_append e1' e2) (l,annot), env))))
     | E_tuple(exps) -> 
       exp_list mode t_level (fun exps env' -> (E_aux (E_tuple exps) (l,annot), env')) V_tuple l_env l_mem [] exps
     | E_vector(exps) ->
@@ -2415,8 +2583,14 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
   | _ -> (Error l "Internal expression escaped to interpreter", l_mem, l_env)
   end
 
+and interp_main mode t_level l_env l_mem exp =
+  let _ = debug_fun_enter mode "interp_main" [show exp] in
+  let retval = __interp_main (indent_mode mode) t_level l_env l_mem exp in
+  let _ = debug_fun_exit mode "interp_main" retval in
+  retval
+
 (*TODO shrink location information on recursive calls *)
- and interp_block mode t_level init_env local_env local_mem l tannot exps =
+and __interp_block mode t_level init_env local_env local_mem l tannot exps =
    match exps with
     | [] -> (Value (V_lit (L_aux (L_unit) Unknown)), local_mem, init_env)
     | [exp] -> 
@@ -2431,12 +2605,18 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                         else debug_out Nothing Nothing (E_aux (E_block exps) (l,tannot)) t_level lm le)
                       (fun a -> update_stack a 
                         (add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env))))
-    end
+   end
+
+and interp_block mode t_level init_env local_env local_mem l tannot exps =
+  let _ = debug_fun_enter mode "interp_block" [show exps] in
+  let retval = __interp_block (indent_mode mode) t_level init_env local_env local_mem l tannot exps in
+  let _ = debug_fun_exit mode "interp_block" retval in
+  retval
 
-and create_write_message_or_update mode t_level value l_env l_mem is_top_level
+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)) * maybe value) =
-   let (Env fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in
+   let (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in
    let (typ,tag,ncs,ef,efr) = match annot with 
      | Nothing -> (T_var "fresh_v", Tag_empty, [],
                    (Effect_aux (Effect_set []) Unknown),(Effect_aux (Effect_set []) Unknown))
@@ -2575,7 +2755,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
                    (match in_env indexes (get_id subreg) with
                     | Just ir -> 
                       (Action 
-                         (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing 
+                         (Write_reg (Form_SubReg subreg (Form_Reg reg annot' default_dir) 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))
@@ -2589,7 +2769,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
                    (match in_env indexes (get_id subreg) with
                     | Just ir -> 
                       (Action 
-                         (Write_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing 
+                         (Write_reg (Form_SubReg subreg (Form_Reg reg annot' default_dir) 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))
@@ -2602,7 +2782,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
                   (fun v le lm -> match v with 
                      | V_lit (L_aux (L_num i) _) -> 
                        let i = natFromInteger i in
-                       (Action (Write_reg (Reg reg annot' default_dir) (Just (i,i)) 
+                       (Action (Write_reg (Form_Reg reg annot' default_dir) (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)
@@ -2619,7 +2799,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
                               | 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' default_dir) (Just (start,stop)) 
+                                (Action (Write_reg (Form_Reg reg annot' default_dir) (Just (start,stop)) 
                                            (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),
@@ -2640,7 +2820,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
                   | (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 default_dir) Nothing 
+                       (Write_reg (Form_Reg reg1 annot1 default_dir) Nothing 
                           (slice_vector value (natFromInteger b1) (natFromInteger r1)))
                        (Thunk_frame
                           (E_aux (E_assign (LEXP_aux (LEXP_id reg2) annot2)
@@ -3062,13 +3242,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
        | Read_mem _ _ _ -> ((Action a s,lm,le), next_builder, Nothing)
        | Read_mem_tagged _ _ _ -> ((Action a s,lm,le), next_builder, Nothing)
        | Call_extern _ _ -> ((Action a s,lm,le), next_builder, Nothing)
-       | Write_reg ((Reg _ (Just(T_id id',_,_,_,_)) _) as regf) Nothing value -> 
+       | Write_reg ((Form_Reg _ (Just(T_id id',_,_,_,_)) _) as regf) Nothing value -> 
          match in_env subregs id' with
            | Just(indexes) ->
              match in_env indexes (get_id id) with
                | Just ir -> 
                  ((Action 
-                     (Write_reg (SubReg id regf ir) Nothing 
+                     (Write_reg (Form_SubReg id regf ir) Nothing 
                         (update_vector_start default_dir (get_first_index_range ir)
                            (get_index_range_size ir) value)) s,
                    lm,le), 
@@ -3076,13 +3256,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
                | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing,Nothing)
                  end 
             | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing,Nothing) end
-       | Write_reg ((Reg _ (Just((T_abbrev(T_id id') _),_,_,_,_)) _) as regf) Nothing value -> 
+       | Write_reg ((Form_Reg _ (Just((T_abbrev(T_id id') _),_,_,_,_)) _) as regf) Nothing value -> 
          match in_env subregs id' with
            | Just(indexes) ->
              match in_env indexes (get_id id) with
                | Just ir -> 
                  ((Action 
-                     (Write_reg (SubReg id regf ir) Nothing 
+                     (Write_reg (Form_SubReg id regf ir) Nothing 
                         (update_vector_start default_dir (get_first_index_range ir)
                            (get_index_range_size ir) value)) s,
                    lm,le), 
@@ -3095,7 +3275,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level
      | e -> e end)
      end
 
-and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
+and create_write_message_or_update mode t_level value l_env l_mem is_top_level le =
+  let _ = debug_fun_enter mode "create_write_message_or_update" [show le] in
+  let retval = __create_write_message_or_update (indent_mode mode) t_level value l_env l_mem is_top_level le in
+  let _ = debug_fun_exit mode "create_write_message_or_update" "_" in
+  retval
+
+and __interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
   match lbind with
   | LB_val_explicit t pat exp ->
     match (interp_main mode t_level l_env l_mem exp) with
@@ -3113,10 +3299,16 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
       | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end)
     | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) (l,annot)))))
     | e -> (e,Nothing) end
-end     
+end
+
+and interp_letbind mode t_level l_env l_mem lb =
+  let _ = debug_fun_enter mode "interp_letbind" [show lb] in
+  let retval = __interp_letbind (indent_mode mode) t_level l_env l_mem lb in
+  let _ = debug_fun_exit mode "interp_letbind" "_" in
+  retval
 
-and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
-  let (Env defs instrs default_dir lets regs ctors subregs aliases) = t_level in 
+and __interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
+  let (Env defs instrs default_dir lets regs ctors subregs aliases debug) = 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
@@ -3130,7 +3322,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
       (match in_env subregs reg_ti with
         | Just indexes -> 
           (match in_env indexes (get_id subreg) with
-           | Just ir -> (Action (Read_reg (SubReg subreg (Reg reg annot' default_dir) ir) Nothing) stack,
+           | Just ir -> (Action (Read_reg (Form_SubReg subreg (Form_Reg reg annot' default_dir) ir) Nothing) stack,
                          l_mem, l_env)
            | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
         | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " reg_ti),
@@ -3140,7 +3332,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 i) _) -> 
             let i = natFromInteger i in
-            (Action (Read_reg (Reg reg annot' default_dir) (Just (i,i))) stack, l_mem, l_env)
+            (Action (Read_reg (Form_Reg reg annot' default_dir) (Just (i,i))) stack, l_mem, l_env)
           | _ -> Assert_extra.failwith "alias bit did not reduce to number" end)
         (fun a -> a) (*Should not currently happen as type system enforces constants*)
     | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> 
@@ -3154,7 +3346,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
                    (match v with
                      | V_lit (L_aux (L_num stop) _) ->
                        let (start,stop) = (natFromInteger start,natFromInteger stop) in
-                       (Action (Read_reg (Reg reg annot' default_dir) (Just (start,stop))) stack, l_mem, l_env)
+                       (Action (Read_reg (Form_Reg reg annot' default_dir) (Just (start,stop))) stack, l_mem, l_env)
                      | _ -> Assert_extra.failwith ("Alias slice evaluted non-lit " ^ (string_of_value v))
                      end))
                  (fun a -> a))
@@ -3162,7 +3354,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
          end)
         (fun a -> a) (*Neither action function should occur, due to above*)
     | AL_concat (RI_aux (RI_id reg1) (l1, annot1)) (RI_aux (RI_id reg2) annot2) -> 
-      (Action (Read_reg (Reg reg1 annot1 default_dir) Nothing)
+      (Action (Read_reg (Form_Reg reg1 annot1 default_dir) Nothing)
               (Hole_frame redex_id
                           (E_aux (E_vector_append (E_aux (E_id redex_id) (l1, (intern_annot annot1)))
                                                   (E_aux (E_id reg2) annot2)) 
@@ -3170,8 +3362,14 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
     | _ -> Assert_extra.failwith "alias spec not well formed"
 end
 
+and interp_alias_read mode t_level l_env l_mem al =
+  let _ = debug_fun_enter mode "interp_alias_read" [show al] in
+  let retval = __interp_alias_read (indent_mode mode) t_level l_env l_mem al in
+  let _ = debug_fun_exit mode "interp_alias_read" retval in
+  retval
+
 let rec eval_toplevel_let handle_action tlevel env mem lbind = 
-  match interp_letbind <|eager_eval=true; track_values=false; track_lmem=false|> tlevel env mem lbind with
+  match interp_letbind <| eager_eval=true; track_values=false; track_lmem=false; debug=false; debug_indent="" |> tlevel env mem lbind with
     | ((Value v, lm, (LEnv _ le)),_) -> Just le
     | ((Action a s,lm,le), Just le_builder) -> 
       (match handle_action (Action a s) with
@@ -3184,7 +3382,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 fdefs instrs default_dir lets regs ctors subregs aliases) = t_level in
+  let  (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) = t_level in
   match defs with
   | [] -> ((Value (V_lit (L_aux L_unit Unknown)), (emem "global_letbinds"), eenv),t_level)
   | def::defs ->
@@ -3194,10 +3392,10 @@ let rec to_global_letbinds handle_action (Defs defs) t_level =
         | Just le -> 
           to_global_letbinds handle_action
             (Defs defs) 
-            (Env fdefs instrs default_dir (Map.(union) lets le) regs ctors subregs aliases)
+            (Env fdefs instrs default_dir (Map.(union) lets le) regs ctors subregs aliases debug)
         | Nothing -> 
           to_global_letbinds handle_action (Defs defs) 
-                                           (Env fdefs instrs default_dir lets regs ctors subregs aliases) end
+                                           (Env fdefs instrs default_dir lets regs ctors subregs aliases debug) end
     | DEF_type (TD_aux tdef _) ->
       match tdef with
       | TD_enum id ns ids _ -> 
@@ -3208,7 +3406,7 @@ let rec to_global_letbinds handle_action (Defs defs) t_level =
             (List.foldl (fun (c,rst) eid -> (1+c,(get_id eid,V_ctor eid typ (C_Enum c) unitv)::rst)) (0,[]) ids)) in
         to_global_letbinds 
           handle_action (Defs defs) 
-                        (Env fdefs instrs default_dir (Map.(union) lets enum_vals) regs ctors subregs aliases)
+                        (Env fdefs instrs default_dir (Map.(union) lets enum_vals) regs ctors subregs aliases debug)
       | _ -> to_global_letbinds handle_action (Defs defs) t_level end
     | _ -> to_global_letbinds handle_action (Defs defs) t_level
     end
@@ -3223,28 +3421,34 @@ let rec extract_default_direction (Defs defs) = match defs with
       | _ -> extract_default_direction (Defs defs) end end
 
 (*TODO Contemplate making execute environment variable instead of constant*)
-let to_top_env external_functions defs = 
+let to_top_env debug external_functions defs =
   let direction = (extract_default_direction defs) in
   let t_level = Env (to_fdefs defs) 
                     (extract_instructions "execute" defs) 
                     direction
                     Map.empty (* empty letbind and enum values, call below will fill in any *) 
                     (to_registers direction defs) 
-                    (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
+                    (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) debug 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)
   end
 
-let interp mode external_functions defs exp =
-  match (to_top_env external_functions defs) with
+let __interp mode external_functions defs exp =
+  match (to_top_env mode.debug external_functions defs) with
     | (Nothing,t_level) -> 
       interp_main mode t_level eenv (emem "top level") exp
     | (Just o,_) -> (o,(emem "top level error"),eenv) 
   end
 
-let rec resume_with_env mode stack value =
+let interp mode external_functions defs exp =
+  let _ = debug_fun_enter mode "interp" [show exp] in
+  let retval = __interp (indent_mode mode) external_functions defs exp in
+  let _ = debug_fun_exit mode "interp" retval in
+  retval
+
+let rec __resume_with_env mode stack value =
   match (stack,value) with
   | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume_with_env",eenv)
   | (Hole_frame id exp t_level env mem Top,Just value) -> 
@@ -3271,10 +3475,17 @@ let rec resume_with_env mode stack value =
       match interp_main mode t_level env mem exp with | (o,_,e) -> (o,e) end 
     | (Action action stack,e) -> (Action action (Thunk_frame exp t_level env mem stack),e)
     | (Error l s,e) -> (Error l s,e)
-    end  
+    end
   end
 
-let rec resume mode stack value =
+and resume_with_env mode stack value =
+  let _ = debug_fun_enter mode "resume_with_env" [show value] in
+  let retval = __resume_with_env (indent_mode mode) stack value in
+  let _ = debug_fun_exit mode "interp" retval in
+  retval
+
+
+let rec __resume mode stack value =
   match (stack,value) with
   | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume",(emem "top level error"),eenv)
   | (Hole_frame id exp t_level env mem Top,Just value) -> 
@@ -3305,3 +3516,8 @@ let rec resume mode stack value =
     end  
   end
 
+and resume mode stack value =
+  let _ = debug_fun_enter mode "resume" [show value] in
+  let retval = __resume (indent_mode mode) stack value in
+  let _ = debug_fun_exit mode "resume" retval in
+  retval