1 files changed, 1 insertions, 38 deletions
diff --git a/src/sail.ml b/src/sail.ml
index c5b8e6ac..4324d650 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -53,12 +53,10 @@ open Process_file
 module Big_int = Nat_big_num
 
 let lib = ref ([] : string list)
-let opt_file_out : string option ref = ref None
 let opt_interactive_script : string option ref = ref None
 let opt_print_version = ref false
 let opt_target = ref None
 let opt_tofrominterp_output_dir : string option ref = ref None
-let opt_memo_z3 = ref false
 let opt_sanity = ref false
 let opt_includes_c = ref ([]:string list)
 let opt_specialize_c = ref false
@@ -397,41 +395,6 @@ let _ =
       opt_file_arguments := (!opt_file_arguments) @ [s])
     usage_msg
 
-let load_files ?check:(check=false) type_envs files =
-  if !opt_memo_z3 then Constraint.load_digests () else ();
-
-  let t = Profile.start () in
-  let parsed = List.map (fun f -> (f, parse_file f)) files in
-  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 = Process_file.preprocess_ast options ast in
-  let ast = Initial_check.process_ast ~generate:(not check) ast in
-  (* The separate loop measures declarations would be awkward to type check, so
-     move them into the definitions beforehand. *)
-  let ast = Rewrites.move_loop_measures ast in
-  Profile.finish "parsing" t;
-
-  let t = Profile.start () in
-  let (ast, type_envs) = check_ast type_envs ast in
-  Profile.finish "type checking" t;
-
-  if !opt_memo_z3 then Constraint.save_digests () else ();
-
-  let out_name = match !opt_file_out with
-    | None when parsed = [] -> "out.sail"
-    | None -> fst (List.hd parsed)
-    | Some f -> f ^ ".sail" in
-
-  (out_name, ast, type_envs)
-
-let descatter type_envs ast =
-  let ast = Scattered.descatter ast in
-  let ast, type_envs = rewrite_ast_initial type_envs ast in
-  (* Recheck after descattering so that the internal type environments
-     always have complete variant types *)
-  Type_error.check Type_check.initial_env ast
-
 let prover_regstate tgt ast type_envs =
   match tgt with
   | Some "coq" ->
@@ -574,7 +537,7 @@ let main () =
     print_endline version
   else
     begin
-      let out_name, ast, type_envs = load_files Type_check.initial_env !opt_file_arguments in
+      let out_name, ast, type_envs = load_files options Type_check.initial_env !opt_file_arguments in
       let ast, type_envs = descatter type_envs ast in
       let ast, type_envs =
         List.fold_right (fun file (ast,_) -> Splice.splice ast file)