Skip to content

Commit

Permalink
Merge pull request #372 from flodiebold/recursive-solver
Browse files Browse the repository at this point in the history
Recursive solver
  • Loading branch information
nikomatsakis authored Apr 15, 2020
2 parents 2bd2e03 + 2aa90be commit 28cef6f
Show file tree
Hide file tree
Showing 26 changed files with 2,041 additions and 109 deletions.
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() {
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(_) => {
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);

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

0 comments on commit 28cef6f

Please sign in to comment.