Module Sstt.VDescr

Full descriptors with top-level variables.

Basics

type t

The type of descriptors with top-level variables (vdescr). It represents a union of intersections of positive and negative variables together with type descriptors of type Descr.t:

      v = \bigcup_{i=i\ldots n} ~~\bigcap_{j=1\ldots m} \alpha_{ij} \cap \bigcap_{j=1\ldots l} \lnot\beta_{ij} ~~\cap~~ d_i
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.

Descriptors

module Descr : sig ... end

Monomorphic type descriptors.

val mk_var : Var.t -> t

mk_var v builds a full descriptor from a given type variable.

val mk_descr : Descr.t -> t

mk_descr d creates a full descriptor from the monomorphic descriptor d.

val get_descr : t -> Descr.t

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

Explicit Disjunctive Normal Form

module Dnf : sig ... end

Explicit Disjunctive Normal Forms (DNF) of variables and monomorphic descriptors.

val dnf : t -> Dnf.t

Return an explicit DNF representation from a full descriptor.

val of_dnf : Dnf.t -> t

Builds a full descriptor from a DNF.

Misc. operations

val map : (Descr.t -> Descr.t) -> t -> t

map f t replaces every descriptor d in t by the descriptor f d.

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

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