diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/process_file.ml | 48 | ||||
| -rw-r--r-- | src/process_file.mli | 3 | ||||
| -rw-r--r-- | src/sail.ml | 6 |
3 files changed, 37 insertions, 20 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index ca013077..38e60ff8 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -51,6 +51,9 @@ open PPrint open Pretty_print_common +let opt_lem_output_dir = ref None +let opt_coq_output_dir = ref None + type out_type = | Lem_out of string list | Coq_out of string list @@ -254,19 +257,24 @@ let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tanno (ast, env) -let open_output_with_check file_name = +let open_output_with_check opt_dir file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in let o' = Format.formatter_of_out_channel o in - (o', (o, temp_file_name, file_name)) + (o', (o, temp_file_name, opt_dir, file_name)) -let open_output_with_check_unformatted file_name = +let open_output_with_check_unformatted opt_dir file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in - (o, temp_file_name, file_name) + (o, temp_file_name, opt_dir, file_name) let always_replace_files = ref true -let close_output_with_check (o, temp_file_name, file_name) = +let close_output_with_check (o, temp_file_name, opt_dir, file_name) = let _ = close_out o in + let file_name = match opt_dir with + | None -> file_name + | Some dir -> if Sys.file_exists dir then () + else Unix.mkdir dir 0o775; + Filename.concat dir file_name in let do_replace = !always_replace_files || (not (Util.same_content_files temp_file_name file_name)) in let _ = if (not do_replace) then Sys.remove temp_file_name else Util.move_file temp_file_name file_name in @@ -275,7 +283,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 opt_dir 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 @@ -308,22 +316,22 @@ let output_lem filename libs defs = string "end" ] ^^ hardline in - let ((ot,_, _) as ext_ot) = - open_output_with_check_unformatted (filename ^ "_types" ^ ".lem") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (filename ^ ".lem") in + let ((ot,_,_,_) as ext_ot) = + open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".lem") in + let ((o,_,_,_) as ext_o) = + open_output_with_check_unformatted opt_dir (filename ^ ".lem") in (Pretty_print.pp_defs_lem (ot, base_imports) (o, base_imports @ (String.capitalize_ascii types_module :: libs)) defs generated_line); close_output_with_check ext_ot; close_output_with_check ext_o; - let ((ol, _, _) as ext_ol) = - open_output_with_check_unformatted (isa_thy_name ^ ".thy") in + let ((ol,_,_,_) as ext_ol) = + open_output_with_check_unformatted opt_dir (isa_thy_name ^ ".thy") in print ol isa_lemmas; close_output_with_check ext_ol -let output_coq filename libs defs = +let output_coq opt_dir filename libs defs = let generated_line = generated_line filename in let types_module = (filename ^ "_types") in let monad_modules = ["Sail2_prompt_monad"; "Sail2_prompt"; "Sail2_state"] in @@ -336,10 +344,10 @@ let output_coq filename libs defs = operators_module ] @ monad_modules in - let ((ot,_, _) as ext_ot) = - open_output_with_check_unformatted (filename ^ "_types" ^ ".v") in - let ((o,_, _) as ext_o) = - open_output_with_check_unformatted (filename ^ ".v") in + let ((ot,_,_,_) as ext_ot) = + open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in + let ((o,_,_,_) as ext_o) = + open_output_with_check_unformatted opt_dir (filename ^ ".v") in (Pretty_print_coq.pp_defs_coq (ot, base_imports) (o, base_imports @ (types_module :: libs)) @@ -355,9 +363,9 @@ 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 f' libs defs + output_lem !opt_lem_output_dir f' libs defs | Coq_out libs -> - output_coq f' libs defs + output_coq !opt_coq_output_dir f' libs defs let output libpath out_arg files = List.iter @@ -374,7 +382,7 @@ let rewrite_step defs (name, rewriter) = begin let filename = f ^ "_rewrite_" ^ string_of_int i ^ "_" ^ name ^ ".sail" in (* output "" Lem_ast_out [filename, defs]; *) - let ((ot,_, _) as ext_ot) = open_output_with_check_unformatted filename in + let ((ot,_,_,_) as ext_ot) = open_output_with_check_unformatted None filename in Pretty_print_sail.pp_defs ot defs; close_output_with_check ext_ot; opt_ddump_rewrite_ast := Some (f, i + 1) diff --git a/src/process_file.mli b/src/process_file.mli index 1d4d629a..2c4973bc 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -71,6 +71,9 @@ val opt_ddump_tc_ast : bool ref 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_coq_output_dir : (string option) ref + type out_type = | Lem_out of string list (* If present, the strings are files to open in the lem backend*) | Coq_out of string list (* If present, the strings are files to open in the coq backend*) diff --git a/src/sail.ml b/src/sail.ml index 59190d15..3e89f39d 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -150,6 +150,9 @@ let options = Arg.align ([ ( "-lem", Arg.Set opt_print_lem, " output a Lem translated version of the input"); + ( "-lem_output_dir", + Arg.String (fun dir -> Process_file.opt_lem_output_dir := Some dir), + " set a custom directory to output generated Lem"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), "<filename> provide additional library to open in Lem output"); @@ -162,6 +165,9 @@ let options = Arg.align ([ ( "-coq", Arg.Set opt_print_coq, " output a Coq translated version of the input"); + ( "-coq_output_dir", + Arg.String (fun dir -> Process_file.opt_coq_output_dir := Some dir), + " set a custom directory to output generated Coq"); ( "-coq_lib", Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq), "<filename> provide additional library to open in Coq output"); |