Module Syncom.Qualified_identifier

Namespaced identifiers.

These are names for referring to bound names nested in namespaces.

Qualified identifiers may be prefixed by the namespaces that need to be opened in order to bring the referred constant in the current scope. The parts of a qualified identifier are delimited by '.'.

For instance, if z is an LF term-level constant, then the following are qualified identifiers:

type t

Constructors

val make : ?location:Location.t -> ?namespaces:Identifier.t Support.List.t -> Identifier.t -> t

make ?location ?namespaces name is the qualified identifier having location location, namespaces namespaces and name name.

The namespaces in namespaces are expected to be in order of appeareance as in the external syntax. That is, the qualified identifier qid = Util.Nat.z has namespaces qid = ["Util"; "Nat"].

  • If location is unspecified and namespaces = [], then the location is that of name.
  • If location is unspecified and namespaces <> [], then the location is the union of the locations for each module in namespaces and the location of name.
val make_simple : Identifier.t -> t

make_simple name is make name.

val prepend_module : Identifier.t -> t -> t

prepend_module module_ qid is the qualified name derived from qid with module_ prepended to it.

Destructors

val location : t -> Location.t

location qid is the location of qid.

val namespaces : t -> Identifier.t Support.List.t

namespaces qid is the module prefixes of qid.

For instance, if qid = Util.Nat.z, then namespaces qid = ["Util"; "Nat"].

val name : t -> Identifier.t

name qid is the identifier in the tail end position of qid.

For instance, if qid = Util.Nat.z, then name qid = "z".

Exceptions

exception Unbound_qualified_identifier of t
exception Unbound_namespace of t

Interoperability

val from_list1 : Identifier.t Support.List1.t -> t

from_list1 (x1, [x2; x3; ...; xn]) is the qualified identifier with namespaces [x1; x2; ...; x(n-1)] and name xn.

val to_list1 : t -> Identifier.t Support.List1.t

to_list1 id is the non-empty list (x1, [x2; x3; ...; xn]) where [x1; x2; ...; x(n-1)] are the namespaces of id, and xn is the name of id.

Instances

Equality of qualified identifiers by namespaces and names. Locations are ignored.

include Support.Eq.EQ with type t := t

Lexicographical ordering of qualified identifiers.

include Support.Ord.ORD with type t := t
val compare : t -> t -> int

compare a b compares a and b for ordering.

  • compare a b < 0 if a precedes b (denoted a < b),
  • compare a b = 0 if a is equal to b (denoted a = b),
  • compare a b > 0 if a succeeds b (denoted a > b).

This should satisfy the following properties:

  • Comparability: (compare a b <= 0 || compare b a >= 0) = true,
  • Transitivity: if (compare a b <= 0) = true and (compare b c <= 0) = true, then (compare a c <= 0) = true,
  • Reflexivity: (compare a a = 0) = true,
  • Antisymmetry: if (compare a b <= 0) = true and (compare a b >= 0) = true then (compare a b = 0) = true.
val (<) : t -> t -> bool
val (<=) : t -> t -> bool
val (>) : t -> t -> bool
val (>=) : t -> t -> bool
val max : t -> t -> t

max a b is a if a >= b and b otherwise.

val min : t -> t -> t

min a b is a if a <= b and b otherwise.

include Support.Eq.EQ with type t := t
val equal : t -> t -> bool

equal a b is true if and only if a and b are equal. This should satisfy the following properties:

  • Reflexivity: equal a a = true
  • Symmetry: equal a b is equivalent to equal b a
  • Transitivity: if equal a b = true and equal b c = true, then equal a c = true
val (=) : t -> t -> bool

Operator alias of equal.

val (<>) : t -> t -> bool

Negation of operator (=).

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.

Collections

module Map : Stdlib.Map.S with type key = t
module Set : Stdlib.Set.S with type elt = t