Make future_goals stack explicit in the evarmap

5 files changed, 135 insertions, 100 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 9d3ae95e7d..7beb7ff738 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -522,7 +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 evd = Evd.filter_future_goals (fun evk' -> not (Evar.equal evk evk')) evd in
+     let evd = Evd.remove_future_goal evd evk 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 9de11bdc1e..584b390cff 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -451,8 +451,6 @@ let key id (_, idtoev) =
 
 end
 
-type goal_kind = ToShelve
-
 type evar_flags =
   { obligation_evars : Evar.Set.t;
     restricted_evars : Evar.t Evar.Map.t;
@@ -466,6 +464,19 @@ type side_effects = {
   seff_roles : side_effect_role Cmap.t;
 }
 
+type future_goals = {
+  future_comb : Evar.t list;
+  future_shelf : Evar.t list;
+  future_principal : Evar.t option; (** if [Some e], [e] must be
+                                        contained in
+                                        [future_comb]. The evar
+                                        [e] will inherit
+                                        properties (now: the
+                                        name) of the evar which
+                                        will be instantiated with
+                                        a term containing [e]. *)
+}
+
 type evar_map = {
   (* Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -481,17 +492,8 @@ type evar_map = {
   evar_flags : evar_flags;
   (** Interactive proofs *)
   effects    : side_effects;
-  future_goals : Evar.t list; (** list of newly created evars, to be
-                                  eventually turned into goals if not solved.*)
-  principal_future_goal : Evar.t option; (** if [Some e], [e] must be
-                                             contained
-                                             [future_goals]. The evar
-                                             [e] will inherit
-                                             properties (now: the
-                                             name) of the evar which
-                                             will be instantiated with
-                                             a term containing [e]. *)
-  future_goals_status : goal_kind EvMap.t;
+  future_goals : future_goals list; (** list of newly created evars, to be
+                                         eventually turned into goals if not solved.*)
   given_up : Evar.Set.t;
   extras : Store.t;
 }
@@ -591,14 +593,19 @@ let new_evar evd ?name ?typeclass_candidate evi =
 let remove d e =
   let undf_evars = EvMap.remove e d.undf_evars in
   let defn_evars = EvMap.remove e d.defn_evars in
-  let principal_future_goal = match d.principal_future_goal with
-  | None -> None
-  | Some e' -> if Evar.equal e e' then None else d.principal_future_goal
+  let remove_future fgl =
+    let future_principal = match fgl.future_principal with
+    | None -> None
+    | Some e' -> if Evar.equal e e' then None else fgl.future_principal
+    in
+    let filter e' = not (Evar.equal e e') in
+    let future_comb = List.filter filter fgl.future_comb in
+    let future_shelf = List.filter filter fgl.future_shelf in
+    { future_principal; future_comb; future_shelf }
   in
-  let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
-  let future_goals_status = EvMap.remove e d.future_goals_status in
+  let future_goals = List.map remove_future d.future_goals in
   let evar_flags = remove_evar_flags e d.evar_flags in
-  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status;
+  { d with undf_evars; defn_evars; future_goals;
            evar_flags }
 
 let find d e =
@@ -714,6 +721,12 @@ let empty_side_effects = {
   seff_roles = Cmap.empty;
 }
 
+let empty_future_goals = {
+  future_principal = None;
+  future_comb = [];
+  future_shelf = [];
+}
+
 let empty = {
   defn_evars = EvMap.empty;
   undf_evars = EvMap.empty;
@@ -724,9 +737,7 @@ let empty = {
   metas      = Metamap.empty;
   effects    = empty_side_effects;
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
-  future_goals = [];
-  principal_future_goal = None;
-  future_goals_status = EvMap.empty;
+  future_goals = [empty_future_goals];
   given_up = Evar.Set.empty;
   extras = Store.empty;
 }
@@ -1063,73 +1074,94 @@ let drop_side_effects evd =
 let eval_side_effects evd = evd.effects
 
 (* Future goals *)
-let declare_future_goal ?tag evk evd =
-  { evd with future_goals = evk::evd.future_goals;
-             future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status }
-
-let declare_principal_goal ?tag evk evd =
-  match evd.principal_future_goal with
-  | None -> { evd with
-    future_goals = evk::evd.future_goals;
-    principal_future_goal=Some evk;
-    future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status;
+let set_future_goals f = function
+  | [] -> anomaly Pp.(str"future_goals stack should not be empty")
+  | hd :: tl ->
+    f hd :: tl
+
+let declare_future_goal ?(shelve=false) evk evd =
+  let add_goal fgl =
+    let (future_comb,future_shelf) =
+      if shelve then (fgl.future_comb,evk::fgl.future_shelf)
+      else (evk::fgl.future_comb,fgl.future_shelf)
+    in
+    { fgl with future_comb; future_shelf }
+  in
+  let future_goals = set_future_goals add_goal evd.future_goals in
+  { evd with future_goals }
+
+let declare_principal_goal ?(shelve=false) evk evd =
+  let add_goal fgl =
+    let (future_comb,future_shelf) =
+      if shelve then (fgl.future_comb,evk::fgl.future_shelf)
+      else (evk::fgl.future_comb,fgl.future_shelf)
+    in
+    let future_principal = Some evk in
+    { future_comb; future_shelf; future_principal }
+  in
+  match (List.hd evd.future_goals).future_principal with
+  | None ->
+    let future_goals = set_future_goals add_goal evd.future_goals in
+    { evd with
+      future_goals;
     }
   | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.")
 
-type future_goals = Evar.t list * Evar.t option * goal_kind EvMap.t
+let push_future_goals evd =
+  { evd with future_goals = empty_future_goals :: evd.future_goals }
 
-let future_goals evd = evd.future_goals
+let pop_future_goals evd =
+  match evd.future_goals with
+  | [] -> anomaly Pp.(str"future_goals stack should not be empty")
+  | hd :: tl ->
+    hd, { evd with future_goals = tl }
 
-let principal_future_goal evd = evd.principal_future_goal
+let future_goals evd =
+  let future_goals = List.hd evd.future_goals in
+  future_goals.future_shelf @ future_goals.future_comb
 
-let save_future_goals evd =
-  (evd.future_goals, evd.principal_future_goal, evd.future_goals_status)
-
-let reset_future_goals evd =
-  { evd with future_goals = [] ; principal_future_goal = None;
-             future_goals_status = EvMap.empty }
-
-let restore_future_goals evd (gls,pgl,map) =
-  { evd with future_goals = gls ; principal_future_goal = pgl;
-             future_goals_status = map }
+let principal_future_goal evd =
+  (List.hd evd.future_goals).future_principal
 
 let fold_future_goals f sigma =
-  List.fold_left f sigma sigma.future_goals
+  let future_goals = List.hd sigma.future_goals in
+  let future_goals = future_goals.future_comb @ future_goals.future_shelf in
+  List.fold_left f sigma future_goals
 
-let map_filter_future_goals f evd =
+let map_filter_future_goals f future_goals =
   (* 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 *)
-  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 future_comb = List.map_filter f future_goals.future_comb in
+  let future_shelf = List.map_filter f future_goals.future_shelf in
+  let future_principal = Option.bind future_goals.future_principal f in
+  { future_comb; future_shelf; future_principal }
 
-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 filter_future_goals f future_goals =
+  let future_comb = List.filter f future_goals.future_comb in
+  let future_shelf = List.filter f future_goals.future_shelf in
+  let future_principal = Option.bind future_goals.future_principal (fun a -> if f a then Some a else None) in
+  { future_comb; future_shelf; future_principal }
 
 let dispatch_future_goals_gen distinguish_shelf evd =
-  let rec aux (comb,shelf as acc) = function
-    | [] -> acc
-    | evk :: gls ->
-       let acc =
-        try match EvMap.find evk evd.future_goals_status with
-        | ToShelve ->
-           if distinguish_shelf then (comb,evk::shelf)
-           else raise Not_found
-        with Not_found -> (evk::comb,shelf) in
-       aux acc gls in
+  let future_goals = List.hd evd.future_goals in
   (* Note: this reverses the order of initial list on purpose *)
-  let (comb,shelf) = aux ([],[]) evd.future_goals in
-  (comb,shelf,evd.principal_future_goal)
+  (List.rev future_goals.future_comb,
+   List.rev future_goals.future_shelf,
+   future_goals.future_principal)
 
 let dispatch_future_goals =
   dispatch_future_goals_gen true
 
 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 }
+  let shelve_future future_goals =
+    let future_shelf = shelved @ future_goals.future_shelf in
+    { future_goals with future_shelf }
+  in
+  { evd with future_goals = set_future_goals shelve_future evd.future_goals }
+
+let remove_future_goal evd evk =
+  let f evk' = not (Evar.equal evk evk') in
+  { evd with future_goals = set_future_goals (filter_future_goals f) evd.future_goals }
 
 let give_up ev evd =
   { evd with given_up = Evar.Set.add ev evd.given_up }
@@ -1152,8 +1184,6 @@ let set_metas evd metas = {
   effects = evd.effects;
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
-  future_goals_status = evd.future_goals_status;
-  principal_future_goal = evd.principal_future_goal;
   given_up = evd.given_up;
   extras = evd.extras;
 }
diff --git a/engine/evd.mli b/engine/evd.mli
index 4e3f95fc42..7a139e44ba 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -347,13 +347,11 @@ val drop_side_effects : evar_map -> evar_map
 
 (** {5 Future goals} *)
 
-type goal_kind = ToShelve
-
-val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
+val declare_future_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
     internal uses only. *)
 
-val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
+val declare_principal_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals and make
     it principal. Only one existential variable can be made principal, an
     error is raised otherwise. For internal uses only. *)
