Trait chalk_engine::slg::ResolventOps

pub trait ResolventOps<I: Interner> {
    // Required methods
    fn resolvent_clause(
        &mut self,
        ops: &dyn UnificationDatabase<I>,
        interner: I,
        environment: &Environment<I>,
        goal: &DomainGoal<I>,
        subst: &Substitution<I>,
        clause: &ProgramClause<I>,
    ) -> Fallible<ExClause<I>>;
    fn apply_answer_subst(
        &mut self,
        interner: I,
        unification_database: &dyn UnificationDatabase<I>,
        ex_clause: &mut ExClause<I>,
        selected_goal: &InEnvironment<Goal<I>>,
        answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
        canonical_answer_subst: Canonical<AnswerSubst<I>>,
    ) -> Fallible<()>;
}

Required Methods

fn resolvent_clause( &mut self, ops: &dyn UnificationDatabase<I>, interner: I, environment: &Environment<I>, goal: &DomainGoal<I>, subst: &Substitution<I>, clause: &ProgramClause<I>, ) -> Fallible<ExClause<I>>

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: I, unification_database: &dyn UnificationDatabase<I>, ex_clause: &mut ExClause<I>, selected_goal: &InEnvironment<Goal<I>>, answer_table_goal: &Canonical<InEnvironment<Goal<I>>>, canonical_answer_subst: Canonical<AnswerSubst<I>>, ) -> Fallible<()>

Implementations on Foreign Types

impl<I: Interner> ResolventOps<I> for InferenceTable<I>

fn resolvent_clause( &mut self, db: &dyn UnificationDatabase<I>, interner: I, environment: &Environment<I>, goal: &DomainGoal<I>, subst: &Substitution<I>, clause: &ProgramClause<I>, ) -> Fallible<ExClause<I>>

Applies the SLG resolvent algorithm to incorporate a program clause into the main X-clause, producing a new X-clause that must be solved.

Parameters

• goal is the goal G that we are trying to solve
• clause is the program clause that may be useful to that end

fn apply_answer_subst( &mut self, interner: I, unification_database: &dyn UnificationDatabase<I>, ex_clause: &mut ExClause<I>, selected_goal: &InEnvironment<Goal<I>>, answer_table_goal: &Canonical<InEnvironment<Goal<I>>>, canonical_answer_subst: Canonical<AnswerSubst<I>>, ) -> Fallible<()>

Implementors