[−][src]Trait chalk_engine::context::Context
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.
Required methods
fn next_subgoal_index(ex_clause: &ExClause<I>) -> usize
Selects the next appropriate subgoal index for evaluation. Used by: logic