Skip to content

馃殌 create a query for the program clauses needed to solve a given goal#49600

Description

@nikomatsakis

One of the key parts of the interface between the Chalk Solver and rustc is when the solver requests the program clauses to solve a given goal:

    /// Returns the set of program clauses that might apply to
    /// `goal`. (This set can be over-approximated, naturally.)
    fn program_clauses(
        &self,
        environment: &I::Environment,
        goal: &I::DomainGoal,
    ) -> Vec<I::ProgramClause>;

In Rustc, this is our chance to do some queries and figure out the full set of clauses. This is building on the work in #49177, where we create the lowering rules for a trait, item, etc (see also the rustc guide coverage).

The set of clauses is somewhat specific to the domain goal:

  • Implemented(P0: Trait<...>)
  • FromEnv(P0: Trait<..>)
    • these come -- ultimately -- from the param environment
    • but because of implied bounds rules we need to combine with the rules from traits
    • we need to compute transitive closure of traits reachable from the env and combine their program clauses, or else iterate over "all traits" (which is actually not easy)
    • I have some code working towards this on my WIP branch for this issue
  • ... the rest have to be written out :)

I'll probably keep iterating on this, but if somebody is keen to hack on it, I'd love to collaborate.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

A-trait-systemArea: Trait systemC-enhancementCategory: An issue proposing an enhancement or a PR with one.T-langRelevant to the language team

Type

No type

Projects

No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions