Fix backtracking heuristic in typeclass resolution.

Now that backtracking is working correctly, we need to avoid a
non-termination issue introduced by the [RelCompFun] definition in
RelationPairs, by adding a [Measure] typeclass. It could be used to have
a uniform notation for measures/interpretations in Numbers and be but in
the interfaces too, only the mimimal change was implemented.
Fix syntax change in test-suite scripts.


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

10 files changed, 79 insertions, 35 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 558ee34d6..6e28cf713 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -348,23 +348,47 @@ let hints_tac hints =
       | [] -> fk ()
     in aux 1 tacs }
 
+let evars_of_term c =
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) -> Intset.add n acc
+    | _ -> fold_constr evrec acc c
+  in evrec Intset.empty c
+
+exception Found_evar of int
+
+let occur_evars evars c =
+  try
+    let rec evrec c =
+      match kind_of_term c with
+      | Evar (n, _) -> if Intset.mem n evars then raise (Found_evar n) else ()
+      | _ -> iter_constr evrec c
+    in evrec c; false
+  with Found_evar _ -> true
+
+let dependent only_classes evd oev concl =
+  let concl_evars = Intset.union (evars_of_term concl)
+    (Option.cata Intset.singleton Intset.empty oev)
+  in not (Intset.is_empty concl_evars)
+
 let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
   let rec aux s (acc : (autogoal list * validation) list) fk = function
     | (gl,info) :: gls ->
 	second.skft (fun ({it=gls';sigma=s'},v') fk' ->
-	  let fk'' = if gls' = [] && Evarutil.is_ground_term s gl.evar_concl then
-	    (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl); fk) else fk' in
-	  let s' = 
+	  let s', needs_backtrack = 
 	    if gls' = [] then
 	      match info.is_evar with
 	      | Some ev -> 
 		  let prf = v' s' [] in
 		  let term, _ = Refiner.extract_open_proof s' prf in
-		    Evd.define ev term s'
-	      | None -> s'
-	    else s'
+		    Evd.define ev term s', dependent info.only_classes s' (Some ev) gl.evar_concl
+	      | None -> s', dependent info.only_classes s' None gl.evar_concl
+	    else s', true
 	  in
-	    aux s' ((gls',v')::acc) fk'' gls) fk {it = (gl,info); sigma = s}
+	  let fk'' = if not needs_backtrack then
+	    (if !typeclasses_debug then msgnl (str"no backtrack on " ++ pr_ev s gl); fk) else fk' 
+	  in aux s' ((gls',v')::acc) fk'' gls)
+	  fk {it = (gl,info); sigma = s}
     | [] -> Some (List.rev acc, s, fk)
   in fun ({it = gls; sigma = s},v) fk ->
     let rec aux' = function
diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v
index a6f1e299b..b4efa7edc 100644
--- a/test-suite/success/AdvancedTypeClasses.v
+++ b/test-suite/success/AdvancedTypeClasses.v
@@ -1,4 +1,4 @@
-Generalizable Variables all.
+Generalizable All Variables.
 
 Open Scope type_scope.
 
@@ -57,7 +57,7 @@ Instance FunCan `(interp_pair a, interp_pair b) : interp_pair (a -> b) :=
 Instance BoolCan : interp_pair bool :=
   { repr := Bool ; link := refl_equal _ }.
 
-Instance VarCan : interp_pair x | 10 := { repr := Var x ; link := refl_equal _ }.
+Instance VarCan x : interp_pair x | 10 := { repr := Var x ; link := refl_equal _ }.
 Instance SetCan : interp_pair Set := { repr := SET ; link := refl_equal _ }.
 Instance PropCan : interp_pair Prop := { repr := PROP ; link := refl_equal _ }.
 Instance TypeCan : interp_pair Type := { repr := TYPE ; link := refl_equal _ }.
diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
index 4ec0a79ba..de34e007d 100644
--- a/test-suite/success/Generalization.v
+++ b/test-suite/success/Generalization.v
@@ -1,4 +1,4 @@
-Generalizable Variables all.
+Generalizable All Variables.
 
 Check `(a = 0).
 Check `(a = 0)%type.
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index a19515d06..fe0165d08 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -50,7 +50,7 @@ Notation " Γ  ; Δ " := (conc Δ Γ) (at level 25, left associativity) : contex
 
 Reserved Notation " Γ ⊢ τ " (at level 30, no associativity).
 
-Generalizable Variables all.
+Generalizable All Variables.
 
 Inductive term : ctx -> type -> Type :=
 | ax : `(Γ, τ ⊢ τ)
@@ -79,7 +79,7 @@ Proof with simpl in * ; eqns ; eauto with lambda.
 
   destruct Δ as [|Δ τ'']...
     apply abs.
-    specialize (IHterm Γ (Δ, τ'', τ0) τ'0)...
+    specialize (IHterm Γ (Δ, τ'', τ))...
 
   intro. eapply app...
 Defined.
@@ -100,7 +100,7 @@ Proof with simpl in * ; eqns ; eauto.
     apply weak...
 
   apply abs...
-    specialize (IHterm Γ (Δ, τ0))...
+    specialize (IHterm Γ (Δ, τ))...
 
   eapply app...
 Defined.
@@ -127,5 +127,5 @@ Inductive Ev : forall t, Exp t -> Exp t -> Prop :=
                Ev (Fst e) e1.
 
 Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2).
-intros t1 t2 e e1 ev. dependent destruction ev. exists e3 ; assumption.
+intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption.
 Qed.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index ecc8ecb79..7ae221d44 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -21,9 +21,6 @@ Implicit Arguments pair [[A] [B]].
 
 (* /NB *)
 
-
-(* NB: is signature_scope the right one for that ? *)
-
 Arguments Scope relation_conjunction
  [type_scope signature_scope signature_scope].
 Arguments Scope relation_equivalence
@@ -37,7 +34,7 @@ Arguments Scope PER [type_scope signature_scope].
 Arguments Scope Equivalence [type_scope signature_scope].
 Arguments Scope StrictOrder [type_scope signature_scope].
 
-Generalizable Variables A B RA RB Ri Ro.
+Generalizable Variables A B RA RB Ri Ro f.
 
 (** Any function from [A] to [B] allow to obtain a relation over [A]
     out of a relation over [B]. *)
@@ -47,6 +44,16 @@ Definition RelCompFun {A B}(R:relation B)(f:A->B) : relation A :=
 
 Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope.
 
+(** We declare measures to the system using the [Measure] class. 
+   Otherwise the instances would easily introduce loops, 
+   never instantiating the [f] function.  *)
+
+Class Measure {A B} (f : A -> B).
+
+(** Standard measures. *)
+
+Instance fst_measure : @Measure (A * B) A fst.
+Instance snd_measure : @Measure (A * B) B snd.
 
 (** We define a product relation over [A*B]: each components should
     satisfy the corresponding initial relation. *)
@@ -56,28 +63,32 @@ Definition RelProd {A B}(RA:relation A)(RB:relation B) : relation (A*B) :=
 
 Infix "*" := RelProd : signature_scope.
 
+Section RelCompFun_Instances.
+  Context {A B : Type} (R : relation B).
 
-Instance RelCompFun_Reflexive {A B}(R:relation B)(f:A->B)
- `(Reflexive _ R) : Reflexive (R@@f).
-Proof. firstorder. Qed.
+  Global Instance RelCompFun_Reflexive
+    `(Measure A B f, Reflexive _ R) : Reflexive (R@@f).
+  Proof. firstorder. Qed. 
+    
+  Global Instance RelCompFun_Symmetric
+    `(Measure A B f, Symmetric _ R) : Symmetric (R@@f).
+  Proof. firstorder. Qed.
+      
+  Global Instance RelCompFun_Transitive
+    `(Measure A B f, Transitive _ R) : Transitive (R@@f).
+  Proof. firstorder. Qed.
 
-Instance RelCompFun_Symmetric {A B}(R:relation B)(f:A->B)
- `(Symmetric _ R) : Symmetric (R@@f).
-Proof. firstorder. Qed.
+  Global Instance RelCompFun_Irreflexive
+    `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f).
+  Proof. firstorder. Qed.
 
