Better encapsulation of future goals

We try to encapsulate the future goals abstraction in the evar map.
A few calls to `save_future_goals` and `restore_future_goals` are still
there, but we try to minimize them.

This is a preliminary refactoring to make the invariants between the
shelf and future goals more explicit, before giving unification access
to the shelf, which is needed for #7825.

7 files changed, 44 insertions, 35 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 01c4e5fd72..9d3ae95e7d 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -522,9 +522,7 @@ let restrict_evar evd evk filter ?src candidates =
      let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
      (* Mark new evar as future goal, removing previous one,
         circumventing Proofview.advance but making Proof.run_tactic catch these. *)
-     let future_goals = Evd.save_future_goals evd in
-     let future_goals = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) future_goals in
-     let evd = Evd.restore_future_goals evd future_goals in
+     let evd = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) evd in
      (Evd.declare_future_goal evk' evd, evk')
 
 let rec check_and_clear_in_constr env evdref err ids global c =
diff --git a/engine/evd.ml b/engine/evd.ml
index 92657c41a9..fa84e45778 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1089,23 +1089,27 @@ let restore_future_goals evd (gls,pgl,map) =
   { evd with future_goals = gls ; principal_future_goal = pgl;
              future_goals_status = map }
 
-let fold_future_goals f sigma (gls,pgl,map) =
-  List.fold_left f sigma gls
+let fold_future_goals f sigma =
+  List.fold_left f sigma sigma.future_goals
 
-let map_filter_future_goals f (gls,pgl,map) =
+let map_filter_future_goals f evd =
   (* Note: map is now a superset of filtered evs, but its size should
     not be too big, so that's probably ok not to update it *)
-  (List.map_filter f gls,Option.bind pgl f,map)
+  let future_goals = List.map_filter f evd.future_goals in
+  let principal_future_goal = Option.bind evd.principal_future_goal f in
+  { evd with future_goals; principal_future_goal }
 
-let filter_future_goals f (gls,pgl,map) =
-  (List.filter f gls,Option.bind pgl (fun a -> if f a then Some a else None),map)
+let filter_future_goals f evd =
+  let future_goals = List.filter f evd.future_goals in
+  let principal_future_goal = Option.bind evd.principal_future_goal (fun a -> if f a then Some a else None) in
+  { evd with future_goals; principal_future_goal }
 
-let dispatch_future_goals_gen distinguish_shelf (gls,pgl,map) =
+let dispatch_future_goals_gen distinguish_shelf evd =
   let rec aux (comb,shelf,givenup as acc) = function
     | [] -> acc
     | evk :: gls ->
        let acc =
-        try match EvMap.find evk map with
+        try match EvMap.find evk evd.future_goals_status with
         | ToGiveUp -> (comb,shelf,evk::givenup)
         | ToShelve ->
            if distinguish_shelf then (comb,evk::shelf,givenup)
@@ -1113,18 +1117,20 @@ let dispatch_future_goals_gen distinguish_shelf (gls,pgl,map) =
         with Not_found -> (evk::comb,shelf,givenup) in
        aux acc gls in
   (* Note: this reverses the order of initial list on purpose *)
-  let (comb,shelf,givenup) = aux ([],[],[]) gls in
-  (comb,shelf,givenup,pgl)
+  let (comb,shelf,givenup) = aux ([],[],[]) evd.future_goals in
+  (comb,shelf,givenup,evd.principal_future_goal)
 
 let dispatch_future_goals =
   dispatch_future_goals_gen true
 
-let extract_given_up_future_goals goals =
-  let (comb,_,givenup,_) = dispatch_future_goals_gen false goals in
+let extract_given_up_future_goals evd =
+  let (comb,_,givenup,_) = dispatch_future_goals_gen false evd in
   (comb,givenup)
 
-let shelve_on_future_goals shelved (gls,pgl,map) =
-  (shelved @ gls, pgl, List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved map)
+let shelve_on_future_goals shelved evd =
+  let future_goals = shelved @ evd.future_goals in
+  let future_goals_status = List.fold_right (fun evk -> EvMap.add evk ToShelve) shelved evd.future_goals_status in
+  {evd with future_goals; future_goals_status }
 
 (**********************************************************)
 (* Accessing metas *)
diff --git a/engine/evd.mli b/engine/evd.mli
index d338b06e0e..91cbbe5d77 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -378,23 +378,23 @@ val restore_future_goals : evar_map -> future_goals -> evar_map
     goals has been consumed. Used by the [refine] primitive of the
     tactic engine. *)
 
-val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map
+val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
 (** Fold future goals *)
 
-val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals
+val map_filter_future_goals : (Evar.t -> Evar.t option) -> evar_map -> evar_map
 (** Applies a function on the future goals *)
 
-val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals
+val filter_future_goals : (Evar.t -> bool) -> evar_map -> evar_map
 (** Applies a filter on the future goals *)
 
