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.

3 files changed, 27 insertions, 23 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}