Tag (sstt.Sstt.Tag)

type t

val mk : string -> t

mk name makes a new identifier of name name. This will generate a fresh identifier even if another identifier has name name.

val name : t -> string

name t returns the name of the identifier t.

val hash : t -> int

val compare : t -> t -> int

val equal : t -> t -> bool

val pp : Stdlib.Format.formatter -> t -> unit

pp fmt t prints the name of t using the formatter fmt.

val pp_unique : Stdlib.Format.formatter -> t -> unit

pp_unique fmt t prints the name of t followed by a unique integer to disambiguate it from other identifiers with the same name.

type prop =

| NoProperty
| Monotonic of {
1. preserves_cup : bool;
2. preserves_cap : bool;
3. preserves_extremum : bool;
}

The properties of the interpretation of a tag. A tagged type $\texttt{tag}(s)$ denotes the image of s by a function $f_\texttt{tag}$ that is specific to the tag; these properties describe that function, and are what makes it possible to compare two types tagged with the same tag.

NoProperty: nothing is known about $f_\texttt{tag}$ , so $\texttt{tag}(s)$ and $\texttt{tag}(s')$ can only be related when s and s' are equivalent.
Monotonic: $f_\texttt{tag}$ is monotonic, that is, s <= s' implies $\texttt{tag}(s) \leq \texttt{tag}(s')$ . In addition, preserves_cup (resp. preserves_cap) states that it distributes over unions (resp. intersections), that is, $\texttt{tag}(s\cup s') \equiv \texttt{tag}(s)\cup\texttt{tag}(s')$ (resp. with $\cap$ ), and preserves_extremum states that it preserves the corresponding extremum, that is, $\texttt{tag}($ 𝟘 $)$ is empty (if preserves_cap is true) and $\texttt{tag}($ 𝟙 $)$ contains every value tagged with this tag (if preserves_cup is true).

val mk' : string -> prop -> t

mk' name prop makes a new tag of name name whose interpretation satisfies prop. As mk, it generates a fresh tag even if another tag has the same name.

val properties : t -> prop

properties tag returns the properties of the interpretation of tag. Tags built with mk are given the properties of the identity, that is, Monotonic with all three fields set to true.