Merge remote-tracking branch 'origin/experiments' into sail2

1 files changed, 9 insertions, 11 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 7a4f71e3..ca23d876 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -53,7 +53,7 @@ let opt_lem_mwords = ref false
 
 type out_type =
   | Lem_ast_out
-  | Lem_out of string option
+  | Lem_out of string list
 
 let get_lexbuf f =
   let in_chan = open_in f in
@@ -101,7 +101,7 @@ let opt_dmono_analysis = ref 0
 let opt_auto_mono = ref false
 
 let monomorphise_ast locs type_env ast =
-  let ast = Monomorphise.monomorphise (!opt_lem_mwords) (!opt_auto_mono) (!opt_dmono_analysis)
+  let ast = Monomorphise.monomorphise (!Pretty_print_lem.opt_mwords) (!opt_auto_mono) (!opt_dmono_analysis)
     locs type_env ast in
   let () = if !opt_ddump_raw_mono_ast then Pretty_print_sail.pp_defs stdout ast else () in
   let ienv = Type_check.Env.no_casts Type_check.initial_env in
@@ -130,10 +130,10 @@ let generated_line f =
 
 let output_lem filename libs defs =
   let generated_line = generated_line filename in
-  let seq_suffix = if !opt_lem_sequential then "_sequential" else "" in
+  let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in
   let types_module = (filename ^ "_embed_types" ^ seq_suffix) in
-  let monad_module = if !opt_lem_sequential then "State" else "Prompt" in
-  let operators_module = if !opt_lem_mwords then "Sail_operators_mwords" else "Sail_operators" in
+  let monad_module = if !Pretty_print_lem.opt_sequential then "State" else "Prompt" in
+  let operators_module = if !Pretty_print_lem.opt_mwords then "Sail_operators_mwords" else "Sail_operators" in
   let libs = List.map (fun lib -> lib ^ seq_suffix) libs in
   let base_imports = [
       "Pervasives_extra";
@@ -146,7 +146,7 @@ let output_lem filename libs defs =
     open_output_with_check_unformatted (filename ^ "_embed_types" ^ seq_suffix ^ ".lem") in
   let ((o,_, _) as ext_o) =
     open_output_with_check_unformatted (filename ^ "_embed" ^ seq_suffix ^ ".lem") in
-  (Pretty_print.pp_defs_lem !opt_lem_sequential !opt_lem_mwords
+  (Pretty_print.pp_defs_lem
      (ot, base_imports)
      (o, base_imports @ (String.capitalize types_module :: libs))
      defs generated_line);
@@ -172,10 +172,8 @@ let output1 libpath out_arg filename defs  =
 	  Pretty_print.pp_lem_defs o defs;
 	  close_output_with_check ext_o
 	end
-      | Lem_out None ->
-        output_lem f' [] defs
-      | Lem_out (Some lib) ->
-        output_lem f' [lib] defs
+      | Lem_out libs ->
+        output_lem f' libs defs
 
 let output libpath out_arg files =
   List.iter
@@ -204,7 +202,7 @@ let rewrite rewriters defs =
      raise (Reporting_basic.err_typ l (Type_check.string_of_type_error err))
 
 let rewrite_ast = rewrite [("initial", Rewriter.rewrite_defs)]
-let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !opt_lem_mwords x)]
+let rewrite_undefined = rewrite [("undefined", fun x -> Rewrites.rewrite_undefined !Pretty_print_lem.opt_mwords x)]
 let rewrite_ast_lem = rewrite Rewrites.rewrite_defs_lem
 let rewrite_ast_ocaml = rewrite Rewrites.rewrite_defs_ocaml
 let rewrite_ast_interpreter = rewrite Rewrites.rewrite_defs_interpreter