make sail produce prompt and state version of shallow embedding files at the same time with the types both have in common factored out into separate file, rename one mips shallow embedding _extras file as required by this

6 files changed, 64 insertions, 55 deletions

diff --git a/src/Makefile b/src/Makefile
index 4f16f2b9..573bef36 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -60,16 +60,11 @@ _build/mips.lem: $(MIPS_SAILS) ./sail.native
 	cd _build ;\
 	../sail.native -lem_ast -o mips $(MIPS_SAILS)
 
-_build/mips_embedded.lem: $(MIPS_SAILS) ./sail.native
+_build/mips_embed_types.lem: $(MIPS_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
 	../sail.native -lem_lib "Mips_extras_embed" -lem -o mips $(MIPS_NOTLB_SAILS)
 
-_build/mips_sequential_embedded.lem: $(MIPS_SAILS) ./sail.native
-	mkdir -p _build
-	cd _build ;\
-	../sail.native -lem_lib "Mips_extras_sequential_embed" -lem_sequential -o mips $(MIPS_NOTLB_SAILS)
-
 _build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ; \
@@ -101,7 +96,7 @@ run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml int
 run_cheri.native:  _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
 	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml  -o run_cheri.native
 
-mips_notlb: _build/mips_notlb.ml  _build/mips_embedded.lem _build/mips_sequential_embedded.lem _build/mips_extras.ml
+mips_notlb: _build/mips_notlb.ml  _build/mips_embed_types.lem _build/mips_extras.ml
 	true
 
 mips: elf run_mips.native
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 65650a33..9c9ad1f4 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -3057,17 +3057,19 @@ let doc_spec_lem regtypes (VS_aux (valspec,annot)) =
 
 
 let doc_def_lem regtypes def = match def with
-  | DEF_default df -> empty
-  | DEF_spec v_spec -> doc_spec_lem regtypes v_spec
-  | DEF_type t_def -> group (doc_typdef_lem regtypes t_def) ^/^ hardline
-  | DEF_fundef f_def -> group (doc_fundef_lem regtypes f_def) ^/^ hardline
-  | DEF_val lbind -> group (doc_let_lem regtypes lbind) ^/^ hardline
-  | DEF_reg_dec dec -> group (doc_dec_lem dec)
+  | DEF_spec v_spec -> (doc_spec_lem regtypes v_spec,empty)
+  | DEF_type t_def -> (group (doc_typdef_lem regtypes t_def) ^/^ hardline,empty)
+  | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty)
+
+  | DEF_default df -> (empty,empty)
+  | DEF_fundef f_def -> (empty,group (doc_fundef_lem regtypes f_def) ^/^ hardline)
+  | DEF_val lbind -> (empty,group (doc_let_lem regtypes lbind) ^/^ hardline)
   | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point"
 
 
 let doc_defs_lem regtypes (Defs defs) =
-  separate_map empty (doc_def_lem regtypes) defs
+  let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in
+  (separate empty typdefs,separate empty valdefs)
 
 let find_regtypes (Defs defs) =
   List.fold_left
@@ -3081,14 +3083,14 @@ let find_regtypes (Defs defs) =
 let typ_to_t env =
   Type_check.typ_to_t env false false
 
-let pp_defs_lem f d top_line opens =
+let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line =
   let regtypes = find_regtypes d in
-  let defs = doc_defs_lem regtypes d in
-  (print f)
+  let (typdefs,valdefs) = doc_defs_lem regtypes d in
+  (print types_file)
     (concat
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
         (separate_map hardline)
-          (fun lib -> separate space [string "open import";string lib]) opens;hardline;
+          (fun lib -> separate space [string "open import";string lib]) types_modules;hardline;
         (separate_map hardline)
           (fun lib -> separate space [string "     import";string lib]) ["Interp";"Interp_ast"]; hardline;
         hardline;
@@ -3096,4 +3098,18 @@ let pp_defs_lem f d top_line opens =
         string "module SIA = Interp_ast"; hardline;
         string "module SV = Sail_values"; hardline;
         hardline;
-        defs])
+        typdefs]);
+  (print prompt_file)
+    (concat
+       [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
+        (separate_map hardline)
+          (fun lib -> separate space [string "open import";string lib]) prompt_modules;hardline;
+        hardline;
+        valdefs]);
+  (print state_file)
+    (concat
+       [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
+        (separate_map hardline)
+          (fun lib -> separate space [string "open import";string lib]) state_modules;hardline;
+        hardline;
+        valdefs]);
diff --git a/src/pretty_print.mli b/src/pretty_print.mli
index 4b51db8a..500d19e2 100644
--- a/src/pretty_print.mli
+++ b/src/pretty_print.mli
@@ -10,4 +10,4 @@ val pat_to_string : tannot pat -> string
 val pp_lem_defs : Format.formatter -> tannot defs -> unit
 
 val pp_defs_ocaml : out_channel -> tannot defs -> string -> string list -> unit
