diff options
| -rw-r--r-- | aarch64_small/Makefile | 2 | ||||
| -rw-r--r-- | src/process_file.ml | 12 | ||||
| -rw-r--r-- | src/sail.ml | 4 |
3 files changed, 14 insertions, 4 deletions
diff --git a/aarch64_small/Makefile b/aarch64_small/Makefile index 2e7c1a7b..e08e51b6 100644 --- a/aarch64_small/Makefile +++ b/aarch64_small/Makefile @@ -1,4 +1,4 @@ -SAIL:=../sail -Ofast_undefined +SAIL:=sail -Ofast_undefined LEM:=../../lem/lem LEM_ISA_LIB?=$(shell opam config var lem:share)/isabelle-lib diff --git a/src/process_file.ml b/src/process_file.ml index 8b542445..6dc6384d 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -54,6 +54,7 @@ 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 +let opt_alt_modules_coq = ref ([]:string list) type out_type = | Lem_out of string list @@ -330,12 +331,12 @@ let output_lem filename libs type_env defs = print ol isa_lemmas; close_output_with_check ext_ol -let output_coq opt_dir filename libs defs = +let output_coq opt_dir filename alt_modules 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 let operators_module = "Sail2_operators_mwords" in - let base_imports = [ + let base_imports_default = [ "Sail2_instr_kinds"; "Sail2_values"; "Sail2_string"; @@ -343,6 +344,11 @@ let output_coq opt_dir filename libs defs = operators_module ] @ monad_modules in + let base_imports = + (match alt_modules with + | [] -> base_imports_default + | _ -> Str.split (Str.regexp "[ \t]+") (String.concat " " alt_modules) + ) in let ((ot,_,_,_) as ext_ot) = open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in let ((o,_,_,_) as ext_o) = @@ -364,7 +370,7 @@ let output1 libpath out_arg filename type_env defs = | Lem_out libs -> output_lem f' libs type_env defs | Coq_out libs -> - output_coq !opt_coq_output_dir f' libs defs + output_coq !opt_coq_output_dir f' !opt_alt_modules_coq libs defs let output libpath out_arg files = List.iter diff --git a/src/sail.ml b/src/sail.ml index 516b3726..06136ca2 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -66,6 +66,7 @@ let opt_smt_serialize = ref false let opt_smt_fuzz = ref false let opt_libs_lem = ref ([]:string list) let opt_libs_coq = ref ([]:string list) +let opt_alt_modules_coq = ref ([]:string list) let opt_file_arguments = ref ([]:string list) let opt_process_elf : string option ref = ref None let opt_ocaml_generators = ref ([]:string list) @@ -251,6 +252,9 @@ let options = Arg.align ([ ( "-coq_lib", Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq), "<filename> provide additional library to open in Coq output"); + ( "-coq_alt_modules", + Arg.String (fun l -> opt_alt_modules_coq := l::!opt_alt_modules_coq), + "<filename> provide alternative modules to use in Coq output"); ( "-dcoq_undef_axioms", Arg.Set Pretty_print_coq.opt_undef_axioms, " generate axioms for functions that are declared but not defined"); |