Module Sstt.Arrows

Arrow components.

type t

A function type is union of intersection of positive and negative arrows:

      \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)

Atoms are single arrows denote by its domain and codomain.

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.