new: Optimize Proof, Optimize Heap

- drops all Defined entries from the evar map (applying the subst to the
  initial evar and the undefined evars types).
- call Gc.compact

Now the question is: where should these two commands be documented?

6 files changed, 28 insertions, 0 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index abd1024d6e..5654e464ad 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -312,6 +312,10 @@ let return p =
 
 let initial_goals p = Proofview.initial_goals p.entry
 
+let compact p =
+  let entry, proofview = Proofview.compact p.entry p.proofview in
+  { p with proofview; entry }
+
 (*** Function manipulation proof extra informations ***)
 
 (*** Tactics ***)
diff --git a/proofs/proof.mli b/proofs/proof.mli
index be23d77296..c55e562a2b 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -77,6 +77,8 @@ val is_done : proof -> bool
 (* Returns the list of partial proofs to initial goals. *)
 val partial_proof : proof -> Term.constr list
 
+val compact : proof -> proof
+
 (* Returns the proofs (with their type) of the initial goals.
     Raises [UnfinishedProof] is some goals remain to be considered.
     Raises [HasShelvedGoals] if some goals are left on the shelf.
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4000db47c2..06ca377192 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -155,6 +155,9 @@ let with_current_proof f =
       ret
 let simple_with_current_proof f = with_current_proof (fun t p -> f t p , ())
 
+let compact_the_proof () = simple_with_current_proof (fun _ -> Proof.compact)
+
+
 (* Sets the tactic to be used when a tactic line is closed with [...] *)
 let set_endline_tactic tac =
   match !pstates with
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index de259a4cca..8dd7396868 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -46,6 +46,8 @@ exception NoCurrentProof
 val give_me_the_proof : unit -> Proof.proof
 (** @raise NoCurrentProof when outside proof mode. *)
 
+val compact_the_proof : unit -> unit
+
 (** When a proof is closed, it is reified into a [proof_object], where
     [id] is the name of the proof, [entries] the list of the proof terms
     (in a form suitable for definitions). Together with the [terminator]
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 7ab7e882ce..e2b92f5649 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -32,6 +32,20 @@ type entry = (Term.constr * Term.types) list
 let proofview p =
   p.comb , p.solution
 
+let compact el { comb; solution } =
+  let nf = Evarutil.nf_evar solution in
+  let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
+  let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
+  let pruned_solution = Evd.drop_all_defined solution in
+  let apply_subst_einfo _ ei =
+    Evd.({ ei with
+       evar_concl =  nf ei.evar_concl;
+       evar_hyps = Environ.map_named_val nf ei.evar_hyps;
+       evar_candidates = Option.map (List.map nf) ei.evar_candidates }) in
+  let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
+  let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
+  msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
+  new_el, { comb; solution = new_solution }
 
 
 (** {6 Starting and querying a proof view} *)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 29828bbbe7..796a6a7baa 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -32,6 +32,9 @@ val proofview : proofview -> Goal.goal list * Evd.evar_map
 (** Abstract representation of the initial goals of a proof. *)
 type entry
 
+(** Optimize memory consumption *)
+val compact : entry -> proofview -> entry * proofview
+
 (** Initialises a proofview, the main argument is a list of
     environements (including a [named_context] which are used as
     hypotheses) pair with conclusion types, creating accordingly many