add option -lem_sequential for producing shallow embedding that refers to state monad, library fixes

1 files changed, 13 insertions, 0 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 3012b288..6270cb66 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -49,6 +49,7 @@ open Type_internal
 type out_type =
   | Lem_ast_out
   | Lem_out of string option
+  | Lem_sequential_out of string option
   | Ocaml_out of string option
 
 let get_lexbuf fn =
@@ -185,6 +186,18 @@ let output1 libpath out_arg filename defs  =
 	 (Pretty_print.pp_defs_lem o defs (generated_line filename))
            ["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values";lib];
          close_output_with_check ext_o;
+      | Lem_sequential_out None ->
+         let ((o,_, _) as ext_o) =
+           open_output_with_check_unformatted (f' ^ "_sequential_embedded.lem") in
+         (Pretty_print.pp_defs_lem o defs (generated_line filename))
+           ["Pervasives_extra";"Sail_impl_base";"State";"Sail_values"];
+         close_output_with_check ext_o
+      | Lem_sequential_out (Some lib) ->
+         let ((o,_, _) as ext_o) =
+           open_output_with_check_unformatted (f' ^ "_sequential_embedded.lem") in
+	 (Pretty_print.pp_defs_lem o defs (generated_line filename))
+           ["Pervasives_extra";"Sail_impl_base";"State";"Sail_values";lib];
+         close_output_with_check ext_o;
       | Ocaml_out None ->
         let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ ".ml") in
 	begin Pretty_print.pp_defs_ocaml o defs (generated_line filename) ["Big_int_Z";"Sail_values"];