Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Only generate clauses requiring Compatible when it is in the environment #566

Merged
merged 1 commit into from
Jul 17, 2020
Merged

Only generate clauses requiring Compatible when it is in the environment #566

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions chalk-integration/src/query.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -172,20 +172,22 @@ fn environment(db: &impl LoweringDatabase) -> Result<Arc<ProgramEnvironment>, Ch

let builder = &mut ClauseBuilder::new(db, &mut program_clauses);

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This function (environment), from what I can tell is a bit of a relic. It's only used bench and in the REPL (when you call "lowered"). It can probably just be removed (along with bench tbh). But that's a separate PR.

let env = chalk_ir::Environment::new(builder.interner());

program
.associated_ty_data
.values()
.for_each(|d| d.to_program_clauses(builder));
.for_each(|d| d.to_program_clauses(builder, &env));

program
.trait_data
.values()
.for_each(|d| d.to_program_clauses(builder));
.for_each(|d| d.to_program_clauses(builder, &env));

program
.adt_data
.values()
.for_each(|d| d.to_program_clauses(builder));
.for_each(|d| d.to_program_clauses(builder, &env));

for (&auto_trait_id, _) in program
.trait_data
Expand All @@ -201,12 +203,12 @@ fn environment(db: &impl LoweringDatabase) -> Result<Arc<ProgramEnvironment>, Ch
// If we encounter a negative impl, do not generate any rule. Negative impls
// are currently just there to deactivate default impls for auto traits.
if datum.is_positive() {
datum.to_program_clauses(builder);
datum.to_program_clauses(builder, &env);
datum
.associated_ty_value_ids
.iter()
.map(|&atv_id| db.associated_ty_value(atv_id))
.for_each(|atv| atv.to_program_clauses(builder));
.for_each(|atv| atv.to_program_clauses(builder, &env));
}
}

Expand Down
19 changes: 19 additions & 0 deletions chalk-ir/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,25 @@ impl<I: Interner> Environment<I> {
ProgramClauses::from_iter(interner, env.clauses.iter(interner).cloned().chain(clauses));
env
}

/// True if any of the clauses in the environment have a consequence of `Compatible`.
/// Panics if the conditions or constraints of that clause are not empty.
pub fn has_compatible_clause(&self, interner: &I) -> bool {
self.clauses.as_slice(interner).iter().any(|c| {
let ProgramClauseData(implication) = c.data(interner);
match implication.skip_binders().consequence {
DomainGoal::Compatible => {
// We currently don't generate `Compatible` with any conditions or constraints
// If this was needed, for whatever reason, then a third "yes, but must evaluate"
// return value would have to be added.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

not really necessary if the clauses code continues to generate clauses that have Compatible as a condition where required, right?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that's true. This wording is a bit conservative.

assert!(implication.skip_binders().conditions.is_empty(interner));
assert!(implication.skip_binders().constraints.is_empty(interner));
true
}
_ => false,
}
})
}
}

/// A goal with an environment to solve it in.
Expand Down
93 changes: 63 additions & 30 deletions chalk-solve/src/clauses.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -238,14 +238,15 @@ fn program_clauses_that_could_match<I: Interner>(

// This is needed for the coherence related impls, as well
// as for the `Implemented(Foo) :- FromEnv(Foo)` rule.
trait_datum.to_program_clauses(builder);
trait_datum.to_program_clauses(builder, environment);

for impl_id in db.impls_for_trait(
trait_ref.trait_id,
trait_ref.substitution.as_slice(interner),
binders,
) {
db.impl_datum(impl_id).to_program_clauses(builder);
db.impl_datum(impl_id)
.to_program_clauses(builder, environment);
}

// If this is a `Foo: Send` (or any auto-trait), then add
Expand Down Expand Up @@ -288,7 +289,25 @@ fn program_clauses_that_could_match<I: Interner>(
..
})
| TyData::Alias(AliasTy::Opaque(OpaqueTy { opaque_ty_id, .. })) => {
db.opaque_ty_data(*opaque_ty_id).to_program_clauses(builder);
db.opaque_ty_data(*opaque_ty_id)
.to_program_clauses(builder, environment);
}
_ => {}
}

// We don't actually do anything here, but we need to record the types it when logging
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This surprised me a bit. But I can't think of a better way to handle it.
The problem here is that foo: Sized (where foo is a function) doesn't actually call fn_def_datum. So the LoggingRustIrDatabase doesn't pick it up. This could be removed when the that actually records the goals too.

match self_ty.data(interner) {
TyData::Apply(ApplicationTy {
name: TypeName::Adt(adt_id),
..
}) => {
let _ = db.adt_datum(*adt_id);
}
TyData::Apply(ApplicationTy {
name: TypeName::FnDef(fn_def_id),
..
}) => {
let _ = db.fn_def_datum(*fn_def_id);
}
_ => {}
}
Expand All @@ -309,7 +328,8 @@ fn program_clauses_that_could_match<I: Interner>(
..
})
| TyData::Alias(AliasTy::Opaque(OpaqueTy { opaque_ty_id, .. })) => {
db.opaque_ty_data(*opaque_ty_id).to_program_clauses(builder);
db.opaque_ty_data(*opaque_ty_id)
.to_program_clauses(builder, environment);
}
_ => {}
}
Expand All @@ -322,11 +342,11 @@ fn program_clauses_that_could_match<I: Interner>(
}

