Skip to content

Commit

Permalink
Auto merge of #624 - nathanwhit:slg-program-clauses, r=nikomatsakis
Browse files Browse the repository at this point in the history 
Pass canonical goals to program clauses code in SLG solver

It seemed like we were leaning towards this solution in the [design meeting](https://rust-lang.zulipchat.com/#narrow/stream/144729-wg-traits/topic/meeting.202020-09-22), and it turned out (assuming these changes are right) to be pretty straightforward.

Closes #568.

This should stop seeing issues related to failing to generalize program clauses pop up, but I'm only going to cc #614 since I'd like some tests maybe.
  • Loading branch information
@bors
bors committed Dec 10, 2020
2 parents 8122127 + 0b391f8 commit 44b6627
Show file tree
Hide file tree
Showing 3 changed files with 69 additions and 46 deletions.
60 changes: 36 additions & 24 deletions chalk-engine/src/logic.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ use crate::{

use chalk_ir::interner::Interner;
use chalk_ir::{
AnswerSubst, Canonical, CanonicalVarKinds, ConstrainedSubst, FallibleOrFloundered, Floundered,
Goal, GoalData, InEnvironment, NoSolution, Substitution, UCanonical, UniverseMap,
AnswerSubst, Canonical, ConstrainedSubst, FallibleOrFloundered, Floundered, Goal, GoalData,
InEnvironment, NoSolution, Substitution, UCanonical, UniverseMap,
};
use chalk_solve::clauses::program_clauses_for_goal;
use chalk_solve::coinductive_goal::IsCoinductive;
Expand Down Expand Up @@ -253,24 +253,30 @@ impl<I: Interner> Forest<I> {
) -> Table<I> {
let coinductive = goal.is_coinductive(context.program());
let mut table = Table::new(goal.clone(), coinductive);
let (infer, subst, InEnvironment { environment, goal }) =
chalk_solve::infer::InferenceTable::from_canonical(
context.program().interner(),
goal.universes,
goal.canonical,
);
let mut infer = TruncatingInferenceTable::new(context.max_size(), infer);
let goal_data = goal.data(context.program().interner());

let goal_data = goal.canonical.value.goal.data(context.program().interner());
match goal_data {
GoalData::DomainGoal(domain_goal) => {
let program = context.program();
let clauses = program_clauses_for_goal(
program,
&environment,
&domain_goal,
&CanonicalVarKinds::empty(program.interner()),
);

let canon_domain_goal = UCanonical {
canonical: Canonical {
binders: goal.canonical.binders,
value: InEnvironment::new(
&goal.canonical.value.environment,
domain_goal.clone(),
),
},
universes: goal.universes,
};
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(),
canon_domain_goal.universes,
canon_domain_goal.canonical,
);
let infer = TruncatingInferenceTable::new(context.max_size(), infer);

match clauses {
Ok(clauses) => {
Expand All @@ -281,7 +287,7 @@ impl<I: Interner> Forest<I> {
context.unification_database(),
context.program().interner(),
&environment,
&domain_goal,
&goal,
&subst,
&clause,
) {
Expand Down Expand Up @@ -309,13 +315,19 @@ impl<I: Interner> Forest<I> {
}

_ => {
// `canonical_goal` is a goal. We can simplify it
// into a series of *literals*, all of which must be
// true. Thus, in EWFS terms, we are effectively
// creating a single child of the `A :- A` goal that
// is like `A :- B, C, D` where B, C, and D are the
// simplified subgoals. You can think of this as
// applying built-in "meta program clauses" that
let (infer, subst, InEnvironment { environment, goal }) =
chalk_solve::infer::InferenceTable::from_canonical(
context.program().interner(),
goal.universes,
goal.canonical,
);
let mut infer = TruncatingInferenceTable::new(context.max_size(), infer);
// The goal for this table is not a domain goal, so we instead
// simplify it into a series of *literals*, all of which must be
// true. Thus, in EWFS terms, we are effectively creating a
// single child of the `A :- A` goal that is like `A :- B, C, D`
// where B, C, and D are the simplified subgoals. You can think
// of this as applying built-in "meta program clauses" that
// reduce goals into Domain goals.
match Self::simplify_goal(context, &mut infer, subst, environment, goal) {
FallibleOrFloundered::Ok(ex_clause) => {
Expand Down
7 changes: 1 addition & 6 deletions chalk-recursive/src/solve.rs
View file
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
48 changes: 32 additions & 16 deletions chalk-solve/src/clauses.rs
View file
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 All @@ -396,6 +403,9 @@ fn program_clauses_that_could_match<I: Interner>(
let trait_datum = db.trait_datum(trait_id);

match self_ty.kind(interner) {
TyKind::InferenceVar(_, _) => {
panic!("Inference vars not allowed when getting program clauses")
}
TyKind::Alias(alias) => {
// An alias could normalize to anything, including `dyn trait`
// or an opaque type, so push a clause that asks for the
Expand Down Expand Up @@ -583,6 +593,9 @@ fn program_clauses_that_could_match<I: Interner>(
let trait_datum = db.trait_datum(trait_id);

let self_ty = alias.self_type_parameter(interner);
if let TyKind::InferenceVar(_, _) = self_ty.kind(interner) {
panic!("Inference vars not allowed when getting program clauses");
}

// Flounder if the self-type is unknown and the trait is non-enumerable.
//
Expand Down Expand Up @@ -840,6 +853,9 @@ fn match_ty<I: Interner>(
) -> Result<(), Floundered> {
let interner = builder.interner();
Ok(match ty.kind(interner) {
TyKind::InferenceVar(_, _) => {
panic!("Inference vars not allowed when getting program clauses")
}
TyKind::Adt(adt_id, _) => builder
.db
.adt_datum(*adt_id)
Expand Down Expand Up @@ -883,7 +899,7 @@ fn match_ty<I: Interner>(
TyKind::Function(_quantified_ty) => {
builder.push_fact(WellFormed::Ty(ty.clone()));
}
TyKind::BoundVar(_) | TyKind::InferenceVar(_, _) => return Err(Floundered),
TyKind::BoundVar(_) => return Err(Floundered),
TyKind::Dyn(dyn_ty) => {
// FIXME(#203)
// - Object safety? (not needed with RFC 2027)
Expand Down

0 comments on commit 44b6627

Please sign in to comment.