Sstt (sstt.Sstt)

Types and their components

The API to manipulate them follows a layered structure to account for the fact that types are equi-recursive:

a type $t$ (implemented by Ty.t) is a reference to a descriptor with top-level variables, $t = v$
a full descriptor with top-level variables $v$ (implemented by type VDescr.t) represents a disjunctive normal form of positive and negative top-level variables and monomorphic descriptors:
```
     v = \bigcup_{i=i\ldots m} ~~\bigcap_{j=1\ldots p} \alpha_{ij} \cap \bigcap_{j=1\ldots n} \lnot\beta_{ij} ~~\cap~~ d_i
     
```
a monomorphic descriptor $d$ (implemented by Descr.t is a disjoint union of components. Components are intervals, enums, tuples, tagged types, arrows and records.
Components intervals and enums correspond to basic types
Components such as tuples, tagged types, arrows and records correspond to type constructors and are union of intersections of atoms, the latter containing type references Ty.t. For instance, the component for arrows represents:
```
      a = \bigcup_{i=1\ldots m} \bigcap_{j=1 \ldots p} t_{ij}^1 \rightarrow t_{ij}^2 \cap \bigcap_{j=1 \ldots n} \lnot(t_{ij}^1 \rightarrow t_{ij}^2) 
      
```

Types and descriptors

module Ty : sig ... end

Set-theoretic types (type references).

module VDescr : sig ... end

Full descriptors with top-level variables.

module Descr : sig ... end

Monomorphic type descriptors.

Components

Components are the building blocks of types. Each component represents a union of intersections (a DNF) of a particular "type constructor" (basic types such as integers or enums, tuples, arrows, …).

The following modules are convenience aliases to modules found in Ty.VDescr.Descr.

Basic components

These components represent the two basic types, integers and enums.

module Intervals : sig ... end

Integer components.

module Enums : sig ... end

Enums components.

Constructor components

Type constructor components come in two flavors: simple constructors such as arrows or records and families such as tuples or tagged type. The latter are infinte sets of components, indexed by a value (the arity for tuples and the tag for tagged types).

module Arrows : sig ... end

Arrow components.

module Records : sig ... end

Record components.

module Tuples : sig ... end

Tuple components.

module TupleComp : sig ... end

Component for a tuple of a particular fixed arity.

module Tags : sig ... end

Tagged types components.

module TagComp : sig ... end

Component for a type tagged with a particular tag.

Named identifiers

Identifiers (type variables, record fields) all share a common interface. The library provides sets and maps whose elements and keys are identifiers.

module type NamedIdentifier = sig ... end

module Label : sig ... end

Labels used for field names in records.

module LabelSet : sig ... end

Sets of labels.

module LabelMap : sig ... end

Maps indexed by labels.

module Var : sig ... end

Type variables.

module VarSet : sig ... end

Sets of type variables.

module VarMap : sig ... end

Maps indexed by type variables.

module Tag : sig ... end

Tags used for tagged type (an alias of TagComp.Atom.Tag).

Operations on types

module Subst : sig ... end

Type substitutions

module Op : sig ... end

High-level operations on types.

module Transform : sig ... end

Type transformation and simplification

module Tallying : sig ... end

Tallying (unification modulo subtyping constraints).

Pretty-printing of types

module Prec : sig ... end

Precedence of operators and associativity

module Printer : sig ... end

Extensions

This modules provides several common data-types, encoded as tagged type with a particular tag.

module Extensions : sig ... end