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

1 files changed, 121 insertions, 121 deletions

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