make outcome_s contain the instruction state pretty print rather than the instruction state, factor out interpreter/shallow embedding value conversion

9 files changed, 581 insertions, 574 deletions

diff --git a/src/gen_lib/deep_shallow_convert.lem b/src/gen_lib/deep_shallow_convert.lem
new file mode 100644
index 00000000..aa16f069
--- /dev/null
+++ b/src/gen_lib/deep_shallow_convert.lem
@@ -0,0 +1,526 @@
+open import Pervasives_extra
+open import Sail_impl_base
+open import Interp
+open import Interp_ast
+open import Sail_values
+
+
+class (ToFromInterpValue 'a)
+  val toInterpValue : 'a -> Interp.value
+  val fromInterpValue : Interp.value -> 'a
+end
+
+let toInterValueBool = function
+  | true -> Interp.V_lit (L_aux (L_one) Unknown)
+  | false -> Interp.V_lit (L_aux (L_zero) Unknown)
+end
+let rec fromInterpValueBool v = match v with
+  | Interp.V_lit (L_aux (L_true) _)  -> true
+  | Interp.V_lit (L_aux (L_false) _) -> false
+  | Interp.V_lit (L_aux (L_one) _)  -> true
+  | Interp.V_lit (L_aux (L_zero) _) -> false
+  | Interp.V_tuple [v] -> fromInterpValueBool v
+  | v -> failwith ("fromInterpValue bool: unexpected value. " ^
+                     Interp.debug_print_value v)
+end
+instance (ToFromInterpValue bool)
+  let toInterpValue = toInterValueBool
+  let fromInterpValue = fromInterpValueBool
+end
+
+
+let toInterpValueUnit () = Interp.V_lit (L_aux (L_unit) Unknown)
+let rec fromInterpValueUnit v = match v with
+  | Interp.V_lit (L_aux (L_unit) _) -> ()
+  | Interp.V_tuple [v] -> fromInterpValueUnit v
+  | v -> failwith ("fromInterpValue unit: unexpected value. " ^
+                     Interp.debug_print_value v)
+end
+instance (ToFromInterpValue unit)
+  let toInterpValue = toInterpValueUnit
+  let fromInterpValue = fromInterpValueUnit
+end
+
+
+let toInterpValueInteger i = V_lit (L_aux (L_num i) Unknown)
+let rec fromInterpValueInteger v = match v with
+  | Interp.V_lit (L_aux (L_num i) _) -> i
+  | Interp.V_tuple [v] -> fromInterpValueInteger v
+  | v -> failwith ("fromInterpValue integer: unexpected value. " ^
+                     Interp.debug_print_value v)
+end
+instance (ToFromInterpValue integer)
+  let toInterpValue = toInterpValueInteger
+  let fromInterpValue = fromInterpValueInteger
+end
+
+
+let toInterpValueString s = V_lit (L_aux (L_string s) Unknown)
+let rec fromInterpValueString v = match v with
+  | Interp.V_lit (L_aux (L_string s) _) -> s
+  | Interp.V_tuple [v] -> fromInterpValueString v
+  | v -> failwith ("fromInterpValue integer: unexpected value. " ^
+                     Interp.debug_print_value v)
+end
+instance (ToFromInterpValue string)
+  let toInterpValue = toInterpValueString
+  let fromInterpValue = fromInterpValueString
+end
+
+
+let toInterpValueBitU = function
+  | I     -> Interp.V_lit (L_aux (L_one) Unknown)
+  | O     -> Interp.V_lit (L_aux (L_zero) Unknown)
+  | Undef -> Interp.V_lit (L_aux (L_undef) Unknown)
+end
+let rec fromInterpValueBitU v = match v with
+  | Interp.V_lit (L_aux (L_one) _)   -> I
+  | Interp.V_lit (L_aux (L_zero) _)  -> O
+  | Interp.V_lit (L_aux (L_undef) _) -> Undef
+  | Interp.V_lit (L_aux (L_true) _)   -> I
+  | Interp.V_lit (L_aux (L_false) _)  -> O
+  | Interp.V_tuple [v] -> fromInterpValueBitU v
+  | v -> failwith ("fromInterpValue bitU: unexpected value. " ^
+                     Interp.debug_print_value v)
+end
+instance (ToFromInterpValue bitU)
+  let toInterpValue = toInterpValueBitU
+  let fromInterpValue = fromInterpValueBitU
+end
+
+
+let tuple2ToInterpValue (a,b) =
+  V_tuple [toInterpValue a;toInterpValue b]
+let rec tuple2FromInterpValue v = match v with
+  | V_tuple [a;b] -> (fromInterpValue a,fromInterpValue b)
+  | V_tuple [v] -> tuple2FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b. ToFromInterpValue 'a, ToFromInterpValue 'b => (ToFromInterpValue ('a * 'b))
+  let toInterpValue = tuple2ToInterpValue
+  let fromInterpValue = tuple2FromInterpValue
+end
+
+
+let tuple3ToInterpValue (a,b,c) =
+  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c]
+let rec tuple3FromInterpValue v = match v with
+  | V_tuple [a;b;c] -> (fromInterpValue a,fromInterpValue b,fromInterpValue c)
+  | V_tuple [v] -> tuple3FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b*c: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b 'c. ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c =>
+    (ToFromInterpValue ('a * 'b * 'c))
+  let toInterpValue = tuple3ToInterpValue
+  let fromInterpValue = tuple3FromInterpValue
+end
+
+
+let tuple4ToInterpValue (a,b,c,d) =
+  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d]
+let rec tuple4FromInterpValue v = match v with
+  | V_tuple [a;b;c;d] -> (fromInterpValue a,fromInterpValue b,
+                          fromInterpValue c,fromInterpValue d)
+  | V_tuple [v] -> tuple4FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b*c*d: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b 'c 'd. ToFromInterpValue 'a, ToFromInterpValue 'b,
+                             ToFromInterpValue 'c, ToFromInterpValue 'd =>
+    (ToFromInterpValue ('a * 'b * 'c * 'd))
+  let toInterpValue = tuple4ToInterpValue
+  let fromInterpValue = tuple4FromInterpValue
+end
+
+
+let tuple5ToInterpValue (a,b,c,d,e) =
+  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;toInterpValue e]
+let rec tuple5FromInterpValue v = match v with
+  | V_tuple [a;b;c;d;e] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e)
+  | V_tuple [v] -> tuple5FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b*c*d*e: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b 'c 'd 'e.
+    ToFromInterpValue 'a, ToFromInterpValue 'b,
+    ToFromInterpValue 'c, ToFromInterpValue 'd,
+    ToFromInterpValue 'e =>
+    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e))
+  let toInterpValue = tuple5ToInterpValue
+  let fromInterpValue = tuple5FromInterpValue
+end
+
+
+let tuple6ToInterpValue (a,b,c,d,e,f) =
+  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
+           toInterpValue e;toInterpValue f]
+let rec tuple6FromInterpValue v = match v with
+  | V_tuple [a;b;c;d;e;f] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e,fromInterpValue f)
+  | V_tuple [v] -> tuple6FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b*c*d*e*f: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b 'c 'd 'e 'f.
+    ToFromInterpValue 'a, ToFromInterpValue 'b,
+    ToFromInterpValue 'c, ToFromInterpValue 'd,
+    ToFromInterpValue 'e, ToFromInterpValue 'f =>
+    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f))
+  let toInterpValue = tuple6ToInterpValue
+  let fromInterpValue = tuple6FromInterpValue
+end
+
+
+let tuple7ToInterpValue (a,b,c,d,e,f,g) =
+  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
+           toInterpValue e;toInterpValue f;toInterpValue g]
+let rec tuple7FromInterpValue v = match v with
+  | V_tuple [a;b;c;d;e;f;g] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e,fromInterpValue f,
+      fromInterpValue g)
+  | V_tuple [v] -> tuple7FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b 'c 'd 'e 'f 'g.
+    ToFromInterpValue 'a, ToFromInterpValue 'b,
+    ToFromInterpValue 'c, ToFromInterpValue 'd,
+    ToFromInterpValue 'e, ToFromInterpValue 'f,
+    ToFromInterpValue 'g =>
+    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g))
+  let toInterpValue = tuple7ToInterpValue
+  let fromInterpValue = tuple7FromInterpValue
+end
+
+
+let tuple8ToInterpValue (a,b,c,d,e,f,g,h) =
+  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
+           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h]
+let rec tuple8FromInterpValue v = match v with
+  | V_tuple [a;b;c;d;e;f;g;h] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e,fromInterpValue f,
+      fromInterpValue g,fromInterpValue h)
+  | V_tuple [v] -> tuple8FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b 'c 'd 'e 'f 'g 'h.
+    ToFromInterpValue 'a, ToFromInterpValue 'b,
+    ToFromInterpValue 'c, ToFromInterpValue 'd,
+    ToFromInterpValue 'e, ToFromInterpValue 'f,
+    ToFromInterpValue 'g, ToFromInterpValue 'h =>
+    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h))
+  let toInterpValue = tuple8ToInterpValue
+  let fromInterpValue = tuple8FromInterpValue
+end
+
+
+let tuple9ToInterpValue (a,b,c,d,e,f,g,h,i) =
+  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
+           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
+           toInterpValue i]
+let rec tuple9FromInterpValue v = match v with
+  | V_tuple [a;b;c;d;e;f;g;h;i] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e,fromInterpValue f,
+      fromInterpValue g,fromInterpValue h,fromInterpValue i)
+  | V_tuple [v] -> tuple9FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i.
+    ToFromInterpValue 'a, ToFromInterpValue 'b,
+    ToFromInterpValue 'c, ToFromInterpValue 'd,
+    ToFromInterpValue 'e, ToFromInterpValue 'f,
+    ToFromInterpValue 'g, ToFromInterpValue 'h,
+    ToFromInterpValue 'i =>
+    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i))
+  let toInterpValue = tuple9ToInterpValue
+  let fromInterpValue = tuple9FromInterpValue
+end
+
+
+let tuple10ToInterpValue (a,b,c,d,e,f,g,h,i,j) =
+  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
+           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
+           toInterpValue i;toInterpValue j;]
+let rec tuple10FromInterpValue v = match v with
+  | V_tuple [a;b;c;d;e;f;g;h;i;j] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e,fromInterpValue f,
+      fromInterpValue g,fromInterpValue h,fromInterpValue i,
+      fromInterpValue j)
+  | V_tuple [v] -> tuple10FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j.
+    ToFromInterpValue 'a, ToFromInterpValue 'b,
+    ToFromInterpValue 'c, ToFromInterpValue 'd,
+    ToFromInterpValue 'e, ToFromInterpValue 'f,
+    ToFromInterpValue 'g, ToFromInterpValue 'h,
+    ToFromInterpValue 'i, ToFromInterpValue 'j =>
+    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j))
+  let toInterpValue = tuple10ToInterpValue
+  let fromInterpValue = tuple10FromInterpValue
+end
+
+
+let tuple11ToInterpValue (a,b,c,d,e,f,g,h,i,j,k) =
+  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
+           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
+           toInterpValue i;toInterpValue j;toInterpValue k;]
+let rec tuple11FromInterpValue v = match v with
+  | V_tuple [a;b;c;d;e;f;g;h;i;j;k] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e,fromInterpValue f,
+      fromInterpValue g,fromInterpValue h,fromInterpValue i,
+      fromInterpValue j,fromInterpValue k)
+  | V_tuple [v] -> tuple11FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j*k: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k.
+    ToFromInterpValue 'a, ToFromInterpValue 'b,
+    ToFromInterpValue 'c, ToFromInterpValue 'd,
+    ToFromInterpValue 'e, ToFromInterpValue 'f,
+    ToFromInterpValue 'g, ToFromInterpValue 'h,
+    ToFromInterpValue 'i, ToFromInterpValue 'j,
+    ToFromInterpValue 'k =>
+    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k))
+  let toInterpValue = tuple11ToInterpValue
+  let fromInterpValue = tuple11FromInterpValue
+end
+
+
+let tuple12ToInterpValue (a,b,c,d,e,f,g,h,i,j,k,l) =
+  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
+           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
+           toInterpValue i;toInterpValue j;toInterpValue k;toInterpValue l;]
+let rec tuple12FromInterpValue v = match v with
+  | V_tuple [a;b;c;d;e;f;g;h;i;j;k;l] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e,fromInterpValue f,
+      fromInterpValue g,fromInterpValue h,fromInterpValue i,
+      fromInterpValue j,fromInterpValue k,fromInterpValue l)
+  | V_tuple [v] -> tuple12FromInterpValue v
+  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j*k*l: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l.
+    ToFromInterpValue 'a, ToFromInterpValue 'b,
+    ToFromInterpValue 'c, ToFromInterpValue 'd,
+    ToFromInterpValue 'e, ToFromInterpValue 'f,
+    ToFromInterpValue 'g, ToFromInterpValue 'h,
+    ToFromInterpValue 'i, ToFromInterpValue 'j,
+    ToFromInterpValue 'k, ToFromInterpValue 'l =>
+    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l))
+  let toInterpValue = tuple12ToInterpValue
+  let fromInterpValue = tuple12FromInterpValue
+end
+
+
+let listToInterpValue l = V_list (List.map toInterpValue l)
+let rec listFromInterpValue v = match v with
+  | V_list l -> List.map fromInterpValue l
+  | V_tuple [v] -> listFromInterpValue v
+  | v -> failwith ("fromInterpValue list 'a: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (list 'a))
+  let toInterpValue = listToInterpValue
+  let fromInterpValue = listFromInterpValue
+end
+
+
+let vectorToInterpValue (Vector vs start direction) =
+  V_vector (natFromInteger start) (if direction then IInc else IDec) (List.map toInterpValue vs)
+let rec vectorFromInterpValue v = match v with
+  | V_vector start direction vs ->
+     Vector (List.map fromInterpValue vs) (integerFromNat start)
+            (match direction with | IInc -> true | IDec -> false end)
+  | V_vector_sparse start length direction valuemap defaultval ->
+     make_indexed_vector
+       (List.map (fun (i,v) -> (integerFromNat i,fromInterpValue v)) valuemap)
+       (fromInterpValue defaultval)
+       (integerFromNat start) (integerFromNat length)
+       (match direction with | IInc -> true | IDec -> false end)
+  | V_tuple [v] -> vectorFromInterpValue v
+  | v -> failwith ("fromInterpValue vector 'a: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (vector 'a))
+  let toInterpValue = vectorToInterpValue
+  let fromInterpValue = vectorFromInterpValue
+end
+
+(* Here the type information is not accurate: instead of T_id "option" it should
+   be T_app (T_id "option") (...), but temporarily we'll do it like this. The
+   same thing has to be fixed in pretty_print.ml when we're generating the
+   type-class instances. *)
+let maybeToInterpValue = function
+  | Nothing -> V_ctor (Id_aux (Id "None") Unknown) (T_id "option") C_Union (V_lit (L_aux L_unit Unknown))
+  | Just a  -> V_ctor (Id_aux (Id "Some") Unknown) (T_id "option") C_Union (toInterpValue a)
+  end
+let rec maybeFromInterpValue v = match v with
+  | V_ctor (Id_aux (Id "None") _) _ _ _ -> Nothing
+  | V_ctor (Id_aux (Id "Some") _) _ _ v -> Just (fromInterpValue v)
+  | V_tuple [v] -> maybeFromInterpValue v
+  | v -> failwith ("fromInterpValue maybe 'a: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+
+instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a))
+  let toInterpValue = maybeToInterpValue
+  let fromInterpValue = maybeFromInterpValue
+end
+
+
+module SI = Interp
+module SIA = Interp_ast
+
+
+let read_kindToInterpValue = function
+  | Read_plain -> V_ctor (Id_aux (Id "Read_plain") Unknown) (T_id "read_kind") (C_Enum 0) (toInterpValue ())
+  | Read_tag -> V_ctor (Id_aux (Id "Read_tag") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ())
+  | Read_tag_reserve -> V_ctor (Id_aux (Id "Read_tag_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ())
+  | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ())
+  | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ())
+  | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ())
+  | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ())
+  | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ())
+  end
+let rec read_kindFromInterpValue v = match v with
+  | V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain
+  | V_ctor (Id_aux (Id "Read_tag") _) _ _ v -> Read_tag
+  | V_ctor (Id_aux (Id "Read_tag_reserve") _) _ _ v -> Read_tag_reserve
+  | V_ctor (Id_aux (Id "Read_reserve") _) _ _ v -> Read_reserve
+  | V_ctor (Id_aux (Id "Read_acquire") _) _ _ v -> Read_acquire
+  | V_ctor (Id_aux (Id "Read_exclusive") _) _ _ v -> Read_exclusive
+  | V_ctor (Id_aux (Id "Read_exclusive_acquire") _) _ _ v -> Read_exclusive_acquire
+  | V_ctor (Id_aux (Id "Read_stream") _) _ _ v -> Read_stream
+  | V_tuple [v] -> read_kindFromInterpValue v
+  | v -> failwith ("fromInterpValue read_kind: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance (ToFromInterpValue read_kind)
+  let toInterpValue = read_kindToInterpValue
+  let fromInterpValue = read_kindFromInterpValue
+end
+
+
+let write_kindToInterpValue = function
+  | Write_plain -> V_ctor (Id_aux (Id "Write_plain") Unknown) (T_id "write_kind") (C_Enum 0) (toInterpValue ())
+  | Write_tag -> V_ctor (Id_aux (Id "Write_tag") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ())
+  | Write_tag_conditional -> V_ctor (Id_aux (Id "Write_tag_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ())
+  | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ())
+  | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ())
+  | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ())
+  | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ())
+  end
+let rec write_kindFromInterpValue v = match v with
+  | V_ctor (Id_aux (Id "Write_plain") _) _ _ v -> Write_plain
+  | V_ctor (Id_aux (Id "Write_tag") _) _ _ v -> Write_tag
+  | V_ctor (Id_aux (Id "Write_tag_conditional") _) _ _ v -> Write_tag_conditional
+  | V_ctor (Id_aux (Id "Write_conditional") _) _ _ v -> Write_conditional
+  | V_ctor (Id_aux (Id "Write_release") _) _ _ v -> Write_release
+  | V_ctor (Id_aux (Id "Write_exclusive") _) _ _ v -> Write_exclusive
+  | V_ctor (Id_aux (Id "Write_exclusive_release") _) _ _ v -> Write_exclusive_release
+  | V_tuple [v] -> write_kindFromInterpValue v
+  | v -> failwith ("fromInterpValue write_kind: unexpected value " ^
+                     Interp.debug_print_value v)
+  end
+instance (ToFromInterpValue write_kind)
+  let toInterpValue = write_kindToInterpValue
+  let fromInterpValue = write_kindFromInterpValue
+end
+
+
+let barrier_kindToInterpValue = function
+  | Barrier_Sync -> V_ctor (Id_aux (Id "Barrier_Sync") Unknown) (T_id "barrier_kind") (C_Enum 0) (toInterpValue ())
+  | Barrier_LwSync -> V_ctor (Id_aux (Id "Barrier_LwSync") Unknown) (T_id "barrier_kind") (C_Enum 1) (toInterpValue ())
+  | Barrier_Eieio -> V_ctor (Id_aux (Id "Barrier_Eieio") Unknown) (T_id "barrier_kind") (C_Enum 2) (toInterpValue ())
+  | Barrier_Isync -> V_ctor (Id_aux (Id "Barrier_Isync") Unknown) (T_id "barrier_kind") (C_Enum 3) (toInterpValue ())
+  | Barrier_DMB -> V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") (C_Enum 4) (toInterpValue ())
+  | Barrier_DMB_ST -> V_ctor (Id_aux (Id "Barrier_DMB_ST") Unknown) (T_id "barrier_kind") (C_Enum 5) (toInterpValue ())
+  | Barrier_DMB_LD -> V_ctor (Id_aux (Id "Barrier_DMB_LD") Unknown) (T_id "barrier_kind") (C_Enum 6) (toInterpValue ())
+  | Barrier_DSB -> V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") (C_Enum 7) (toInterpValue ())
+  | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ())
+  | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ())
+  | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ())
+  end
+let rec barrier_kindFromInterpValue v = match v with
+  | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync
+  | V_ctor (Id_aux (Id "Barrier_LwSync") _) _ _ v -> Barrier_LwSync
+  | V_ctor (Id_aux (Id "Barrier_Eieio") _) _ _ v -> Barrier_Eieio
+  | V_ctor (Id_aux (Id "Barrier_Isync") _) _ _ v -> Barrier_Isync
+  | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> Barrier_DMB
+  | V_ctor (Id_aux (Id "Barrier_DMB_ST") _) _ _ v -> Barrier_DMB_ST
+  | V_ctor (Id_aux (Id "Barrier_DMB_LD") _) _ _ v -> Barrier_DMB_LD
+  | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> Barrier_DSB
+  | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST
+  | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD
+  | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB
+  | V_tuple [v] -> barrier_kindFromInterpValue v
+  | v -> failwith ("fromInterpValue barrier_kind: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance (ToFromInterpValue barrier_kind)
+  let toInterpValue = barrier_kindToInterpValue
+  let fromInterpValue = barrier_kindFromInterpValue
+end
+
+
+let instruction_kindToInterpValue = function
+  | IK_barrier v -> V_ctor (Id_aux (Id "IK_barrier") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
+  | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
+  | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
+  | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
+  | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
+  end
+let rec instruction_kindFromInterpValue v = match v with
+  | V_ctor (Id_aux (Id "IK_barrier") _) _ _ v -> IK_barrier (fromInterpValue v)
+  | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v)
+  | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v)
+  | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch
+  | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple
+  | V_tuple [v] -> instruction_kindFromInterpValue v
+  | v -> failwith ("fromInterpValue instruction_kind: unexpected value. " ^
+                     Interp.debug_print_value v)
+  end
+instance (ToFromInterpValue instruction_kind)
+  let toInterpValue = instruction_kindToInterpValue
+  let fromInterpValue = instruction_kindFromInterpValue
+end
+
+let regfpToInterpValue = function
+  | RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
+  | RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
+  | RSliceBit v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
+  | RField v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RField") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
+  end
+
+let rec regfpFromInterpValue v = match v with
+  | SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") _) _ _ v -> RFull (fromInterpValue v)
+  | SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v)
+  | SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v)
+  | SI.V_ctor (SIA.Id_aux (SIA.Id "RField") _) _ _ v -> RField (fromInterpValue v)
+  | SI.V_tuple [v] -> regfpFromInterpValue v
+  | v -> failwith ("fromInterpValue regfp: unexpected value. " ^ Interp.debug_print_value v)
+  end
+
+instance (ToFromInterpValue regfp)
+  let toInterpValue = regfpToInterpValue
+  let fromInterpValue = regfpFromInterpValue
+end
+
+
+
+
diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 5532089d..f770042c 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -2,14 +2,10 @@ open import Pervasives_extra
 open import Sail_impl_base
 open import Sail_values
 
