additional option to tweak Coq output to support user-defined monad:

 -coq_alt_modules2 <filename>             provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default definitions of MR and M monads

4 files changed, 19 insertions, 8 deletions

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 3d50d48c..bbee8fdc 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -3149,7 +3149,7 @@ let find_unimplemented defs =
   in
   List.fold_left adjust_def IdSet.empty defs
 
-let pp_defs_coq (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line =
+let pp_defs_coq (types_file,types_modules) (defs_file,defs_modules) (Defs defs) top_line suppress_MR_M =
 try
   (* let regtypes = find_regtypes d in *)
   let state_ids =
@@ -3189,10 +3189,10 @@ try
         separate empty (List.map doc_def statedefs); hardline;
         hardline;
         register_refs; hardline;
-        concat [
+        (if suppress_MR_M then empty else concat [
           string ("Definition MR a r := monadR register_value a r " ^ exc_typ ^ "."); hardline;
           string ("Definition M a := monad register_value a " ^ exc_typ ^ "."); hardline
-        ]
+        ])
         ]);
   (print defs_file)
     (concat
diff --git a/src/process_file.ml b/src/process_file.ml
index 6dc6384d..eeb7c0d7 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -55,6 +55,7 @@ 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)
+let opt_alt_modules2_coq = ref ([]:string list)
 
 type out_type =
   | Lem_out of string list
@@ -331,7 +332,7 @@ let output_lem filename libs type_env defs =
   print ol isa_lemmas;
   close_output_with_check ext_ol
 
-let output_coq opt_dir filename alt_modules libs defs =
+let output_coq opt_dir filename alt_modules alt_modules2 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
@@ -349,14 +350,20 @@ let output_coq opt_dir filename alt_modules libs defs =
     | [] -> base_imports_default
     | _ -> Str.split (Str.regexp "[ \t]+") (String.concat " " alt_modules)
     ) in  
+  let alt_modules2_imports =
+    (match alt_modules2 with
+    | [] -> []
+    | _ -> Str.split (Str.regexp "[ \t]+") (String.concat " " alt_modules2)
+    ) 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))
-     defs generated_line);
+     (o, base_imports @ (types_module :: libs) @ alt_modules2)
+     defs generated_line)
+     (alt_modules2 <> []); (* suppress MR and M defns if alt_modules2 present*)
   close_output_with_check ext_ot;
   close_output_with_check ext_o
 
@@ -370,7 +377,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' !opt_alt_modules_coq libs defs
+     output_coq !opt_coq_output_dir f' !opt_alt_modules_coq !opt_alt_modules2_coq libs defs
 
 let output libpath out_arg files =
   List.iter
diff --git a/src/process_file.mli b/src/process_file.mli
index 6d865867..fa0aeb31 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -73,6 +73,7 @@ val opt_lem_output_dir : (string option) ref
 val opt_isa_output_dir : (string option) ref
 val opt_coq_output_dir : (string option) ref
 val opt_alt_modules_coq : (string list) ref
+val opt_alt_modules2_coq : (string list) ref
 
 type out_type =
   | Lem_out of string list (* If present, the strings are files to open in the lem backend*)
diff --git a/src/sail.ml b/src/sail.ml
index adf61393..21075818 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -253,7 +253,10 @@ let options = Arg.align ([
     "<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");
+    "<filename> provide alternative modules to open in Coq output");
+  ( "-coq_alt_modules2",
+    Arg.String (fun l -> opt_alt_modules2_coq := l::!opt_alt_modules2_coq),
+    "<filename> provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default definitions of MR and M monads");
   ( "-dcoq_undef_axioms",
     Arg.Set Pretty_print_coq.opt_undef_axioms,
     " generate axioms for functions that are declared but not defined");