Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680(************************************************************************)(* * 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) *)(************************************************************************)
(** This file defines a lot of different notions of names used pervasively in the kernel as well as in other places. The essential datatypes exported by this API are:
- Id.t is the type of identifiers, that is morally a subset of strings which only contains Unicode characters of the Letter kind (and a few more). - Name.t is an ad-hoc variant of Id.t option allowing to handle optionally named objects. - DirPath.t represents generic paths as sequences of identifiers. - ModPath.t are module paths. - KerName.t are absolute names of objects in Rocq.*)
open Util
(** {6 Identifiers } *)
(** Representation and operations on identifiers. *)module Id :sig type t (** Values of this type represent (Rocq) identifiers. *)
val equal : t -> t -> bool (** Equality over identifiers. *)
val compare : t -> t -> int (** Comparison over identifiers. *)
val hash : t -> int (** Hash over identifiers. *)
val is_valid : string -> bool (** Check that a string may be converted to an identifier. *)
val is_valid_ident_part : string -> bool (** Check that a string is a valid part of an identifier *)
val of_bytes : bytes -> t val of_string : string -> t (** Converts a string into an identifier. @raise UserError if the string is invalid as an identifier. *)
val of_string_soft : string -> t (** Same as {!of_string} except that any string made of supported UTF-8 characters is accepted. @raise UserError if the string is invalid as an UTF-8 string. *)
val to_string : t -> string (** Converts a identifier into an string. *)
val print : t -> Pp.t (** Pretty-printer. *)
module Set : Set.ExtS with type elt = t (** Finite sets of identifiers. *)
module Map : Map.ExtS with type key = t and module Set := Set (** Finite maps of identifiers. *)
module Pred : Predicate.S with type elt = t (** Predicates over identifiers. *)
module List : List.MonoS with type elt = t (** Operations over lists of identifiers. *)
val hcons : t Hashcons.f (** Hashconsing of identifiers. *)
end
(** Representation and operations on identifiers that are allowed to be anonymous (i.e. "_" in concrete syntax). *)module Name :sig type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *)
val mk_name : Id.t -> t (** constructor *)
val is_anonymous : t -> bool (** Return [true] iff a given name is [Anonymous]. *)
val is_name : t -> bool (** Return [true] iff a given name is [Name _]. *)
val compare : t -> t -> int (** Comparison over names. *)
val equal : t -> t -> bool (** Equality over names. *)
val hash : t -> int (** Hash over names. *)
val hcons : t Hashcons.f (** Hashconsing over names. *)
val print : t -> Pp.t (** Pretty-printer (print "_" for [Anonymous]. *)
end
(** {6 Type aliases} *)
type name = Name.t = Anonymous | Name of Id.t[@@ocaml.deprecated "(8.8) Use Name.t"]
type variable = Id.t
(** {6 Directory paths = section names paths } *)
module DirPath :sig type t (** Type of directory paths. Essentially a list of module identifiers. The order is reversed to improve sharing. E.g. A.B.C is ["C";"B";"A"] *)
val equal : t -> t -> bool (** Equality over directory paths. *)
val compare : t -> t -> int (** Comparison over directory paths. *)
val hash : t -> int (** Hash over directory paths. *)
val make : Id.t list -> t (** Create a directory path. (The list must be reversed). *)
val repr : t -> Id.t list (** Represent a directory path. (The result list is reversed). *)
val empty : t (** The empty directory path. *)
val is_empty : t -> bool (** Test whether a directory path is empty. *)
val dummy : t (** Used in [Safe_typing.empty_environment] and similar *)
val hcons : t Hashcons.f (** Hashconsing of directory paths. *)
val to_string : t -> string (** Print non-empty directory paths as ["root.module.submodule"] *)
val print : t -> Pp.t
module Set : Set.ExtS with type elt = t module Map : Map.ExtS with type key = t and module Set := Setend
module DPset = DirPath.Set [@@deprecated "(9.2) Use DirPath.Set"]module DPmap = DirPath.Map [@@deprecated "(9.2) Use DirPath.Map"]
(** {6 Unique names for bound modules} *)
module MBId :sig type t (** Unique names for bound modules. Each call to [make] constructs a fresh unique identifier. *)
val equal : t -> t -> bool (** Equality over unique bound names. *)
val compare : t -> t -> int (** Comparison over unique bound names. *)
val hash : t -> int (** Hash over unique bound names. *)
val make : DirPath.t -> Id.t -> t (** The first argument is a file name, to prevent conflict between different files. *)
val repr : t -> int * Id.t * DirPath.t (** Reverse of [make]. *)
val to_id : t -> Id.t (** Return the identifier contained in the argument. *)
val to_string : t -> string (** Encode as a string (not to be used for user-facing messages). *)
val debug_to_string : t -> string (** Same as [to_string], but outputs extra information related to debug. *)
module Set : Set.ExtS with type elt = t module Map : Map.ExtS with type key = t and module Set := Set
end
module MBIset = MBId.Set [@@deprecated "(9.2) Use MBId.Set"]module MBImap = MBId.Map [@@deprecated "(9.2) Use MBId.Map"]
(** {6 The module part of the kernel name } *)
module ModPath :sig type t = | MPfile of DirPath.t | MPbound of MBId.t | MPdot of t * Id.t
val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int
val subpath : t -> t -> bool (* [subpath p q] is true when q = p.l1. ... . ln, where n is potentially 0 *)
val is_bound : t -> bool
val dummy : t (** ([= MPfile DirPath.dummy]) *)
val dp : t -> DirPath.t
val to_string : t -> string (** Converts a identifier into an string. *)
val print : t -> Pp.t (** Pretty-printer. *)
val debug_to_string : t -> string (** Same as [to_string], but outputs extra information related to debug. *)
module Set : Set.ExtS with type elt = t module Map : Map.ExtS with type key = t and module Set := Set
end
module MPset = ModPath.Set [@@deprecated "(9.2) Use ModPath.Set"]module MPmap = ModPath.Map [@@deprecated "(9.2) Use ModPath.Map"]
(** {6 The absolute names of objects seen by kernel } *)
module KerName :sig type t
(** Constructor and destructor *) val make : ModPath.t -> Id.t -> t val repr : t -> ModPath.t * Id.t
(** Projections *) val modpath : t -> ModPath.t val label : t -> Id.t
val to_string : t -> string (** Encode as a string (not to be used for user-facing messages). *)
val print : t -> Pp.t (** Print internal representation (not to be used for user-facing messages). *)
val debug_to_string : t -> string (** Same as [to_string], but outputs extra information related to debug. *)
val debug_print : t -> Pp.t (** Same as [print], but outputs extra information related to debug. *)
(** Comparisons *) val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int
module Set : CSig.USetS with type elt = t module Map : Map.UExtS with type key = t and module Set := Set module Pred : Predicate.S with type elt = t
end
module KNset = KerName.Set [@@deprecated "(9.2) Use KerName.Set"]module KNpred = KerName.Pred [@@deprecated "(9.2) Use KerName.Pred"]module KNmap = KerName.Map [@@deprecated "(9.2) Use KerName.Map"]
(** {6 Signature for quotiented names} *)
module type EqType =sig type t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> intend
module type QNameS =sig type t (** A type of reference that implements an implicit quotient by containing two different names. The first one is the user name, i.e. what the user sees when printing. The second one is the canonical name, which is the actual absolute name of the reference.
This mechanism is fundamentally tied to the module system of Rocq. Functor application and module inclusion are the typical ways to introduce names where the canonical and user components differ. In particular, the two components should be undistinguishable from the point of view of typing, i.e. from a "kernel" ground. This aliasing only makes sense inside an environment, but at this point this notion is not even defined so, this dual name trick is fragile. One has to ensure many invariants when creating such names, but the kernel is quite lenient when it comes to checking that these invariants hold. (Read: there are soundness bugs lurking in the module system.)
One could enforce the invariants by splitting the names and storing that information in the environment instead, but unfortunately, this wreaks havoc in the upper layers. The latter are infamously not stable by syntactic equality, in particular they might observe the difference between canonical and user names if not packed together.
For this reason, it is discouraged to use the canonical-accessing API in the upper layers, notably the [CanOrd] module below. Instead, one should use their quotiented versions defined in the [Environ] module. Eventually all uses to [CanOrd] outside of the kernel should be removed.
CAVEAT: name sets and maps are still exposing a canonical-accessing API surreptitiously. *)
module CanOrd : EqType with type t = t (** Equality functions over the canonical name. Their use should be restricted to the kernel. *)
module UserOrd : EqType with type t = t (** Equality functions over the user name. *)
val canonize : t -> t (** Returns the canonical version of the name *)end
(** {6 Constant Names } *)
module Constant:sig type t
(** Constructors *)
val make : KerName.t -> KerName.t -> t (** Builds a constant name from a user and a canonical kernel name. *)
val make1 : KerName.t -> t (** Special case of [make] where the user name is canonical. *)
val make2 : ModPath.t -> Id.t -> t (** Shortcut for [(make1 (KerName.make ...))] *)
(** Projections *)
val user : t -> KerName.t val canonical : t -> KerName.t
val modpath : t -> ModPath.t (** Shortcut for [KerName.modpath (user ...)] *)
val label : t -> Id.t (** Shortcut for [KerName.label (user ...)] *)
(** Comparisons *)
include QNameS with type t := t
val change_label : t -> Id.t -> t (** Builds a new constant name with a different label *)
(** Displaying *)
val to_string : t -> string (** Encode as a string (not to be used for user-facing messages). *)
val print : t -> Pp.t (** Print internal representation (not to be used for user-facing messages). *)
val debug_to_string : t -> string (** Same as [to_string], but outputs extra information related to debug. *)
val debug_print : t -> Pp.t (** Same as [print], but outputs extra information related to debug. *)
end
(** Sets and maps use the UserOrd ordering to index keys. *)module Cset : CSig.USetS with type elt = Constant.tmodule Cmap : Map.UExtS with type key = Constant.t and module Set := Cset
module Cpred : Predicate.S with type elt = Constant.t(* CAVEAT: uses CanOrd to index keys. *)
module Cset_env = Cset[@@ocaml.deprecated "(9.4) Use Cset"]module Cmap_env = Cmap[@@ocaml.deprecated "(9.4) Use Cmap"]
(** {6 Inductive names} *)
module MutInd :sig type t
(** Constructors *)
val make : KerName.t -> KerName.t -> t (** Builds a mutual inductive name from a user and a canonical kernel name. *)
val make1 : KerName.t -> t (** Special case of [make] where the user name is canonical. *)
val make2 : ModPath.t -> Id.t -> t (** Shortcut for [(make1 (KerName.make ...))] *)
(** Projections *)
val user : t -> KerName.t val canonical : t -> KerName.t
val modpath : t -> ModPath.t (** Shortcut for [KerName.modpath (user ...)] *)
val label : t -> Id.t (** Shortcut for [KerName.label (user ...)] *)
(** Comparisons *)
include QNameS with type t := t
(** Displaying *)
val to_string : t -> string (** Encode as a string (not to be used for user-facing messages). *)
val print : t -> Pp.t (** Print internal representation (not to be used for user-facing messages). *)
val debug_to_string : t -> string (** Same as [to_string], but outputs extra information related to debug. *)
val debug_print : t -> Pp.t (** Same as [print], but outputs extra information related to debug. *)
end
module Mindset : CSig.USetS with type elt = MutInd.tmodule Mindmap : Map.UExtS with type key = MutInd.t and module Set := Mindset
module Mindmap_env = Mindmap[@@ocaml.deprecated "(9.4) Use Mindmap"]
module Ind :sig (** Designation of a (particular) inductive type. *) type t = MutInd.t (* the name of the inductive type *) * int (* the position of this inductive type within the block of mutually-recursive inductive types. BEWARE: indexing starts from 0. *) val modpath : t -> ModPath.t
include QNameS with type t := t
end
type inductive = Ind.t
module Construct :sig (** Designation of a (particular) constructor of a (particular) inductive type. *) type t = Ind.t (* designates the inductive type *) * int (* the index of the constructor BEWARE: indexing starts from 1. *)
val modpath : t -> ModPath.t
include QNameS with type t := t
end
type constructor = Construct.t
module Indset : CSet.ExtS with type elt = inductivemodule Constrset : CSet.ExtS with type elt = constructor
module Indmap : CMap.ExtS with type key = inductive and module Set := Indsetmodule Constrmap : CMap.ExtS with type key = constructor and module Set := Constrset
module Indset_env = Indset[@@ocaml.deprecated "(9.4) Use Indset"]module Constrset_env = Constrset[@@ocaml.deprecated "(9.4) Use Constrset"]module Indmap_env = Indmap[@@ocaml.deprecated "(9.4) Use Indmap"]module Constrmap_env = Constrmap[@@ocaml.deprecated "(9.4) Use Constrmap"]
val ith_mutual_inductive : inductive -> int -> inductiveval ith_constructor_of_inductive : inductive -> int -> constructorval inductive_of_constructor : constructor -> inductiveval index_of_constructor : constructor -> int
(** {6 Hash-consing } *)
val hcons_con : Constant.t Hashcons.fval hcons_mind : MutInd.t Hashcons.fval hcons_ind : inductive Hashcons.fval hcons_construct : constructor Hashcons.f
(******)
type 'a tableKey = | ConstKey of 'a | VarKey of Id.t | RelKey of Int.t
type inv_rel_key = int (** index in the [rel_context] part of environment starting by the end, {e inverse} of de Bruijn indice *)
val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> boolval hash_table_key : ('a -> int) -> 'a tableKey -> intval eq_constant_key : Constant.t -> Constant.t -> bool
(** {5 Module paths} *)
type module_path = ModPath.t = | MPfile of DirPath.t | MPbound of MBId.t | MPdot of ModPath.t * Id.t[@@ocaml.deprecated "(8.8) Alias type"]
module Projection : sig module Repr : sig type t
val make : inductive -> proj_npars:int -> proj_arg:int -> t
include QNameS with type t := t
val inductive : t -> inductive val mind : t -> MutInd.t val npars : t -> int val arg : t -> int
val map : (MutInd.t -> MutInd.t) -> t -> t val map_npars : (int -> int) -> t -> t
val to_string : t -> string (** Encode as a string (not to be used for user-facing messages). *)
val print : t -> Pp.t (** Print internal representation (not to be used for user-facing messages). *)
end type t (* = Repr.t * bool *)
val make : Repr.t -> bool -> t val repr : t -> Repr.t
include QNameS with type t := t
val mind : t -> MutInd.t val inductive : t -> inductive val npars : t -> int val arg : t -> int val unfolded : t -> bool val unfold : t -> t
val hcons : t Hashcons.f (** Hashconsing of projections. *)
val map : (MutInd.t -> MutInd.t) -> t -> t val map_npars : (int -> int) -> t -> t
val to_string : t -> string (** Encode as a string (not to be used for user-facing messages). *)
val print : t -> Pp.t (** Print internal representation (not to be used for user-facing messages). *)
val debug_to_string : t -> string (** Same as [to_string], but outputs extra information related to debug. *)
val debug_print : t -> Pp.t (** Same as [print], but outputs extra information related to debug. *)
end
module PRset : CSig.USetS with type elt = Projection.Repr.tmodule PRmap : Map.UExtS with type key = Projection.Repr.t and module Set := PRset
module PRset_env = PRset[@@ocaml.deprecated "(9.4) Use PRset"]module PRmap_env = PRmap[@@ocaml.deprecated "(9.4) Use PRmap"]
(* CAVEAT: uses CanOrd to index keys. *)module PRpred : Predicate.S with type elt = Projection.Repr.t
(** {6 Global reference is a kernel side type for all references together } *)
module GlobRef : sig
type t = | VarRef of variable (** A reference to the section-context. *) | ConstRef of Constant.t (** A reference to the environment. *) | IndRef of inductive (** A reference to an inductive type. *) | ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
val is_bound : t -> bool
include QNameS with type t := t
module Set : CSig.USetS with type elt = t module Map : Map.UExtS with type key = t and module Set := Set
module Set_env = Set [@@ocaml.deprecated "(9.4) Use GlobRef.Set"] module Map_env = Map [@@ocaml.deprecated "(9.4) Use GlobRef.Map"]
val print : t -> Pp.t (** Print internal representation (not to be used for user-facing messages). *)
end
(** Located identifiers and objects with syntax. *)
type lident = Id.t CAst.ttype lname = Name.t CAst.ttype lstring = string CAst.t
val lident_eq : lident -> lident -> bool
(** Deprecated *)module Label : sig type t = Id.t (** Type of labels *)
val equal : t -> t -> bool (** Equality over labels *)
val compare : t -> t -> int (** Comparison over labels. *)
val hash : t -> int (** Hash over labels. *)
val make : string -> t (** Create a label out of a string. *)
val of_id : Id.t -> t (** Conversion from an identifier. *)
val to_id : t -> Id.t (** Conversion to an identifier. *)
val to_string : t -> string (** Conversion to string. *)
val print : t -> Pp.t (** Pretty-printer. *)
module Set : Set.ExtS with type elt = t module Map : Map.ExtS with type key = t and module Set := Set
val hcons : t Hashcons.f
end [@@deprecated "(9.2) Use Id"]