diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 23 |
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"]; |