-Instance RelCompFun_Transitive {A B}(R:relation B)(f:A->B)
- `(Transitive _ R) : Transitive (R@@f).
-Proof. firstorder. Qed.
-
-Instance RelCompFun_Irreflexive {A B}(R:relation B)(f:A->B)
- `(Irreflexive _ R) : Irreflexive (R@@f).
-Proof. firstorder. Qed.
+  Global Instance RelCompFun_Equivalence
+    `(Measure A B f, Equivalence _ R) : Equivalence (R@@f).
 
-Instance RelCompFun_Equivalence {A B}(R:relation B)(f:A->B)
- `(Equivalence _ R) : Equivalence (R@@f).
+  Global Instance RelCompFun_StrictOrder
+    `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f).
 
-Instance RelCompFun_StrictOrder {A B}(R:relation B)(f:A->B)
- `(StrictOrder _ R) : StrictOrder (R@@f).
+End RelCompFun_Instances.
 
 Instance RelProd_Reflexive {A B}(RA:relation A)(RB:relation B)
  `(Reflexive _ RA, Reflexive _ RB) : Reflexive (RA*RB).
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index a2a686d94..ec432de83 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -605,6 +605,10 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
 
   (** Specification of [lt] *)
   Instance lt_strorder : StrictOrder lt.
+  Proof. constructor ; unfold lt; red.
+    unfold complement. red. intros. apply (irreflexivity H).
+    intros. transitivity y; auto.
+  Qed.
 
   Instance lt_compat : Proper (eq==>eq==>iff) lt.
   Proof.
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index b99df747a..da33059c9 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -61,6 +61,7 @@ Ltac wsimpl :=
  unfold eq, zero, succ, pred, add, sub, mul; autorewrite with w.
 Ltac wcongruence := repeat red; intros; wsimpl; congruence.
 
+Instance znz_measure: Measure w_op.(znz_to_Z).
 Instance eq_equiv : Equivalence eq.
 
 Instance succ_wd : Proper (eq ==> eq) succ.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index d3f4776a6..410af329d 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -36,6 +36,7 @@ Hint Rewrite
 Ltac zsimpl := unfold Z.eq in *; autorewrite with zspec.
 Ltac zcongruence := repeat red; intros; zsimpl; congruence.
 
+Instance Z_measure: @Measure Z.t Z Z.to_Z.
 Instance eq_equiv : Equivalence Z.eq.
 
 Obligation Tactic := zcongruence.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 49e7d7256..aa291cfdc 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -34,6 +34,8 @@ Ltac ncongruence := unfold N.eq; repeat red; intros; nsimpl; congruence.
 
 Obligation Tactic := ncongruence.
 
+Instance: @Measure N.t Z N.to_Z.
+
 Instance eq_equiv : Equivalence N.eq.
 
 Program Instance succ_wd : Proper (N.eq==>N.eq) N.succ.
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index d0cf499ab..14646fa84 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -94,6 +94,7 @@ Local Open Scope bigQ_scope.
 
 (** [BigQ] is a setoid *)
 
+Instance bigQ_measure: RelationPairs.Measure BigQ.to_Q.
 Instance BigQeq_rel : Equivalence BigQ.eq.
 
 Instance BigQadd_wd : Proper (BigQ.eq==>BigQ.eq==>BigQ.eq) BigQ.add.