Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
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
43 changes: 37 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. `skip_binder` is only valid
/// when you are either extracting data that has nothing to
/// do with bound vars, 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
}

/// Converts `&Binders<T>` to `Binders<&T>`. Produces new `Binders`
/// with cloned quantifiers containing a reference to the original
/// value, leaving the original in place.
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 Down Expand Up @@ -1199,6 +1224,12 @@ impl<T> Binders<T> {
}
}

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
42 changes: 17 additions & 25 deletions chalk-solve/src/coherence/solve.rs
Original file line number Diff line number Diff line change
Expand Up @@ -85,9 +85,20 @@ 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 = lhs_bound
.trait_ref
.substitution
.parameters(interner)
.iter()
.cloned();
let rhs_params = rhs_bound
.trait_ref
.substitution
.parameters(interner)
.iter()
.map(|param| param.shifted_in(interner));

Expand All @@ -98,10 +109,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 +123,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 @@ -267,12 +268,3 @@ impl<I: Interner> CoherenceSolver<'_, I> {
result
}
}

fn params<'a, I: Interner>(interner: &I, impl_datum: &'a ImplDatum<I>) -> &'a [Parameter<I>] {
impl_datum
.binders
.value
.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