Syncom.Name
A `name' represents the original named representation of a variable. These are primarily used in parsing and pretty- printing. Names should never be constructed directly. See `mk_name'.
val base_name : t -> string
val get_modules : t -> string list
val mk_blank : Location.t option -> t
Generate a blank name (underscore).
val location : t -> Location.t
Retrieves the location of this identifier. For identifiers generated internally, this will be a ghost.
Finds the maximum number used for the given name hint in the given context. Returns None if the name hint is unused.
val mk_bvar_name : (unit -> string) option -> t
mk_bvar_name vGen_opt
generates a fresh name for an LF-bound variable.
val mk_mvar_name : (unit -> string) option -> t
mk_mvar_name vGen_opt
generates a fresh name for a meta-variable.
val mk_svar_name : (unit -> string) option -> t
mk_svar_name vGen_opt
generates a fresh name for a substitution variable.
val mk_pvar_name : (unit -> string) option -> t
mk_pvar_name vGen_opt
generates a fresh name for a parameter variable.
val mk_no_name : unit -> t
mk_no_name ()
generates a fresh name.
val mk_some_string : string -> t
mk_some_name s
generates a fresh name derived from s
.
val make_from_identifier : Identifier.t -> t
make_from_identifier identifier
constructs a name from identifier
. This should be deprecated once the Name
module is fully replaced with Identifier
and Qualified_identifier
.
val make_from_qualified_identifier : Qualified_identifier.t -> t
make_from_qualified_identifier identifier
constructs a name from identifier
. This should be deprecated once the Name
module is fully replaced with Identifier
and Qualified_identifier
.
val to_identifier : t -> Identifier.t
to_identifier name
is name
as an Identifier.t
.
It is assumed that get_module name = []
.
val string_of_name : t -> string
val pp_list : Support.Format.formatter -> t list -> unit
Prints a list of space-separated names. This printer does not open a box!
Decide whether two names represent the same thing. This simply compares the string representations of the names. This corresponds with a user's intuition about when names are equal, and ignores all name generation hinting built in to the t
type.
include Support.Eq.EQ with type t := t
equal a b
is true
if and only if a
and b
are equal. This should satisfy the following properties:
equal a a = true
equal a b
is equivalent to equal b a
equal a b = true
and equal b c = true
, then equal a c = true
include Support.Show.SHOW with type t := t
val pp : Support.Format.formatter -> t -> unit
pp ppf t
emits t
pretty-printed to ppf
.
val show : t -> string
show t
pretty-prints t
to a string.
include Support.Hash.HASH with type t := t
val hash : t -> int
hash e
is the hash code computed for e
.
If e1
and e2
as equal, then hash e1
and hash e2
must be equal.