[−][src]Trait chalk_engine::context::UnificationOps

pub trait UnificationOps<I: Interner, C: Context<I>> {
    fn instantiate_binders_universally(
        &mut self, 
        interner: &I, 
        arg: &Binders<Goal<I>>
    ) -> Goal<I>;

    fn instantiate_binders_existentially(
        &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>;

    fn fully_canonicalize_goal(
        &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>>;

    fn canonicalize_constrained_subst(
        &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>>;

    fn invert_goal(
        &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<()>;
}

Methods for unifying and manipulating terms and binders.

Required methods

fn instantiate_binders_universally(
    &mut self,
    interner: &I,
    arg: &Binders<Goal<I>>
) -> Goal<I>

fn instantiate_binders_existentially(
    &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>

fn fully_canonicalize_goal(
    &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>>

fn canonicalize_constrained_subst(
    &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>>

fn invert_goal(
    &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<()>

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

Loading content...

Implementors

Loading content...