progress on lem backend: auto-generate read_register and write_register functions, and state definition

1 files changed, 14 insertions, 7 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 135f0931..1a776cff 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -173,14 +173,21 @@ let output1 libpath out_arg filename defs (* alldoc_accum alldoc_inc_accum alldo
 	  close_output_with_check ext_o
 	end
       | Lem_out None ->
-        let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ "embed.lem") in
-	begin Pretty_print.pp_defs_lem o defs (generated_line filename) ["Sail_values";];
-        close_output_with_check ext_o
-        end
+         let ((o1,_, _) as ext_o1) =
+           open_output_with_check_unformatted ("arch.lem") in
+         let ((o2,_, _) as ext_o2) =
+           open_output_with_check_unformatted (f' ^ "embed.lem") in
+         Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename) ["Sail_values"];
+         close_output_with_check ext_o1;
+         close_output_with_check ext_o2
       | Lem_out (Some lib) ->
-        let ((o,temp_file_name, _) as ext_o) = open_output_with_check_unformatted (f' ^ "embed.lem") in
-	Pretty_print.pp_defs_lem o defs (generated_line filename) ["Sail_values"; lib];
-        close_output_with_check ext_o
+         let ((o1,_, _) as ext_o1) =
+           open_output_with_check_unformatted ("arch.lem") in
+         let ((o2,_, _) as ext_o2) =
+           open_output_with_check_unformatted (f' ^ "embed.lem") in
+	 Pretty_print.pp_defs_lem o1 o2 defs (generated_line filename) ["Sail_values"; lib];
+         close_output_with_check ext_o1;
+         close_output_with_check ext_o2
       | 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"];