bteauto: a Proofview.tactic for multiple goals

Add an option to force backtracking at toplevel, which
is used by default when calling typeclasses eauto on a set of goals.
They might be depended on by other subgoals, so the tactic should
be backtracking by default, a once can make it not backtrack.

5 files changed, 120 insertions, 49 deletions

diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index 93fa3abd19..01af90e27d 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -66,8 +66,9 @@ VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
 END
 
 TACTIC EXTEND typeclasses_eauto
-| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ Proofview.V82.tactic (typeclasses_eauto l) ]
-| [ "typeclasses" "eauto" ] -> [ Proofview.V82.tactic (typeclasses_eauto ~only_classes:true [Hints.typeclasses_db]) ]
+| [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ typeclasses_eauto l ]
+| [ "typeclasses" "eauto" ] -> [
+    typeclasses_eauto ~only_classes:true [Hints.typeclasses_db] ]
 END
 
 TACTIC EXTEND head_of_constr
@@ -93,16 +94,16 @@ TACTIC EXTEND fulleauto
     let dbs = match dbnames with [] -> ["typeclass_instances"]
                                | l -> l in
     let dbs = List.map Hints.searchtable_map dbs in
-    Class_tactics.new_eauto_tac false ?limit:depth dbs 
+    Class_tactics.new_eauto_tac false ?limit:depth true dbs
   ]
 | ["fulleauto" depth(depth) ] -> [
     let dbs = ["typeclass_instances"] in
     let dbs = List.map Hints.searchtable_map dbs in
-    Class_tactics.new_eauto_tac false ?limit:depth dbs 
+    Class_tactics.new_eauto_tac false ?limit:depth true dbs
   ]
 | ["fulleauto" ] -> [
     let dbs = ["typeclass_instances"] in
     let dbs = List.map Hints.searchtable_map dbs in
-    Class_tactics.new_eauto_tac false dbs 
+    Class_tactics.new_eauto_tac false true dbs
   ]
 END
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 565d1c5794..61a8956e07 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -900,44 +900,28 @@ let rec eauto_tac' only_classes hints limit depth =
             Proofview.tclZERO ~info e))
                                                     
    
-let new_eauto_tac_gl ?st only_classes hints limit i sigma gls gl :
+let new_eauto_tac_gl ?st only_classes dep hints limit i sigma gls gl :
       unit Proofview.tactic =
   let open Proofview in
   let open Proofview.Notations in
-  let dep = Proofview.unifiable sigma (Goal.goal gl) gls in
+  let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
   let info = make_autogoal' ?st only_classes dep (cut_of_hints hints) i gl in
   eauto_tac' only_classes hints limit 1 info
 
 exception HasShelvedGoals
              
-let new_eauto_tac ?(st=full_transparent_state) only_classes hints limit : unit Proofview.tactic =
+let new_eauto_tac ?(st=full_transparent_state) only_classes dep hints limit : unit Proofview.tactic =
   let open Proofview in
   let eautotac sigma gls i =
     Goal.nf_enter
-      { enter = fun gl -> new_eauto_tac_gl ~st only_classes
-                                        hints limit (succ i) sigma gls gl }
+      { enter = fun gl ->
+                new_eauto_tac_gl ~st only_classes dep hints limit (succ i) sigma gls gl }
   in
