Module `Notation`Source

Notations

Sourceval notation_cat : Libobject.category

Sourceval pr_notation : Constrexpr.notation -> Pp.t

Printing

val notation_entry_eq : 
  Constrexpr.notation_entry ->
  Constrexpr.notation_entry ->
  bool

Equality on notation_entry.

Source

val notation_entry_level_eq : 
  Constrexpr.notation_entry_level ->
  Constrexpr.notation_entry_level ->
  bool

Equality on notation_entry_level.

Source

val notation_with_optional_scope_eq : 
  Constrexpr.notation_with_optional_scope ->
  Constrexpr.notation_with_optional_scope ->
  bool

Sourceval notation_eq : Constrexpr.notation -> Constrexpr.notation -> bool

Equality on notation.

Sourcemodule NotationSet : Set.S with type elt = Constrexpr.notation

Source

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

Sourcemodule SpecificNotationSet : Set.S with type elt = Constrexpr.specific_notation

Source

module SpecificNotationMap : 
  CMap.ExtS
    with type key = Constrexpr.specific_notation
     and module Set := SpecificNotationSet

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

Open scope

Sourceval open_close_scope : (bool * bool * Notation_term.scope_name) -> unit

Sourceval empty_scope_stack : scopes

Extend a list of scopes

Sourceval push_scope : Notation_term.scope_name -> scopes -> scopes

Sourceval find_scope : Notation_term.scope_name -> scope

Declare delimiters for printing

Sourceval declare_delimiters : Notation_term.scope_name -> delimiters -> unit

Sourceval remove_delimiters : Notation_term.scope_name -> unit

Source

val 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

Sourcetype required_module = Libnames.full_path * string list

Sourcetype 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.

Sourcetype prim_token_uid = string

Sourcetype 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> Glob_term.glob_constr

Sourcetype 'a prim_token_uninterpreter = Glob_term.any_glob_constr -> 'a option

Source

type 'a prim_token_interpretation =
  'a prim_token_interpreter * 'a prim_token_uninterpreter

Source

val register_rawnumeral_interpretation : 
  ?allow_overwrite:bool ->
  prim_token_uid ->
  rawnum prim_token_interpretation ->
  unit

Source

val register_bignumeral_interpretation : 
  ?allow_overwrite:bool ->
  prim_token_uid ->
  Z.t prim_token_interpretation ->
  unit

Source

val register_string_interpretation : 
  ?allow_overwrite:bool ->
  prim_token_uid ->
  string prim_token_interpretation ->
  unit

* Number notation

Sourcetype prim_token_notation_error =

| UnexpectedTerm of Constr.t
| UnexpectedNonOptionTerm of Constr.t

Source

exception PrimTokenNotationError of string
  * Environ.env
  * Evd.evar_map
  * prim_token_notation_error

Sourcetype numnot_option =

| Nop
| Warning of NumTok.UnsignedNat.t
| Abstract of NumTok.UnsignedNat.t

Sourcetype int_ty = {

dec_uint : Names.inductive;
dec_int : Names.inductive;
hex_uint : Names.inductive;
hex_int : Names.inductive;
uint : Names.inductive;
int : Names.inductive;

}

Sourcetype z_pos_ty = {

z_ty : Names.inductive;
pos_ty : Names.inductive;

}

Sourcetype number_ty = {

int : int_ty;
decimal : Names.inductive;
hexadecimal : Names.inductive;
number : Names.inductive;

}

Sourcetype pos_neg_int63_ty = {

pos_neg_int63_ty : Names.inductive;

}

Sourcetype 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

Sourcetype string_target_kind =

| ListByte
| Byte

Sourcetype option_kind =

| Option
| Direct

Sourcetype 'target conversion_kind = 'target * option_kind

Sourcetype 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.

Sourcetype ('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;

}

Sourcetype number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj

Sourcetype string_notation_obj = (string_target_kind, unit) prim_token_notation_obj

Sourcetype prim_token_interp_info =

| Uid of prim_token_uid
| NumberNotation of number_notation_obj
| StringNotation of string_notation_obj

Sourcetype 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.

Sourceval enable_prim_token_interpretation : prim_token_infos -> unit

Compatibility. Avoid the next two functions, they will now store unnecessary objects in the library segment. Instead, combine register_*_interpretation and enable_prim_token_interpretation (the latter inside a Mltop.declare_cache_obj).

Source

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

Source

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

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

Source

val interp_prim_token : 
  ?loc:Loc.t ->
  Constrexpr.prim_token ->
  Notation_term.subscopes ->
  Glob_term.glob_constr * (notation_location * Notation_term.scope_name option)

Source

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

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

Source

val uninterp_prim_token : 
  'a Glob_term.glob_constr_g ->
  Notation_term.subscopes ->
  Constrexpr.prim_token * delimiters option

Source

val uninterp_prim_token_cases_pattern : 
  'a Glob_term.cases_pattern_g ->
  Notation_term.subscopes ->
  Names.Name.t * Constrexpr.prim_token * delimiters option

Source

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

Binds a notation in a given scope to an interpretation

Sourcetype notation_use =

| OnlyPrinting
| OnlyParsing
| ParsingAndPrinting

Source

val declare_uninterpretation : 
  ?also_in_cases_pattern:bool ->
  Notation_term.interp_rule ->
  Notation_term.interpretation ->
  unit

Sourcetype entry_coercion_kind =

