Functor Dalton.Make

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.

Parameters:

`Ground`	:	`Dalton_sig.GROUND`
`Print`	:	`Dalton_sig.PRINT`
`Draw`	:	`Dalton_sig.DRAW`
`Report`	:	`Dalton_sig.ERROR_REPORT`

Constraint sets

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.

Terms

type node

(Multi-equations 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.

Setting constraints

type skeleton

Multi-skeletons are represented by values of type skeleton.

type node_or_skeleton =

`\|`	`Nd of node`
`\|`	`Sk of 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.

Substitutions

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.

Schemes

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.