new command line option -marshal <file> to marshal out rewritten AST to a file

Adds new dependency: base64

4 files changed, 21 insertions, 4 deletions

diff --git a/.merlin b/.merlin
index a71b2802..c7e92de2 100644
--- a/.merlin
+++ b/.merlin
@@ -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
diff --git a/opam b/opam
index be29c2ef..62674d50 100644
--- a/opam
+++ b/opam
@@ -30,5 +30,6 @@ depends: [
   "ott" {>= "0.28"}
   "lem"
   "linksem" {>= "0.3"}
+  "base64"
 ]
 available: [ocaml-version >= "4.02.3"]
diff --git a/src/_tags b/src/_tags
index c5f4e127..6b2bf716 100644
--- a/src/_tags
+++ b/src/_tags
@@ -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