package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module NotationSource

Notations

Sourceval notation_cat : Libobject.category
Sourceval pr_notation : Constrexpr.notation -> Pp.t

Printing

module NotationMap : CMap.ExtS with type key = Constrexpr.notation and module Set := NotationSet
Scopes

A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters

Sourcetype delimiters = string
Sourcetype scope
Sourcetype scopes

= scope_name list

Sourceval declare_scope : Notation_term.scope_name -> unit
Sourceval ensure_scope : Notation_term.scope_name -> unit
Sourceval current_scopes : unit -> scopes
Sourceval scope_is_open_in_scopes : Notation_term.scope_name -> scopes -> bool

Check where a scope is opened or not in a scope list, or in * the current opened scopes

Sourceval scope_is_open : Notation_term.scope_name -> bool
Sourceval open_scope : Notation_term.scope_name -> unit

Open scope

Sourceval close_scope : Notation_term.scope_name -> unit
Sourceval normalize_scope : string -> Notation_term.scope_name

Return a scope taking either a scope name or delimiter

Sourceval empty_scope_stack : scopes

Extend a list of scopes

Sourceval scope_delimiters : scope -> delimiters option

Declare delimiters for printing

Sourceval declare_delimiters : Notation_term.scope_name -> delimiters -> unit
Sourceval remove_delimiters : Notation_term.scope_name -> unit
Sourceval find_delimiters_scope : ?loc:Loc.t -> delimiters -> Notation_term.scope_name
Declare and uses back and forth an interpretation of primitive token

A number interpreter is the pair of an interpreter for **(hexa)decimal** numbers in terms and an optional interpreter in pattern, if non integer or negative numbers are not supported, the interpreter must fail with an appropriate error message

Sourcetype notation_location = (Names.DirPath.t * Names.DirPath.t) * string

1st dirpath: dirpath of the library 2nd dirpath: module and section-only dirpath (ie Lib.current_dirpath true) string: string used to generate the notation

dirpaths are used for dumpglob and for Locate, string for printing (pr_notation_info)

Sourcetype required_module = Libnames.full_path * string list
Sourcetype prim_token_infos = {
  1. pt_local : bool;
    (*

    Is this interpretation local?

    *)
  2. pt_scope : Notation_term.scope_name;
    (*

    Concerned scope

    *)
  3. pt_interp_info : PrimNotations.prim_token_interp_info;
    (*

    Unique id "pointing" to (un)interp functions, OR a number notation object describing (un)interp functions

    *)
  4. pt_required : required_module;
    (*

    Module that should be loaded first

    *)
  5. pt_refs : Names.GlobRef.t list;
    (*

    Entry points during uninterpretation

    *)
  6. pt_in_match : bool;
    (*

    Is this prim token legal in match patterns ?

    *)
}

Note: most of the time, the pt_refs field above will contain inductive constructors (e.g. O and S for nat). But it could also be injection functions such as IZR for reals.

Activate a prim token interpretation whose unique id and functions have already been registered.

Sourceval enable_prim_token_interpretation : prim_token_infos -> unit

Return the term/cases_pattern bound to a primitive token in a given scope context

Sourceval interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (Glob_term.glob_constr -> unit) -> Constrexpr.prim_token -> Notation_term.subscopes -> Glob_term.glob_constr * Notation_term.scope_name option

Return the primitive token associated to a term/cases_pattern; raise No_match if no such token

Sourceval uninterp_prim_token : print_float:bool -> 'a Glob_term.glob_constr_g -> Notation_term.subscopes -> Constrexpr.prim_token * delimiters option
Sourceval uninterp_prim_token_cases_pattern : print_float:bool -> 'a Glob_term.cases_pattern_g -> Notation_term.subscopes -> Names.Name.t * Constrexpr.prim_token * delimiters option
Sourceval availability_of_prim_token : Constrexpr.prim_token -> Notation_term.scope_name -> Notation_term.subscopes -> delimiters option option
Declare and interpret back and forth a notation
Sourceval warning_overridden_name : string
Sourcetype entry_coercion_kind =
  1. | IsEntryCoercion of Constrexpr.notation_entry_level * Constrexpr.notation_entry_relative_level
  2. | IsEntryGlobal of Globnames.CustomName.t * int
  3. | IsEntryIdent of Globnames.CustomName.t * int

Return the interpretation bound to a notation

Sourceval availability_of_notation : Constrexpr.specific_notation -> Notation_term.subscopes -> (Notation_term.scope_name option * delimiters option) option

Test if a notation is available in the scopes context scopes; if available, the result is not None; the first argument is itself not None if a delimiters is needed

Sourceval is_printing_inactive_rule : Notationextern.interp_rule -> Notation_term.interpretation -> bool
Sourcetype 'a notation_query_pattern_gen = {
  1. notation_entry_pattern : Constrexpr.notation_entry list;
  2. interp_rule_key_pattern : (Constrexpr.notation_key, 'a) Util.union option;
  3. use_pattern : Notationextern.notation_use;
  4. scope_pattern : Constrexpr.notation_with_optional_scope option;
  5. interpretation_pattern : Notation_term.interpretation option;
}
Sourceval toggle_notations : on:bool -> all:bool -> ?verbose:bool -> (Glob_term.glob_constr -> Pp.t) -> notation_query_pattern -> unit
Miscellaneous
Sourceval interpret_notation_string : string -> string

