typeclass instances for converting between shallow and deep embedding

3 files changed, 471 insertions, 15 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 9307ef80..3e4971df 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -1,6 +1,8 @@
 open import Pervasives_extra
 open import Sail_impl_base
 open import Vector
+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 *)
 
 type i = integer
 type n = natural
@@ -21,6 +23,10 @@ type register =
   | RegisterPair of register * register
 
 let dir is_inc = if is_inc then D_increasing else D_decreasing
+let bool_of_dir = function
+  | D_increasing -> true
+  | D_decreasing -> false
+  end
 
 let name_of_reg (Register name _ _ _ _) = name
 let size_of_reg (Register _ size _ _ _) = size
@@ -646,3 +652,344 @@ let assert' b msg_opt =
   | Nothing  -> "unspecified error"
   end in
   if to_bool b then failwith msg else ()
+
+
+class (ToFromInterpValue 'a)
+  val toInterpValue : 'a -> Interp.value
+  val fromInterpValue : Interp.value -> 'a
+end
+
+instance (ToFromInterpValue bool)
+  let toInterpValue = function
+    | true -> Interp.V_lit (L_aux (L_one) Unknown)
+    | false -> Interp.V_lit (L_aux (L_zero) Unknown)
+    end
+  let fromInterpValue = function
+    | 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
+    | _ -> failwith "fromInterpValue bool: unexpected value"
+    end
+end
+
+instance (ToFromInterpValue unit)
+  let toInterpValue = fun () -> Interp.V_lit (L_aux (L_unit) Unknown)
+  let fromInterpValue = function
+    | Interp.V_lit (L_aux (L_unit) _) -> ()
+    | _ -> failwith "fromInterpValue unit: unexpected value"
+    end
+end
+
+instance (ToFromInterpValue integer)
+  let toInterpValue i = V_lit (L_aux (L_num i) Unknown)
+  let fromInterpValue = function
+    | Interp.V_lit (L_aux (L_num i) _) -> i
+    | _ -> failwith "fromInterpValue integer: unexexpected value"
+    end
+end
+
+instance (ToFromInterpValue string)
+  let toInterpValue s = V_lit (L_aux (L_string s) Unknown)
+  let fromInterpValue = function
+    | Interp.V_lit (L_aux (L_string s) _) -> s
+    | _ -> failwith "fromInterpValue integer: unexexpected value"
+    end
+end
+
+instance (ToFromInterpValue bitU)
+  let toInterpValue = 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 fromInterpValue = function
+    | Interp.V_lit (L_aux (L_one) _)   -> I
+    | Interp.V_lit (L_aux (L_zero) _)  -> O
+    | Interp.V_lit (L_aux (L_undef) _) -> Undef
+    | _ -> failwith "fromInterpValue bitU: unexpected value"
+    end
+end
+
+
+let tuple2ToInterpValue (a,b) =
+  V_tuple [toInterpValue a;toInterpValue b]
+let tuple2FromInterpValue = function
+  | V_tuple [a;b] -> (fromInterpValue a,fromInterpValue b)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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 tuple3FromInterpValue = function
+  | V_tuple [a;b;c] -> (fromInterpValue a,fromInterpValue b,fromInterpValue c)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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 tuple4FromInterpValue = function
+  | V_tuple [a;b;c;d] -> (fromInterpValue a,fromInterpValue b,
+                          fromInterpValue c,fromInterpValue d)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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 tuple5FromInterpValue = function
+  | V_tuple [a;b;c;d;e] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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 tuple6FromInterpValue = function
+  | V_tuple [a;b;c;d;e;f] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e,fromInterpValue f)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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 tuple7FromInterpValue = function
+  | V_tuple [a;b;c;d;e;f;g] ->
+     (fromInterpValue a,fromInterpValue b,fromInterpValue c,
+      fromInterpValue d,fromInterpValue e,fromInterpValue f,
+      fromInterpValue g)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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 tuple8FromInterpValue = function
+  | 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)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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 tuple9FromInterpValue = function
+  | 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)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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 tuple10FromInterpValue = function
+  | 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)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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 tuple11FromInterpValue = function
+  | 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)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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 tuple12FromInterpValue = function
+  | 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)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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
+
+
+
+val listToInterpValue : forall 'a. ToFromInterpValue 'a => list 'a -> Interp.value
+let listToInterpValue l = V_list (List.map toInterpValue l)
+
+val listFromInterpValue : forall 'a. ToFromInterpValue 'a => Interp.value -> list 'a
+let listFromInterpValue = function
+  | V_list l -> List.map fromInterpValue l
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  end
+
+instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (list 'a))
+  let toInterpValue = listToInterpValue
+  let fromInterpValue = listFromInterpValue
+end
+
+
+val vectorToInterpValue : forall 'a. ToFromInterpValue 'a => vector 'a -> Interp.value
+let vectorToInterpValue (Vector vs start direction) =
+  V_vector (natFromInteger start) (if direction then IInc else IDec) (List.map toInterpValue vs)
+
+val vectorFromInterpValue : forall 'a. ToFromInterpValue 'a => Interp.value -> vector 'a
+let vectorFromInterpValue = function
+  | 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)
+  | _ -> failwith "fromInterpValue a*b: unexpected value"
+  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. *)
+val maybeToInterpValue : forall 'a. ToFromInterpValue 'a => maybe 'a -> Interp.value
+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
+
+val maybeFromInterpValue : forall 'a. ToFromInterpValue 'a => Interp.value -> maybe 'a
+let maybeFromInterpValue = function
+  | V_ctor (Id_aux (Id "None") _) _ _ _ -> Nothing
+  | V_ctor (Id_aux (Id "Some") _) _ _ v -> Just (fromInterpValue v)
+  | _ -> failwith "fromInterpValue maybe: unexpected value"
+  end
+
+instance forall 'a. ToFromInterpValue 'a => (ToFromInterpValue (maybe 'a))
+  let toInterpValue = maybeToInterpValue
+  let fromInterpValue = maybeFromInterpValue
+end
+
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index d53ee417..5aec2d03 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -2798,16 +2798,115 @@ let doc_typdef_lem regtypes (TD_aux(td,_)) = match td with
       doc_op equals
              (concat [string "type"; space; doc_id_lem_type id;])
              (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space)))
