Unify the shelves

Before this patch, the proof engine had three notions of shelves:
- A local shelf in `proofview`
- A global shelf in `Proof.t`
- A future shelf in `evar_map`

This has lead to a lot of confusion and limitations or bugs, because
some components have only a partial view of the shelf: the pretyper can
see only the future shelf, tactics can see only the local and future
shelves. In particular, this refactoring is needed for #7825.

The solution we choose is to move shelf information to the evar map, as
a shelf stack (for nested `unshelve` tacticals).

Closes #8770.
Closes #6292.

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>

7 files changed, 109 insertions, 95 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index b20700143f..65df2643f2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -468,7 +468,6 @@ module FutureGoals : sig
 
   type t = private {
     comb : Evar.t list;
-    shelf : Evar.t list;
     principal : Evar.t option; (** if [Some e], [e] must be
                                    contained in
                                    [comb]. The evar
@@ -492,20 +491,17 @@ module FutureGoals : sig
   val push : stack -> stack
   val pop : stack -> t * stack
 
-  val add : shelve:bool -> principal:bool -> Evar.t -> stack -> stack
+  val add : principal:bool -> Evar.t -> stack -> stack
   val remove : Evar.t -> stack -> stack
 
   val fold : ('a -> Evar.t -> 'a) -> 'a -> stack -> 'a
 
-  val put_shelf : Evar.t list -> stack -> stack
-
   val pr_stack : stack -> Pp.t
 
 end = struct
 
   type t = {
     comb : Evar.t list;
-    shelf : Evar.t list;
     principal : Evar.t option; (** if [Some e], [e] must be
                                    contained in
                                    [comb]. The evar
@@ -523,12 +519,9 @@ end = struct
   | hd :: tl ->
     f hd :: tl
 
-  let add ~shelve ~principal evk stack =
+  let add ~principal evk stack =
     let add fgl =
-      let (comb,shelf) =
-        if shelve then (fgl.comb,evk::fgl.shelf)
-        else (evk::fgl.comb,fgl.shelf)
-      in
+      let comb = evk :: fgl.comb in
       let principal =
         if principal then
           match fgl.principal with
@@ -536,7 +529,7 @@ end = struct
           | None -> Some evk
         else fgl.principal
       in
-      { comb; shelf; principal }
+      { comb; principal }
     in
     set add stack
 
@@ -545,15 +538,13 @@ end = struct
       let filter e' = not (Evar.equal e e') in
       let principal = Option.filter filter fgl.principal in
       let comb = List.filter filter fgl.comb in
-      let shelf = List.filter filter fgl.shelf in
-      { principal; comb; shelf }
+      { principal; comb }
     in
     List.map remove stack
 
   let empty = {
     principal = None;
     comb = [];
-    shelf = [];
   }
 
   let empty_stack = [empty]
@@ -568,27 +559,17 @@ end = struct
 
   let fold f acc stack =
     let future_goals = List.hd stack in
-    let future_goals = future_goals.comb @ future_goals.shelf in
-    List.fold_left f acc future_goals
+    List.fold_left f acc future_goals.comb
 
   let filter f fgl =
     let comb = List.filter f fgl.comb in
-    let shelf = List.filter f fgl.shelf in
     let principal = Option.filter f fgl.principal in
-    { comb; shelf; principal }
+    { comb; principal }
 
   let map_filter f fgl =
     let comb = List.map_filter f fgl.comb in
-    let shelf = List.map_filter f fgl.shelf in
     let principal = Option.bind fgl.principal f in
-    { comb; shelf; principal }
-
-  let put_shelf shelved stack =
-    match stack with
-    | [] -> anomaly Pp.(str"future_goals stack should not be empty")
-    | hd :: tl ->
-      let shelf = shelved @ hd.shelf in
-      { hd with shelf } :: tl
+    { comb; principal }
 
   let pr_stack stack =
     let open Pp in
@@ -601,7 +582,6 @@ end = struct
 
 end
 
-
 type evar_map = {
   (* Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -620,6 +600,7 @@ type evar_map = {
   future_goals : FutureGoals.stack; (** list of newly created evars, to be
                                         eventually turned into goals if not solved.*)
   given_up : Evar.Set.t;
+  shelf : Evar.t list list;
   extras : Store.t;
 }
 
@@ -848,6 +829,7 @@ let empty = {
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
   future_goals = FutureGoals.empty_stack;
   given_up = Evar.Set.empty;
+  shelf = [[]];
   extras = Store.empty;
 }
 
@@ -859,6 +841,8 @@ let has_undefined evd = not (EvMap.is_empty evd.undf_evars)
 
 let has_given_up evd = not (Evar.Set.is_empty evd.given_up)
 
+let has_shelved evd = not (List.for_all List.is_empty evd.shelf)
+
 let evars_reset_evd ?(with_conv_pbs=false) ?(with_univs=true) evd d =
   let conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs in
   let last_mods = if with_conv_pbs then evd.last_mods else d.last_mods in
@@ -1183,12 +1167,12 @@ let drop_side_effects evd =
 let eval_side_effects evd = evd.effects
 
 (* Future goals *)
-let declare_future_goal ?(shelve=false) evk evd =
-  let future_goals = FutureGoals.add ~shelve ~principal:false evk evd.future_goals in
+let declare_future_goal evk evd =
+  let future_goals = FutureGoals.add ~principal:false evk evd.future_goals in
   { evd with future_goals }
 
-let declare_principal_goal ?(shelve=false) evk evd =
-  let future_goals = FutureGoals.add ~shelve ~principal:true evk evd.future_goals in
+let declare_principal_goal evk evd =
+  let future_goals = FutureGoals.add ~principal:true evk evd.future_goals in
   { evd with future_goals }
 
 let push_future_goals evd =
@@ -1201,10 +1185,6 @@ let pop_future_goals evd =
 let fold_future_goals f sigma =
   FutureGoals.fold f sigma sigma.future_goals
 
-let shelve_on_future_goals shelved evd =
-  let future_goals = FutureGoals.put_shelf shelved evd.future_goals in
-  { evd with future_goals }
-
 let remove_future_goal evd evk =
   { evd with future_goals = FutureGoals.remove evk evd.future_goals }
 
@@ -1214,8 +1194,36 @@ let pr_future_goals_stack evd =
 let give_up ev evd =
   { evd with given_up = Evar.Set.add ev evd.given_up }
 
+let push_shelf evd =
+  { evd with shelf = [] :: evd.shelf }
+
+let pop_shelf evd =
+  match evd.shelf with
+  | [] -> anomaly Pp.(str"shelf stack should not be empty")
+  | hd :: tl ->
+    hd, { evd with shelf = tl }
+
+let filter_shelf f evd =
+  { evd with shelf = List.map (List.filter f) evd.shelf }
+
+let shelve evd l =
+  match evd.shelf with
+  | [] -> anomaly Pp.(str"shelf stack should not be empty")
+  | hd :: tl ->
+    { evd with shelf = (hd@l) :: tl }
+
+let unshelve evd l =
+  { evd with shelf = List.map (List.filter (fun ev -> not (CList.mem_f Evar.equal ev l))) evd.shelf }
+
 let given_up evd = evd.given_up
 
+let shelf evd = List.flatten evd.shelf
+
+let pr_shelf evd =
+  let open Pp in
+  if List.is_empty evd.shelf then str"(empty stack)"
+  else prlist_with_sep (fun () -> str"||") (prlist_with_sep spc Evar.print) evd.shelf
+
 (**********************************************************)
 (* Accessing metas *)
 
@@ -1233,6 +1241,7 @@ let set_metas evd metas = {
   evar_names = evd.evar_names;
   future_goals = evd.future_goals;
   given_up = evd.given_up;
+  shelf = evd.shelf;
   extras = evd.extras;
 }
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 9dc106a3d7..9394f9a9dd 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -171,6 +171,10 @@ val has_given_up : evar_map -> bool
 (** [has_given_up sigma] is [true] if and only if
     there are given up evars in [sigma]. *)
 
+val has_shelved : evar_map -> bool
+(** [has_shelved sigma] is [true] if and only if
+    there are shelved evars in [sigma]. *)
+
 val new_evar : evar_map ->
   ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
 (** Creates a fresh evar mapping to the given information. *)
@@ -347,11 +351,11 @@ val drop_side_effects : evar_map -> evar_map
 
 (** {5 Future goals} *)
 
-val declare_future_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map
+val declare_future_goal : Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
     internal uses only. *)
 
-val declare_principal_goal : ?shelve:bool -> Evar.t -> evar_map -> evar_map
+val declare_principal_goal : 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. *)
@@ -360,7 +364,6 @@ module FutureGoals : sig
 
   type t = private {
     comb : Evar.t list;
-    shelf : Evar.t list;
     principal : Evar.t option; (** if [Some e], [e] must be
                                    contained in
                                    [future_comb]. The evar
@@ -385,19 +388,29 @@ val pop_future_goals : evar_map -> FutureGoals.t * evar_map
 
 val fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> evar_map
 
-(** Fold future goals *)
-
-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 pr_future_goals_stack : evar_map -> Pp.t
 
+val push_shelf : evar_map -> evar_map
+
+val pop_shelf : evar_map -> Evar.t list * evar_map
+
+val filter_shelf : (Evar.t -> bool) -> evar_map -> evar_map
+
 val give_up : Evar.t -> evar_map -> evar_map
 
+val shelve : evar_map -> Evar.t list -> evar_map
+
+val unshelve : evar_map -> Evar.t list -> evar_map
+
 val given_up : evar_map -> Evar.Set.t
 
+val shelf : evar_map -> Evar.t list
+
+val pr_shelf : evar_map -> Pp.t
+
 (** {5 Sort variables}
 
     Evar maps also keep track of the universe constraints defined at a given
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 5b0e6f5785..978088872c 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -69,13 +69,13 @@ let dependent_init =
   let src = Loc.tag @@ Evar_kinds.GoalEvar in
   (* Main routine *)
   let rec aux = function
-  | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
+  | TNil sigma -> [], { solution = sigma; comb = [] }
   | TCons (env, sigma, typ, t) ->
     let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in
     let (gl, _) = EConstr.destEvar sigma econstr in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let entry = (econstr, typ) :: ret in
-    entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
+    entry, { solution = sol; comb = with_empty_state gl :: comb }
   in
   fun t ->
     let t = map_telescope_evd Evd.push_future_goals t in
@@ -235,8 +235,6 @@ let apply ~name ~poly env t sp =
   match ans with
   | Nil (e, info) -> Exninfo.iraise (TacticFailure e, info)
   | Cons ((r, (state, _), status, info), _) ->
-    let status = (status, state.shelf) in
-    let state = { state with shelf = [] } in
     r, state, status, Trace.to_tree info
 
 
@@ -621,7 +619,8 @@ let shelve =
   Comb.get >>= fun initial ->
   Comb.set [] >>
   InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve")) >>
-  Shelf.modify (fun gls -> gls @ CList.map drop_state initial)
+  let initial = CList.map drop_state initial in
+  Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution initial })
 
 let shelve_goals l =
   let open Proof in
@@ -629,7 +628,7 @@ let shelve_goals l =
   let comb = CList.filter (fun g -> not (CList.mem (drop_state g) l)) initial in
   Comb.set comb >>
   InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_goals")) >>
-  Shelf.modify (fun gls -> gls @ l)
+  Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution l })
 
 (** [depends_on sigma src tgt] checks whether the goal [src] appears
     as an existential variable in the definition of the goal [tgt] in
@@ -696,7 +695,7 @@ let shelve_unifiable_informative =
   Comb.set n >>
   InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"shelve_unifiable")) >>
   let u = CList.map drop_state u in
-  Shelf.modify (fun gls -> gls @ u) >>
+  Pv.modify (fun pv -> { pv with solution = Evd.shelve pv.solution u }) >>
   tclUNIT u
 
 let shelve_unifiable =
@@ -716,13 +715,17 @@ let guard_no_unifiable =
       let l = CList.map (fun id -> Names.Name id) l in
       tclUNIT (Some l)
 
-(** [unshelve l p] adds all the goals in [l] at the end of the focused
-    goals of p *)
+(** [unshelve l p] moves all the goals in [l] from the shelf and put them at
+    the end of the focused goals of p, if they are still undefined after [advance] *)
 let unshelve l p =
+  let solution = Evd.unshelve p.solution l in
   let l = List.map with_empty_state l in
   (* advance the goals in case of clear *)
   let l = undefined p.solution l in
-  { p with comb = p.comb@l }
+  { comb = p.comb@l; solution }
+
+let filter_shelf f pv =
+  { pv with solution = Evd.filter_shelf f pv.solution }
 
 let mark_in_evm ~goal evd evars =
   let evd =
@@ -750,19 +753,20 @@ let mark_in_evm ~goal evd evars =
 let with_shelf tac =
   let open Proof in
   Pv.get >>= fun pv ->
-  let { shelf; solution } = pv in
-  Pv.set { pv with shelf = []; solution = Evd.push_future_goals solution } >>
+  let { solution } = pv in
+  Pv.set { pv with solution = Evd.push_shelf @@ Evd.push_future_goals solution } >>
   tac >>= fun ans ->
   Pv.get >>= fun npv ->
-  let { shelf = gls; solution = sigma } = npv in
+  let { solution = sigma } = npv in
+  let gls, sigma = Evd.pop_shelf sigma in
   (* The pending future goals are necessarily coming from V82.tactic *)
   (* and thus considered as to shelve, as in Proof.run_tactic *)
   let fgl, sigma = Evd.pop_future_goals sigma in
   (* Ensure we mark and return only unsolved goals *)
-  let gls' = CList.rev_append fgl.Evd.FutureGoals.shelf (CList.rev_append fgl.Evd.FutureGoals.comb gls) in
+  let gls' = CList.rev_append fgl.Evd.FutureGoals.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
+  let npv = { npv with solution = sigma } in
   Pv.set npv >> tclUNIT (gls', ans)
 
 (** [goodmod p m] computes the representative of [p] modulo [m] in the
@@ -993,6 +997,8 @@ let tclProofInfo =
 
 module Unsafe = struct
 
+  let (>>=) = tclBIND
+
   let tclEVARS evd =
     Pv.modify (fun ps -> { ps with solution = evd })
 
@@ -1002,21 +1008,22 @@ module Unsafe = struct
       { step with comb = step.comb @ gls }
     end
 
+  let tclNEWSHELVED gls =
+    Pv.modify begin fun step ->
+      let gls = undefined_evars step.solution gls in
+      { step with solution = Evd.shelve step.solution gls }
+    end
+
+  let tclGETSHELF = tclEVARMAP >>= fun sigma -> tclUNIT @@ Evd.shelf sigma
+
   let tclSETENV = Env.set
 
   let tclGETGOALS = Comb.get
 
   let tclSETGOALS = Comb.set
 
-  let tclGETSHELF = Shelf.get
-
-  let tclSETSHELF = Shelf.set
-
-  let tclPUTSHELF to_shelve =
-    tclBIND tclGETSHELF (fun shelf -> tclSETSHELF (to_shelve@shelf))
-
   let tclEVARSADVANCE evd =
-    Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
+    Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
 
   let tclEVARUNIVCONTEXT ctx =
     Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
@@ -1226,7 +1233,7 @@ module V82 = struct
       let sgs = CList.flatten goalss in
       let sgs = undefined evd sgs in
       InfoL.leaf (Info.Tactic (fun _ _ -> Pp.str"<unknown>")) >>
-      Pv.set { ps with solution = evd; comb = sgs; }
+      Pv.set { solution = evd; comb = sgs; }
     with e when catchable_exception e ->
       let (e, info) = Exninfo.capture e in
       tclZERO ~info e
@@ -1266,7 +1273,7 @@ module V82 = struct
   let of_tactic t gls =
     try
       let env = Global.env () in
-      let init = { shelf = []; solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
+      let init = { solution = gls.Evd.sigma ; comb = [with_empty_state gls.Evd.it] } in
       let name, poly = Names.Id.of_string "legacy_pe", false in
       let (_,final,_,_) = apply ~name ~poly (goal_env env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = CList.map drop_state final.comb }
diff --git a/engine/proofview.mli b/engine/proofview.mli
index db6509c84e..816b45984b 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -162,7 +162,7 @@ val apply
   -> 'a tactic
   -> proofview
   -> 'a * proofview
-       * (bool*Evar.t list)
+       * bool
        * Proofview_monad.Info.tree
 
 (** {7 Monadic primitives} *)
@@ -331,17 +331,16 @@ val unifiable : Evd.evar_map -> Evar.t -> Evar.t list -> bool
     considered). *)
 val shelve_unifiable : unit tactic
 
-(** Idem but also returns the list of shelved variables *)
-val shelve_unifiable_informative : Evar.t list tactic
-
 (** [guard_no_unifiable] returns the list of unifiable goals if some
     goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
 val guard_no_unifiable : Names.Name.t list option tactic
 
-(** [unshelve l p] adds all the goals in [l] at the end of the focused
-    goals of p *)
+(** [unshelve l p] moves all the goals in [l] from the shelf and put them at
+    the end of the focused goals of p, if they are still undefined after [advance] *)
 val unshelve : Evar.t list -> proofview -> proofview
 
+val filter_shelf : (Evar.t -> bool) -> proofview -> proofview
+
 (** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
 val depends_on : Evd.evar_map -> Evar.t -> Evar.t -> bool
 
@@ -454,6 +453,10 @@ module Unsafe : sig
       goal is already solved, it is not added. *)
   val tclNEWGOALS : Proofview_monad.goal_with_state list -> unit tactic
 
+  (** [tclNEWSHELVED gls] adds the goals [gls] to the shelf. If a
+      goal is already solved, it is not added. *)
+  val tclNEWSHELVED : Evar.t list -> unit tactic
+
   (** [tclSETGOALS gls] sets goals [gls] as the goals being under focus. If a
       goal is already solved, it is not set. *)
   val tclSETGOALS : Proofview_monad.goal_with_state list -> unit tactic
@@ -461,15 +464,9 @@ module Unsafe : sig
   (** [tclGETGOALS] returns the list of goals under focus. *)
   val tclGETGOALS : Proofview_monad.goal_with_state list tactic
 
-  (** [tclSETSHELF gls] sets goals [gls] as the current shelf. *)
-  val tclSETSHELF : Evar.t list -> unit tactic
-
   (** [tclGETSHELF] returns the list of goals on the shelf. *)
   val tclGETSHELF : Evar.t list tactic
 
-  (** [tclPUTSHELF] appends goals to the shelf. *)
-  val tclPUTSHELF : Evar.t list -> unit tactic
-
   (** Sets the evar universe context. *)
   val tclEVARUNIVCONTEXT : UState.t -> unit tactic
 
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml
index 4b3dd8f633..df9fc5dab3 100644
--- a/engine/proofview_monad.ml
+++ b/engine/proofview_monad.ml
@@ -166,7 +166,6 @@ let map_goal_with_state f (g, s) = (f g, s)
 type proofview = {
   solution : Evd.evar_map;
   comb : goal_with_state list;
-  shelf : goal list;
 }
 
 (** {6 Instantiation of the logic monad} *)
@@ -238,14 +237,6 @@ module Status : Writer with type t := bool = struct
   let put s = Logical.put s
 end
 
-module Shelf : State with type t = goal list = struct
-    (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
-  type t = goal list
-  let get = Logical.map (fun {shelf} -> shelf) Pv.get
-  let set c = Pv.modify (fun pv -> { pv with shelf = c })
-  let modify f = Pv.modify (fun pv -> { pv with shelf = f pv.shelf })
-end
-
 (** Lens and utilities pertaining to the info trace *)
 module InfoL = struct
   let recording = Logical.(map (fun {P.trace} -> trace) current)
diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index af866528c8..6cca3f5a5e 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -83,7 +83,6 @@ val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state
 type proofview = {
   solution : Evd.evar_map;
   comb : goal_with_state list;
-  shelf : goal list;
 }
 
 (** {6 Instantiation of the logic monad} *)
@@ -137,10 +136,6 @@ module Env : State with type t := Environ.env
 (** Lens to the tactic status ([true] if safe, [false] if unsafe) *)
 module Status : Writer with type t := bool
 
-(** Lens to the list of goals which have been shelved during the
-    execution of the tactic. *)
-module Shelf : State with type t = goal list
-
 (** Lens and utilities pertaining to the info trace *)
 module InfoL : sig
   (** [record_trace t] behaves like [t] and compute its [info] trace. *)
diff --git a/engine/termops.ml b/engine/termops.ml
index 7579631313..ac6870a39e 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -301,10 +301,12 @@ let pr_evar_map_gen with_univs pr_evars env sigma =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
       str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma
+  and shelf =
+    str "SHELF:" ++ brk (0, 1) ++ Evd.pr_shelf sigma ++ fnl ()
   and future_goals =
     str "FUTURE GOALS STACK:" ++ brk (0, 1) ++ Evd.pr_future_goals_stack sigma ++ fnl ()
   in
-  evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ future_goals
+  evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ shelf ++ future_goals
 
 let pr_evar_list env sigma l =
   let open Evd in