Module Notation

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

Printing

module NotationSet : Stdlib.Set.S with type NotationSet.elt = Constrexpr.notation
module NotationMap : CMap.ExtS with type key = Constrexpr.notation and module Set := NotationSet
module SpecificNotationSet : Stdlib.Set.S with type SpecificNotationSet.elt = Constrexpr.specific_notation
module SpecificNotationMap : CMap.ExtS with type key = Constrexpr.specific_notation and module Set := SpecificNotationSet
Scopes
type delimiters = string
type scope
type scopes

= scope_name list

val declare_scope : Notation_term.scope_name -> unit
val ensure_scope : Notation_term.scope_name -> unit
val current_scopes : unit -> scopes
val 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

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

Open scope

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

Return a scope taking either a scope name or delimiter

val empty_scope_stack : scopes

Extend a list of scopes

val push_scope : Notation_term.scope_name -> scopes -> scopes
val find_scope : Notation_term.scope_name -> scope
val declare_delimiters : Notation_term.scope_name -> delimiters -> unit
val remove_delimiters : Notation_term.scope_name -> unit
val find_delimiters_scope : ?⁠loc:Loc.t -> delimiters -> Notation_term.scope_name
Declare and uses back and forth an interpretation of primitive token
type 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, string for printing (pr_notation_info)

type required_module = Libnames.full_path * string list
type rawnum = NumTok.Signed.t
type prim_token_uid = string
type 'a prim_token_interpreter = ?⁠loc:Loc.t -> 'a -> Glob_term.glob_constr
type 'a prim_token_uninterpreter = Glob_term.any_glob_constr -> 'a option
type 'a prim_token_interpretation = 'a prim_token_interpreter * 'a prim_token_uninterpreter
val register_rawnumeral_interpretation : ?⁠allow_overwrite:bool -> prim_token_uid -> rawnum prim_token_interpretation -> unit
val register_bignumeral_interpretation : ?⁠allow_overwrite:bool -> prim_token_uid -> Z.t prim_token_interpretation -> unit
val register_string_interpretation : ?⁠allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
type prim_token_notation_error =
| UnexpectedTerm of Constr.t
| UnexpectedNonOptionTerm of Constr.t
exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error
type numnot_option =
| Nop
| Warning of NumTok.UnsignedNat.t
| Abstract of NumTok.UnsignedNat.t
type int_ty = {
dec_uint : Names.inductive;
dec_int : Names.inductive;
hex_uint : Names.inductive;
hex_int : Names.inductive;
uint : Names.inductive;
int : Names.inductive;
}
type z_pos_ty = {
z_ty : Names.inductive;
pos_ty : Names.inductive;
}
type number_ty = {
int : int_ty;
decimal : Names.inductive;
hexadecimal : Names.inductive;
number : Names.inductive;
}
type pos_neg_int63_ty = {
pos_neg_int63_ty : Names.inductive;
}
type target_kind =
| Int of int_ty
| UInt of int_ty
| Z of z_pos_ty
| Int63 of pos_neg_int63_ty
| Float64
| Number of number_ty
type string_target_kind =
| ListByte
| Byte
type option_kind =
| Option
| Direct
type 'target conversion_kind = 'target * option_kind
type to_post_arg =
| ToPostCopy
| ToPostAs of int
| ToPostHole
| ToPostCheck of Constr.t

A postprocessing translation to_post can be done after execution of the to_ty interpreter. The reverse translation is performed before the of_ty uninterpreter.

to_post is an array of n lists l_i of tuples (f, t, args). When the head symbol of the translated term matches one of the f in the list l_0 it is replaced by t and its arguments are translated acording to args where ToPostCopy means that the argument is kept unchanged and ToPostAs k means that the argument is recursively translated according to l_k. ToPostHole introduces an additional implicit argument hole (in the reverse translation, the corresponding argument is removed). ToPostCheck r behaves as ToPostCopy except in the reverse translation which fails if the copied term is not r. When n is null, no translation is performed.

