Spilling

A rule that threads a value from one call straight into the next has to name that value, and a name like Tmp or Aux1 carries no information: it is there only to plumb the two calls together. Spilling removes the name. { E } (Terms) lifts the goal E out to just before the smallest enclosing predicate call and puts a fresh variable in its place, one for each argument E is not given (its output arguments, so one in the common case):

f X R :- foo X Y, bar Y R.      % written out, with the plumbing variable Y
f X R :- bar {foo X} R.         % the same, spilled

If E has several missing arguments, { E } becomes that many variables at once:

g X R :- h X Y Z, k Y Z R.      % h has two outputs
g X R :- k {h X} R.             % {h X} stands for the two of them, Y and Z

For this to work Elpi has to know the spilled predicate’s arity, from its pred / func signature (Type declarations); an undeclared predicate cannot be spilled.

The spilled call is inserted just before the closest call recognised as a predicate, which today means a monomorphic, first-order signature; a polymorphic or higher-order argument position (as in an anonymous predicate passed to std.map) may place it one level up if the callee’s own type isn’t precise enough to pin it down. elpi -print FILE prints a program after spilling (and other compilation passes), so any doubt about where a particular { } ended up can be checked directly.

Here {std.rev L} becomes a fresh variable produced by an std.rev goal inserted right before std.append:

../code/palindrome.elpi:

% Example used in the "Spilling" chapter.
% The spilled call {std.rev L} is rewritten to a fresh variable bound by an
% std.rev goal inserted just before std.append.

pred make-palindrome list A -> list A.
make-palindrome L Result :- std.append L {std.rev L} Result.

main :- make-palindrome [1, 2, 3] R, print R.

[1, 2, 3, 3, 2, 1]

Spilling into a binder

Under pi and in the conclusion of ==>, the spilled goal is placed inside the binder, so its fresh variable can still mention the names and hypotheses in scope there. A pretty-printer that recurses under lam spills {pp (F x)} right where the fresh x and its pp x "x" hypothesis are visible:

../code/spilling-under-binder.elpi:

% Spilling reaches into a binder: in the `lam` rule, `{pp (F x)}` is lifted
% to a `pp (F x) R` goal placed *inside* the `pi x\ ... ==>`, so it can use the
% fresh `x` and the `pp x "x"` hypothesis. The `app` rule spills twice in one
% `is`, both lifted before the enclosing call.

data tm.
symb app tm -> tm -> tm.
symb lam (tm -> tm) -> tm.

func pp tm -> string.
pp (app F X) S :- S is "(" ^ {pp F} ^ " " ^ {pp X} ^ ")".
pp (lam F) S :- pi x\ pp x "x" ==> S is "\\x." ^ {pp (F x)}.

main :- pp (lam f\ app f f) S, print S.

\x.(x x)

elpi -print FILE shows where the spilled goal landed: in the lam rule it sits after the ==>, inside the pi and under its own sigma, equivalent to writing

pp (lam F) S :- pi x\ pp x "x" ==> sigma R\ (pp (F x) R, S is "\x." ^ R).

Only the conclusion of an implication may spill. A { } in the hypothesis is rejected at compile time (Spilling in negative position is forbidden), since the lifted goal would have to run before the hypothesis it depends on is in scope.

Spilling out of a term-level lambda

A { } inside a lambda that is passed as data, not the body of a pi or an implication, goes the other way: the goal is lifted out past the lambda and the fresh variable is η-expanded so it can still depend on the bound name. apply (x\ {f x}) becomes

main :- apply (x\ {f x}).
% becomes
main :- pi c\ f c (R c), apply (x\ R x).

The spilled f c runs once, before apply, with c a fresh constant. This is only meaningful when f does not actually need c’s value; a { } under a term-level lambda that genuinely depends on the bound variable is usually a mistake.

Spilling a conjunction

When { } wraps a conjunction, only its last conjunct is spilled, and that conjunct’s missing output is what becomes the fresh variable. The earlier conjuncts run in place, typically to bind a variable the last one then reads:

foo :- pi x\ f {g x Y, h Y}.
% becomes
foo :- pi x\ sigma S\ (g x Y, h Y S), f S.

g x Y runs first and binds Y; h Y is the spilled conjunct, so h Y S computes the value S that takes the place of the whole { … }.