Coq: SSReflect's Search tool does not take Search Blacklist table into account

[anton-trunov]

Version

Coq 8.8.1

Operating system

macOS 10.13.6

Description of the problem

Please see the comments in the snippet below:

Print Table Search Blacklist.
(* Current search blacklist :  _subterm _subproof Private_. *)

Axiom T : Type.
Axiom Private_t : T.
Axiom NonPriv_t : T.

(** the standard search tool respects the blacklist *)
Search T.
(* NonPriv_t: T *)

(** but ssr does not *)
From Coq Require Import ssreflect.
Search _ T.
(*
NonPriv_t  T
Private_t  T
*)

[Zimmi48]

Probably the best fix here is to remove the Search tool of SSReflect and merge whatever special features are useful in the main one.

[tchajed]

From the SSReflect documentation the features missing from the built-in Search are:

1. A special conclusion-only first pattern. This isn't the same as SearchHead (which only matches the head of the conclusion) and is anyway more powerful because it can be combined with other patterns that match anywhere. Note that this only provides more precise filtering.
2. When searching for a notation, SSReflect reports the notation and its expansion in addition to including it in searches.
3. Diagnostics around multiple matching notations, when a partial notation is given. Coq Search doesn't support partial notations.
4. Issues a warning if a notation has another interpretation in a different scope.

Of these, to me (2) is the most useful to port while the others aren't really necessary. (3) and (4) are better handled by Locate in any case (eg, neither the built-in nor ssreflect Search handle the exists2 notation for ex2 correctly). (1) is kind of nice, but the way SSReflect handles it (the first pattern is special) is confusing UI and I don't think it's a necessary improvement over SearchHead. I've never felt I needed better filtering tools for Search.

[herbelin]

Adding 2. to vanilla Coq would be easy and I can do it if noone objects.

About 1., there are various syntax we could think of. For instance, we could allow ccl:term_pattern to mean that the pattern (or notation string) is to be searched only in the conclusion. We could even generalize this to search in hypotheses only, say with hyp:term_pattern.

We could imagine various modifiers actually, like rhs: and lhs: to mean to restrict the search on the right-hand side of an equality (or even of a binary relation for some definition of binary relation). Or combinations such as rhs:ccl:term_pattern. Or head: to mean the head symbol as in SearchHead. The space design is large...

[Zimmi48]

Maybe no need to overthink this if actual use cases are already covered by SearchHead. It would be interesting to have more feedback from users.