Skip to content

Commit

Permalink
Simplify program clause methods
Browse files Browse the repository at this point in the history
  • Loading branch information
nathanwhit authored and jackh726 committed Dec 9, 2020
1 parent cc4778e commit d719618
Show file tree
Hide file tree
Showing 3 changed files with 24 additions and 27 deletions.
7 changes: 1 addition & 6 deletions chalk-engine/src/logic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -269,12 +269,7 @@ impl<I: Interner> Forest<I> {
},
universes: goal.universes,
};
let clauses = program_clauses_for_goal(
program,
&canon_domain_goal.canonical.value.environment,
&canon_domain_goal.canonical.value.goal,
&canon_domain_goal.canonical.binders,
);
let clauses = program_clauses_for_goal(program, &canon_domain_goal);
let (infer, subst, InEnvironment { environment, goal }) =
chalk_solve::infer::InferenceTable::from_canonical(
context.program().interner(),
Expand Down
7 changes: 1 addition & 6 deletions chalk-recursive/src/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -205,12 +205,7 @@ trait SolveIterationHelpers<I: Interner>: SolveDatabase<I> {
&self,
canonical_goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
) -> Result<Vec<ProgramClause<I>>, Floundered> {
program_clauses_for_goal(
self.db(),
&canonical_goal.canonical.value.environment,
&canonical_goal.canonical.value.goal,
&canonical_goal.canonical.binders,
)
program_clauses_for_goal(self.db(), &canonical_goal)
}
}

Expand Down
37 changes: 22 additions & 15 deletions chalk-solve/src/clauses.rs
Original file line number Diff line number Diff line change
Expand Up @@ -344,24 +344,28 @@ pub fn push_auto_trait_impls_generator_witness<I: Interner>(
#[instrument(level = "debug", skip(db))]
pub fn program_clauses_for_goal<'db, I: Interner>(
db: &'db dyn RustIrDatabase<I>,
environment: &Environment<I>,
goal: &DomainGoal<I>,
binders: &CanonicalVarKinds<I>,
goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
) -> Result<Vec<ProgramClause<I>>, Floundered> {
let interner = db.interner();

let custom_clauses = db.custom_clauses().into_iter();
let clauses_that_could_match = program_clauses_that_could_match(db, environment, goal, binders)
.map(|cl| cl.into_iter())?;
let clauses_that_could_match =
program_clauses_that_could_match(db, goal).map(|cl| cl.into_iter())?;

let clauses: Vec<ProgramClause<I>> = custom_clauses
.chain(clauses_that_could_match)
.chain(
db.program_clauses_for_env(environment)
db.program_clauses_for_env(&goal.canonical.value.environment)
.iter(interner)
.cloned(),
)
.filter(|c| c.could_match(interner, db.unification_database(), goal))
.filter(|c| {
c.could_match(
interner,
db.unification_database(),
&goal.canonical.value.goal,
)
})
.collect();

debug!(?clauses);
Expand All @@ -373,21 +377,24 @@ pub fn program_clauses_for_goal<'db, I: Interner>(
/// `goal`. This can be any superset of the correct set, but the
/// more precise you can make it, the more efficient solving will
/// be.
#[instrument(level = "debug", skip(db, environment))]
#[instrument(level = "debug", skip(db))]
fn program_clauses_that_could_match<I: Interner>(
db: &dyn RustIrDatabase<I>,
environment: &Environment<I>,
goal: &DomainGoal<I>,
// FIXME: These are the binders for `goal`. We're passing them separately
// because `goal` is not necessarily canonicalized: The recursive solver
// passes the canonical goal; the SLG solver instantiates the goal first.
// (See #568.)
binders: &CanonicalVarKinds<I>,
goal: &UCanonical<InEnvironment<DomainGoal<I>>>,
) -> Result<Vec<ProgramClause<I>>, Floundered> {
let interner = db.interner();
let mut clauses: Vec<ProgramClause<I>> = vec![];
let builder = &mut ClauseBuilder::new(db, &mut clauses);

let UCanonical {
canonical:
Canonical {
value: InEnvironment { environment, goal },
binders,
},
universes: _,
} = goal;

match goal {
DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => {
let self_ty = trait_ref.self_type_parameter(interner);
Expand Down

0 comments on commit d719618

Please sign in to comment.