Take a notation string and turn it into a notation key. eg. "x + y" becomes "_ + _".

Sourcetype notation_as_reference_error =
  1. | AmbiguousNotationAsReference of Constrexpr.notation_key
  2. | NotationNotReference of Environ.env * Evd.evar_map * Constrexpr.notation_key * (Constrexpr.notation_key * Notation_term.notation_constr) list
Sourceexception NotationAsReferenceError of notation_as_reference_error
Sourceval interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (Names.GlobRef.t -> bool) -> Constrexpr.notation_key -> delimiters option -> Names.GlobRef.t

If head is true, also allows applied global references. Raise NotationAsReferenceError if not resolvable as a global reference

Same together with the full notation

Sourceval declare_arguments_scope : bool -> Names.GlobRef.t -> Notation_term.scope_name list list -> unit

Declares and looks for scopes associated to arguments of a global ref

Sourceval find_arguments_scope : Environ.env -> Names.GlobRef.t -> Notation_term.scope_name list list
Sourcetype scope_class
Sourceval scope_class_compare : scope_class -> scope_class -> int

Comparison of scope_class

Sourceval subst_scope_class : Environ.env -> Mod_subst.substitution -> scope_class -> scope_class option
Sourcetype add_scope_where =
  1. | AddScopeTop
  2. | AddScopeBottom
    (*

    add new scope at top or bottom of existing stack (default is reset)

    *)
Sourceval declare_scope_class : bool -> Notation_term.scope_name -> ?where:add_scope_where -> scope_class -> unit
Sourceval declare_ref_arguments_scope : Names.GlobRef.t -> unit
Sourceval compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> Notation_term.scope_name list list
Sourceval compute_glob_type_scope : 'a Glob_term.glob_constr_g -> Notation_term.scope_name list
Sourceval current_type_scope_names : unit -> Notation_term.scope_name list

Get the current scopes bound to Sortclass

Sourceval scope_class_of_class : Coercionops.cl_typ -> scope_class

Building notation key

Sourcetype symbol =
  1. | Terminal of string
  2. | NonTerminal of Names.Id.t
  3. | SProdList of Names.Id.t * symbol list
  4. | Break of int
Sourceval symbol_eq : symbol -> symbol -> bool

Make/decompose a notation of the form "_ U _"

Sourceval decompose_notation_key : Constrexpr.notation -> Constrexpr.notation_entry * symbol list
Sourcetype notation_symbols = {
  1. recvars : (Names.Id.t * Names.Id.t) list;
  2. mainvars : Names.Id.t list;
  3. symbols : symbol list;
}
Sourceval is_prim_token_constant_in_constr : (Constrexpr.notation_entry * symbol list) -> bool
Sourceval decompose_raw_notation : string -> notation_symbols

Decompose a notation of the form "a 'U' b" together with the lists of pairs of recursive variables and the list of all variables binding in the notation

Sourceval pr_scope_class : scope_class -> Pp.t

Prints scopes (expects a pure aconstr printer)

Sourceval pr_scopes : (Glob_term.glob_constr -> Pp.t) -> Pp.t
Sourceval pr_visibility : (Glob_term.glob_constr -> Pp.t) -> Notation_term.scope_name option -> Pp.t

Coercions between entries

For a rule of the form "Notation string := x (in some-entry, x at some-relative-entry)", tell if going from some-entry to some-relative-entry is coercing

Sourceval declare_entry_coercion : Constrexpr.specific_notation -> Constrexpr.notation_entry_level -> Constrexpr.notation_entry_relative_level -> unit

Add a coercion from some-entry to some-relative-entry

Sourcetype entry_coercion = (Constrexpr.notation_with_optional_scope * Constrexpr.notation) list
Sourceval availability_of_entry_coercion : ?non_included:bool -> Constrexpr.notation_entry_relative_level -> Constrexpr.notation_entry_level -> entry_coercion option

Return a coercion path from some-relative-entry to some-entry if there is one

Special properties of entries

Sourceval declare_custom_entry_has_global : Globnames.CustomName.t -> int -> unit
Sourceval declare_custom_entry_has_ident : Globnames.CustomName.t -> int -> unit
Sourceval entry_has_global : Constrexpr.notation_entry_relative_level -> bool
Sourceval entry_has_ident : Constrexpr.notation_entry_relative_level -> bool
Sourceval app_level : int
Sourceval may_capture_cont_after : Constrexpr.entry_level option -> Constrexpr.entry_relative_level -> bool
Declare and test the level of a (possibly uninterpreted) notation
Sourceval declare_notation_level : Constrexpr.notation -> Notationextern.level -> unit

raise Not_found if not declared

Rem: printing rules for primitive token are canonical

Sourceval with_notation_protection : ('a -> 'b) -> 'a -> 'b