-  let rec finish =
-    function Fail (e,ie) -> tclZERO ~info:ie e
-           | Next ((shelf,()), cont) ->
-              Proofview.tclEVARMAP >>= fun sigma ->
-              (* if List.for_all (fun ev -> Evd.is_defined sigma ev) shelf then *)
-              (*   (if !typeclasses_debug > 0 then *)
-              (*      msg_debug (str"Proof found with solved shelved goals:" ++ *)
-              (*                   prlist_with_sep spc (pr_ev sigma) shelf); *)
-              shelve_goals shelf
-              (* else *)
-              (*   (if !typeclasses_debug > 0 then *)
-              (*       msg_debug (str"Proof found but with unsolved shelved goals:" ++ *)
-              (*                    prlist_with_sep spc (pr_ev sigma) *)
-              (*                    (List.filter (Evd.is_undefined sigma) shelf) ++ *)
-              (*                str", trying another proof"); *)
-              (*    tclCASE (cont (HasShelvedGoals, Exninfo.null)) >>= finish) *)
-  in Proofview.Unsafe.tclGETGOALS >>= fun gls ->
+  Proofview.Unsafe.tclGETGOALS >>= fun gls ->
      Proofview.tclEVARMAP >>= fun sigma ->
      let j = List.length gls in
-     tclCASE (with_shelf (tclDISPATCH
-                            (List.init j (fun i -> eautotac sigma gls i)))) >>= finish
+     (tclDISPATCH
+        (List.init j (fun i -> eautotac sigma gls i)))
        
 let fix_iterative t =
   let rec aux depth =
@@ -956,17 +940,17 @@ let fix_iterative_limit limit t =
                
   in aux 1
 
-let new_eauto_tac ?(st=full_transparent_state) only_classes ?limit hints =
+let new_eauto_tac ?(st=full_transparent_state) only_classes ?limit dep hints =
   let tac =
     if get_typeclasses_iterative_deepening () then
       match limit with
       | None ->
-         fix_iterative (new_eauto_tac ~st only_classes hints)
+         fix_iterative (new_eauto_tac ~st only_classes dep hints)
       | Some l ->
-         fix_iterative_limit l (new_eauto_tac ~st only_classes hints)
+         fix_iterative_limit l (new_eauto_tac ~st only_classes dep hints)
     else
       let limit = match limit with None -> -1 | Some d -> d in
-      new_eauto_tac ~st only_classes hints limit
+      new_eauto_tac ~st only_classes dep hints limit
   in
   let error (e, ie) =
     match e with
@@ -1012,7 +996,7 @@ let run_on_evars ?(unique=false) p evm tac =
     with Logic_monad.TacticFailure _ -> raise Not_found
 
 let real_new_eauto ?limit unique st hints p evd =
-  let eauto_tac = new_eauto_tac ~st true ?limit hints in
+  let eauto_tac = new_eauto_tac ~st true ?limit false hints in
   let res = run_on_evars ~unique p evd eauto_tac in
     match res with
     | None -> evd
@@ -1244,7 +1228,7 @@ let resolve_all_evars_once debug limit unique p evd =
   let db = searchtable_map typeclasses_db in
     real_eauto ?limit unique (Hint_db.transparent_state db) [db] p evd
 
-let eauto ?(only_classes=true) ?st ?limit hints g =
+let eauto85 ?(only_classes=true) ?st ?limit hints g =
   let gl = { it = make_autogoal ~only_classes ?st
                     (cut_of_hints hints) None g; sigma = project g; } in
     match run_tac (eauto_tac ?limit hints) gl with
@@ -1278,7 +1262,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
     Goal.V82.mk_goal sigma nc gl Store.empty in
   let gls = { it = gl ; sigma = sigma; } in
   let hints = searchtable_map typeclasses_db in
-  let gls' = eauto ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in
+  let gls' = eauto85 ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in
   let evd = sig_sig gls' in
   let t' = let (ev, inst) = destEvar t in
     mkEvar (ev, Array.of_list subst)
@@ -1426,16 +1410,22 @@ let solve_inst env evd filter unique split fail =
 let _ =
   Typeclasses.solve_instantiations_problem := solve_inst
 
-let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs gl =
-  try
-    let dbs = List.map_filter
-      (fun db -> try Some (searchtable_map db)
-        with e when Errors.noncritical e -> None)
-      dbs
-    in
-    let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
-      eauto ?limit:!typeclasses_depth ~only_classes ~st dbs gl
-   with Not_found -> tclFAIL 0 (str" typeclasses eauto failed on: " ++ Printer.pr_goal gl) gl
+let eauto ?limit ~only_classes ~st dbs =
+  new_eauto_tac ~st only_classes ?limit dbs
+
+let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) dbs =
+  let dbs = List.map_filter
+              (fun db -> try Some (searchtable_map db)
+                      with e when Errors.noncritical e -> None)
+              dbs
+  in
+  let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
+  if get_typeclasses_compat () = Flags.V8_5 then
+    Tacticals.New.tclORELSE (Proofview.V82.tactic (eauto85 ?limit:!typeclasses_depth ~only_classes ~st dbs))
+     (Proofview.Goal.nf_enter ({ enter = fun gl ->
+       Tacticals.New.tclFAIL 0 (str" typeclasses eauto failed on: " ++
+                    Goal.pr_goal (Proofview.Goal.goal gl))}))
+  else eauto ?limit:!typeclasses_depth ~only_classes ~st true dbs
 
 (** Take the head of the arity of a constr.
     Used in the partial application tactic. *)
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index e9d915de1b..48abba1aaa 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -23,7 +23,7 @@ val get_typeclasses_depth : unit -> int option
 val progress_evars : unit Proofview.tactic -> unit Proofview.tactic
 
 val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state ->
