diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 65 |
1 files changed, 29 insertions, 36 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 6d4bcea0..1c133ce8 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -134,6 +134,31 @@ 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 generated_line = generated_line filename in + let types_module = (filename ^ "_embed_types") in + let types_module_sequential = (filename ^ "_embed_types_sequential") in + let ((ot,_, _) as ext_ot) = + open_output_with_check_unformatted (filename ^ "_embed_types.lem") in + let ((ots,_, _) as ext_ots) = + open_output_with_check_unformatted (filename ^ "_embed_types_sequential.lem") in + let ((o,_, _) as ext_o) = + 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"; + String.capitalize types_module] @ libs) + (os,["Pervasives_extra";"Sail_impl_base";"Sail_values";"State"; + String.capitalize types_module_sequential] @ libs_seq) + defs generated_line); + close_output_with_check ext_ot; + close_output_with_check ext_ots; + close_output_with_check ext_o; + close_output_with_check ext_os + let output1 libpath out_arg filename defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with @@ -180,43 +205,9 @@ 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' ^ "_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"]) - (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; - close_output_with_check ext_o'; - close_output_with_check ext_o''; + output_lem f' [] [] defs | 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' ^ "_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"]) - (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'' + output_lem f' [lib] [lib ^ "_sequential"] 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"]; @@ -234,6 +225,8 @@ let output libpath out_arg files = files let rewrite_step defs rewriter = + (* print_endline "=============================== REWRITE STEP"; + Pretty_print.pp_defs stdout defs; *) let defs = rewriter defs in let _ = match !(opt_ddump_rewrite_ast) with | Some (f, i) -> |