Trait chalk_engine::context::ResolventOps

pub trait ResolventOps<C: Context> {
    fn resolvent_clause(
        &mut self, 
        interner: &C::Interner, 
        environment: &C::Environment, 
        goal: &C::DomainGoal, 
        subst: &C::Substitution, 
        clause: &C::ProgramClause
    ) -> Fallible<ExClause<C>>;
    fn apply_answer_subst(
        &mut self, 
        interner: &C::Interner, 
        ex_clause: &mut ExClause<C>, 
        selected_goal: &C::GoalInEnvironment, 
        answer_table_goal: &C::CanonicalGoalInEnvironment, 
        canonical_answer_subst: &C::CanonicalAnswerSubst
    ) -> Fallible<()>;
}

Required methods

fn resolvent_clause(
    &mut self,
    interner: &C::Interner,
    environment: &C::Environment,
    goal: &C::DomainGoal,
    subst: &C::Substitution,
    clause: &C::ProgramClause
) -> Fallible<ExClause<C>>

Combines the goal (instantiated within infer) with the given program clause to yield the start of a new strand (a canonical ex-clause).

The bindings in infer are unaffected by this operation.

fn apply_answer_subst(
    &mut self,
    interner: &C::Interner,
    ex_clause: &mut ExClause<C>,
    selected_goal: &C::GoalInEnvironment,
    answer_table_goal: &C::CanonicalGoalInEnvironment,
    canonical_answer_subst: &C::CanonicalAnswerSubst
) -> Fallible<()>

Loading content...

Implementors

Loading content...