module Dalton_aux: sig end
Auxiliary definitions
This module define several auxiliary datatypes that are useful for the
description of the ground algebra. They are also used internally by
the solver.
type 'a printer = Format.formatter -> 'a -> unit
Pretty-printing in the library is performed by the Format module.
Therefore a printer of values of type 'a may be viewed as a
function of type 'a printer.
type printing = Format.formatter -> unit
Similarly, the printing of some message on a formatter may be abstractly
represented by a function of type printing.
type color = int
For drawing purposes, a color is represented by a simple integer,
as in the Graphics module of the Objective Caml standard library.
type kind =
| |
Katom |
| |
Ktype |
| |
Krow of kind |
In the term algebra considered by the solver, terms may have one of
the following kinds:
Katom for atoms,Ktype for type,Krow k for rows whose elements have kind k.
module Kind: sig end
Basic operations on kinds are provided by the module Variance.
type variance =
| |
Covariant |
| |
Contravariant |
| |
Invariant |
A variance is one of the three elements Covariant, Contravariant
and Invariant.
module Variance: sig end
Basic operations on variances are provided by the module Variance.
type constructor_arg = {
|
variance : variance; |
(* | The variance of the argument. | *) |
|
kind : kind; |
(* | The kind of the argument. | *) |
|
ldestr : bool; |
(* | A boolean setting whether left destructor decomposes on this
argument. | *) |
|
rdestr : bool; |
(* | A boolean setting whether right destructor decomposes on this
argument. | *) |
}
Signatures of type constructors are specified by giving for each
argument a record of type constructor_arg.