@@ -366,29 +364,30 @@ val principal_future_goal : evar_map -> Evar.t option
 (** Retrieves the name of the principal existential variable if there
     is one. Used by the [refine] primitive of the tactic engine. *)
 
-type future_goals
-
-val save_future_goals : evar_map -> future_goals
-(** Retrieves the list of future goals including the principal future
-    goal. Used by the [refine] primitive of the tactic engine. *)
+type future_goals = {
+  future_comb : Evar.t list;
+  future_shelf : Evar.t list;
+  future_principal : Evar.t option; (** if [Some e], [e] must be
+                                        contained in
+                                        [future_comb]. The evar
+                                        [e] will inherit
+                                        properties (now: the
+                                        name) of the evar which
+                                        will be instantiated with
+                                        a term containing [e]. *)
+}
 
-val reset_future_goals : evar_map -> evar_map
-(** Clears the list of future goals (as well as the principal future
-    goal). Used by the [refine] primitive of the tactic engine. *)
+val push_future_goals : evar_map -> evar_map
 
-val restore_future_goals : evar_map -> future_goals -> evar_map
-(** Sets the future goals (including the principal future goal) to a
-    previous value. Intended to be used after a local list of future
-    goals has been consumed. Used by the [refine] primitive of the
-    tactic engine. *)
+val pop_future_goals : 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) -> evar_map -> evar_map
+val map_filter_future_goals : (Evar.t -> Evar.t option) -> future_goals -> future_goals
 (** Applies a function on the future goals *)
 
