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

pub trait ResolventOps<I: Interner> {
    fn resolvent_clause(
        &mut self, 
        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, 
        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,
    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,
    ex_clause: &mut ExClause<I>,
    selected_goal: &InEnvironment<Goal<I>>,
    answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
    canonical_answer_subst: &Canonical<AnswerSubst<I>>
) -> Fallible<()>

Loading content...

Implementors

impl<I: Interner> ResolventOps<I> for TruncatingInferenceTable<I>[src]

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

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
Loading content...