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>

1 files changed, 45 insertions, 36 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;
 }