curry.backends.py.eval.rts_bindings module

Implements RuntimeState methods related to bindings. This module is not intended to be imported except by rts.py.

A binding is private to the configuration that made it (Configuration.bindings, a copy-on-write map keyed by the group id of the variable). A nested configuration, the capsule of a set function, starts with an empty map, and a variable of its goal that an enclosing configuration bound keeps its binding there. So get_binding and has_binding read through the queue stack (walk_qstack), as read_fp reads the decisions of the enclosing configurations: the map of the configuration first, then the bindings its queue absorbed (Queue.absorbed), then the map of the front configuration of each enclosing queue and the bindings of that queue, under the group id of the variable in that configuration. Without the walk the capsule took such a variable for unbound: it bound the variable anew, to the other side of its comparison, or narrowed it, and the enclosing configuration then met the generator of a variable it had bound (issue #97). A binding found above the configuration’s own level is private state of the configuration there, and a capsule that reads it may be shared by configurations with other bindings (issue #86): get_binding raises E_DIVERGE, and allValues (currylib/setfunctions.py) clones the capsule for that configuration, which absorbs the binding, before the read takes effect. The writers (add_binding, apply_binding, update_binding) use the map of the configuration alone. The C++ runtime has the same rule (RuntimeState::get_binding and diverge).

curry.backends.py.eval.rts_bindings.add_binding(rts, arg, value, config=None)

Create a binding from arg to value. The bindings sit under the root of the class (update_binding keeps them there at a union). The return value indicates whether the binding succeeded: False when the class holds a different binding.

curry.backends.py.eval.rts_bindings.apply_binding(rts, arg=None, config=None)

Applies the binding of arg to config, whose root is an alternative of the generator of the variable (fork): the root e becomes (generator =:<= binding) &> e, so the side of the generator agrees with the binding. The binding is consumed. The constraint carries it into the variables of the generator, and a configuration that forks on the generator again applies nothing. Applied at every fork, the constraint pull-tabbed the same generator to the root, the fork applied the binding once more, and so on without end (issue #97). The C++ runtime has the same step (RuntimeState::apply_binding).

Parameters:

arg –

The argument whose binding to apply. Must be a choice or free variable

node, or ID. The associated ID must refer to a free variable.

config:

The configuration to use as context.

Returns:

Nothing.

curry.backends.py.eval.rts_bindings.get_binding(rts, arg=None, config=None)

Get the binding associated with arg: the configuration’s own, the one its queue absorbed, or that of the nearest enclosing level. A binding of an enclosing level raises E_DIVERGE: the capsule is cloned for the configuration that holds it, and the read runs again in the clone (see the module docstring).

curry.backends.py.eval.rts_bindings.has_binding(rts, arg=None, config=None)

Indicates whether arg has a binding, in this configuration, in its queue, or in an enclosing level. A test alone; get_binding raises E_DIVERGE for a binding of an enclosing level.

curry.backends.py.eval.rts_bindings.make_value_bindings(rts, freevar, values, typedef)

Builds the value bindings of a free variable of a builtin type: one ValueBinding per value, under a tree of choices. freevar is the Variable at the variable, or the node itself. The pair holds the node, without the set guards crossed on the way to it: constrain_equal reads the id of the pair, and a guard has none, so a binding made through the box of a captured argument was dropped (the cause of issue #121). The C++ step builds the same pair (make_value_bindings in state/rts_bindings.cpp).

curry.backends.py.eval.rts_bindings.update_binding(rts, arg=None, config=None, guards=None)

Moves the binding of arg to the root of its class when its group ID changed: arg is a root of a class before a union, and the binding goes under the root after it, so a class keeps one binding, under its root (issue #128). The map of the configuration alone is read.

When the two roots hold distinct binding cells, the class keeps the binding of the new root and the pair (dropped, kept) goes into guards (decision D26 of 2026-10-12): the two classes were bound to two terms, and the strict equality of the two terms, as a guard above the result of the constraint step, decides the merge (fairscheme.D). An equality that fails drops the configuration, as the inconsistent merge did before the decision; one that succeeds keeps the value the failure lost (two equal terms not yet evaluated: eqShapeG18 of unit_constraints.py). One cell under both roots is one binding: nothing to guard. Without a list (a caller outside the constraint step at the root: the fork, the pairing of get_generator) such a merge returns False and fails the step, as before the decision. No program is known to reach it, so the checker counts it (unguarded_merges) and the tests pin the count at zero. The C++ runtime has the same step (merge_binding in state/rts_constraints.cpp).