summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/gen_lib/sail_values.lem347
-rw-r--r--src/pretty_print.ml137
-rw-r--r--src/process_file.ml2
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 06:40:57 +0000