[−][src]Trait chalk_engine::context::UnificationOps
Methods for unifying and manipulating terms and binders.
Required methods
fn instantiate_binders_universally(
&mut self,
interner: &I,
arg: &Binders<Goal<I>>
) -> Goal<I>
&mut self,
interner: &I,
arg: &Binders<Goal<I>>
) -> Goal<I>
fn instantiate_binders_existentially(
&mut self,
interner: &I,
arg: &Binders<Goal<I>>
) -> Goal<I>
&mut self,
interner: &I,
arg: &Binders<Goal<I>>
) -> Goal<I>
fn debug_ex_clause<'v>(
&mut self,
interner: &I,
value: &'v ExClause<I>
) -> Box<dyn Debug + 'v>
&mut self,
interner: &I,
value: &'v ExClause<I>
) -> Box<dyn Debug + 'v>
fn fully_canonicalize_goal(
&mut self,
interner: &I,
value: &InEnvironment<Goal<I>>
) -> (UCanonical<InEnvironment<Goal<I>>>, UniverseMap)
&mut self,
interner: &I,
value: &InEnvironment<Goal<I>>
) -> (UCanonical<InEnvironment<Goal<I>>>, UniverseMap)
fn canonicalize_ex_clause(
&mut self,
interner: &I,
value: &ExClause<I>
) -> Canonical<ExClause<I>>
&mut self,
interner: &I,
value: &ExClause<I>
) -> Canonical<ExClause<I>>
fn canonicalize_constrained_subst(
&mut self,
interner: &I,
subst: Substitution<I>,
constraints: Vec<InEnvironment<Constraint<I>>>
) -> Canonical<ConstrainedSubst<I>>
&mut self,
interner: &I,
subst: Substitution<I>,
constraints: Vec<InEnvironment<Constraint<I>>>
) -> Canonical<ConstrainedSubst<I>>
fn canonicalize_answer_subst(
&mut self,
interner: &I,
subst: Substitution<I>,
constraints: Vec<InEnvironment<Constraint<I>>>,
delayed_subgoals: Vec<InEnvironment<Goal<I>>>
) -> Canonical<AnswerSubst<I>>
&mut self,
interner: &I,
subst: Substitution<I>,
constraints: Vec<InEnvironment<Constraint<I>>>,
delayed_subgoals: Vec<InEnvironment<Goal<I>>>
) -> Canonical<AnswerSubst<I>>
fn invert_goal(
&mut self,
interner: &I,
value: &InEnvironment<Goal<I>>
) -> Option<InEnvironment<Goal<I>>>
&mut self,
interner: &I,
value: &InEnvironment<Goal<I>>
) -> Option<InEnvironment<Goal<I>>>
fn unify_generic_args_into_ex_clause(
&mut self,
interner: &I,
environment: &Environment<I>,
a: &GenericArg<I>,
b: &GenericArg<I>,
ex_clause: &mut ExClause<I>
) -> Fallible<()>
&mut self,
interner: &I,
environment: &Environment<I>,
a: &GenericArg<I>,
b: &GenericArg<I>,
ex_clause: &mut ExClause<I>
) -> Fallible<()>
First unify the parameters, then add the residual subgoals as new subgoals of the ex-clause. Also add region constraints.
If the parameters fail to unify, then Error
is returned