summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/sail.ml9
-rw-r--r--src/toFromInterp_backend.ml65
-rw-r--r--src/toFromInterp_lib.ml61
3 files changed, 113 insertions, 22 deletions
diff --git a/src/sail.ml b/src/sail.ml
index edf1bda4..a801ad81 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -60,6 +60,7 @@ let opt_print_initial_env = ref false
let opt_print_verbose = ref false
let opt_print_lem = ref false
let opt_print_tofrominterp = ref false
+let opt_tofrominterp_output_dir : string option ref = ref None
let opt_print_ocaml = ref false
let opt_print_c = ref false
let opt_print_latex = ref false
@@ -99,6 +100,12 @@ let options = Arg.align ([
( "-tofrominterp",
Arg.Set opt_print_tofrominterp,
" output OCaml functions to translate between shallow embedding and interpreter");
+ ( "-tofrominterp_lem",
+ Arg.Set ToFromInterp_backend.lem_mode,
+ " output embedding translation for the Lem backend rather than the OCaml backend");
+ ( "-tofrominterp_output_dir",
+ Arg.String (fun dir -> opt_tofrominterp_output_dir := Some dir),
+ " set a custom directory to output embedding translation OCaml");
( "-ocaml",
Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen],
" output an OCaml translated version of the input");
@@ -415,7 +422,7 @@ let main() =
then
let ast = rewrite_ast_interpreter type_envs ast in
let out = match !opt_file_out with None -> "out" | Some s -> s in
- ToFromInterp_backend.tofrominterp_output out ast
+ ToFromInterp_backend.tofrominterp_output !opt_tofrominterp_output_dir out ast
else ());
(if !(opt_print_c)
then
diff --git a/src/toFromInterp_backend.ml b/src/toFromInterp_backend.ml
index 85708712..5a03ca83 100644
--- a/src/toFromInterp_backend.ml
+++ b/src/toFromInterp_backend.ml
@@ -56,6 +56,11 @@ open Util
open Pretty_print_common
open Ocaml_backend
+let lem_mode = ref false
+
+let maybe_zencode s = if !lem_mode then s else zencode_string s
+let maybe_zencode_upper s = if !lem_mode then String.capitalize_ascii s else zencode_upper_string s
+
let frominterp_typedef (TD_aux (td_aux, (l, _))) =
let fromValueArgs (Typ_aux (typ_aux, _)) = match typ_aux with
| Typ_tup typs -> brackets (separate (semi ^^ space) (List.mapi (fun i _ -> string ("v" ^ (string_of_int i))) typs))
@@ -75,10 +80,10 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) =
| A_order order -> string ("Order_" ^ (string_of_order order))
| _ -> string "TYP_ARG"
and fromValueTyp ((Typ_aux (typ_aux, l)) as typ) arg_name = match typ_aux with
- | Typ_id id -> parens (concat [string (zencode_string (string_of_id id)); string ("FromInterpValue"); space; string arg_name])
+ | Typ_id id -> parens (concat [string (maybe_zencode (string_of_id id)); string ("FromInterpValue"); space; string arg_name])
| Typ_app (typ_id, typ_args) ->
assert (typ_args <> []);
- parens (separate space ([string (zencode_string (string_of_id typ_id) ^ "FromInterpValue")] @ List.map fromValueTypArg typ_args @ [string arg_name]))
+ parens (separate space ([string (maybe_zencode (string_of_id typ_id) ^ "FromInterpValue")] @ List.map fromValueTypArg typ_args @ [string arg_name]))
| Typ_var kid -> parens (separate space [fromValueKid kid; string arg_name])
| Typ_fn _ -> parens (string "failwith \"fromValueTyp: Typ_fn arm unimplemented\"")
| _ -> parens (string "failwith \"fromValueTyp: type arm unimplemented\"")
@@ -108,7 +113,7 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) =
| Id_aux ((Id "diafp"),_) -> empty *)
(* | Id_aux ((Id "option"),_) -> empty *)
| _ ->
- let fromInterpValueName = concat [string (zencode_string (string_of_id id)); string "FromInterpValue"] in
+ let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in
let fromFallback = separate space [pipe; underscore; arrow; string "failwith";
dquotes (string ("invalid interpreter value for " ^ (string_of_id id)))] in
let fromInterpValue =
@@ -120,7 +125,7 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) =
[pipe; string "V_ctor"; parens (concat [dquotes (string (string_of_id ctor_id)); comma_sp;
fromValueArgs typ
]);
- arrow; string (zencode_upper_string (string_of_id ctor_id)); fromValueVals typ
+ arrow; string (maybe_zencode_upper (string_of_id ctor_id)); fromValueVals typ
]
)
arms)
@@ -129,13 +134,13 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) =
fromInterpValue ^^ (twice hardline)
end
| TD_abbrev (id, typq, typ_arg) ->
- let fromInterpValueName = concat [string (zencode_string (string_of_id id)); string "FromInterpValue"] in
+ let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in
let fromInterpValue =
(separate space [string "let"; fromInterpValueName; separate space (fromValueTypqs typq); equals; fromValueTypArg typ_arg])
in
fromInterpValue ^^ (twice hardline)
| TD_enum (id, ids, _) ->
- let fromInterpValueName = concat [string (zencode_string (string_of_id id)); string "FromInterpValue"] in
+ let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in
let fromFallback = separate space [pipe; underscore; arrow; string "failwith";
dquotes (string ("invalid interpreter value for " ^ (string_of_id id)))] in
let fromInterpValue =
@@ -145,12 +150,26 @@ let frominterp_typedef (TD_aux (td_aux, (l, _))) =
(fun id ->
separate space
[pipe; string "V_ctor"; parens (concat [dquotes (string (string_of_id id)); comma_sp; string "[]"]);
- arrow; string (zencode_upper_string (string_of_id id))]
+ arrow; string (maybe_zencode_upper (string_of_id id))]
)
ids)
^^ hardline ^^ fromFallback)
in
fromInterpValue ^^ (twice hardline)
+ | TD_record (id, typq, fields, _) ->
+ let fromInterpField (typ, id) =
+ separate space [string (maybe_zencode (string_of_id id)); equals; fromValueTyp typ ("(StringMap.find \"" ^ (string_of_id id) ^ "\" fs)")]
+ in
+ let fromInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "FromInterpValue"] in
+ let fromFallback = separate space [pipe; underscore; arrow; string "failwith";
+ dquotes (string ("invalid interpreter value for " ^ (string_of_id id)))] in
+ let fromInterpValue =
+ prefix 2 1
+ (separate space [string "let"; fromInterpValueName; separate space (fromValueTypqs typq @ [string "v"]); equals; string "match v with"])
+ ((separate space [pipe; string "V_record fs"; arrow; braces (separate_map (semi ^^ space) fromInterpField fields)])
+ ^^ hardline ^^ fromFallback)
+ in
+ fromInterpValue ^^ (twice hardline)
| _ -> empty
let tointerp_typedef (TD_aux (td_aux, (l, _))) =
@@ -172,10 +191,10 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) =
| A_order order -> string ("Order_" ^ (string_of_order order))
| _ -> string "TYP_ARG"
and toValueTyp ((Typ_aux (typ_aux, l)) as typ) arg_name = match typ_aux with
- | Typ_id id -> parens (concat [string (zencode_string (string_of_id id)); string "ToInterpValue"; space; string arg_name])
+ | Typ_id id -> parens (concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"; space; string arg_name])
| Typ_app (typ_id, typ_args) ->
assert (typ_args <> []);
- parens (separate space ([string ((zencode_string (string_of_id typ_id)) ^ "ToInterpValue")] @ List.map toValueTypArg typ_args @ [string arg_name]))
+ parens (separate space ([string ((maybe_zencode (string_of_id typ_id)) ^ "ToInterpValue")] @ List.map toValueTypArg typ_args @ [string arg_name]))
| Typ_var kid -> parens (separate space [toValueKid kid; string arg_name])
| _ -> parens (string "failwith \"toValueTyp: type arm unimplemented\"")
in
@@ -204,14 +223,14 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) =
| Id_aux ((Id "diafp"),_) -> empty *)
(* | Id_aux ((Id "option"),_) -> empty *)
| _ ->
- let toInterpValueName = concat [string (zencode_string (string_of_id id)); string "ToInterpValue"] in
+ let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in
let toInterpValue =
prefix 2 1
(separate space [string "let"; toInterpValueName; separate space (toValueTypqs typq @ [string "v"]); equals; string "match v with"])
((separate_map hardline
(fun (Tu_aux (Tu_ty_id (typ, ctor_id), _)) ->
separate space
- [pipe; string (zencode_upper_string (string_of_id ctor_id)); toValueArgs typ;
+ [pipe; string (maybe_zencode_upper (string_of_id ctor_id)); toValueArgs typ;
arrow; string "V_ctor"; parens (concat [dquotes (string (string_of_id ctor_id)); comma_sp; toValueVals typ])
]
)
@@ -220,25 +239,36 @@ let tointerp_typedef (TD_aux (td_aux, (l, _))) =
toInterpValue ^^ (twice hardline)
end
| TD_abbrev (id, typq, typ_arg) ->
- let toInterpValueName = concat [string (zencode_string (string_of_id id)); string "ToInterpValue"] in
+ let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in
let toInterpValue =
(separate space [string "let"; toInterpValueName; separate space (toValueTypqs typq); equals; toValueTypArg typ_arg])
in
toInterpValue ^^ (twice hardline)
| TD_enum (id, ids, _) ->
- let toInterpValueName = concat [string (zencode_string (string_of_id id)); string "ToInterpValue"] in
+ let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in
let toInterpValue =
prefix 2 1
(separate space [string "let"; toInterpValueName; string "v"; equals; string "match v with"])
((separate_map hardline
(fun id ->
separate space
- [pipe; string (zencode_upper_string (string_of_id id));
+ [pipe; string (maybe_zencode_upper (string_of_id id));
arrow; string "V_ctor"; parens (concat [dquotes (string (string_of_id id)); comma_sp; string "[]"])]
)
ids))
in
toInterpValue ^^ (twice hardline)
+ | TD_record (id, typq, fields, _) ->
+ let toInterpField (typ, id) =
+ parens (separate comma_sp [dquotes (string (string_of_id id)); toValueTyp typ ("r." ^ (maybe_zencode (string_of_id id)))])
+ in
+ let toInterpValueName = concat [string (maybe_zencode (string_of_id id)); string "ToInterpValue"] in
+ let toInterpValue =
+ prefix 2 1
+ (separate space [string "let"; toInterpValueName; separate space (toValueTypqs typq @ [string "r"]); equals])
+ (separate space [string "V_record"; parens (separate space [string "List.fold_left (fun m (k, v) -> StringMap.add k v m) StringMap.empty"; (brackets (separate_map (semi ^^ space) toInterpField fields))])])
+ in
+ toInterpValue ^^ (twice hardline)
| _ -> empty
@@ -257,9 +287,8 @@ let tofrominterp_defs name (Defs defs) =
let tofrominterp_pp_defs name f defs =
ToChannel.pretty 1. 80 f (tofrominterp_defs name defs)
-let tofrominterp_output name defs =
- let out_chan = open_out (name ^ "_toFromInterp.ml") in
+let tofrominterp_output maybe_dir name defs =
+ let dir = match maybe_dir with Some dir -> dir | None -> "." in
+ let out_chan = open_out (Filename.concat dir (name ^ "_toFromInterp.ml")) in
tofrominterp_pp_defs name out_chan defs;
close_out out_chan
-
-
diff --git a/src/toFromInterp_lib.ml b/src/toFromInterp_lib.ml
index b045e4e8..5e776853 100644
--- a/src/toFromInterp_lib.ml
+++ b/src/toFromInterp_lib.ml
@@ -16,17 +16,67 @@ let zunitFromInterpValue v = match v with
let zunitToInterpValue () = V_unit
+let unitFromInterpValue = zunitFromInterpValue
+let unitToInterpValue = zunitToInterpValue
let zatomFromInterpValue typq_'n v = match v with
- | V_int i ->
- assert (typq_'n = i);
- i
+ | V_int i when typq_'n = i -> i
| _ -> failwith "invalid interpreter value for atom"
let zatomToInterpValue typq_'n v =
assert (typq_'n = v);
V_int v
+let atomFromInterpValue = zatomFromInterpValue
+let atomToInterpValue = zatomToInterpValue
+
+let zintFromInterpValue v = match v with
+ | V_int i -> i
+ | _ -> failwith "invalid interpreter value for int"
+
+let zintToInterpValue v = V_int v
+
+let intFromInterpValue = zintFromInterpValue
+let intToInterpValue = zintToInterpValue
+
+let znatFromInterpValue v = match v with
+ | V_int i when i >= Big_int.zero -> i
+ | _ -> failwith "invalid interpreter value for nat"
+
+let znatToInterpValue v =
+ assert (v >= Big_int.zero);
+ V_int v
+
+let natFromInterpValue = znatFromInterpValue
+let natToInterpValue = znatToInterpValue
+
+
+let zboolFromInterpValue v = match v with
+ | V_bool b -> b
+ | _ -> failwith "invalid interpreter value for bool"
+
+let zboolToInterpValue v = V_bool v
+
+let boolFromInterpValue = zboolFromInterpValue
+let boolToInterpValue = zboolToInterpValue
+
+let zstringFromInterpValue v = match v with
+ | V_string s -> s
+ | _ -> failwith "invalid interpreter value for string"
+
+let zstringToInterpValue v = V_string v
+
+let stringFromInterpValue = zstringFromInterpValue
+let stringToInterpValue = zstringToInterpValue
+
+let zlistFromInterpValue typq_'a v = match v with
+ | V_list vs -> List.map typq_'a vs
+ | _ -> failwith "invalid interpreter value for list"
+
+let zlistToInterpValue typq_'a v = V_list (List.map typq_'a v)
+
+let listFromInterpValue = zlistFromInterpValue
+let listToInterpValue = zlistToInterpValue
let zvectorFromInterpValue typq_'n typq_'ord typq_'a v = match v with
| V_vector vs ->
@@ -38,9 +88,14 @@ let zvectorToInterpValue typq_'n typq_'ord typq_'a v =
assert (Big_int.of_int (List.length v) = typq_'n);
V_vector (List.map typq_'a v)
+let vectorFromInterpValue = zvectorFromInterpValue
+let vectorToInterpValue = zvectorToInterpValue
let zbitFromInterpValue v = match v with
| V_bit b -> b
| _ -> failwith "invalid interpreter value for bit"
let zbitToInterpValue v = V_bit v
+
+let bitFromInterpValue = zbitFromInterpValue
+let bitToInterpValue = zbitToInterpValue
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 05:51:20 +0000