From 72a2f5354c062247b3f35cf2cd29856e96e45824 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 16 May 2017 16:26:43 +0200 Subject: Fix bug #5360: anomalies in typeclass resolution output Now we properly report NoApplicableEx/ReachedLimit and CannotUnify exceptions that can be raised during resolution. --- tactics/auto.ml | 2 +- tactics/class_tactics.ml | 48 ++++++++++++++++++++++++++++++++---------------- 2 files changed, 33 insertions(+), 17 deletions(-) diff --git a/tactics/auto.ml b/tactics/auto.ml index c2d12ebd0..2f55d8e65 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -139,7 +139,7 @@ let conclPattern concl pat tac = try Proofview.tclUNIT (Constr_matching.matches env sigma pat concl) with Constr_matching.PatternMatchingFailure -> - Tacticals.New.tclZEROMSG (str "conclPattern") + Tacticals.New.tclZEROMSG (str "pattern-matching failed") in Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2d6dffdd2..d82d137f3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -236,16 +236,22 @@ let e_give_exact flags poly (c,clenv) = Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma) end } +let clenv_unique_resolver_tac with_evars ~flags clenv' = + Proofview.Goal.enter { enter = begin fun gls -> + let resolve = + try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls) + with e -> Proofview.tclZERO e + in resolve >>= fun clenv' -> + Clenvtac.clenv_refine with_evars ~with_classes:false clenv' + end } + let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) -> let clenv', c = connect_hint_clenv poly c clenv gls in - let clenv' = clenv_unique_resolver ~flags clenv' gls in - Clenvtac.clenv_refine true ~with_classes:false clenv' - end } + clenv_unique_resolver_tac true ~flags clenv' end } let unify_resolve poly flags = { enter = begin fun gls (c,_,clenv) -> let clenv', _ = connect_hint_clenv poly c clenv gls in - let clenv' = clenv_unique_resolver ~flags clenv' gls in - Clenvtac.clenv_refine false ~with_classes:false clenv' + clenv_unique_resolver_tac false ~flags clenv' end } (** Application of a lemma using [refine] instead of the old [w_unify] *) @@ -701,7 +707,7 @@ module V85 = struct let merge_failures x y = match x, y with | _, ReachedLimit - | ReachedLimit, _ -> ReachedLimit + | ReachedLimit, _ -> ReachedLimit | NotApplicable, NotApplicable -> NotApplicable let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = @@ -1014,9 +1020,9 @@ module Search = struct (** In the proof engine failures are represented as exceptions *) exception ReachedLimitEx - exception NotApplicableEx + exception NoApplicableEx - (** ReachedLimitEx has priority over NotApplicableEx to handle + (** ReachedLimitEx has priority over NoApplicableEx to handle iterative deepening: it should fail when no hints are applicable, but go to a deeper depth otherwise. *) let merge_exceptions e e' = @@ -1052,7 +1058,7 @@ module Search = struct Feedback.msg_debug (pr_depth info.search_depth ++ str": failure due to non-class subgoal " ++ pr_ev sigma (Proofview.Goal.goal gl)); - Proofview.tclZERO NotApplicableEx) } + Proofview.tclZERO NoApplicableEx) } (** The general hint application tactic. tac1 + tac2 .... The choice of OR or ORELSE is determined @@ -1088,14 +1094,24 @@ module Search = struct let derivs = path_derivate info.search_cut name in let pr_error ie = if !typeclasses_debug > 1 then - let msg = - pr_depth (!idx :: info.search_depth) ++ str": " ++ + let idx = if fst ie == NoApplicableEx then pred !idx else !idx in + let header = + pr_depth (idx :: info.search_depth) ++ str": " ++ Lazy.force pp ++ (if !foundone != true then str" on" ++ spc () ++ pr_ev s (Proofview.Goal.goal (Proofview.Goal.assume gl)) else mt ()) in - Feedback.msg_debug (msg ++ str " failed with " ++ CErrors.iprint ie) + let msg = + match fst ie with + | Pretype_errors.PretypeError (env, evd, Pretype_errors.CannotUnify (x,y,_)) -> + str"Cannot unify " ++ print_constr_env env evd x ++ str" and " ++ + print_constr_env env evd y + | ReachedLimitEx -> str "Proof-search reached its limit." + | NoApplicableEx -> str "Proof-search failed." + | e -> CErrors.iprint ie + in + Feedback.msg_debug (header ++ str " failed with: " ++ msg) else () in let tac_of gls i j = Goal.enter { enter = fun gl' -> @@ -1206,10 +1222,10 @@ module Search = struct str" possibilities"); match e with | (ReachedLimitEx,ie) -> Proofview.tclZERO ~info:ie ReachedLimitEx - | (_,ie) -> Proofview.tclZERO ~info:ie NotApplicableEx + | (_,ie) -> Proofview.tclZERO ~info:ie NoApplicableEx in - if backtrack then aux (NotApplicableEx,Exninfo.null) poss - else tclONCE (aux (NotApplicableEx,Exninfo.null) poss) + if backtrack then aux (NoApplicableEx,Exninfo.null) poss + else tclONCE (aux (NoApplicableEx,Exninfo.null) poss) let hints_tac hints info kont : unit Proofview.tactic = Proofview.Goal.enter @@ -1313,7 +1329,7 @@ module Search = struct match e with | ReachedLimitEx -> Tacticals.New.tclFAIL 0 (str"Proof search reached its limit") - | NotApplicableEx -> + | NoApplicableEx -> Tacticals.New.tclFAIL 0 (str"Proof search failed" ++ (if Option.is_empty depth then mt() else str" without reaching its limit")) -- cgit v1.2.3