module Make: functor (Ground : Dalton_sig.GROUND) >
functor (Print : Dalton_sig.PRINT) >
functor (Draw : Dalton_sig.DRAW) >
functor (Report : Dalton_sig.ERROR_REPORT) > sig end
The constraint solver comes as a functor parametrized by four modules
whose respective expected signatures are given in
Dalton_sig
.
type cset
Constraint sets are represented by values of type cset
.
val cset : unit > cset
Each invokation of cset ()
returns a new fresh empty constraint
set.
val merge_cset : cset > cset > unit
merge_cset cs1 cs2
merges the two constraint sets cs1
and cs2
.
After invoking this function, cs1
and cs2
point to the same
constraint set cs
which corresponds to the conjunction of the
previous cs1
and cs2
.
type node
(Multiequations of) Terms are represented by values of type node
.
val variable : cset > Dalton_aux.kind > node
variable cs k
returns a fresh variable term of kind k
. This
variable may be used in the constraint set cs
.
val variable_in_sk : node > node
variable_in_sk nd
returns a fresh variable belonging to the same
skeleton (and the same constraint set) as the node nd
.
val typ : cset > node Ground.Type.t > node
typ cs t
returns a fresh type term described by the type constructor
t
in the constraint set cs
. Every son of t
must be a node
belonging to cs
.
val row : cset >
Ground.Label.t * node * node > node
row cs (lbl, nd_lbl, nd')
returns a fresh row node representing
the term lbl: nd_lbl, nd'
in the constraint set cs
. nd_lbl
and
nd'
must both belong to cs
.
type skeleton
Multiskeletons are represented by values of type skeleton
.
type node_or_skeleton =
A value of type node_or_skeleton
is either a node or a
skeleton. Such values are used to represent weak inequalities.
type unification_report
Unification errors are described by a value of type
unification_report
. The implementation of this type is not
described. As a result, reports may be used only in order to
print error messages thanks to the function report_unification
.
exception UnificationError of unification_report
Above functions report unification errors by raising an
exception UnificationError
with an appropriate report as
argument.
val report_unification : Format.formatter > unification_report > unit
report_unification ppf r
pretty prints an error message on the
formatter ppf
describing the unification error reported by r
.
val same_skel : node > node > unit
same_skel nd1 nd2
sets a constraint nd1 ~ nd2
. nd1
and nd2
must be nodes of the same constraint set and the same kind. If
setting this constrain entails an unification error, an exception
UnificationError
is raised.
val equal : node > node > unit
equal nd1 nd2
sets a constraint nd1 = nd2
. nd1
and nd2
must be nodes of the same constraint set and the same kind. If
setting this constrain entails an unification error, an exception
UnificationError
is raised.
val strong_leq : node > node > unit
strong_leq nd1 nd2
sets the strong inequality ns1 < ns2
. nd1
and nd2
must be nodes of the same constraint set and the same kind.
If setting this constrain entails an unification error, an exception
UnificationError
is raised.
val weak_leq : node_or_skeleton > node_or_skeleton > unit
weak_leq ns1 ns2
sets a weak inequality ns1 < ns2
. ns1
and
ns2
must be nodes or skeletons of the same constraint set.
val lower_bound : Ground.Lb.t > node_or_skeleton > unit
lower_bound lb ns
sets the weak inequality lb < ns
.
val upper_bound : node_or_skeleton > Ground.Ub.t > unit
upper_bound ns ub
sets the weak inequality ns < ub
.
type subst = {

lb : Ground.Lb.t > Ground.Lb.t ; 
(*  The substitution applied on lower bounds appearing in
the constraint set.  *) 

ub : Ground.Ub.t > Ground.Ub.t ; 
(*  The substitution applied on upper bounds appearing in
the constraint set.  *) 

typ : 'a. 'a Ground.Type.t > 'a Ground.Type.t ; 
(*  The substitution applied on type constructors.  *) 

label : Ground.Label.t > Ground.Label.t ; 
(*  The substitution applied on row labels.  *) 
}
A substitution may be applied while copying a scheme. It is defined
by a record of four functions of type subst
.
module type SCHEME_ROOT = sig end
A (type) scheme is made of a constraint set and a series of entry
nodes, its roots.
module Scheme: functor (Root : SCHEME_ROOT) > sig end
The functor scheme allows to build an implementation of functions
dealing which each considered form schemes.