Update libsail slightly with recent changes

Also don't include the toplevel files in the library, and move
load_files and descatter into process_file where they can be called

5 files changed, 51 insertions, 55 deletions

diff --git a/src/isail.ml b/src/isail.ml
index 31919f00..02908321 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -393,7 +393,7 @@ let load_session upto file =
   | Some upto_file when Filename.basename upto_file = file -> None
   | Some upto_file ->
      let (_, ast, env) =
-       load_files ~check:true !Interactive.env [Filename.concat (Filename.dirname upto_file) file]
+       Process_file.load_files ~check:true options !Interactive.env [Filename.concat (Filename.dirname upto_file) file]
      in
      Interactive.ast := append_ast !Interactive.ast ast;
      Interactive.env := env;
@@ -509,7 +509,7 @@ let handle_input' input =
         begin match cmd with
         | ":l" | ":load" ->
            let files = Util.split_on_char ' ' arg in
-           let (_, ast, env) = load_files !Interactive.env files in
+           let (_, ast, env) = Process_file.load_files options !Interactive.env files in
            Interactive.ast := append_ast !Interactive.ast ast;
            interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
            Interactive.env := env;
@@ -601,7 +601,7 @@ let handle_input' input =
            Interactive.ast := ast;
            vs_ids := val_spec_ids !Interactive.ast
         | ":compile" ->
-           let out_name = match !opt_file_out with
+           let out_name = match !Process_file.opt_file_out with
              | None -> "out.sail"
              | Some f -> f ^ ".sail"
            in
@@ -628,7 +628,7 @@ let handle_input' input =
            begin
              try
                load_into_session arg;
-               let (_, ast, env) = load_files ~check:true !Interactive.env [arg] in
+               let (_, ast, env) = Process_file.load_files ~check:true options !Interactive.env [arg] in
                Interactive.ast := append_ast !Interactive.ast ast;
                interactive_state := initial_state !Interactive.ast !Interactive.env !Value.primops;
                Interactive.env := env;
diff --git a/src/libsail.mllib b/src/libsail.mllib
index 2d1f568f..f0322043 100644
--- a/src/libsail.mllib
+++ b/src/libsail.mllib
@@ -14,13 +14,14 @@ Graph
 Initial_check
 Interactive
 Interpreter
-Isail
 Jib
 Jib_compile
 Jib_optimize
 Jib_ssa
 Jib_smt
 Jib_util
+Jib_interactive
+Jib_ir
 Latex
 Lexer
 Manifest
@@ -48,7 +49,6 @@ Property
 Reporting
 Rewriter
 Rewrites
-Sail
 Sail2_values
 Sail_lib
 Scattered
diff --git a/src/process_file.ml b/src/process_file.ml
index 72e25777..d2a86595 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -56,6 +56,8 @@ let opt_isa_output_dir = ref None
 let opt_coq_output_dir = ref None
 let opt_alt_modules_coq = ref ([]:string list)
 let opt_alt_modules2_coq = ref ([]:string list)
+let opt_memo_z3 = ref false
+let opt_file_out : string option ref = ref None
 
 type out_type =
   | Lem_out of string list
@@ -238,12 +240,6 @@ let rec preprocess opts = function
 
 let preprocess_ast opts (Parse_ast.Defs defs) = Parse_ast.Defs (preprocess opts defs)
 
-let load_file_no_check opts order f = Initial_check.process_ast (preprocess_ast opts (parse_file f))
-
-let load_file opts order env f =
-  let ast = Initial_check.process_ast (preprocess_ast opts (parse_file f)) in
-  Type_error.check env ast
-
 let opt_just_check = ref false
 let opt_ddump_tc_ast = ref false
 let opt_ddump_rewrite_ast = ref None
@@ -256,6 +252,33 @@ let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tanno
   let () = if !opt_just_check then exit 0 else () in
   (ast, env)
 
+let load_files ?check:(check=false) options 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 = 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 open_output_with_check opt_dir file_name =
   let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in
@@ -348,12 +371,12 @@ let output_coq opt_dir filename alt_modules alt_modules2 libs defs =
     (match alt_modules with
     | [] -> base_imports_default
     | _ -> Str.split (Str.regexp "[ \t]+") (String.concat " " alt_modules)
-    ) in  
+    ) in
   let alt_modules2_imports =
     (match alt_modules2 with
     | [] -> []
     | _ -> Str.split (Str.regexp "[ \t]+") (String.concat " " alt_modules2)
-    ) in  
+    ) in
   let ((ot,_,_,_) as ext_ot) =
     open_output_with_check_unformatted opt_dir (filename ^ "_types" ^ ".v") in
   let ((o,_,_,_) as ext_o) =
@@ -413,3 +436,10 @@ let rewrite_ast_initial env = rewrite env [("initial", fun env defs -> Rewriter.
 let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_defs_target tgt)
 
 let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check
+
+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
diff --git a/src/process_file.mli b/src/process_file.mli
index fa0aeb31..d1fa2cb8 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -61,9 +61,8 @@ val rewrite_ast_initial : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type
 val rewrite_ast_target : string -> Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
 val rewrite_ast_check : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
 
-val load_file_no_check : (Arg.key * Arg.spec * Arg.doc) list -> Ast.order -> string -> unit Ast.defs
-val load_file : (Arg.key * Arg.spec * Arg.doc) list -> Ast.order -> Type_check.Env.t -> string -> Type_check.tannot Ast.defs * Type_check.Env.t
-
+val opt_file_out : string option ref
+val opt_memo_z3 : bool ref
 val opt_just_check : bool ref
 val opt_ddump_tc_ast : bool ref
 val opt_ddump_rewrite_ast : ((string * int) option) ref
@@ -90,3 +89,7 @@ val output :
     files existed before. If it is set to [false] and an output file already exists,
     the output file is only updated, if its content really changes. *)
 val always_replace_files : bool ref
+
+val load_files : ?check:bool -> (Arg.key * Arg.spec * Arg.doc) list -> Type_check.Env.t -> string list -> (string * Type_check.tannot Ast.defs * Type_check.Env.t)
+
+val descatter : Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t
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)