package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Notations

val notation_cat : Libobject.category
val 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

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

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

* Number notation

type prim_token_notation_error =
  1. | UnexpectedTerm of Constr.t
  2. | UnexpectedNonOptionTerm of Constr.t
exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_token_notation_error
type numnot_option =
  1. | Nop
  2. | Warning of NumTok.UnsignedNat.t
  3. | Abstract of NumTok.UnsignedNat.t
type int_ty = {
  1. dec_uint : Names.inductive;
  2. dec_int : Names.inductive;
  3. hex_uint : Names.inductive;
  4. hex_int : Names.inductive;
  5. uint : Names.inductive;
  6. int : Names.inductive;
}
type z_pos_ty = {
  1. z_ty : Names.inductive;
  2. pos_ty : Names.inductive;
}
type number_ty = {
  1. int : int_ty;
  2. decimal : Names.inductive;
  3. hexadecimal : Names.inductive;
  4. number : Names.inductive;
}
type pos_neg_int63_ty = {
  1. pos_neg_int63_ty : Names.inductive;
}
type target_kind =
  1. | Int of int_ty
  2. | UInt of int_ty
  3. | Z of z_pos_ty
  4. | Int63 of pos_neg_int63_ty
  5. | Float64
  6. | Number of number_ty
type string_target_kind =
  1. | ListByte
  2. | Byte
  3. | PString
type option_kind =
  1. | Option
  2. | Direct
type 'target conversion_kind = 'target * option_kind
type to_post_arg =
  1. | ToPostCopy
  2. | ToPostAs of int
  3. | ToPostHole
  4. | 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 = {
  1. to_kind : 'target conversion_kind;
  2. to_ty : Names.GlobRef.t;
  3. to_post : (Names.GlobRef.t * Names.GlobRef.t * to_post_arg list) list array;
  4. of_kind : 'target conversion_kind;
  5. of_ty : Names.GlobRef.t;
  6. ty_name : Libnames.qualid;
  7. 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 =
  1. | Uid of prim_token_uid
  2. | NumberNotation of number_notation_obj
  3. | StringNotation of string_notation_obj
type prim_token_infos = {
  1. pt_local : bool;
    (*

    Is this interpretation local?

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

    Concerned scope

    *)
  3. pt_interp_info : 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.

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_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_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
val warning_overridden_name : string
type entry_coercion_kind =
  1. | IsEntryCoercion of Constrexpr.notation_entry_level * Constrexpr.notation_entry_relative_level
  2. | IsEntryGlobal of string * int
  3. | IsEntryIdent of string * int

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

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
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 =
  1. | AddScopeTop
  2. | 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

Building notation key

type symbol =
  1. | Terminal of string
  2. | NonTerminal of Names.Id.t
  3. | SProdList of Names.Id.t * symbol list
  4. | 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 = {
  1. recvars : (Names.Id.t * Names.Id.t) list;
  2. mainvars : Names.Id.t list;
  3. 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_scopes : (Glob_term.glob_constr -> Pp.t) -> Pp.t
val 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

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

Rem: printing rules for primitive token are canonical

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

Conversion from bigint to int63

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct