Merge branch 'sail2' into asl_flow2

1 files changed, 27 insertions, 18 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index ed34238b..00013775 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -51,6 +51,10 @@
 open PPrint
 open Pretty_print_common
 
+let opt_lem_output_dir = ref None
+let opt_isa_output_dir = ref None
+let opt_coq_output_dir = ref None
+
 type out_type =
   | Lem_out of string list
   | Coq_out of string list
@@ -254,19 +258,24 @@ let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tanno
   (ast, env)
 
 
-let open_output_with_check file_name =
+let open_output_with_check opt_dir file_name =
   let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
   let o' = Format.formatter_of_out_channel o in
-  (o', (o, temp_file_name, file_name))
+  (o', (o, temp_file_name, opt_dir, file_name))
 
-let open_output_with_check_unformatted file_name =
+let open_output_with_check_unformatted opt_dir file_name =
   let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
-  (o, temp_file_name, file_name)
+  (o, temp_file_name, opt_dir, file_name)
 
 let always_replace_files = ref true
 
-let close_output_with_check (o, temp_file_name, file_name) =
+let close_output_with_check (o, temp_file_name, opt_dir, file_name) =
   let _ = close_out o in
+  let file_name = match opt_dir with
+                  | None     -> file_name
+                  | Some dir -> if Sys.file_exists dir then ()
+                                else Unix.mkdir dir 0o775;
+                                Filename.concat dir file_name in
   let do_replace = !always_replace_files || (not (Util.same_content_files temp_file_name file_name)) in
   let _ = if (not do_replace) then Sys.remove temp_file_name
           else Util.move_file temp_file_name file_name in
@@ -308,22 +317,22 @@ let output_lem filename libs type_env defs =
       string  "end"
     ] ^^ hardline
   in
-  let ((ot,_, _) as ext_ot) =
-    open_output_with_check_unformatted (filename ^ "_types" ^ ".lem") in
-  let ((o,_, _) as ext_o) =
-    open_output_with_check_unformatted (filename ^ ".lem") in
+  let ((ot,_,_,_) as ext_ot) =
+    open_output_with_check_unformatted !opt_lem_output_dir (filename ^ "_types" ^ ".lem") in
+  let ((o,_,_,_) as ext_o) =
+    open_output_with_check_unformatted !opt_lem_output_dir (filename ^ ".lem") in
   (Pretty_print.pp_defs_lem
      (ot, base_imports)
      (o, base_imports @ (String.capitalize_ascii types_module :: libs))
      type_env defs generated_line);
   close_output_with_check ext_ot;
   close_output_with_check ext_o;
-  let ((ol, _, _) as ext_ol) =
-    open_output_with_check_unformatted (isa_thy_name ^ ".thy") in
+  let ((ol,_,_,_) as ext_ol) =
+    open_output_with_check_unformatted !opt_isa_output_dir (isa_thy_name ^ ".thy") in
   print ol isa_lemmas;
   close_output_with_check ext_ol
 
-let output_coq filename libs defs =
+let output_coq opt_dir filename libs defs =
   let generated_line = generated_line filename in
   let types_module = (filename ^ "_types") in
   let monad_modules = ["Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_state"] in
@@ -336,10 +345,10 @@ let output_coq filename libs defs =
       operators_module
     ] @ monad_modules
   in
-  let ((ot,_, _) as ext_ot) =
-    open_output_with_check_unformatted (filename ^ "_types" ^ ".v") in
-  let ((o,_, _) as ext_o) =
-    open_output_with_check_unformatted (filename ^ ".v") in
+  let ((ot,_,_,_) as ext_ot) =
+    open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in
+  let ((o,_,_,_) as ext_o) =
+    open_output_with_check_unformatted opt_dir (filename ^ ".v") in
   (Pretty_print_coq.pp_defs_coq
      (ot, base_imports)
      (o, base_imports @ (types_module :: libs))
@@ -357,7 +366,7 @@ let output1 libpath out_arg filename type_env defs  =
   | Lem_out libs ->
      output_lem f' libs type_env defs
   | Coq_out libs ->
-     output_coq f' libs defs
+     output_coq !opt_coq_output_dir f' libs defs
 
 let output libpath out_arg files =
   List.iter
@@ -374,7 +383,7 @@ let rewrite_step n total defs (name, rewriter) =
       begin
         let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in
         (* output "" Lem_ast_out [filename, defs]; *)
-        let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in
+        let ((ot,_,_,_) as ext_ot) = open_output_with_check_unformatted None filename in
         Pretty_print_sail.pp_defs ot defs;
         close_output_with_check ext_ot;
         opt_ddump_rewrite_ast := Some (f, i + 1)