Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Namesopen Libnamesopen Constrexpropen Glob_termopen Notation_termopen Notationexternopen Globnames
(** Notations *)
val notation_cat : Libobject.category
val pr_notation : notation -> Pp.t(** Printing *)
module NotationSet : CSet.ExtS with type elt = notationmodule NotationMap : CMap.ExtS with type key = notation and module Set := NotationSetmodule SpecificNotationSet : CSet.ExtS with type elt = specific_notationmodule SpecificNotationMap : CMap.ExtS with type key = specific_notation and module Set := SpecificNotationSet
(** {6 Scopes } *)(** A scope is a set of interpreters for symbols + optional interpreter and printers for integers + optional delimiters *)
type delimiters = stringtype scopetype scopes (** = [scope_name list] *)
val declare_scope : scope_name -> unit
(* To be removed after deprecation phase *)val ensure_scope : scope_name -> unit
val current_scopes : unit -> scopes
(** Check where a scope is opened or not in a scope list, or in * the current opened scopes *)val scope_is_open_in_scopes : scope_name -> scopes -> boolval scope_is_open : scope_name -> bool
(** Open scope *)val open_scope : scope_name -> unitval close_scope : scope_name -> unit
(** Return a scope taking either a scope name or delimiter *)val normalize_scope : string -> scope_name
(** Extend a list of scopes *)val empty_scope_stack : scopesval push_scope : scope_name -> scopes -> scopes
val find_scope : scope_name -> scope
val scope_delimiters : scope -> delimiters option
(** Declare delimiters for printing *)
val declare_delimiters : scope_name -> delimiters -> unitval remove_delimiters : scope_name -> unitval find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
(** {6 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 = (DirPath.t * DirPath.t * Loc.t option) * string(** 1st dirpath: dirpath of the library 2nd dirpath: module and section-only dirpath (ie [Lib.current_dirpath true]) location: The location. Presumably you can recover the dirpaths from that but I don't know how. string: string used to generate the notation
dirpaths are used for dumpglob, the location for Locate, and string for printing (pr_notation_info)*)
type required_module = full_path * string list
type prim_token_infos = { pt_local : bool; (** Is this interpretation local? *) pt_scope : 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 : 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 -> prim_token -> subscopes -> glob_constr(* This function returns a glob_const representing a pattern *)val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (Glob_term.glob_constr -> unit) -> prim_token -> subscopes -> glob_constr
(** Return the primitive token associated to a [term]/[cases_pattern]; raise [No_match] if no such token *)
val uninterp_prim_token : print_float:bool -> 'a glob_constr_g -> subscopes -> prim_token * delimiters optionval uninterp_prim_token_cases_pattern : print_float:bool -> 'a cases_pattern_g -> subscopes -> Name.t * prim_token * delimiters option
val availability_of_prim_token : prim_token -> scope_name -> subscopes -> delimiters option option
(** {6 Declare and interpret back and forth a notation } *)
val warning_overridden_name : string
type entry_coercion_kind = | IsEntryCoercion of notation_entry_level * notation_entry_relative_level | IsEntryGlobal of CustomName.t * int | IsEntryIdent of CustomName.t * int
val declare_notation : notation_with_optional_scope * notation -> interpretation -> notation_location -> use:notation_use -> entry_coercion_kind option -> UserWarn.t option -> unit
(** Return the interpretation bound to a notation *)val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option)
(** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the returned subscopes is itself not the empty list if delimiters are needed *)val availability_of_notation : specific_notation -> subscopes -> (subscopes * delimiters option) option
val is_printing_inactive_rule : Notationextern.interp_rule -> interpretation -> bool
type 'a notation_query_pattern_gen = { notation_entry_pattern : notation_entry list; interp_rule_key_pattern : (notation_key, 'a) Util.union option; use_pattern : notation_use; scope_pattern : notation_with_optional_scope option; interpretation_pattern : interpretation option; }
type notation_query_pattern = qualid notation_query_pattern_gen
val toggle_notations : on:bool -> all:bool -> ?verbose:bool -> (glob_constr -> Pp.t) -> notation_query_pattern -> unit
(** {6 Miscellaneous} *)
(** Take a notation string and turn it into a notation key. eg. ["x + y"] becomes ["_ + _"]. *)val interpret_notation_string : string -> string
type notation_as_reference_error = | AmbiguousNotationAsReference of notation_key | NotationNotReference of Environ.env * Evd.evar_map * notation_key * (notation_key * notation_constr) list
exception NotationAsReferenceError of notation_as_reference_error
(** If head is true, also allows applied global references. Raise NotationAsReferenceError if not resolvable as a global reference *)val interp_notation_as_global_reference : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) -> notation_key -> delimiters option -> GlobRef.t
(** Same together with the full notation *)val interp_notation_as_global_reference_expanded : ?loc:Loc.t -> head:bool -> (GlobRef.t -> bool) -> notation_key -> delimiters option -> notation * notation_key * notation_with_optional_scope * interpretation * GlobRef.t
(** Declares and looks for scopes associated to arguments of a global ref *)val declare_arguments_scope : bool (** true=local *) -> GlobRef.t -> subscopes list -> unit
val find_arguments_scope : Environ.env -> GlobRef.t -> subscopes list
type scope_class
(** Comparison of scope_class *)val scope_class_compare : scope_class -> scope_class -> int
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 : (* local: *) bool -> scope_name -> ?where:add_scope_where -> scope_class -> unitval declare_ref_arguments_scope : GlobRef.t -> unit
val compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> subscopes listval compute_type_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name listval compute_glob_type_scope : 'a Glob_term.glob_constr_g -> scope_name list
(** Get the current scopes bound to Sortclass *)val current_type_scope_names : unit -> scope_name list
val scope_class_of_class : Coercionops.cl_typ -> scope_class
(** Building notation key *)
type symbol = | Terminal of string (* an expression including symbols or a simply-quoted ident, e.g. "'U'" or "!" *) | NonTerminal of Id.t (* an identifier "x" *) | SProdList of Id.t * symbol list (* an expression "x sep .. sep y", remembering x (or y) and sep *) | Break of int (* a sequence of blanks > 1, e.g. " " *)
val symbol_eq : symbol -> symbol -> bool
(** Make/decompose a notation of the form "_ U _" *)val make_notation_key : notation_entry -> symbol list -> notationval decompose_notation_key : notation -> notation_entry * symbol list
(** This is the output of decomposing a notation declaration: [mainvars] include all notation variables, keeping only one for each pair (typically the first one) in case of a recursive pattern (e.g. in ``Notation "[ x ; y ; .. ; z ]" := ...'', the mainvars are [x;y]); [maintypes] describes the structure of the pattern, e.g., for the same notation, it is [[NtnRawTypeVar "x"; NtnRawTypeVarList (NtnRawTypeVar ("y", "z"))]] [symbols] describes the parsing rule, e.g. for the same notation, it is [[Terminal "["; NonTerminal "x"; SProdList ("y",[Terminal ";"]); Terminal "]"]] *)type notation_symbols = { mainvars : Id.t list; (* names of "toplevel" non-terminals *) maintypes : Id.t notation_raw_type list; (* types of "toplevel" non-terminals *) symbols : symbol list; (* the decomposition of the notation into terminals and nonterminals; there, recursive patterns refer to the left-hand variable *)}
val is_prim_token_constant_in_constr : notation_entry * symbol list -> bool
(** 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 decompose_raw_notation : string -> notation_symbols
(** Prints scopes (expects a pure aconstr printer) *)val pr_scope_class : scope_class -> Pp.tval pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.tval pr_scopes : (glob_constr -> Pp.t) -> Pp.tval locate_notation : (glob_constr -> Pp.t) -> notation_key -> scope_name option -> Pp.t
val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
(** Coercions between entries *)
val is_coercion : notation_entry_level -> 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 : specific_notation -> notation_entry_level -> notation_entry_relative_level -> unit (** Add a coercion from some-entry to some-relative-entry *)
type entry_coercion = (notation_with_optional_scope * notation) listval availability_of_entry_coercion : ?non_included:bool -> notation_entry_relative_level -> 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 : CustomName.t -> int -> unitval declare_custom_entry_has_ident : CustomName.t -> int -> unit
val entry_has_global : notation_entry_relative_level -> boolval entry_has_ident : notation_entry_relative_level -> bool
val app_level : int
val prec_less : entry_level -> entry_relative_level -> boolval may_capture_cont_after : entry_level option -> entry_relative_level -> bool
(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
val declare_notation_level : notation -> level -> unitval level_of_notation : notation -> level (** raise [Not_found] if not declared *)
(** Rem: printing rules for primitive token are canonical *)
val with_notation_protection : ('a -> 'b) -> 'a -> 'b
val declare_ntn_gram_loc : notation -> Loc.t option -> unit