curry.backends.py.eval.rts module

class curry.backends.py.eval.rts.InterpreterState

Bases: object

The part of the runtime system state that belongs to the interpreter. Each interpreter keeps its own ID factory. Storing this with the interpreter is necessary to ensure that all expressions built by the interpreter are compatible.

class curry.backends.py.eval.rts.RuntimeState(interp, goal=None)

Bases: object

property C

The current configuration. Equivalent to Q[0].

Choice = InfoTable(name='_Choice', arity=3, tag=-2, flags=0, step=None, typedef=None, pyformat=None)

property E

The current root expression. Equivalent to C.root.

Failure = InfoTable(name='_Failure', arity=0, tag=-6, flags=0, step=None, typedef=None, pyformat='failed')

Free = InfoTable(name='_Free', arity=2, tag=-4, flags=0, step=None, typedef=None, pyformat='_{1}')

Fwd = InfoTable(name='_Fwd', arity=1, tag=-3, flags=0, step=None, typedef=None, pyformat='{1}')

NonStrictConstraint = InfoTable(name='_NonStrictConstraint', arity=2, tag=-5, flags=0, step=None, typedef=None, pyformat=None)

PartApplic = InfoTable(name='_PartApplic', arity=2, tag=0, flags=8, step=None, typedef=None, pyformat='{2}')

property Q

The current queue. Equivalent to qtable[qid].

property S

The current set evaluation.

class SetFunctionEval

Bases: object

An object representing the evaluation of a set function.

Created when a set-function-wrapped function is evaluated. It holds the escape set: the choices that escape the set function. The queues of the set function name it by its id (Queue.sid); a choice that escapes splits a queue into two (split_queue), one per side of the choice. The queues hold references to Configuration objects, so steps applied in one queue take effect in all. A step therefore never writes the side of a choice that an enclosing configuration decided into a configuration or into the shared graph: the side is read at a fork through the queue stack (read_fp), after the escape of the choice has bound the queue to that side (choice_escapes, owns_decision).

SetGuard = InfoTable(name='_SetGuard', arity=2, tag=-7, flags=0, step=None, typedef=None, pyformat=None)

StrictConstraint = InfoTable(name='_StrictConstraint', arity=2, tag=-5, flags=0, step=None, typedef=None, pyformat=None)

ValueBinding = InfoTable(name='_ValueBinding', arity=2, tag=-5, flags=0, step=None, typedef=None, pyformat=None)

