Module `Cduce_types__Types`

Algebra

ℂDuce types can be built using to class of operation : type constructors (products, arrows, records, …) and type connectives (union, intersection, difference). Types must have two properties :

regularity: an infinite (co-inductive) type must have finite number of distinct subtrees.
contractivity: an infinite (co-inductive) type must crosse inifinitely many type constructors.

These invariants are enforced by the operations in this module.

type descr: The type of ℂDuce types, also aliased as t.

Basic operations on t. Note that equality here denotes the operation on the structural equality on the internal representation of t, not the semantic notion of equivalence between ℂDuce types.

include Custom.T with type t = descr

type t = descr

val dump : Stdlib.Format.formatter -> t -> unit
val check : t -> unit
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int

module Node : Custom.T

val make : unit -> Node.t: make () creates a fresh type reference, pointing to the empty type.

val define : Node.t -> t -> unit

define n t updates a reference to set its content to the given type. This can be used to define recursive types :

let nil = Types.atom (AtomSet.atom (AtomSet.V.mk_ascii "nil")) in
let x = Types.make () in
let prod = Types.times (Types.cons Types.Int.any) ilist
let ilist = Types.cup nil prod in
define x ilist;
(* use ilist or x, they represent the same recursive type [ [Int*] ] *)

val cons : t -> Node.t: const t wraps the type t in a reference

val id : Node.t -> int: id n returns the internal identifier of the reference.

val descr : Node.t -> t: descr n extract the type boxed in the reference n.

Boolean connectives

val empty : t: The empty type, 𝟘.

val any : t: The top type, 𝟙

val var : Cduce_types.Var.t -> t: var x creates the polymorphic variable x.

val cup : t -> t -> t: cup t1 t2 returns the union of t1 and t2

val cap : t -> t -> t: cap t1 t2 returns the intersection of t1 and t2

val diff : t -> t -> t: diff t1 t2 returns the difference of t1 and t2

val neg : t -> t: neg t returns the complement of t

Subtyping

