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.

1 files changed, 22 insertions, 11 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 59a64658d..5981ad32d 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 ->