From d2c50bb29df8f0b23f7ee498abeda43a672fc688 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 Dec 2017 08:58:50 +0100
Subject: Proof engine: consider the pair principal and future goals as an
 entity.

---
 engine/evd.ml       | 2 +-
 engine/evd.mli      | 2 +-
 engine/proofview.ml | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index 185cab1019..e0453713e5 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -946,7 +946,7 @@ let principal_future_goal evd = evd.principal_future_goal
 let reset_future_goals evd =
   { evd with future_goals = [] ; principal_future_goal=None }
 
-let restore_future_goals evd gls pgl =
+let restore_future_goals evd (gls,pgl) =
   { evd with future_goals = gls ; principal_future_goal = pgl }
 
 (**********************************************************)
diff --git a/engine/evd.mli b/engine/evd.mli
index 49c953f6d3..49632d2e76 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -303,7 +303,7 @@ 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 restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map
+val restore_future_goals : evar_map -> Evar.t list * Evar.t option -> 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
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 8a844bbf54..4f8da53787 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -771,7 +771,7 @@ let with_shelf tac =
   let gls' = Evd.future_goals sigma in
   let fgoals = Evd.future_goals solution in
   let pgoal = Evd.principal_future_goal solution in
-  let sigma = Evd.restore_future_goals sigma fgoals pgoal in
+  let sigma = Evd.restore_future_goals sigma (fgoals,pgoal) in
   (* Ensure we mark and return only unsolved goals *)
   let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
   let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
-- 
cgit v1.2.3


From e508aec3a90aca93c188c54b707d19114ef5ff83 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 Dec 2017 09:01:45 +0100
Subject: Proof engine: adding a function to save future goals including
 principal one.

---
 engine/evd.ml  | 2 ++
 engine/evd.mli | 4 ++++
 2 files changed, 6 insertions(+)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index e0453713e5..60bc2eb40d 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -943,6 +943,8 @@ let future_goals evd = evd.future_goals
 
 let principal_future_goal evd = evd.principal_future_goal
 
+let save_future_goals evd = (evd.future_goals, evd.principal_future_goal)
+
 let reset_future_goals evd =
   { evd with future_goals = [] ; principal_future_goal=None }
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 49632d2e76..44ec4a7e5c 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -299,6 +299,10 @@ 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. *)
 
+val save_future_goals : evar_map -> Evar.t list * Evar.t option
+(** Retrieves the list of future goals including the principal future
+    goal. Used by the [refine] primitive of the tactic engine. *)
+
 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. *)
-- 
cgit v1.2.3


From bfb393596b1df815a109c9c600b9a2b413561fcb Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 Dec 2017 09:30:26 +0100
Subject: Proof engine: using save_future_goal when relevant.

---
 engine/proofview.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 4f8da53787..73f26c3208 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -769,9 +769,8 @@ let with_shelf tac =
   Pv.get >>= fun npv ->
   let { shelf = gls; solution = sigma } = npv in
   let gls' = Evd.future_goals sigma in
-  let fgoals = Evd.future_goals solution in
-  let pgoal = Evd.principal_future_goal solution in
-  let sigma = Evd.restore_future_goals sigma (fgoals,pgoal) in
+  let fgoals = Evd.save_future_goals solution in
+  let sigma = Evd.restore_future_goals sigma fgoals in
   (* Ensure we mark and return only unsolved goals *)
   let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
   let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
-- 
cgit v1.2.3


From b731022c022cfeae9203f6b10b4e1f68b85d9071 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 17 Feb 2018 22:59:32 +0100
Subject: Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe.

Adding also tclSETSHELF/tclGETSHELF by consistency with
tclSETGOALS/tclGETGOALS.

However, I feel that this is too low-level to be exported as a
"tcl". Doesn't a "tcl" mean that it is supposed to be used by common
tactics? But is it reasonable that a common tactic can change and
modify comb and shelf without passing by a level which e.g. checks
that no goal is lost in the process.

So, I would rather be in favor of removing tclSETGOALS/tclGETGOALS
which are anyway aliases for Comb.get/Comb.set.

Conversely, what is the right expected level of abstraction for
proofview.ml?
---
 engine/proofview.ml  |  9 +++++++++
 engine/proofview.mli | 12 ++++++++++++
 2 files changed, 21 insertions(+)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 73f26c3208..53b3cdd9b5 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1010,6 +1010,15 @@ module Unsafe = struct
 
   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 tclPUTGIVENUP = Giveup.put
+
   let tclEVARSADVANCE evd =
     Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 4862791874..e7be665527 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -435,6 +435,18 @@ 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
+
+  (** [tclPUTGIVENUP] add an given up goal. *)
+  val tclPUTGIVENUP : Evar.t list -> unit tactic
+
   (** Sets the evar universe context. *)
   val tclEVARUNIVCONTEXT : UState.t -> unit tactic
 
-- 
cgit v1.2.3


From 6f30f76def8f6cf1abe7859f482b68c91b4c8709 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 Dec 2017 09:32:51 +0100
Subject: Proof engine: support for nesting tactic-in-term within other
 tactics.

