diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/src/sail.ml b/src/sail.ml index 9bb7cfcb..41ca792c 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -52,6 +52,7 @@ open Process_file let lib = ref ([] : string list) let opt_file_out : string option ref = ref None +let opt_interactive = ref false let opt_print_version = ref false let opt_print_initial_env = ref false let opt_print_verbose = ref false @@ -59,7 +60,6 @@ let opt_print_lem_ast = ref false let opt_print_lem = ref false let opt_print_sil = ref false let opt_print_ocaml = ref false -let opt_convert = ref false let opt_memo_z3 = ref false let opt_sanity = ref false let opt_libs_lem = ref ([]:string list) @@ -71,6 +71,9 @@ let options = Arg.align ([ ( "-o", Arg.String (fun f -> opt_file_out := Some f), "<prefix> select output filename prefix"); + ( "-i", + Arg.Tuple [Arg.Set opt_interactive; Arg.Set Initial_check.opt_undefined_gen], + " start interactive interpreter"); ( "-ocaml", Arg.Tuple [Arg.Set opt_print_ocaml; Arg.Set Initial_check.opt_undefined_gen], " output an OCaml translated version of the input"); @@ -114,12 +117,6 @@ let options = Arg.align ([ ( "-no_effects", Arg.Set Type_check.opt_no_effects, " (experimental) turn off effect checking"); - ( "-new_parser", - Arg.Set Process_file.opt_new_parser, - " (experimental) use new parser"); - ( "-convert", - Arg.Set opt_convert, - " (experimental) convert sail to new syntax for use with -new_parser"); ( "-just_check", Arg.Set opt_just_check, " (experimental) terminate immediately after typechecking"); @@ -169,6 +166,8 @@ let _ = opt_file_arguments := (!opt_file_arguments) @ [s]) usage_msg +let interactive_ast = ref (Ast.Defs []) +let interactive_env = ref Type_check.initial_env let main() = if !opt_print_version @@ -182,10 +181,6 @@ let main() = -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in let ast = convert_ast Ast_util.inc_ord ast in - if !opt_convert - then (Pretty_print_sail2.pp_defs stdout ast; exit 0) - else (); - let (ast, type_envs) = check_ast ast in let (ast, type_envs) = @@ -208,13 +203,17 @@ let main() = (*let _ = Printf.eprintf "Type checked, next to pretty print" in*) begin + (if !(opt_interactive) + then + (interactive_ast := Process_file.rewrite_ast_interpreter ast; interactive_env := type_envs) + else ()); (if !(opt_sanity) then let _ = rewrite_ast_check ast in () else ()); (if !(opt_print_verbose) - then ((Pretty_print.pp_defs stdout) ast) + then ((Pretty_print_sail.pp_defs stdout) ast) else ()); (if !(opt_print_lem_ast) then output "" Lem_ast_out [out_name,ast] @@ -222,7 +221,7 @@ let main() = (if !(opt_print_sil) then let ast = rewrite_ast_sil ast in - Pretty_print_sail2.pp_defs stdout ast + Pretty_print_sail.pp_defs stdout ast else ()); (if !(opt_print_ocaml) then |