Search (rocq-runtime.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 ->
  Evd.evar_map ->
  Constr.constr ->
  unit

Generic filter functions

val blacklist_filter : filter_function

Check whether a reference is blacklisted.

val module_filter : 
  Libnames.full_path list Vernacexpr.search_restriction ->
  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 ->
  Libnames.full_path list Vernacexpr.search_restriction ->
  display_function ->
  unit

val search_pattern : 
  Environ.env ->
  Evd.evar_map ->
  Pattern.constr_pattern ->
  Libnames.full_path list Vernacexpr.search_restriction ->
  display_function ->
  unit

val search : 
  Environ.env ->
  Evd.evar_map ->
  (bool * glob_search_request) list ->
  Libnames.full_path list Vernacexpr.search_restriction ->
  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 Libnames.full_path
(*
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 -> Evd.evar_map -> 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.