diff options
Diffstat (limited to 'kernel/names.mli')
-rw-r--r-- | kernel/names.mli | 38 |
1 files changed, 26 insertions, 12 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 59419af2e..38a51a392 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -10,30 +10,33 @@ open Util (** {6 Identifiers } *) +(** Representation and operations on identifiers. *) module Id : sig type t - (** Type of identifiers *) + (** Values of this type represent (Coq) identifiers. *) val equal : t -> t -> bool - (** Equality over identifiers *) + (** Equality over identifiers. *) val compare : t -> t -> int - (** Comparison over identifiers *) + (** Comparison over identifiers. *) val hash : t -> int - (** Hash over identifiers *) + (** Hash over identifiers. *) val is_valid : string -> bool - (** Check that a string may be converted to an identifier. *) + (** Check that a string may be converted to an identifier. + @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) val of_string : string -> t - (** Converts a string into an identifier. May raise [UserError _] if the - string is not valid, or echo a warning if it contains invalid identifier - characters. *) + (** Converts a string into an identifier. + @raise UserError if the string is not valid, or echo a warning if it contains invalid identifier characters. + @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) val of_string_soft : string -> t - (** Same as {!of_string} except that no warning is ever issued. *) + (** Same as {!of_string} except that no warning is ever issued. + @raise Unicode.Unsupported if the provided string contains unsupported UTF-8 characters. *) val to_string : t -> string (** Converts a identifier into an string. *) @@ -58,10 +61,12 @@ sig end +(** Representation and operations on identifiers that are allowed to be anonymous + (i.e. "_" in concrete syntax). *) module Name : sig - type t = Name of Id.t | Anonymous - (** A name is either undefined, either an identifier. *) + type t = Anonymous (** anonymous identifier *) + | Name of Id.t (** non-anonymous identifier *) val compare : t -> t -> int (** Comparison over names. *) @@ -79,7 +84,7 @@ end (** {6 Type aliases} *) -type name = Name.t = Name of Id.t | Anonymous +type name = Name.t = Anonymous | Name of Id.t type variable = Id.t type module_ident = Id.t @@ -160,6 +165,8 @@ sig module Set : Set.S with type elt = t module Map : Map.ExtS with type key = t and module Set := Set + val hcons : t -> t + end (** {6 Unique names for bound modules} *) @@ -217,6 +224,9 @@ sig val to_string : t -> string + val debug_to_string : t -> string + (** Same as [to_string], but outputs information related to debug. *) + val initial : t (** Name of the toplevel structure ([= MPfile initial_dir]) *) @@ -244,6 +254,10 @@ sig (** Display *) val to_string : t -> string + + val debug_to_string : t -> string + (** Same as [to_string], but outputs information related to debug. *) + val print : t -> Pp.std_ppcmds (** Comparisons *) |