Merge branch 'experiments' of https://bitbucket.org/Peter_Sewell/sail into experiments

1 files changed, 13 insertions, 10 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 6a3fc24c..46b6538e 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -134,10 +134,11 @@ let close_output_with_check (o, temp_file_name, file_name) =
 let generated_line f =
   Printf.sprintf "Generated by Sail from %s." f
 
-let output_lem filename libs libs_seq defs =
+let output_lem filename libs defs =
   let generated_line = generated_line filename in
   let types_module = (filename ^ "_embed_types") in
-  let types_module_sequential = (filename ^ "_embed_types_sequential") in
+  let types_module_seq = (filename ^ "_embed_types_sequential") in
+  let libs_seq = List.map (fun lib -> lib ^ "_sequential") libs in
   let ((ot,_, _) as ext_ot) =
     open_output_with_check_unformatted (filename ^ "_embed_types.lem") in
   let ((ots,_, _) as ext_ots) =
@@ -146,13 +147,15 @@ let output_lem filename libs libs_seq defs =
     open_output_with_check_unformatted (filename ^ "_embed.lem") in
   let ((os,_, _) as ext_os) =
     open_output_with_check_unformatted (filename ^ "_embed_sequential.lem") in
-  (Pretty_print.pp_defs_lem
-     (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Prompt"])
-     (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State"])
-     (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Prompt";
+  (Pretty_print.pp_defs_lem false false
+     (ot,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt"])
+     (o,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators";"Prompt";
        String.capitalize types_module] @ libs)
-     (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State";
-       String.capitalize types_module_sequential] @ libs_seq)
+     defs generated_line);
+  (Pretty_print.pp_defs_lem true true
+     (ots,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State"])
+     (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"Sail_operators_mwords";"State";
+       String.capitalize types_module_seq] @ libs_seq)
      defs generated_line);
   close_output_with_check ext_ot;
   close_output_with_check ext_ots;
@@ -205,9 +208,9 @@ let output1 libpath out_arg filename defs  =
 	  close_output_with_check ext_o
 	end
       | Lem_out None ->
-        output_lem f' [] [] defs
+        output_lem f' [] defs
       | Lem_out (Some lib) ->
-        output_lem f' [lib] [lib ^ "_sequential"] defs
+        output_lem f' [lib] defs
       | 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"];