-  | TD_variant(id,nm,typq,ar,_) ->
-    let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in
-    doc_op equals
-      (concat [string "type"; space; doc_id_lem_type id;])
-      (doc_typquant_lem typq ar_doc)
+   | TD_variant(id,nm,typq,ar,_) ->
+      let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in
+      let typ_pp = (doc_op equals)
+                     (concat [string "type"; space; doc_id_lem_type id;])
+                     (doc_typquant_lem typq ar_doc) in
+      let make_id pat id =
+        separate space [string "SIA.Id_aux";
+                        parens (string "SIA.Id " ^^ string_lit (doc_id id));
+                        if pat then underscore else string "SIA.Unknown"] in
+      let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in
+      let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in
+      let fromInterpValuePP =
+        (prefix 2 1)
+          (separate space [string "let";fromInterpValueF;equals;string "function"])
+          (
+            ((separate_map (break 1))
+               (fun (Tu_aux (tu,_)) ->
+                 match tu with
+                 | Tu_ty_id (ty,cid) ->
+                    (separate space)
+                      [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+                       arrow;
+                       doc_id_lem_ctor cid;
+                       parens (string "fromInterpValue v")]
+                 | Tu_id cid ->
+                    (separate space)
+                      [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+                       arrow;
+                       doc_id_lem_ctor cid])
+               ar) ^/^
+              string "end") in
+      let toInterpValuePP =
+        (prefix 2 1)
+          (separate space [string "let";toInterpValueF;equals;string "function"])
+          (
+            ((separate_map (break 1))
+               (fun (Tu_aux (tu,_)) ->
+                 match tu with
+                 | Tu_ty_id (ty,cid) ->
+                    (separate space)
+                      [pipe;doc_id_lem_ctor cid;string "v";arrow;
+                       string "SI.V_ctor";
+                       parens (make_id false cid);
+                       parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+                       string "SI.C_Union";
+                       parens (string "toInterpValue v")]
+                 | Tu_id cid ->
+                    (separate space)
+                      [pipe;doc_id_lem_ctor cid;arrow;
+                       string "SI.V_ctor";
+                       parens (make_id false cid);
+                       parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+                       string "SI.C_Union";
+                       parens (string "toInterpValue ()")])
+               ar) ^/^
+              string "end") in
+      typ_pp ^^ hardline ^^ hardline ^^
+        fromInterpValuePP ^^ hardline ^^ hardline ^^
+          toInterpValuePP ^^ hardline
   | TD_enum(id,nm,enums,_) ->
