Module Sstt.Records

Record components.

type t

Record types is a union of intersection of positive and negative records:

        \bigcup_{i=1\ldots m} \bigcap_{j=1 \ldots p} \texttt{\{}l_{j}{^1}:o_{j}^1,\ldots,l_{j}^k:o_{j}^{k} ~~ b_j\texttt{\}} \cap
        \bigcap_{j=1 \ldots n} \lnot(\{l_{j}{^1}:o_{j}^1,\ldots,l_{j}^l:o_{j}^{l} ~~ b_j\})

with b_j \in \{\texttt{..},~ \epsilon\}.

Basics

The minimal signature of a component.

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.

Explicit DNF, construction and extraction

val dnf : t -> Dnf.t

dnf t returns a disjunctive normal form of t.

val of_dnf : Dnf.t -> t

dnf d builds a component from a disjunctive normal form d.

val mk : Atom.t -> t

Creates a component from an atom.

val map_nodes : (Ty.t -> Ty.t) -> t -> t

map_nodes f t replaces every node n in t by the node f n.

Records have a condensed representation where each record atom requires the existence of extra labels. For instance, given the (closed) record

      \texttt{\{} x:t, y:s \texttt{\}}

its negation can be written as a union of positive condensed atoms:

      \texttt{\{} x:\lnot t, \texttt{.. \}}\cup
      \texttt{\{} y:\lnot s, \texttt{.. \}}\cup
      \texttt{\{} x:t, y:s, \overline{\{x, y\}}~\texttt{.. \}}

meaning any record which has label x associated to a type that is not t, or any record which has label y associated to a type that is not s, or any record which has both labels associated to their original type but which also has an extra label that is neither x nor y.

Condensed DNF

The abstract module representing condensed atoms.

Explicit DNF over condensed atoms.

val dnf' : t -> Dnf'.t

dnf t returns the condensed DNF of t.

val of_dnf' : Dnf'.t -> t

of_dnf' d builds a component from an condensed DNF d.