O (sstt.Sstt.Ty.O)

type node = Ty.t

An alias for the type Ty.t.

type t = node * bool

The type of optional types. Whenever the boolean component is true, it means that the type contains the undefined element $\bot$ . Otherwise, when the boolean component is false, the type is equivalent to a plain Ty.t type.

val any : t

The top element of t (the set of all values of type t).

val empty : t

The bottom element of t (the empty set of values of type t).

val compare : t -> t -> int

Comparison working on the internal representation of t.

val equal : t -> t -> bool

Equality, equal a b is equivalent to compare a b = 0.

val absent : t

absent is the singleton type containing the undefined value, $\bot$ .

val required : node -> t

required t returns the type t, false.

val optional : node -> t

optional t returns t, true which represents the type $t\cup \bot$ .

val cap : t -> t -> t

The intersection of two types, $t_1 \cap t_2$ .

val cup : t -> t -> t

The union of two types, $t_1 \cup t_2$ .

val diff : t -> t -> t

The difference of two types, $t_1 \setminus t_2$ .

val neg : t -> t

The negation of a type, $\lnot t$ .

val conj : t list -> t

conj l is the intersection of all the types in l. It returns any if l is the empty list.

val disj : t list -> t

disj l is the union of all the types in l. It returns empty if l is the empty list.

val is_empty : t -> bool

Emptyness test. is_empty t returns true if and only if t is semantically equivalent to empty.

val is_any : t -> bool

Fullness test. is_any t returns true if and only if t is semantically equivalent to any.

val leq : t -> t -> bool

Subtyping test. leq t1 t2 returns true if and only if t1 is a subtype of t2.

val equiv : t -> t -> bool

Type equivalence test. equiv t1 t2 returns true if and only if leq t1 t2 and leq t2 t1.

val disjoint : t -> t -> bool

Disjointedness test. disjoint t1 t2 returns true if and only if cap t1 t2 is empty.

val is_absent : t -> bool

Tests whether $\bot \equiv t$ .

val is_required : t -> bool

Tests whether $\bot \not\in t$ .

val is_optional : t -> bool

Tests whether $\bot \in t$

val get : t -> node

Returns get (t, b) returns t.