Trait chalk_engine::slg::ResolventOps [−][src]
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>>
[src]
&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<()>
[src]
&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>
[src]
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>>
[src]
&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 solveclause
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<()>
[src]
&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<()>