Constraint handling rules

A goal can be suspended instead of solved: it becomes a constraint, and sits in the constraint store until it is woken up. Constraint handling rules (CHR) look at that store as a whole, and can drop constraints from it and spawn new goals. The syntax has three parts: the constraint block, the rules inside it, and the declare_constraint builtin that puts a goal in the store. How the store then evolves and how rules fire is covered in The constraint store.

The constraint block

A constraint block names a clique of predicates and holds the rules that act on their constraints:

constraint even odd {
  rule (even X) (odd X) <=> false.
}

The rule keyword may appear only inside such a block. The cliques of a program must be pairwise disjoint.

A resumed constraint carries a context with it: the hypothetical rules that were in force when it was suspended (see Sequent patterns below). By default that context is trimmed to the rules of the constraint’s own clique. An optional context filter, written before ?-, names further predicates whose rules are kept as well:

constraint ctx ?- infer {
  % rules for `infer`; a resumed `infer` constraint also keeps
  % the rules it accumulated for `ctx`
}

The ?- is omitted when the filter is empty, as in the even odd block above.

Rules

A rule has four parts. Only the rule keyword itself is required; each of the others may be left out:

rule  TO-MATCH  \ TO-REMOVE  | GUARD  <=> NEW-GOAL .

TO-MATCH and TO-REMOVE are sequences of sequent patterns, matched against the constraints in the store. A constraint matched on the left of the \ stays in the store; one matched on its right is taken out. With no \ at all, nothing is removed, and the rule fires at most once for each ordering of the constraints it matches, so a rule that only adds goals does not loop. A two-pattern rule with two matching constraints in the store therefore fires twice, once per ordering of the pair, not once; The constraint store works this through.

GUARD, after the |, is a goal that must succeed for the rule to fire. Once it does, the choice is committed: no later rule is tried on the same constraints.

NEW-GOAL, after the <=>, is a sequent (see below) that is run as a fresh goal when the rule fires.

So rule (even X) (odd X) <=> false runs the goal false, which fails, whenever the store holds both even X and odd X for one X; because a rule that has fired is not reconsidered, that failure is final. A rule may be preceded by :name "…" (naming it for trace output) and :if "…" (Rule attributes).

Sequent patterns

Elpi manages a context for every goal: the eigenvariables introduced by pi and the hypothetical rules introduced by ==>. A suspended goal therefore is not a bare predicate but a sequent, Eigen ▷ Context ⊢ Goal, and a sequent pattern chooses how much of that to match:

  • Goal matches only the goal, ignoring the eigenvariables and hypotheses the constraint carried;

  • (Context ?- Goal) also matches the hypotheses. Context is the list of rules added by implication before the constraint was suspended, ordered most-recently-added first, so its head is the highest-priority rule. It holds only the rules for the predicates the context filter admits: the clique’s own, plus any named before ?- in the constraint block;

  • (Eigen :> Context ?- Goal) also matches Eigen, the list of eigenvariables (the pi-introduced constants) the constraint lives under.

Context and Eigen are ordinary patterns: they may be _, a variable, or a list pattern, and any variable they bind is in scope in the guard and in the new goal.

Every unification variable inside a matched constraint is frozen: replaced by a fresh constant that the rule cannot assign. Freezing is what makes a rule match the store rather than unify with it: the non-linear K in the rule below does not merge two unrelated constraints, it only fires when two constraints really are about the same variable. A frozen variable is shown to the rule through the uvar head pattern (Unification and variables) as uvar K L, where K identifies it and L is the list of bound variables in its scope; two uvar K … with the same K are the same variable.

When holes never appear under a binder, the “a hole has one type” rule needs no context at all: keep the first typing, unify the second with it.

constraint infer {
  rule (infer (uvar K _) T1)
     \ (infer (uvar K _) T2)
     <=> (T1 = T2).
}

