Skip to content

Commit df646ae

Browse files
authored
Merge pull request #415 from flodiebold/dyn-super-traits
Make `dyn Trait` implement its super traits as well
2 parents cf0b0db + 2a90671 commit df646ae

File tree

8 files changed

+430
-109
lines changed

8 files changed

+430
-109
lines changed

chalk-integration/src/lowering.rs

+1-2
Original file line numberDiff line numberDiff line change
@@ -2,13 +2,12 @@ use chalk_ir::cast::{Cast, Caster};
22
use chalk_ir::interner::{ChalkIr, HasInterner};
33
use chalk_ir::{
44
self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, ParameterKinds,
5-
QuantifiedWhereClauses, StructId, Substitution, TraitId,
5+
QuantifiedWhereClauses, StructId, Substitution, ToParameter, TraitId,
66
};
77
use chalk_parse::ast::*;
88
use chalk_rust_ir as rust_ir;
99
use chalk_rust_ir::{
1010
Anonymize, AssociatedTyValueId, IntoWhereClauses, OpaqueTyDatum, OpaqueTyDatumBound,
11-
ToParameter,
1211
};
1312
use lalrpop_intern::intern;
1413
use std::collections::BTreeMap;

chalk-ir/src/lib.rs

+99
Original file line numberDiff line numberDiff line change
@@ -1250,6 +1250,14 @@ impl<T: HasInterner> Binders<T> {
12501250
Self { binders, value }
12511251
}
12521252

1253+
/// Wraps the given value in a binder without variables, i.e. `for<>
1254+
/// (value)`. Since our deBruijn indices count binders, not variables, this
1255+
/// is sometimes useful.
1256+
pub fn empty(interner: &T::Interner, value: T) -> Self {
1257+
let binders = ParameterKinds::new(interner);
1258+
Self { binders, value }
1259+
}
1260+
12531261
/// Skips the binder and returns the "bound" value. This is a
12541262
/// risky thing to do because it's easy to get confused about
12551263
/// De Bruijn indices and the like. `skip_binder` is only valid
@@ -1287,6 +1295,20 @@ impl<T: HasInterner> Binders<T> {
12871295
}
12881296
}
12891297

1298+
/// Transforms the inner value according to the given function; returns
1299+
/// `None` if the function returns `None`.
1300+
pub fn filter_map<U, OP>(self, op: OP) -> Option<Binders<U>>
1301+
where
1302+
OP: FnOnce(T) -> Option<U>,
1303+
U: HasInterner<Interner = T::Interner>,
1304+
{
1305+
let value = op(self.value)?;
1306+
Some(Binders {
1307+
binders: self.binders,
1308+
value,
1309+
})
1310+
}
1311+
12901312
pub fn map_ref<'a, U, OP>(&'a self, op: OP) -> Binders<U>
12911313
where
12921314
OP: FnOnce(&'a T) -> U,
@@ -1295,6 +1317,19 @@ impl<T: HasInterner> Binders<T> {
12951317
self.as_ref().map(op)
12961318
}
12971319

1320+
/// Creates a `Substitution` containing bound vars such that applying this
1321+
/// substitution will not change the value, i.e. `^0.0, ^0.1, ^0.2` and so
1322+
/// on.
1323+
pub fn identity_substitution(&self, interner: &T::Interner) -> Substitution<T::Interner> {
1324+
Substitution::from(
1325+
interner,
1326+
self.binders
1327+
.iter(interner)
1328+
.enumerate()
1329+
.map(|(i, pk)| (pk, i).to_parameter(interner)),
1330+
)
1331+
}
1332+
12981333
/// Creates a fresh binders that contains a single type
12991334
/// variable. The result of the closure will be embedded in this
13001335
/// binder. Note that you should be careful with what you return
@@ -1317,6 +1352,36 @@ impl<T: HasInterner> Binders<T> {
13171352
}
13181353
}
13191354

1355+
impl<T, I> Binders<Binders<T>>
1356+
where
1357+
T: Fold<I, I> + HasInterner<Interner = I>,
1358+
T::Result: HasInterner<Interner = I>,
1359+
I: Interner,
1360+
{
1361+
/// This turns two levels of binders (`for<A> for<B>`) into one level (`for<A, B>`).
1362+
pub fn fuse_binders(self, interner: &T::Interner) -> Binders<T::Result> {
1363+
let num_binders = self.len(interner);
1364+
// generate a substitution to shift the indexes of the inner binder:
1365+
let subst = Substitution::from(
1366+
interner,
1367+
self.value
1368+
.binders
1369+
.iter(interner)
1370+
.enumerate()
1371+
.map(|(i, pk)| (pk, i + num_binders).to_parameter(interner)),
1372+
);
1373+
let value = self.value.substitute(interner, &subst);
1374+
let binders = ParameterKinds::from(
1375+
interner,
1376+
self.binders
1377+
.iter(interner)
1378+
.chain(self.value.binders.iter(interner))
1379+
.cloned(),
1380+
);
1381+
Binders { binders, value }
1382+
}
1383+
}
1384+
13201385
impl<T: HasInterner> From<Binders<T>> for (ParameterKinds<T::Interner>, T) {
13211386
fn from(binders: Binders<T>) -> Self {
13221387
(binders.binders, binders.value)
@@ -2073,6 +2138,40 @@ where
20732138
}
20742139
}
20752140

