Trait chalk_engine::context::ContextOps

pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
    fn is_coinductive(&self, goal: &C::UCanonicalGoalInEnvironment) -> bool;
    fn program_clauses(
        &self, 
        environment: &C::Environment, 
        goal: &C::DomainGoal, 
        infer: &mut C::InferenceTable
    ) -> Result<Vec<C::ProgramClause>, Floundered>;
    fn add_clauses(
        &self, 
        env: &C::Environment, 
        clauses: C::ProgramClauses
    ) -> C::Environment;
    fn instantiate_ucanonical_goal(
        &self, 
        arg: &C::UCanonicalGoalInEnvironment
    ) -> (C::InferenceTable, C::Substitution, C::Environment, C::Goal);
    fn instantiate_ex_clause(
        &self, 
        num_universes: usize, 
        canonical_ex_clause: &C::CanonicalExClause
    ) -> (C::InferenceTable, ExClause<C>);
    fn instantiate_answer_subst(
        &self, 
        num_universes: usize, 
        answer: &C::CanonicalAnswerSubst
    ) -> (C::InferenceTable, C::Substitution, Vec<C::RegionConstraint>, Vec<C::GoalInEnvironment>);
    fn constrained_subst_from_answer(
        &self, 
        answer: CompleteAnswer<C>
    ) -> C::CanonicalConstrainedSubst;
    fn identity_constrained_subst(
        &self, 
        goal: &C::UCanonicalGoalInEnvironment
    ) -> C::CanonicalConstrainedSubst;
    fn map_goal_from_canonical(
        &self, 
        _: &C::UniverseMap, 
        value: &C::CanonicalGoalInEnvironment
    ) -> C::CanonicalGoalInEnvironment;
    fn map_subst_from_canonical(
        &self, 
        _: &C::UniverseMap, 
        value: &C::CanonicalAnswerSubst
    ) -> C::CanonicalAnswerSubst;
    fn interner(&self) -> &C::Interner;
    fn into_goal(&self, domain_goal: C::DomainGoal) -> C::Goal;
    fn is_trivial_substitution(
        &self, 
        u_canon: &C::UCanonicalGoalInEnvironment, 
        canonical_subst: &C::CanonicalAnswerSubst
    ) -> bool;
    fn into_hh_goal(&self, goal: C::Goal) -> HhGoal<C>;
}

Required methods

fn is_coinductive(&self, goal: &C::UCanonicalGoalInEnvironment) -> bool

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

fn program_clauses(
    &self,
    environment: &C::Environment,
    goal: &C::DomainGoal,
    infer: &mut C::InferenceTable
) -> Result<Vec<C::ProgramClause>, Floundered>

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

If this callback returns None, that indicates that the set of program clauses cannot be enumerated because there are unresolved type variables that would have to be resolved first; the goal will be considered floundered.

fn add_clauses(
    &self,
    env: &C::Environment,
    clauses: C::ProgramClauses
) -> C::Environment

fn instantiate_ucanonical_goal(
    &self,
    arg: &C::UCanonicalGoalInEnvironment
) -> (C::InferenceTable, C::Substitution, C::Environment, C::Goal)

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

fn instantiate_ex_clause(
    &self,
    num_universes: usize,
    canonical_ex_clause: &C::CanonicalExClause
) -> (C::InferenceTable, ExClause<C>)

fn instantiate_answer_subst(
    &self,
    num_universes: usize,
    answer: &C::CanonicalAnswerSubst
) -> (C::InferenceTable, C::Substitution, Vec<C::RegionConstraint>, Vec<C::GoalInEnvironment>)

fn constrained_subst_from_answer(
    &self,
    answer: CompleteAnswer<C>
) -> C::CanonicalConstrainedSubst

returns unique solution from answer

fn identity_constrained_subst(
    &self,
    goal: &C::UCanonicalGoalInEnvironment
) -> C::CanonicalConstrainedSubst

Returns a identity substitution.

fn map_goal_from_canonical(
    &self,
    _: &C::UniverseMap,
    value: &C::CanonicalGoalInEnvironment
) -> C::CanonicalGoalInEnvironment

Convert a goal G from the canonical universes into our local universes. This will yield a goal G' that is the same but for the universes of universally quantified names.

fn map_subst_from_canonical(
    &self,
    _: &C::UniverseMap,
    value: &C::CanonicalAnswerSubst
) -> C::CanonicalAnswerSubst

Convert a substitution from the canonical universes into our local universes. This will yield a substitution S' that is the same but for the universes of universally quantified names.

fn interner(&self) -> &C::Interner

fn into_goal(&self, domain_goal: C::DomainGoal) -> C::Goal

Upcast this domain goal into a more general goal.

fn is_trivial_substitution(
    &self,
    u_canon: &C::UCanonicalGoalInEnvironment,
    canonical_subst: &C::CanonicalAnswerSubst
) -> bool

fn into_hh_goal(&self, goal: C::Goal) -> HhGoal<C>

Convert the context's goal type into the HhGoal type that the SLG solver understands. The expectation is that the context's goal type has the same set of variants, but with different names and a different setup. If you inspect HhGoal, you will see that this is a "shallow" or "lazy" conversion -- that is, we convert the outermost goal into an HhGoal, but the goals contained within are left as context goals.

Loading content...

Implementors

Loading content...