Adding an unshelve tactical.

This tactical is inspired by discussions on the Coq-club list. For now
it is still undocumented, and there is room left for design issues.

4 files changed, 48 insertions, 24 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 59a64658dc..5981ad32da 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -32,7 +32,7 @@ type entry = (Term.constr * Term.types) list
 let proofview p =
   p.comb , p.solution
 
-let compact el { comb; solution } =
+let compact el ({ solution } as pv) =
   let nf = Evarutil.nf_evar solution in
   let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
   let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
@@ -45,7 +45,7 @@ let compact el { comb; solution } =
   let new_solution = Evd.raw_map_undefined apply_subst_einfo pruned_solution in
   let new_size = Evd.fold (fun _ _ i -> i+1) new_solution 0 in
   msg_info (Pp.str (Printf.sprintf "Evars: %d -> %d\n" size new_size));
-  new_el, { comb; solution = new_solution }
+  new_el, { pv with solution = new_solution; }
 
 
 (** {6 Starting and querying a proof view} *)
@@ -62,13 +62,13 @@ let dependent_init =
   let src = (Loc.ghost,Evar_kinds.GoalEvar) in
   (* Main routine *)
   let rec aux = function
-  | TNil sigma -> [], { solution = sigma; comb = []; }
+  | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
     let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
-    entry, { solution = sol; comb = gl :: comb; }
+    entry, { solution = sol; comb = gl :: comb; shelf = [] }
   in
   fun t ->
     let entry, v = aux t in
@@ -232,6 +232,9 @@ let apply env t sp =
   match ans with
   | Nil (e, info) -> iraise (TacticFailure e, info)
   | Cons ((r, (state, _), status, info), _) ->
+    let (status, gaveup) = status in
+    let status = (status, state.shelf, gaveup) in
+    let state = { state with shelf = [] } in
     r, state, status, Trace.to_tree info
 
 
@@ -578,7 +581,7 @@ let shelve =
   Comb.get >>= fun initial ->
   Comb.set [] >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
-  Shelf.put initial
+  Shelf.modify (fun gls -> gls @ initial)
 
 
 (** [contained_in_info e evi] checks whether the evar [e] appears in
@@ -617,7 +620,7 @@ let shelve_unifiable =
   let (u,n) = partition_unifiable initial.solution initial.comb in
   Comb.set n >>
   InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
-  Shelf.put u
+  Shelf.modify (fun gls -> gls @ u)
 
 (** [guard_no_unifiable] fails with error [UnresolvedBindings] if some
     goals are unifiable (see {!shelve_unifiable}) in the current focus. *)
@@ -639,6 +642,14 @@ let unshelve l p =
   let l = undefined p.solution l in
   { p with comb = p.comb@l }
 
+let with_shelf tac =
+  let open Proof in
+  Shelf.get >>= fun shelf ->
+  Shelf.set [] >>
+  tac >>= fun ans ->
+  Shelf.get >>= fun gls ->
+  Shelf.set shelf >>
+  tclUNIT (gls, ans)
 
 (** [goodmod p m] computes the representative of [p] modulo [m] in the
     interval [[0,m-1]].*)
@@ -867,7 +878,7 @@ module Unsafe = struct
   let tclSETGOALS = Comb.set
 
   let tclEVARSADVANCE evd =
-    Pv.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb })
+    Pv.modify (fun ps -> { ps with solution = evd; comb = undefined evd ps.comb })
 
   let tclEVARUNIVCONTEXT ctx = 
     Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
@@ -1085,7 +1096,7 @@ struct
     let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
     let open Proof in
     InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
-    Pv.set { solution = sigma; comb; }
+    Pv.modify (fun ps -> { ps with solution = sigma; comb; })
   end
 
   (** Useful definitions *)
@@ -1164,7 +1175,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 { solution = evd; comb = sgs; }
+      Pv.set { ps with solution = evd; comb = sgs; }
     with e when catchable_exception e ->
       let (e, info) = Errors.push e in
       tclZERO ~info e
