A tactic shelve_unifiable.

Puts on the shelf every goals under focus on which other goals under focus
depend. Useful when we want to solve these goals by unification (as in a
first order proof search procedure, for instance).

Also meant to be able to recover approximately the semantics of the old
refine with the new implementation (use refine t; shelve_unifiable).

TODO: bug dans l'example de shelve_unifiable

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17017 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 83 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 81e7db6dc..a78e3448e 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4621,6 +4621,26 @@ This tactic moves all goals under focus to a shelf. While on the shelf, goals
 will not be focused on. They can be solved by unification, or they can be called
 back into focus with the command {\tt Unshelve} (Section~\ref{unshelve}).
 
+\begin{Variants}
+  \item \texttt{shelve\_unifiable}\tacindex{shelve\_unifiable}
+
+    Shelves only these goals under focused which are mentioned in other goals.
+    Goals which appear in the type of other goals can be solve by unification.
+    
+\Example
+\begin{coq_example}
+Goal exists n, n=0.
+refine (ex_intro _ _ _).
+all:shelve_unifiable.
+reflexivity.
+\end{coq_example}
+
+\begin{coq_eval}
+Reset Initial.
+\end{coq_eval}
+
+\end{Variants}
+
 \subsection[\tt Unshelve]{\tt Unshelve\comindex{Unshelve}\label{unshelve}}
 
 This command moves all the goals on the shelf (see Section~\ref{shelve}) from the
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 5601cef82..a9a0be28d 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -84,6 +84,32 @@ let equal evars1 gl1 evars2 gl2 =
   let evi2 = content evars2 gl2 in
   Evd.eq_evar_info evi1 evi2
 
+(* [contained_in_info e evi] checks whether the evar [e] appears in
+   the hypotheses, the conclusion or the body of the evar_info
+   [evi]. Note: since we want to use it on goals, the body is actually
+   supposed to be empty. *)
+let contained_in_info e evi =
+  Evar.Set.mem e (Evarutil.evars_of_evar_info evi)
+
+(* [depends_on sigma src tgt] checks whether the goal [src] appears as an
+   existential variable in the definition of the goal [tgt] in [sigma]. *)
+let depends_on sigma src tgt =
+  let evi = Evd.find sigma tgt.content in
+  contained_in_info src.content evi
+
+(* [unifiable sigma g l] checks whether [g] appears in another subgoal
+   of [l]. The list [l] may contain [g], but it does not affect the
+   result. *)
+let unifiable sigma g l =
+  List.exists (fun tgt -> g != tgt && depends_on sigma g tgt) l
+
+(* [partition_unifiable sigma l] partitions [l] into a pair [(u,n)]
+   where [u] is composed of the unifiable goals, i.e. the goals on
+   whose definition other goals of [l] depend, and [n] are the
+   non-unifiable goals. *)
+let partition_unifiable sigma l =
+  List.partition (fun g -> unifiable sigma g l) l
+
 (*** Goal tactics ***)
 
 
diff --git a/proofs/goal.mli b/proofs/goal.mli
index fb6c9ddb1..39c7ed793 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -35,6 +35,12 @@ val advance : Evd.evar_map -> goal -> goal option
    and conclusion are equal. *)
 val equal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
+(* [partition_unifiable sigma l] partitions [l] into a pair [(u,n)]
+   where [u] is composed of the unifiable goals, i.e. the goals on
+   whose definition other goals of [l] depend, and [n] are the
+   non-unifiable goals. *)
+val partition_unifiable : Evd.evar_map -> goal list -> goal list * goal list
+
 (*** Goal tactics ***)
 
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 40b9c0f8a..f08689538 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -576,6 +576,18 @@ let shelve =
   Proof.set {initial with comb=[]} >>
   Proof.put (true,initial.comb)
 
+(* Shelves the unifiable goals under focus, i.e. the goals which
+   appear in other goals under focus (the unfocused goals are not
+   considered). *)
+let shelve_unifiable =
+  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+  let (>>=) = Proof.bind in
+  let (>>) = Proof.seq in
+  Proof.get >>= fun initial ->
+  let (u,n) = Goal.partition_unifiable initial.solution initial.comb in
+  Proof.set {initial with comb=n} >>
+  Proof.put (true,u)
+
 (* [unshelve l p] adds all the goals in [l] at the end of the focused
    goals of p *)
 let unshelve l p =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index c483cd371..0899f52dd 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -214,6 +214,11 @@ val tclENV : Environ.env tactic
    shelf for later use (or being solved by side-effects). *)
 val shelve : unit tactic
 
+(* Shelves the unifiable goals under focus, i.e. the goals which
+   appear in other goals under focus (the unfocused goals are not
+   considered). *)
+val shelve_unifiable : unit tactic
+
 (* [unshelve l p] adds all the goals in [l] at the end of the focused
    goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 44719a962..a7a89eae7 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -810,6 +810,14 @@ TACTIC EXTEND shelve
     [ Proofview.shelve ]
 END
 
+(* Shelves the unifiable goals under focus, i.e. the goals which
+   appear in other goals under focus (the unfocused goals are not
+   considered). *)
+TACTIC EXTEND shelve_unifiable
+| [ "shelve_unifiable" ] ->
+    [ Proofview.shelve_unifiable ]
+END
+
 (* Command to add every unshelved variables to the focus *)
 VERNAC COMMAND EXTEND Unshelve
 [ "Unshelve" ]
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index cb4bc01a3..eae2be017 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2206,6 +2206,12 @@ and interp_atomic ist tac =
       end
 
   (* For extensions *)
+  | TacExtend (loc,opn,[]) ->
+      (* spiwack: a special case for tactics (from TACTIC EXTEND) without arguments to
+         be interpreted without a [Proofview.Goal.enter]. Eventually we should make
+         something more fine-grained by modifying [interp_genarg]. *)
+      let tac = lookup_tactic opn in
+      tac [] ist
   | TacExtend (loc,opn,l) ->
       Proofview.Goal.enter begin fun gl ->
       let goal_sigma = Proofview.Goal.sigma gl in