move value type definitions to ott, and introduce new E_internal_value ast node for passing around encapsulated evaluated values; change Interp.to_exp to now just wrap values in this node

8 files changed, 750 insertions, 810 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 9c88eec7..a0276963 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -54,8 +54,6 @@ open import Interp_ast
 open import Interp_utilities
 open import Instruction_extractor
 
-type tannot = Interp_utilities.tannot
-
 val debug_print : string -> unit
 declare ocaml target_rep function debug_print s = `Printf.eprintf` "%s" s
 
@@ -78,36 +76,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
@@ -249,7 +225,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 +253,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"
@@ -439,7 +415,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 +1015,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 +1060,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
@@ -1573,6 +1468,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
       (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 +1533,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 +1719,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 +1729,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,22 +1741,22 @@ 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
@@ -2575,7 +2471,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 +2485,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 +2498,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 +2515,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 +2536,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 +2958,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 +2972,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), 
@@ -3130,7 +3026,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 +3036,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 +3050,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 +3058,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)) 
diff --git a/src/lem_interp/interp_ast.lem b/src/lem_interp/interp_ast.lem
index b706d3aa..733d1a36 100644
--- a/src/lem_interp/interp_ast.lem
+++ b/src/lem_interp/interp_ast.lem
@@ -40,9 +40,11 @@
 (*  SUCH DAMAGE.                                                          *)
 (*========================================================================*)
 
-(* generated by Ott 0.25 from: l2_typ.ott l2.ott *)
+(* generated by Ott 0.25 from: l2.ott *)
 open import Pervasives
 
+open import Pervasives
+open import Pervasives_extra
 open import Map
 open import Maybe
 open import Set_extra
@@ -72,21 +74,17 @@ type base_kind_aux =  (* base kind *)
  | BK_effect (* kind of effect sets *)
 
 
-type base_kind = 
- | BK_aux of base_kind_aux * l
-
-
-type kid_aux =  (* variables with kind, ticked to differntiate from program variables *)
+type kid_aux =  (* kinded IDs: $Type$, $Nat$, $Order$, and $Effect$ variables *)
  | Var of x
 
 
-type id_aux =  (* Identifier *)
+type id_aux =  (* identifier *)
  | Id of x
  | DeIid of x (* remove infix status *)
 
 
-type kind_aux =  (* kinds *)
- | K_kind of list base_kind
+type base_kind = 
+ | BK_aux of base_kind_aux * l
 
 
 type kid = 
@@ -97,24 +95,28 @@ type id =
  | Id_aux of id_aux * l
 
 
-type kind = 
- | K_aux of kind_aux * l
+type kind_aux =  (* kinds *)
+ | K_kind of list base_kind
 
 
-type nexp_aux =  (* expression of kind Nat, for vector sizes and origins *)
- | Nexp_id of id (* identifier, bound by def Nat x = nexp *)
+type nexp_aux =  (* numeric expression, of kind $Nat$ *)
+ | Nexp_id of id (* abbreviation identifier *)
  | Nexp_var of kid (* variable *)
  | Nexp_constant of integer (* constant *)
  | Nexp_times of nexp * nexp (* product *)
  | Nexp_sum of nexp * nexp (* sum *)
  | Nexp_minus of nexp * nexp (* subtraction *)
  | Nexp_exp of nexp (* exponential *)
- | Nexp_neg of nexp (* For internal use *)
+ | Nexp_neg of nexp (* for internal use only *)
 
 and nexp = 
  | Nexp_aux of nexp_aux * l
 
 
+type kind = 
+ | K_aux of kind_aux * l
+
+
 type base_effect_aux =  (* effect *)
  | BE_rreg (* read register *)
  | BE_wreg (* write register *)
@@ -129,23 +131,23 @@ type base_effect_aux =  (* effect *)
  | BE_depend (* dynamic footprint *)
  | BE_undef (* undefined-instruction exception *)
  | BE_unspec (* unspecified values *)
- | BE_nondet (* nondeterminism from intra-instruction parallelism *)
- | BE_escape (* Tracking of expressions and functions that might call exit *)
- | BE_lset (* Local mutation happend; not user-writable *)
- | BE_lret (* Local return happened; not user-writable *)
+ | BE_nondet (* nondeterminism, from $nondet$ *)
+ | BE_escape (* potential call of  $exit$ *)
+ | BE_lset (* local mutation; not user-writable *)
+ | BE_lret (* local return; not user-writable *)
 
 
 type base_effect = 
  | BE_aux of base_effect_aux * l
 
 
-type order_aux =  (* vector order specifications, of kind Order *)
+type order_aux =  (* vector order specifications, of kind $Order$ *)
  | Ord_var of kid (* variable *)
- | Ord_inc (* increasing (little-endian) *)
- | Ord_dec (* decreasing (big-endian) *)
+ | Ord_inc (* increasing *)
+ | Ord_dec (* decreasing *)
 
 
-type effect_aux =  (* effect set, of kind Effects *)
+type effect_aux =  (* effect set, of kind $Effect$ *)
  | Effect_var of kid
  | Effect_set of list base_effect (* effect set *)
 
@@ -163,11 +165,6 @@ let effect_union e1 e2 =
   end
 
 
-type kinded_id_aux =  (* optionally kind-annotated identifier *)
- | KOpt_none of kid (* identifier *)
- | KOpt_kind of kind * kid (* kind-annotated variable *)
-
-
 type n_constraint_aux =  (* constraint over kind $Nat$ *)
  | NC_fixed of nexp * nexp
  | NC_bounded_ge of nexp * nexp
@@ -175,17 +172,22 @@ type n_constraint_aux =  (* constraint over kind $Nat$ *)
  | NC_nat_set_bounded of kid * list integer
 
 
-type kinded_id = 
- | KOpt_aux of kinded_id_aux * l
+type kinded_id_aux =  (* optionally kind-annotated identifier *)
+ | KOpt_none of kid (* identifier *)
+ | KOpt_kind of kind * kid (* kind-annotated variable *)
 
 
 type n_constraint = 
  | NC_aux of n_constraint_aux * l
 
 
-type quant_item_aux =  (* Either a kinded identifier or a nexp constraint for a typquant *)
- | QI_id of kinded_id (* An optionally kinded identifier *)
- | QI_const of n_constraint (* A constraint for this type *)
+type kinded_id = 
+ | KOpt_aux of kinded_id_aux * l
+
+
+type quant_item_aux =  (* kinded identifier or $Nat$ constraint *)
+ | QI_id of kinded_id (* optionally kinded identifier *)
+ | QI_const of n_constraint (* $Nat$ constraint *)
 
 
 type quant_item = 
@@ -194,38 +196,25 @@ type quant_item =
 
 type typquant_aux =  (* type quantifiers and constraints *)
  | TypQ_tq of list quant_item
- | TypQ_no_forall (* sugar, omitting quantifier and constraints *)
-
-
-type lit_aux =  (* Literal constant *)
- | L_unit (* $() : unit$ *)
- | L_zero (* $bitzero : bit$ *)
- | L_one (* $bitone : bit$ *)
- | L_true (* $true : bool$ *)
- | L_false (* $false : bool$ *)
- | L_num of integer (* natural number constant *)
- | L_hex of string (* bit vector constant, C-style *)
- | L_bin of string (* bit vector constant, C-style *)
- | L_undef (* constant representing undefined values *)
- | L_string of string (* string constant *)
+ | TypQ_no_forall (* empty *)
 
 
 type typquant = 
  | TypQ_aux of typquant_aux * l
 
 
-type typ_aux =  (* Type expressions, of kind $Type$ *)
- | Typ_wild (* Unspecified type *)
- | Typ_id of id (* Defined type *)
- | Typ_var of kid (* Type variable *)
- | Typ_fn of typ * typ * effect (* Function type (first-order only in user code) *)
- | Typ_tup of list typ (* Tuple type *)
+type typ_aux =  (* type expressions, of kind $Type$ *)
+ | Typ_wild (* unspecified type *)
+ | Typ_id of id (* defined type *)
+ | Typ_var of kid (* type variable *)
+ | Typ_fn of typ * typ * effect (* Function (first-order only in user code) *)
+ | Typ_tup of list typ (* Tuple *)
  | Typ_app of id * list typ_arg (* type constructor application *)
 
 and typ = 
  | Typ_aux of typ_aux * l
 
-and typ_arg_aux =  (* Type constructor arguments of all kinds *)
+and typ_arg_aux =  (* type constructor arguments of all kinds *)
  | Typ_arg_nexp of nexp
  | Typ_arg_typ of typ
  | Typ_arg_order of order
@@ -235,15 +224,41 @@ and typ_arg =
  | Typ_arg_aux of typ_arg_aux * l
 
 
-type lit = 
- | L_aux of lit_aux * l
+type lit_aux =  (* literal constant *)
+ | L_unit (* $() : unit$ *)
+ | L_zero (* $bitzero : bit$ *)
+ | L_one (* $bitone : bit$ *)
+ | L_true (* $true : bool$ *)
+ | L_false (* $false : bool$ *)
+ | L_num of integer (* natural number constant *)
+ | L_hex of string (* bit vector constant, C-style *)
+ | L_bin of string (* bit vector constant, C-style *)
+ | L_string of string (* string constant *)
+ | L_undef (* undefined-value constant *)
+
+
+type index_range_aux =  (* index specification, for bitfields in register types *)
+ | BF_single of integer (* single index *)
+ | BF_range of integer * integer (* index range *)
+ | BF_concat of index_range * index_range (* concatenation of index ranges *)
+
+and index_range = 
+ | BF_aux of index_range_aux * l
 
 
 type typschm_aux =  (* type scheme *)
  | TypSchm_ts of typquant * typ
 
 
