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

pub trait ContextOps<I: Interner, C: Context<I>>: Sized + Clone + Debug {
    fn is_coinductive(&self, goal: &UCanonical<InEnvironment<Goal<I>>>) -> bool;

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

    fn add_clauses(
        &self, 
        env: &Environment<I>, 
        clauses: ProgramClauses<I>
    ) -> Environment<I>;

    fn instantiate_ucanonical_goal(
        &self, 
        arg: &UCanonical<InEnvironment<Goal<I>>>
    ) -> (C::InferenceTable, Substitution<I>, Environment<I>, Goal<I>);

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

    fn instantiate_answer_subst(
        &self, 
        num_universes: usize, 
        answer: &Canonical<AnswerSubst<I>>
    ) -> (C::InferenceTable, Substitution<I>, Vec<InEnvironment<Constraint<I>>>, Vec<InEnvironment<Goal<I>>>);

    fn identity_constrained_subst(
        &self, 
        goal: &UCanonical<InEnvironment<Goal<I>>>
    ) -> Canonical<ConstrainedSubst<I>>;

    fn map_goal_from_canonical(
        &self, 
        _: &UniverseMap, 
        value: &Canonical<InEnvironment<Goal<I>>>
    ) -> Canonical<InEnvironment<Goal<I>>>;

    fn map_subst_from_canonical(
        &self, 
        _: &UniverseMap, 
        value: &Canonical<AnswerSubst<I>>
    ) -> Canonical<AnswerSubst<I>>;

    fn interner(&self) -> &I;

    fn into_goal(&self, domain_goal: DomainGoal<I>) -> Goal<I>;

    fn is_trivial_constrained_substitution(
        &self, 
        constrained_subst: &Canonical<ConstrainedSubst<I>>
    ) -> bool;

    fn is_trivial_substitution(
        &self, 
        u_canon: &UCanonical<InEnvironment<Goal<I>>>, 
        canonical_subst: &Canonical<AnswerSubst<I>>
    ) -> bool;
}

Required methods

fn is_coinductive(&self, goal: &UCanonical<InEnvironment<Goal<I>>>) -> bool

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

fn program_clauses(
    &self,
    environment: &Environment<I>,
    goal: &DomainGoal<I>,
    infer: &mut C::InferenceTable
) -> Result<Vec<ProgramClause<I>>, 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: &Environment<I>,
    clauses: ProgramClauses<I>
) -> Environment<I>

fn instantiate_ucanonical_goal(
    &self,
    arg: &UCanonical<InEnvironment<Goal<I>>>
) -> (C::InferenceTable, Substitution<I>, Environment<I>, Goal<I>)

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: &Canonical<ExClause<I>>
) -> (C::InferenceTable, ExClause<I>)

fn instantiate_answer_subst(
    &self,
    num_universes: usize,
    answer: &Canonical<AnswerSubst<I>>
) -> (C::InferenceTable, Substitution<I>, Vec<InEnvironment<Constraint<I>>>, Vec<InEnvironment<Goal<I>>>)

fn identity_constrained_subst(
    &self,
    goal: &UCanonical<InEnvironment<Goal<I>>>
) -> Canonical<ConstrainedSubst<I>>

Returns a identity substitution.

fn map_goal_from_canonical(
    &self,
    _: &UniverseMap,
    value: &Canonical<InEnvironment<Goal<I>>>
) -> Canonical<InEnvironment<Goal<I>>>

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,
    _: &UniverseMap,
    value: &Canonical<AnswerSubst<I>>
) -> Canonical<AnswerSubst<I>>

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) -> &I

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

Upcast this domain goal into a more general goal.

fn is_trivial_constrained_substitution(
    &self,
    constrained_subst: &Canonical<ConstrainedSubst<I>>
) -> bool

fn is_trivial_substitution(
    &self,
    u_canon: &UCanonical<InEnvironment<Goal<I>>>,
    canonical_subst: &Canonical<AnswerSubst<I>>
) -> bool

Loading content...

Implementors

Loading content...