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.

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

Recursive solver #372

Merged
merged 50 commits into from
Apr 15, 2020
Merged
Show file tree
Hide file tree
Changes from 49 commits
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
126bf6f
Add back the code for the recursive solver (not yet building)
flodiebold Mar 8, 2020
9bb94d1
Getting past name resolution errors
flodiebold Mar 8, 2020
6fc0808
Fix many errors
flodiebold Mar 8, 2020
b10ae55
Fix more errors
flodiebold Mar 8, 2020
d9e1a55
Fix another error
flodiebold Mar 8, 2020
22bfbc0
Fix another error
flodiebold Mar 8, 2020
8209476
Fix the next error, method resolution succeeds
flodiebold Mar 8, 2020
311eb33
Fix remaining errors
flodiebold Mar 8, 2020
298c3b9
Add recursive solver to SolverChoice
flodiebold Mar 8, 2020
d3267cf
Temporary: Use recursive solver by default in tests
flodiebold Mar 8, 2020
52dc02a
Delete unused file
flodiebold Mar 8, 2020
faae7fd
Fix dyn_Foo_Bar failure
flodiebold Mar 11, 2020
30fe8c5
Clause priorities (WIP)
flodiebold Mar 17, 2020
64c9215
Disable currently non-existent caching
flodiebold Mar 17, 2020
9ee8178
Check for input equality
flodiebold Mar 17, 2020
27bc264
Ignore tests currently overflowing/infinitely looping (REMOVE AGAIN)
flodiebold Mar 17, 2020
47a473c
Projection equality test is fixed
flodiebold Mar 17, 2020
9c27db6
Sort constraints in tests
flodiebold Mar 17, 2020
fa6dd01
Implement floundering for too-general goals, like the SLG solver
flodiebold Mar 18, 2020
a81d345
Truncate goals like in the SLG solver
flodiebold Mar 18, 2020
d8ed629
Revert "Ignore tests currently overflowing/infinitely looping (REMOVE…
flodiebold Mar 18, 2020
3e8c1ae
Add back the old caching for now
flodiebold Mar 22, 2020
de95b37
Keep track of clause priority for longer to avoid infinite loop
flodiebold Mar 22, 2020
9ab02e2
Flounder for AliasEq with unspecific self type as well
flodiebold Mar 24, 2020
e661d85
Rebase fixes
flodiebold Mar 27, 2020
7e48a62
Truncate when adding obligations to avoid messing up the progress ass…
flodiebold Mar 27, 2020
04b57da
Rebase fixes
flodiebold Mar 30, 2020
b1453e5
Undo floundering for AliasEq, it's not the right approach
flodiebold Mar 30, 2020
3a074e4
Move floundering logic to program_clauses
flodiebold Mar 31, 2020
ea15431
Run tests with both solvers by default
flodiebold Apr 5, 2020
62b0da6
Fix futures_ambiguity test
flodiebold Apr 5, 2020
9374586
Make program_clauses_for_env add the actual env clauses as well
flodiebold Apr 5, 2020
27f9ef7
Rebase fixes
flodiebold Apr 10, 2020
60b3892
Use Floundered error in program_clauses
flodiebold Apr 10, 2020
835fa68
Make the prioritization code slightly nicer
flodiebold Apr 10, 2020
9166f3e
Add another test
flodiebold Apr 10, 2020
2d193f3
Move generalizer to its own module
flodiebold Apr 10, 2020
d69da2f
Add back Normalize floundering
flodiebold Apr 11, 2020
31d6f2a
Increase hard-coded max size to 30
flodiebold Apr 11, 2020
f6c1623
Add some more tests
flodiebold Apr 14, 2020
0abdef9
Don't inherit clause priority in implications
flodiebold Apr 14, 2020
2316ca6
Remove AliasTy::type_parameters
flodiebold Apr 14, 2020
8fcad2f
Address some review comments
flodiebold Apr 14, 2020
5768375
ensure all tests run for recursive solve
nikomatsakis Apr 14, 2020
13b66f1
don't silently ignore recursive solver
nikomatsakis Apr 14, 2020
72be500
Move recursive module from mod.rs to recursive.rs
flodiebold Apr 15, 2020
a952c87
add some more projection tests
nikomatsakis Apr 15, 2020
77f262f
Rebase fixes; flounder instead of truncating, like SLG
flodiebold Apr 15, 2020
b032df6
Use combine_with_priorities when combining answers from cycles as well
flodiebold Apr 15, 2020
2aa90be
cite chalk#399 in the fixme
nikomatsakis Apr 15, 2020
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
5 changes: 3 additions & 2 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
use chalk_ir::cast::{Cast, Caster};
use chalk_ir::interner::ChalkIr;
use chalk_ir::{
self, AssocTypeId, BoundVar, DebruijnIndex, ImplId, QuantifiedWhereClauses, StructId,
Substitution, TraitId,
self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, QuantifiedWhereClauses,
StructId, Substitution, TraitId,
};
use chalk_parse::ast::*;
use chalk_rust_ir as rust_ir;
Expand Down Expand Up @@ -1193,6 +1193,7 @@ impl LowerClause for Clause {
.map(|consequence| chalk_ir::ProgramClauseImplication {
consequence,
conditions: conditions.clone(),
priority: ClausePriority::High,
})
.collect::<Vec<_>>();
Ok(implications)
Expand Down
2 changes: 2 additions & 0 deletions chalk-ir/src/cast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -187,6 +187,7 @@ where
ProgramClauseData::Implies(ProgramClauseImplication {
consequence: self.cast(interner),
conditions: Goals::new(interner),
priority: ClausePriority::High,
})
.intern(interner)
}
Expand All @@ -201,6 +202,7 @@ where
ProgramClauseData::ForAll(self.map(|bound| ProgramClauseImplication {
consequence: bound.cast(interner),
conditions: Goals::new(interner),
priority: ClausePriority::High,
}))
.intern(interner)
}
Expand Down
1 change: 1 addition & 0 deletions chalk-ir/src/fold/boring_impls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -243,6 +243,7 @@ copy_fold!(DebruijnIndex);
copy_fold!(chalk_engine::TableIndex);
copy_fold!(chalk_engine::TimeStamp);
copy_fold!(());
copy_fold!(ClausePriority);

