Struct chalk_recursive::fixed_point::RecursiveContext

pub(crate) struct RecursiveContext<K, V>
where
    K: Hash + Eq + Debug + Clone,
    V: Debug + Clone,
{
    stack: Stack,
    search_graph: SearchGraph<K, V>,
    cache: Option<Cache<K, V>>,
    max_size: usize,
}

Fields

stack: Stack

search_graph: SearchGraph<K, V>

The “search graph” stores “in-progress results” that are still being solved.

cache: Option<Cache<K, V>>

The “cache” stores results for goals that we have completely solved. Things are added to the cache when we have completely processed their result.

max_size: usize

The maximum size for goals.

Implementations

impl<K, V> RecursiveContext<K, V>

where K: Hash + Eq + Debug + Clone, V: Debug + Clone,

pub fn new( overflow_depth: usize, max_size: usize, cache: Option<Cache<K, V>> ) -> Self

pub fn max_size(&self) -> usize

pub fn solve_root_goal( &mut self, canonical_goal: &K, solver_stuff: impl SolverStuff<K, V>, should_continue: impl Fn() -> bool + Clone ) -> V

Solves a canonical goal. The substitution returned in the solution will be for the fully decomposed goal. For example, given the program

struct u8 { }
struct SomeType<T> { }
trait Foo<T> { }
impl<U> Foo<u8> for SomeType<U> { }

and the goal exists<V> { forall<U> { SomeType<U>: Foo<V> } }, into_peeled_goal can be used to create a canonical goal SomeType<!1>: Foo<?0>. This function will then return a solution with the substitution ?0 := u8.

pub fn solve_goal( &mut self, goal: &K, minimums: &mut Minimums, solver_stuff: impl SolverStuff<K, V>, should_continue: impl Fn() -> bool + Clone ) -> V

Attempt to solve a goal that has been fully broken down into leaf form and canonicalized. This is where the action really happens, and is the place where we would perform caching in rustc (and may eventually do in Chalk).

fn solve_new_subgoal( &mut self, canonical_goal: &K, depth: StackDepth, dfn: DepthFirstNumber, solver_stuff: impl SolverStuff<K, V>, should_continue: impl Fn() -> bool + Clone ) -> Minimums