-val filter_future_goals : (Evar.t -> bool) -> evar_map -> evar_map
+val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals
 (** Applies a filter on the future goals *)
 
 val dispatch_future_goals : evar_map -> Evar.t list * Evar.t list * Evar.t option
@@ -398,6 +397,8 @@ val dispatch_future_goals : evar_map -> Evar.t list * Evar.t list * Evar.t optio
 val shelve_on_future_goals : Evar.t list -> evar_map -> evar_map
 (** Push goals on the shelve of future goals *)
 
+val remove_future_goal : evar_map -> Evar.t -> evar_map
+
 val give_up : Evar.t -> evar_map -> evar_map
 
 val given_up : evar_map -> Evar.Set.t
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 0ed945f5d4..21cb6f42a7 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -60,6 +60,10 @@ type telescope =
   | TNil of Evd.evar_map
   | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
 
+let map_telescope_evd f = function
+  | TNil sigma -> TNil (f sigma)
+  | TCons (env,sigma,ty,g) -> TCons(env,(f sigma),ty,g)
+
 let dependent_init =
   (* Goals don't have a source location. *)
   let src = Loc.tag @@ Evar_kinds.GoalEvar in
@@ -74,9 +78,10 @@ let dependent_init =
     entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
   in
   fun t ->
+    let t = map_telescope_evd Evd.push_future_goals t in
     let entry, v = aux t in
     (* The created goal are not to be shelved. *)
-    let solution = Evd.reset_future_goals v.solution in
+    let _goals, solution = Evd.pop_future_goals v.solution in
     entry, { v with solution }
 
 let init =
@@ -746,17 +751,16 @@ let with_shelf tac =
   let open Proof in
   Pv.get >>= fun pv ->
   let { shelf; solution } = pv in
-  Pv.set { pv with shelf = []; solution = Evd.reset_future_goals solution } >>
+  Pv.set { pv with shelf = []; solution = Evd.push_future_goals solution } >>
   tac >>= fun ans ->
   Pv.get >>= fun npv ->
   let { shelf = gls; solution = sigma } = npv in
   (* The pending future goals are necessarily coming from V82.tactic *)
   (* and thus considered as to shelve, as in Proof.run_tactic *)
-  let gls' = Evd.future_goals sigma in
-  let fgoals = Evd.save_future_goals solution in
-  let sigma = Evd.restore_future_goals sigma fgoals in
+  let fgl, sigma = Evd.pop_future_goals sigma in
   (* Ensure we mark and return only unsolved goals *)
-  let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
+  let gls' = CList.rev_append fgl.Evd.future_shelf (CList.rev_append fgl.Evd.future_comb gls) in
+  let gls' = undefined_evars sigma gls' in
   let sigma = mark_in_evm ~goal:false sigma gls' in
   let npv = { npv with shelf; solution = sigma } in
   Pv.set npv >> tclUNIT (gls', ans)
@@ -1017,8 +1021,8 @@ module Unsafe = struct
   let tclEVARUNIVCONTEXT ctx =
     Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
 
-  let reset_future_goals p =
-    { p with solution = Evd.reset_future_goals p.solution }
+  let push_future_goals p =
+    { p with solution = Evd.push_future_goals p.solution }
 
   let mark_as_goals evd content =
     mark_in_evm ~goal:true evd content
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 29425b10f2..8853013a84 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -474,7 +474,7 @@ module Unsafe : sig
   val tclEVARUNIVCONTEXT : UState.t -> unit tactic
 
   (** Clears the future goals store in the proof view. *)
-  val reset_future_goals : proofview -> proofview
+  val push_future_goals : proofview -> proofview
 
   (** Give the evars the status of a goal (changes their source location
       and makes them unresolvable for type classes. *)