diff options
| -rw-r--r-- | .merlin | 2 | ||||
| -rw-r--r-- | opam | 1 | ||||
| -rw-r--r-- | src/_tags | 6 | ||||
| -rw-r--r-- | src/sail.ml | 16 |
4 files changed, 21 insertions, 4 deletions
@@ -9,4 +9,4 @@ S src/lem_interp/** S src/pprint/** S src/test/** B src/_build/** -PKG num str unix uint zarith linksem lem linenoise +PKG num str unix uint zarith linksem lem linenoise base64 @@ -30,5 +30,6 @@ depends: [ "ott" {>= "0.28"} "lem" "linksem" {>= "0.3"} + "base64" ] available: [ocaml-version >= "4.02.3"] @@ -1,12 +1,12 @@ true: -traverse, debug, use_menhir <**/*.ml>: bin_annot, annot -<sail.{byte,native}>: package(zarith), package(linksem), package(lem), use_pprint -<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), use_pprint +<sail.{byte,native}>: package(zarith), package(linksem), package(lem), package(base64), use_pprint +<isail.{byte,native}>: package(zarith), package(linenoise), package(linksem), package(lem), package(base64), use_pprint <isail.ml>: package(linenoise) <elf_loader.ml>: package(linksem) -<**/*.m{l,li}>: package(lem) +<**/*.m{l,li}>: package(lem), package(base64) <gen_lib>: include <pprint> or <pprint/src>: include diff --git a/src/sail.ml b/src/sail.ml index 2748cb81..5deaa340 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -72,6 +72,7 @@ let opt_libs_coq = ref ([]:string list) let opt_file_arguments = ref ([]:string list) let opt_process_elf : string option ref = ref None let opt_ocaml_generators = ref ([]:string list) +let opt_marshal_defs = ref false let options = Arg.align ([ ( "-o", @@ -111,6 +112,9 @@ let options = Arg.align ([ ( "-latex", Arg.Set opt_print_latex, " pretty print the input to latex"); + ( "-marshal", + Arg.Set opt_marshal_defs, + " OCaml-marshal out the rewritten AST to a file"); ( "-c", Arg.Tuple [Arg.Set opt_print_c; Arg.Set Initial_check.opt_undefined_gen], " output a C translated version of the input"); @@ -368,6 +372,18 @@ let main() = close_out chan end else ()); + (if !(opt_marshal_defs) + then + begin + let ast_marshal = rewrite_ast_ocaml type_envs ast in + let out_filename = match !opt_file_out with None -> "out" | Some s -> s in + let f = open_out_bin (out_filename ^ ".defs") in + Marshal.to_string ast_marshal [Marshal.No_sharing; Marshal.Compat_32] + |> B64.encode + |> output_string f; + close_out f + end + else ()); end let _ = try |