2141+
pub trait ToParameter {
2142+
/// Utility for converting a list of all the binders into scope
2143+
/// into references to those binders. Simply pair the binders with
2144+
/// the indices, and invoke `to_parameter()` on the `(binder,
2145+
/// index)` pair. The result will be a reference to a bound
2146+
/// variable of appropriate kind at the corresponding index.
2147+
fn to_parameter<I: Interner>(&self, interner: &I) -> Parameter<I> {
2148+
self.to_parameter_at_depth(interner, DebruijnIndex::INNERMOST)
2149+
}
2150+
2151+
fn to_parameter_at_depth<I: Interner>(
2152+
&self,
2153+
interner: &I,
2154+
debruijn: DebruijnIndex,
2155+
) -> Parameter<I>;
2156+
}
2157+
2158+
impl<'a> ToParameter for (&'a ParameterKind<()>, usize) {
2159+
fn to_parameter_at_depth<I: Interner>(
2160+
&self,
2161+
interner: &I,
2162+
debruijn: DebruijnIndex,
2163+
) -> Parameter<I> {
2164+
let &(binder, index) = self;
2165+
let bound_var = BoundVar::new(debruijn, index);
2166+
match *binder {
2167+
ParameterKind::Lifetime(_) => LifetimeData::BoundVar(bound_var)
2168+
.intern(interner)
2169+
.cast(interner),
2170+
ParameterKind::Ty(_) => TyData::BoundVar(bound_var).intern(interner).cast(interner),
2171+
}
2172+
}
2173+
}
2174+
20762175
impl<'i, I: Interner> Folder<'i, I> for &SubstFolder<'i, I> {
20772176
fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
20782177
self

chalk-rust-ir/src/lib.rs

+13-37
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,9 @@ use chalk_ir::cast::Cast;
99
use chalk_ir::fold::shift::Shift;
1010
use chalk_ir::interner::{Interner, TargetInterner};
1111
use chalk_ir::{
12-
AliasEq, AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, LifetimeData,
13-
OpaqueTyId, Parameter, ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId,
14-
Substitution, TraitId, TraitRef, Ty, TyData, TypeName, WhereClause,
12+
AliasEq, AliasTy, AssocTypeId, Binders, DebruijnIndex, ImplId, OpaqueTyId, Parameter,
13+
ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId, Substitution, ToParameter,
14+
TraitId, TraitRef, Ty, TyData, TypeName, WhereClause,
1515
};
1616
use std::iter;
1717

@@ -167,6 +167,16 @@ impl<I: Interner> TraitDatum<I> {
167167
pub fn is_coinductive_trait(&self) -> bool {
168168
self.flags.coinductive
169169
}
170+
171+
/// Gives access to the where clauses of the trait, quantified over the type parameters of the trait:
172+
///
173+
/// ```ignore
174+
/// trait Foo<T> where T: Debug { }
175+
/// ^^^^^^^^^^^^^^
176+
/// ```
177+
pub fn where_clauses(&self) -> Binders<&Vec<QuantifiedWhereClause<I>>> {
178+
self.binders.as_ref().map(|td| &td.where_clauses)
179+
}
170180
}
171181

172182
#[derive(Clone, Debug, PartialEq, Eq, Hash, HasInterner)]
@@ -331,40 +341,6 @@ impl<T> Anonymize for [ParameterKind<T>] {
331341
}
332342
}
333343

334-
pub trait ToParameter {
335-
/// Utility for converting a list of all the binders into scope
336-
/// into references to those binders. Simply pair the binders with
337-
/// the indices, and invoke `to_parameter()` on the `(binder,
338-
/// index)` pair. The result will be a reference to a bound
339-
/// variable of appropriate kind at the corresponding index.
340-
fn to_parameter<I: Interner>(&self, interner: &I) -> Parameter<I> {
341-
self.to_parameter_at_depth(interner, DebruijnIndex::INNERMOST)
342-
}
343-
344-
fn to_parameter_at_depth<I: Interner>(
345-
&self,
346-
interner: &I,
347-
debruijn: DebruijnIndex,
348-
) -> Parameter<I>;
349-
}
350-
351-
impl<'a> ToParameter for (&'a ParameterKind<()>, usize) {
352-
fn to_parameter_at_depth<I: Interner>(
353-
&self,
354-
interner: &I,
355-
debruijn: DebruijnIndex,
356-
) -> Parameter<I> {
357-
let &(binder, index) = self;
358-
let bound_var = BoundVar::new(debruijn, index);
359-
match *binder {
360-
ParameterKind::Lifetime(_) => LifetimeData::BoundVar(bound_var)
361-
.intern(interner)
362-
.cast(interner),
363-
ParameterKind::Ty(_) => TyData::BoundVar(bound_var).intern(interner).cast(interner),
364-
}
365-
}
366-
}
367-
368344
/// Represents an associated type declaration found inside of a trait:
369345
///
370346
/// ```notrust

