curry.toolchain.flat2icurry.bindingopt module

The binding optimization, a FlatCurry-to-FlatCurry pass over the FlatCurry file of a module.

PAKCS and KiCS2 run the tool transbooleq over every FlatCurry file they compile (the property bindingoptimization of PAKCS, fast by default). This module is a port of its fast mode. The ideas are in “From Boolean Equalities to Constraints” (Antoy and Hanus, LOPSTR 2015) and “Transforming Boolean equalities into constraints” (Formal Aspects of Computing, 2017).

A Boolean equality whose value is required to be True is replaced by the equational constraint, which binds free variables where the Boolean equality on a primitive type suspends:

• e1 == e2 and e1 === e2 become constrEq e1 e2.

• e1 /= e2 and e1 /== e2 with required value False become not (constrEq e1 e2).

The required value comes from the context. The condition of a rule is required True: the front end writes a guard as case c of True -> e; False -> failed. The scrutinee of a case with one branch that does not fail is required to be the constructor of that branch. The fast mode knows the required values of the arguments of a few Prelude operations and no others (PRELUDE_REQUIRED_VALUES): the arguments of && and & required True are required True, the argument of not required False is required True, and so on. An operation outside the table requires nothing of its arguments. So f x | x == 3 = x and f x | x == 1 && y == 2 bind, while if x == 3 then a else b and a guard with an otherwise branch keep the Boolean equality, as under PAKCS.

The pass changes the semantics of a program in the same way PAKCS does. (1 == 2) & True is False under the plain semantics and fails after the pass, because & requires both arguments True whatever its result is required to be. An equivalence == is replaced on the assumption that the Eq instance defines equality; the tool of PAKCS makes the same assumption.

optimize_file() applies the pass to a FlatCurry file in place, as PAKCS does before any compiler reads the file (preprocessFcyFile of its compiler): the file is written again when the pass replaced an equality, and left as it is otherwise. Both routes from Curry to ICurry (curry.toolchain._frontend and the icurry program, see curry.toolchain._curry2icurry) run it after the front end and before the translation, as the first pass of the rewrite step (rewrite; the set0 lift of setlift is the second), so the .fcy file on disk is the optimized program and the two routes translate the same text. The pass is idempotent: over an optimized program it replaces nothing and writes nothing. optimize_bindings() is the pass on a program in memory; the oracle tests of the translation never apply it, because the files icurry wrote for the oracle come from the FlatCurry as the front end wrote it.

The command line of rewrite rewrites FlatCurry files by hand, with both passes:

python -m curry.toolchain.flat2icurry.rewrite [-q] M.fcy...

The products made from the file before (the ICurry and what follows it) are not touched by it; sprite-make --rewrite-flat runs the step of a module again and makes them from the rewritten file.

curry.toolchain.flat2icurry.bindingopt.case_arg_type(branches)

The required value of the scrutinee of a case. True when the second branch is False -> failed, the translation of a guard. Otherwise the constructor of the one branch that does not fail, or ANY.

curry.toolchain.flat2icurry.bindingopt.constructors(a)

The constructor set of a constructor value.

curry.toolchain.flat2icurry.bindingopt.contains_equality(e, equivalence=True)

Whether an expression holds a Boolean equality or disequality call. The walk keeps its own stack, so a nested application of any depth needs no recursion.

curry.toolchain.flat2icurry.bindingopt.equality_operands(e, eq, equivalence=True)

The two operands of a call of a Boolean equality (eq) or disequality (not eq), or None. Three shapes count: a saturated call of the method with the operands last, after any dictionaries; a method applied to a dictionary and then to the operands through apply; and a default instance method without a dictionary, applied the same way.

curry.toolchain.flat2icurry.bindingopt.lub(a, b)

The least upper bound of two abstract values, lubAType of the analysis. ANY absorbs every value, ANYC absorbs a constructor value, and two constructor values join to the set of their constructors: a single name when both name the same constructor, else a frozenset. The join of True and False is such a set, not ANYC: it is the required value of the argument of not as a value, and it requires nothing of the arguments of a call below it (see required_argument_values).

curry.toolchain.flat2icurry.bindingopt.optimize_bindings(prog, equivalence=True)

Applies the binding optimization to a FlatCurry program. Returns the transformed program when an equality was replaced, else prog itself: transbooleq writes a file only then, so a rule whose equalities all stay is rebuilt (its $ reduced) only in a program that is transformed.

curry.toolchain.flat2icurry.bindingopt.optimize_file(fcyfile, equivalence=True)

Applies the binding optimization to the FlatCurry file fcyfile in place. The file is written again, in the format of the front end, when the pass replaced an equality; else it is left as it is, with its time. Returns the number of equalities replaced.

curry.toolchain.flat2icurry.bindingopt.required_argument_values(qname, reqval, nargs)

The required values of the nargs arguments of a call of qname whose result is required to be reqval: argumentTypesFor of transbooleq. The table gives the arguments of the entry with that result, else of an entry with an unrequired result, else the join of all entries when reqval is ANY or ANYC. An operation outside the table, and any other case, requires nothing. A set of constructors is such a case: not as a value requires True or False of its argument, so not ((x == 1) & (y == 2)) and not (solve (x == 3)) keep their equalities and suspend, as under PAKCS, while not (not e) requires nothing of e, and the join path transforms & and solve in it.

curry.toolchain.flat2icurry.bindingopt.transform_exp(e, reqval, equivalence=True)

Transforms an expression whose value is required to be reqval. Returns the new expression and the number of equalities replaced. 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.bindingopt.transform_func(fd, equivalence=True)

Transforms a function declaration. Returns it with the count. As in transbooleq, a rule without a Boolean equality is returned as it is, and a rule with one is rebuilt, so its applications of $ to a partial application are reduced to calls whether or not an equality is replaced.

curry.toolchain.flat2icurry.bindingopt.transform_prog(prog, equivalence=True)

Transforms a FlatCurry program. Returns the new program and the number of equalities replaced. Without equivalence only === and /== are replaced, as under the option -s of transbooleq.