Show "autoapply" for tc eauto; include dbnames in tactic for info where

needed

doc/changelog/04-tactics/19823-tce_autoapply.rst

@@ -0,0 +1,7 @@
+- **Fixed:**
+  Debug output for :tacn:`typeclasses eauto` now shows :tacn:`autoapply` instead of :n:`simple *apply`.
+  The :tacn:`trivial` shown in :n:`*auto` debug output for :cmd:`Hint Immediate` hints
+  now includes the hint databases passed to :n:`*auto`
+  (`#19823 <https://github.com/coq/coq/pull/19823>`_,
+  fixes `#19799 <https://github.com/coq/coq/issues/19799>`_,
+  by Jim Fehrle).

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)
 

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

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
 

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 when dbname <> None ->
+    (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 ()
@@ -1864,7 +1881,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
@@ -1900,3 +1919,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

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

test-suite/output/HintLocality.out

@@ -40,15 +40,15 @@ Unfoldable constant definitions: all
 Unfoldable projection definitions: all
 Cut: emp
 For any goal ->   
-For nat ->   simple apply 0 ; trivial (cost 1, pattern nat, id 0)
+For nat ->   simple apply 0; trivial (cost 1, pattern nat, id 0)
 
 Non-discriminated database
 Unfoldable variable definitions: all
 Unfoldable constant definitions: all
 Unfoldable projection definitions: all
 Cut: emp
 For any goal ->   
-For nat ->   simple apply 0 ; trivial (cost 1, pattern nat, id 0)
+For nat ->   simple apply 0; trivial (cost 1, pattern nat, id 0)
 
 Non-discriminated database
 Unfoldable variable definitions: all
@@ -65,7 +65,7 @@ Unfoldable constant definitions: all
 Unfoldable projection definitions: all
 Cut: emp
 For any goal ->   
-For nat ->   simple apply 0 ; trivial (cost 1, pattern nat, id 0)
+For nat ->   simple apply 0; trivial (cost 1, pattern nat, id 0)
 
 Non-discriminated database
 Unfoldable variable definitions: all
@@ -95,7 +95,7 @@ Unfoldable projection definitions: all
 Cut: _
 For any goal ->   
 For S (modes !) ->   
-For nat ->   simple apply 0 ; trivial (cost 1, pattern nat, id 0)
+For nat ->   simple apply 0; trivial (cost 1, pattern nat, id 0)
 
 File "./output/HintLocality.v", line 92, characters 0-39:
 Warning: This hint is not local but depends on a section variable. It will

test-suite/output/TypeclassDebug.out

@@ -1,17 +1,17 @@
 Debug: 1: looking for foo without backtracking
-Debug: 1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1: autoapply H with foo on foo, 1 subgoal(s)
 Debug: 1.1-1 : foo
 Debug: 1.1-1: looking for foo without backtracking
-Debug: 1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1: autoapply H with foo on foo, 1 subgoal(s)
 Debug: 1.1-1.1-1 : foo
 Debug: 1.1-1.1-1: looking for foo without backtracking
-Debug: 1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1: autoapply H with foo on foo, 1 subgoal(s)
 Debug: 1.1-1.1-1.1-1 : foo
 Debug: 1.1-1.1-1.1-1: looking for foo without backtracking
-Debug: 1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1.1: autoapply H with foo on foo, 1 subgoal(s)
 Debug: 1.1-1.1-1.1-1.1-1 : foo
 Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking
-Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1.1-1.1: autoapply H with foo on foo, 1 subgoal(s)
 Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo
 File "./output/TypeclassDebug.v", line 9, characters 5-33:
 The command has indeed failed with message:

test-suite/output/bug19799.out

@@ -0,0 +1,11 @@
+(* info auto: *)
+intro.
+intro.
+simple apply eq_sym; trivial with zarith (in core).
+(* info eauto: *)
+intro.
+intro.
+simple apply eq_sym; trivial with zarith.
+File "./output/bug19799.v", line 8, characters 2-52:
+The command has indeed failed with message:
+No applicable tactic.

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.