diff options
| -rw-r--r-- | doc/refman/Classes.tex | 13 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 47 | ||||
| -rw-r--r-- | test-suite/success/Typeclasses.v | 17 | ||||
| -rw-r--r-- | test-suite/success/bteauto.v | 10 | ||||
| -rw-r--r-- | test-suite/success/eauto.v | 1 |
5 files changed, 61 insertions, 27 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 254fca28f..d6a553e1a 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -394,7 +394,18 @@ than {\tt eauto} and {\tt auto}. The main differences are the following: {\tt typeclass\_instances} database by default (instead of {\tt core}) and will try to solve \emph{only} typeclass goals. Other subgoals are automatically shelved and \emph{must be} resolved entirely when the - other typeclass subgoals are resolved or the proof search will fail. + other typeclass subgoals are resolved or the proof search will fail + \emph{globally}, \emph{without} the possibility to find another + complete solution with no shelved subgoals. + + \emph{Note: } As of Coq 8.6, {\tt all:once (typeclasses eauto)} + faithfully mimicks what happens during typeclass resolution when it is + called during refinement/type-inference. It might move to {\tt + all:typeclasses eauto} in future versions when the refinement engine + will be able to backtrack. +\item When called with specific databases (e.g. {\tt with}), {\tt + typeclasses eauto} allows shelved goals to remain at any point + during search and treat typeclasses goals like any other. \item The transparency information of databases is used consistently for all hints declared in them. It is always used when calling the unifier. When considering the local hypotheses, we use the transparent diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 72e410160..91eb388b3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1265,21 +1265,29 @@ module Search = struct | (e,ie) -> Proofview.tclZERO ~info:ie e) in aux 1 - let disallow_shelved tac = + let disallow_shelved initshelf tac = let open Proofview in - with_shelf (tclONCE tac) >>= fun (shelved,result) -> - (if not (List.is_empty shelved) then - begin - Proofview.tclEVARMAP >>= fun sigma -> - let gls = prlist_with_sep spc (pr_ev sigma) shelved in - (if !typeclasses_debug > 0 then - Feedback.msg_debug (str"Non-empty shelf at end of resolution:" ++ gls)); - Tacticals.New.tclFAIL 1 (str"Proof search failed: " ++ - str"shelved goals remain: " ++ gls) - end - else tclUNIT result) - - let eauto_tac ?(st=full_transparent_state) ?(unique=false) ~only_classes ~depth ~dep hints = + let casefn = function + | Fail (e,info) -> tclZERO ~info e + | Next ((shelved, result), k) -> + if not (List.is_empty shelved) then + begin + Proofview.tclEVARMAP >>= fun sigma -> + let gls = prlist_with_sep spc (pr_ev sigma) shelved in + (if !typeclasses_debug > 0 then + let initgls = prlist_with_sep spc (pr_ev sigma) initshelf in + Feedback.msg_debug (str"Non-empty shelf at end of resolution:" ++ gls + ++ str" initially: " ++ initgls ++ str".")); + Tacticals.New.tclZEROMSG (str"Proof search failed: " ++ + str"shelved goals remain: " ++ gls) + end + else + tclOR (tclUNIT result) (fun e -> k e >>= fun (gls, result) -> tclUNIT result) + in + tclCASE (with_shelf tac) >>= casefn + + let eauto_tac ?(st=full_transparent_state) ?(unique=false) + ~only_classes ~depth ~dep hints = let open Proofview in let tac = let search = search_tac ~st only_classes dep hints in @@ -1310,7 +1318,16 @@ module Search = struct Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac else tac in - let tac = if only_classes then disallow_shelved tac else tac in + with_shelf numgoals >>= fun (initshelf, i) -> + (if !typeclasses_debug > 1 then + Feedback.msg_debug (str"Starting resolution with " ++ int i ++ + str" goal(s) under focus and " ++ + int (List.length initshelf) ++ str " shelved goal(s)" ++ + if only_classes then str " in only_classes mode" else + str " in regular mode" ++ + match depth with None -> str ", unbounded" + | Some i -> str ", with depth limit " ++ int i)); + let tac = if only_classes then disallow_shelved initshelf tac else tac in tac let run_on_evars p evm tac = diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 4581a7ce4..6885717ec 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -6,10 +6,10 @@ Module onlyclasses. Goal Foo * Foo. split. shelve. Set Typeclasses Debug. - typeclasses eauto. + Fail typeclasses eauto. typeclasses eauto with typeclass_instances. Unshelve. typeclasses eauto with typeclass_instances. - Abort. + Qed. End onlyclasses. Module shelve_non_class_subgoals. @@ -22,22 +22,23 @@ Module shelve_non_class_subgoals. Typeclasses eauto := debug. Set Typeclasses Debug Verbosity 2. Goal Bar. - (* Solution has shelved subgoals *) + (* Solution has shelved subgoals (of non typeclass type) *) Fail typeclasses eauto. Abort. End shelve_non_class_subgoals. -Module shelve_non_class_subgoals2. +Module Leivantex2PR339. + (** Was a bug preventing to find hints associated with no pattern *) Class Bar := {}. - Instance bar1 (t:Type) : Bar. Hint Extern 0 => exact True : typeclass_instances. Typeclasses eauto := debug. Goal Bar. Fail typeclasses eauto. - debug eauto with typeclass_instances. - Qed. -End shelve_non_class_subgoals2. + Set Typeclasses Debug Verbosity 2. + typeclasses eauto with typeclass_instances. + Qed. +End Leivantex2PR339. Module bt. Require Import Equivalence. diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v index bb1cf0654..f97f764b4 100644 --- a/test-suite/success/bteauto.v +++ b/test-suite/success/bteauto.v @@ -8,7 +8,7 @@ Module Backtracking. Qed. Arguments foo A : clear implicits. - + Require Import Program.Tactics. Example find42 : exists n, n = 42. Proof. eexists. @@ -20,9 +20,13 @@ Module Backtracking. Fail reflexivity. Undo 2. (* Without multiple successes it fails *) - Fail all:((once typeclasses eauto) + apply eq_refl). + Set Typeclasses Debug Verbosity 2. + Fail all:((once (typeclasses eauto with typeclass_instances)) + + apply eq_refl). (* Does backtrack if other goals fail *) - all:((typeclasses eauto) + reflexivity). + all:[> typeclasses eauto + reflexivity .. ]. + Undo 1. + all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *) Show Proof. Qed. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 9bcecfe1f..160f2d9de 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -176,6 +176,7 @@ Definition trivial a (H : Foo a) : {b : myType & Qux b}. Proof. Time typeclasses eauto 10 with typeclass_instances. Undo. Set Typeclasses Iterative Deepening. + (* Much faster in iteratove deepening mode *) Time typeclasses eauto with typeclass_instances. Defined. |