From a92bd71d50ba5d3069007432cdaa5b527379ff0f Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 9 Nov 2024 20:16:46 -0800 Subject: [PATCH] Show "autoapply" for tc eauto; include dbnames in tactic for info where needed --- tactics/auto.ml | 3 ++- tactics/class_tactics.ml | 4 +++- tactics/eauto.ml | 3 ++- tactics/hints.ml | 36 +++++++++++++++++++++++++++++++--- tactics/hints.mli | 6 +++++- test-suite/output/bug19799.out | 10 ++++++++++ test-suite/output/bug19799.v | 10 ++++++++++ 7 files changed, 65 insertions(+), 7 deletions(-) create mode 100644 test-suite/output/bug19799.out create mode 100644 test-suite/output/bug19799.v diff --git a/tactics/auto.ml b/tactics/auto.ml index aaa2e51670fc..a20d8cbb225d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -334,11 +334,12 @@ and tac_of_hint dbg db_list local_db concl = conclPattern concl p tacast in let pr_hint h env sigma = + let dbname, dblist = format_db_info false h db_list in let origin = match FullHint.database h with | None -> mt () | Some n -> str " (in " ++ str n ++ str ")" in - FullHint.print env sigma h ++ origin + FullHint.print env sigma ?dbname ~dblist h ++ origin in fun h -> tclLOG dbg (pr_hint h) (FullHint.run h tactic) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 2075240be9a7..2d1a1aa716e3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -301,7 +301,9 @@ and e_my_find_search db_list local_db secvars hdc complete env sigma concl0 = | Extern _ -> true | _ -> false in - (tac, FullHint.priority h, extern, name, lazy (FullHint.print env sigma h)) + let dbname, dblist = format_db_info true h db_list in + (tac, FullHint.priority h, extern, name, + lazy (FullHint.print env sigma ~tce:true ?dbname ~dblist h)) in let hint_of_db = hintmap_of env sigma hdc secvars concl in let hintl = List.map_filter (fun db -> match hint_of_db db with diff --git a/tactics/eauto.ml b/tactics/eauto.ml index c6c3c5667b8c..1f75bb7bd931 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -146,7 +146,8 @@ and e_my_find_search env sigma db_list local_db secvars concl = in let b = { cost_priority = priority; cost_subgoals = subgoals } in let tac = FullHint.run h tac in - (tac, b, lazy (FullHint.print env sigma h)) + let dbname, dblist = format_db_info false h db_list in + (tac, b, lazy (FullHint.print env sigma ?dbname ~dblist h)) in List.map tac_of_hint hintl diff --git a/tactics/hints.ml b/tactics/hints.ml index b0dcba74d17d..048dea0af689 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -625,6 +625,7 @@ val add_modes : hint_mode array list GlobRef.Map.t -> t -> t val modes : t -> hint_mode array list GlobRef.Map.t val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a +val name : t -> string option end = struct @@ -830,6 +831,7 @@ struct let modes db = GlobRef.Map.map (fun se -> se.sentry_mode) db.hintdb_map let use_dn db = db.use_dn + let name db = db.hintdb_name end @@ -1612,17 +1614,32 @@ let push_resolve_hyp env sigma decl db = let pr_hint_elt env sigma h = pr_econstr_env env sigma h.hint_term -let pr_hint env sigma h = match h.obj with +let with_db dbname = match dbname with | Some n -> str " with " ++ str n | None -> mt () +let with_dblist dblist = + if dblist = [] then mt () + else str " with" ++ (List.fold_left (fun acc db -> acc ++ str " " ++ str db) (mt ())) dblist + +let pr_hint env sigma ?dbname ?(dblist=[]) h = match h.obj with | Res_pf c -> (str"simple apply " ++ pr_hint_elt env sigma c) | ERes_pf c -> (str"simple eapply " ++ pr_hint_elt env sigma c) | Give_exact c -> (str"exact " ++ pr_hint_elt env sigma c) | Res_pf_THEN_trivial_fail c -> - (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial") + (str"simple apply " ++ pr_hint_elt env sigma c ++ str"; trivial" ++ with_dblist dblist) | Unfold_nth c -> str"unfold " ++ pr_evaluable_reference c | Extern (_, tac) -> str "(*external*) " ++ Pputils.pr_glb_generic env sigma tac +let pr_hint_tceauto env sigma ?dbname ?(dblist=[]) h = + match h.obj with + | Res_pf c + | ERes_pf c -> + (str"autoapply " ++ pr_hint_elt env sigma c ++ with_db dbname) + | Res_pf_THEN_trivial_fail c -> + (str"autoapply " ++ pr_hint_elt env sigma c ++ with_db dbname ++ + str"; trivial" ++ with_dblist dblist) + | _ -> pr_hint env sigma ?dbname ~dblist h + let pr_id_hint env sigma (id, v) = let pr_pat p = match p.pat with | None -> mt () @@ -1871,7 +1888,9 @@ struct | Some (ConstrPattern p | SyntacticPattern p) -> Some p | Some DefaultPattern -> None let run (h : t) k = run_hint h.code k - let print env sigma (h : t) = pr_hint env sigma h.code + let print env sigma ?(tce=false) ?dbname ?dblist (h : t) = + let pr = if tce then pr_hint_tceauto else pr_hint in + pr env sigma ?dbname ?dblist h.code let name (h : t) = h.name let subgoals (h : t) = match h.code.obj with @@ -1907,3 +1926,14 @@ let hint_res_pf ?with_evars ?with_classes ?flags h = let clenv = connect_hint_clenv h gl in Clenv.res_pf ?with_evars ?with_classes ?flags clenv end + +let format_db_info tceauto h db_list = + let n = FullHint.database h in + let dbname = if n = Some "core" && (not tceauto) then None else n in + let dblist = List.rev (List.fold_left (fun acc db -> + let n = Hint_db.name db in + match n with + | Some n when n <> "core" || tceauto -> n :: acc + | _ -> acc + ) [] db_list) in + dbname, dblist diff --git a/tactics/hints.mli b/tactics/hints.mli index 4db5bcd4e527..cff24dc5d66d 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -60,7 +60,8 @@ sig val database : t -> string option val run : t -> (hint hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic val name : t -> GlobRef.t option - val print : env -> evar_map -> t -> Pp.t + val print : env -> evar_map -> ?tce:bool -> ?dbname:string -> + ?dblist:string list -> t -> Pp.t val subgoals : t -> int option (** This function is for backward compatibility only, not to use in newly @@ -152,6 +153,7 @@ module Hint_db : val add_modes : hint_mode array list GlobRef.Map.t -> t -> t val modes : t -> hint_mode array list GlobRef.Map.t + val name : t -> string option end type hint_db = Hint_db.t @@ -242,3 +244,5 @@ val pr_applicable_hint : Proof.t -> Pp.t val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t + +val format_db_info : bool -> FullHint.t -> Hint_db.t list -> string option * string list diff --git a/test-suite/output/bug19799.out b/test-suite/output/bug19799.out new file mode 100644 index 000000000000..e4766a84d642 --- /dev/null +++ b/test-suite/output/bug19799.out @@ -0,0 +1,10 @@ +(* info auto: *) +intro. +intro. +simple apply eq_sym; trivial with zarith (in core). +(* info auto: *) +intro. +intro. +simple apply eq_sym; trivial with zarith (in core). +The command has indeed failed with message: +No applicable tactic. diff --git a/test-suite/output/bug19799.v b/test-suite/output/bug19799.v new file mode 100644 index 000000000000..85fb20ba0231 --- /dev/null +++ b/test-suite/output/bug19799.v @@ -0,0 +1,10 @@ +Require Import ZArith_base Zcomplements. Local Open Scope Z_scope. + +(* Set Typeclasses Debug Verbosity 1. *) +Goal forall A acc, Zlength_aux acc A nil = acc + Z.of_nat (@length A nil). +Proof. + Succeed (solve [info_auto with zarith]). + Succeed (solve [info_eauto with zarith]). + Fail (solve [typeclasses eauto with zarith core]). + (* no applicable tactic *) +Abort.