curry.backends.py.eval.rts_setfunctions module
Implements RuntimeState methods related to set functions. This module is not intended to be imported except by rts.py.
- class curry.backends.py.eval.rts_setfunctions.SetFunctionEval[source]
Bases:
objectAn 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).
- curry.backends.py.eval.rts_setfunctions.choice_escapes(rts, cid)[source]
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).
- curry.backends.py.eval.rts_setfunctions.clone_queue(rts, qid, vid, binding)[source]
Clones queue
qidfor the configuration that runs it, whose binding ofvidthe 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 absorbsbindingforvid. The C++ runtime has the same step (Queue::clone), where the two queues share the configurations and clone one before a step.
- curry.backends.py.eval.rts_setfunctions.failure_level(rts, sids)[source]
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.
- curry.backends.py.eval.rts_setfunctions.guard_held(rts, expr, guards)[source]
Puts
guardson 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_andapplyS), 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).
- curry.backends.py.eval.rts_setfunctions.owns_decision(rts, cid)[source]
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).
- curry.backends.py.eval.rts_setfunctions.record_failure(rts, guards=())[source]
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);
guardsadds 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.
- curry.backends.py.eval.rts_setfunctions.split_queue(rts, qid, cid)[source]
Splits queue
qidon choicecid, 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).
- curry.backends.py.eval.rts_setfunctions.walk_qstack(rts, firstconfig=None)[source]
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.