Module `Notation`Source

Notations

Sourceval notation_cat : Libobject.category

Sourceval 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

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 push_scope : Notation_term.scope_name -> scopes -> scopes

Sourceval find_scope : Notation_term.scope_name -> scope

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

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

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 = {

pt_local : bool;
(*
Is this interpretation local?
*)
pt_scope : Notation_term.scope_name;
(*
Concerned scope
*)
pt_interp_info : PrimNotations.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

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_term.scope_name option

Source

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

Source

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

Source

val 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

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

Sourceval warning_overridden_name : string

Sourcetype entry_coercion_kind =

| IsEntryCoercion of Constrexpr.notation_entry_level * Constrexpr.notation_entry_relative_level
| IsEntryGlobal of Globnames.CustomName.t * int
| IsEntryIdent of Globnames.CustomName.t * int

Source

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

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

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 : 
  Notationextern.interp_rule ->
  Notation_term.interpretation ->
  bool

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

}

Sourcetype notation_query_pattern = Libnames.qualid notation_query_pattern_gen

Source

val 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 =

| AmbiguousNotationAsReference of Constrexpr.notation_key
| 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

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. Raise NotationAsReferenceError if not resolvable as a global reference

Source

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

Source

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

Source

val 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

Source

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

Sourcetype add_scope_where =

| AddScopeTop
| AddScopeBottom
(*
add new scope at top or bottom of existing stack (default is reset)
*)

Source

val declare_scope_class : 
  bool ->
  Notation_term.scope_name ->
  ?where:add_scope_where ->
  scope_class ->
  unit

Sourceval declare_ref_arguments_scope : Names.GlobRef.t -> unit

Source

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

Source

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

Source

val 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 =

| 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;

}

Source

val 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)

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

Coercions between entries

Source

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

Source

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

Source

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

Source

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

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

Source

val prec_less : 
  Constrexpr.entry_level ->
  Constrexpr.entry_relative_level ->
  bool

Source

val may_capture_cont_after : 
  Constrexpr.entry_level option ->
  Constrexpr.entry_relative_level ->
  bool

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

Source

val declare_notation_level : 
  Constrexpr.notation ->
  Notationextern.level ->
  unit

Sourceval level_of_notation : Constrexpr.notation -> Notationextern.level

raise Not_found if not declared

Rem: printing rules for primitive token are canonical

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

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.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 rocq-runtime

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.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

dune-project
Dependency

Module `Notation`Source