Module chalk_engine::context[][src]

Traits

AggregateOps

Methods for combining solutions to yield an aggregate solution.

AnswerStream
Context

The "context" in which the SLG solver operates. It defines all the types that the SLG solver may need to refer to, as well as a few very simple interconversion methods.

ContextOps
InferenceTable

An "inference table" contains the state to support unification and other operations on terms.

ResolventOps
TruncateOps

"Truncation" (called "abstraction" in the papers referenced below) refers to the act of modifying a goal or answer that has become too large in order to guarantee termination. The SLG solver doesn't care about the precise truncation function, so long as it's deterministic and so forth.

UnificationOps

Methods for unifying and manipulating terms and binders.

WithInstantiatedExClause

Callback trait for instantiate_ex_clause. Unlike the other traits in this file, this is not implemented by the context crate, but rather by code in this crate.

WithInstantiatedUCanonicalGoal

Callback trait for instantiate_ucanonical_goal. Unlike the other traits in this file, this is not implemented by the context crate, but rather by code in this crate.