Subtyping operations should only be called on fully defined types (that is, not on a recursive type whose cycles haven't yet been closed with define).

val is_empty : t -> bool: is_empty t returns true if and only if t is empty.

val non_empty : t -> bool: non_empty t returns true if and only if t is non empty empty. This is just a convenience function for not(is_empty t).

val subtype : t -> t -> bool: subtype t1 t2 returns true if and only if t1 is a subtype of t2. This is an alias for is_empty (diff t2 t1).

val disjoint : t -> t -> bool: disjoint t1 t2 returns true if and only if t1 and t2 have an empty intersection. This is an alias for is_empty (cap t1 t2).

val equiv : t -> t -> bool: equiv t1 t2 returns true if and only if t1 and t2 are semantically equal. This is an alias for subtype t1 t2 && subtype t2 t1.

Components of a type

A type in ℂDuce is a finite union of disjoint kinds :

Integers
Atoms
Characters
Abstract types
Products
XML products
Arrows
Records
Absent type (representing optional record fields.)

The following modules allow one to project a particular component of a type, retrieve its dijunctive normal form (DNF) and conversely create a ℂDuce type from such a DNF. These modules also define the top type of each kind.

module type Kind = sig ... end: The components of a type

Integers

module Int : Kind with module Dnf = Cduce_types__.Bdd.VarIntervals: access the integer component of a type

val interval : Cduce_types.Intervals.t -> t: interval i creates a type from an interval i.

Atoms

module Atom : Kind with module Dnf = Cduce_types__.Bdd.VarAtomSet: Access the atom component of a type

val atom : Cduce_types.AtomSet.t -> t: atom a creates a type from an AtomSet.t.

Characters

module Char : Kind with module Dnf = Cduce_types__.Bdd.VarCharSet: Access the char component of a type.

val char : Cduce_types.CharSet.t -> t

Abstract types

module Abstract : Kind with module Dnf = Cduce_types__.Bdd.VarAbstractSet: Access the abstract component of a type.

val abstract : Cduce_types.AbstractSet.t -> t: abstract a creates a type from an AbstractSet.t.

val get_abstract : t -> Cduce_types.AbstractSet.t: get_abstract a is an alias for Abstract.get a.

Products

module Times : Kind with type Dnf.atom = Node.t * Node.t and type Dnf.line = (Node.t * Node.t) Cduce_types__.Bdd.line and type Dnf.dnf = (Node.t * Node.t) Cduce_types__.Bdd.dnf: Access the product component of a type.

val times : Node.t -> Node.t -> t: times n1 n2 is an alias for Times.mk (Times.Dnf.atom (n1, n2)).

val tuple : Node.t list -> t

tuple nl creates right nested tuples from the elements in nl. tuple [t1; t2; t3; … ; tn] returns the type (t1, (t2, (t3, … (tn-1,tn))))

raises Failure: if nl is not at least of length 2.

XML products

module Xml : Kind with type Dnf.atom = Node.t * Node.t and type Dnf.t = Times.Dnf.t and type Dnf.line = Times.Dnf.line and type Dnf.dnf = Times.Dnf.dnf: Access the XML component of a type. Note that Xml.any is different from the AnyXml type of ℂDuce, which is a recursive type X where X = <_ ..>[(X|Char)*]

val xml : Node.t -> Node.t -> t: xml n1 n2 is an alias for Xml.mk (Xml.Dnf.atom (n1, n2)). Although this constructor can be freely called, it is expected that n1 is a subtype of Atom and n2 a subtype of ({ ..}, [Any*]), to represent the type of XML documents.

Records

module Rec : Kind with type Dnf.atom = bool * Node.t Cduce_types.Ident.label_map and type Dnf.line = (bool * Node.t Cduce_types.Ident.label_map) Cduce_types__.Bdd.line and type Dnf.dnf = (bool * Node.t Cduce_types.Ident.label_map) Cduce_types__.Bdd.dnf

val record_fields : (bool * Node.t Cduce_types.Ident.label_map) -> t

record_fiels (b, lm) is an alias for Rec.mk (Rec.Dnf.atom (b, lm)). If b is true the resulting record type is open, otherwise it is closed. See Ident.LabelMap to build the lm argument.

Example :

open Types
let int = Int.any in 
let int_opt = cup int Absent.any in
let lab = Ident.Label.mk_ascii "mylabel" in
let lm = Ident.LabelMap.singleton lab int_opt in
let r = record_fields (true, lm) in
(* r is the record { mylabel=?Int ..} *)

val record : Cduce_types.Ident.label -> Node.t -> t: record l n creates an open record type with a single explicit label l.

val rec_of_list : bool -> (bool * Cduce_types.Ident.label * t) list -> t

rec_of_list op fields creates a record type. If op is true the record is open otherwise it is closed. The fields argument is a list of triples (opt, lab, t). The boolean opt indicate whether the field is optionnal (when opt = true) (thus the type t given for a field is expected to not be absent already).

raises [Failure]: if fields contains duplicate labels.

val empty_closed_record : t: The type {} , that is a closed record with no fields.

val empty_open_record : t: The type { ..}, that is an opened record with no explicit fields. This is an alias for Rec.any.

Arrows

module Function : Kind with type Dnf.atom = Node.t * Node.t and type Dnf.t = Times.Dnf.t and type Dnf.line = Times.Dnf.line and type Dnf.dnf = Times.Dnf.dnf: Access the arrow component of a type.

val arrow : Node.t -> Node.t -> t: arrow n1 n2 is an alias for Function.mk (Function.Dnf.atom (n1, n2)).

Absent types

Absent types represent the type of optional fields. They are represented by a kind that only has two values empty ≡ false and any ≡ true.

It is the programmer's responsibility to prevent optional absent types from appearing outside of record fields.

module Absent : sig ... end: Access the absent component of a type.

type const = | Integer of Cduce_types.Intervals.V.t | Atom of Cduce_types.AtomSet.V.t | Char of Cduce_types.CharSet.V.t | Pair of const * const | Xml of const * const | Record of const Cduce_types.Ident.label_map | String of Encodings.Utf8.uindex * Encodings.Utf8.uindex * Encodings.Utf8.t * const: An auxiliary type to denote syntactic constants and build singleton types from its values.

module Const : Custom.T with type t = const: The const type equiped with basic operations.

val constant : const -> t: constant c returns a (singleton) type built from the constant description c.

type pair_kind = [ | `Normal | `XML ]

Normalization

Type constructors may yield equivalent types that are not structurally equal. For instance, the type t = (A, B) | (A, C) may also be represented as t = (A, B|C). In general, given a union of products, its decomposition is not unique.

The following modules allow one to compute various normalized forms for the product, XML, record and arrow type constructor.

These modules also provide the typing for high level operations such as first and second projection for products, field projection and concatenation for records and function application.

module Product : sig ... end: Product normalization.

module Record : sig ... end: Record normalization.

module Arrow : sig ... end: Arrow normalization.

val non_constructed : t: Utilities
A type that is a union of all basic types, that is, neither a product, arrow, XML or record type.

val print_witness : Stdlib.Format.formatter -> t -> unit

print_witness fmt t prints a witness for the non empty type t to the given formatter. A witness is a in most case a constant representing an inhabitant of the type, except for arrows and abstract types for which a generic type name is used.

raises Not_found: if t is the empty type.

module Cache : sig ... end: A semantic cache indexed by types. Semantic equivalence is used to check whether a type is present in the cache.

Utilities