Spilling and functional syntax

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 need for that name.

pred f int -> int.
f X R :- foo X Tmp, bar Tmp R.  % the plumbing variable Tmp

Wrapping a partially-applied call in braces, { 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 :- bar {foo X} R.         % the same, spilled

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

pred h int -> int, int.
g X R :- h X Tmp1 Tmp2, k Tmp1 Tmp2 R.   % h has two outputs: Tmp1 Tmp2
g X R :- k {h X} R.                      % {h X} stands for the two of them

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, walking backward, inside out. 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 in the head of a rule

{ } may also appear in a rule’s head even though a head is not a goal sequence and cannot simply join a , conjunction the way a spill in the body can. The spilled goal is relocated to just after :-, in front of whatever body the rule already had;:

func copy tm -> tm.
copy (app A B) (app {copy A} {copy B}).
% becomes
copy (app A B) (app R S) :- copy A R, copy B S.

Spilling in the head is restricted to an output argument.

Spilling without { }

{ } marks explicitly which under-applied call to spill. The :autospill rule attribute (Rule attributes) spills every under-applied call in the rule instead, wherever it appears, exactly as if each had its own { }:

:autospill
main :- std.append (std.append [1] [2]) [3] L, L = [1,2,3].

A call is spilled automatically when it is applied to all of its input arguments but none of its outputs arguments. A call that already supplies every argument, outputs included, is left untouched – and so is a call already surrounded by { }, even though it too supplies all its inputs and no outputs.

The :autospill attribute is turned on automatically by the functional rule syntax (Inference rules and queries) — a rule head written with -> to separate inputs from outputs. A recursive call is the typical beneficiary, since its own result is exactly the value still missing from it: below, map F XS stands for its own missing output:

../code/autospill-map.elpi:

func map (func A -> B), list A -> list B.
map _ [] -> [].
map F [X|XS] -> [F X|map F XS].

This is the same predicate as the version written out with every argument in place and an ordinary body:

../code/map.elpi:

func map (func A -> B), list A -> list B.
map _ [] [].
map F [X|XS] [Y|YS] :- F X Y, map F XS YS.

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).

{ } may spill in the premise (the hypothesis) of ==> too. Spilling in the premise is handled the same way as spilling in a rule’s own head (above) and the premise becomes a rule with premises of its own and the fresh variable used for spilling is quantified with pi around the entire premise:

main :- p {succ 1} ==> p X, print X.

is elaborated to:

main :- (pi R\ p R :- succ 1 R) ==> p X, print X.

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 { … }.

Spilling specification

This sections is a deliberately simplified mockup of the real compiler pass in src/compiler/spilling.ml and gives an informal account of how spilling is performed. The input syntax contains a spill_call node that is eliminated during spilling (spill_term, reached from the entry point spill_rule); spill_bound is an auxiliary node representing the output of a spilled predicate call.

../code/spilling_spec.elpi:

% A simplified mockup of the compiler's spilling algorithm, in Elpi itself.
data qkind.
symb piK    qkind.
symb sigmaK qkind.

data term.
% core syntax of data
symb con string -> term.             % constants
symb app list term -> term.          % f X Y
symb lam (term -> term) -> term.     % x\

% injection of predicate call inside terms, always missing one argument
symb spill_call string -> list term -> term. % {p X}
% temporary node: output of a spilled call
symb spill_bound string -> term.

% syntax of goals and rules, rules are pi-closed
data goal.
typeabbrev goals (list goal).
symb quantifier   qkind -> (term -> goals) -> goal. % pi x\, sigma x\
symb implication  goal -> goals -> goal.            % h ==>  g
symb goal         string -> list term -> goal.      % p X Y

% auxiliary data: each spilled call is a goal and the one variable used
% for its missing (output) argument
data spilled.
typeabbrev spills (list spilled).
symb spilled string -> goal -> spilled.

% ------------------------------------------------------------------
% Helpers
% ------------------------------------------------------------------

func flip_quantifier qkind -> qkind.
flip_quantifier piK sigmaK.
flip_quantifier sigmaK piK.

func fresh_name -> string.
fresh_name Name :- new_int N, Name is "%Spill" ^ int_to_string N.