-val dispatch_future_goals : future_goals -> Evar.t list * Evar.t list * Evar.t list * Evar.t option
+val dispatch_future_goals : evar_map -> Evar.t list * Evar.t list * Evar.t list * Evar.t option
 (** Returns the future_goals dispatched into regular, shelved, given_up
    goals; last argument is the goal tagged as principal if any *)
 
-val extract_given_up_future_goals : future_goals -> Evar.t list * Evar.t list
+val extract_given_up_future_goals : evar_map -> Evar.t list * Evar.t list
 (** An ad hoc variant for Proof.proof; not for general use *)
 
-val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals
+val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map
 (** Push goals on the shelve of future goals *)
 
 (** {5 Sort variables}
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1c3aed8fc2..7aea07d6f0 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -56,12 +56,18 @@ module V82 = struct
        be shelved. It must not appear as a future_goal, so the future
        goals are restored to their initial value after the evar is
        created. *)
-    let prev_future_goals = Evd.save_future_goals evars in
     let inst = EConstr.identity_subst_val hyps in
-    let (evars, evk) =
-      Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false ~identity:inst hyps evars concl
+    let evi = { Evd.evar_hyps = hyps;
+                Evd.evar_concl = concl;
+                Evd.evar_filter = Evd.Filter.identity;
+                Evd.evar_abstract_arguments = Evd.Abstraction.identity;
+                Evd.evar_body = Evd.Evar_empty;
+                Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
+                Evd.evar_candidates = None;
+                Evd.evar_identity = Evd.Identity.make inst;
+              }
     in
-    let evars = Evd.restore_future_goals evars prev_future_goals in
+    let (evars, evk) = Evd.new_evar evars ~typeclass_candidate:false evi in
     let ev = EConstr.mkEvar (evk,inst) in
     (evk, ev, evars)
 
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 38fcdd6e5f..c427c07b93 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -373,7 +373,7 @@ let run_tactic env tac pr =
     Proofview.tclEVARMAP >>= fun sigma ->
     (* Already solved goals are not to be counted as shelved. Nor are
       they to be marked as unresolvable. *)
-    let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) (Evd.save_future_goals sigma) in
+    let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) sigma in
     let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in
     (* Check that retrieved given up is empty *)
     if not (List.is_empty retrieved_given_up) then
diff --git a/proofs/refine.ml b/proofs/refine.ml
index a10bbcbdd4..8909b9639d 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -55,15 +55,14 @@ let generic_refine ~typecheck f gl =
   (* Create the refinement term *)
   Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () ->
   f >>= fun (v, c) ->
-  Proofview.tclEVARMAP >>= fun sigma ->
+  Proofview.tclEVARMAP >>= fun sigma' ->
   Proofview.V82.wrap_exceptions begin fun () ->
-  let evs = Evd.save_future_goals sigma in
   (* Redo the effects in sigma in the monad's env *)
-  let privates_csts = Evd.eval_side_effects sigma in
+  let privates_csts = Evd.eval_side_effects sigma' in
   let env = Safe_typing.push_private_constants env privates_csts.Evd.seff_private in
   (* Check that the introduced evars are well-typed *)
   let fold accu ev = typecheck_evar ev env accu in
-  let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
+  let sigma = if typecheck then Evd.fold_future_goals fold sigma' else sigma' in
   (* Check that the refined term is typesafe *)
   let sigma = if typecheck then Typing.check env sigma c concl else sigma in
   (* Check that the goal itself does not appear in the refined term *)
@@ -75,7 +74,7 @@ let generic_refine ~typecheck f gl =
   (* Restore the [future goals] state. *)
   let sigma = Evd.restore_future_goals sigma prev_future_goals in
   (* Select the goals *)
-  let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in
+  let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) sigma' in
   let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
   (* Proceed to the refinement *)
   let sigma = match Proofview.Unsafe.advance sigma self with
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 2f55cc071f..31132824f5 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -934,7 +934,6 @@ module Search = struct
        let tac = tac <*> Proofview.Unsafe.tclGETGOALS >>=
          fun stuck -> Proofview.shelve_goals (List.map Proofview_monad.drop_state stuck) in
        let evm = Evd.set_typeclass_evars evm Evar.Set.empty in
-       let fgoals = Evd.save_future_goals evm in
        let _, pv = Proofview.init evm [] in
        let pv = Proofview.unshelve goalsl pv in
        try
@@ -956,7 +955,8 @@ module Search = struct
                          (str "leaking evar " ++ int (Evar.repr ev) ++
                             spc () ++ pr_ev evm' ev);
                      acc && okev) evm' true);
-           let fgoals = Evd.shelve_on_future_goals shelved fgoals in
+           let evm = Evd.shelve_on_future_goals shelved evm in
+           let fgoals = Evd.save_future_goals evm in
            let evm' = Evd.restore_future_goals evm' fgoals in
            let nongoals' =
              Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with