-val pp_defs_lem : out_channel -> tannot defs -> string -> string list -> unit
+val pp_defs_lem : (out_channel * string list) -> (out_channel * string list) -> (out_channel * string list) -> tannot defs -> string -> unit
diff --git a/src/process_file.ml b/src/process_file.ml
index 8f5dec40..7bd7e134 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -49,7 +49,6 @@ 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 =
@@ -175,33 +174,43 @@ let output1 libpath out_arg filename defs  =
 	  close_output_with_check ext_o
 	end
       | Lem_out None ->
+         let generated_line = generated_line filename in
+         let types_module = (f' ^ "_embed_types") in
          let ((o,_, _) as ext_o) =
-           open_output_with_check_unformatted (f' ^ "_embedded.lem") in
-         (Pretty_print.pp_defs_lem o defs (generated_line filename))
-           ["Pervasives_extra";"Sail_impl_base";"Prompt";
-            "Sail_values";"Deep_shallow_convert"];
-         close_output_with_check ext_o
-      | Lem_out (Some lib) ->
-         let ((o,_, _) as ext_o) =
-           open_output_with_check_unformatted (f' ^ "_embedded.lem") in
-	 (Pretty_print.pp_defs_lem o defs (generated_line filename))
-           ["Pervasives_extra";"Sail_impl_base";"Prompt";
-            "Sail_values";"Deep_shallow_convert";lib];
+           open_output_with_check_unformatted (f' ^ "_embed_types.lem") in
+         let ((o',_, _) as ext_o') =
+           open_output_with_check_unformatted (f' ^ "_embed.lem") in
+         let ((o'',_, _) as ext_o'') =
+           open_output_with_check_unformatted (f' ^ "embed_sequential.lem") in
+	 (Pretty_print.pp_defs_lem
+            (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Deep_shallow_convert"])
+            (o',["Pervasives_extra";"Sail_impl_base";"Prompt";"Sail_values";
+            String.capitalize types_module])
+            (o'',["Pervasives_extra";"Sail_impl_base";"State";"Sail_values";
+            String.capitalize types_module])
+            defs generated_line);
          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";"Deep_shallow_convert"];
-         close_output_with_check ext_o
-      | Lem_sequential_out (Some lib) ->
+         close_output_with_check ext_o';
+         close_output_with_check ext_o'';
+      | Lem_out (Some lib) ->
+         let generated_line = generated_line filename in
+         let types_module = (f' ^ "_embed_types") in
          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";"Deep_shallow_convert";lib];
+           open_output_with_check_unformatted (f' ^ "_embed_types.lem") in
+         let ((o',_, _) as ext_o') =
+           open_output_with_check_unformatted (f' ^ "_embed.lem") in
+         let ((o'',_, _) as ext_o'') =
+           open_output_with_check_unformatted (f' ^ "_embed_sequential.lem") in
+	 (Pretty_print.pp_defs_lem
+            (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Deep_shallow_convert";lib])
+            (o',["Pervasives_extra";"Sail_impl_base";"Prompt";
+                 "Sail_values";String.capitalize types_module;lib])
+            (o'',["Pervasives_extra";"Sail_impl_base";"State";
+                  "Sail_values";String.capitalize types_module;lib ^ "_sequential"])
+            defs generated_line);
          close_output_with_check ext_o;
+         close_output_with_check ext_o';
+         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"];
diff --git a/src/process_file.mli b/src/process_file.mli
index 52c5474e..66b1d8af 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -55,7 +55,6 @@ val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot As
 type out_type =
   | Lem_ast_out
   | Lem_out of string option (* If present, the string is a file to open in the lem backend*)
-  | Lem_sequential_out of string option (* If present, the string is a file to open in the lem backend*)
   | Ocaml_out of string option (* If present, the string is a file to open in the ocaml backend*)
 
 val output :
diff --git a/src/sail.ml b/src/sail.ml
index 0464fc22..80560746 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -52,7 +52,6 @@ let opt_print_version = ref false
 let opt_print_verbose = ref false
 let opt_print_lem_ast = ref false
 let opt_print_lem = ref false
-let opt_print_lem_sequential = ref false
 let opt_print_ocaml = ref false
 let opt_libs_lem = ref ([]:string list)
 let opt_libs_ocaml = ref ([]:string list)
@@ -70,9 +69,6 @@ let options = Arg.align ([
   ( "-lem",
     Arg.Set opt_print_lem,
     " print a Lem translated version of the specification to integrate with a concurrency model");
-  ( "-lem_sequential",
-    Arg.Set opt_print_lem_sequential,
-    " print a Lem translated version of the specification as a sequential model");
   ( "-ocaml",
     Arg.Set opt_print_ocaml,
     " print an Ocaml translated version of the specification");
@@ -138,12 +134,6 @@ let main() =
          then output "" (Lem_out None) [out_name,ast_lem]
          else output "" (Lem_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem]
        else ());
-      (if !(opt_print_lem_sequential)
-       then let ast_lem = rewrite_ast_lem ast in
-         if !(opt_libs_lem) = []
-         then output "" (Lem_sequential_out None) [out_name,ast_lem]
-         else output "" (Lem_sequential_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem]
-       else ())
     end
 
 let _ =  try