Trait chalk_engine::context::Context

pub trait Context<I: Interner>: Clone + Debug {
    type InferenceTable: InferenceTable<I, Self> + Clone;
    fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize;
}

The "context" in which the SLG solver operates. It defines all the types that the SLG solver may need to refer to, as well as a few very simple interconversion methods.

At any given time, the SLG solver may have more than one context active. First, there is always the global context, but when we are in the midst of pursuing some particular strand, we will instantiate a second context just for that work, via the instantiate_ucanonical_goal and instantiate_ex_clause methods.

In the chalk implementation, these two contexts are mapped to the same type. But in the rustc implementation, this second context corresponds to a fresh arena, and data allocated in that second context will be freed once the work is done. (The "canonicalizing" steps offer a way to convert data from the inference context back into the global context.)

FIXME: Clone and Debug bounds are just for easy derive, they are not actually necessary. But dang are they convenient.

Associated Types

type InferenceTable: InferenceTable<I, Self> + Clone

Represents an inference table.

Loading content...

Required methods

fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize

Selects the next appropriate subgoal index for evaluation. Used by: logic

Loading content...

Implementors

Loading content...