[internal]: make public some functions needed by external projects

Author: alleystoughton

src/ecCommands.ml

@@ -188,6 +188,9 @@ end = struct
     List.mem (norm p) ld.ld_stack
 end
 
+(* -------------------------------------------------------------------- *)
+type loader = Loader.loader
+
 (* -------------------------------------------------------------------- *)
 let process_search scope qs =
   EcScope.Search.search scope qs
@@ -441,7 +444,10 @@ and process_th_require1 ld scope (nm, (sysname, thname), io) =
 
         try_finally (fun () ->
           let commands = EcIo.parseall (EcIo.from_file filename) in
-          let commands = List.fold_left (process_internal subld) iscope commands in
+          let commands =
+            List.fold_left 
+              (fun scope g -> process_internal subld scope g.gl_action)
+              iscope commands in
           commands)
         (fun () -> Pragma.set i_pragma)
       in
@@ -673,9 +679,14 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
     scope
 
 (* -------------------------------------------------------------------- *)
-and process_internal ld scope g =
-  try  odfl scope (process ld scope g.gl_action)
-  with e -> raise (EcScope.toperror_of_exn ~gloc:(loc g.gl_action) e)
+and process_internal
+  (ld     : Loader.loader)
+  (scope  : EcScope.scope)
+  (action : global_action located)
+  : EcScope.scope
+=
+  try  odfl scope (process ld scope action)
+  with e -> raise (EcScope.toperror_of_exn ~gloc:(loc action) e)
 
 (* -------------------------------------------------------------------- *)
 let loader = Loader.create ()

src/ecCommands.mli

@@ -5,6 +5,9 @@ open EcLocation
 exception Restart
 
 (* -------------------------------------------------------------------- *)
+type loader
+
+val loader   : loader
 val addidir  : ?namespace:EcLoader.namespace -> ?recursive:bool -> string -> unit
 val loadpath : unit -> (EcLoader.namespace option * string) list
 
@@ -21,6 +24,8 @@ type checkmode = {
   cm_iterate  : bool;
 }
 
+val initial : checkmode:checkmode -> boot:bool -> EcScope.scope
+
 val initialize  :
      restart:bool
   -> undo:bool
@@ -31,6 +36,13 @@ val initialize  :
 val current     : unit -> EcScope.scope
 val addnotifier : notifier -> unit
 
+(* -------------------------------------------------------------------- *)
+val process_internal :
+     loader
+  -> EcScope.scope
+  -> EcParsetree.global_action located
+  -> EcScope.scope
+
 (* -------------------------------------------------------------------- *)
 val process : ?timed:bool -> ?break:bool ->
   EcParsetree.global_action located -> float option

src/ecScope.ml

@@ -606,10 +606,10 @@ module Prover = struct
     }
 
   (* -------------------------------------------------------------------- *)
-  let mk_prover_info scope (options : smt_options) =
+  let mk_prover_info_from_dft (dft : EcProvers.prover_infos)
+      (options : smt_options) : EcProvers.prover_infos =
     let open EcProvers in
 
-    let dft          = Prover_info.get scope.sc_options in
     let gn_debug     = odfl dft.gn_debug options.gn_debug in
     let pr_maxprocs  = odfl dft.pr_maxprocs options.po_nprovers in
     let pr_timelimit = max 0 (odfl dft.pr_timelimit options.po_timeout) in
@@ -637,11 +637,23 @@ module Prover = struct
       pr_dumpin  ;
       gn_debug   ; }
 
+  (* -------------------------------------------------------------------- *)
+  let mk_prover_info scope (options : smt_options) =
+    let dft = Prover_info.get scope.sc_options in
+    mk_prover_info_from_dft dft options
+
   (* -------------------------------------------------------------------- *)
   let do_prover_info scope ppr =
     let options = process_prover_option (env scope) ppr in
     mk_prover_info scope options
 
+  (* -------------------------------------------------------------------- *)
+  let pprover_infos_to_prover_infos
+      (env : EcEnv.env) (dft : EcProvers.prover_infos)
+      (ppr : pprover_infos) : EcProvers.prover_infos =
+    let options = process_prover_option env ppr in
+    mk_prover_info_from_dft dft options
+
   (* -------------------------------------------------------------------- *)
   let process scope ppr =
     let pi = do_prover_info scope ppr in
@@ -823,7 +835,7 @@ module Ax = struct
           PSCheck proof
     in
     let puc =
-      let active =        
+      let active =
         { puc_name    = name
         ; puc_started = false
         ; puc_jdg     = puc
@@ -2033,6 +2045,16 @@ module Theory = struct
 
       | None -> assert false
 
+  (* ------------------------------------------------------------------ *)
+  let update_with_required ~(dst : scope) ~(src : scope) =
+    let dst =
+      let sc_loaded =
+        Msym.union
+          (fun _ x y -> assert (x ==(*phy*) y); Some x)
+          dst.sc_loaded src.sc_loaded
+      in { dst with sc_loaded }
+    in List.fold_right require_loaded src.sc_required dst
+
   (* ------------------------------------------------------------------ *)
   let add_clears clears scope =
     let clears =

src/ecScope.mli

@@ -68,6 +68,11 @@ val attop  : scope -> bool
 val goal   : scope -> proof_auc option
 val xgoal  : scope -> proof_uc option
 
+(* Creates a scope that is identical to the supplied one except
+ * that the environment and required theories are reset to the ones
+ * from the prelude. *)
+val for_loading : scope -> scope
+
 type topmode = [`InProof | `InActiveProof | `InTop]
 
 val check_state : topmode -> string -> scope -> unit
@@ -135,6 +140,10 @@ module Theory : sig
 
   exception TopScope
 
+  (* [update_with_required dst src] updates [dst] with the required
+   * theories of [src] *)
+  val update_with_required : dst:scope -> src:scope -> scope
+
   (* [enter scope mode name] start a theory in scope [scope] with
    * name [name] and mode (abstract/concrete) [mode]. *)
   val enter : scope -> thmode -> symbol -> EcTypes.is_local -> scope
@@ -210,6 +219,12 @@ module Prover : sig
   val set_default : scope -> smt_options -> scope
   val full_check  : scope -> scope
   val check_proof : scope -> bool -> scope
+
+  val pprover_infos_to_prover_infos :
+       EcEnv.env
+    -> EcProvers.prover_infos
+    -> pprover_infos
+    -> EcProvers.prover_infos
 end
 
 (* -------------------------------------------------------------------- *)