curry.toolchain.flat2icurry.setlift module

The set0 lift, a FlatCurry-to-FlatCurry pass over the FlatCurry file of a module (decision D28 of 2026-10-12).

set0 e is the set function of the expression e. When e holds variables of the enclosing context (the captured variables), those variables are arguments of the capsule, boxed at the entry as the arguments of setk are: the set function of e is the set function of the operation \v_1 .. v_p -> e applied to v_1 .. v_p, and the non-determinism and the failure of a captured variable stay outside the set, one set per outside alternative. That is the semantics of weakly encapsulated search (Christiansen, Hanus, Reck and Seidel, PPDP 2013, section 3.3): let x = coin in allValues x yields {0} and {1}, and let x = failed in allValues x fails instead of yielding a set. The implementations that scope by the time of the first evaluation (KiCS2, PAKCS) are not the authority; the paper is.

The compiler, not the runtime, makes it so. The runtime boxes the arguments a function value holds (set_step of cyrt/currylib/setfunctions.cpp, set_ of the Python backend; issue #117), so set1 (f x_1 .. x_(k-1)) x_k and setk f x_1 .. x_k reach one entry state for any k, and this pass turns every saturated call set0 e whose argument has captured variables x_1 .. x_k into that call:

• A new function L x_1 .. x_k = e, Private, with the arity k and a fresh polymorphic type forall a_0 .. a_k. a_0 -> .. -> a_k (the file is written to disk, and a reader of the file may read the type; the ICurry compiler ignores it). A type annotation at the root of e is removed first: a root annotation over a let, a free declaration or a case meets a defect of icurry 3.1.0 (see compiler.to_iblock).

• The call becomes setk L x_1 .. x_k for k up to seven, the arities the library has, and set1 (L x_1 .. x_(k-1)) x_k beyond, which reaches the same entry state.

The captured variables are the variables e does not bind (the Curry unboundVars), in the order of their first occurrence in e. A class dictionary and a variable of a where .. free declaration outside e are captured variables like any other, as they are arguments of a lambda-lifted function. The pass runs bottom-up, so a set0 inside e is lifted first, and it reaches every rule of the module, the lifted lambdas of the front end (f._#lambdaN) and the bodies of lets and cases included. set0 $ e is the call set0 e (the $ on a partial application is reduced as the binding optimization reduces it).

The name of a lifted function is f_SET0n, where f is the local name of the enclosing function and n counts from zero per enclosing function; a name an original function of the module has is skipped, and the counter still advances. The front end writes no such name (f._#lambdaN, f.g.N, _impl#, _inst#, _super#, _def#), and the case lifting of the translation (caselifting, names f_CASEn, f_LETn, f_FREEn, f_COMPLEXCASEn) runs after this pass over a program that holds the lifted functions, whose names it skips. A lifted function has no entry in the interface M.fint, which the pass never writes: it is private, and the importers number the public functions of the module from that file.

A closed set0 e (no captured variable) is unchanged: an encapsulated expression, with no argument to box. A set0 that is not a saturated call, a partial application such as map set0 xs or a set0 reached through a variable, is left alone: the pass sees no argument there.

optimize_file() applies the pass to a FlatCurry file in place, as bindingopt.optimize_file() applies the binding optimization; the routes apply the two passes together (rewrite.rewrite_file()), after the front end and before the translation, so the .fcy on disk is the lifted program and both routes translate the same text. The pass is idempotent: over a lifted program it lifts nothing and writes nothing.

curry.toolchain.flat2icurry.setlift.captured_vars(e)

The variables e does not bind (the Curry unboundVars), each once, in the order of their first occurrence in a left-to-right walk of e: the arguments of a call in order, the bindings of a let before its body, the scrutinee of a case before its branches. A variable a let, a free declaration or a pattern of e binds is left out under its binder. The walk keeps its own stack, so an expression of any depth needs no recursion.

curry.toolchain.flat2icurry.setlift.contains_set0(e)

Whether an expression holds a call or a partial application of set0. The walk keeps its own stack.

curry.toolchain.flat2icurry.setlift.is_lifted_name(name)

Whether the local name name is the name of a lifted function.

curry.toolchain.flat2icurry.setlift.lift_type(k)

The type of a lifted function of arity k: a fresh polymorphic scheme over k + 1 type variables, forall a_0 .. a_k. a_0 -> .. -> a_k, written as the front end writes a scheme.

curry.toolchain.flat2icurry.setlift.lifted_functions(prog)

The qualified names of the lifted functions of a program.

curry.toolchain.flat2icurry.setlift.optimize_file(fcyfile)

Applies the set0 lift to the FlatCurry file fcyfile in place. The file is written again, in the format of the front end, when the pass lifted a call; else it is left as it is, with its time. Returns the number of calls lifted.

curry.toolchain.flat2icurry.setlift.optimize_set0(prog)

Applies the set0 lift to a FlatCurry program. Returns the transformed program when a call was lifted, else prog itself.

curry.toolchain.flat2icurry.setlift.set0_call(e)

The saturated call set0 e' that e is, or None. Two shapes count: the call itself, and set0 $ e' (a call of $ on the partial application set0, which is reduced to the call). A partial application of set0 alone is no call.

curry.toolchain.flat2icurry.setlift.strip_typed(e)

The expression under any type annotations at the root.

curry.toolchain.flat2icurry.setlift.transform_exp(state, e)

Transforms an expression bottom-up: the subexpressions first, then the expression itself when it is a saturated call of set0 whose argument has captured variables. The walk runs on a stack of its own (utility.trampoline.trampoline()), so a nested application of any depth needs no recursion (issue #125).

curry.toolchain.flat2icurry.setlift.transform_func(fd, names)

Transforms a function declaration. Returns the declaration and the list of the functions lifted out of it. names is the set of the qualified names of the functions of the module, which the new names join. A rule without a set0, and one whose every set0 is closed or not a saturated call, is returned as it is.

curry.toolchain.flat2icurry.setlift.transform_prog(prog)

Transforms a FlatCurry program. Returns the new program and the number of set0 calls lifted, or the program itself and zero. A lifted function follows the function it was lifted out of.