func copy_term term -> term.
copy_term (con S) (con S) :- !.
copy_term (spill_bound S) (spill_bound S) :- !.
copy_term (app Args) (app Args') :- !, std.map Args copy_term Args'.
copy_term (lam F) (lam F') :- !, pi x\ copy_term (F x) (F' x).
copy_term (spill_call N Args) (spill_call N Args') :- !, std.map Args copy_term Args'.
copy_term X X :- name X.

func copy_goal goal -> goal.
copy_goal (quantifier K F) (quantifier K F') :-
  pi x\ std.map (F x) copy_goal (F' x).
copy_goal (implication H B) (implication H' B') :-
  copy_goal H H', std.map B copy_goal B'.
copy_goal (goal S B) (goal S B') :-
  std.map B copy_term B'.

func bind_var_in_goals string, goals -> (term -> goals).
bind_var_in_goals V G G' :- pi Y\ copy_term (spill_bound V) Y =!=> std.map G copy_goal (G' Y).

func bind_name_in_goal term, goal -> (term -> goal).
bind_name_in_goal V G G' :- name V, pi Y\ copy_term V Y =!=> copy_goal G (G' Y).

% ------------------------------------------------------------------
% Main algorithm
% ------------------------------------------------------------------
func spill_term qkind, term -> spills, term.

spill_term _ T [] T :- (T = con _ ; name T), !.

spill_term Q (app Args) Spills (app Args') :- !,
  spill_term_list Q Args Spills Args'.

spill_term Q (lam F) Sbody' (lam F') :- !,
  pi x\
  spill_term Q (F x) (Sbody x) (Body' x),
  lift_out_of_lambda x (Sbody x) (Body' x) Sbody' (F' x).

spill_term Q (spill_call Name Args) AllSpills (spill_bound Fresh) :- !,
  spill_term_list Q Args Sargs Args',
  fresh_name Fresh,
  std.append Args' [spill_bound Fresh] CallArgs,
  std.append Sargs [spilled Fresh (goal Name CallArgs)] AllSpills.

func spill_term_list qkind, list term -> spills, list term.
spill_term_list _ [] [] [].
spill_term_list Q [X|XS] Spills [Y|YS] :-
  spill_term Q X Sx Y, spill_term_list Q XS Rxs YS,
  std.append Sx Rxs Spills.

func spill_goal qkind, goal -> goal.

spill_goal Q (quantifier K F) (quantifier K F') :- !,
  pi x\ std.map (F x) (spill_goal Q) (F' x).

spill_goal Q (implication Head Body) (implication Head' Body') :- !,
  flip_quantifier Q Q',
  spill_rule Q' Head Head',
  std.map Body (spill_goal Q) Body'.

spill_goal Q (goal Name Args) G' :- !,
  spill_call_args Q Name Args Sargs Call,
  add_spilled Q Sargs [Call] [G'].

func spill_call_args qkind, string, list term -> spills, goal.
spill_call_args Q Name Args Sargs (goal Name Args') :- !,
  spill_term_list Q Args Sargs Args'.

func quantify_spill qkind, spilled, goal -> goal.
quantify_spill Q (spilled Var _) Acc Res :-
  place_spilling_quantifier Q Var [Acc] Res.

func spill_rule qkind, goal -> goal.

spill_rule Q (quantifier piK x\[Inner x]) (quantifier piK x\[Inner' x]) :- !,
  pi x\ spill_rule Q (Inner x) (Inner' x).

spill_rule Q (implication (goal Name Args) Body) Result :- !,
  spill_call_args Q Name Args Sh Head',
  flip_quantifier Q Q',
  std.map Body (spill_goal Q') Body0,
  std.fold-right Sh Body0 place_spilled_call Body',
  std.fold-right Sh (implication Head' Body') (quantify_spill Q) Result.

spill_rule Q (goal Name Args) Result :- !,
  spill_call_args Q Name Args Sh T',
  if (Sh = [])
     (Result = T')
     (std.fold-right Sh [] place_spilled_call Body',
      std.fold-right Sh (implication T' Body') (quantify_spill Q) Result).

func place_spilled_call spilled, goals -> goals.
place_spilled_call (spilled _ Goal) Rest [Goal|Rest] :- !.

func place_spilling_quantifier qkind, string, goals -> goal.
place_spilling_quantifier Q Var Gs (quantifier Q Gs') :-
  bind_var_in_goals Var Gs Gs'.

func add_spilled_one qkind, spilled, goals -> goals.
add_spilled_one Q (spilled Var _ as S) GL [SG] :- !,
  place_spilled_call S GL SGL,
  place_spilling_quantifier Q Var SGL SG.

func add_spilled qkind, spills, goals -> goals.
add_spilled Q Spills Rest Result :- !, std.fold-right Spills Rest (add_spilled_one Q) Result.

func apply_spilled_var_to (func A -> A), term, string, A -> A.
apply_spilled_var_to F X V T T' :-
  (copy_term (spill_bound V) (app [spill_bound V,X])) =!=>
  (pi Rest RestX\
    copy_term (app [spill_bound V|Rest]) (app [spill_bound V|RestX]) :- std.append Rest [X] RestX) =!=>
  F T T'.

func apply_spilled_vars_to (func A -> A), term, spilled, A -> A.
apply_spilled_vars_to F X (spilled Var _) T T' :- apply_spilled_var_to F X Var T T'.

func lift_out_of_lambda term, spills, term -> spills, term.
lift_out_of_lambda X Spills Body Spills' Body' :- !,
  std.fold Spills Body (apply_spilled_vars_to copy_term X) Body',
  std.map Spills (s\r\ sigma Var G G0 G'\
    s = spilled Var G,
    bind_name_in_goal X G G0,
    (pi y\ apply_spilled_vars_to copy_goal y s (G0 y) (G' y)),
    r = spilled Var (quantifier piK y\[G' y]))
  Spills'.

Related work. Similar transformations exist in other systems under different names, although none of them handles lambda-tree syntax. Here some pointers:

• Picat replaces a function call f(t1,...,tn) by a new variable V, and inserts a new predicate call p(t1,...,tn,V) before the goal in which the function call occurs (Zhou, PADL 2017).

• Curry’s intermediate representation, FlatCurry, normalizes nested function calls the same way via let-insertion (y:ins(x,ys) becomes let {z = ins(x,ys)} in y:z) (Antoy, Hanus, Jost & Libby, Declare 2019).

• A-normal form, the general functional-compiler ancestor of this family: flatten nested expressions by let-binding every intermediate result (Sabry & Felleisen, LFP 1992; Flanagan, Sabry, Duba & Felleisen, PLDI 1993).

• Prolog’s CLP(FD) flattens arithmetic expressions the same way, scoped to arithmetic: X #= Y+Z*W compiles to a sequence of primitive constraint goals over fresh variables via goal_expansion/2 (Triska, FLOPS 2012).