Begin refactoring Sail library

- Add back support for bit list representation of bit vectors, for backwards
  compatibility in order to ease integration with the interpreter.  For this
purpose, split out a file sail_operators.lem from sail_values.lem, and add a
variant sail_operators_mwords.lem for the machine word representation of
bitvectors.  Currently, Sail is hardcoded to use machine words for the
sequential state monad, and bit lists for the free monad, but this could be
turned into a command line flag.

- Add a prelude_wrappers.sail file for glueing the Sail prelude to the Lem
  library.  The wrappers make use of sizeof expressions to extract type
information from bitvectors (length, start index) in order to pass it to the
Lem functions.

- Add early return support to the free monad, using a new constructor "Return
  of 'r".  As with the sequential monad, functions with early return are
wrapped into "catch_early_return", which extracts the return value at the end
of the function execution.

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"];