db.associated_ty_data(proj.associated_ty_id)
.to_program_clauses(builder)
.to_program_clauses(builder, environment)
}
AliasTy::Opaque(opaque_ty) => db
.opaque_ty_data(opaque_ty.opaque_ty_id)
.to_program_clauses(builder),
.to_program_clauses(builder, environment),
},
DomainGoal::Holds(WhereClause::LifetimeOutlives(..)) => {
builder.push_bound_lifetime(|builder, a| {
Expand Down Expand Up @@ -363,7 +383,7 @@ fn program_clauses_that_could_match<I: Interner>(
DomainGoal::WellFormed(WellFormed::Trait(trait_ref))
| DomainGoal::LocalImplAllowed(trait_ref) => {
db.trait_datum(trait_ref.trait_id)
.to_program_clauses(builder);
.to_program_clauses(builder, environment);
}
DomainGoal::ObjectSafe(trait_id) => {
if builder.db.is_object_safe(*trait_id) {
Expand Down Expand Up @@ -414,18 +434,21 @@ fn program_clauses_that_could_match<I: Interner>(

push_program_clauses_for_associated_type_values_in_impls_of(
builder,
environment,
trait_id,
trait_parameters,
binders,
);

push_clauses_for_compatible_normalize(
db,
builder,
interner,
trait_id,
proj.associated_ty_id,
);
if environment.has_compatible_clause(interner) {
push_clauses_for_compatible_normalize(
db,
builder,
interner,
trait_id,
proj.associated_ty_id,
);
}
}
AliasTy::Opaque(_) => (),
},
Expand Down Expand Up @@ -509,6 +532,7 @@ fn push_clauses_for_compatible_normalize<I: Interner>(
#[instrument(level = "debug", skip(builder))]
fn push_program_clauses_for_associated_type_values_in_impls_of<I: Interner>(
builder: &mut ClauseBuilder<'_, I>,
environment: &Environment<I>,
trait_id: TraitId<I>,
trait_parameters: &[GenericArg<I>],
binders: &CanonicalVarKinds<I>,
Expand All @@ -527,7 +551,7 @@ fn push_program_clauses_for_associated_type_values_in_impls_of<I: Interner>(
for &atv_id in &impl_datum.associated_ty_value_ids {
let atv = builder.db.associated_ty_value(atv_id);
debug!(?atv_id, ?atv);
atv.to_program_clauses(builder);
atv.to_program_clauses(builder, environment);
}
}
}
Expand All @@ -550,18 +574,18 @@ fn match_ty<I: Interner>(
) -> Result<(), Floundered> {
let interner = builder.interner();
Ok(match ty.data(interner) {
TyData::Apply(application_ty) => match_type_name(builder, interner, application_ty),
TyData::Apply(application_ty) => match_type_name(builder, environment, application_ty),
TyData::Placeholder(_) => {
builder.push_clause(WellFormed::Ty(ty.clone()), Some(FromEnv::Ty(ty.clone())));
}
TyData::Alias(AliasTy::Projection(proj)) => builder
.db
.associated_ty_data(proj.associated_ty_id)
.to_program_clauses(builder),
.to_program_clauses(builder, environment),
TyData::Alias(AliasTy::Opaque(opaque_ty)) => builder
.db
.opaque_ty_data(opaque_ty.opaque_ty_id)
.to_program_clauses(builder),
.to_program_clauses(builder, environment),
TyData::Function(quantified_ty) => {
builder.push_fact(WellFormed::Ty(ty.clone()));
quantified_ty
Expand All @@ -579,24 +603,28 @@ fn match_ty<I: Interner>(
/// Lower a Rust IR application type to logic
fn match_type_name<I: Interner>(
builder: &mut ClauseBuilder<'_, I>,
interner: &I,
environment: &Environment<I>,
application: &ApplicationTy<I>,
) {
let interner = builder.interner();
match application.name {
TypeName::Adt(adt_id) => match_adt(builder, adt_id),
TypeName::Adt(adt_id) => builder
.db
.adt_datum(adt_id)
.to_program_clauses(builder, environment),
TypeName::OpaqueType(opaque_ty_id) => builder
.db
.opaque_ty_data(opaque_ty_id)
.to_program_clauses(builder),
.to_program_clauses(builder, environment),
TypeName::Error => {}
TypeName::AssociatedType(type_id) => builder
.db
.associated_ty_data(type_id)
.to_program_clauses(builder),
.to_program_clauses(builder, environment),
TypeName::FnDef(fn_def_id) => builder
.db
.fn_def_datum(fn_def_id)
.to_program_clauses(builder),
.to_program_clauses(builder, environment),
TypeName::Tuple(_)
| TypeName::Scalar(_)
| TypeName::Str
Expand All @@ -611,20 +639,20 @@ fn match_type_name<I: Interner>(
}
}

fn match_alias_ty<I: Interner>(builder: &mut ClauseBuilder<'_, I>, alias: &AliasTy<I>) {
fn match_alias_ty<I: Interner>(
builder: &mut ClauseBuilder<'_, I>,
environment: &Environment<I>,
alias: &AliasTy<I>,
) {
match alias {
AliasTy::Projection(projection_ty) => builder
.db
.associated_ty_data(projection_ty.associated_ty_id)
.to_program_clauses(builder),
.to_program_clauses(builder, environment),
_ => (),
}
}

fn match_adt<I: Interner>(builder: &mut ClauseBuilder<'_, I>, adt_id: AdtId<I>) {
builder.db.adt_datum(adt_id).to_program_clauses(builder)
}

pub fn program_clauses_for_env<'db, I: Interner>(
db: &'db dyn RustIrDatabase<I>,
environment: &Environment<I>,
Expand All @@ -638,7 +666,12 @@ pub fn program_clauses_for_env<'db, I: Interner>(
let mut closure = last_round.clone();
let mut next_round = FxHashSet::default();
while !last_round.is_empty() {
elaborate_env_clauses(db, &last_round.drain().collect::<Vec<_>>(), &mut next_round);
elaborate_env_clauses(
db,
&last_round.drain().collect::<Vec<_>>(),
&mut next_round,
environment,
);
last_round.extend(
next_round
.drain()
Expand Down
26 changes: 17 additions & 9 deletions chalk-solve/src/clauses/env_elaborator.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ use crate::Ty;
use crate::{debug_span, TyData};
use chalk_ir::interner::Interner;
use chalk_ir::visit::{Visit, Visitor};
use chalk_ir::DebruijnIndex;
use chalk_ir::{DebruijnIndex, Environment};
use rustc_hash::FxHashSet;
use tracing::instrument;

Expand All @@ -23,10 +23,11 @@ pub(super) fn elaborate_env_clauses<I: Interner>(
db: &dyn RustIrDatabase<I>,
in_clauses: &[ProgramClause<I>],
out: &mut FxHashSet<ProgramClause<I>>,
environment: &Environment<I>,
) {
let mut this_round = vec![];
in_clauses.visit_with(
&mut EnvElaborator::new(db, &mut this_round),
&mut EnvElaborator::new(db, &mut this_round, environment),
DebruijnIndex::INNERMOST,
);
out.extend(this_round);
Expand All @@ -35,13 +36,19 @@ pub(super) fn elaborate_env_clauses<I: Interner>(
struct EnvElaborator<'me, I: Interner> {
db: &'me dyn RustIrDatabase<I>,
builder: ClauseBuilder<'me, I>,
environment: &'me Environment<I>,
}

impl<'me, I: Interner> EnvElaborator<'me, I> {
fn new(db: &'me dyn RustIrDatabase<I>, out: &'me mut Vec<ProgramClause<I>>) -> Self {
fn new(
db: &'me dyn RustIrDatabase<I>,
out: &'me mut Vec<ProgramClause<I>>,
environment: &'me Environment<I>,
) -> Self {
EnvElaborator {
db,
builder: ClauseBuilder::new(db, out),
environment,
}
}
}
Expand All @@ -58,12 +65,13 @@ impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> {
}
#[instrument(level = "debug", skip(self, _outer_binder))]
fn visit_ty(&mut self, ty: &Ty<I>, _outer_binder: DebruijnIndex) {
let interner = self.db.interner();
match ty.data(interner) {
match ty.data(self.interner()) {
TyData::Apply(application_ty) => {
match_type_name(&mut self.builder, interner, application_ty)
match_type_name(&mut self.builder, self.environment, application_ty)
}
TyData::Alias(alias_ty) => {
match_alias_ty(&mut self.builder, self.environment, alias_ty)
}
TyData::Alias(alias_ty) => match_alias_ty(&mut self.builder, alias_ty),
TyData::Placeholder(_) => {}

// FIXME(#203) -- We haven't fully figured out the implied
Expand All @@ -81,15 +89,15 @@ impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> {
FromEnv::Trait(trait_ref) => {
let trait_datum = self.db.trait_datum(trait_ref.trait_id);

trait_datum.to_program_clauses(&mut self.builder);
trait_datum.to_program_clauses(&mut self.builder, self.environment);

// If we know that `T: Iterator`, then we also know
// things about `<T as Iterator>::Item`, so push those
// implied bounds too:
for &associated_ty_id in &trait_datum.associated_ty_ids {
self.db
.associated_ty_data(associated_ty_id)
.to_program_clauses(&mut self.builder);
.to_program_clauses(&mut self.builder, self.environment);
}
}
FromEnv::Ty(ty) => ty.visit_with(self, outer_binder),
Expand Down
Loading