diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 785d7a18..ed34238b 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -275,7 +275,7 @@ 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 defs = +let output_lem filename libs type_env defs = let generated_line = generated_line filename in (* let seq_suffix = if !Pretty_print_lem.opt_sequential then "_sequential" else "" in *) let types_module = (filename ^ "_types") in @@ -315,7 +315,7 @@ let output_lem filename libs defs = (Pretty_print.pp_defs_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) - defs generated_line); + type_env defs generated_line); close_output_with_check ext_ot; close_output_with_check ext_o; let ((ol, _, _) as ext_ol) = @@ -351,18 +351,18 @@ let rec iterate (f : int -> unit) (n : int) : unit = if n = 0 then () else (f n; iterate f (n - 1)) -let output1 libpath out_arg filename defs = +let output1 libpath out_arg filename type_env defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with | Lem_out libs -> - output_lem f' libs defs + output_lem f' libs type_env defs | Coq_out libs -> output_coq f' libs defs let output libpath out_arg files = List.iter - (fun (f, defs) -> - output1 libpath out_arg f defs) + (fun (f, type_env, defs) -> + output1 libpath out_arg f type_env defs) files let rewrite_step n total defs (name, rewriter) = |