#[macro_export]
macro_rules! id_fold {
Expand Down
69 changes: 68 additions & 1 deletion chalk-ir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -229,6 +229,14 @@ impl<I: Interner> Ty<I> {
}
}

/// Returns true if this is a `BoundVar` or `InferenceVar`.
pub fn is_var(&self, interner: &I) -> bool {
match self.data(interner) {
TyData::BoundVar(_) | TyData::InferenceVar(_) => true,
_ => false,
}
}

pub fn is_alias(&self, interner: &I) -> bool {
match self.data(interner) {
TyData::Alias(..) => true,
Expand Down Expand Up @@ -547,7 +555,7 @@ impl DebruijnIndex {
/// known. It is referenced within the type using `^1`, indicating
/// a bound type with debruijn index 1 (i.e., skipping through one
/// level of binder).
#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit)]
#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)]
pub struct DynTy<I: Interner> {
pub bounds: Binders<QuantifiedWhereClauses<I>>,
}
Expand Down Expand Up @@ -839,6 +847,14 @@ impl<I: Interner> AliasTy<I> {
pub fn intern(self, interner: &I) -> Ty<I> {
Ty::new(interner, self)
}

pub fn self_type_parameter(&self, interner: &I) -> Ty<I> {
self.substitution
.iter(interner)
.find_map(move |p| p.ty(interner))
.unwrap()
.clone()
}
}

#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, HasInterner)]
Expand Down Expand Up @@ -1106,6 +1122,15 @@ impl<I: Interner> DomainGoal<I> {
goal => goal,
}
}

pub fn inputs(&self, interner: &I) -> Vec<Parameter<I>> {
match self {
DomainGoal::Holds(WhereClause::AliasEq(alias_eq)) => {
vec![ParameterKind::Ty(alias_eq.alias.clone().intern(interner)).intern(interner)]
}
_ => Vec::new(),
}
}
}

#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit)]
Expand Down Expand Up @@ -1304,6 +1329,23 @@ impl<V: IntoIterator> Iterator for BindersIntoIterator<V> {
pub struct ProgramClauseImplication<I: Interner> {
pub consequence: DomainGoal<I>,
pub conditions: Goals<I>,
pub priority: ClausePriority,
}

#[derive(Copy, Clone, PartialEq, Eq, Hash, Debug)]
pub enum ClausePriority {
High,
Low,
}

impl std::ops::BitAnd for ClausePriority {
type Output = ClausePriority;
fn bitand(self, rhs: ClausePriority) -> Self::Output {
match (self, rhs) {
(ClausePriority::High, ClausePriority::High) => ClausePriority::High,
_ => ClausePriority::Low,
}
}
}

#[derive(Clone, PartialEq, Eq, Hash, Fold, HasInterner)]
Expand All @@ -1318,6 +1360,7 @@ impl<I: Interner> ProgramClauseImplication<I> {
ProgramClauseImplication {
consequence: self.consequence.into_from_env_goal(interner),
conditions: self.conditions.clone(),
priority: self.priority,
}
} else {
self
Expand Down Expand Up @@ -1466,6 +1509,30 @@ impl<T> UCanonical<T> {
);
subst.is_identity_subst(interner)
}

pub fn trivial_substitution<I: Interner>(&self, interner: &I) -> Substitution<I> {
let binders = &self.canonical.binders;
Substitution::from(
interner,
binders
.iter()
.enumerate()
.map(|(index, pk)| {
let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, index);
match pk {
ParameterKind::Ty(_) => {
ParameterKind::Ty(TyData::BoundVar(bound_var).intern(interner))
.intern(interner)
}
ParameterKind::Lifetime(_) => ParameterKind::Lifetime(
LifetimeData::BoundVar(bound_var).intern(interner),
)
.intern(interner),
}
})
.collect::<Vec<_>>(),
)
}
}

#[derive(Clone, PartialEq, Eq, Hash, HasInterner)]
Expand Down
3 changes: 2 additions & 1 deletion chalk-ir/src/visit/boring_impls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
//! The more interesting impls of `Visit` remain in the `visit` module.

use crate::{
AssocTypeId, DebruijnIndex, Goals, ImplId, Interner, Parameter, ParameterKind,
AssocTypeId, ClausePriority, DebruijnIndex, Goals, ImplId, Interner, Parameter, ParameterKind,
PlaceholderIndex, ProgramClause, ProgramClauseData, ProgramClauses, QuantifiedWhereClauses,
QuantifierKind, StructId, Substitution, SuperVisit, TraitId, UniverseIndex, Visit, VisitResult,
Visitor,
Expand Down Expand Up @@ -205,6 +205,7 @@ const_visit!(QuantifierKind);
const_visit!(DebruijnIndex);
const_visit!(chalk_engine::TableIndex);
const_visit!(chalk_engine::TimeStamp);
const_visit!(ClausePriority);
const_visit!(());

#[macro_export]
Expand Down
4 changes: 3 additions & 1 deletion chalk-ir/src/zip.rs
Original file line number Diff line number Diff line change
Expand Up @@ -200,6 +200,7 @@ eq_zip!(I => TypeName<I>);
eq_zip!(I => QuantifierKind);
eq_zip!(I => PhantomData<I>);
eq_zip!(I => PlaceholderIndex);
eq_zip!(I => ClausePriority);

/// Generates a Zip impl that zips each field of the struct in turn.
macro_rules! struct_zip {
Expand Down Expand Up @@ -242,7 +243,8 @@ struct_zip!(impl[I: Interner] Zip<I> for AliasEq<I> { alias, ty });
struct_zip!(impl[I: Interner] Zip<I> for EqGoal<I> { a, b });
struct_zip!(impl[I: Interner] Zip<I> for ProgramClauseImplication<I> {
consequence,
conditions
conditions,
priority,
});

impl<I: Interner> Zip<I> for Environment<I> {
Expand Down
93 changes: 65 additions & 28 deletions chalk-solve/src/clauses.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ use self::env_elaborator::elaborate_env_clauses;
use self::program_clauses::ToProgramClauses;
use crate::split::Split;
use crate::RustIrDatabase;
use chalk_engine::context::Floundered;
use chalk_ir::cast::Cast;
use chalk_ir::could_match::CouldMatch;
use chalk_ir::interner::Interner;
Expand All @@ -12,6 +13,7 @@ use rustc_hash::FxHashSet;
pub mod builder;
mod builtin_traits;
mod env_elaborator;
mod generalize;
pub mod program_clauses;

/// For auto-traits, we generate a default rule for every struct,
Expand Down Expand Up @@ -111,7 +113,7 @@ pub(crate) fn program_clauses_for_goal<'db, I: Interner>(
db: &'db dyn RustIrDatabase<I>,
environment: &Environment<I>,
goal: &DomainGoal<I>,
) -> Vec<ProgramClause<I>> {
) -> Result<Vec<ProgramClause<I>>, Floundered> {
debug_heading!(
"program_clauses_for_goal(goal={:?}, environment={:?})",
goal,
Expand All @@ -121,13 +123,13 @@ pub(crate) fn program_clauses_for_goal<'db, I: Interner>(

let mut vec = vec![];
vec.extend(db.custom_clauses());
program_clauses_that_could_match(db, environment, goal, &mut vec);
program_clauses_that_could_match(db, environment, goal, &mut vec)?;
program_clauses_for_env(db, environment, &mut vec);
vec.retain(|c| c.could_match(interner, goal));

debug!("vec = {:#?}", vec);

vec
Ok(vec)
}

/// Returns a set of program clauses that could possibly match
Expand All @@ -139,17 +141,26 @@ fn program_clauses_that_could_match<I: Interner>(
environment: &Environment<I>,
goal: &DomainGoal<I>,
clauses: &mut Vec<ProgramClause<I>>,
) {
) -> Result<(), Floundered> {
let interner = db.interner();
let builder = &mut ClauseBuilder::new(db, clauses);

match goal {
DomainGoal::Holds(WhereClause::Implemented(trait_ref)) => {
let trait_id = trait_ref.trait_id;

let trait_datum = db.trait_datum(trait_id);

if trait_datum.is_non_enumerable_trait() || trait_datum.is_auto_trait() {
let self_ty = trait_ref.self_type_parameter(interner);
if self_ty.bound(interner).is_some() || self_ty.inference_var(interner).is_some() {
nikomatsakis marked this conversation as resolved.
Show resolved Hide resolved
return Err(Floundered);
}
}

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

for impl_id in db.impls_for_trait(
trait_ref.trait_id,
Expand All @@ -168,8 +179,8 @@ fn program_clauses_that_could_match<I: Interner>(
push_auto_trait_impls(builder, trait_id, struct_id);
}
}
TyData::InferenceVar(_) => {
panic!("auto-traits should flounder if nothing is known")
TyData::InferenceVar(_) | TyData::BoundVar(_) => {
nikomatsakis marked this conversation as resolved.
Show resolved Hide resolved
return Err(Floundered);
}
_ => {}
}
Expand Down Expand Up @@ -222,19 +233,29 @@ fn program_clauses_that_could_match<I: Interner>(
// and `bounded_ty` is the `exists<T> { .. }`
// clauses shown above.

for exists_qwc in dyn_ty.bounds.map_ref(|r| r.iter(interner)) {
// Replace the `T` from `exists<T> { .. }` with `self_ty`,
// yielding clases like
//
// ```
// forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) }
// ```
let qwc = exists_qwc.substitute(interner, &[self_ty.clone().cast(interner)]);

builder.push_binders(&qwc, |builder, wc| {
builder.push_fact(wc);
});
}
// Turn free BoundVars in the type into new existentials. E.g.
// we might get some `dyn Foo<?X>`, and we don't want to return
// a clause with a free variable. We can instead return a
// slightly more general clause by basically turning this into
// `exists<A> dyn Foo<A>`.
let generalized_dyn_ty = generalize::Generalize::apply(db.interner(), dyn_ty);
nikomatsakis marked this conversation as resolved.
Show resolved Hide resolved

builder.push_binders(&generalized_dyn_ty, |builder, dyn_ty| {
for exists_qwc in dyn_ty.bounds.map_ref(|r| r.iter(interner)) {
// Replace the `T` from `exists<T> { .. }` with `self_ty`,
// yielding clases like
//
// ```
// forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) }
// ```
let qwc =
exists_qwc.substitute(interner, &[self_ty.clone().cast(interner)]);

builder.push_binders(&qwc, |builder, wc| {
builder.push_fact(wc);
});
}
});
}

if let Some(well_known) = trait_datum.well_known {
Expand All @@ -257,9 +278,9 @@ fn program_clauses_that_could_match<I: Interner>(
}
DomainGoal::WellFormed(WellFormed::Ty(ty))
| DomainGoal::IsUpstream(ty)
| DomainGoal::DownstreamType(ty) => match_ty(builder, environment, ty),
| DomainGoal::DownstreamType(ty) => match_ty(builder, environment, ty)?,
DomainGoal::IsFullyVisible(ty) | DomainGoal::IsLocal(ty) => {
match_ty(builder, environment, ty)
match_ty(builder, environment, ty)?
}
DomainGoal::FromEnv(_) => (), // Computed in the environment
DomainGoal::Normalize(Normalize { alias, ty: _ }) => {
Expand All @@ -277,6 +298,18 @@ fn program_clauses_that_could_match<I: Interner>(
let associated_ty_datum = db.associated_ty_data(alias.associated_ty_id);
let trait_id = associated_ty_datum.trait_id;
let trait_parameters = db.trait_parameters_from_projection(alias);

let trait_datum = db.trait_datum(trait_id);

// Flounder if the self-type is unknown and the trait is non-enumerable.
//
// e.g., Normalize(<?X as Iterator>::Item = u32)
if (alias.self_type_parameter(interner).is_var(interner))
&& trait_datum.is_non_enumerable_trait()
{
return Err(Floundered);
}

push_program_clauses_for_associated_type_values_in_impls_of(
builder,
trait_id,
Expand All @@ -288,6 +321,8 @@ fn program_clauses_that_could_match<I: Interner>(
.to_program_clauses(builder),
DomainGoal::Compatible(()) => (),
};

Ok(())
}

/// Generate program clauses from the associated-type values
Expand Down Expand Up @@ -348,9 +383,9 @@ fn match_ty<I: Interner>(
builder: &mut ClauseBuilder<'_, I>,
environment: &Environment<I>,
ty: &Ty<I>,
) {
) -> Result<(), Floundered> {
let interner = builder.interner();
match ty.data(interner) {
Ok(match ty.data(interner) {
TyData::Apply(application_ty) => match_type_name(builder, application_ty.name),
TyData::Placeholder(_) => {
builder.push_clause(WellFormed::Ty(ty.clone()), Some(FromEnv::Ty(ty.clone())));
Expand All @@ -365,12 +400,12 @@ fn match_ty<I: Interner>(
.substitution
.iter(interner)
.map(|p| p.assert_ty_ref(interner))
.for_each(|ty| match_ty(builder, environment, &ty))
.map(|ty| match_ty(builder, environment, &ty))
.collect::<Result<_, Floundered>>()?;
}
TyData::BoundVar(_) => {}
TyData::InferenceVar(_) => panic!("should have floundered"),
TyData::BoundVar(_) | TyData::InferenceVar(_) => return Err(Floundered),
TyData::Dyn(_) => {}
}
})
}

fn match_type_name<I: Interner>(builder: &mut ClauseBuilder<'_, I>, name: TypeName<I>) {
Expand All @@ -396,6 +431,8 @@ fn program_clauses_for_env<'db, I: Interner>(
environment: &Environment<I>,
clauses: &mut Vec<ProgramClause<I>>,
) {
clauses.extend(environment.clauses.iter(db.interner()).cloned());

let mut last_round = FxHashSet::default();
elaborate_env_clauses(
db,
Expand Down
Loading