add -coq_alt_modules option to override the default imported modules

1 files changed, 9 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