-     import Interp_interface
-(* this needs to go away: it's only so we can make the ppcmem outcome types the
-same *)
-
-val return : forall 's 'a. 'a -> outcome 's 'a
+val return : forall 'a. 'a -> outcome 'a
 let return a = Done a
 
-val bind : forall 's 'a 'b. outcome 's 'a -> ('a -> outcome 's 'b) -> outcome 's 'b
+val bind : forall 'a 'b. outcome 'a -> ('a -> outcome 'b) -> outcome 'b
 let rec bind m f = match m with
   | Done a ->              f a
   | Read_mem descr k ->    Read_mem descr   (fun v -> let (o,opt) = k v in (bind o f,opt))
@@ -26,7 +22,7 @@ let rec bind m f = match m with
 end
 
 
-type M 'a = Sail_impl_base.outcome Interp_interface.instruction_state 'a
+type M 'a = outcome 'a
 
 let inline (>>=) = bind
 val (>>) : forall 'b. M unit -> M 'b -> M 'b
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 2ad25110..3357fe3d 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -1,6 +1,4 @@
 open import Pervasives_extra
-open import Interp     (* only for converting between shallow- and deep-embedding values *)
-open import Interp_ast (* only for converting between shallow- and deep-embedding values *)
 open import Sail_impl_base
 
 
@@ -18,7 +16,6 @@ let rec replace bs ((n : integer),b') = match bs with
   end
 
 
-                     
 (*** Bits *)
 type bitU = O | I | Undef
 
@@ -887,9 +884,6 @@ let assert' b msg_opt =
   end in
   if bitU_to_bool b then () else failwith msg
 
-
-
-                                     
 (* convert numbers unsafely to naturals *)
 
 class (ToNatural 'a) val toNatural : 'a -> natural end
@@ -906,532 +900,24 @@ let toNaturalFiveTup (n1,n2,n3,n4,n5) =
    toNatural n5)
 
 
-
-(* convert to/from interpreter values *)
-
-class (ToFromInterpValue 'a)
-  val toInterpValue : 'a -> Interp.value
-  val fromInterpValue : Interp.value -> 'a
-end
-
-let toInterValueBool = function
-  | true -> Interp.V_lit (L_aux (L_one) Unknown)
-  | false -> Interp.V_lit (L_aux (L_zero) Unknown)
-end
-let rec fromInterpValueBool v = match v with
-  | Interp.V_lit (L_aux (L_true) _)  -> true
-  | Interp.V_lit (L_aux (L_false) _) -> false
-  | Interp.V_lit (L_aux (L_one) _)  -> true
-  | Interp.V_lit (L_aux (L_zero) _) -> false
-  | Interp.V_tuple [v] -> fromInterpValueBool v
-  | v -> failwith ("fromInterpValue bool: unexpected value. " ^
-                     Interp.debug_print_value v)
-end
-instance (ToFromInterpValue bool)
-  let toInterpValue = toInterValueBool
-  let fromInterpValue = fromInterpValueBool
-end
-
-
-let toInterpValueUnit () = Interp.V_lit (L_aux (L_unit) Unknown)
-let rec fromInterpValueUnit v = match v with
-  | Interp.V_lit (L_aux (L_unit) _) -> ()
-  | Interp.V_tuple [v] -> fromInterpValueUnit v
-  | v -> failwith ("fromInterpValue unit: unexpected value. " ^
-                     Interp.debug_print_value v)
-end
-instance (ToFromInterpValue unit)
-  let toInterpValue = toInterpValueUnit
-  let fromInterpValue = fromInterpValueUnit
-end
-
-
-let toInterpValueInteger i = V_lit (L_aux (L_num i) Unknown)
-let rec fromInterpValueInteger v = match v with
-  | Interp.V_lit (L_aux (L_num i) _) -> i
-  | Interp.V_tuple [v] -> fromInterpValueInteger v
-  | v -> failwith ("fromInterpValue integer: unexpected value. " ^
-                     Interp.debug_print_value v)
-end
-instance (ToFromInterpValue integer)
-  let toInterpValue = toInterpValueInteger
-  let fromInterpValue = fromInterpValueInteger
-end
-
-
-let toInterpValueString s = V_lit (L_aux (L_string s) Unknown)
-let rec fromInterpValueString v = match v with
-  | Interp.V_lit (L_aux (L_string s) _) -> s
-  | Interp.V_tuple [v] -> fromInterpValueString v
-  | v -> failwith ("fromInterpValue integer: unexpected value. " ^
-                     Interp.debug_print_value v)
-end
-instance (ToFromInterpValue string)
-  let toInterpValue = toInterpValueString
-  let fromInterpValue = fromInterpValueString
-end
-
-
-let toInterpValueBitU = function
-  | I     -> Interp.V_lit (L_aux (L_one) Unknown)
-  | O     -> Interp.V_lit (L_aux (L_zero) Unknown)
-  | Undef -> Interp.V_lit (L_aux (L_undef) Unknown)
-end
-let rec fromInterpValueBitU v = match v with
-  | Interp.V_lit (L_aux (L_one) _)   -> I
-  | Interp.V_lit (L_aux (L_zero) _)  -> O
-  | Interp.V_lit (L_aux (L_undef) _) -> Undef
-  | Interp.V_lit (L_aux (L_true) _)   -> I
-  | Interp.V_lit (L_aux (L_false) _)  -> O
-  | Interp.V_tuple [v] -> fromInterpValueBitU v
-  | v -> failwith ("fromInterpValue bitU: unexpected value. " ^
-                     Interp.debug_print_value v)
-end
-instance (ToFromInterpValue bitU)
-  let toInterpValue = toInterpValueBitU
-  let fromInterpValue = fromInterpValueBitU
-end
-
-
-let tuple2ToInterpValue (a,b) =
-  V_tuple [toInterpValue a;toInterpValue b]
-let rec tuple2FromInterpValue v = match v with
-  | V_tuple [a;b] -> (fromInterpValue a,fromInterpValue b)
-  | V_tuple [v] -> tuple2FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b. ToFromInterpValue 'a, ToFromInterpValue 'b => (ToFromInterpValue ('a * 'b))
-  let toInterpValue = tuple2ToInterpValue
-  let fromInterpValue = tuple2FromInterpValue
-end
-
-
-let tuple3ToInterpValue (a,b,c) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c]
-let rec tuple3FromInterpValue v = match v with
-  | V_tuple [a;b;c] -> (fromInterpValue a,fromInterpValue b,fromInterpValue c)
-  | V_tuple [v] -> tuple3FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c. ToFromInterpValue 'a, ToFromInterpValue 'b, ToFromInterpValue 'c =>
-    (ToFromInterpValue ('a * 'b * 'c))
-  let toInterpValue = tuple3ToInterpValue
-  let fromInterpValue = tuple3FromInterpValue
-end
-
-
-let tuple4ToInterpValue (a,b,c,d) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d]
-let rec tuple4FromInterpValue v = match v with
-  | V_tuple [a;b;c;d] -> (fromInterpValue a,fromInterpValue b,
-                          fromInterpValue c,fromInterpValue d)
-  | V_tuple [v] -> tuple4FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd. ToFromInterpValue 'a, ToFromInterpValue 'b,
-                             ToFromInterpValue 'c, ToFromInterpValue 'd =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd))
-  let toInterpValue = tuple4ToInterpValue
-  let fromInterpValue = tuple4FromInterpValue
-end
-
-
-let tuple5ToInterpValue (a,b,c,d,e) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;toInterpValue e]
-let rec tuple5FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e)
-  | V_tuple [v] -> tuple5FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e))
-  let toInterpValue = tuple5ToInterpValue
-  let fromInterpValue = tuple5FromInterpValue
-end
-
-
-let tuple6ToInterpValue (a,b,c,d,e,f) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f]
-let rec tuple6FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f)
-  | V_tuple [v] -> tuple6FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f))
-  let toInterpValue = tuple6ToInterpValue
-  let fromInterpValue = tuple6FromInterpValue
-end
-
-
-let tuple7ToInterpValue (a,b,c,d,e,f,g) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g]
-let rec tuple7FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g)
-  | V_tuple [v] -> tuple7FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g))
-  let toInterpValue = tuple7ToInterpValue
-  let fromInterpValue = tuple7FromInterpValue
-end
-
-
-let tuple8ToInterpValue (a,b,c,d,e,f,g,h) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h]
-let rec tuple8FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g;h] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g,fromInterpValue h)
-  | V_tuple [v] -> tuple8FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g 'h.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g, ToFromInterpValue 'h =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h))
-  let toInterpValue = tuple8ToInterpValue
-  let fromInterpValue = tuple8FromInterpValue
-end
-
-
-let tuple9ToInterpValue (a,b,c,d,e,f,g,h,i) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
-           toInterpValue i]
-let rec tuple9FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g;h;i] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g,fromInterpValue h,fromInterpValue i)
-  | V_tuple [v] -> tuple9FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g, ToFromInterpValue 'h,
-    ToFromInterpValue 'i =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i))
-  let toInterpValue = tuple9ToInterpValue
-  let fromInterpValue = tuple9FromInterpValue
-end
-
-
-let tuple10ToInterpValue (a,b,c,d,e,f,g,h,i,j) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
-           toInterpValue i;toInterpValue j;]
-let rec tuple10FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g;h;i;j] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g,fromInterpValue h,fromInterpValue i,
-      fromInterpValue j)
-  | V_tuple [v] -> tuple10FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g, ToFromInterpValue 'h,
-    ToFromInterpValue 'i, ToFromInterpValue 'j =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j))
-  let toInterpValue = tuple10ToInterpValue
-  let fromInterpValue = tuple10FromInterpValue
-end
-
-
-let tuple11ToInterpValue (a,b,c,d,e,f,g,h,i,j,k) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
-           toInterpValue i;toInterpValue j;toInterpValue k;]
-let rec tuple11FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g;h;i;j;k] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g,fromInterpValue h,fromInterpValue i,
-      fromInterpValue j,fromInterpValue k)
-  | V_tuple [v] -> tuple11FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j*k: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g, ToFromInterpValue 'h,
-    ToFromInterpValue 'i, ToFromInterpValue 'j,
-    ToFromInterpValue 'k =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k))
-  let toInterpValue = tuple11ToInterpValue
-  let fromInterpValue = tuple11FromInterpValue
-end
-
-
-let tuple12ToInterpValue (a,b,c,d,e,f,g,h,i,j,k,l) =
-  V_tuple [toInterpValue a;toInterpValue b;toInterpValue c;toInterpValue d;
-           toInterpValue e;toInterpValue f;toInterpValue g;toInterpValue h;
-           toInterpValue i;toInterpValue j;toInterpValue k;toInterpValue l;]
-let rec tuple12FromInterpValue v = match v with
-  | V_tuple [a;b;c;d;e;f;g;h;i;j;k;l] ->
-     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
-      fromInterpValue d,fromInterpValue e,fromInterpValue f,
-      fromInterpValue g,fromInterpValue h,fromInterpValue i,
-      fromInterpValue j,fromInterpValue k,fromInterpValue l)
-  | V_tuple [v] -> tuple12FromInterpValue v
-  | v -> failwith ("fromInterpValue a*b*c*d*e*f*g*h*i*j*k*l: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l.
-    ToFromInterpValue 'a, ToFromInterpValue 'b,
-    ToFromInterpValue 'c, ToFromInterpValue 'd,
-    ToFromInterpValue 'e, ToFromInterpValue 'f,
-    ToFromInterpValue 'g, ToFromInterpValue 'h,
-    ToFromInterpValue 'i, ToFromInterpValue 'j,
-    ToFromInterpValue 'k, ToFromInterpValue 'l =>
-    (ToFromInterpValue ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l))
-  let toInterpValue = tuple12ToInterpValue
-  let fromInterpValue = tuple12FromInterpValue
-end
-
-
-let listToInterpValue l = V_list (List.map toInterpValue l)
-let rec listFromInterpValue v = match v with
-  | V_list l -> List.map fromInterpValue l
-  | V_tuple [v] -> listFromInterpValue v
-  | v -> failwith ("fromInterpValue list 'a: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (list 'a))
-  let toInterpValue = listToInterpValue
-  let fromInterpValue = listFromInterpValue
-end
-
-
-let vectorToInterpValue (Vector vs start direction) =
-  V_vector (natFromInteger start) (if direction then IInc else IDec) (List.map toInterpValue vs)
-let rec vectorFromInterpValue v = match v with
-  | V_vector start direction vs ->
-     Vector (List.map fromInterpValue vs) (integerFromNat start)
-            (match direction with | IInc -> true | IDec -> false end)
-  | V_vector_sparse start length direction valuemap defaultval ->
-     make_indexed_vector
-       (List.map (fun (i,v) -> (integerFromNat i,fromInterpValue v)) valuemap)
-       (fromInterpValue defaultval)
-       (integerFromNat start) (integerFromNat length)
-       (match direction with | IInc -> true | IDec -> false end)
-  | V_tuple [v] -> vectorFromInterpValue v
-  | v -> failwith ("fromInterpValue vector 'a: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (vector 'a))
-  let toInterpValue = vectorToInterpValue
-  let fromInterpValue = vectorFromInterpValue
-end
-
-(* Here the type information is not accurate: instead of T_id "option" it should
-   be T_app (T_id "option") (...), but temporarily we'll do it like this. The
-   same thing has to be fixed in pretty_print.ml when we're generating the
-   type-class instances. *)
-let maybeToInterpValue = function
-  | Nothing -> V_ctor (Id_aux (Id "None") Unknown) (T_id "option") C_Union (V_lit (L_aux L_unit Unknown))
-  | Just a  -> V_ctor (Id_aux (Id "Some") Unknown) (T_id "option") C_Union (toInterpValue a)
-  end
-let rec maybeFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "None") _) _ _ _ -> Nothing
-  | V_ctor (Id_aux (Id "Some") _) _ _ v -> Just (fromInterpValue v)
-  | V_tuple [v] -> maybeFromInterpValue v
-  | v -> failwith ("fromInterpValue maybe 'a: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-
-instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a))
-  let toInterpValue = maybeToInterpValue
-  let fromInterpValue = maybeFromInterpValue
-end
-
-
-module SI = Interp
-module SIA = Interp_ast
-
-
-let read_kindToInterpValue = function
-  | Read_plain -> V_ctor (Id_aux (Id "Read_plain") Unknown) (T_id "read_kind") (C_Enum 0) (toInterpValue ())
-  | Read_tag -> V_ctor (Id_aux (Id "Read_tag") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ())
-  | Read_tag_reserve -> V_ctor (Id_aux (Id "Read_tag_reserve") Unknown) (T_id "read_kind") (C_Enum 1) (toInterpValue ())
-  | Read_reserve -> V_ctor (Id_aux (Id "Read_reserve") Unknown) (T_id "read_kind") (C_Enum 2) (toInterpValue ())
-  | Read_acquire -> V_ctor (Id_aux (Id "Read_acquire") Unknown) (T_id "read_kind") (C_Enum 3) (toInterpValue ())
-  | Read_exclusive -> V_ctor (Id_aux (Id "Read_exclusive") Unknown) (T_id "read_kind") (C_Enum 4) (toInterpValue ())
-  | Read_exclusive_acquire -> V_ctor (Id_aux (Id "Read_exclusive_acquire") Unknown) (T_id "read_kind") (C_Enum 5) (toInterpValue ())
-  | Read_stream -> V_ctor (Id_aux (Id "Read_stream") Unknown) (T_id "read_kind") (C_Enum 6) (toInterpValue ())
-  end
-let rec read_kindFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "Read_plain") _) _ _ v -> Read_plain
-  | V_ctor (Id_aux (Id "Read_tag") _) _ _ v -> Read_tag
-  | V_ctor (Id_aux (Id "Read_tag_reserve") _) _ _ v -> Read_tag_reserve
-  | V_ctor (Id_aux (Id "Read_reserve") _) _ _ v -> Read_reserve
-  | V_ctor (Id_aux (Id "Read_acquire") _) _ _ v -> Read_acquire
-  | V_ctor (Id_aux (Id "Read_exclusive") _) _ _ v -> Read_exclusive
-  | V_ctor (Id_aux (Id "Read_exclusive_acquire") _) _ _ v -> Read_exclusive_acquire
-  | V_ctor (Id_aux (Id "Read_stream") _) _ _ v -> Read_stream
-  | V_tuple [v] -> read_kindFromInterpValue v
-  | v -> failwith ("fromInterpValue read_kind: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue read_kind)
-  let toInterpValue = read_kindToInterpValue
-  let fromInterpValue = read_kindFromInterpValue
-end
-
-
-let write_kindToInterpValue = function
-  | Write_plain -> V_ctor (Id_aux (Id "Write_plain") Unknown) (T_id "write_kind") (C_Enum 0) (toInterpValue ())
-  | Write_tag -> V_ctor (Id_aux (Id "Write_tag") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ())
-  | Write_tag_conditional -> V_ctor (Id_aux (Id "Write_tag_conditional") Unknown) (T_id "write_kind") (C_Enum 1) (toInterpValue ())
-  | Write_conditional -> V_ctor (Id_aux (Id "Write_conditional") Unknown) (T_id "write_kind") (C_Enum 2) (toInterpValue ())
-  | Write_release -> V_ctor (Id_aux (Id "Write_release") Unknown) (T_id "write_kind") (C_Enum 3) (toInterpValue ())
-  | Write_exclusive -> V_ctor (Id_aux (Id "Write_exclusive") Unknown) (T_id "write_kind") (C_Enum 4) (toInterpValue ())
-  | Write_exclusive_release -> V_ctor (Id_aux (Id "Write_exclusive_release") Unknown) (T_id "write_kind") (C_Enum 5) (toInterpValue ())
-  end
-let rec write_kindFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "Write_plain") _) _ _ v -> Write_plain
-  | V_ctor (Id_aux (Id "Write_tag") _) _ _ v -> Write_tag
-  | V_ctor (Id_aux (Id "Write_tag_conditional") _) _ _ v -> Write_tag_conditional
-  | V_ctor (Id_aux (Id "Write_conditional") _) _ _ v -> Write_conditional
-  | V_ctor (Id_aux (Id "Write_release") _) _ _ v -> Write_release
-  | V_ctor (Id_aux (Id "Write_exclusive") _) _ _ v -> Write_exclusive
-  | V_ctor (Id_aux (Id "Write_exclusive_release") _) _ _ v -> Write_exclusive_release
-  | V_tuple [v] -> write_kindFromInterpValue v
-  | v -> failwith ("fromInterpValue write_kind: unexpected value " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue write_kind)
-  let toInterpValue = write_kindToInterpValue
-  let fromInterpValue = write_kindFromInterpValue
-end
-
-
-let barrier_kindToInterpValue = function
-  | Barrier_Sync -> V_ctor (Id_aux (Id "Barrier_Sync") Unknown) (T_id "barrier_kind") (C_Enum 0) (toInterpValue ())
-  | Barrier_LwSync -> V_ctor (Id_aux (Id "Barrier_LwSync") Unknown) (T_id "barrier_kind") (C_Enum 1) (toInterpValue ())
-  | Barrier_Eieio -> V_ctor (Id_aux (Id "Barrier_Eieio") Unknown) (T_id "barrier_kind") (C_Enum 2) (toInterpValue ())
-  | Barrier_Isync -> V_ctor (Id_aux (Id "Barrier_Isync") Unknown) (T_id "barrier_kind") (C_Enum 3) (toInterpValue ())
-  | Barrier_DMB -> V_ctor (Id_aux (Id "Barrier_DMB") Unknown) (T_id "barrier_kind") (C_Enum 4) (toInterpValue ())
-  | Barrier_DMB_ST -> V_ctor (Id_aux (Id "Barrier_DMB_ST") Unknown) (T_id "barrier_kind") (C_Enum 5) (toInterpValue ())
-  | Barrier_DMB_LD -> V_ctor (Id_aux (Id "Barrier_DMB_LD") Unknown) (T_id "barrier_kind") (C_Enum 6) (toInterpValue ())
-  | Barrier_DSB -> V_ctor (Id_aux (Id "Barrier_DSB") Unknown) (T_id "barrier_kind") (C_Enum 7) (toInterpValue ())
-  | Barrier_DSB_ST -> V_ctor (Id_aux (Id "Barrier_DSB_ST") Unknown) (T_id "barrier_kind") (C_Enum 8) (toInterpValue ())
-  | Barrier_DSB_LD -> V_ctor (Id_aux (Id "Barrier_DSB_LD") Unknown) (T_id "barrier_kind") (C_Enum 9) (toInterpValue ())
-  | Barrier_ISB -> V_ctor (Id_aux (Id "Barrier_ISB") Unknown) (T_id "barrier_kind") (C_Enum 10) (toInterpValue ())
-  end
-let rec barrier_kindFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "Barrier_Sync") _) _ _ v -> Barrier_Sync
-  | V_ctor (Id_aux (Id "Barrier_LwSync") _) _ _ v -> Barrier_LwSync
-  | V_ctor (Id_aux (Id "Barrier_Eieio") _) _ _ v -> Barrier_Eieio
-  | V_ctor (Id_aux (Id "Barrier_Isync") _) _ _ v -> Barrier_Isync
-  | V_ctor (Id_aux (Id "Barrier_DMB") _) _ _ v -> Barrier_DMB
-  | V_ctor (Id_aux (Id "Barrier_DMB_ST") _) _ _ v -> Barrier_DMB_ST
-  | V_ctor (Id_aux (Id "Barrier_DMB_LD") _) _ _ v -> Barrier_DMB_LD
-  | V_ctor (Id_aux (Id "Barrier_DSB") _) _ _ v -> Barrier_DSB
-  | V_ctor (Id_aux (Id "Barrier_DSB_ST") _) _ _ v -> Barrier_DSB_ST
-  | V_ctor (Id_aux (Id "Barrier_DSB_LD") _) _ _ v -> Barrier_DSB_LD
-  | V_ctor (Id_aux (Id "Barrier_ISB") _) _ _ v -> Barrier_ISB
-  | V_tuple [v] -> barrier_kindFromInterpValue v
-  | v -> failwith ("fromInterpValue barrier_kind: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue barrier_kind)
-  let toInterpValue = barrier_kindToInterpValue
-  let fromInterpValue = barrier_kindFromInterpValue
-end
-
-
-let instruction_kindToInterpValue = function
-  | IK_barrier v -> V_ctor (Id_aux (Id "IK_barrier") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
-  | IK_mem_read v -> V_ctor (Id_aux (Id "IK_mem_read") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
-  | IK_mem_write v -> V_ctor (Id_aux (Id "IK_mem_write") Unknown) (T_id "instruction_kind") C_Union (toInterpValue v)
-  | IK_cond_branch -> V_ctor (Id_aux (Id "IK_cond_branch") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
-  | IK_simple -> V_ctor (Id_aux (Id "IK_simple") Unknown) (T_id "instruction_kind") C_Union (toInterpValue ())
-  end
-let rec instruction_kindFromInterpValue v = match v with
-  | V_ctor (Id_aux (Id "IK_barrier") _) _ _ v -> IK_barrier (fromInterpValue v)
-  | V_ctor (Id_aux (Id "IK_mem_read") _) _ _ v -> IK_mem_read (fromInterpValue v)
-  | V_ctor (Id_aux (Id "IK_mem_write") _) _ _ v -> IK_mem_write (fromInterpValue v)
-  | V_ctor (Id_aux (Id "IK_cond_branch") _) _ _ v -> IK_cond_branch
-  | V_ctor (Id_aux (Id "IK_simple") _) _ _ v -> IK_simple
-  | V_tuple [v] -> instruction_kindFromInterpValue v
-  | v -> failwith ("fromInterpValue instruction_kind: unexpected value. " ^
-                     Interp.debug_print_value v)
-  end
-instance (ToFromInterpValue instruction_kind)
-  let toInterpValue = instruction_kindToInterpValue
-  let fromInterpValue = instruction_kindFromInterpValue
-end
-
-
 type regfp =
   | RFull of (string)
   | RSlice of (string * integer * integer)
   | RSliceBit of (string * integer)
   | RField of (string * string)
 
-let regfpToInterpValue = function
-  | RFull v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
-  | RSlice v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
-  | RSliceBit v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
-  | RField v -> SI.V_ctor (SIA.Id_aux (SIA.Id "RField") SIA.Unknown) (SIA.T_id "regfp") SI.C_Union (toInterpValue v)
-  end
-
-let rec regfpFromInterpValue v = match v with
-  | SI.V_ctor (SIA.Id_aux (SIA.Id "RFull") _) _ _ v -> RFull (fromInterpValue v)
-  | SI.V_ctor (SIA.Id_aux (SIA.Id "RSlice") _) _ _ v -> RSlice (fromInterpValue v)
-  | SI.V_ctor (SIA.Id_aux (SIA.Id "RSliceBit") _) _ _ v -> RSliceBit (fromInterpValue v)
-  | SI.V_ctor (SIA.Id_aux (SIA.Id "RField") _) _ _ v -> RField (fromInterpValue v)
-  | SI.V_tuple [v] -> regfpFromInterpValue v
-  | v -> failwith ("fromInterpValue regfp: unexpected value. " ^ Interp.debug_print_value v)
-  end
-
-instance (ToFromInterpValue regfp)
-  let toInterpValue = regfpToInterpValue
-  let fromInterpValue = regfpFromInterpValue
-end
+type niafp = 
+  | NIAFP_successor
+  | NIAFP_concrete_address of vector bitU
+  | NIAFP_LR
+  | NIAFP_CTR
+  | NIAFP_register of regfp
 
+(* only for MIPS *)
+type diafp = 
+  | DIAFP_none
+  | DIAFP_concrete of vector bitU
+  | DIAFP_reg of regfp
 
 let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction * (nat * nat))) = function
   | RFull name -> 
@@ -1454,20 +940,6 @@ let regfp_to_reg (reg_info : string -> maybe string -> (nat * nat * direction *
      Reg_field name start direction field_name slice
 end
 
-
-type niafp = 
-  | NIAFP_successor
-  | NIAFP_concrete_address of vector bitU
-  | NIAFP_LR
-  | NIAFP_CTR
-  | NIAFP_register of regfp
-
-(* only for MIPS *)
-type diafp = 
-  | DIAFP_none
-  | DIAFP_concrete of vector bitU
-  | DIAFP_reg of regfp
-
 let niafp_to_nia reginfo = function
   | NIAFP_successor -> NIA_successor
   | NIAFP_concrete_address v -> NIA_concrete_address (address_of_bitv v)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 857a81a3..d35653c9 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -841,9 +841,12 @@ let interp mode (IState interp_state context) =
     | (o,_) -> o
 end 
 
-val state_to_outcome_s : forall 'v. interp_mode -> instruction_state -> Sail_impl_base.outcome_s instruction_state unit
-val outcome_to_outcome : interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome instruction_state unit
-let rec outcome_to_outcome mode = function
+val state_to_outcome_s : (instruction_state -> unit -> (string * string)) -> interp_mode -> instruction_state -> Sail_impl_base.outcome_s unit
+val outcome_to_outcome : (instruction_state -> unit -> (string * string)) -> interp_mode -> Interp_interface.outcome -> Sail_impl_base.outcome unit
+
+let rec outcome_to_outcome pp_instruction_state mode = 
+  let state_to_outcome_s = state_to_outcome_s pp_instruction_state in
+  function
   | Interp_interface.Read_mem rk addr size _ k ->
      Sail_impl_base.Read_mem (rk,addr,size) (fun v -> state_to_outcome_s mode (k v))
   | Interp_interface.Write_mem rk addr size _ mv _ k ->
@@ -876,16 +879,15 @@ let rec outcome_to_outcome mode = function
      failwith ("Interpreter error: " ^ message)
 end
 
-and state_to_outcome_s mode state = 
+and state_to_outcome_s pp_instruction_state mode state = 
   let next_outcome' = interp mode state in
-  let next_outcome = outcome_to_outcome mode next_outcome' in
-  (next_outcome, Just state)
-
+  let next_outcome = outcome_to_outcome pp_instruction_state mode next_outcome' in
+  (next_outcome, Just (pp_instruction_state state))
 
-let initial_outcome_s_of_instruction context mode instruction =
+val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit
+let initial_outcome_s_of_instruction pp_instruction_state context mode instruction =
   let state = instruction_to_istate context instruction in
-  let initial_outcome' = interp mode state in
-  (outcome_to_outcome mode initial_outcome',Just state)
+  state_to_outcome_s pp_instruction_state mode state
 
 
 (*Update slice potentially here*)
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index ea3ba154..b4a6c92b 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -202,5 +202,5 @@ val instruction_analysis :
   -> maybe (list (reg_name * register_value)) -> instruction -> (list reg_name * list reg_name * list reg_name * list nia * dia * instruction_kind)
 
 
-val initial_outcome_s_of_instruction : context -> interp_mode -> instruction -> Sail_impl_base.outcome_s instruction_state unit
+val initial_outcome_s_of_instruction : (instruction_state -> unit -> (string * string)) -> context -> interp_mode -> instruction -> Sail_impl_base.outcome_s unit
 
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index ee67c2c7..760b0a35 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -3,7 +3,7 @@ open Interp_ast ;;
 open Sail_impl_base ;;
 open Interp_utilities ;;
 open Interp_interface ;;
-open Interp_inter_imp ;;
+
 
 open Nat_big_num ;;
 
@@ -498,3 +498,6 @@ 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 print_instruction printer instr = printer (instruction_to_string instr)
+
+let pp_instruction_state state () =
+  (instruction_stack_to_string state,local_variables_to_string state)
diff --git a/src/lem_interp/printing_functions.mli b/src/lem_interp/printing_functions.mli
index 9eb89324..f629a307 100644
--- a/src/lem_interp/printing_functions.mli
+++ b/src/lem_interp/printing_functions.mli
@@ -71,3 +71,5 @@ val logfile_address_to_string : address -> string
 
 val byte_list_to_string : byte list -> string
 val bit_lifted_to_string : bit_lifted -> string
+
+val pp_instruction_state : instruction_state -> unit -> (string * string)
diff --git a/src/lem_interp/sail_impl_base.lem b/src/lem_interp/sail_impl_base.lem
index e932282c..e29b3391 100644
--- a/src/lem_interp/sail_impl_base.lem
+++ b/src/lem_interp/sail_impl_base.lem
@@ -1,5 +1,5 @@
 open import Pervasives_extra
-open import Interp_ast (* only because the instruction type refers to base effect *)
+open import Interp_ast (* this can go away *)
             
 (* maybe isn't a member of type Ord - this should be in the Lem standard library*)
 instance forall 'a. Ord 'a => (Ord (maybe 'a))
@@ -415,30 +415,32 @@ they just have particular nias (and will be IK_simple *)
   | IK_simple
 
 (* the address_lifted types should go away here and be replaced by address *)
-type outcome 's 'a =
+type outcome 'a =
   (* Request to read memory, value is location to read, integer is size to read,
      followed by registers that were used in computing that size *)
-  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> outcome_s 's 'a)
+  | Read_mem of (read_kind * address_lifted * nat) * (memory_value -> outcome_s 'a)
   (* Tell the system a write is imminent, at address lifted, of size nat *)
-  | Write_ea of (write_kind * address_lifted * nat) * outcome_s 's 'a
+  | Write_ea of (write_kind * address_lifted * nat) * outcome_s 'a
   (* Request to write memory at last signalled address. Memory value should be 8
      times the size given in ea signal *)
-  | Write_memv of memory_value * (bool -> outcome_s 's 'a)
+  | Write_memv of memory_value * (bool -> outcome_s 'a)
   (* Request a memory barrier *)
-  | Barrier of barrier_kind * outcome_s 's 'a
+  | Barrier of barrier_kind * outcome_s 'a
   (* Tell the system to dynamically recalculate dependency footprint *)
-  | Footprint of outcome_s 's 'a
+  | Footprint of outcome_s 'a
   (* Request to read register, will track dependency when mode.track_values *)
-  | Read_reg of reg_name * (register_value -> outcome_s 's 'a)
+  | Read_reg of reg_name * (register_value -> outcome_s 'a)
   (* Request to write register *)
-  | Write_reg of (reg_name * register_value) * (outcome_s 's 'a)
-  | Escape of maybe string * maybe (outcome_s 's unit)
+  | Write_reg of (reg_name * register_value) * (outcome_s 'a)
+  | Escape of maybe string * maybe (outcome_s unit)
   (*Result of a failed assert with possible error message to report*)
   | Fail of maybe string
-  | Internal of (maybe string * maybe (unit -> string)) * outcome_s 's 'a
+  | Internal of (maybe string * maybe (unit -> string)) * outcome_s 'a
   | Done of 'a
   | Error of string
- and outcome_s 's 'a = outcome 's 'a * maybe 's
+ and outcome_s 'a = outcome 'a * maybe (unit -> (string * string))
+(* first string : output of instruction_stack_to_string
+   second string: output of local_variables_to_string *)
 
 let ~{ocaml} read_kindCompare rk1 rk2 =
   match (rk1, rk2) with
diff --git a/src/process_file.ml b/src/process_file.ml
index 6270cb66..8f5dec40 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -178,25 +178,29 @@ let output1 libpath out_arg filename defs  =
          let ((o,_, _) as ext_o) =
            open_output_with_check_unformatted (f' ^ "_embedded.lem") in
          (Pretty_print.pp_defs_lem o defs (generated_line filename))
-           ["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values"];
+           ["Pervasives_extra";"Sail_impl_base";"Prompt";
+            "Sail_values";"Deep_shallow_convert"];
          close_output_with_check ext_o
       | Lem_out (Some lib) ->
          let ((o,_, _) as ext_o) =
            open_output_with_check_unformatted (f' ^ "_embedded.lem") in
 	 (Pretty_print.pp_defs_lem o defs (generated_line filename))
-           ["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values";lib];
+           ["Pervasives_extra";"Sail_impl_base";"Prompt";
+            "Sail_values";"Deep_shallow_convert";lib];
          close_output_with_check ext_o;
       | Lem_sequential_out None ->
          let ((o,_, _) as ext_o) =
            open_output_with_check_unformatted (f' ^ "_sequential_embedded.lem") in
          (Pretty_print.pp_defs_lem o defs (generated_line filename))
-           ["Pervasives_extra";"Sail_impl_base";"State";"Sail_values"];
+           ["Pervasives_extra";"Sail_impl_base";"State";
+            "Sail_values";"Deep_shallow_convert"];
          close_output_with_check ext_o
       | Lem_sequential_out (Some lib) ->
          let ((o,_, _) as ext_o) =
            open_output_with_check_unformatted (f' ^ "_sequential_embedded.lem") in
 	 (Pretty_print.pp_defs_lem o defs (generated_line filename))
-           ["Pervasives_extra";"Sail_impl_base";"State";"Sail_values";lib];
+           ["Pervasives_extra";"Sail_impl_base";"State";
+            "Sail_values";"Deep_shallow_convert";lib];
          close_output_with_check ext_o;
       | Ocaml_out None ->
         let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in