chalk-solve/src/clauses.rs

+13-68
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ use rustc_hash::FxHashSet;
1212

1313
pub mod builder;
1414
mod builtin_traits;
15+
mod dyn_ty;
1516
mod env_elaborator;
1617
mod generalize;
1718
pub mod program_clauses;
@@ -198,76 +199,20 @@ fn program_clauses_that_could_match<I: Interner>(
198199
}
199200
}
200201

201-
// If the self type `S` is a `dyn trait` type, we wish to generate program-clauses
202-
// that indicates that it implements its own traits. For example, a `dyn Write` type
203-
// implements `Write` and so on.
202+
// If the self type is a `dyn trait` type, generate program-clauses
203+
// that indicates that it implements its own traits.
204+
// FIXME: This is presently rather wasteful, in that we don't check that the
205+
// these program clauses we are generating are actually relevant to the goal
206+
// `goal` that we are actually *trying* to prove (though there is some later
207+
// code that will screen out irrelevant stuff).
204208
//
205-
// To see how this works, consider as an example the type `dyn Fn(&u8)`. This is
206-
// really shorthand for `dyn for<'a> Fn<(&'a u8), Output = ()>`, and we represent
207-
// that type as something like this:
208-
//
209-
// ```
210-
// dyn(exists<T> {
211-
// forall<'a> { Implemented(T: Fn<'a>) },
212-
// forall<'a> { AliasEq(<T as Fn<'a>>::Output, ()) },
213-
// })
214-
// ```
215-
//
216-
// so what we will do is to generate one program clause
217-
// for each of the conditions. Thus we get two program
218-
// clauses:
219-
//
220-
// ```
221-
// forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) }
222-
// ```
223-
//
224-
// and
225-
//
226-
// ```
227-
// forall<'a> { AliasEq(<dyn Fn(&u8) as Fn<'a>>::Output, ()) },
228-
// ```
229-
//
230-
// FIXME. This is presently rather wasteful, in that we
231-
// don't check that the these program clauses we are
232-
// generating are actually relevant to the goal `goal`
233-
// that we are actually *trying* to prove (though there is
234-
// some later code that will screen out irrelevant
235-
// stuff).
236-
//
237-
// In other words, in our example, if we were trying to
238-
// prove `Implemented(dyn Fn(&u8): Clone)`, we would have
239-
// generated two clauses that are totally irrelevant to
240-
// that goal, because they let us prove other things but
241-
// not `Clone`.
209+
// In other words, if we were trying to prove `Implemented(dyn
210+
// Fn(&u8): Clone)`, we would still generate two clauses that are
211+
// totally irrelevant to that goal, because they let us prove other
212+
// things but not `Clone`.
242213
let self_ty = trait_ref.self_type_parameter(interner);
243-
if let TyData::Dyn(dyn_ty) = self_ty.data(interner) {
244-
// In this arm, `self_ty` is the `dyn Fn(&u8)`,
245-
// and `bounded_ty` is the `exists<T> { .. }`
246-
// clauses shown above.
247-
248-
// Turn free BoundVars in the type into new existentials. E.g.
249-
// we might get some `dyn Foo<?X>`, and we don't want to return
250-
// a clause with a free variable. We can instead return a
251-
// slightly more general clause by basically turning this into
252-
// `exists<A> dyn Foo<A>`.
253-
let generalized_dyn_ty = generalize::Generalize::apply(db.interner(), dyn_ty);
254-
255-
builder.push_binders(&generalized_dyn_ty, |builder, dyn_ty| {
256-
for exists_qwc in dyn_ty.bounds.map_ref(|r| r.iter(interner)) {
257-
// Replace the `T` from `exists<T> { .. }` with `self_ty`,
258-
// yielding clases like
259-
//
260-
// ```
261-
// forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) }
262-
// ```
263-
let qwc =
264-
exists_qwc.substitute(interner, &[self_ty.clone().cast(interner)]);
265-
266-
builder.push_binders(&qwc, |builder, wc| {
267-
builder.push_fact(wc);
268-
});
269-
}
270-
});
214+
if let TyData::Dyn(_) = self_ty.data(interner) {
215+
dyn_ty::build_dyn_self_ty_clauses(db, builder, self_ty.clone())
271216
}
272217

273218
match self_ty.data(interner) {

chalk-solve/src/clauses/builder.rs

-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,6 @@ use crate::RustIrDatabase;
33
use chalk_ir::fold::Fold;
44
use chalk_ir::interner::{HasInterner, Interner};
55
use chalk_ir::*;
6-
use chalk_rust_ir::*;
76
use std::marker::PhantomData;
87

98
/// The "clause builder" is a useful tool for building up sets of

0 commit comments

Comments
 (0)