@@ -1176,7 +1187,7 @@ module V82 = struct
     Pv.modify begin fun ps ->
     let map g s = GoalV82.nf_evar s g in
     let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in
-    { solution = evd; comb = goals; }
+    { ps with solution = evd; comb = goals; }
     end
       
   let has_unresolved_evar pv =
@@ -1221,7 +1232,7 @@ module V82 = struct
 
   let of_tactic t gls =
     try
-      let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
+      let init = { shelf = []; solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
       let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
     with Logic_monad.TacticFailure e as src ->
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 927df33a0c..659b783cb2 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -303,6 +303,10 @@ val guard_no_unifiable : unit tactic
     goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview
 
+(** [with_shelf tac] executes [tac] and returns its result together with the set
+    of goals shelved by [tac]. The current shelf is unchanged. *)
+val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
+
 (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
     is negative, then it puts the [n] last goals first.*)
 val cycle : int -> unit tactic
diff --git a/proofs/proofview_monad.ml b/proofs/proofview_monad.ml
index 6e68cd2e45..a9faf0a833 100644
--- a/proofs/proofview_monad.ml
+++ b/proofs/proofview_monad.ml
@@ -157,8 +157,11 @@ end
 
 (** Type of proof views: current [evar_map] together with the list of
     focused goals. *)
-type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
-
+type proofview = {
+  solution : Evd.evar_map;
+  comb : Goal.goal list;
+  shelf : Goal.goal list;
+}
 
 (** {6 Instantiation of the logic monad} *)
 
@@ -171,10 +174,10 @@ module P = struct
   type e = bool
 
   (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * Evar.t list * Evar.t list
+  type w = bool * Evar.t list
 
-  let wunit = true , [] , []
-  let wprod (b1,s1,g1) (b2,s2,g2) = b1 && b2 , s1@s2 , g1@g2
+  let wunit = true , []
+  let wprod (b1, g1) (b2, g2) = b1 && b2 , g1@g2
 
   type u = Info.state
 
@@ -226,19 +229,21 @@ module Env : State with type t := Environ.env = struct
 end
 
 module Status : Writer with type t := bool = struct
-  let put s = Logical.put (s,[],[])
+  let put s = Logical.put (s, [])
 end
 
-module Shelf : Writer with type t = Evar.t list = struct
+module Shelf : State with type t = Evar.t list = struct
     (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
   type t = Evar.t list
-  let put sh = Logical.put (true,sh,[])
+  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
 
 module Giveup : Writer with type t = Evar.t list = struct
     (* spiwack: I don't know why I cannot substitute ([:=]) [t] with a type expression. *)
   type t = Evar.t list
-  let put gs = Logical.put (true,[],gs)
+  let put gs = Logical.put (true, gs)
 end
 
 (** Lens and utilies pertaining to the info trace *)
diff --git a/proofs/proofview_monad.mli b/proofs/proofview_monad.mli
index d2a2e55fb1..a172259170 100644
--- a/proofs/proofview_monad.mli
+++ b/proofs/proofview_monad.mli
@@ -68,15 +68,19 @@ end
 
 (** Type of proof views: current [evar_map] together with the list of
     focused goals. *)
-type proofview = { solution : Evd.evar_map; comb : Goal.goal list }
+type proofview = {
+  solution : Evd.evar_map;
+  comb : Goal.goal list;
+  shelf : Goal.goal list;
+}
 
 (** {6 Instantiation of the logic monad} *)
 
 module P : sig
   type s = proofview * Environ.env
 
-  (** Status (safe/unsafe) * shelved goals * given up *)
-  type w = bool * Evar.t list * Evar.t list
+  (** Status (safe/unsafe) * given up *)
+  type w = bool * Evar.t list
 
   val wunit : w
   val wprod : w -> w -> w
@@ -123,7 +127,7 @@ 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 : Writer with type t = Evar.t list
+module Shelf : State with type t = Evar.t list
 
 (** Lens to the list of goals which were given up during the execution
     of the tactic. *)