add -coq_alt_modules option to override the default imported modules

2 files changed, 13 insertions, 3 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 8b542445..6dc6384d 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -54,6 +54,7 @@ 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
+let opt_alt_modules_coq = ref ([]:string list)
 
 type out_type =
   | Lem_out of string list
@@ -330,12 +331,12 @@ let output_lem filename libs type_env defs =
   print ol isa_lemmas;
   close_output_with_check ext_ol
 
-let output_coq opt_dir filename libs defs =
+let output_coq opt_dir filename alt_modules 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
   let operators_module = "Sail2_operators_mwords" in
-  let base_imports = [
+  let base_imports_default = [
       "Sail2_instr_kinds";
       "Sail2_values";
       "Sail2_string";
@@ -343,6 +344,11 @@ let output_coq opt_dir filename libs defs =
       operators_module
     ] @ monad_modules
   in
+  let base_imports =
+    (match alt_modules with
+    | [] -> base_imports_default
+    | _ -> Str.split (Str.regexp "[ \t]+") (String.concat " " alt_modules)
+    ) in  
   let ((ot,_,_,_) as ext_ot) =
     open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in
   let ((o,_,_,_) as ext_o) =
@@ -364,7 +370,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 !opt_coq_output_dir f' libs defs
+     output_coq !opt_coq_output_dir f' !opt_alt_modules_coq libs defs
 
 let output libpath out_arg files =
   List.iter
diff --git a/src/sail.ml b/src/sail.ml
index 516b3726..06136ca2 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -66,6 +66,7 @@ let opt_smt_serialize = ref false
 let opt_smt_fuzz = ref false
 let opt_libs_lem = ref ([]:string list)
 let opt_libs_coq = ref ([]:string list)
+let opt_alt_modules_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)
@@ -251,6 +252,9 @@ let options = Arg.align ([
   ( "-coq_lib",
     Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq),
     "<filename> provide additional library to open in Coq output");
+  ( "-coq_alt_modules",
+    Arg.String (fun l -> opt_alt_modules_coq := l::!opt_alt_modules_coq),
+    "<filename> provide alternative modules to use in Coq output");
   ( "-dcoq_undef_axioms",
     Arg.Set Pretty_print_coq.opt_undef_axioms,
     " generate axioms for functions that are declared but not defined");