Did you know ... | Search Documentation: |
CHR Constraint declaration |
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. Example:
:- chr_constraint get_value(+,?). :- chr_constraint domain(?int, +list(int)), alldifferent(?list(int)).
Modes
A mode is one of:
-
+
?
Types
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:
:- 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)).
Type Checking
Currently two complementary forms of type checking are performed:
Two kinds of type error are detected. The first is where a variable has to belong to two types. For example, in the program:
:-chr_type foo ---> foo. :-chr_type bar ---> bar. :-chr_constraint abc(?foo). :-chr_constraint def(?bar). foobar @ abc(X) <=> def(X).
the variable X
has to be of both type foo
and bar
. This is reported as a type clash error:
CHR compiler ERROR: `--> Type clash for variable _ in rule foobar: expected type foo in body goal def(_, _) expected type bar in head def(_, _)
The second kind of error is where a functor is used that does not belong to the declared type. For example in:
:- chr_type foo ---> foo. :- chr_type bar ---> bar. :- chr_constraint abc(?foo). foo @ abc(bar) <=> true.
bar
appears in the head of the rule where something of
type foo
is expected. This is reported as:
CHR compiler ERROR: `--> Invalid functor in head abc(bar) of rule foo: found `bar', expected type `foo'!
No runtime overhead is incurred in static type checking.
The kind of error detected by dynamic type checking is where a functor is used that does not belong to the declared type. For example, for the program:
:-chr_type foo ---> foo. :-chr_constraint abc(?foo).
we get the following error in an erroneous query:
?- abc(bar). ERROR: Type error: `foo' expected, found `bar' (CHR Runtime Type Error)
Dynamic type checking is weaker than static type checking in the sense that it only checks the particular program execution at hand rather than all possible executions. It is stronger in the sense that it tracks types throughout the whole program.
Note that it is enabled only in debug mode, as it incurs some (minor) runtime overhead.