-  Hints.hint_db_name list -> tactic
+  Hints.hint_db_name list -> unit Proofview.tactic
 
 val head_of_constr : Id.t -> Term.constr -> unit Proofview.tactic
 
@@ -49,6 +49,8 @@ val make_autogoal' : ?st:Names.transparent_state ->
            Hints.hints_path -> int -> ([ `NF ], 'c) Proofview.Goal.t -> newautoinfo
 
 val new_eauto_tac : ?st:Names.transparent_state ->
-           bool -> ?limit:Int.t -> 
-           Hints.hint_db list -> unit Proofview.tactic
+  bool -> ?limit:Int.t ->
+  bool -> (* Should the tactic be made backtracking, whatever the dependencies
+            betwwen initial goals are *)
+  Hints.hint_db list -> unit Proofview.tactic
 
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index f25e18acd6..8d6cbfcdeb 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,41 @@
+Module bt.
+Require Import Equivalence.
+
+Record Equ (A : Type) (R : A -> A -> Prop).
+Definition equiv {A} R (e : Equ A R) := R.
+Record Refl (A : Type) (R : A -> A -> Prop).
+Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e).
+Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [|shelve|] : foo.
+
+Variable R : nat -> nat -> Prop.
+Lemma bas : Equ nat R.
+Admitted.
+Hint Resolve bas : foo.
+Hint Extern 1 => match goal with |- (_ -> _ -> Prop) => shelve end : foo.
+
+Goal exists R, @Refl nat R.
+  eexists.
+  Set Typeclasses Debug.
+  (* Fail solve [unshelve eauto with foo]. *)
+  Set Typeclasses Debug Verbosity 1.
+  solve [typeclasses eauto with foo].
+Qed.
+
+(* Set Typeclasses Compatibility "8.5". *)
+Parameter f : nat -> Prop.
+Parameter g : nat -> nat -> Prop.
+Parameter h : nat -> nat -> nat -> Prop.
+Axiom a : forall x y, g x y -> f x -> f y.
+Axiom b : forall x (y : Empty_set), g (fst (x,y)) x.
+Axiom c : forall x y z, h x y z -> f x -> f y.
+Hint Resolve a b c : mybase.
+Goal forall x y z, h x y z -> f x -> f y.
+  intros.
+  Set Typeclasses Debug.
+  typeclasses eauto with mybase.
+  Unshelve.
+Abort.
+End bt.
 Generalizable All Variables.
 
 Module mon.
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
new file mode 100644
index 0000000000..f55e320326
--- /dev/null
+++ b/test-suite/success/bteauto.v
@@ -0,0 +1,40 @@
+
+Class A := { foo : nat }.
+
+Instance A_1 : A | 2 := { foo := 42 }.
+Instance A_0 : A | 1 := { foo := 0 }.
+Lemma aeq (a : A) : foo = foo.
+  reflexivity.
+Qed.
+
+Goal exists n, n = 42.
+  eexists.
+  eapply eq_trans.
+  evar (a : A). subst a.
+  refine (@aeq ?a).
+  Unshelve. all:cycle 1.
+  typeclasses eauto.
+  Fail reflexivity.
+  Undo 2.
+  Set Typeclasses Debug.
+  (* Without multiple successes it fails *)
+  Fail all:((once typeclasses eauto) + reflexivity).
+  (* Does backtrack if other goals fail *)
+  all:((typeclasses eauto) + reflexivity).
+Qed.
+
+Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.
+
+Goal exists n, n = 42.
+  eexists.
+  eapply eq_trans.
+  evar (a : A). subst a.
+  refine (@aeq ?a).
+  Unshelve. all:cycle 1.
+  typeclasses eauto.
+  Fail reflexivity.
+  Undo 2.
+  Set Typeclasses Debug.
+  (* Does backtrack between individual goals *)
+  all:(typeclasses eauto).
+Qed.