add_binding(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.

append(config)

Append a configuration to the queue.

apply_binding(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.

catch_control(ground=True, nondet=False, residual=False, restart=False, steplimit=False, unwind=False)

Catch and handle flow-control exceptions.

Parameters:

• ground – Require ground terms. Propagate E_RESIDUAL only if this is true.

• nondet – Catch non-determinism and raise NondetMonadError if it occurs. This takes priority over all other options.

• residual – Handle residuals by updating the current configuration and rotating the queue.

• restart – Catch and ignore E_RESTART.

• steplimit – Handle a spent step budget by rotating the queue. The exception names the queue to rotate (see count_step). When that is an enclosing queue, the exception propagates to the handler of that queue. The set-function evaluations in between are suspended. They resume when their configuration runs again. A RecursionError raised by deep evaluation goes to overflow: the configuration runs again after the others when it made progress, and an alternative that is stuck at the same depth is dropped. So the other alternatives still produce their values.

• unwind – Catch and ignore E_UNWIND.

Returns:

A context manager.

choice_escapes(cid)

Tells whether the choice at the root of the current configuration escapes the set function: rule SF.1 of the dissertation (chapter 4, Figure 4.2). The choice escapes when it is in the escape set of the set of the current queue, or of an enclosing set, and the queue has not escaped it before. A choice in the escape set of an enclosing set came through the guard of an argument of that set function, so it is non-determinism from outside that capsule, and from outside every capsule nested in it. An escape splits the queue, and both queues record the choice (split_queue), so a configuration meets it a second time without an escape: it forks on it, and the fork reads the side from its own fingerprint, or from the enclosing configuration, which runs this queue because it decided the choice that way. A configuration that decided the choice itself, through an occurrence outside the guards (set f $< x $> x), still escapes it, and the split sorts it to its side; a refusal would keep the two sides of the argument in one set. A capsule consumed in part may be shared by enclosing configurations that decided the choice differently (issue #61): the choice node the escape makes is pruned by each of them, where a refusal would write the values of one into the graph the other reads.

A choice in no escape set escapes as well when an enclosing configuration has decided it: a captured occurrence (set f $< x, or an encapsulated expression) of a choice that the outside decided after the capsule started. A fork would prune it, inside a capsule that another enclosing configuration, with the other side, may share, to the side of the configuration that runs the capsule now. The escape splits the capsule instead, and each side prunes its own copy. A choice that no enclosing configuration decided is encapsulated: the configuration forks on it. The fingerprint of the configuration itself is not read here. The C++ runtime has the same rule (RuntimeState::choice_escapes).

clone_generator(bound, unbound)

clone_queue(qid, vid, binding)

Clones queue qid for the configuration that runs it, whose binding of vid the nested evaluation read (E_DIVERGE; see allValues in currylib/setfunctions.py), and returns the id of the clone. The clone holds a copy of every configuration (Configuration.share), the decisions and the absorbed bindings, and absorbs binding for vid. The C++ runtime has the same step (Queue::clone), where the two queues share the configurations and clone one before a step.

constrain_equal(arg0, arg1, constraint_type=STRICT_CONSTRAINT, config=None, guards=None)

Constrain the given arguments to be equal in the specified context. This implements the equational constraints (=:=) and (=:<=). For strict constraints, both arguments must be choices or both free variables, and, in the latter case, the free variables must represent values of the same type (as is guaranteed by the type system). For non-strict constraints, the first argument must be a free variable, and the second is any expression. This implements the “binding” part of (=:<=). When the left-hand side is not a variable, ordinary pull-tabbing computations will proceed until the term is evaluated or this function is called.

Recursive constraints arise from interleaving the rules of (=:=) or (=:<=) with narrowing steps. Suppose x =:= y is first evaluated, then x and y are subsequently narrowed to (x0:x1) and (y0:y1), resp. The recursive constraints over subvariables, x0 =:= y0 and x1 =:= y1, must then be evaluated. The timing of this differs slightly for the two constraint types. With strict constraints, the subvariables are immediately equated. For non-strict constraints this that would give incorrect semantics. Instead, this function creates a binding. When (and if) the binding is later applied, the recursive non-strict constraints between subvariables are evaluated.

Parameters:

• arg0 –

  The arguments to constrain. Each must be a choice or free variable

  node, or ID. The associated IDs must refer to free variables.

  constraint_type:

  The constraint type. Must be STRICT_CONSTRAINT or NONSTRICT_CONSTRAINT.

  config:

  The configuration to use as context.

  guards:

  A list that takes the pairs of bindings (dropped, kept) of the unions that merge two bound classes (update_binding; decision D26 of 2026-10-12), or None: such a merge then fails the step. The constraint step at the root (fairscheme.D) puts the strict equality of each pair above its result.

• arg1 –

  The arguments to constrain. Each must be a choice or free variable

  node, or ID. The associated IDs must refer to free variables.

  constraint_type:

  The constraint type. Must be STRICT_CONSTRAINT or NONSTRICT_CONSTRAINT.

  config:

  The configuration to use as context.

  guards:

  A list that takes the pairs of bindings (dropped, kept) of the unions that merge two bound classes (update_binding; decision D26 of 2026-10-12), or None: such a merge then fails the step. The constraint step at the root (fairscheme.D) puts the strict equality of each pair above its result.

Returns:

A Boolean indicating whether the resulting configuration remains consistent.

constraint_type(arg=None, config=None)

Indicates the constraint type.

count_step()

Account for one rewrite step of the current configuration.

Called from S after each completed step. The step belongs to the current configuration and to the configuration at the head of each enclosing queue, because a set-function evaluation runs inside a step of the enclosing configuration. Each of them counts the step and spends one unit of its budget.

When a configuration has spent its budget, the queue that holds it rotates so that the other configurations get a turn. A queue with one configuration cannot rotate. The outermost queue that can rotate is the target. D rotates it when it handles E_STEPLIMIT, which carries the ID of the queue (see catch_control). The exception suspends the nested evaluations. They resume when their configuration runs again. A nested queue that can rotate is rotated here, in place, before the exception is raised. Otherwise a nested queue whose budget expires together with the budget of an enclosing queue would never rotate. With no step budget, only the counts are kept.

create_queue(sid, goal)

create_setfunction()

drop(trace=True)

Drop the current configuration.

equate_fp(arg0, arg1, config=None)

Equate two IDs in a fingerprint. Set both to the same value and return True, if that is consistent, or return False otherwise.

extend(configs)

Extend the queue.

failure_level(sids)

The level of an outside failure that crossed the guards of the sets sids: the position, in the chain of the capsules innermost first, of the outermost capsule of the chain among them. Zero names the current capsule: none of the sets is on the chain.

fork(config=None)

Fork a choice-rooted configuration. Yields each consistent configuration arising from fixing the choice to the LEFT or RIGHT.

property forks_total

The number of times a configuration forked in this evaluation.

freshvar(target=None)

Places a fresh free variable at the specified location.

freshvar_args()

Generates arguments for a fresh free variable using the next available ID.

generate_values()

Generate the values of the goal.

The evaluator nests one Python call per level of a deep expression, so each value is computed under a raised recursion limit, the flag recursion_limit (see utility.maxrecursion). The limit is restored between values. With the flag None the limit of the interpreter stays.

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

get_freevar(arg=None, config=None)

get_generator(arg=None, config=None)

Returns the generator for the given free variable. The first argument must be a choice or free variable node, or ID.

A variable of a decided class without a generator of its own is bound through the class (Def 2.74 of the note on the Fair Scheme): it gets a clone of the generator of a member that has one, paired leaf by leaf (_constrain_equal_rec of rts_constraints.py, which searches the class; the variable may be the root, which the union by size can leave without a generator; issue #127).

grp_id(arg=None, config=None)

Returns the group ID. The argument must be a choice or variable node, or ID.

Every distinct group of free variables constrained equal with (=:=) belong to a group with a unique group ID. The group ID is the object ID of one arbitrary, distinguished member, called the representative.

Two variables are constrained equal if and only if they share the same group ID (reflexivity permitted).

guard(expr, guards, target=None)

guard_args(expr, guards)

guard_held(expr, guards)

Puts guards on an argument a partial application holds (the box rule for a partial application reached through set guards; see apply and applyS). A guard without a set, the box of an argument of a PartialS (set_ and applyS), stays outermost: evalS gives the new set to the direct successors of its goal alone. The guards go on the value inside that box. The C++ runtime has the same rule (guard_successors).

has_binding(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.

has_generator(arg=None, config=None)

property in_recursive_call

instantiate(var, typedef, config=None)

Instantiates a needed free variable, at the specified location.

Returns:

The expression the free variable was replaced with.

is_builtin_type(ty)

is_io(func)

is_narrowed(arg=None, config=None)

Indicates whether the given free varaible was narrowed in this configuration. The argument must be a free variable node or ID.

is_nondet(arg=None, config=None)

Returns True if the argument is a choice or variable.

is_void(arg=None, config=None)

Indicates whether a free variable is missing any information that would allow a computation needing it to proceed. Used to implement Prelude.ensureNotFree.

lift_constraint(var, rewrite=None)

Similar to a pull-tab step, lift the constraint at var.target above var.root.

make_value(arg=None, config=None)

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

obj_id(arg=None, config=None)

Returns the choice or variable ID of a node. The node argument must be a choice or free variable node. For convenience, arg may be an ID, in which case it is simply returned.

overflow(error)

Handle a RecursionError raised by the evaluation of the current configuration. Returns True when D continues with the current queue, and False when the error goes to the enclosing queue. This mirrors RuntimeState::unwind of the C++ backend.

A configuration that took no step since it last overflowed is stuck: it repeats the same descent and overflows at the same point. The steps of a nested set-function evaluation count for the enclosing configuration. Re-scanning a configuration from its root repeats the descent but loses no work, because the graph holds every result.

In the outermost queue, a configuration that made progress runs again after the others. A stuck one is dropped. Its error waits in rts.deferred_error until the queue is empty (see D and ready), so the other alternatives still produce their values. In a nested queue, a configuration cannot be dropped without losing a value of the set function. It runs again after the others when any step was taken since it last overflowed. When no step was taken, the enclosing queue decides.

owns_decision(cid)

Tells whether the current configuration owns the decision of choice cid: it made the choice itself, or its queue was split on the choice (Queue.decisions), so every configuration that runs the queue decided the choice the same way. A configuration that owns the decision may take the side of an escaped choice at once (allValues in currylib/setfunctions.py). One that reads the side from an enclosing configuration alone may be in a capsule that enclosing configurations with different decisions share, so the side goes into no state of its own: the choice node stays, reaches its root, and escapes in turn (choice_escapes), up to the configuration that decided it. The C++ runtime has the same test (RuntimeState::owns_decision).

pop_queue(trace=True)

pull_tab(root, target, realpath, rewrite=None)

Make a choice node with ID cid whose alternatives are derived by replacing node[path] with the alternatives of choice-rooted expression``alternatives``. If alternatives is not specified, then node[path] is used. If rewrite is supplied, the specified node is overwritten. Otherwise a new node is created.

push_queue(sid=None, qid=None, trace=True)

property qid

The ID of the current queue.

queue_scope(sid=None, qid=None, trace=True)

raise_deferred_error()

Raise the error of an alternative dropped at the stack limit, if there is one. Only the outermost queue reports it, after the other alternatives have run. See overflow.

read_fp(arg=None, config=None)

Read the fingerprint for the given argument. The argument must be a choice or variable node, ID, or ChoiceState. The group ID is always used to read a fingerprint. For convenience, if a ChoiceState is provided, it is simply returned.

ready()

Checks whether the runtime is ready to continue evaluation. Skips over blocked configurations and raises EvaluationSuspended if the queue contains only blocked configurations. Returns True when the queue is not empty and the configuration at the head is ready to be further evaluated.

record_failure(guards=())

Records a failure met by the current configuration in its capsule: rule (d1) of the failure rule F2 in its deferred form (Definition 2.94 of the note on the Fair Scheme). The caller drops the configuration as every failure does (D at a failed root; N and hnf hand the failure up to it). This records what the failure was for the verdict on the empty queue (Queue.fails_at_end and Queue.failure_guards; allValues in currylib/setfunctions.py).

The failure is boxed when the path from the root of the configuration to the failure crosses a set guard. The path is read from the call stack of the configuration: the guards of the variable of each hnf frame, and the guards the walk of each N frame crossed (the guards of its variable and the set ids it pushed); guards adds those of the position in hand. A guard of the current set at the root, which D stripped, set escape_all. A boxed failure came through the box of an argument of a set function, this one or an enclosing one, as the box rule of the dissertation (chapter 4) keeps every reference to a boxed expression boxed. So it is a failure of the context, not of the function: the capsule records an outside failure with the ids of the enclosing sets whose guards it crossed, less the current set, and the level at which it entered the chain of the capsules (the position, innermost first, of the outermost capsule of the chain among them; zero when none is on the chain). A failure that crossed no guard is the function’s own: the capsule records an inside failure (rule SF.5 of the dissertation drops the alternative). A capsule whose queue empties with no value, no inside failure and some outside failure is itself a failure, the semantics of weakly encapsulated search (Christiansen, Hanus, Reck and Seidel, PPDP 2013), as KiCS2 behaves. Outside every set function nothing is recorded.

A failure is observed at the position that met it first, with the whole path, and again at each level above it on the way to the root, with a shorter path (hnf rewrites the redex to the failure and unwinds, and the caller meets the failure at the redex). The first observation makes the record and sets Configuration.failure_recorded; the rest make none. A constraint that fails at the root of D (the occurs check, or the union of two classes with different instances) is a failure at the root like a failure cell there: the path crossed no guard, so the record is an inside failure, unless the configuration stripped a guard of its set at the root before (escape_all). The C++ runtime has the same rule (RuntimeState::record_failure).

The level of an outside failure is failure_level, and the choice of the records at the end of the capsule is failure_guards of queue.py; the checker calls both (check_failure_record and check_capsule_end), so a change of the reading of rule (d3) touches those two functions alone.

register_freevar(var)

Update the vtable for variable var. The variable is added to the table so that it can be found later, if needed.

register_freevars(root)

Registers every free variable of the expression at root in the vtable. A goal built outside this evaluation can hold variables that no table of this state knows: a curry.free marker shared with an earlier goal, whose node the step of Prelude.unknown forwarded to a free variable; the result of the single rewrite step of a compiled expression; a raw Free node of curry.raw_expr; a value of an earlier evaluation. The item of a generator node is built during the evaluation, so its step walks the item as well (prelude/string.py). The walk is iterative with a visited set, because a goal can be cyclic. It follows forward nodes and descends into every node successor: data, partial applications, set guards, constraints, choices, and the generators of free variables. The C++ runtime has the same method.

release_value()

Makes a value from the first configuration, detaches that configuration from the computation state, and then returns the value.

restart()

Unwind to the next N() or S() procedure.

rotate(n=1)

Rotate the queue by n positions. By default, the current configuration is moved to the end.

scheduler_counters()

The scheduler counters of this evaluation. The Python backend has none; see cyrt/state/counters.hpp for the C++ runtime.

set_goal(goal)

property setfunctions

property sid

The ID of the current set.

single_step(node)

Takes one rewrite step at the root of node, outside the step loop (see evaluator.single_step). The step function takes the root as a variable, as in S. A completed step counts as in S: the step counter and the current configuration take it up. A step that raises left its redex as it was and counts nothing.

split_queue(qid, cid)

Splits queue qid on choice cid, which escapes the set function, and returns the id of the new queue (rule SF.1; see allValues in currylib/setfunctions.py). A configuration that made the choice LEFT stays, and one that made it RIGHT moves to the new queue. One that has not made it is in both queues. Both queues record the choice (Queue.decisions), so that a configuration forks on it instead of escaping it again (choice_escapes). Whether a configuration made the choice is read from its own fingerprint, never from an enclosing configuration. The C++ runtime has the same split (Queue::split).

property steps_total

The number of rewrite steps taken in this evaluation.

suspend(arg, config=None)

Suspend a configuration with the given residual(s).

unwind()

Unwind to the next N() or S() procedure.

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

update_escape_set(sid, cid)

update_escape_sets(sids, cid)

update_fp(choicestate, arg=None, config=None)

Update the fingerprint to reflect the ID associated with arg` being set to choicestate.

If choicestate is UNDETERMINED, this does nothing. Otherwise, the current value of arg is determined, consulting the fingerprint, if necessary. If it is consistent with choicestate then it is updated and True is returned. Otherwise, False is returned.

Parameters:

• choicestate – The choice state to set. Must be a ChoiceState, choice or free variable node, or ID.

• arg – The ID to update in the fingerprint. Must be a choice or free variable node, or ID.

• config – The Configuration to use as context.

Returns:

A Boolean indicating whether the change is consistent.

variable(parent, logicalpath=None)

Creates an instance of Variable.

walk_qstack(firstconfig=None)

Walk the chain of active configurations up the queue stack. This visits each set function application up to the top.

Parameters:

firstconfig – The optional first (i.e., current) configuration. If provided , it will take the place of the current configuration. This does not affect any parent configuration in the chain.

Yields:

Each active configuration on the stack.