diff options
Diffstat (limited to 'src/sail.ml')
| -rw-r--r-- | src/sail.ml | 64 |
1 files changed, 38 insertions, 26 deletions
diff --git a/src/sail.ml b/src/sail.ml index 4e76551f..3500b213 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -53,6 +53,7 @@ let opt_print_ocaml = ref false let opt_libs_lem = ref ([]:string list) let opt_libs_ocaml = ref ([]:string list) let opt_file_arguments = ref ([]:string list) +let opt_mono_split = ref ([]:((string * int) * string) list) let options = Arg.align ([ ( "-o", Arg.String (fun f -> opt_file_out := Some f), @@ -77,15 +78,34 @@ let options = Arg.align ([ Arg.String (fun l -> lib := l::!lib), "<library_filename> treat this file as input only and generate no output for it"); *) - ( "-print_initial_env", - Arg.Set opt_print_initial_env, - " print the built-in initial type environment and terminate"); ( "-verbose", Arg.Set opt_print_verbose, " (debug) pretty-print the input to standard output"); - ( "-skip_constraints", - Arg.Clear Type_internal.do_resolve_constraints, - " (debug) skip constraint resolution in type-checking"); + ( "-mono-split", + Arg.String (fun s -> + let l = Util.split_on_char ':' s in + match l with + | [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split + | _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))), + "<filename>:<line>:<variable> to case split for monomorphisation"); + ( "-new_typecheck", + Arg.Set opt_new_typecheck, + " (experimental) use new typechecker with Z3 constraint solving"); + ( "-just_check", + Arg.Tuple [Arg.Set opt_new_typecheck; Arg.Set opt_just_check], + " (experimental) terminate immediately after typechecking, implies -new_typecheck"); + ( "-ddump_tc_ast", + Arg.Set opt_ddump_tc_ast, + " (debug) dump the typechecked ast to stdout"); + ( "-dtc_verbose", + Arg.Int (fun verbosity -> Type_check.opt_tc_debug := verbosity), + " (debug) verbose typechecker output: 0 is silent"); + ( "-dno_cast", + Arg.Set opt_dno_cast, + " (debug) typecheck without any implicit casting"); + ( "-no_effects", + Arg.Set Type_check.opt_no_effects, + " turn off effect checking"); ( "-v", Arg.Set opt_print_version, " print version"); @@ -106,35 +126,27 @@ let _ = let main() = if !(opt_print_version) then Printf.printf "Sail private release \n" - else if !(opt_print_initial_env) then - let ppd_initial_typ_env = - String.concat "" - (List.map - (function (comment,tenv) -> - "(* "^comment^" *)\n" ^ - String.concat "" - (List.map - (function (id,tannot) -> - id ^ " : " ^ - Pretty_print.pp_format_annot_ascii tannot - ^ "\n") - tenv)) - Type_internal.initial_typ_env_list) in - Printf.printf "%s" ppd_initial_typ_env ; - else + else let parsed = (List.map (fun f -> (f,(parse_file f))) !opt_file_arguments) in - let ast = + let ast = List.fold_right (fun (_,(Parse_ast.Defs ast_nodes)) (Parse_ast.Defs later_nodes) -> Parse_ast.Defs (ast_nodes@later_nodes)) parsed (Parse_ast.Defs []) in - let (ast,kenv,ord) = convert_ast ast in - let (ast,type_envs) = check_ast ast kenv ord in + let ast = convert_ast ast in + let (ast, type_envs) = check_ast ast in + + let (ast, type_envs) = + match !opt_mono_split with + | [] -> ast, type_envs + | locs -> monomorphise_ast locs ast + in + let ast = rewrite_ast ast in let out_name = match !opt_file_out with | None -> fst (List.hd parsed) | Some f -> f ^ ".sail" in (*let _ = Printf.eprintf "Type checked, next to pretty print" in*) - begin + begin (if !(opt_print_verbose) then ((Pretty_print.pp_defs stdout) ast) else ()); |