10.34.3.2 Constraint Declaration

Every constraint used in CHR rules has to be declared with a chr_constraint/1 declaration by the constraint specifier. For convenience multiple constraints may be declared at once with the same chr_constraint/1 declaration followed by a comma-separated list of constraint specifiers.

A constraint specifier is, in its compact form, F/A where F and A are respectively the functor name and arity of the constraint, e.g.

     :- chr_constraint foo/1.
     :- chr_constraint bar/2, baz/3.

In its extended form, a constraint specifier is c(A_1,...,A_n) where c is the constraint's functor, n its arity and the A_i are argument specifiers. An argument specifier is a mode, optionally followed by a type. E.g.

     :- chr_constraint get_value(+,?).
     :- chr_constraint domain(?int,+list(int)),
                        alldifferent(?list(int)).

A mode is one of the following:

-

The corresponding argument of every occurrence of the constraint is always unbound.

+

The corresponding argument of every occurrence of the constraint is always ground.

?

The corresponding argument of every occurrence of the constraint can have any instantiation, which may change over time. This is the default value.

A type can be a user-defined type or one of the built-in types. A type comprises a (possibly infinite) set of values. The type declaration for a constraint argument means that for every instance of that constraint the corresponding argument is only ever bound to values in that set. It does not state that the argument necessarily has to be bound to a value.

The built-in types are:

int

The corresponding argument of every occurrence of the constraint is an integer.

float

... a floating point number.

number

... a number.

natural

... a positive integer.

any

The corresponding argument of every occurrence of the constraint can have any type. This is the default value.

User-defined types are algebraic data types, similar to those in Haskell or the discriminated unions in Mercury. An algebraic data type is defined using

     :- chr_type type ---> body.

If the type term is a functor of arity zero (i.e. one having zero arguments), it names a monomorphic type. Otherwise, it names a polymorphic type; the arguments of the functor must be distinct type variables. The body term is defined as a sequence of constructor definitions separated by semi-colons.

Each constructor definition must be a functor whose arguments (if any) are types. Discriminated union definitions must be transparent: all type variables occurring in the body must also occur in the type.

Here are some examples of algebraic data type definitions:

     :- chr_type color ---> red ; blue ; yellow ; green.
     :- chr_type tree --->  empty ; leaf(int) ; branch(tree, tree).
     :- chr_type list(T) --->    [] ; [T | list(T)].
     :- chr_type pair(T1, T2) ---> (T1 - T2).

Each algebraic data type definition introduces a distinct type. Two algebraic data types that have the same bodies are considered to be distinct types (name equivalence).

Constructors may be overloaded among different types: there may be any number of constructors with a given name and arity, so long as they all have different types.

Aliases can be defined using ‘==’. For example, if your program uses lists of lists of integers, you can define an alias as follows:

     :- chr_type lli == list(list(int)).