Once holes can occur under binders, the same hole shows up in different contexts, and the two types live in different scopes. Each matched constraint is frozen into its own space of names (the Eigen lists of two matched sequents are disjoint), so the rule must relate the terms across them itself, in the guard, before it can compare them. This is the rule coq-elpi’s elaborator actually uses for uniqueness of typing:

constraint declare-evar evar decl def cache rm-evar {
  rule (E1 :> G1 ?- evar _ T1 (uvar K L1))         % K's declared type, in scope L1
     \ (E2 :> G2 ?- evar _ T2 (uvar K L2))         % a use of K, in scope L2
     | (canonical? L1, utc L1 T1 L2 T2 Condition)  % relocate T1 into L2's scope,
                                                   % producing a goal `Condition`
    <=> (E2 :> G2 ?- Condition).                   % run it under the using
}                                                  % sequent's eigenvars and hypotheses

The guard utc (“uniqueness of typing”) walks L1 and L2 in step, substituting the canonical eigenvariables for the ones actually supplied, and hands back Condition, the goal that checks the two relocated types agree. <=> (E2 :> G2 ?- Condition) then runs that goal back inside the second sequent’s context, where its eigenvariables and hypotheses are in scope again. The full treatment, for a type theory where terms occur in types, is given by Guidi, Sacerdoti Coen & Tassi; see also The constraint store.

Generating a constraint

declare_constraint turns a goal into a constraint and puts it in the store. The goal must be a function: it needs a func signature (Type declarations), and a relational predicate is rejected. The constraint is suspended on one or more keys, each of which must be a unification variable (or _):

declare_constraint (even X) [X]

The constraint sits in the store until one of its keys is assigned, and then runs as an ordinary goal again. A key given as _, and a constraint keyed on the empty list, are never resumed. Several keys may be passed as one list, [X, Y], or as separate arguments.

Every unification variable that occurs in the constraint should be among the keys; an assignment to one that is left out will not wake the constraint. Elpi does not check this yet (issue #441).

The usual idiom is a rule that fires while the interesting argument is still a variable, matched with the uvar pattern (Unification and variables), and suspends the goal on it:

func even int.
even (uvar as X) :- !, declare_constraint (even X) [X].
even 0 :- !.
even N :- N > 0, !, M is N - 2, even M.

At the top-level prompt a leftover constraint is printed after the solution; print_constraints prints the store at any point:

goal> declare_constraint (even X) [X].
Success:
  X = X0
Constraints:
 even X0  /* suspended on X0 */

goal> declare_constraint (even X) [X], X = 1.
Failure

A larger program using every part of the syntax above is Euclid’s GCD, with each gcd fact reduced against the others in its group until one number is left:

../code/chr.elpi:

 1% Euclid's GCD as constraint handling rules. Each `gcd N G` fact says "N is one
 2% of the numbers of group G"; the rules keep reducing the store until a single
 3% number per group is left — its GCD.
 4
 5data group.
 6symb group-1, group-2 group.
 7
 8func gcd int, group.
 9
10% suspend until the group is known
11gcd A (uvar as G) :- !, declare_constraint (gcd A G) [G].
12
13% once resumed on a concrete group, report the surviving number
14gcd X group-1 :- print "group 1 GCD is" X.
15gcd X group-2 :- print "group 2 GCD is" X.
16
17constraint gcd {
18  % drop a duplicate number
19  rule (gcd A _) \ (gcd B _) | (A = B).
20  % replace the larger number by the difference
21  rule (gcd A _) \ (gcd B G) | (A < B) <=> (C is B - A, gcd C G).
22}
23
24main :-
25  gcd 99 X, gcd 66 X, gcd 22 X,      % group X = { 99, 66, 22 }
26  gcd 14 Y, gcd 77 Y,                % group Y = { 14, 77 }
27  X = group-1, Y = group-2.          % force resumption

group 1 GCD is 11
group 2 GCD is 7