Module Sstt.TupleComp

Component for a tuple of a particular fixed arity.

type t

The component of n-tuples is a union of intersections of positive and negative n-tuples.

An atom for a tuple of arity n si simply an (orederd) list of n nodes.

Basics

The minimal signature of a component.

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 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.

Operations for indexed components

Operations on components that are indexed by a type, such as tuples (indexed by integers) or tagged types (indexed by a symbolic tag).

val any : int -> t

The top element for the given index.

val empty : int -> t

The bottom element for the given index.

val of_dnf : int -> Dnf.t -> t

of_dnf idx d builds a component for the given index and DNF.

val len : t -> int

len t returns the common arity of all tuple types in t.

Condensed DNF

Tuples commute with intersection, so a union of intersection of tuples can be compactly represented as a union of products.

Explicit DNF over condensed atoms.

val dnf' : t -> Dnf'.t

dnf t returns the condensed DNF of t.

val of_dnf' : int -> Dnf'.t -> t

of_dnf' idx d builds a component for the given index and optimized DNF.