Search (coq-core.Search)

Search facilities.

type glob_search_item =

| GlobSearchSubPattern of Vernacexpr.glob_search_where
  * bool
  * Pattern.constr_pattern

| GlobSearchString of string

| GlobSearchKind of Decls.logical_kind

| GlobSearchFilter of Names.GlobRef.t -> bool

type glob_search_request =

| GlobSearchLiteral of glob_search_item

| GlobSearchDisjConj of (bool * glob_search_request) list list

type filter_function =
  Names.GlobRef.t ->
  Decls.logical_kind option ->
  Environ.env ->
  Evd.evar_map ->
  Constr.constr ->
  bool

type display_function =
  Names.GlobRef.t ->
  Decls.logical_kind option ->
  Environ.env ->
  Constr.constr ->
  unit

Generic filter functions

val blacklist_filter : filter_function

Check whether a reference is blacklisted.

val module_filter : (Names.DirPath.t list * bool) -> filter_function

Check whether a reference pertains or not to a set of modules

val search_filter : glob_search_item -> filter_function

Specialized search functions

search_xxx gl pattern modinout searches the hypothesis of the glth goal and the global environment for things matching pattern and satisfying module exclude/include clauses of modinout.

val search_rewrite : 
  Environ.env ->
  Evd.evar_map ->
  Pattern.constr_pattern ->
  (Names.DirPath.t list * bool) ->
  display_function ->
  unit

val search_pattern : 
  Environ.env ->
  Evd.evar_map ->
  Pattern.constr_pattern ->
  (Names.DirPath.t list * bool) ->
  display_function ->
  unit

val search : 
  Environ.env ->
  Evd.evar_map ->
  (bool * glob_search_request) list ->
  (Names.DirPath.t list * bool) ->
  display_function ->
  unit

type search_constraint =

`\| Name_Pattern of Str.regexp`	(* Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
`\| Type_Pattern of Pattern.constr_pattern`	(* Whether the object type satisfies a pattern *)
`\| SubType_Pattern of Pattern.constr_pattern`	(* Whether some subtype of object type satisfies a pattern *)
`\| In_Module of Names.DirPath.t`	(* Whether the object pertains to a module *)
`\| Include_Blacklist`	(* Bypass the Search blacklist *)

type 'a coq_object = {

coq_object_prefix : string list;

coq_object_qualid : string list;

coq_object_object : 'a;

}

val interface_search : 
  Environ.env ->
  Evd.evar_map ->
  (search_constraint * bool) list ->
  Constr.constr coq_object list

Generic search function

val generic_search : Environ.env -> display_function -> unit

This function iterates over all hypothesis of the goal numbered glnum (if present) and all known declarations.

Search function modifiers

val prioritize_search : 
  ( display_function -> unit ) ->
  display_function ->
  unit

prioritize_search iter iterates over the values of iter (seen as a sequence of declarations), in a relevance order. This requires to perform the entire iteration of iter before starting streaming. So prioritize_search should not be used for low-latency streaming.