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

pub trait ContextOps<C: Context> {
    fn is_coinductive(&self, goal: &C::UCanonicalGoalInEnvironment) -> bool;

    fn program_clauses(
        &self, 
        environment: &C::Environment, 
        goal: &C::DomainGoal
    ) -> Vec<C::ProgramClause>;

    fn goal_in_environment(
        environment: &C::Environment, 
        goal: C::Goal
    ) -> C::GoalInEnvironment;

    fn instantiate_ucanonical_goal<R, impl FnOnce(&mut dyn InferenceTable, C::Substitution, C::Environment,
            C::Goal) -> R: FnOnce(&mut InferenceTable<C>, C::Substitution, C::Environment, C::Goal) -> R>(
        &self, 
        arg: &C::UCanonicalGoalInEnvironment, 
        op: impl FnOnce(&mut dyn InferenceTable, C::Substitution, C::Environment,
            C::Goal) -> R
    ) -> R;

    fn instantiate_ex_clause<R, impl FnOnce(&mut dyn InferenceTable, ExClause) -> R: FnOnce(&mut InferenceTable<C>, ExClause<C>) -> R>(
        &self, 
        num_universes: usize, 
        canonical_ex_clause: &C::CanonicalExClause, 
        op: impl FnOnce(&mut dyn InferenceTable, ExClause) -> R
    ) -> R;
}

Required Methods

True if this is a coinductive goal -- e.g., proving an auto trait.

Returns the set of program clauses that might apply to goal. (This set can be over-approximated, naturally.)

Create an inference table for processing a new goal and instantiate that goal in that context, returning "all the pieces".

More specifically: given a u-canonical goal arg, creates a new inference table T and populates it with the universes found in arg. Then, creates a substitution S that maps each bound variable in arg to a fresh inference variable from T. Returns:

  • the table T
  • the substitution S
  • the environment and goal found by substitution S into arg

Implementors