Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
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
18 changes: 6 additions & 12 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -169,10 +169,7 @@ impl<'k> Env<'k> {
{
let binders: Vec<_> = binders.into_iter().collect();
let env = self.introduce(binders.iter().cloned())?;
Ok(chalk_ir::Binders {
binders: binders.anonymize(),
value: op(&env)?,
})
Ok(chalk_ir::Binders::new(binders.anonymize(), op(&env)?))
}
}

Expand Down Expand Up @@ -528,10 +525,7 @@ impl LowerTypeKind for StructDefn {
Ok(TypeKind {
sort: TypeSort::Struct,
name: self.name.str,
binders: chalk_ir::Binders {
binders: self.all_parameters().anonymize(),
value: (),
},
binders: chalk_ir::Binders::new(self.all_parameters().anonymize(), ()),
})
}
}
Expand All @@ -548,11 +542,11 @@ impl LowerTypeKind for TraitDefn {
Ok(TypeKind {
sort: TypeSort::Trait,
name: self.name.str,
binders: chalk_ir::Binders {
binders: chalk_ir::Binders::new(
// for the purposes of the *type*, ignore `Self`:
binders: binders.anonymize(),
value: (),
},
binders.anonymize(),
(),
),
})
}
}
Expand Down
4 changes: 2 additions & 2 deletions chalk-integration/src/program.rs
Original file line number Diff line number Diff line change
Expand Up @@ -275,7 +275,7 @@ impl RustIrDatabase<ChalkIr> for Program {
self.impl_data
.iter()
.filter(|(_, impl_datum)| {
let trait_ref = &impl_datum.binders.value.trait_ref;
let trait_ref = &impl_datum.binders.skip_binders().trait_ref;
trait_id == trait_ref.trait_id && {
assert_eq!(trait_ref.substitution.len(interner), parameters.len());
<[_] as CouldMatch<[_]>>::could_match(
Expand Down Expand Up @@ -308,7 +308,7 @@ impl RustIrDatabase<ChalkIr> for Program {
// Look for an impl like `impl Send for Foo` where `Foo` is
// the struct. See `push_auto_trait_impls` for more.
self.impl_data.values().any(|impl_datum| {
let impl_trait_ref = &impl_datum.binders.value.trait_ref;
let impl_trait_ref = &impl_datum.binders.skip_binders().trait_ref;
impl_trait_ref.trait_id == auto_trait_id
&& match impl_trait_ref.self_type_parameter(interner).data(interner) {
TyData::Apply(apply) => match apply.name {
Expand Down
64 changes: 58 additions & 6 deletions chalk-ir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1144,14 +1144,43 @@ impl<I: Interner> HasInterner for AliasEq<I> {
#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
pub struct Binders<T> {
pub binders: Vec<ParameterKind<()>>,
pub value: T,
value: T,
}

impl<T: HasInterner> HasInterner for Binders<T> {
type Interner = T::Interner;
}

impl<T> Binders<T> {
pub fn new(binders: Vec<ParameterKind<()>>, value: T) -> Self {
Self { binders, value }
}

/// Skips the binder and returns the "bound" value. This is a
/// risky thing to do because it's easy to get confused about
/// De Bruijn indices and the like. It is usually better to
/// discharge the binder using `no_bound_vars` or something
/// like that. `skip_binder` is only valid when you are either
/// extracting data that has nothing to do with bound vars, you
/// are doing some sort of test that does not involve bound
/// regions, or you are being very careful about your depth
/// accounting.
///
/// Some examples where `skip_binder` is reasonable:
///
/// - extracting the `TraitId` from a TraitRef;
/// - checking if there are any fields in a StructDatum
pub fn skip_binders(&self) -> &T {
&self.value
}

pub fn as_ref(&self) -> Binders<&T> {
Binders {
binders: self.binders.clone(),
value: &self.value,
}
}

pub fn map<U, OP>(self, op: OP) -> Binders<U>
where
OP: FnOnce(T) -> U,
Expand All @@ -1167,11 +1196,7 @@ impl<T> Binders<T> {
where
OP: FnOnce(&'a T) -> U,
{
let value = op(&self.value);
Binders {
binders: self.binders.clone(),
value,
}
self.as_ref().map(op)
}

/// Creates a fresh binders that contains a single type
Expand All @@ -1194,11 +1219,38 @@ impl<T> Binders<T> {
}
}

/// Unwraps and returns the value within, but only if it contains
/// no vars bound by this binder. (In other words, if this binder --
/// and indeed any enclosing binder -- doesn't bind anything at
/// all.) Otherwise, returns `None`.
///
/// (One could imagine having a method that just unwraps a single
/// binder, but permits late-bound vars bound by enclosing
/// binders, but that would require adjusting the debruijn
/// indices, and given the shallow binding structure we often use,
/// would not be that useful.)
pub fn no_bound_vars<I: Interner>(&self, interner: &I) -> Option<&T>
where
T: Visit<I>,
{
if self.skip_binders().has_free_vars(interner) {
None
} else {
Some(self.skip_binders())
}
}

pub fn len(&self) -> usize {
self.binders.len()
}
}

impl<T> From<Binders<T>> for (Vec<ParameterKind<()>>, T) {
fn from(binders: Binders<T>) -> Self {
(binders.binders, binders.value)
}
}

impl<T, I> Binders<T>
where
T: Fold<I, I> + HasInterner<Interner = I>,
Expand Down
14 changes: 4 additions & 10 deletions chalk-rust-ir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ impl<I: Interner> ImplDatum<I> {
}

pub fn trait_id(&self) -> TraitId<I> {
self.binders.value.trait_ref.trait_id
self.binders.skip_binders().trait_ref.trait_id
}
}

Expand Down Expand Up @@ -234,13 +234,8 @@ impl<I: Interner> IntoWhereClauses<I> for QuantifiedInlineBound<I> {

fn into_where_clauses(&self, interner: &I, self_ty: Ty<I>) -> Vec<QuantifiedWhereClause<I>> {
let self_ty = self_ty.shifted_in(interner);
self.value
.into_where_clauses(interner, self_ty)
self.map_ref(|b| b.into_where_clauses(interner, self_ty))
.into_iter()
.map(|wc| Binders {
binders: self.binders.clone(),
value: wc,
})
.collect()
}
}
Expand Down Expand Up @@ -413,8 +408,7 @@ impl<I: Interner> AssociatedTyDatum<I> {
/// these quantified where clauses are in the scope of the
/// `binders` field.
pub fn bounds_on_self(&self, interner: &I) -> Vec<QuantifiedWhereClause<I>> {
let Binders { binders, value } = &self.binders;

let (binders, assoc_ty_datum) = self.binders.as_ref().into();
Copy link
Member

Choose a reason for hiding this comment

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

This does technically add a clone to binders. But I don't think it matters.

// Create a list `P0...Pn` of references to the binders in
// scope for this associated type:
let substitution = Substitution::from(
Expand All @@ -435,7 +429,7 @@ impl<I: Interner> AssociatedTyDatum<I> {
// ```
// <P0 as Foo<P1..Pn>>::Item<Pn..Pm>: Debug
// ```
value
assoc_ty_datum
.bounds
.iter()
.flat_map(|b| b.into_where_clauses(interner, self_ty.clone()))
Expand Down
12 changes: 3 additions & 9 deletions chalk-solve/src/clauses/builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,11 +55,8 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
.push(ProgramClauseData::Implies(clause).intern(interner));
} else {
self.clauses.push(
ProgramClauseData::ForAll(Binders {
binders: self.binders.clone(),
value: clause,
})
.intern(interner),
ProgramClauseData::ForAll(Binders::new(self.binders.clone(), clause))
.intern(interner),
);
}

Expand Down Expand Up @@ -121,10 +118,7 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
#[allow(dead_code)]
pub fn push_bound_ty(&mut self, op: impl FnOnce(&mut Self, Ty<I>)) {
let interner = self.interner();
let binders = Binders {
binders: vec![ParameterKind::Ty(())],
value: PhantomData::<I>,
};
let binders = Binders::new(vec![ParameterKind::Ty(())], PhantomData::<I>);
self.push_binders(&binders, |this, PhantomData| {
let ty = this
.placeholders_in_scope()
Expand Down
2 changes: 1 addition & 1 deletion chalk-solve/src/clauses/builtin_traits/sized.rs
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ pub fn add_sized_program_clauses<I: Interner>(
let struct_datum = db.struct_datum(struct_id);

// Structs with no fields are always Sized
if struct_datum.binders.map_ref(|b| b.fields.is_empty()).value {
if struct_datum.binders.skip_binders().fields.is_empty() {
builder.push_fact(trait_ref.clone());
return;
}
Expand Down
38 changes: 15 additions & 23 deletions chalk-solve/src/coherence/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -85,9 +85,12 @@ impl<I: Interner> CoherenceSolver<'_, I> {

let interner = self.db.interner();

let (lhs_binders, lhs_bound) = lhs.binders.as_ref().into();
let (rhs_binders, rhs_bound) = rhs.binders.as_ref().into();
Copy link
Contributor

Choose a reason for hiding this comment

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

This is slightly misleading, because as_ref is cloning the binders, whereas it wasn't before.

Copy link
Contributor Author

@basil-cow basil-cow Apr 10, 2020

Choose a reason for hiding this comment

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

binders are cloned later anyway, but I agree, as_ref is kind of a bad name (I just copied it from rustc), should I change it?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Oh, you mean the names, hmm, ok

Copy link
Member

Choose a reason for hiding this comment

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

I think as_ref is fine. Just be sure the doc comments are clear. (The binders will almost certainly end up being an interned type instead of a vec anyways, so the clone should be cheap).


// Upshift the rhs variables in params to account for the joined binders
let lhs_params = params(interner, lhs).iter().cloned();
let rhs_params = params(interner, rhs)
let lhs_params = params(interner, lhs_bound).iter().cloned();
let rhs_params = params(interner, rhs_bound)
.iter()
.map(|param| param.shifted_in(interner));

Expand All @@ -98,10 +101,8 @@ impl<I: Interner> CoherenceSolver<'_, I> {
.map(|(a, b)| GoalData::EqGoal(EqGoal { a, b }).intern(interner));

// Upshift the rhs variables in where clauses
let lhs_where_clauses = lhs.binders.value.where_clauses.iter().cloned();
let rhs_where_clauses = rhs
.binders
.value
let lhs_where_clauses = lhs_bound.where_clauses.iter().cloned();
let rhs_where_clauses = rhs_bound
.where_clauses
.iter()
.map(|wc| wc.shifted_in(interner));
Expand All @@ -114,16 +115,8 @@ impl<I: Interner> CoherenceSolver<'_, I> {
// Join all the goals we've created together with And, then quantify them
// over the joined binders. This is our query.
let goal = Box::new(Goal::all(interner, params_goals.chain(wc_goals)))
.quantify(
interner,
QuantifierKind::Exists,
lhs.binders.binders.clone(),
)
.quantify(
interner,
QuantifierKind::Exists,
rhs.binders.binders.clone(),
)
.quantify(interner, QuantifierKind::Exists, lhs_binders)
.quantify(interner, QuantifierKind::Exists, rhs_binders)
.compatible(interner)
.negate(interner);

Expand Down Expand Up @@ -268,11 +261,10 @@ impl<I: Interner> CoherenceSolver<'_, I> {
}
}

fn params<'a, I: Interner>(interner: &I, impl_datum: &'a ImplDatum<I>) -> &'a [Parameter<I>] {
impl_datum
.binders
.value
.trait_ref
.substitution
.parameters(interner)
fn params<'a, I: Interner>(
interner: &I,
impl_datum_bound: &'a ImplDatumBound<I>,
) -> &'a [Parameter<I>] {
// We can skip binders here because the caller is handling correct binders handling
impl_datum_bound.trait_ref.substitution.parameters(interner)
}
4 changes: 3 additions & 1 deletion chalk-solve/src/coinductive_goal.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,9 @@ impl<I: Interner> IsCoinductive<I> for Goal<I> {
WhereClause::AliasEq(..) => false,
},
GoalData::DomainGoal(DomainGoal::WellFormed(WellFormed::Trait(..))) => true,
GoalData::Quantified(QuantifierKind::ForAll, goal) => goal.value.is_coinductive(db),
GoalData::Quantified(QuantifierKind::ForAll, goal) => {
goal.skip_binders().is_coinductive(db)
}
_ => false,
}
}
Expand Down
2 changes: 1 addition & 1 deletion chalk-solve/src/infer/instantiate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ impl<'a, T> IntoBindersAndValue for &'a Binders<T> {
type Value = &'a T;

fn into_binders_and_value(self) -> (Self::Binders, Self::Value) {
(self.binders.iter().cloned(), &self.value)
(self.binders.iter().cloned(), self.skip_binders())
}
}

Expand Down
2 changes: 1 addition & 1 deletion chalk-solve/src/solve/slg/resolvent.rs
Original file line number Diff line number Diff line change
Expand Up @@ -485,7 +485,7 @@ impl<'i, I: Interner> Zipper<'i, I> for AnswerSubstitutor<'i, I> {
T: Zip<I> + Fold<I, Result = T>,
{
self.outer_binder.shift_in();
Zip::zip_with(self, &answer.value, &pending.value)?;
Zip::zip_with(self, &answer.skip_binders(), &pending.skip_binders())?;
self.outer_binder.shift_out();
Ok(())
}
Expand Down