Correctly do backtracking during type class resolution even if only new

existentials are generated (at last!). The code simply keeps failure
continuations and apply them if needed.
Fix bottomup and topdown rewrite strategies that looped.
Use auto introduction flag for typeclass instances as well.


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

4 files changed, 70 insertions, 40 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index a5adb9169..a45d9a3b2 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -46,8 +46,6 @@ let typeclasses_db = "typeclass_instances"
 let _ = Auto.auto_init := (fun () ->
   Auto.create_hint_db false typeclasses_db full_transparent_state true)
 
-let run_on_evars_forward = ref (fun _ _ _ _ -> assert false)
-
 exception Found of evar_map
 
 let is_dependent ev evm =
@@ -109,11 +107,23 @@ let auto_unif_flags = {
   use_evars_pattern_unification = true;
 }
 
-let tac_on_evars p tac gl =
-  let db = searchtable_map typeclasses_db in
-    match !run_on_evars_forward [db] (Hint_db.transparent_state db) p (project gl)  with
-    | None -> tclIDTAC gl
-    | Some evm' -> Refiner.tclEVARS evm' gl
+let rec eq_constr_mod_evars x y =
+  match kind_of_term x, kind_of_term y with
+  | Evar (e1, l1), Evar (e2, l2) when e1 <> e2 -> true
+  | _, _ -> compare_constr eq_constr_mod_evars x y
+
+let progress_evars t gl =
+  let concl = pf_concl gl in
+  let check gl' = 
+    let newconcl = pf_concl gl' in
+      if eq_constr_mod_evars concl newconcl 
+      then tclFAIL 0 (str"No progress made (modulo evars)") gl'
+      else tclIDTAC gl'
+  in tclTHEN t check gl
+
+TACTIC EXTEND progress_evars
+  [ "progress_evars" tactic(t) ] -> [ progress_evars (snd t) ]
+END
 
 let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
@@ -329,8 +339,11 @@ let then_tac (first : atac) (second : atac) : atac =
 let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option =
   t.skft (fun x _ -> Some x) (fun _ -> None) gl
 
-let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : auto_result option =
-  (then_list t (fun x _ -> Some x))
+
+type run_list_res = (auto_result * run_list_res fk) option
+
+let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res =
+  (then_list t (fun x fk -> Some (x, fk)))
     (gl, fun s pfs -> valid goals p (ref s) pfs)
     (fun _ -> None)
 
