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?

11 files changed, 42 insertions, 0 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ab595be25..d36a6a20f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -655,6 +655,8 @@ let to_list d =
 
 let undefined_map d = d.undf_evars
 
+let drop_all_defined d = { d with defn_evars = EvMap.empty }
+
 (* spiwack: not clear what folding over an evar_map, for now we shall
     simply fold over the inner evar_map. *)
 let fold f d a =
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 513ade646..6c7ef2168 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -208,6 +208,8 @@ val undefined_map : evar_map -> evar_info Evar.Map.t
 val eq_evar_info : evar_map -> evar_info -> evar_info -> bool
 (** Compare the evar_info's up to the universe constraints of the evar map. *)
 
+val drop_all_defined : evar_map -> evar_map
+
 (** {6 Instantiating partial terms} *)
 
 exception NotInstantiatedEvar
diff --git a/proofs/proof.ml b/proofs/proof.ml
index abd1024d6..5654e464a 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 be23d7729..c55e562a2 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 4000db47c..06ca37719 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 de259a4cc..8dd739686 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 7ab7e882c..e2b92f564 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 29828bbbe..796a6a7ba 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
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 53eb1a3f2..cc960a267 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -223,3 +223,4 @@ let rec classify_vernac e =
 let classify_as_query =
   VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
 let classify_as_sideeff = VtSideff [], VtLater
+let classify_as_proofstep = VtProofStep false, VtLater
diff --git a/stm/vernac_classifier.mli b/stm/vernac_classifier.mli
index 329c90198..41e3661e6 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/vernac_classifier.mli
@@ -24,4 +24,5 @@ val set_undo_classifier : (vernac_expr -> vernac_classification) -> unit
 (** Standard constant classifiers *)
 val classify_as_query : vernac_classification
 val classify_as_sideeff : vernac_classification
+val classify_as_proofstep : vernac_classification
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0c0204081..bf7e8b348 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -998,3 +998,11 @@ END
 VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
 | [ "Print" "Equivalent" "Keys" ] -> [ msg_info (Keys.pr_keys Printer.pr_global) ]
 END
+
+
+VERNAC COMMAND EXTEND OptimizeProof
+| [ "Optimize" "Proof" ] => [ Vernac_classifier.classify_as_proofstep ] ->
+  [ Proof_global.compact_the_proof () ]
+| [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] ->
+  [ Gc.compact () ]
+END