Node:CHR Pragmas, Next:, Previous:How CHR Work, Up:CHR Library


Pragmas are annotations to rules and constraints that enable the compiler to generate more specific, more optimized code. A pragma can be a conjunction of the following terms:

The intention of simplification and simpagation rules is often to combine the heads into a stronger version of one of them. Depending on the strength of the guard, the new constraint may be identical to one of the heads to removed by the rule. This removal followed by addition is inefficient and may even cause termination problems. If the pragma is used, this situation is detected and the corresponding problems are avoided. The pragma applies to all constraints removed by the rule.
Shares the intention of the previous pragma, but affects only the constraint indicated via Id. Note that one can use more than one pragma per rule.
No code will be generated for the specified constraint in the particular head position. This means that the constraint will not see the rule, it is passive in that rule. This changes the behavior of the CHR system, because normally, a rule can be entered starting from each head constraint. Usually this pragma will improve the efficiency of the constraint handler, but care has to be taken in order not to lose completeness.

For example, in the handler leq, any pair of constraints, say A leq B, B leq A, that matches the head X leq Y , Y leq X of the antisymmetry rule, will also match it when the constraints are exchanged, B leq A, A leq B. Therefore it is enough if a currently active constraint enters this rule in the first head only, the second head can be declared to be passive. Similarly for the idempotence rule. For this rule, it is more efficient to declare the first head passive, so that the currently active constraint will be removed when the rule fires (instead of removing the older constraint and redoing all the propagation with the currently active constraint). Note that the compiler itself detects the symmetry of the two head constraints in the simplification rule antisymmetry, thus it is automatically declared passive and the compiler outputs CHR eliminated code for head 2 in antisymmetry.

antisymmetry  X leq Y , Y leq X # Id <=> X=Y pragma passive(Id).
idempotence   X leq Y # Id \ X leq Y <=> true pragma passive(Id).
transitivity  X leq Y # Id , Y leq Z ==> X leq Z pragma passive(Id).
Declaring the first head of rule transitivity passive changes the behavior of the handler. It will propagate less depending on the order in which the constraints arrive:
| ?- X leq Y, Y leq Z.
X leq Y,
Y leq Z,
X leq Z

| ?- Y leq Z, X leq Y.
Y leq Z,
X leq Y

| ?- Y leq Z, X leq Y, Z leq X.
Y = X,
Z = X
The last query shows that the handler is still complete in the sense that all circular chains of leq-relations are collapsed into equalities.