diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/sail.ml b/src/sail.ml index 85719f4d..f459d774 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -62,9 +62,11 @@ let opt_print_lem = ref false let opt_print_ocaml = ref false let opt_print_c = ref false let opt_print_latex = ref false +let opt_print_coq = ref false let opt_memo_z3 = ref false let opt_sanity = ref false let opt_libs_lem = ref ([]:string list) +let opt_libs_coq = ref ([]:string list) let opt_file_arguments = ref ([]:string list) let opt_mono_split = ref ([]:((string * int) * string) list) let opt_process_elf : string option ref = ref None @@ -120,6 +122,12 @@ let options = Arg.align ([ ( "-lem_mwords", Arg.Set Pretty_print_lem.opt_mwords, " use native machine word library for Lem output"); + ( "-coq", + Arg.Set opt_print_coq, + " output a Coq translated version of the input"); + ( "-coq_lib", + Arg.String (fun l -> opt_libs_coq := l::!opt_libs_coq), + "<filename> provide additional library to open in Coq output"); ( "-latex_prefix", Arg.String (fun prefix -> Latex.opt_prefix_latex := prefix), " set a custom prefix for generated latex command (default sail)"); @@ -149,6 +157,9 @@ let options = Arg.align ([ ( "-enum_casts", Arg.Set Initial_check.opt_enum_casts, " allow enumerations to be automatically casted to numeric range types"); + ( "-no_lexp_bounds_check", + Arg.Set Type_check.opt_no_lexp_bounds_check, + " turn off bounds checking for vector assignments in l-expressions"); ( "-no_effects", Arg.Set Type_check.opt_no_effects, " (experimental) turn off effect checking"); @@ -310,6 +321,12 @@ let main() = let ast_lem = rewrite_ast_lem ast_lem in output "" (Lem_out (!opt_libs_lem)) [out_name,ast_lem] else ()); + (if !(opt_print_coq) + then + let type_envs, ast_coq = State.add_regstate_defs true type_envs ast in + let ast_coq = rewrite_ast_coq ast_coq in + output "" (Coq_out (!opt_libs_coq)) [out_name,ast_coq] + else ()); (if !(opt_print_latex) then begin |