-type pat_aux 'a =  (* Pattern *)
+type lit = 
+ | L_aux of lit_aux * l
+
+
+type typschm = 
+ | TypSchm_aux of typschm_aux * l
+
+
+type pat_aux 'a =  (* pattern *)
  | P_lit of lit (* literal constant pattern *)
  | P_wild (* wildcard *)
  | P_as of (pat 'a) * id (* named pattern *)
@@ -260,207 +275,33 @@ type pat_aux 'a =  (* Pattern *)
 and pat 'a = 
  | P_aux of (pat_aux 'a) * annot 'a
 
-and fpat_aux 'a =  (* Field pattern *)
+and fpat_aux 'a =  (* field pattern *)
  | FP_Fpat of id * (pat 'a)
 
 and fpat 'a = 
  | FP_aux of (fpat_aux 'a) * annot 'a
 
 
-type typschm = 
- | TypSchm_aux of typschm_aux * l
-
-
-type reg_id_aux 'a = 
- | RI_id of id
-
-
-type exp_aux 'a =  (* Expression *)
- | E_block of list (exp 'a) (* block *)
- | E_nondet of list (exp 'a) (* nondeterminisitic block, expressions evaluate in an unspecified order, or concurrently *)
- | E_id of id (* identifier *)
- | E_lit of lit (* literal constant *)
- | E_cast of typ * (exp 'a) (* cast *)
- | E_app of id * list (exp 'a) (* function application *)
- | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *)
- | E_tuple of list (exp 'a) (* tuple *)
- | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *)
- | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *)
- | E_vector of list (exp 'a) (* vector (indexed from 0) *)
- | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *)
- | E_vector_access of (exp 'a) * (exp 'a) (* vector access *)
- | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *)
- | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *)
- | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update (with vector) *)
- | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *)
- | E_list of list (exp 'a) (* list *)
- | E_cons of (exp 'a) * (exp 'a) (* cons *)
- | E_record of (fexps 'a) (* struct *)
- | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *)
- | E_field of (exp 'a) * id (* field projection from struct *)
- | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *)
- | E_let of (letbind 'a) * (exp 'a) (* let expression *)
- | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *)
- | E_sizeof of nexp (* Expression to return the value of the nexp variable or expression at run time *)
- | E_exit of (exp 'a) (* expression to halt all current execution, potentially calling a system, trap, or interrupt handler with exp *)
- | E_return of (exp 'a) (* expression to end current function execution and return the value of exp from the function; this can be used to break out of for loops *)
- | E_assert of (exp 'a) * (exp 'a) (* expression to halt with error, when the first expression is false, reporting the optional string as an error *)
- | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
- | E_internal_exp of annot 'a (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
- | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *)
- | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *)
- | E_comment of string (* For generated unstructured comments *)
- | E_comment_struc of (exp 'a) (* For generated structured comments *)
- | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *)
- | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *)
- | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *)
-
-and exp 'a = 
- | E_aux of (exp_aux 'a) * annot 'a
-
-and lexp_aux 'a =  (* lvalue expression *)
- | LEXP_id of id (* identifier *)
- | LEXP_memory of id * list (exp 'a) (* memory write via function call *)
- | LEXP_cast of typ * id
- | LEXP_tup of list (lexp 'a) (* set multiple at a time, a check will ensure it's not memory *)
- | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *)
- | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *)
- | LEXP_field of (lexp 'a) * id (* struct field *)
-
-and lexp 'a = 
- | LEXP_aux of (lexp_aux 'a) * annot 'a
-
-and fexp_aux 'a =  (* Field-expression *)
- | FE_Fexp of id * (exp 'a)
-
-and fexp 'a = 
- | FE_aux of (fexp_aux 'a) * annot 'a
-
-and fexps_aux 'a =  (* Field-expression list *)
- | FES_Fexps of list (fexp 'a) * bool
-
-and fexps 'a = 
- | FES_aux of (fexps_aux 'a) * annot 'a
-
-and opt_default_aux 'a =  (* Optional default value for indexed vectors, to define a defualt value for any unspecified positions in a sparse map *)
- | Def_val_empty
- | Def_val_dec of (exp 'a)
-
-and opt_default 'a = 
- | Def_val_aux of (opt_default_aux 'a) * annot 'a
-
-and pexp_aux 'a =  (* Pattern match *)
- | Pat_exp of (pat 'a) * (exp 'a)
-
-and pexp 'a = 
- | Pat_aux of (pexp_aux 'a) * annot 'a
-
-and letbind_aux 'a =  (* Let binding *)
- | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* value binding, explicit type ((pat 'a) must be total) *)
- | LB_val_implicit of (pat 'a) * (exp 'a) (* value binding, implicit type ((pat 'a) must be total) *)
-
-and letbind 'a = 
- | LB_aux of (letbind_aux 'a) * annot 'a
-
-
-type reg_id 'a = 
- | RI_aux of (reg_id_aux 'a) * annot 'a
-
-
-type type_union_aux =  (* Type union constructors *)
- | Tu_id of id
- | Tu_ty_id of typ * id
-
-
-type name_scm_opt_aux =  (* Optional variable-naming-scheme specification for variables of defined type *)
+type name_scm_opt_aux =  (* optional variable naming-scheme constraint *)
  | Name_sect_none
  | Name_sect_some of string
 
 
-type effect_opt_aux =  (* Optional effect annotation for functions *)
- | Effect_opt_pure (* sugar for empty effect set *)
- | Effect_opt_effect of effect
-
-
-type funcl_aux 'a =  (* Function clause *)
- | FCL_Funcl of id * (pat 'a) * (exp 'a)
-
-
-type rec_opt_aux =  (* Optional recursive annotation for functions *)
- | Rec_nonrec (* non-recursive *)
- | Rec_rec (* recursive *)
-
-
-type tannot_opt_aux =  (* Optional type annotation for functions *)
- | Typ_annot_opt_some of typquant * typ
-
-
-type alias_spec_aux 'a =  (* Register alias expression forms. Other than where noted, each id must refer to an unaliased register of type vector *)
- | AL_subreg of (reg_id 'a) * id
- | AL_bit of (reg_id 'a) * (exp 'a)
- | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a)
- | AL_concat of (reg_id 'a) * (reg_id 'a)
-
-
-type type_union = 
- | Tu_aux of type_union_aux * l
-
-
-type index_range_aux =  (* index specification, for bitfields in register types *)
- | BF_single of integer (* single index *)
- | BF_range of integer * integer (* index range *)
- | BF_concat of index_range * index_range (* concatenation of index ranges *)
-
-and index_range = 
- | BF_aux of index_range_aux * l
+type type_union_aux =  (* type union constructors *)
+ | Tu_id of id
+ | Tu_ty_id of typ * id
 
 
 type name_scm_opt = 
  | Name_sect_aux of name_scm_opt_aux * l
 
 
-type effect_opt = 
- | Effect_opt_aux of effect_opt_aux * l
-
-
-type funcl 'a = 
- | FCL_aux of (funcl_aux 'a) * annot 'a
-
-
-type rec_opt = 
- | Rec_aux of rec_opt_aux * l
-
-
-type tannot_opt = 
- | Typ_annot_opt_aux of tannot_opt_aux * l
-
-
-type alias_spec 'a = 
- | AL_aux of (alias_spec_aux 'a) * annot 'a
-
-
-type default_spec_aux 'a =  (* Default kinding or typing assumption *)
- | DT_kind of base_kind * kid
- | DT_order of order
- | DT_typ of typschm * id
-
-
-type type_def_aux 'a =  (* Type definition body *)
- | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
- | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
- | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
- | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
- | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
-
-
-type val_spec_aux 'a =  (* Value type specification *)
- | VS_val_spec of typschm * id
- | VS_extern_no_rename of typschm * id
- | VS_extern_spec of typschm * id * string (* Specify the type and id of a function from Lem, where the string must provide an explicit path to the required function but will not be checked *)
+type type_union = 
+ | Tu_aux of type_union_aux * l
 
 
-type kind_def_aux 'a =  (* Definition body for elements of kind; many are shorthands for type\_defs *)
- | KD_nabbrev of kind * id * name_scm_opt * nexp (* nexp abbreviation *)
+type kind_def_aux 'a =  (* Definition body for elements of kind *)
+ | KD_nabbrev of kind * id * name_scm_opt * nexp (* $Nat$-expression abbreviation *)
  | KD_abbrev of kind * id * name_scm_opt * typschm (* type abbreviation *)
  | KD_record of kind * id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
  | KD_variant of kind * id * name_scm_opt * typquant * list type_union * bool (* union type definition *)
@@ -468,71 +309,20 @@ type kind_def_aux 'a =  (* Definition body for elements of kind; many are shorth
  | KD_register of kind * id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
-type scattered_def_aux 'a =  (* Function and type union definitions that can be spread across
-         a file. Each one must end in $id$ *)
- | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
- | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *)
- | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
- | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
- | SD_scattered_end of id (* scattered definition end *)
-
-
-type fundef_aux 'a =  (* Function definition *)
- | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
-
-
-type dec_spec_aux 'a =  (* Register declarations *)
- | DEC_reg of typ * id
- | DEC_alias of id * (alias_spec 'a)
- | DEC_typ_alias of typ * id * (alias_spec 'a)
-
-
-type default_spec 'a = 
- | DT_aux of (default_spec_aux 'a) * l
-
-
-type type_def 'a = 
- | TD_aux of (type_def_aux 'a) * annot 'a
-
-
-type val_spec 'a = 
- | VS_aux of (val_spec_aux 'a) * annot 'a
+type type_def_aux 'a =  (* type definition body *)
+ | TD_abbrev of id * name_scm_opt * typschm (* type abbreviation *)
+ | TD_record of id * name_scm_opt * typquant * list (typ * id) * bool (* struct type definition *)
+ | TD_variant of id * name_scm_opt * typquant * list type_union * bool (* tagged union type definition *)
+ | TD_enum of id * name_scm_opt * list id * bool (* enumeration type definition *)
+ | TD_register of id * nexp * nexp * list (index_range * id) (* register mutable bitfield type definition *)
 
 
 type kind_def 'a = 
  | KD_aux of (kind_def_aux 'a) * annot 'a
 
 
-type scattered_def 'a = 
- | SD_aux of (scattered_def_aux 'a) * annot 'a
-
-
-type fundef 'a = 
- | FD_aux of (fundef_aux 'a) * annot 'a
-
-
-type dec_spec 'a = 
- | DEC_aux of (dec_spec_aux 'a) * annot 'a
-
-
-type dec_comm 'a =  (* Top-level generated comments *)
- | DC_comm of string (* generated unstructured comment *)
- | DC_comm_struct of (def 'a) (* generated structured comment *)
-
-and def 'a =  (* Top-level definition *)
- | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *)
- | DEF_type of (type_def 'a) (* type definition *)
- | DEF_fundef of (fundef 'a) (* function definition *)
- | DEF_val of (letbind 'a) (* value definition *)
- | DEF_spec of (val_spec 'a) (* top-level type constraint *)
- | DEF_default of (default_spec 'a) (* default kind and type assumptions *)
- | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *)
- | DEF_reg_dec of (dec_spec 'a) (* register declaration *)
- | DEF_comm of (dec_comm 'a) (* generated comments *)
-
-
-type defs 'a =  (* Definition sequence *)
- | Defs of list (def 'a)
+type type_def 'a = 
+ | TD_aux of (type_def_aux 'a) * annot 'a
 
 
 let rec remove_one i l =
@@ -569,6 +359,24 @@ type ne =  (* internal numeric expressions *)
  | Ne_unary of ne
 
 
+type t =  (* Internal types *)
+ | T_id of x
+ | T_var of x
+ | T_fn of t * t * effect
+ | T_tup of list t
+ | T_app of x * t_args
+ | T_abbrev of t * t
+
+and t_arg =  (* Argument to type constructors *)
+ | T_arg_typ of t
+ | T_arg_nexp of ne
+ | T_arg_effect of effect
+ | T_arg_order of order
+
+and t_args =  (* Arguments to type constructors *)
+ | T_args of list t_arg
+
+
 type k =  (* Internal kinds *)
  | Ki_typ
  | Ki_nat
@@ -578,15 +386,6 @@ type k =  (* Internal kinds *)
  | Ki_infer (* Representing an unknown kind, inferred by context *)
 
 
-type nec =  (* Numeric expression constraints *)
- | Nec_lteq of ne * ne
- | Nec_eq of ne * ne
- | Nec_gteq of ne * ne
- | Nec_in of x * list integer
- | Nec_cond of list nec * list nec
- | Nec_branch of list nec
-
-
 type tid =  (* A type identifier or type variable *)
  | Tid_id of id
  | Tid_var of kid
@@ -597,22 +396,13 @@ type kinf =  (* Whether a kind is default or from a local binding *)
  | Kinf_def of k
 
 
-type t =  (* Internal types *)
- | T_id of x
- | T_var of x
- | T_fn of t * t * effect
- | T_tup of list t
- | T_app of x * t_args
- | T_abbrev of t * t
-
-and t_arg =  (* Argument to type constructors *)
- | T_arg_typ of t
- | T_arg_nexp of ne
- | T_arg_effect of effect
- | T_arg_order of order
-
-and t_args =  (* Arguments to type constructors *)
- | T_args of list t_arg
+type nec =  (* Numeric expression constraints *)
+ | Nec_lteq of ne * ne
+ | Nec_eq of ne * ne
+ | Nec_gteq of ne * ne
+ | Nec_in of x * list integer
+ | Nec_cond of list nec * list nec
+ | Nec_branch of list nec
 
 
 type tag =  (* Data indicating where the identifier arises and thus information necessary in compilation *)
@@ -640,26 +430,26 @@ type conformsto =  (* how much conformance does overloading need *)
  | Conformsto_parm
 
 
+type widennum = 
+ | Widennum_widen
+ | Widennum_dont
+ | Widennum_dontcare
+
+
 type widenvec = 
  | Widenvec_widen
  | Widenvec_dont
  | Widenvec_dontcare
 
 
-type widennum = 
- | Widennum_widen
- | Widennum_dont
- | Widennum_dontcare
+type widening =  (* Should we widen vector start locations, should we widen atoms and ranges *)
+ | Widening_w of widennum * widenvec
 
 
 type tinflist =  (* In place so that a list of tinfs can be referred to without the dot form *)
  | Tinfs_empty
  | Tinfs_ls of list tinf
 
-
-type widening =  (* Should we widen vector start locations, should we widen atoms and ranges *)
- | Widening_w of widennum * widenvec
-
  type definition_env =
    | DenvEmp
    | Denv of (map tid kinf) * (map (list (id*t)) tinf) * (map t (list (nat*id)))
@@ -705,10 +495,253 @@ let fresh_kid denv = Var "x" (*TODO When strings can be manipulated, this should
 
 
 
+type I = inf
+
+
 type E = env
 
 
-type I = inf
+type tannot = maybe (t * tag * list nec * effect * effect)
+
+
+
+type i_direction = 
+ | IInc
+ | IDec
+
+
+type reg_id_aux 'a = 
+ | RI_id of id
+
+
+type reg_form = 
+ | Form_Reg of id * tannot * i_direction
+ | Form_SubReg of id * reg_form * index_range
+
+
+type ctor_kind = 
+ | C_Enum of nat
+ | C_Union
+
+
+type reg_id 'a = 
+ | RI_aux of (reg_id_aux 'a) * annot 'a
+
+
+type exp_aux 'a =  (* expression *)
+ | E_block of list (exp 'a) (* sequential block *)
+ | E_nondet of list (exp 'a) (* nondeterministic block *)
+ | E_id of id (* identifier *)
+ | E_lit of lit (* literal constant *)
+ | E_cast of typ * (exp 'a) (* cast *)
+ | E_app of id * list (exp 'a) (* function application *)
+ | E_app_infix of (exp 'a) * id * (exp 'a) (* infix function application *)
+ | E_tuple of list (exp 'a) (* tuple *)
+ | E_if of (exp 'a) * (exp 'a) * (exp 'a) (* conditional *)
+ | E_for of id * (exp 'a) * (exp 'a) * (exp 'a) * order * (exp 'a) (* loop *)
+ | E_vector of list (exp 'a) (* vector (indexed from 0) *)
+ | E_vector_indexed of list (integer * (exp 'a)) * (opt_default 'a) (* vector (indexed consecutively) *)
+ | E_vector_access of (exp 'a) * (exp 'a) (* vector access *)
+ | E_vector_subrange of (exp 'a) * (exp 'a) * (exp 'a) (* subvector extraction *)
+ | E_vector_update of (exp 'a) * (exp 'a) * (exp 'a) (* vector functional update *)
+ | E_vector_update_subrange of (exp 'a) * (exp 'a) * (exp 'a) * (exp 'a) (* vector subrange update, with vector *)
+ | E_vector_append of (exp 'a) * (exp 'a) (* vector concatenation *)
+ | E_list of list (exp 'a) (* list *)
+ | E_cons of (exp 'a) * (exp 'a) (* cons *)
+ | E_record of (fexps 'a) (* struct *)
+ | E_record_update of (exp 'a) * (fexps 'a) (* functional update of struct *)
+ | E_field of (exp 'a) * id (* field projection from struct *)
+ | E_case of (exp 'a) * list (pexp 'a) (* pattern matching *)
+ | E_let of (letbind 'a) * (exp 'a) (* let expression *)
+ | E_assign of (lexp 'a) * (exp 'a) (* imperative assignment *)
+ | E_sizeof of nexp (* the value of nexp at run time *)
+ | E_return of (exp 'a) (* return (exp 'a) from current function *)
+ | E_exit of (exp 'a) (* halt all current execution *)
+ | E_assert of (exp 'a) * (exp 'a) (* halt with error (exp 'a) when not (exp 'a) *)
+ | E_internal_cast of annot 'a * (exp 'a) (* This is an internal cast, generated during type checking that will resolve into a syntactic cast after *)
+ | E_internal_exp of annot 'a (* This is an internal use for passing nexp information  to library functions, postponed for constraint solving *)
+ | E_sizeof_internal of annot 'a (* For sizeof during type checking, to replace nexp with internal n *)
+ | E_internal_exp_user of annot 'a * annot 'a (* This is like the above but the user has specified an implicit parameter for the current function *)
+ | E_comment of string (* For generated unstructured comments *)
+ | E_comment_struc of (exp 'a) (* For generated structured comments *)
+ | E_internal_let of (lexp 'a) * (exp 'a) * (exp 'a) (* This is an internal node for compilation that demonstrates the scope of a local mutable variable *)
+ | E_internal_plet of (pat 'a) * (exp 'a) * (exp 'a) (* This is an internal node, used to distinguised some introduced lets during processing from original ones *)
+ | E_internal_return of (exp 'a) (* For internal use to embed into monad definition *)
+ | E_internal_value of value (* For internal use in interpreter to wrap pre-evaluated values when returning an action *)
+
+and exp 'a = 
+ | E_aux of (exp_aux 'a) * annot 'a
+
+and value =  (* interpreter evaluated value *)
+ | V_boxref of nat * t
+ | V_lit of lit
+ | V_tuple of list value
+ | V_list of list value
+ | V_vector of nat * i_direction * list value
+ | 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
+ | V_register of reg_form
+ | V_register_alias of alias_spec tannot * tannot
+ | V_track of value * set reg_form
+
+and lexp_aux 'a =  (* lvalue expression *)
+ | LEXP_id of id (* identifier *)
+ | LEXP_memory of id * list (exp 'a) (* memory or register write via function call *)
+ | LEXP_cast of typ * id (* cast *)
+ | LEXP_tup of list (lexp 'a) (* multiple (non-memory) assignment *)
+ | LEXP_vector of (lexp 'a) * (exp 'a) (* vector element *)
+ | LEXP_vector_range of (lexp 'a) * (exp 'a) * (exp 'a) (* subvector *)
+ | LEXP_field of (lexp 'a) * id (* struct field *)
+
+and lexp 'a = 
+ | LEXP_aux of (lexp_aux 'a) * annot 'a
+
+and fexp_aux 'a =  (* field expression *)
+ | FE_Fexp of id * (exp 'a)
+
+and fexp 'a = 
+ | FE_aux of (fexp_aux 'a) * annot 'a
+
+and fexps_aux 'a =  (* field expression list *)
+ | FES_Fexps of list (fexp 'a) * bool
+
+and fexps 'a = 
+ | FES_aux of (fexps_aux 'a) * annot 'a
+
+and opt_default_aux 'a =  (* optional default value for indexed vector expressions *)
+ | Def_val_empty
+ | Def_val_dec of (exp 'a)
+
+and opt_default 'a = 
+ | Def_val_aux of (opt_default_aux 'a) * annot 'a
+
+and pexp_aux 'a =  (* pattern match *)
+ | Pat_exp of (pat 'a) * (exp 'a)
+
+and pexp 'a = 
+ | Pat_aux of (pexp_aux 'a) * annot 'a
+
+and letbind_aux 'a =  (* let binding *)
+ | LB_val_explicit of typschm * (pat 'a) * (exp 'a) (* let, explicit type ((pat 'a) must be total) *)
+ | LB_val_implicit of (pat 'a) * (exp 'a) (* let, implicit type ((pat 'a) must be total) *)
+
+and letbind 'a = 
+ | LB_aux of (letbind_aux 'a) * annot 'a
+
+and alias_spec_aux 'a =  (* register alias expression forms *)
+ | AL_subreg of (reg_id 'a) * id
+ | AL_bit of (reg_id 'a) * (exp 'a)
+ | AL_slice of (reg_id 'a) * (exp 'a) * (exp 'a)
+ | AL_concat of (reg_id 'a) * (reg_id 'a)
+
+and alias_spec 'a = 
+ | AL_aux of (alias_spec_aux 'a) * annot 'a
+
+
+type funcl_aux 'a =  (* function clause *)
+ | FCL_Funcl of id * (pat 'a) * (exp 'a)
+
+
+type rec_opt_aux =  (* optional recursive annotation for functions *)
+ | Rec_nonrec (* non-recursive *)
+ | Rec_rec (* recursive *)
+
+
+type tannot_opt_aux =  (* optional type annotation for functions *)
+ | Typ_annot_opt_some of typquant * typ
+
+
+type effect_opt_aux =  (* optional effect annotation for functions *)
+ | Effect_opt_pure (* sugar for empty effect set *)
+ | Effect_opt_effect of effect
+
+
+type funcl 'a = 
+ | FCL_aux of (funcl_aux 'a) * annot 'a
+
+
+type rec_opt = 
+ | Rec_aux of rec_opt_aux * l
+
+
+type tannot_opt = 
+ | Typ_annot_opt_aux of tannot_opt_aux * l
+
+
+type effect_opt = 
+ | Effect_opt_aux of effect_opt_aux * l
+
+
+type val_spec_aux 'a =  (* value type specification *)
+ | VS_val_spec of typschm * id (* specify the type of an upcoming definition *)
+ | VS_extern_no_rename of typschm * id (* specify the type of an external function *)
+ | VS_extern_spec of typschm * id * string (* specify the type of a function from Lem *)
+
+
+type fundef_aux 'a =  (* function definition *)
+ | FD_function of rec_opt * tannot_opt * effect_opt * list (funcl 'a)
+
+
+type scattered_def_aux 'a =  (* scattered function and union type definitions *)
+ | SD_scattered_function of rec_opt * tannot_opt * effect_opt * id (* scattered function definition header *)
+ | SD_scattered_funcl of (funcl 'a) (* scattered function definition clause *)
+ | SD_scattered_variant of id * name_scm_opt * typquant (* scattered union definition header *)
+ | SD_scattered_unioncl of id * type_union (* scattered union definition member *)
+ | SD_scattered_end of id (* scattered definition end *)
+
+
+type default_spec_aux 'a =  (* default kinding or typing assumption *)
+ | DT_order of order
+ | DT_kind of base_kind * kid
+ | DT_typ of typschm * id
+
+
+type dec_spec_aux 'a =  (* register declarations *)
+ | DEC_reg of typ * id
+ | DEC_alias of id * (alias_spec 'a)
+ | DEC_typ_alias of typ * id * (alias_spec 'a)
+
+
+type val_spec 'a = 
+ | VS_aux of (val_spec_aux 'a) * annot 'a
+
+
+type fundef 'a = 
+ | FD_aux of (fundef_aux 'a) * annot 'a
+
+
+type scattered_def 'a = 
+ | SD_aux of (scattered_def_aux 'a) * annot 'a
+
+
+type default_spec 'a = 
+ | DT_aux of (default_spec_aux 'a) * l
+
+
+type dec_spec 'a = 
+ | DEC_aux of (dec_spec_aux 'a) * annot 'a
+
+
+type dec_comm 'a =  (* top-level generated comments *)
+ | DC_comm of string (* generated unstructured comment *)
+ | DC_comm_struct of (def 'a) (* generated structured comment *)
+
+and def 'a =  (* top-level definition *)
+ | DEF_kind of (kind_def 'a) (* definition of named kind identifiers *)
+ | DEF_type of (type_def 'a) (* type definition *)
+ | DEF_fundef of (fundef 'a) (* function definition *)
+ | DEF_val of (letbind 'a) (* value definition *)
+ | DEF_spec of (val_spec 'a) (* top-level type constraint *)
+ | DEF_default of (default_spec 'a) (* default kind and type assumptions *)
+ | DEF_scattered of (scattered_def 'a) (* scattered function and type definition *)
+ | DEF_reg_dec of (dec_spec 'a) (* register declaration *)
+ | DEF_comm of (dec_comm 'a) (* generated comments *)
+
+
+type defs 'a =  (* definition sequence *)
+ | Defs of list (def 'a)
 
 
 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index f0d7dec4..69958109 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -51,13 +51,13 @@ open import Interp_ast
 open import Sail_impl_base
 open import Interp_interface
 
-val intern_reg_value : register_value -> Interp.value
-val intern_mem_value : interp_mode -> direction -> memory_value -> Interp.value
-val extern_reg_value : reg_name -> Interp.value -> register_value
-val extern_with_track: forall 'a. interp_mode -> (Interp.value -> 'a) -> Interp.value -> ('a * maybe (list reg_name))
-val extern_vector_value: Interp.value -> list byte_lifted
-val extern_mem_value :   Interp.value -> memory_value
-val extern_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name
+val intern_reg_value : register_value -> Interp_ast.value
+val intern_mem_value : interp_mode -> direction -> memory_value -> Interp_ast.value
+val extern_reg_value : reg_name -> Interp_ast.value -> register_value
+val extern_with_track: forall 'a. interp_mode -> (Interp_ast.value -> 'a) -> Interp_ast.value -> ('a * maybe (list reg_name))
+val extern_vector_value: Interp_ast.value -> list byte_lifted
+val extern_mem_value :   Interp_ast.value -> memory_value
+val extern_reg : Interp_ast.reg_form -> maybe (nat * nat) -> reg_name
 
 let make_interpreter_mode eager_eval tracking_values = 
   <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false|>;;
@@ -71,15 +71,15 @@ let make_eager_mode mode = <| internal_mode = <|mode.internal_mode with Interp.e
 let make_default_mode = fun () -> <|internal_mode = make_interpreter_mode false false|>;;
 
 let bitl_to_ibit = function 
-  | Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) 
-  | Bitl_one ->  (Interp.V_lit (L_aux L_one Interp_ast.Unknown))
-  | Bitl_undef -> (Interp.V_lit (L_aux L_undef Interp_ast.Unknown))
-  | Bitl_unknown -> Interp.V_unknown
+  | Bitl_zero -> (Interp_ast.V_lit (L_aux L_zero Interp_ast.Unknown)) 
+  | Bitl_one ->  (Interp_ast.V_lit (L_aux L_one Interp_ast.Unknown))
+  | Bitl_undef -> (Interp_ast.V_lit (L_aux L_undef Interp_ast.Unknown))
+  | Bitl_unknown -> Interp_ast.V_unknown
 end
 
 let bit_to_ibit = function
-  | Bitc_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown))
-  | Bitc_one -> (Interp.V_lit (L_aux L_one Interp_ast.Unknown))
+  | Bitc_zero -> (Interp_ast.V_lit (L_aux L_zero Interp_ast.Unknown))
+  | Bitc_one -> (Interp_ast.V_lit (L_aux L_one Interp_ast.Unknown))
 end
 
 let to_bool = function 
@@ -99,13 +99,13 @@ end
 let bitl_from_ibit b = 
     let b = Interp.detaint b in
     match b with
-    | Interp.V_lit (L_aux L_zero _) -> Bitl_zero
-    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_zero _)] -> Bitl_zero
-    | Interp.V_lit (L_aux L_one _)  -> Bitl_one
-    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_one _)] -> Bitl_one
-    | Interp.V_lit (L_aux L_undef _) -> Bitl_undef
-    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_undef _)] -> Bitl_undef
-    | Interp.V_unknown -> Bitl_unknown
+    | Interp_ast.V_lit (L_aux L_zero _) -> Bitl_zero
+    | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_zero _)] -> Bitl_zero
+    | Interp_ast.V_lit (L_aux L_one _)  -> Bitl_one
+    | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_one _)] -> Bitl_one
+    | Interp_ast.V_lit (L_aux L_undef _) -> Bitl_undef
+    | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_undef _)] -> Bitl_undef
+    | Interp_ast.V_unknown -> Bitl_unknown
     | _ -> Assert_extra.failwith ("bit_from_ibit given unexpected " ^ (Interp.string_of_value b)) end
 
 let bits_to_ibits l = List.map bit_to_ibit l
@@ -116,10 +116,10 @@ let bits_from_ibits l = List.map
   (fun b -> 
     let b = Interp.detaint b in
     match b with
-    | Interp.V_lit (L_aux L_zero _) -> Bitc_zero
-    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_zero _)] -> Bitc_zero
-    | Interp.V_lit (L_aux L_one _)  -> Bitc_one
-    | Interp.V_vector _ _ [Interp.V_lit (L_aux L_one _)] -> Bitc_one
+    | Interp_ast.V_lit (L_aux L_zero _) -> Bitc_zero
+    | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_zero _)] -> Bitc_zero
+    | Interp_ast.V_lit (L_aux L_one _)  -> Bitc_one
+    | Interp_ast.V_vector _ _ [Interp_ast.V_lit (L_aux L_one _)] -> Bitc_one
     | _ -> Assert_extra.failwith ("bits_from_ibits given unexpected " ^ (Interp.string_of_value b))
    end) l
 
@@ -138,23 +138,23 @@ let bits_to_word8 b =
   else Assert_extra.failwith "bits_to_word8 given a non-8 list or one containing ? and u"
 
 let intern_direction = function
-  | D_increasing -> Interp.IInc
-  | D_decreasing -> Interp.IDec
+  | D_increasing -> Interp_ast.IInc
+  | D_decreasing -> Interp_ast.IDec
 end
 
 let extern_direction = function
-  | Interp.IInc -> D_increasing
-  | Interp.IDec -> D_decreasing
+  | Interp_ast.IInc -> D_increasing
+  | Interp_ast.IDec -> D_decreasing
 end
 
 let intern_opcode direction (Opcode v) =
   let bits = List.concatMap (fun (Byte(bits)) -> (List.map bit_to_ibit bits)) v in
   let direction = intern_direction direction in
-  Interp.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) - 1)) direction bits
+  Interp_ast.V_vector (if Interp.is_inc(direction) then 0 else (List.length(bits) - 1)) direction bits
                    
 let intern_reg_value v = match v with
   | <| rv_bits=[b] |> -> bitl_to_ibit b
-  | _ -> Interp.V_vector v.rv_start_internal (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits)
+  | _ -> Interp_ast.V_vector v.rv_start_internal (intern_direction v.rv_dir) (bitls_to_ibits v.rv_bits)
 end
 
 let intern_mem_value mode direction v =
@@ -162,12 +162,12 @@ let intern_mem_value mode direction v =
   $> List.concatMap (fun (Byte_lifted bits) -> bitls_to_ibits bits)
   $> fun bits ->
   let direction = intern_direction direction in
-  Interp.V_vector (if Interp.is_inc direction then 0 else (List.length bits) -1) direction bits
+  Interp_ast.V_vector (if Interp.is_inc direction then 0 else (List.length bits) -1) direction bits
 
 let intern_ifield_value direction v =
   let bits = bits_to_ibits v in
   let direction = intern_direction direction in
-  Interp.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits
+  Interp_ast.V_vector (if Interp.is_inc direction then 0 else (List.length(bits) -1)) direction bits
 
 let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
   match d with
@@ -179,25 +179,25 @@ let extern_slice (d:direction) (start:nat) ((i,j):(nat*nat)) =
    end 
 
 let extern_reg r slice = match (r,slice) with
-  | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Nothing) -> 
+  | (Interp_ast.Form_Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Nothing) -> 
     Reg x (Interp.reg_start_pos r) (Interp.reg_size r) (extern_direction dir)
-  | (Interp.Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Just(i1,i2)) -> 
+  | (Interp_ast.Form_Reg (Id_aux (Id x) _) (Just(t,_,_,_,_)) dir,Just(i1,i2)) -> 
     let start = Interp.reg_start_pos r in
     let edir = extern_direction dir in
     Reg_slice x start edir (extern_slice edir start (i1, i2))
-  | (Interp.SubReg (Id_aux (Id x) _) ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_single i) _),
+  | (Interp_ast.Form_SubReg (Id_aux (Id x) _) ((Interp_ast.Form_Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_single i) _),
      Nothing) -> 
     let i = natFromInteger i in
     let start = Interp.reg_start_pos main_r in
     let edir = extern_direction dir in
     Reg_field y start edir x (extern_slice edir start (i,i))
-  | (Interp.SubReg (Id_aux (Id x) _) ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _),
+  | (Interp_ast.Form_SubReg (Id_aux (Id x) _) ((Interp_ast.Form_Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _),
      Nothing) -> 
     let start = Interp.reg_start_pos main_r in
     let edir = extern_direction dir in
     Reg_field y start edir x (extern_slice edir start (natFromInteger i,natFromInteger j))
-  | (Interp.SubReg (Id_aux (Id x) _) 
-       ((Interp.Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Just(i1,j1)) ->
+  | (Interp_ast.Form_SubReg (Id_aux (Id x) _) 
+       ((Interp_ast.Form_Reg (Id_aux (Id y) _) _ dir) as main_r) (BF_aux(BF_range i j) _), Just(i1,j1)) ->
     let start = Interp.reg_start_pos main_r in
     let edir = extern_direction dir in
     Reg_f_slice y start edir x (extern_slice edir start (natFromInteger i,natFromInteger j)) 
@@ -207,8 +207,8 @@ end
 
 let rec extern_reg_value reg_name v = 
   match v with
-    | Interp.V_track v regs -> extern_reg_value reg_name v 
-    | Interp.V_vector_sparse fst stop inc bits default ->
+    | Interp_ast.V_track v regs -> extern_reg_value reg_name v 
+    | Interp_ast.V_vector_sparse fst stop inc bits default ->
       extern_reg_value reg_name (Interp_lib.fill_in_sparse v)
     | _ ->
       let (internal_start, external_start, direction) =
@@ -226,13 +226,13 @@ let rec extern_reg_value reg_name v =
              slice_start, dir) end) in
       let bit_list = 
         (match v with 
-          | Interp.V_vector fst dir bits -> bitls_from_ibits bits
-          | Interp.V_lit (L_aux L_zero _) -> [Bitl_zero]
-          | Interp.V_lit (L_aux L_false _) -> [Bitl_zero]
-          | Interp.V_lit (L_aux L_one _) -> [Bitl_one]
-          | Interp.V_lit (L_aux L_true _) -> [Bitl_one]
-          | Interp.V_lit (L_aux L_undef _) -> [Bitl_undef]
-          | Interp.V_unknown -> [Bitl_unknown]
+          | Interp_ast.V_vector fst dir bits -> bitls_from_ibits bits
+          | Interp_ast.V_lit (L_aux L_zero _) -> [Bitl_zero]
+          | Interp_ast.V_lit (L_aux L_false _) -> [Bitl_zero]
+          | Interp_ast.V_lit (L_aux L_one _) -> [Bitl_one]
+          | Interp_ast.V_lit (L_aux L_true _) -> [Bitl_one]
+          | Interp_ast.V_lit (L_aux L_undef _) -> [Bitl_undef]
+          | Interp_ast.V_unknown -> [Bitl_unknown]
           | _ -> Assert_extra.failwith ("extern_reg_val given non externable value " ^ (Interp.string_of_value v)) end)
      in
       <| rv_bits=bit_list; 
@@ -242,7 +242,7 @@ let rec extern_reg_value reg_name v =
 end 
 
 let extern_with_track mode f = function
-  | Interp.V_track v regs ->
+  | Interp_ast.V_track v regs ->
     (f v,
      if mode.internal_mode.Interp.track_values
      then (Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList regs)))
@@ -251,13 +251,13 @@ let extern_with_track mode f = function
   end
 
 let rec extern_vector_value v = match v with
-  | Interp.V_vector _fst _inc bits ->
+  | Interp_ast.V_vector _fst _inc bits ->
     bitls_from_ibits bits
     $> to_bytes
-  | Interp.V_vector_sparse _fst _stop _inc _bits _default ->
+  | Interp_ast.V_vector_sparse _fst _stop _inc _bits _default ->
     Interp_lib.fill_in_sparse v
     $> extern_vector_value
-  | Interp.V_track v _ -> extern_vector_value v
+  | Interp_ast.V_track v _ -> extern_vector_value v
   | _ -> Assert_extra.failwith ("extern_vector_value received non-externable value " ^ (Interp.string_of_value v))
 end
 
@@ -265,19 +265,19 @@ let rec extern_mem_value v = List.reverse (extern_vector_value v)
 
 
 let rec extern_ifield_value i_name field_name v ftyp = match (v,ftyp) with
-  | (Interp.V_track v regs,_) -> extern_ifield_value i_name field_name v ftyp
-  | (Interp.V_vector fst inc bits,_) -> bits_from_ibits bits
-  | (Interp.V_vector_sparse fst stop inc bits default,_) ->
+  | (Interp_ast.V_track v regs,_) -> extern_ifield_value i_name field_name v ftyp
+  | (Interp_ast.V_vector fst inc bits,_) -> bits_from_ibits bits
+  | (Interp_ast.V_vector_sparse fst stop inc bits default,_) ->
     extern_ifield_value i_name field_name (Interp_lib.fill_in_sparse v) ftyp
-  | (Interp.V_lit (L_aux L_zero _),_) -> [Bitc_zero]
-  | (Interp.V_lit (L_aux L_false _),_) -> [Bitc_zero]
-  | (Interp.V_lit (L_aux L_one _),_) ->  [Bitc_one]
-  | (Interp.V_lit (L_aux L_true _),_) -> [Bitc_one]
-  | (Interp.V_lit (L_aux (L_num i) _),Range (Just n)) -> bit_list_of_integer n i
-  | (Interp.V_lit (L_aux (L_num i) _),Enum _ n) -> bit_list_of_integer n i
-  | (Interp.V_lit (L_aux (L_num i) _),_) -> bit_list_of_integer 64 i
-  | (Interp.V_ctor _ _ (Interp.C_Enum i) _,Enum _ n) -> bit_list_of_integer n (integerFromNat i)
-  | (Interp.V_ctor _ _ (Interp.C_Enum i) _,_) -> bit_list_of_integer 64 (integerFromNat i)
+  | (Interp_ast.V_lit (L_aux L_zero _),_) -> [Bitc_zero]
+  | (Interp_ast.V_lit (L_aux L_false _),_) -> [Bitc_zero]
+  | (Interp_ast.V_lit (L_aux L_one _),_) ->  [Bitc_one]
+  | (Interp_ast.V_lit (L_aux L_true _),_) -> [Bitc_one]
+  | (Interp_ast.V_lit (L_aux (L_num i) _),Range (Just n)) -> bit_list_of_integer n i
+  | (Interp_ast.V_lit (L_aux (L_num i) _),Enum _ n) -> bit_list_of_integer n i
+  | (Interp_ast.V_lit (L_aux (L_num i) _),_) -> bit_list_of_integer 64 i
+  | (Interp_ast.V_ctor _ _ (Interp_ast.C_Enum i) _,Enum _ n) -> bit_list_of_integer n (integerFromNat i)
+  | (Interp_ast.V_ctor _ _ (Interp_ast.C_Enum i) _,_) -> bit_list_of_integer 64 (integerFromNat i)
   | _ ->
     Assert_extra.failwith ("extern_ifield_value of " ^ i_name ^ " for field " ^ field_name
                            ^ " given non-externable " ^ (Interp.string_of_value v) ^ " ftyp is " ^ show ftyp)
@@ -351,8 +351,8 @@ let initial_instruction_state top_level main args =
 
 type interp_value_helper_mode = Ivh_translate | Ivh_decode | Ivh_unsupported | Ivh_illegal | Ivh_analysis
 type interp_value_return =
-  | Ivh_value of Interp.value
-  | Ivh_value_after_exn of Interp.value
+  | Ivh_value of Interp_ast.value
+  | Ivh_value_after_exn of Interp_ast.value
   | Ivh_error of decode_error
 
 let rec interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen thunk =
@@ -374,8 +374,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
          | Ivh_analysis -> (Ivh_value value, events_out)
          | _ ->
            (match value with
-            | Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out)
-            | Interp.V_ctor (Id_aux (Id "None") _) _ _ _ ->
+            | Interp_ast.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out)
+            | Interp_ast.V_ctor (Id_aux (Id "None") _) _ _ _ ->
               (match (ivh_mode,arg) with
                | (Ivh_decode, (Just arg)) -> (Ivh_error (Interp_interface.Not_an_instruction_error arg), events_out)
                | (Ivh_illegal, (Just arg)) -> (Ivh_error (Interp_interface.Not_an_instruction_error arg), events_out)
@@ -395,7 +395,7 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
       end
     | (Interp.Action (Interp.Fail v) stack, _, _) ->
       match (Interp.detaint v) with
-      | Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_string s) _)) ->
+      | Interp_ast.V_ctor (Id_aux (Id "Some") _) _ _ (Interp_ast.V_lit (L_aux (L_string s) _)) ->
         (Ivh_error (Interp_interface.Internal_error ("Assert failed: " ^ s)), events_out)
       | _ -> (Ivh_error (Interp_interface.Internal_error "Assert failed"), events_out) end
     | (Interp.Action (Interp.Exit exp) stack,_,_) ->
@@ -403,8 +403,8 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
         (fun _ -> Interp.resume mode (Interp.set_in_context stack exp) Nothing)
     | (Interp.Action (Interp.Read_reg r slice) stack,_,_) ->
       let rname = match r with 
-        | Interp.Reg (Id_aux (Id i) _) _ _ -> i
-        | Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i
+        | Interp_ast.Form_Reg (Id_aux (Id i) _) _ _ -> i
+        | Interp_ast.Form_SubReg (Id_aux (Id i) _) (Interp_ast.Form_Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i
         | _ -> Assert_extra.failwith "Reg not following expected structure" end in
       let err_value =
         (Ivh_error (Interp_interface.Internal_error ("Register read of "^ rname^" request in a " ^ errk_str ^ " of " ^ err_str)),
@@ -466,7 +466,7 @@ let translate_address top_level end_flag thunk_name registers address =
   let intern_val = intern_mem_value mode direction (memory_value_of_address end_flag address) in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
-  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
+  let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (address_error,events) =
     interp_to_value_helper (Just (Opcode bytes)) Ivh_translate val_str ("",[]) internal_direction
       registers [] false
@@ -489,7 +489,7 @@ end
 let value_of_instruction_param direction (name,typ,v) = 
   let vec = intern_ifield_value direction v in
   let v = match vec with
-    | Interp.V_vector start dir bits ->
+    | Interp_ast.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.Unsigned vec
@@ -500,8 +500,8 @@ let value_of_instruction_param direction (name,typ,v) =
   end in v
 
 let intern_instruction direction (name,parms) =
-  Interp.V_ctor (Interp.id_of_string name) (T_id "ast") Interp.C_Union
-    (Interp.V_tuple (List.map (value_of_instruction_param direction) parms))
+  Interp_ast.V_ctor (Interp.id_of_string name) (T_id "ast") Interp_ast.C_Union
+    (Interp_ast.V_tuple (List.map (value_of_instruction_param direction) parms))
 
 let instruction_analysis top_level end_flag thunk_name regn_to_reg_details registers instruction =
   let mode = make_mode true false in
@@ -510,7 +510,7 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
   let intern_val = intern_instruction direction instruction in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp int_mode Interp.eenv intern_val in
-  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
+  let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (analysis_or_error,events) =
     interp_to_value_helper Nothing Ivh_analysis val_str ("",[]) internal_direction
       registers [] false
@@ -523,31 +523,31 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
   match (analysis_or_error) with
   | Ivh_value analysis ->
     (match analysis with
-     | Interp.V_tuple [Interp.V_list regs1;
-                       Interp.V_list regs2;
-                       Interp.V_list regs3;
-                       Interp.V_list nias;
+     | Interp_ast.V_tuple [Interp_ast.V_list regs1;
+                       Interp_ast.V_list regs2;
+                       Interp_ast.V_list regs3;
+                       Interp_ast.V_list nias;
                        dia;
                        ik] ->
        let reg_to_reg_name v = match v with
-         | Interp.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp.V_lit (L_aux (L_string n) _)) ->
+         | Interp_ast.V_ctor (Id_aux (Id "RFull") _) _ _ (Interp_ast.V_lit (L_aux (L_string n) _)) ->
            let (start,length,direction,_) = regn_to_reg_details n Nothing in
            Reg n start length direction
-         | Interp.V_ctor (Id_aux (Id "RSlice") _) _ _
-             (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _);
-                              Interp.V_lit (L_aux (L_num s1) _);
-                              Interp.V_lit (L_aux (L_num s2) _);]) ->
+         | Interp_ast.V_ctor (Id_aux (Id "RSlice") _) _ _
+             (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _);
+                              Interp_ast.V_lit (L_aux (L_num s1) _);
+                              Interp_ast.V_lit (L_aux (L_num s2) _);]) ->
            let (start,length,direction,_) = regn_to_reg_details n Nothing in
            Reg_slice n start direction (extern_slice direction start (natFromInteger s1, natFromInteger s2))
                                        (*Note, this may need to change order depending on the direction*)
-         | Interp.V_ctor (Id_aux (Id "RSliceBit") _) _ _
-             (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _);
-                              Interp.V_lit (L_aux (L_num s) _);]) ->
+         | Interp_ast.V_ctor (Id_aux (Id "RSliceBit") _) _ _
+             (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _);
+                              Interp_ast.V_lit (L_aux (L_num s) _);]) ->
            let (start,length,direction,_) = regn_to_reg_details n Nothing in
            Reg_slice n start direction (extern_slice direction start (natFromInteger s,natFromInteger s))
-         | Interp.V_ctor (Id_aux (Id "RField") _) _ _
-             (Interp.V_tuple [Interp.V_lit (L_aux (L_string n) _);
-                              Interp.V_lit (L_aux (L_string f) _);]) ->
+         | Interp_ast.V_ctor (Id_aux (Id "RField") _) _ _
+             (Interp_ast.V_tuple [Interp_ast.V_lit (L_aux (L_string n) _);
+                              Interp_ast.V_lit (L_aux (L_string f) _);]) ->
            let (start,length,direction,span) = regn_to_reg_details n (Just f) in
            Reg_field n start direction f (extern_slice direction start span)             
          | _ -> Assert_extra.failwith "Register footprint analysis did not return an element of the specified type" end
@@ -556,23 +556,23 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
          | Just addr -> addr
          | Nothing -> failwith "get_nia encountered invalid address" end in
        let dia_to_dia = function
-         | Interp.V_ctor (Id_aux (Id "DIAFP_none") _) _ _ _ -> DIA_none
-         | Interp.V_ctor (Id_aux (Id "DIAFP_concrete") _) _ _ address ->
+         | Interp_ast.V_ctor (Id_aux (Id "DIAFP_none") _) _ _ _ -> DIA_none
+         | Interp_ast.V_ctor (Id_aux (Id "DIAFP_concrete") _) _ _ address ->
             DIA_concrete_address (get_addr address)
-         | Interp.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) 
+         | Interp_ast.V_ctor (Id_aux (Id "DIAFP_reg") _) _ _ reg -> DIA_register (reg_to_reg_name reg) 
          | _ -> failwith "Register footprint analysis did not return dia of expected type" end in
        let nia_to_nia = function
-         | Interp.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor
-         | Interp.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address ->
+         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_successor") _) _ _ _-> NIA_successor
+         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_concrete_address") _) _ _ address ->
             NIA_concrete_address (get_addr address)
-         | Interp.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR
-         | Interp.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR
-         | Interp.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg ->
+         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_LR") _) _ _ _ -> NIA_LR
+         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_CTR") _) _ _ _ -> NIA_CTR
+         | Interp_ast.V_ctor (Id_aux (Id "NIAFP_register") _) _ _ reg ->
             NIA_register (reg_to_reg_name reg)
          | _ -> failwith "Register footprint analysis did not return nia of expected type" end in
        let ik_to_ik = function
-         | Interp.V_ctor (Id_aux (Id "IK_barrier") _) _ _
-           (Interp.V_ctor (Id_aux (Id b) _) _ _ _) ->
+         | Interp_ast.V_ctor (Id_aux (Id "IK_barrier") _) _ _
+           (Interp_ast.V_ctor (Id_aux (Id b) _) _ _ _) ->
             IK_barrier (match b with
                         | "Barrier_Sync" ->   Barrier_Sync
                         | "Barrier_LwSync" -> Barrier_LwSync
@@ -587,8 +587,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
                         | "Barrier_ISB" ->    Barrier_ISB
                         | "Barrier_MIPS_SYNC" ->    Barrier_MIPS_SYNC
                         end)
-         | Interp.V_ctor (Id_aux (Id "IK_mem_read") _) _ _
-           (Interp.V_ctor (Id_aux (Id r) _) _ _ _) ->
+         | Interp_ast.V_ctor (Id_aux (Id "IK_mem_read") _) _ _
+           (Interp_ast.V_ctor (Id_aux (Id r) _) _ _ _) ->
             IK_mem_read (match r with
                          | "Read_plain" ->             Read_plain
                          | "Read_reserve" ->           Read_reserve
@@ -597,8 +597,8 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
                          | "Read_exclusive_acquire" -> Read_exclusive_acquire
                          | "Read_stream" ->            Read_stream
                          end)
-         | Interp.V_ctor (Id_aux (Id "IK_mem_write") _) _ _
-           (Interp.V_ctor (Id_aux (Id w) _) _ _ _) ->
+         | Interp_ast.V_ctor (Id_aux (Id "IK_mem_write") _) _ _
+           (Interp_ast.V_ctor (Id_aux (Id w) _) _ _ _) ->
             IK_mem_write (match w with
                          | "Write_plain" ->             Write_plain
                          | "Write_conditional" ->       Write_conditional
@@ -606,9 +606,9 @@ let instruction_analysis top_level end_flag thunk_name regn_to_reg_details regis
                          | "Write_exclusive" ->         Write_exclusive
                          | "Write_exclusive_release" -> Write_exclusive_release
                           end)
-         | Interp.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ ->
+         | Interp_ast.V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ _ ->
             IK_cond_branch
-         | Interp.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ ->
+         | Interp_ast.V_ctor (Id_aux (Id "IK_simple") _) _ _ _ ->
             IK_simple
          | _ -> failwith "Analysis returned unexpected instruction kind"
        end in
@@ -648,15 +648,15 @@ end
 let interp_value_to_instr_external top_level instr = 
   let (Context (Interp.Env _ instructions _ _ _ _ _ _) _ _ _ _ _ _ _ _ _ _) = top_level in
   match instr with
-  | Interp.V_ctor (Id_aux (Id i) _) _ _ parm ->
+  | Interp_ast.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
-        | (Interp.V_lit (L_aux L_unit _),[]) -> (name, [])
+        | (Interp_ast.V_lit (L_aux L_unit _),[]) -> (name, [])
         | (value,[(p_name,ie_typ)]) -> 
            let t = migrate_typ ie_typ in
            (name, [(p_name,t, (extern_ifield_value name p_name value t))])
-        | (Interp.V_tuple vals,parms) -> 
+        | (Interp_ast.V_tuple vals,parms) -> 
            (name, 
             (Interp_utilities.map2 (fun value (p_name,ie_typ) -> 
                  let t = migrate_typ ie_typ in
@@ -675,7 +675,7 @@ let decode_to_instruction top_level registers value : instruction_or_decode_erro
   let intern_val = intern_opcode direction value in
   let val_str = Interp.string_of_value intern_val in
   let (arg,_) = Interp.to_exp mode Interp.eenv intern_val in
-  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
+  let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   let (instr_decoded_error,events) =
     interp_to_value_helper (Just value) Ivh_decode val_str ("",[]) internal_direction registers [] false
       (fun _ -> Interp.resume 
@@ -729,7 +729,7 @@ let instr_external_to_interp_value top_level instr =
   let get_value (_,typ,v) = 
     let vec = intern_ifield_value direction v in
     match vec with
-      | Interp.V_vector start dir bits ->
+      | Interp_ast.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.Unsigned vec
@@ -740,12 +740,12 @@ let instr_external_to_interp_value top_level instr =
     end in
 
   let parmsV = match parms with
-    | [] -> Interp.V_lit (L_aux L_unit Unknown)
-    | _  -> Interp.V_tuple (List.map get_value parms)
+    | [] -> Interp_ast.V_lit (L_aux L_unit Unknown)
+    | _  -> Interp_ast.V_tuple (List.map get_value parms)
     end in
   (*This type shouldn't be hard-coded*)
-  Interp.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) 
-                (T_id "ast") Interp.C_Union parmsV
+  Interp_ast.V_ctor (Interp_ast.Id_aux (Interp_ast.Id name) Interp_ast.Unknown) 
+                (T_id "ast") Interp_ast.C_Union parmsV
 
 val instruction_to_istate : context -> instruction -> instruction_state 
 let instruction_to_istate (top_level:context) (((name, parms) as instr):instruction) : instruction_state  = 
@@ -761,7 +761,7 @@ let instruction_to_istate (top_level:context) (((name, parms) as instr):instruct
 
 let rec interp_to_outcome mode context thunk = 
   let (Context _ direction mem_reads mem_reads_tagged mem_writes mem_write_eas mem_write_vals mem_write_vals_tagged barriers excl_res spec_externs) = context in
-  let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
+  let internal_direction = if direction = D_increasing then Interp_ast.IInc else Interp_ast.IDec in
   match thunk () with
   | (Interp.Value _,lm,le) -> (Done,lm)
   | (Interp.Error l msg,lm,le) -> (Error msg,lm)
@@ -771,7 +771,7 @@ let rec interp_to_outcome mode context thunk =
         (Read_reg (extern_reg reg_form slice) 
           (fun v -> 
             let v = (intern_reg_value v) in
-            let v = if mode.internal_mode.Interp.track_values then (Interp.V_track v (Set.fromList [reg_form])) else v in 
+            let v = if mode.internal_mode.Interp.track_values then (Interp_ast.V_track v (Set.fromList [reg_form])) else v in 
             IState (Interp.add_answer_to_stack next_state v) context), lm)
       | Interp.Write_reg reg_form slice value ->
         let reg_name = extern_reg reg_form slice in
@@ -798,7 +798,7 @@ let rec interp_to_outcome mode context thunk =
               | Just bs -> Just (integer_of_byte_list bs)
               | _ -> Nothing end in
                 Read_mem_tagged read_k (Address_lifted location address_int) length tracking 
-                  (fun (tag, v) -> IState (Interp.add_answer_to_stack next_state (Interp.V_tuple ([(bitl_to_ibit tag);(intern_mem_value mode direction v)]))) context)
+                  (fun (tag, v) -> IState (Interp.add_answer_to_stack next_state (Interp_ast.V_tuple ([(bitl_to_ibit tag);(intern_mem_value mode direction v)]))) context)
             else Error ("Memory address on read is not 64 bits")
           | _ -> Error ("Memory function " ^ i ^ " not found")
         end  , lm)
@@ -844,7 +844,7 @@ let rec interp_to_outcome mode context thunk =
             | (Just (MV parmf return)) -> 
               let (value, v_tracking) = 
                 match (Interp.detaint write_val) with
-                  | Interp.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v)
+                  | Interp_ast.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v)
                   | _ -> extern_with_track mode extern_mem_value write_val end in
                let location_opt = match parmf mode address_val with
                   | Nothing -> Nothing
@@ -863,7 +863,7 @@ let rec interp_to_outcome mode context thunk =
             | (Just (MVT parmf return)) -> 
               let (value, v_tracking) = 
                 match (Interp.detaint write_val) with
-                  | Interp.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v)
+                  | Interp_ast.V_tuple[_;v] -> extern_with_track mode extern_mem_value (Interp.retaint write_val v)
                   | _ -> extern_with_track mode extern_mem_value write_val end in
                let location_opt = match parmf mode address_val with
                   | Nothing -> Nothing
@@ -913,7 +913,7 @@ let rec interp_to_outcome mode context thunk =
            (Internal (Just name) (Just (fun _ -> Interp.string_of_value value)) (IState next_state context), lm)
          | Interp.Fail value ->
            (match value with
-            | Interp.V_ctor (Id_aux (Id "Some") _) _ _ (Interp.V_lit (L_aux (L_string s) _)) -> (Fail (Just s),lm)
+            | Interp_ast.V_ctor (Id_aux (Id "Some") _) _ _ (Interp_ast.V_lit (L_aux (L_string s) _)) -> (Fail (Just s),lm)
             | _ -> (Fail Nothing,lm) end)
          | Interp.Exit e -> 
            (Escape (match e with
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 0ce7b43a..937db466 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -162,7 +162,7 @@ end
 
 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 specification = Interp_ast.defs Interp_ast.tannot (*Deem abstract*)
 type interpreter_mode = Interp.interp_mode (*Deem abstract*)
 type interp_mode = <| internal_mode: interpreter_mode |>
 val make_mode : (*eager*) bool -> (*tracking*) bool -> interp_mode
@@ -171,12 +171,12 @@ val tracking_dependencies : interp_mode -> bool
 
 
 (*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))
+type external_functions = list (string * (Interp_ast.value -> Interp_ast.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 optional_memory_transformer = interp_mode -> Interp.value -> maybe memory_value
+type memory_parameter_transformer = interp_mode -> Interp_ast.value -> (memory_value * nat * maybe (list reg_name))
+type optional_memory_transformer = interp_mode -> Interp_ast.value -> maybe memory_value
 type memory_read = MR of read_kind * memory_parameter_transformer
 type memory_reads  = list (string * memory_read)
 type memory_read_tagged  = MRT of read_kind * memory_parameter_transformer
@@ -264,7 +264,7 @@ val initial_instruction_state : context -> string -> list register_value -> inst
   (* string is a function name, list of value are the parameters to that function *)
 
 type instruction_or_decode_error =
-  | IDE_instr of instruction * Interp.value
+  | IDE_instr of instruction * Interp_ast.value
   | IDE_decode_error of decode_error
 
 (** propose to remove the following type and use the above instead *)
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index b019fb53..a51598b3 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -71,6 +71,92 @@ let pp_format_id (Id_aux(i,_)) =
   | Id(i) -> i
   | DeIid(x) -> "(deinfix " ^ x ^ ")"
 
+let lit_to_string = function
+  | L_unit -> "unit"
+  | L_zero -> "0b0"
+  | L_one -> "0b1"
+  | L_true -> "true"
+  | L_false -> "false"
+  | L_num n -> Nat_big_num.to_string n
+  | L_hex s -> "0x"^s
+  | L_bin s -> "0b"^s
+  | L_undef -> "undefined"
+  | L_string s -> "\"" ^ s ^ "\""
+;;
+
+let id_to_string = function
+  | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s
+;;
+
+let rec loc_to_string = function
+  | Unknown -> "location unknown"
+  | Int(s,_) -> s
+  | Generated l -> "Generated near " ^ loc_to_string l
+  | Range(s,fline,fchar,tline,tchar) -> 
+     if fline = tline
+     then sprintf "%s:%d:%d" s fline fchar
+     else sprintf "%s:%d:%d-%d:%d" s fline fchar tline tchar
+;;
+  
+let collapse_leading s =
+  if String.length s <= 8 then s else
+  let first_bit = s.[0] in
+  let templ = sprintf "%c...%c" first_bit first_bit in
+
+  let rec find_first_diff str cha pos =
+    if pos >= String.length str then None
+    else if str.[pos] != cha then Some pos
+    else find_first_diff str cha (pos+1)
+  in
+
+  match find_first_diff s first_bit 0 with
+  | None -> templ
+  | Some pos when pos > 4 -> templ ^ (String.sub s pos ((String.length s)- pos))
+  | _ -> s
+;;
+
+(* pp the bytes of a Bytevector as a hex value *)
+
+let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (function
+  | Interp_ast.V_lit(L_aux(L_zero, _)) -> "0"
+  | Interp_ast.V_lit(L_aux(L_one, _)) -> "1"
+  | Interp_ast.V_lit(L_aux(L_undef, _)) -> "u"
+  | Interp_ast.V_unknown -> "?"
+  | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) 
+								                                               (List.map Interp.detaint l)))
+  ;;
+
+
+let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function
+ | Interp_ast.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory)
+ | Interp_ast.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
+ | Interp_ast.V_tuple l ->
+     let repr = String.concat ", " (List.map (val_to_string_internal mem) l) in
+     sprintf "(%s)" repr
+ | Interp_ast.V_list l ->
+     let repr = String.concat "; " (List.map (val_to_string_internal mem) l) in
+     sprintf "[||%s||]" repr
+ | Interp_ast.V_vector (first_index, inc, l) ->
+     let last_index = (if (Interp_ast.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_int first_index) (string_of_int last_index)
+ | (Interp_ast.V_vector_sparse(first_index,last_index,inc,l,default) as v) -> 
+   val_to_string_internal mem (Interp_lib.fill_in_sparse v)
+ | Interp_ast.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_ast.V_ctor (id,_,_, value) ->
+     sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value)
+ | Interp_ast.V_register _ | Interp_ast.V_register_alias _ ->
+     sprintf "reg-as-value" 
+ | Interp_ast.V_unknown -> "unknown"
+ | Interp_ast.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v)
+;;
+
 (****************************************************************************
  * PPrint-based source-to-source pretty printer
 ****************************************************************************)
@@ -293,108 +379,108 @@ let doc_pat, doc_atomic_pat =
   in pat, atomic_pat
 
 let doc_exp, doc_let =
-  let rec exp env add_red show_hole_contents e = group (or_exp env add_red show_hole_contents e)
-  and or_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+  let rec exp env mem add_red show_hole_contents e = group (or_exp env mem add_red show_hole_contents e)
+  and or_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id ("|" | "||"),_) as op),r) ->
-      doc_op (doc_id op) (and_exp env add_red show_hole_contents l) (or_exp env add_red show_hole_contents r)
-  | _ -> and_exp env add_red show_hole_contents expr
-  and and_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (and_exp env mem add_red show_hole_contents l) (or_exp env mem add_red show_hole_contents r)
+  | _ -> and_exp env mem add_red show_hole_contents expr
+  and and_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id ("&" | "&&"),_) as op),r) ->
-    doc_op (doc_id op) (eq_exp env add_red show_hole_contents l) (and_exp env add_red show_hole_contents r)
-  | _ -> eq_exp env add_red show_hole_contents expr
-  and eq_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+    doc_op (doc_id op) (eq_exp env mem add_red show_hole_contents l) (and_exp env mem add_red show_hole_contents r)
+  | _ -> eq_exp env mem add_red show_hole_contents expr
+  and eq_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id (
     (* XXX this is not very consistent - is the parser bogus here? *)
       "=" | "==" | "!="
     | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u"
     | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u"
     ),_) as op),r) ->
-      doc_op (doc_id op) (eq_exp env add_red show_hole_contents l) (at_exp env add_red show_hole_contents r)
+      doc_op (doc_id op) (eq_exp env mem add_red show_hole_contents l) (at_exp env mem add_red show_hole_contents r)
   (* XXX assignment should not have the same precedence as equal etc. *)
   | E_assign(le,exp) ->
-    doc_op coloneq (doc_lexp env add_red show_hole_contents le) (at_exp env add_red show_hole_contents exp)
-  | _ -> at_exp env add_red show_hole_contents expr
-  and at_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+    doc_op coloneq (doc_lexp env mem add_red show_hole_contents le) (at_exp env mem add_red show_hole_contents exp)
+  | _ -> at_exp env mem add_red show_hole_contents expr
+  and at_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id ("@" | "^^" | "^" | "~^"),_) as op),r) ->
-      doc_op (doc_id op) (cons_exp env add_red show_hole_contents l) (at_exp env add_red show_hole_contents r)
-  | _ -> cons_exp env add_red show_hole_contents expr
-  and cons_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (cons_exp env mem add_red show_hole_contents l) (at_exp env mem add_red show_hole_contents r)
+  | _ -> cons_exp env mem add_red show_hole_contents expr
+  and cons_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_vector_append(l,r) ->
-      doc_op colon (shift_exp env add_red show_hole_contents l) (cons_exp env add_red show_hole_contents r)
+      doc_op colon (shift_exp env mem add_red show_hole_contents l) (cons_exp env mem add_red show_hole_contents r)
   | E_cons(l,r) ->
-      doc_op colon (shift_exp env add_red show_hole_contents l) (cons_exp env add_red show_hole_contents r)
-  | _ -> shift_exp env add_red show_hole_contents expr
-  and shift_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+      doc_op colon (shift_exp env mem add_red show_hole_contents l) (cons_exp env mem add_red show_hole_contents r)
+  | _ -> shift_exp env mem add_red show_hole_contents expr
+  and shift_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id (">>" | ">>>" | "<<" | "<<<"),_) as op),r) ->
-      doc_op (doc_id op) (shift_exp env add_red show_hole_contents l) (plus_exp env add_red show_hole_contents r)
-  | _ -> plus_exp env add_red show_hole_contents expr
-  and plus_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (shift_exp env mem add_red show_hole_contents l) (plus_exp env mem add_red show_hole_contents r)
+  | _ -> plus_exp env mem add_red show_hole_contents expr
+  and plus_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id ("+" | "-"| "+_s" | "-_s" ),_) as op),r) ->
-      doc_op (doc_id op) (plus_exp env add_red show_hole_contents l) (star_exp env add_red show_hole_contents r)
-  | _ -> star_exp env add_red show_hole_contents expr
-  and star_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (plus_exp env mem add_red show_hole_contents l) (star_exp env mem add_red show_hole_contents r)
+  | _ -> star_exp env mem add_red show_hole_contents expr
+  and star_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id (
       "*" | "/"
     | "div" | "quot" | "rem" | "mod" | "quot_s" | "mod_s" 
     | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) ->
-      doc_op (doc_id op) (star_exp env add_red show_hole_contents l) (starstar_exp env add_red show_hole_contents r)
-  | _ -> starstar_exp env add_red show_hole_contents expr
-  and starstar_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (star_exp env mem add_red show_hole_contents l) (starstar_exp env mem add_red show_hole_contents r)
+  | _ -> starstar_exp env mem add_red show_hole_contents expr
+  and starstar_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_app_infix(l,(Id_aux(Id "**",_) as op),r) ->
-      doc_op (doc_id op) (starstar_exp env add_red show_hole_contents l) (app_exp env add_red show_hole_contents r)
-  | E_if _ | E_for _ | E_let _ -> right_atomic_exp env add_red show_hole_contents expr
-  | _ -> app_exp env add_red show_hole_contents expr
-  and right_atomic_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+      doc_op (doc_id op) (starstar_exp env mem add_red show_hole_contents l) (app_exp env mem add_red show_hole_contents r)
+  | E_if _ | E_for _ | E_let _ -> right_atomic_exp env mem add_red show_hole_contents expr
+  | _ -> app_exp env mem add_red show_hole_contents expr
+  and right_atomic_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   (* Special case: omit "else ()" when the else branch is empty. *)
   | E_if(c,t,E_aux(E_block [], _)) ->
-      string "if" ^^ space ^^ group (exp env add_red show_hole_contents c) ^/^
-      string "then" ^^ space ^^ group (exp env add_red show_hole_contents t)
+      string "if" ^^ space ^^ group (exp env mem add_red show_hole_contents c) ^/^
+      string "then" ^^ space ^^ group (exp env mem add_red show_hole_contents t)
   | E_if(c,t,e) ->
-      string "if" ^^ space ^^ group (exp env add_red show_hole_contents c) ^/^
-      string "then" ^^ space ^^ group (exp env add_red show_hole_contents t) ^/^
-      string "else" ^^ space ^^ group (exp env add_red show_hole_contents e)
+      string "if" ^^ space ^^ group (exp env mem add_red show_hole_contents c) ^/^
+      string "then" ^^ space ^^ group (exp env mem add_red show_hole_contents t) ^/^
+      string "else" ^^ space ^^ group (exp env mem add_red show_hole_contents e)
   | E_for(id,exp1,exp2,exp3,order,exp4) ->
       string "foreach" ^^ space ^^
       group (parens (
         separate (break 1) [
           doc_id id;
-          string "from " ^^ (atomic_exp env add_red show_hole_contents exp1);
-          string "to " ^^ (atomic_exp env add_red show_hole_contents exp2);
-          string "by " ^^ (atomic_exp env add_red show_hole_contents exp3);
+          string "from " ^^ (atomic_exp env mem add_red show_hole_contents exp1);
+          string "to " ^^ (atomic_exp env mem add_red show_hole_contents exp2);
+          string "by " ^^ (atomic_exp env mem add_red show_hole_contents exp3);
           string "in " ^^ doc_ord order
         ]
       )) ^/^
-        (exp env add_red show_hole_contents exp4)
-  | E_let(leb,e) -> doc_op (string "in") (let_exp env add_red show_hole_contents leb) (exp env add_red show_hole_contents e)
-  | _ -> group (parens (exp env add_red show_hole_contents expr))
-  and app_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+        (exp env mem add_red show_hole_contents exp4)
+  | E_let(leb,e) -> doc_op (string "in") (let_exp env mem add_red show_hole_contents leb) (exp env mem add_red show_hole_contents e)
+  | _ -> group (parens (exp env mem add_red show_hole_contents expr))
+  and app_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_app(f,args) ->
-      doc_unop (doc_id f) (parens (separate_map comma (exp env add_red show_hole_contents) args))
-  | _ -> vaccess_exp env add_red show_hole_contents expr
-  and vaccess_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+      doc_unop (doc_id f) (parens (separate_map comma (exp env mem add_red show_hole_contents) args))
+  | _ -> vaccess_exp env mem add_red show_hole_contents expr
+  and vaccess_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
   | E_vector_access(v,e) ->
-    (atomic_exp env add_red show_hole_contents v) ^^ brackets (exp env add_red show_hole_contents e)
+    (atomic_exp env mem add_red show_hole_contents v) ^^ brackets (exp env mem add_red show_hole_contents e)
   | E_vector_subrange(v,e1,e2) ->
-    (atomic_exp env add_red show_hole_contents v) ^^
-    brackets (doc_op dotdot (exp env add_red show_hole_contents e1) (exp env add_red show_hole_contents e2))
-  | _ -> field_exp env add_red show_hole_contents expr
-  and field_exp env add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
-  | E_field(fexp,id) -> (atomic_exp env add_red show_hole_contents fexp) ^^ dot ^^ doc_id id
-  | _ -> atomic_exp env add_red show_hole_contents expr
-  and atomic_exp env add_red (show_hole_contents:bool) ((E_aux(e,annot)) as expr) = match e with
+    (atomic_exp env mem add_red show_hole_contents v) ^^
+    brackets (doc_op dotdot (exp env mem add_red show_hole_contents e1) (exp env mem add_red show_hole_contents e2))
+  | _ -> field_exp env mem add_red show_hole_contents expr
+  and field_exp env mem add_red show_hole_contents ((E_aux(e,_)) as expr) = match e with
+  | E_field(fexp,id) -> (atomic_exp env mem add_red show_hole_contents fexp) ^^ dot ^^ doc_id id
+  | _ -> atomic_exp env mem add_red show_hole_contents expr
+  and atomic_exp env mem add_red (show_hole_contents:bool) ((E_aux(e,annot)) as expr) = match e with
   (* Special case: an empty block is equivalent to unit, but { } is a syntactic struct *)
   | E_block [] -> string "()"
   | E_block exps ->
-      let exps_doc = separate_map (semi ^^ hardline) (exp env add_red show_hole_contents) exps in
+      let exps_doc = separate_map (semi ^^ hardline) (exp env mem add_red show_hole_contents) exps in
       surround 2 1 lbrace exps_doc rbrace
   | E_nondet exps ->
-    let exps_doc = separate_map (semi ^^ hardline) (exp env add_red show_hole_contents) exps in
+    let exps_doc = separate_map (semi ^^ hardline) (exp env mem add_red show_hole_contents) exps in
     string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace)
   | E_id id -> 
     (match id with
     | Id_aux(Id("0"), _) -> 
         (match Interp.in_lenv env id with
-          | Interp.V_unknown -> string (add_red "[_]")
+          | Interp_ast.V_unknown -> string (add_red "[_]")
           | v ->
             if show_hole_contents
             then string (add_red (Interp.string_of_value v))
@@ -403,22 +489,22 @@ let doc_exp, doc_let =
   | E_lit lit -> doc_lit lit
   | E_cast(typ,e) ->
       if !ignore_casts then
-        atomic_exp env add_red show_hole_contents e
+        atomic_exp env mem add_red show_hole_contents e
       else
-        prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp env add_red show_hole_contents e))
+        prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp env mem add_red show_hole_contents e))
   | E_internal_cast(_,e) ->
       (* XXX ignore internal casts in the interpreter *)
-      atomic_exp env add_red show_hole_contents e
+      atomic_exp env mem add_red show_hole_contents e
   | E_tuple exps ->
-      parens (separate_map comma (exp env add_red show_hole_contents) exps)
+      parens (separate_map comma (exp env mem add_red show_hole_contents) exps)
   | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
-      braces (separate_map semi_sp (doc_fexp env add_red show_hole_contents) fexps)
+      braces (separate_map semi_sp (doc_fexp env mem add_red show_hole_contents) fexps)
   | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) ->
     braces (doc_op (string "with")
-              (exp env add_red show_hole_contents e)
-              (separate_map semi_sp (doc_fexp env add_red show_hole_contents) fexps))
+              (exp env mem add_red show_hole_contents e)
+              (separate_map semi_sp (doc_fexp env mem add_red show_hole_contents) fexps))
   | E_vector exps ->
-    let default_print _ = brackets (separate_map comma (exp env add_red show_hole_contents) exps) in
+    let default_print _ = brackets (separate_map comma (exp env mem add_red show_hole_contents) exps) in
     (match exps with
      | [] -> default_print ()
      | es ->
@@ -441,28 +527,28 @@ let doc_exp, doc_let =
     let default_string = 
       (match default with
         | Def_val_empty -> string "" 
-        | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp env add_red show_hole_contents e)]) in 
-      let iexp (i,e) = doc_op equals (doc_int i) (exp env add_red show_hole_contents e) in
+        | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp env mem add_red show_hole_contents e)]) in 
+      let iexp (i,e) = doc_op equals (doc_int i) (exp env mem add_red show_hole_contents e) in
       brackets (concat [(separate_map comma iexp iexps);default_string])
   | E_vector_update(v,e1,e2) ->
     brackets (doc_op (string "with")
-                (exp env add_red show_hole_contents v)
-                (doc_op equals (atomic_exp env add_red show_hole_contents e1)
-                   (exp env add_red show_hole_contents e2)))
+                (exp env mem add_red show_hole_contents v)
+                (doc_op equals (atomic_exp env mem add_red show_hole_contents e1)
+                   (exp env mem add_red show_hole_contents e2)))
   | E_vector_update_subrange(v,e1,e2,e3) ->
       brackets (
-        doc_op (string "with") (exp env add_red show_hole_contents v)
-          (doc_op equals ((atomic_exp env add_red show_hole_contents e1) ^^ colon
-                          ^^ (atomic_exp env add_red show_hole_contents e2)) (exp env add_red show_hole_contents e3)))
+        doc_op (string "with") (exp env mem add_red show_hole_contents v)
+          (doc_op equals ((atomic_exp env mem add_red show_hole_contents e1) ^^ colon
+                          ^^ (atomic_exp env mem add_red show_hole_contents e2)) (exp env mem add_red show_hole_contents e3)))
   | E_list exps ->
-      squarebarbars (separate_map comma (exp env add_red show_hole_contents) exps)
+      squarebarbars (separate_map comma (exp env mem add_red show_hole_contents) exps)
   | E_case(e,pexps) ->
-      let opening = separate space [string "switch"; exp env add_red show_hole_contents e; lbrace] in
-      let cases = separate_map (break 1) (doc_case env add_red show_hole_contents) pexps in
+      let opening = separate space [string "switch"; exp env mem add_red show_hole_contents e; lbrace] in
+      let cases = separate_map (break 1) (doc_case env mem add_red show_hole_contents) pexps in
       surround 2 1 opening cases rbrace
-  | E_exit e -> separate space [string "exit"; exp env add_red show_hole_contents e;]
-  | E_return e -> separate space [string "return"; exp env add_red show_hole_contents e;]
-  | E_assert(e,msg) -> string "assert" ^^ parens (separate_map comma (exp env add_red show_hole_contents) [e; msg])
+  | E_exit e -> separate space [string "exit"; exp env mem add_red show_hole_contents e;]
+  | E_return e -> separate space [string "return"; exp env mem add_red show_hole_contents e;]
+  | E_assert(e,msg) -> string "assert" ^^ parens (separate_map comma (exp env mem add_red show_hole_contents) [e; msg])
   (* adding parens and loop for lower precedence *)
   | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _)
   | E_cons (_, _)|E_field (_, _)|E_assign (_, _)
@@ -484,57 +570,59 @@ let doc_exp, doc_let =
     | "*_s" | "*_si" | "*_u" | "*_ui"
     | "**"), _))
     , _) ->
-      group (parens (exp env add_red show_hole_contents expr))
+      group (parens (exp env mem add_red show_hole_contents expr))
   (* XXX fixup deinfix into infix ones *)
   | E_app_infix(l, (Id_aux((DeIid op), annot')), r) ->
     group (parens
-             (exp env add_red show_hole_contents (E_aux ((E_app_infix (l, (Id_aux(Id op, annot')), r)), annot))))
+             (exp env mem add_red show_hole_contents (E_aux ((E_app_infix (l, (Id_aux(Id op, annot')), r)), annot))))
   (* XXX default precedence for app_infix? *)
   | E_app_infix(l,op,r) ->
       failwith ("unexpected app_infix operator " ^ (pp_format_id op))
       (* doc_op (doc_id op) (exp l) (exp r) *)
   (* XXX missing case *)
-  | E_comment _ | E_comment_struc _ -> string "" 
+  | E_comment _ | E_comment_struc _ -> string ""
+  | E_internal_value v ->
+     string (val_to_string_internal mem v)
   | _-> failwith "internal expression escaped"
 
-  and let_exp env add_red show_hole_contents (LB_aux(lb,_)) = match lb with
+  and let_exp env mem add_red show_hole_contents (LB_aux(lb,_)) = match lb with
   | LB_val_explicit(ts,pat,e) ->
       prefix 2 1
         (separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals])
-        (exp env add_red show_hole_contents e)
+        (exp env mem add_red show_hole_contents e)
   | LB_val_implicit(pat,e) ->
       prefix 2 1
         (separate space [string "let"; doc_atomic_pat pat; equals])
-        (exp env add_red show_hole_contents e)
+        (exp env mem add_red show_hole_contents e)
 
-  and doc_fexp env add_red show_hole_contents (FE_aux(FE_Fexp(id,e),_)) =
-    doc_op equals (doc_id id) (exp env add_red show_hole_contents e)
+  and doc_fexp env mem add_red show_hole_contents (FE_aux(FE_Fexp(id,e),_)) =
+    doc_op equals (doc_id id) (exp env mem add_red show_hole_contents e)
 
-  and doc_case env add_red show_hole_contents (Pat_aux(Pat_exp(pat,e),_)) =
-    doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp env add_red show_hole_contents e))
+  and doc_case env mem add_red show_hole_contents (Pat_aux(Pat_exp(pat,e),_)) =
+    doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp env mem add_red show_hole_contents e))
 
   (* lexps are parsed as eq_exp - we need to duplicate the precedence
    * structure for them *)
-  and doc_lexp env add_red show_hole_contents le = app_lexp env add_red show_hole_contents le
-  and app_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with
-  | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma (exp env add_red show_hole_contents) args)
-  | _ -> vaccess_lexp env add_red show_hole_contents le
-  and vaccess_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with
+  and doc_lexp env mem add_red show_hole_contents le = app_lexp env mem add_red show_hole_contents le
+  and app_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with
+  | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma (exp env mem add_red show_hole_contents) args)
+  | _ -> vaccess_lexp env mem add_red show_hole_contents le
+  and vaccess_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with
     | LEXP_vector(v,e) ->
-      (atomic_lexp env add_red show_hole_contents v) ^^ brackets (exp env add_red show_hole_contents e)
+      (atomic_lexp env mem add_red show_hole_contents v) ^^ brackets (exp env mem add_red show_hole_contents e)
     | LEXP_vector_range(v,e1,e2) ->
-      (atomic_lexp env add_red show_hole_contents v) ^^
-      brackets ((exp env add_red show_hole_contents e1) ^^ dotdot ^^ (exp env add_red show_hole_contents e2))
-    | _ -> field_lexp env add_red show_hole_contents le
-  and field_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with
-  | LEXP_field(v,id) -> (atomic_lexp env add_red show_hole_contents v) ^^ dot ^^ doc_id id
-  | _ -> atomic_lexp env add_red show_hole_contents le
-  and atomic_lexp env add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with
+      (atomic_lexp env mem add_red show_hole_contents v) ^^
+      brackets ((exp env mem add_red show_hole_contents e1) ^^ dotdot ^^ (exp env mem add_red show_hole_contents e2))
+    | _ -> field_lexp env mem add_red show_hole_contents le
+  and field_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with
+  | LEXP_field(v,id) -> (atomic_lexp env mem add_red show_hole_contents v) ^^ dot ^^ doc_id id
+  | _ -> atomic_lexp env mem add_red show_hole_contents le
+  and atomic_lexp env mem add_red show_hole_contents ((LEXP_aux(lexp,_)) as le) = match lexp with
   | LEXP_id id -> doc_id id
   | LEXP_cast(typ,id) -> prefix 2 1 (parens (doc_typ typ)) (doc_id id)
-  | LEXP_tup(lexps) -> group (parens (separate_map comma (doc_lexp env add_red show_hole_contents) lexps))
+  | LEXP_tup(lexps) -> group (parens (separate_map comma (doc_lexp env mem add_red show_hole_contents) lexps))
   | LEXP_memory _ | LEXP_vector _ | LEXP_vector_range _
-  | LEXP_field _ -> group (parens (doc_lexp env add_red show_hole_contents le))
+  | LEXP_field _ -> group (parens (doc_lexp env mem add_red show_hole_contents le))
 
   (* expose doc_exp and doc_let *)
   in exp, let_exp
@@ -611,15 +699,15 @@ let doc_effects_opt (Effect_opt_aux(e,_)) = match e with
   | Effect_opt_pure -> string "pure"
   | Effect_opt_effect e -> doc_effects e
 
-let doc_funcl env add_red (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
-  group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp env add_red false exp))
+let doc_funcl env mem add_red (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
+  group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp env mem add_red false exp))
 
-let doc_fundef env add_red (FD_aux(FD_function(r, typa, efa, fcls),_)) =
+let doc_fundef env mem add_red (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
   | _ ->
       let sep = hardline ^^ string "and" ^^ space in
-      let clauses = separate_map sep (doc_funcl env add_red) fcls in
+      let clauses = separate_map sep (doc_funcl env mem add_red) fcls in
       separate space [string "function";
         doc_rec r ^^ doc_tannot_opt typa;
         string "effect"; doc_effects_opt efa;
@@ -629,7 +717,7 @@ let doc_dec (DEC_aux(d,_)) = match d with
   | DEC_reg(typ,id) -> separate space [string "register"; doc_atomic_typ typ; doc_id id]
   | _ -> failwith "interpreter printing out declarations unexpectedly"
 
-let doc_scattered env add_red (SD_aux (sdef, _)) = match sdef with
+let doc_scattered env mem add_red (SD_aux (sdef, _)) = match sdef with
  | SD_scattered_function (r, typa, efa, id) ->
      separate space [
        string "scattered function";
@@ -641,35 +729,35 @@ let doc_scattered env add_red (SD_aux (sdef, _)) = match sdef with
        (string "scattered typedef" ^^ space ^^ doc_id id ^^ doc_namescm ns)
        (doc_typquant tq empty)
  | SD_scattered_funcl funcl ->
-     string "function clause" ^^ space ^^ doc_funcl env add_red funcl
+     string "function clause" ^^ space ^^ doc_funcl env mem add_red funcl
  | SD_scattered_unioncl (id, tu) ->
      separate space [string "union"; doc_id id;
      string "member"; doc_type_union tu]
  | SD_scattered_end id -> string "end" ^^ space ^^ doc_id id
 
-let rec doc_def env add_red def = group (match def with
+let rec doc_def env mem add_red def = group (match def with
   | DEF_default df -> doc_default df
   | DEF_spec v_spec -> doc_spec v_spec
   | DEF_type t_def -> doc_typdef t_def
   | DEF_kind k_def -> failwith "interpreter unexpectedly printing kind def"
-  | DEF_fundef f_def -> doc_fundef env add_red f_def
-  | DEF_val lbind -> doc_let env add_red false lbind
+  | DEF_fundef f_def -> doc_fundef env mem add_red f_def
+  | DEF_val lbind -> doc_let env mem add_red false lbind
   | DEF_reg_dec dec -> doc_dec dec
-  | DEF_scattered sdef -> doc_scattered env add_red sdef
-  | DEF_comm comm_dec -> string "(*" ^^ doc_comm_dec env add_red comm_dec ^^ string "*)"
+  | DEF_scattered sdef -> doc_scattered env mem add_red sdef
+  | DEF_comm comm_dec -> string "(*" ^^ doc_comm_dec env mem add_red comm_dec ^^ string "*)"
   ) ^^ hardline
 
-and doc_comm_dec env add_red dec = match dec with
+and doc_comm_dec env mem add_red dec = match dec with
   | DC_comm s -> string s
-  | DC_comm_struct d -> doc_def env add_red d
+  | DC_comm_struct d -> doc_def env mem add_red d
                           
-let doc_defs env add_red (Defs(defs)) =
-  separate_map hardline (doc_def env add_red) defs
+let doc_defs env mem add_red (Defs(defs)) =
+  separate_map hardline (doc_def env mem add_red) defs
 
 let print ?(len=80) channel doc = ToChannel.pretty 1. len channel doc
 let to_buf ?(len=80) buf doc = ToBuffer.pretty 1. len buf doc
 
-let pp_exp env add_red show_hole_contents e =
+let pp_exp env mem add_red show_hole_contents e =
   let b = Buffer.create 20 in
-  to_buf b (doc_exp env add_red show_hole_contents e);
+  to_buf b (doc_exp env mem add_red show_hole_contents e);
   Buffer.contents b
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index f0c0d392..79a86113 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -49,60 +49,13 @@ open Interp_interface ;;
 
 open Nat_big_num ;;
 
-let lit_to_string = function
- | L_unit -> "unit"
- | L_zero -> "0b0"
- | L_one -> "0b1"
- | L_true -> "true"
- | L_false -> "false"
- | L_num n -> to_string n
- | L_hex s -> "0x"^s
- | L_bin s -> "0b"^s
- | L_undef -> "undefined"
- | L_string s -> "\"" ^ s ^ "\""
-;;
-
-let id_to_string = function
-  | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s
-;;
-
-let rec loc_to_string = function
-  | Unknown -> "location unknown"
-  | Int(s,_) -> s
-  | Generated l -> "Generated near " ^ loc_to_string l
-  | Range(s,fline,fchar,tline,tchar) -> 
-      if fline = tline
-      then sprintf "%s:%d:%d" s fline fchar
-      else sprintf "%s:%d:%d-%d:%d" s fline fchar tline tchar
-;;
-
-let collapse_leading s =
-  if String.length s <= 8 then s else
-  let first_bit = s.[0] in
-  let templ = sprintf "%c...%c" first_bit first_bit in
-
-  let rec find_first_diff str cha pos =
-    if pos >= String.length str then None
-    else if str.[pos] != cha then Some pos
-    else find_first_diff str cha (pos+1)
-  in
-
-  match find_first_diff s first_bit 0 with
-  | None -> templ
-  | Some pos when pos > 4 -> templ ^ (String.sub s pos ((String.length s)- pos))
-  | _ -> s
-;;
+let val_to_string_internal = Pretty_interp.val_to_string_internal ;;
+let lit_to_string = Pretty_interp.lit_to_string ;;
+let id_to_string = Pretty_interp.id_to_string ;;
+let loc_to_string = Pretty_interp.loc_to_string ;;
+let bitvec_to_string = Pretty_interp.bitvec_to_string ;;
+let collapse_leading = Pretty_interp.collapse_leading ;;
 
-let bitvec_to_string l = "0b" ^ collapse_leading (String.concat "" (List.map (function
-  | Interp.V_lit(L_aux(L_zero, _)) -> "0"
-  | Interp.V_lit(L_aux(L_one, _)) -> "1"
-  | Interp.V_lit(L_aux(L_undef, _)) -> "u"
-  | Interp.V_unknown -> "?"
-  | v -> (Printf.printf "bitvec found a non bit %s%!\n" (Interp.string_of_value v));assert false) 
-								      (List.map Interp.detaint l)))
-;;
-
-(* pp the bytes of a Bytevector as a hex value *)
 
 type bits_lifted_homogenous = 
   | Bitslh_concrete of bit list
@@ -322,36 +275,6 @@ let reg_name_to_string = function
 
 let dependencies_to_string dependencies = String.concat ", " (List.map reg_name_to_string dependencies)
 
-let rec val_to_string_internal ((Interp.LMem (_,_,memory,_)) as mem) = function
- | Interp.V_boxref(n, t) -> val_to_string_internal mem (Pmap.find n memory)
- | Interp.V_lit (L_aux(l,_)) -> sprintf "%s" (lit_to_string l)
- | Interp.V_tuple l ->
-     let repr = String.concat ", " (List.map (val_to_string_internal mem) l) in
-     sprintf "(%s)" repr
- | Interp.V_list l ->
-     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 = (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_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) ->
-     sprintf "%s %s" (id_to_string id) (val_to_string_internal mem value)
- | Interp.V_register _ | Interp.V_register_alias _ ->
-     sprintf "reg-as-value" 
- | Interp.V_unknown -> "unknown"
- | Interp.V_track(v,rs) -> (*"tainted by {" ^ (Interp_utilities.list_to_string Interp.string_of_reg_form "," rs) ^ "} --" ^ *) (val_to_string_internal mem v)
-;;
-
 let rec top_frame_exp_state = function
   | Interp.Top -> raise (Invalid_argument "top_frame_exp")
   | Interp.Hole_frame(_, e, _, env, mem, Interp.Top)
@@ -485,27 +408,27 @@ let yellow = color true 3
 let blue = color true 4
 let grey = color false 7
 
-let exp_to_string env show_hole_value e = Pretty_interp.pp_exp env red show_hole_value e
+let exp_to_string env mem show_hole_value e = Pretty_interp.pp_exp env mem red show_hole_value e
 
 let get_loc (E_aux(_, (l, (_ : tannot)))) = loc_to_string l
-let print_exp printer env show_hole_value e =
-  printer ((get_loc e) ^ ": " ^ (Pretty_interp.pp_exp env red show_hole_value e) ^ "\n")
+let print_exp printer env mem show_hole_value e =
+  printer ((get_loc e) ^ ": " ^ (Pretty_interp.pp_exp env mem red show_hole_value e) ^ "\n")
 
 let instruction_state_to_string (IState(stack, _)) =
-  List.fold_right (fun (e,(env,mem)) es -> (exp_to_string env true e) ^ "\n" ^ es) (compact_stack stack) ""
+  List.fold_right (fun (e,(env,mem)) es -> (exp_to_string env mem true e) ^ "\n" ^ es) (compact_stack stack) ""
 
 let top_instruction_state_to_string (IState(stack,_)) = 
-  let (exp,(env,_)) = top_frame_exp_state stack in exp_to_string env true exp
+  let (exp,(env,mem)) = top_frame_exp_state stack in exp_to_string env mem true exp
 
 let instruction_stack_to_string (IState(stack,_)) =
   let rec stack_to_string = function
       Interp.Top -> ""
     | Interp.Hole_frame(_,e,_,env,mem,Interp.Top)
     | Interp.Thunk_frame(e,_,env,mem,Interp.Top) ->
-      exp_to_string env true e
+      exp_to_string env mem true e
     | Interp.Hole_frame(_,e,_,env,mem,s) 
     | Interp.Thunk_frame(e,_,env,mem,s) ->
-      (exp_to_string env false e) ^ "\n----------------------------------------------------------\n" ^
+      (exp_to_string env mem false e) ^ "\n----------------------------------------------------------\n" ^
       (stack_to_string s)
   in
   match stack with
@@ -536,7 +459,7 @@ let instr_parm_to_string (name, typ, value) =
     | Other -> "Unrepresentable external value"
     | _ -> let intern_v = (Interp_inter_imp.intern_ifield_value D_increasing value) in
 	      match Interp_lib.to_num Interp_lib.Unsigned intern_v with
-		| Interp.V_lit (L_aux(L_num n, _)) -> to_string n
+		| Interp_ast.V_lit (L_aux(L_num n, _)) -> to_string n
 		| _ -> ifield_to_string value
 
 let rec instr_parms_to_string ps = 
@@ -551,12 +474,12 @@ let instruction_to_string (name, parms) =
   ((*pad 5*) (String.lowercase name)) ^ " " ^ instr_parms_to_string parms 
 
 let print_backtrace_compact printer (IState(stack,_)) =
-  List.iter (fun (e,(env,mem)) -> print_exp printer env true e) (compact_stack stack)
+  List.iter (fun (e,(env,mem)) -> print_exp printer env mem true e) (compact_stack stack)
 
 let print_stack printer is = printer (instruction_stack_to_string is)
 
 let print_continuation printer (IState(stack,_)) = 
-  let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env true e
+  let (e,(env,mem)) = top_frame_exp_state stack in print_exp printer env mem true e
 let print_instruction printer instr = printer (instruction_to_string instr)
 
 let pp_instruction_state state () =
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index f629a307..85744d61 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -10,7 +10,7 @@ val loc_to_string : l -> string
 val get_loc : tannot exp -> string
 (*interp_interface.value to string*)
 val reg_value_to_string : register_value -> string
-val val_to_string_internal : Interp.lmem -> Interp.value -> string
+val val_to_string_internal : Interp.lmem -> Interp_ast.value -> string
 
 (*(*Force all representations to hex strings instead of a mixture of hex and binary strings*)
 val val_to_hex_string : value0 -> string*)
@@ -19,7 +19,7 @@ val reg_name_to_string : reg_name -> string
 (* format the register dependencies *)
 val dependencies_to_string : reg_name list -> string
 (* formats an expression, using interp_pretty *)
-val exp_to_string : Interp.lenv -> bool -> tannot exp -> string
+val exp_to_string : Interp.lenv -> Interp.lmem -> bool -> tannot exp -> string
 
 (* Functions to set the color of parts of the output *)
 type ppmode = 
@@ -55,7 +55,7 @@ val local_variables_to_string : instruction_state -> string
 val instruction_to_string : instruction -> string
 
 (*Functions to take a print function and cause a print event for the above functions *)
-val print_exp : (string-> unit) -> Interp.lenv -> bool -> tannot exp -> unit 
+val print_exp : (string-> unit) -> Interp.lenv -> Interp.lmem -> bool -> tannot exp -> unit 
 val print_backtrace_compact : (string -> unit) -> instruction_state -> unit
 val print_continuation : (string -> unit) -> instruction_state -> unit
 val print_instruction : (string -> unit) -> instruction -> unit
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index d6f6e30c..602efad3 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -339,7 +339,7 @@ let run
         let (top_exp,(top_env,top_mem)) = top_frame_exp_state stack in
         let loc = get_loc (compact_exp top_exp) in
         if mode = Step || force then begin
-          interactf "%s\n" (Pretty_interp.pp_exp top_env Printing_functions.red true top_exp);
+          interactf "%s\n" (Pretty_interp.pp_exp top_env top_mem Printing_functions.red true top_exp);
           interact mode env' state
         end else
           mode in
@@ -470,7 +470,7 @@ let run
   let (IState(instr_state,context)) = istate in
   let (top_exp,(top_env,top_mem)) = top_frame_exp_state instr_state in
   interactf "%s: %s %s\n" (grey name) (blue "evaluate") 
-    (Pretty_interp.pp_exp top_env Printing_functions.red true top_exp);
+    (Pretty_interp.pp_exp top_env top_mem Printing_functions.red true top_exp);
   try
     Printexc.record_backtrace true;
     loop mode (reg, mem,tagmem) (Interp_inter_imp.interp0 imode istate)