[−][src]Trait chalk_engine::context::ContextOps
Required methods
fn is_coinductive(&self, goal: &UCanonical<InEnvironment<Goal<I>>>) -> bool
True if this is a coinductive goal -- e.g., proving an auto trait.
fn program_clauses(
&self,
environment: &Environment<I>,
goal: &DomainGoal<I>,
infer: &mut C::InferenceTable
) -> Result<Vec<ProgramClause<I>>, Floundered>
&self,
environment: &Environment<I>,
goal: &DomainGoal<I>,
infer: &mut C::InferenceTable
) -> Result<Vec<ProgramClause<I>>, Floundered>
Returns the set of program clauses that might apply to
goal
. (This set can be over-approximated, naturally.)
If this callback returns None
, that indicates that the set
of program clauses cannot be enumerated because there are
unresolved type variables that would have to be resolved
first; the goal will be considered floundered.
fn add_clauses(
&self,
env: &Environment<I>,
clauses: ProgramClauses<I>
) -> Environment<I>
&self,
env: &Environment<I>,
clauses: ProgramClauses<I>
) -> Environment<I>
fn instantiate_ucanonical_goal(
&self,
arg: &UCanonical<InEnvironment<Goal<I>>>
) -> (C::InferenceTable, Substitution<I>, Environment<I>, Goal<I>)
&self,
arg: &UCanonical<InEnvironment<Goal<I>>>
) -> (C::InferenceTable, Substitution<I>, Environment<I>, Goal<I>)
Create an inference table for processing a new goal and instantiate that goal in that context, returning "all the pieces".
More specifically: given a u-canonical goal arg
, creates a
new inference table T
and populates it with the universes
found in arg
. Then, creates a substitution S
that maps
each bound variable in arg
to a fresh inference variable
from T. Returns:
- the table
T
- the substitution
S
- the environment and goal found by substitution
S
intoarg
fn instantiate_ex_clause(
&self,
num_universes: usize,
canonical_ex_clause: &Canonical<ExClause<I>>
) -> (C::InferenceTable, ExClause<I>)
&self,
num_universes: usize,
canonical_ex_clause: &Canonical<ExClause<I>>
) -> (C::InferenceTable, ExClause<I>)
fn instantiate_answer_subst(
&self,
num_universes: usize,
answer: &Canonical<AnswerSubst<I>>
) -> (C::InferenceTable, Substitution<I>, Vec<InEnvironment<Constraint<I>>>, Vec<InEnvironment<Goal<I>>>)
&self,
num_universes: usize,
answer: &Canonical<AnswerSubst<I>>
) -> (C::InferenceTable, Substitution<I>, Vec<InEnvironment<Constraint<I>>>, Vec<InEnvironment<Goal<I>>>)
fn identity_constrained_subst(
&self,
goal: &UCanonical<InEnvironment<Goal<I>>>
) -> Canonical<ConstrainedSubst<I>>
&self,
goal: &UCanonical<InEnvironment<Goal<I>>>
) -> Canonical<ConstrainedSubst<I>>
Returns a identity substitution.
fn map_goal_from_canonical(
&self,
_: &UniverseMap,
value: &Canonical<InEnvironment<Goal<I>>>
) -> Canonical<InEnvironment<Goal<I>>>
&self,
_: &UniverseMap,
value: &Canonical<InEnvironment<Goal<I>>>
) -> Canonical<InEnvironment<Goal<I>>>
Convert a goal G from the canonical universes into our local universes. This will yield a goal G' that is the same but for the universes of universally quantified names.
fn map_subst_from_canonical(
&self,
_: &UniverseMap,
value: &Canonical<AnswerSubst<I>>
) -> Canonical<AnswerSubst<I>>
&self,
_: &UniverseMap,
value: &Canonical<AnswerSubst<I>>
) -> Canonical<AnswerSubst<I>>
Convert a substitution from the canonical universes into our local universes. This will yield a substitution S' that is the same but for the universes of universally quantified names.
fn interner(&self) -> &I
fn into_goal(&self, domain_goal: DomainGoal<I>) -> Goal<I>
Upcast this domain goal into a more general goal.
fn is_trivial_constrained_substitution(
&self,
constrained_subst: &Canonical<ConstrainedSubst<I>>
) -> bool
&self,
constrained_subst: &Canonical<ConstrainedSubst<I>>
) -> bool
fn is_trivial_substitution(
&self,
u_canon: &UCanonical<InEnvironment<Goal<I>>>,
canonical_subst: &Canonical<AnswerSubst<I>>
) -> bool
&self,
u_canon: &UCanonical<InEnvironment<Goal<I>>>,
canonical_subst: &Canonical<AnswerSubst<I>>
) -> bool