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

pub trait ResolventOps<C: Context> {
    fn resolvent_clause(
        &mut self, 
        environment: &C::Environment, 
        goal: &C::DomainGoal, 
        subst: &C::Substitution, 
        clause: &C::ProgramClause
    ) -> Fallible<C::CanonicalExClause>;

    fn apply_answer_subst(
        &mut self, 
        ex_clause: ExClause<C>, 
        selected_goal: &C::GoalInEnvironment, 
        answer_table_goal: &C::CanonicalGoalInEnvironment, 
        canonical_answer_subst: &C::CanonicalConstrainedSubst
    ) -> Fallible<ExClause<C>>;
}

Required Methods

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.

Implementors