-    let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_lem_ctor enums) in
-    doc_op equals
-      (concat [string "type"; space; doc_id_lem_type id;])
-      (enums_doc)
+     let rec range i j = if i > j then [] else i :: (range (i+1) j) in
+     let nats = range 0 in
+     let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_lem_ctor enums) in
+     let typ_pp = (doc_op equals)
+                    (concat [string "type"; space; doc_id_lem_type id;])
+                    (enums_doc) in
+     let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in
+     let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in
+     let make_id pat id =
+       separate space [string "SIA.Id_aux";
+                       parens (string "SIA.Id " ^^ string_lit (doc_id id));
+                       if pat then underscore else string "SIA.Unknown"] in
+     let fromInterpValuePP =
+       (prefix 2 1)
+         (separate space [string "let";fromInterpValueF;equals;string "function"])
+         (
+           ((separate_map (break 1))
+              (fun cid ->
+                (separate space)
+                  [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+                   arrow;
+                   doc_id_lem_ctor cid])
+              enums) ^/^
+             string "end") in
+     let toInterpValuePP =
+       (prefix 2 1)
+         (separate space [string "let";toInterpValueF;equals;string "function"])
+         (
+           ((separate_map (break 1))
+              (fun (cid,number) ->
+                (separate space)
+                  [pipe;doc_id_lem_ctor cid;arrow;
+                   string "SI.V_ctor";
+                   parens (make_id false cid);
+                   parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+                   parens (string ("SI.C_Enum " ^ string_of_int number));
+                   parens (string "toInterpValue ()")])
+              (List.combine enums (nats ((List.length enums) - 1)))) ^/^
+             string "end") in
+     let fromToInterpValuePP =
+       ((prefix 2 1)
+         (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)])
+         (concat [string "let toInterpValue = ";toInterpValueF;hardline;
+                  string "let fromInterpValue = ";fromInterpValueF]))
+       ^/^ string "end" in
+      typ_pp ^^ hardline ^^ hardline ^^
+        fromInterpValuePP ^^ hardline ^^ hardline ^^
+          toInterpValuePP ^^ hardline ^^ hardline ^^
+            fromToInterpValuePP ^^ hardline
   | TD_register(id,n1,n2,rs) ->
     match n1,n2 with
     | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
@@ -2923,12 +3022,22 @@ let find_regtypes (Defs defs) =
     ) [] defs
 
 
+let typ_to_t env =
+  Type_check.typ_to_t env false false
+
 let pp_defs_lem f d top_line opens =
   let regtypes = find_regtypes d in
   let defs = doc_defs_lem regtypes d in
   (print f)
-    (string "(*" ^^ (string top_line) ^^ string "*)" ^/^
-       ((separate_map hardline)
-          (fun lib -> separate space [string "open import";string lib]) opens) ^/^
-         hardline ^^ defs);
-
+    (concat 
+       [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
+        (separate_map hardline)
+          (fun lib -> separate space [string "open import";string lib]) opens;hardline;
+        (separate_map hardline)
+          (fun lib -> separate space [string "     import";string lib]) ["Interp";"Interp_ast"]; hardline;
+        hardline;
+        string "module SI = Interp"; hardline;
+        string "module SIA = Interp_ast"; hardline;
+        hardline;
+        defs])
+       
diff --git a/src/process_file.ml b/src/process_file.ml
index aecf642f..16feb92b 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -183,7 +183,7 @@ 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";"Vector";"Prompt";"Sail_values"; lib];
+           ["Pervasives_extra";"Sail_impl_base";"Vector";"Prompt";"Sail_values";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