type ('target, 'warning) prim_token_notation_obj = {
to_kind : 'target conversion_kind;
to_ty : Names.GlobRef.t;
to_post : (Names.GlobRef.t * Names.GlobRef.t * to_post_arg list) list array;
of_kind : 'target conversion_kind;
of_ty : Names.GlobRef.t;
ty_name : Libnames.qualid;
warning : 'warning;
}
type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
type prim_token_interp_info =
| Uid of prim_token_uid
| NumberNotation of number_notation_obj
| StringNotation of string_notation_obj
type prim_token_infos = {
pt_local : bool;

Is this interpretation local?

pt_scope : Notation_term.scope_name;

Concerned scope

pt_interp_info : prim_token_interp_info;

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

pt_required : required_module;

Module that should be loaded first

pt_refs : Names.GlobRef.t list;

Entry points during uninterpretation

pt_in_match : bool;

Is this prim token legal in match patterns ?

}
val enable_prim_token_interpretation : prim_token_infos -> unit
val declare_numeral_interpreter : ?⁠local:bool -> Notation_term.scope_name -> required_module -> Z.t prim_token_interpreter -> (Glob_term.glob_constr list * Z.t prim_token_uninterpreter * bool) -> unit
val declare_string_interpreter : ?⁠local:bool -> Notation_term.scope_name -> required_module -> string prim_token_interpreter -> (Glob_term.glob_constr list * string prim_token_uninterpreter * bool) -> unit
val interp_prim_token : ?⁠loc:Loc.t -> Constrexpr.prim_token -> Notation_term.subscopes -> Glob_term.glob_constr * Notation_term.scope_name option
val 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
val uninterp_prim_token : 'a Glob_term.glob_constr_g -> Notation_term.subscopes -> Constrexpr.prim_token * delimiters option
val uninterp_prim_token_cases_pattern : 'a Glob_term.cases_pattern_g -> Notation_term.subscopes -> Names.Name.t * Constrexpr.prim_token * delimiters option
val 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
type entry_coercion_kind =
| IsEntryCoercion of Constrexpr.notation_entry_level * Constrexpr.notation_entry_relative_level
| IsEntryGlobal of string * int
| IsEntryIdent of string * int
val declare_notation : (Constrexpr.notation_with_optional_scope * Constrexpr.notation) -> Notation_term.interpretation -> notation_location -> use:Notationextern.notation_use -> entry_coercion_kind option -> Deprecation.t option -> unit
val interp_notation : ?⁠loc:Loc.t -> Constrexpr.notation -> Notation_term.subscopes -> Notation_term.interpretation * (notation_location * Notation_term.scope_name option)

Return the interpretation bound to a notation

val 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

val is_printing_inactive_rule : Notationextern.interp_rule -> Notation_term.interpretation -> bool
type 'a notation_query_pattern_gen = {
notation_entry_pattern : Constrexpr.notation_entry list;
interp_rule_key_pattern : (Constrexpr.notation_key, 'a) Util.union option;
use_pattern : Notationextern.notation_use;
scope_pattern : Constrexpr.notation_with_optional_scope option;
interpretation_pattern : Notation_term.interpretation option;
}
type notation_query_pattern = Libnames.qualid notation_query_pattern_gen
val toggle_notations : on:bool -> all:bool -> (Glob_term.glob_constr -> Pp.t) -> notation_query_pattern -> unit
Miscellaneous
val interpret_notation_string : string -> string

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

type notation_as_reference_error =
| AmbiguousNotationAsReference of Constrexpr.notation_key
| NotationNotReference of Environ.env * Evd.evar_map * Constrexpr.notation_key * (Constrexpr.notation_key * Notation_term.notation_constr) list
exception NotationAsReferenceError of notation_as_reference_error
val 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

val 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

val find_arguments_scope : Names.GlobRef.t -> Notation_term.scope_name list list
type scope_class
val scope_class_compare : scope_class -> scope_class -> int

Comparison of scope_class

val subst_scope_class : Environ.env -> Mod_subst.substitution -> scope_class -> scope_class option
type add_scope_where =
| AddScopeTop
| AddScopeBottom

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

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

Get the current scopes bound to Sortclass

val scope_class_of_class : Coercionops.cl_typ -> scope_class
type symbol =
| Terminal of string
| NonTerminal of Names.Id.t
| SProdList of Names.Id.t * symbol list
| Break of int
val symbol_eq : symbol -> symbol -> bool
val make_notation_key : Constrexpr.notation_entry -> symbol list -> Constrexpr.notation

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

val decompose_notation_key : Constrexpr.notation -> Constrexpr.notation_entry * symbol list
type notation_symbols = {
recvars : (Names.Id.t * Names.Id.t) list;
mainvars : Names.Id.t list;
symbols : symbol list;
}
val is_prim_token_constant_in_constr : (Constrexpr.notation_entry * symbol list) -> bool
val 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

val pr_scope_class : scope_class -> Pp.t

Prints scopes (expects a pure aconstr printer)

val pr_scope : (Glob_term.glob_constr -> Pp.t) -> Notation_term.scope_name -> Pp.t
val pr_scopes : (Glob_term.glob_constr -> Pp.t) -> Pp.t
val locate_notation : (Glob_term.glob_constr -> Pp.t) -> Constrexpr.notation_key -> Notation_term.scope_name option -> Pp.t
val pr_visibility : (Glob_term.glob_constr -> Pp.t) -> Notation_term.scope_name option -> Pp.t
val is_coercion : Constrexpr.notation_entry_level -> Constrexpr.notation_entry_relative_level -> bool

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

val 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

type entry_coercion = (Constrexpr.notation_with_optional_scope * Constrexpr.notation) list
val availability_of_entry_coercion : ?⁠non_empty: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

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

raise Not_found if not declared

val with_notation_protection : ('a -> 'b) -> 'a -> 'b
val int63_of_pos_bigint : Z.t -> Uint63.t

Conversion from bigint to int63