diff options
| author | Thomas Bauereiss | 2019-01-21 18:37:24 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-01-21 18:37:24 +0000 |
| commit | d34329753b1e8faa32a7c95ac085733555c16749 (patch) | |
| tree | d8fce99abf71a3807b193af4a17ee1ee12e041bf /src/process_file.ml | |
| parent | d2d7321afb0112142966c44a8dc4719851f20035 (diff) | |
Add output directory option for generated Isabelle auxiliary theories
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 38e60ff8..094b0ecb 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -52,6 +52,7 @@ open PPrint open Pretty_print_common let opt_lem_output_dir = ref None +let opt_isa_output_dir = ref None let opt_coq_output_dir = ref None type out_type = @@ -283,7 +284,7 @@ let close_output_with_check (o, temp_file_name, opt_dir, file_name) = let generated_line f = Printf.sprintf "Generated by Sail from %s." f -let output_lem opt_dir filename libs defs = +let output_lem filename libs 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 @@ -317,9 +318,9 @@ let output_lem opt_dir filename libs defs = ] ^^ hardline in let ((ot,_,_,_) as ext_ot) = - open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".lem") in + open_output_with_check_unformatted !opt_lem_output_dir (filename ^ "_types" ^ ".lem") in let ((o,_,_,_) as ext_o) = - open_output_with_check_unformatted opt_dir (filename ^ ".lem") in + open_output_with_check_unformatted !opt_lem_output_dir (filename ^ ".lem") in (Pretty_print.pp_defs_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) @@ -327,7 +328,7 @@ let output_lem opt_dir filename libs defs = close_output_with_check ext_ot; close_output_with_check ext_o; let ((ol,_,_,_) as ext_ol) = - open_output_with_check_unformatted opt_dir (isa_thy_name ^ ".thy") in + open_output_with_check_unformatted !opt_isa_output_dir (isa_thy_name ^ ".thy") in print ol isa_lemmas; close_output_with_check ext_ol @@ -363,7 +364,7 @@ let output1 libpath out_arg filename defs = let f' = Filename.basename (Filename.chop_extension filename) in match out_arg with | Lem_out libs -> - output_lem !opt_lem_output_dir f' libs defs + output_lem f' libs defs | Coq_out libs -> output_coq !opt_coq_output_dir f' libs defs |