| IsEntryCoercion of Constrexpr.notation_entry_level
| IsEntryGlobal of string * int
| IsEntryIdent of string * int

Source

val declare_notation : 
  (Constrexpr.notation_with_optional_scope * Constrexpr.notation) ->
  Notation_term.interpretation ->
  notation_location ->
  use:notation_use ->
  also_in_cases_pattern:bool ->
  entry_coercion_kind option ->
  Deprecation.t option ->
  unit

Source

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

Sourcetype notation_applicative_status =

| AppBoundedNotation of int
| AppUnboundedNotation
| NotAppNotation

Source

type notation_rule =
  Notation_term.interp_rule
  * Notation_term.interpretation
  * notation_applicative_status

Sourceval uninterp_notations : 'a Glob_term.glob_constr_g -> notation_rule list

Return the possible notations for a given term

Source

val uninterp_cases_pattern_notations : 
  'a Glob_term.cases_pattern_g ->
  notation_rule list

Sourceval uninterp_ind_pattern_notations : Names.inductive -> notation_rule list

Source

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

Source

val is_printing_inactive_rule : 
  Notation_term.interp_rule ->
  Notation_term.interpretation ->
  bool

Miscellaneous

Sourceval interpret_notation_string : string -> string

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

Source

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.

Source

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

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

Source

val find_arguments_scope : 
  Names.GlobRef.t ->
  Notation_term.scope_name option list

Sourcetype scope_class

Sourceval scope_class_compare : scope_class -> scope_class -> int

Comparison of scope_class

Source

val subst_scope_class : 
  Environ.env ->
  Mod_subst.substitution ->
  scope_class ->
  scope_class option

Sourceval declare_scope_class : Notation_term.scope_name -> scope_class -> unit

Sourceval declare_ref_arguments_scope : Evd.evar_map -> Names.GlobRef.t -> unit

Source

val compute_arguments_scope : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  Notation_term.scope_name option list

Source

val compute_type_scope : 
  Environ.env ->
  Evd.evar_map ->
  EConstr.types ->
  Notation_term.scope_name option

Sourceval current_type_scope_name : unit -> Notation_term.scope_name option

Get the current scope bound to Sortclass, if it exists

Sourceval scope_class_of_class : Coercionops.cl_typ -> scope_class

Building notation key

Sourcetype symbol =

| Terminal of string
| NonTerminal of Names.Id.t
| SProdList of Names.Id.t * symbol list
| Break of int

Sourceval symbol_eq : symbol -> symbol -> bool

Source

val make_notation_key : 
  Constrexpr.notation_entry ->
  symbol list ->
  Constrexpr.notation

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

Source

val decompose_notation_key : 
  Constrexpr.notation ->
  Constrexpr.notation_entry * symbol list

Sourcetype notation_symbols = {

recvars : (Names.Id.t * Names.Id.t) list;
mainvars : Names.Id.t list;
symbols : symbol list;

}

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)

Source

val pr_scope : 
  (Glob_term.glob_constr -> Pp.t) ->
  Notation_term.scope_name ->
  Pp.t

Sourceval pr_scopes : (Glob_term.glob_constr -> Pp.t) -> Pp.t

Source

val locate_notation : 
  (Glob_term.glob_constr -> Pp.t) ->
  Constrexpr.notation_key ->
  Notation_term.scope_name option ->
  Pp.t

Source

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

Source

val make_notation_entry_level : 
  Constrexpr.notation_entry ->
  Constrexpr.entry_level ->
  Constrexpr.notation_entry_level

Source

type entry_coercion =
  (Constrexpr.notation_with_optional_scope * Constrexpr.notation) list

Source

val declare_entry_coercion : 
  Constrexpr.specific_notation ->
  Constrexpr.entry_level option ->
  Constrexpr.notation_entry_level ->
  unit

Source

val availability_of_entry_coercion : 
  Constrexpr.notation_entry_level ->
  Constrexpr.notation_entry_level ->
  entry_coercion option

Sourceval declare_custom_entry_has_global : string -> int -> unit

Sourceval declare_custom_entry_has_ident : string -> int -> unit

Sourceval entry_has_global : Constrexpr.notation_entry_level -> bool

Sourceval entry_has_ident : Constrexpr.notation_entry_level -> bool

Dealing with precedences

Source

type level =
  Constrexpr.notation_entry
  * Constrexpr.entry_level
  * Constrexpr.entry_relative_level list

Sourceval level_eq : level -> level -> bool

Source

val entry_relative_level_eq : 
  Constrexpr.entry_relative_level ->
  Constrexpr.entry_relative_level ->
  bool

Declare and test the level of a (possibly uninterpreted) notation

Sourceval declare_notation_level : Constrexpr.notation -> level -> unit

Sourceval level_of_notation : Constrexpr.notation -> level

raise Not_found if not declared

Rem: printing rules for primitive token are canonical

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

Sourceval int63_of_pos_bigint : Z.t -> Uint63.t

Conversion from bigint to int63

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.interp/Notation/index.html

Module `Notation`Source

Scopes

Declare and uses back and forth an interpretation of primitive token

Declare and interpret back and forth a notation

Miscellaneous

Declare and test the level of a (possibly uninterpreted) notation

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.interp/Notation/index.html

Module NotationSource

Scopes

Declare and uses back and forth an interpretation of primitive token

Declare and interpret back and forth a notation

Miscellaneous

Declare and test the level of a (possibly uninterpreted) notation

Module `Notation`Source