@@ -375,22 +388,24 @@ let make_autogoals ?(st=full_transparent_state) gs evm' =
     let (gl, auto) = make_autogoal ~st {it = snd g; sigma = evm'} in
       (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
 
+let get_result r = 
+  match r with
+  | None -> None
+  | Some ((gls, v), fk) ->
+      try ignore(v (sig_sig gls) []); assert(false)
+      with Found evm' -> Some (evm', fk)
+	
 let run_on_evars ?(st=full_transparent_state) p evm tac =
   match evars_to_goals p evm with
-  | None -> None
+  | None -> None (* This happens only because there's no evar having p *)
   | Some (goals, evm') ->
-      match run_list_tac tac p goals (make_autogoals ~st goals evm') with
-      | None -> raise Not_found
-      | Some (gls, v) ->
-	  try ignore(v (sig_sig gls) []); assert(false)
-	  with Found evm' ->
-	    Some (Evd.evars_reset_evd evm' evm)
-
+      let res = run_list_tac tac p goals (make_autogoals ~st goals evm') in
+	match get_result res with
+	| None -> raise Not_found
+	| Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk)
 
 let eauto_tac hints = fix (or_tac intro_tac (hints_tac hints))
 
-let () = run_on_evars_forward := (fun hints st p evd -> run_on_evars ~st p evd (eauto_tac hints))
-
 let eauto hints g =
   let gl = { it = make_autogoal ~st:(Hint_db.transparent_state (List.hd hints)) g; sigma = project g } in
     match run_tac (eauto_tac hints) gl with
@@ -399,11 +414,20 @@ let eauto hints g =
 	{it = List.map fst goals; sigma = s}, valid s
 
 let real_eauto st hints p evd =
-  let rec aux evd =
-    match run_on_evars ~st p evd (eauto_tac hints) with
-    | None -> evd
-    | Some evd' -> aux evd'
-  in aux evd
+  let rec aux evd fails =
+    let res, fails =
+      try run_on_evars ~st p evd (eauto_tac hints), fails
+      with Not_found ->
+	List.fold_right (fun fk (res, fails) ->
+	  match res with
+	  | Some r -> res, fk :: fails
+	  | None -> get_result (fk ()), fails)
+	  fails (None, [])
+    in
+      match res with
+      | None -> evd
+      | Some (evd', fk) -> aux evd' (fk :: fails)
+  in aux evd []
 
 let resolve_all_evars_once debug (mode, depth) p evd =
   let db = searchtable_map typeclasses_db in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 1c48988c7..0884b3462 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -460,7 +460,8 @@ let resolve_subrelation env sigma car rel rel' res =
 
 let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars =
   let evars, morph_instance, proj, sigargs, m', args, args' =
-    let first = try (array_find args' (fun i b -> b <> None)) with Not_found -> raise (Invalid_argument "resolve_morphism") in
+    let first = try (array_find args' (fun i b -> b <> None)) 
+      with Not_found -> raise (Invalid_argument "resolve_morphism") in
     let morphargs, morphobjs = array_chop first args in
     let morphargs', morphobjs' = array_chop first args' in
     let appm = mkApp(m, morphargs) in
@@ -741,10 +742,10 @@ module Strategies =
       seq s (any s)
 
     let bu (s : strategy) : strategy =
-      fix (fun s' -> seq (choice (all_subterms s') s) (try_ s'))
+      fix (fun s' -> seq (choice (progress (all_subterms s')) s) (try_ s'))
 
     let td (s : strategy) : strategy =
-      fix (fun s' -> seq (choice s (all_subterms s')) (try_ s'))
+      fix (fun s' -> seq (choice s (progress (all_subterms s'))) (try_ s'))
 
     let innermost (s : strategy) : strategy =
       fix (fun ins -> choice (one_subterm ins) s)
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 0222ad115..bc25fe488 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -358,12 +358,14 @@ Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relatio
 
 (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
+Set Automatic Introduction.
+
 Instance relation_equivalence_equivalence (A : Type) :
   Equivalence (@relation_equivalence A).
-Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
+Proof. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed.
 
-Instance relation_implication_preorder : PreOrder (@subrelation A).
-Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
+Instance relation_implication_preorder A : PreOrder (@subrelation A).
+Proof. exact (@predicate_implication_preorder (cons A (cons A nil))). Qed.
 
 (** *** Partial Order.
    A partial order is a preorder which is additionally antisymmetric.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 50bcf589b..5633b7273 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -141,12 +141,15 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
     | Explicit -> cl
   in
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
-  let k, ctx', imps, subst =
-    let c = Command.generalize_constr_expr tclass ctx in
-    let imps, c' = interp_type_evars evars env c in
-    let ctx, c = decompose_prod_assum c' in
-    let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
-      cl, ctx, imps, List.rev args
+  let k, ctx', len, imps, subst =
+    let (env', ctx), imps = interp_context_evars evars env ctx in
+    let c', imps' = interp_type_evars_impls ~evdref:evars env' tclass in
+    let len = List.length ctx in
+    let imps = imps @ Impargs.lift_implicits len imps' in
+    let ctx', c = decompose_prod_assum c' in
+    let ctx' = ctx' @ ctx in
+    let cl, args = Typeclasses.dest_class_app (push_rel_context ctx' env) c in
+      cl, ctx', len, imps, List.rev args
   in
   let id =
     match snd instid with
@@ -227,7 +230,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 	let term = Termops.it_mkLambda_or_LetIn app ctx' in
 	evars := Evarutil.nf_evar_defs !evars;
 	let term = Evarutil.nf_isevar !evars term in
-	let evm =  (undefined_evars !evars) in
+	let evm = undefined_evars !evars in
 	Evarutil.check_evars env Evd.empty !evars termtype;
 	  if Evd.is_empty evm then
 	    declare_instance_constant k pri global imps ?hook id term termtype
@@ -238,9 +241,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
 		Command.start_proof id kind termtype
 		  (fun _ -> function ConstRef cst -> instance_hook k pri global imps ?hook cst
 		    | _ -> assert false);
-		if props <> [] then
-		  Pfedit.by (* (Refiner.tclTHEN (Refiner.tclEVARS !evars) *)
-		    (!refine_ref (evm, term));
+		if props <> [] then Pfedit.by (!refine_ref (evm, term))
+		else if Flags.is_auto_intros () then
+		  Pfedit.by (Refiner.tclDO len Tactics.intro);
 		(match tac with Some tac -> Pfedit.by tac | None -> ())) ();
 	      Flags.if_verbose (msg $$ Printer.pr_open_subgoals) ();
 	      id