Notation
Notations
val notation_cat : Libobject.category
val pr_notation : Constrexpr.notation -> Pp.t
Printing
module NotationSet : CSet.ExtS with type elt = Constrexpr.notation
module NotationMap : CMap.ExtS with type key = Constrexpr.notation and module Set := NotationSet
module SpecificNotationSet : CSet.ExtS with type elt = Constrexpr.specific_notation
module SpecificNotationMap : CMap.ExtS with type key = Constrexpr.specific_notation and module Set := SpecificNotationSet
A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters
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 scope_delimiters : scope -> delimiters option
Declare delimiters for printing
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
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
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
The unique id string below will be used to refer to a particular registered interpreter/uninterpreter of number or string notation. Using the same uid for different (un)interpreters will fail. If at most one interpretation of prim token is used per scope, then the scope name could be used as unique id.
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
* Number notation
exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error
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 number_ty = {
int : int_ty; |
decimal : Names.inductive; |
hexadecimal : Names.inductive; |
number : 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 'target conversion_kind = 'target * option_kind
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 ? *) |
}
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.
val enable_prim_token_interpretation : prim_token_infos -> unit
Return the term
/cases_pattern
bound to a primitive token in a given scope context
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
Return the primitive token associated to a term
/cases_pattern
; raise No_match
if no such token
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
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 -> UserWarn.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 -> ?verbose:bool -> (Glob_term.glob_constr -> Pp.t) -> notation_query_pattern -> unit
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 interp_notation_as_global_reference_expanded : ?loc:Loc.t -> head:bool ->
(Names.GlobRef.t -> bool) -> Constrexpr.notation_key -> delimiters option -> (Constrexpr.notation_entry * Constrexpr.notation_key) * Constrexpr.notation_key * Constrexpr.notation_with_optional_scope * Notation_term.interpretation * Names.GlobRef.t
Same together with the full notation
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
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
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
Building notation key
type symbol =
| Terminal of string |
| NonTerminal of Names.Id.t |
| SProdList of Names.Id.t * symbol list |
| Break of int |
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
Coercions between entries
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_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
val entry_has_global : Constrexpr.notation_entry_relative_level -> bool
val entry_has_ident : Constrexpr.notation_entry_relative_level -> bool
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
val declare_notation_level : Constrexpr.notation -> Notationextern.level -> unit
val level_of_notation : Constrexpr.notation -> Notationextern.level
raise Not_found
if not declared
Rem: printing rules for primitive token are canonical
val int63_of_pos_bigint : Z.t -> Uint63.t
Conversion from bigint to int63