Tactic-in-term can be called from within a tactic itself. We have to
preserve the preexisting future_goals (if called from pretyping) and
we have to inform of the existence of pending goals, using
future_goals which is the only way to tell it in the absence of being
part of an encapsulating proofview.

This fixes #6313.

Conversely, future goals, created by pretyping, can call ltac:(giveup) or
ltac:(shelve), and this has to be remembered. So, we do it.
---
 engine/evd.ml  | 71 +++++++++++++++++++++++++++++++++++++++++++++++++---------
 engine/evd.mli | 31 +++++++++++++++++++++----
 2 files changed, 88 insertions(+), 14 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index 60bc2eb40d..b7b87370e2 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -408,6 +408,8 @@ let key id (_, idtoev) =
 
 end
 
+type goal_kind = ToShelve | ToGiveUp
+
 type evar_map = {
   (** Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -432,6 +434,7 @@ type evar_map = {
                                              name) of the evar which
                                              will be instantiated with
                                              a term containing [e]. *)
+  future_goals_status : goal_kind EvMap.t;
   extras : Store.t;
 }
 
@@ -471,7 +474,8 @@ let remove d e =
   | Some e' -> if Evar.equal e e' then None else d.principal_future_goal
   in
   let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
-  { d with undf_evars; defn_evars; principal_future_goal; future_goals }
+  let future_goals_status = EvMap.remove e d.future_goals_status in
+  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status }
 
 let find d e =
   try EvMap.find e d.undf_evars
@@ -581,6 +585,7 @@ let empty = {
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
   future_goals = [];
   principal_future_goal = None;
+  future_goals_status = EvMap.empty;
   extras = Store.empty;
 }
 
@@ -929,27 +934,72 @@ let drop_side_effects evd =
 let eval_side_effects evd = evd.effects
 
 (* Future goals *)
-let declare_future_goal evk evd =
-  { evd with future_goals = evk::evd.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 evk evd =
+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; }
+    principal_future_goal=Some evk;
+    future_goals_status = Option.fold_right (EvMap.add evk) tag evd.future_goals_status;
+    }
   | 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 future_goals evd = evd.future_goals
 
 let principal_future_goal evd = evd.principal_future_goal
 
-let save_future_goals evd = (evd.future_goals, evd.principal_future_goal)
+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 }
-
-let restore_future_goals evd (gls,pgl) =
-  { evd with future_goals = gls ; principal_future_goal = pgl }
+  { 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 fold_future_goals f sigma (gls,pgl,map) =
+  List.fold_left f sigma gls
+
+let map_filter_future_goals f (gls,pgl,map) =
+  (* 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 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 dispatch_future_goals_gen distinguish_shelf (gls,pgl,map) =
+  let rec aux (comb,shelf,givenup as acc) = function
+    | [] -> acc
+    | evk :: gls ->
+       let acc =
+        try match EvMap.find evk map with
+        | ToGiveUp -> (comb,shelf,evk::givenup)
+        | ToShelve ->
+           if distinguish_shelf then (comb,evk::shelf,givenup)
+           else raise Not_found
+        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 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
+  (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)
 
 (**********************************************************)
 (* Accessing metas *)
@@ -966,6 +1016,7 @@ 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;
   extras = evd.extras;
 }
diff --git a/engine/evd.mli b/engine/evd.mli
index 44ec4a7e5c..bd9d75c6b0 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -282,11 +282,13 @@ val drop_side_effects : evar_map -> evar_map
 
 (** {5 Future goals} *)
 
-val declare_future_goal : Evar.t -> evar_map -> evar_map
+type goal_kind = ToShelve | ToGiveUp
+
+val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map
 (** Adds an existential variable to the list of future goals. For
     internal uses only. *)
 
-val declare_principal_goal : Evar.t -> evar_map -> evar_map
+val declare_principal_goal : ?tag:goal_kind -> 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. *)
@@ -299,7 +301,9 @@ 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. *)
 
-val save_future_goals : evar_map -> Evar.t list * Evar.t option
+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. *)
 
@@ -307,12 +311,31 @@ 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 restore_future_goals : evar_map -> Evar.t list * Evar.t option -> 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 fold_future_goals : (evar_map -> Evar.t -> evar_map) -> evar_map -> future_goals -> evar_map
+(** Fold future goals *)
+
+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) -> future_goals -> future_goals
+(** 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
+(** 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
+(** An ad hoc variant for Proof.proof; not for general use *)
+
+val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals
+(** Push goals on the shelve of future goals *)
+
 (** {5 Sort variables}
 
     Evar maps also keep track of the universe constraints defined at a given
-- 
cgit v1.2.3


From 29aa2d94b253dad0ade8c877fd7f46b8537a5847 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 21 Feb 2018 23:37:26 +0100
Subject: A comment in Proofview.with_shelf.

---
 engine/proofview.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine')

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 53b3cdd9b5..22271dd02c 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -768,6 +768,8 @@ let with_shelf tac =
   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
-- 
cgit v1.2.3