diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/process_file.ml | 11 | ||||
| -rw-r--r-- | src/process_file.mli | 1 | ||||
| -rw-r--r-- | src/sail.ml | 3 |
3 files changed, 10 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 diff --git a/src/process_file.mli b/src/process_file.mli index 2c4973bc..e209c829 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -72,6 +72,7 @@ val opt_ddump_rewrite_ast : ((string * int) option) ref val opt_dno_cast : bool ref val opt_lem_output_dir : (string option) ref +val opt_isa_output_dir : (string option) ref val opt_coq_output_dir : (string option) ref type out_type = diff --git a/src/sail.ml b/src/sail.ml index a5cac041..920542bc 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -156,6 +156,9 @@ let options = Arg.align ([ ( "-lem_output_dir", Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir), " set a custom directory to output generated Lem"); + ( "-isa_output_dir", + Arg.String (fun dir -> Process_file.opt_isa_output_dir := Some dir), + " set a custom directory to output generated Isabelle auxiliary theories"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), "<filename> provide additional library to open in Lem output"); |