diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/src/sail.ml b/src/sail.ml index 5e979738..b63f807c 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -65,7 +65,7 @@ let options = Arg.align ([ Arg.Set opt_print_lem, " output a Lem translated version of the input"); ( "-ocaml", - Arg.Set opt_print_ocaml, + Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen], " output an OCaml translated version of the input"); ( "-lem_lib", Arg.String (fun l -> opt_libs_lem := l::!opt_libs_lem), @@ -73,6 +73,12 @@ let options = Arg.align ([ ( "-ocaml_lib", Arg.String (fun l -> opt_libs_ocaml := l::!opt_libs_ocaml), "<filename> provide additional library to open in OCaml output"); + ( "-lem_sequential", + Arg.Set Process_file.opt_lem_sequential, + " use sequential state monad for Lem output"); + ( "-lem_mwords", + Arg.Set Process_file.opt_lem_mwords, + " use native machine word library for Lem output"); (* ( "-i", Arg.String (fun l -> lib := l::!lib), @@ -93,7 +99,7 @@ let options = Arg.align ([ " (experimental) use new parser"); ( "-just_check", Arg.Set opt_just_check, - " (experimental) terminate immediately after typechecking, implies -new_typecheck"); + " (experimental) terminate immediately after typechecking"); ( "-ddump_tc_ast", Arg.Set opt_ddump_tc_ast, " (debug) dump the typechecked ast to stdout"); @@ -109,6 +115,9 @@ let options = Arg.align ([ ( "-no_effects", Arg.Set Type_check.opt_no_effects, " turn off effect checking"); + ( "-undefined-gen", + Arg.Set Initial_check.opt_undefined_gen, + " generate undefined_type functions for types in the specification"); ( "-v", Arg.Set opt_print_version, " print version"); |