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

4 files changed, 49 insertions, 0 deletions

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