pub(crate) struct SolveState<'forest, I: Interner> {
    forest: &'forest mut Forest<I>,
    context: &'forest SlgContextOps<'forest, I>,
    stack: Stack<I>,
}

Fields

forest: &'forest mut Forest<I>context: &'forest SlgContextOps<'forest, I>stack: Stack<I>

Implementations

Ensures that answer with the given index is available from the given table. Returns Ok if there is an answer.

This function first attempts to fetch answer that is cached in the table. If none is found, then it will recursively search to find an answer.

This is called when an answer is available for the selected subgoal of the strand. First, if the selected subgoal is a Positive subgoal, it first clones the strand pursuing the next answer. Then, it merges the answer into the provided Strand. On success, Ok is returned and the Strand can be continued to process On failure, Err is returned and the Strand should be discarded

This is called when the selected subgoal for a strand has floundered. We have to decide what this means for the strand.

  • If the strand was positively dependent on the subgoal, we flounder, the subgoal, then return false. This strand may be able to be retried later.
  • If the strand was negatively dependent on the subgoal, then strand has led nowhere of interest and we return true. This strand should be discarded.

In other words, we return whether this strand flounders.

This is called if the selected subgoal for a Strand is a coinductive cycle.

This is called if the selected subgoal for strand is a positive, non-coinductive cycle.

Parameters
  • strand the strand from the top of the stack we are pursuing
  • minimums is the collected minimum clock times

Invoked after we’ve selected a (new) subgoal for the top-most strand. Attempts to pursue this selected subgoal.

Returns:

  • Ok if we should keep searching.
  • Err if the subgoal failed in some way such that the strand can be abandoned.

This is called when there are no remaining subgoals for a strand, so it represents an answer. If the strand is ambiguous and we don’t want it yet, we just enqueue it again to pick it up later. Otherwise, we add the answer from the strand onto the table.

A “refinement” strand is used in coinduction. When the root table on the stack publishes an answer has delayed subgoals, we create a new strand that will attempt to prove out those delayed subgoals (the root answer here is not special except in so far as that there is nothing above it, and hence we know that the delayed subgoals (which resulted in some cycle) must be referring to a table that now has completed).

Note that it is important for this to be a refinement strand – meaning that the answer with delayed subgoals has been published. This is necessary because sometimes the strand must build on that very answer that it is refining. See Delayed Trivial Self Cycle, Variant 3.

Unwinds the entire stack, returning all active strands back to their tables (this time at the end of the queue).

Invoked after we have determined that every strand in table encounters a cycle; strands is the set of strands (which have been moved out of the table). This method then recursively clears the active strands from the tables referenced in strands, since all of them must encounter cycles too.

Invoked when a strand represents an answer. This means that the strand has no subgoals left. There are two possibilities:

  • the strand may represent an answer we have already found; in that case, we can return None, as this strand led nowhere of interest.
  • the strand may represent a new answer, in which case it is added to the table and Some(()) is returned.

Removes the subgoal at subgoal_index from the strand’s subgoal list and adds it to the strand’s floundered subgoal list.

True if all the tables on the stack starting from depth and continuing until the top of the stack are coinductive.

Example: Given a program like:

struct Foo { a: Option<Box<Bar>> }
struct Bar { a: Option<Box<Foo>> }
trait XXX { }
impl<T: Send> XXX for T { }

and then a goal of Foo: XXX, we would eventually wind up with a stack like this:

StackIndexTable Goal
0Foo: XXX
1Foo: Send
2Bar: Send

Here, the top of the stack is Bar: Send. And now we are asking top_of_stack_is_coinductive_from(1) – the answer would be true, since Send is an auto trait, which yields a coinductive goal. But top_of_stack_is_coinductive_from(0) is false, since XXX is not an auto trait.

Trait Implementations

Executes the destructor for this type. Read more

Auto Trait Implementations

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Cast a value to type U using CastTo.

Returns the argument unchanged.

Instruments this type with the provided Span, returning an Instrumented wrapper. Read more

Instruments this type with the current Span, returning an Instrumented wrapper. Read more

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

The type returned in the event of a conversion error.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.

Attaches the provided Subscriber to this type, returning a WithDispatch wrapper. Read more

Attaches the current default Subscriber to this type, returning a WithDispatch wrapper. Read more