Module Constraint (.ml)

module Constraint: sig .. end

This module manages a data structure for constraint in a multi-equation framework.

type sname =

`\|`	`SName of string`

sname is the type of the names that are used to refer to type schemes inside constraints. These names are bound by CLet constraints and referred to by CInstance constraints.

type ('crterm, 'variable) type_constraint =

`\|`	`CTrue of Positions.position`
`\|`	`CDump of Positions.position`
`\|`	`CEquation of Positions.position * 'crterm * 'crterm`
`\|`	`CConjunction of ('crterm, 'variable) type_constraint list`
`\|`	`CLet of ('crterm, 'variable) scheme list * ('crterm, 'variable) type_constraint`
`\|`	`CInstance of Positions.position * sname * 'crterm`
`\|`	`CDisjunction of ('crterm, 'variable) type_constraint list`

type_constraint defines a syntax for the constraints between types.

type ('crterm, 'variable) scheme =

`\|`	`Scheme of Positions.position * 'variable list * 'variable list * ('crterm, 'variable) type_constraint * ('crterm * Positions.position) Misc.StringMap.t`

A type scheme is a pair of a constraint c and a header h, wrapped within two sets of universal quantifiers rqs and fqs. The former are considered rigid, while the latter are considered flexible. More precisely, for the type scheme to be considered consistent, the constraint forall rqs.exists fqs.c must hold. Rigid and flexible quantifiers otherwise play the same role, that is, they all end up universally quantified in the type scheme. A header is a mapping of names to types.

type variable = MultiEquation.variable

The variables that appear in contraints are the same as the multi-equation ones.

type crterm = variable CoreAlgebra.arterm

The types in contraints are implemented using the internal data structure defined in CoreAlgebra. The same data structure is also used in MultiEquation.

type tconstraint = (crterm, variable) type_constraint

Here is an abbreviation for the type constraint structure instantiated using our internal variable and term representations.

type tscheme = (crterm, variable) scheme

Here is an abbreviation for the type scheme structure instantiated using out internal variable and term representations.

val cposition : ('a, 'b) type_constraint -> Positions.position

cposition c returns the position related to c.

val (=?=) : crterm ->
       crterm -> Positions.position -> tconstraint

t1 =?= t2 is an equality constraint

val ex : ?pos:Positions.position ->
       variable list -> tconstraint -> tconstraint

ex qs c returns the constraint exists qs.c. We encode existential constraints in terms of let constraints, since the latter are more general.

val fl : ?pos:Positions.position ->
       variable list -> tconstraint -> tconstraint

fl qs c returns the constraint forall qs.c. We encode universal constraints in terms of let constraints, since the latter are more general.

val (<?) : sname ->
       crterm -> Positions.position -> tconstraint

x <? t is a conjunction constraint.

val (^) : tconstraint -> tconstraint -> tconstraint

c1 ^ c2 is a conjunction constraint.

val conj : tconstraint list -> tconstraint

conj cs builds a conjunction between a list of constraints.

val exists : ?pos:Positions.position ->
       (crterm -> tconstraint) -> tconstraint

exists f creates a fresh variable x and returns the constraint exists x.(f x).

val exists3 : ?pos:Positions.position ->
       (crterm ->
        crterm -> crterm -> tconstraint) ->
       tconstraint

exists3 f is a shortcut for exists (fun x -> exists (fun y -> exists (fun z -> f x y z))).

val fl : ?pos:Positions.position ->
       variable list -> tconstraint -> tconstraint

fl vs c returns the constraint forall vs.c.

val exists_list : ?pos:Positions.position ->
       'a list ->
       (('a * crterm) list -> tconstraint) ->
       tconstraint

exists_list l f associates a fresh variable with every element in the list l, yielding an association list m, and returns the constraint exists m.(f m).

val forall_list : ?pos:Positions.position ->
       MultiEquation.tname list ->
       ((MultiEquation.tname * crterm) list -> tconstraint) ->
       tconstraint

forall_list l f associates a fresh variable with every element in the list l, yielding an association list m, and returns the constraint forall m.(f m).

val exists_set : ?pos:Positions.position ->
       Misc.StringSet.t ->
       ((crterm * Positions.position) Misc.StringMap.t ->
        tconstraint) ->
       tconstraint

exists_set names f associates a fresh variable with every name in the set names, yielding a map m of names to variables, and returns the constraint exists m.(f m).

val monoscheme : ?pos:Positions.position ->
       (crterm * Positions.position) Misc.StringMap.t ->
       tscheme

monoscheme header turns header into a monomorphic type scheme.

val scheme : ?pos:Positions.position ->
       variable list ->
       Misc.StringSet.t ->
       ((crterm * Positions.position) Misc.StringMap.t ->
        tconstraint) ->
       tscheme

scheme rqs names f associates a fresh variable with every name in the set names, yielding a map m of names to variables, and returns the type scheme forall rqs m [f m] m, where the variables in rqs are rigid and the variables in m are flexible.

val scheme' : ?pos:Positions.position ->
       variable list ->
       Misc.StringSet.t ->
       Misc.StringSet.t ->
       ((crterm * Positions.position) Misc.StringMap.t ->
        tconstraint) ->
       tscheme

scheme' rqs rnames fnames f associates a fresh variable with every name in the set fnames and rnames, yielding a map m of names to variables, and returns the type scheme forall (rqs @ rm) fm [f m] m, where the variables in rqs and rm are rigid and the variables in fm are flexible.