Ty (sstt.Sstt.Ty)

Basics

type t

The type of (set-theoretic) types. A value of type t is a reference to a descriptor that represent its structure (its variables, components, …). Each value of type t contains a unique internal identifier which is used for equality

val equal : t -> t -> bool

equal t1 t2 returns true if and only if t1 and t2 denote the same reference. It is provided e.g. to implement hash tables indexed by types and does not implement syntactic nor semantic equality. The function runs in constant time.

val compare : t -> t -> int

compare t1 t2 implements a total order on types, seen as references. compare t1 t2 = 0 if and only if equal t1 t2 = true. The function runs in constant time.

val hash : t -> int

hash t returns a hash for the given type. The function runs in constant time.

Set-theoretic operations

val empty : t

The empty type, 𝟘.

val any : t

The top type, 𝟙.

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.

Full descriptors

The VDescr module and its operations allow one to access the internal structure of a type.

module VDescr : sig ... end

Full descriptors with top-level variables.

val def : t -> VDescr.t

def t returns the full descriptor of t. For a given type (reference) t, def t is not necessarily constant: it may change over time, for instance when the descriptor of t is simplified.

val of_def : VDescr.t -> t

of_def d creates a type from the full descriptor d.

val mk_var : Var.t -> t

mk_var v creates a type from a type variable.

val mk_descr : VDescr.Descr.t -> t

mk_descr d creates a type from the monomorphic descriptor d.

val get_descr : t -> VDescr.Descr.t

get_descr t extracts a monomorphic descriptor from t, which describes t by ignoring its top-level type variables.s

Misc. operations

val vars : t -> VarSet.t

vars t returns the set of all variables in t. Note that due to simplifications some variables may or may not be present. For instance, if $t_1 \equiv \alpha$ and $t_2 \equiv \lnot \alpha$

val vars_toplevel : t -> VarSet.t

vars_toplevel t returns the top-level variables of t, that is, occurrences of variables that are not below a constructor.

val nodes : t -> t list

nodes t returns all the nodes appearing in t (including t itself).

val of_eqs : (Var.t * t) list -> (Var.t * t) list

of_eqs [(x1,t1);...;(xn,tn)] returns the types x1, ..., xn satisfying the system of equations x1=t1, ..., xn=tn. Raises: Invalid_argument if the set of equations is not contractive.

val substitute : t VarMap.t -> t -> t

substitute s t applies the type variable substitution s to t.

val factorize : t -> t

factorize t factorizes equivalent nodes in t. This operation may be expensive since it calls equiv internally.

Optional types

module O : sig ... end

Optional types are subsets of 𝟙 $\cup\bot$ . They are used for the type of record fields, to denote the fact that a field may be absent.