Struct chalk_engine::logic::SolveState

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

impl<'forest, I: Interner> SolveState<'forest, I>

fn ensure_root_answer( &mut self, initial_table: TableIndex, initial_answer: AnswerIndex, ) -> Result<(), RootSearchFail>

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.

fn merge_answer_into_strand( &mut self, infer: &mut InferenceTable<I>, strand: &mut Strand<I>, ) -> Result<(), RootSearchFail>

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

fn propagate_floundered_subgoal( &mut self, strand: &mut Canonical<Strand<I>>, ) -> bool

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.

fn on_coinductive_subgoal( &mut self, canonical_strand: Canonical<Strand<I>>, ) -> Result<(), RootSearchFail>

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

fn on_positive_cycle( &mut self, canonical_strand: Canonical<Strand<I>>, minimums: Minimums, ) -> Result<(), RootSearchFail>

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

fn on_subgoal_selected( &mut self, canonical_strand: Canonical<Strand<I>>, ) -> Result<(), RootSearchFail>

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.

fn on_no_remaining_subgoals( &mut self, canonical_strand: Canonical<Strand<I>>, ) -> NoRemainingSubgoalsResult

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.

fn create_refinement_strand( &self, table: TableIndex, answer: &Answer<I>, ) -> Option<Canonical<Strand<I>>>

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.

fn on_no_strands_left(&mut self) -> Result<(), RootSearchFail>

fn unwind_stack(&mut self)

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

fn clear_strands_after_cycle( &mut self, strands: impl IntoIterator<Item = Canonical<Strand<I>>>, )

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.

fn select_subgoal( &mut self, canonical_strand: &mut Canonical<Strand<I>>, ) -> SubGoalSelection

fn pursue_answer( &mut self, canonical_strand: Canonical<Strand<I>>, ) -> Option<AnswerIndex>

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.

fn reconsider_floundered_subgoals(&mut self, ex_clause: &mut ExClause<I>)

fn flounder_subgoal(&self, ex_clause: &mut ExClause<I>, subgoal_index: usize)

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

pub(crate) fn top_of_stack_is_coinductive_from(&self, depth: StackIndex) -> bool

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:

StackIndex	Table Goal
0	Foo: XXX
1	Foo: Send
2	Bar: 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

impl<'forest, I: Interner> Drop for SolveState<'forest, I>

fn drop(&mut self)

Executes the destructor for this type.