Skip to content

Commit

Permalink
Make dyn Trait implement its super traits as well
Browse files Browse the repository at this point in the history
This implements the impl rules from rust-lang#203, as far as I understood them. It
doesn't do the well-formedness or object safety rules.
  • Loading branch information
flodiebold committed May 4, 2020
1 parent cf0b0db commit 2a90671
Show file tree
Hide file tree
Showing 8 changed files with 430 additions and 109 deletions.
3 changes: 1 addition & 2 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,13 +2,12 @@ use chalk_ir::cast::{Cast, Caster};
use chalk_ir::interner::{ChalkIr, HasInterner};
use chalk_ir::{
self, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, ImplId, OpaqueTyId, ParameterKinds,
QuantifiedWhereClauses, StructId, Substitution, TraitId,
QuantifiedWhereClauses, StructId, Substitution, ToParameter, TraitId,
};
use chalk_parse::ast::*;
use chalk_rust_ir as rust_ir;
use chalk_rust_ir::{
Anonymize, AssociatedTyValueId, IntoWhereClauses, OpaqueTyDatum, OpaqueTyDatumBound,
ToParameter,
};
use lalrpop_intern::intern;
use std::collections::BTreeMap;
Expand Down
99 changes: 99 additions & 0 deletions chalk-ir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1250,6 +1250,14 @@ impl<T: HasInterner> Binders<T> {
Self { binders, value }
}

/// Wraps the given value in a binder without variables, i.e. `for<>
/// (value)`. Since our deBruijn indices count binders, not variables, this
/// is sometimes useful.
pub fn empty(interner: &T::Interner, value: T) -> Self {
let binders = ParameterKinds::new(interner);
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
Expand Down Expand Up @@ -1287,6 +1295,20 @@ impl<T: HasInterner> Binders<T> {
}
}

/// Transforms the inner value according to the given function; returns
/// `None` if the function returns `None`.
pub fn filter_map<U, OP>(self, op: OP) -> Option<Binders<U>>
where
OP: FnOnce(T) -> Option<U>,
U: HasInterner<Interner = T::Interner>,
{
let value = op(self.value)?;
Some(Binders {
binders: self.binders,
value,
})
}

pub fn map_ref<'a, U, OP>(&'a self, op: OP) -> Binders<U>
where
OP: FnOnce(&'a T) -> U,
Expand All @@ -1295,6 +1317,19 @@ impl<T: HasInterner> Binders<T> {
self.as_ref().map(op)
}

/// Creates a `Substitution` containing bound vars such that applying this
/// substitution will not change the value, i.e. `^0.0, ^0.1, ^0.2` and so
/// on.
pub fn identity_substitution(&self, interner: &T::Interner) -> Substitution<T::Interner> {
Substitution::from(
interner,
self.binders
.iter(interner)
.enumerate()
.map(|(i, pk)| (pk, i).to_parameter(interner)),
)
}

/// Creates a fresh binders that contains a single type
/// variable. The result of the closure will be embedded in this
/// binder. Note that you should be careful with what you return
Expand All @@ -1317,6 +1352,36 @@ impl<T: HasInterner> Binders<T> {
}
}

impl<T, I> Binders<Binders<T>>
where
T: Fold<I, I> + HasInterner<Interner = I>,
T::Result: HasInterner<Interner = I>,
I: Interner,
{
/// This turns two levels of binders (`for<A> for<B>`) into one level (`for<A, B>`).
pub fn fuse_binders(self, interner: &T::Interner) -> Binders<T::Result> {
let num_binders = self.len(interner);
// generate a substitution to shift the indexes of the inner binder:
let subst = Substitution::from(
interner,
self.value
.binders
.iter(interner)
.enumerate()
.map(|(i, pk)| (pk, i + num_binders).to_parameter(interner)),
);
let value = self.value.substitute(interner, &subst);
let binders = ParameterKinds::from(
interner,
self.binders
.iter(interner)
.chain(self.value.binders.iter(interner))
.cloned(),
);
Binders { binders, value }
}
}

impl<T: HasInterner> From<Binders<T>> for (ParameterKinds<T::Interner>, T) {
fn from(binders: Binders<T>) -> Self {
(binders.binders, binders.value)
Expand Down Expand Up @@ -2073,6 +2138,40 @@ where
}
}

pub trait ToParameter {
/// Utility for converting a list of all the binders into scope
/// into references to those binders. Simply pair the binders with
/// the indices, and invoke `to_parameter()` on the `(binder,
/// index)` pair. The result will be a reference to a bound
/// variable of appropriate kind at the corresponding index.
fn to_parameter<I: Interner>(&self, interner: &I) -> Parameter<I> {
self.to_parameter_at_depth(interner, DebruijnIndex::INNERMOST)
}

fn to_parameter_at_depth<I: Interner>(
&self,
interner: &I,
debruijn: DebruijnIndex,
) -> Parameter<I>;
}

impl<'a> ToParameter for (&'a ParameterKind<()>, usize) {
fn to_parameter_at_depth<I: Interner>(
&self,
interner: &I,
debruijn: DebruijnIndex,
) -> Parameter<I> {
let &(binder, index) = self;
let bound_var = BoundVar::new(debruijn, index);
match *binder {
ParameterKind::Lifetime(_) => LifetimeData::BoundVar(bound_var)
.intern(interner)
.cast(interner),
ParameterKind::Ty(_) => TyData::BoundVar(bound_var).intern(interner).cast(interner),
}
}
}

impl<'i, I: Interner> Folder<'i, I> for &SubstFolder<'i, I> {
fn as_dyn(&mut self) -> &mut dyn Folder<'i, I> {
self
Expand Down
50 changes: 13 additions & 37 deletions chalk-rust-ir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,9 @@ use chalk_ir::cast::Cast;
use chalk_ir::fold::shift::Shift;
use chalk_ir::interner::{Interner, TargetInterner};
use chalk_ir::{
AliasEq, AliasTy, AssocTypeId, Binders, BoundVar, DebruijnIndex, ImplId, LifetimeData,
OpaqueTyId, Parameter, ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId,
Substitution, TraitId, TraitRef, Ty, TyData, TypeName, WhereClause,
AliasEq, AliasTy, AssocTypeId, Binders, DebruijnIndex, ImplId, OpaqueTyId, Parameter,
ParameterKind, ProjectionTy, QuantifiedWhereClause, StructId, Substitution, ToParameter,
TraitId, TraitRef, Ty, TyData, TypeName, WhereClause,
};
use std::iter;

Expand Down Expand Up @@ -167,6 +167,16 @@ impl<I: Interner> TraitDatum<I> {
pub fn is_coinductive_trait(&self) -> bool {
self.flags.coinductive
}

/// Gives access to the where clauses of the trait, quantified over the type parameters of the trait:
///
/// ```ignore
/// trait Foo<T> where T: Debug { }
/// ^^^^^^^^^^^^^^
/// ```
pub fn where_clauses(&self) -> Binders<&Vec<QuantifiedWhereClause<I>>> {
self.binders.as_ref().map(|td| &td.where_clauses)
}
}

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

pub trait ToParameter {
/// Utility for converting a list of all the binders into scope
/// into references to those binders. Simply pair the binders with
/// the indices, and invoke `to_parameter()` on the `(binder,
/// index)` pair. The result will be a reference to a bound
/// variable of appropriate kind at the corresponding index.
fn to_parameter<I: Interner>(&self, interner: &I) -> Parameter<I> {
self.to_parameter_at_depth(interner, DebruijnIndex::INNERMOST)
}

fn to_parameter_at_depth<I: Interner>(
&self,
interner: &I,
debruijn: DebruijnIndex,
) -> Parameter<I>;
}

impl<'a> ToParameter for (&'a ParameterKind<()>, usize) {
fn to_parameter_at_depth<I: Interner>(
&self,
interner: &I,
debruijn: DebruijnIndex,
) -> Parameter<I> {
let &(binder, index) = self;
let bound_var = BoundVar::new(debruijn, index);
match *binder {
ParameterKind::Lifetime(_) => LifetimeData::BoundVar(bound_var)
.intern(interner)
.cast(interner),
ParameterKind::Ty(_) => TyData::BoundVar(bound_var).intern(interner).cast(interner),
}
}
}

/// Represents an associated type declaration found inside of a trait:
///
/// ```notrust
Expand Down
81 changes: 13 additions & 68 deletions chalk-solve/src/clauses.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ use rustc_hash::FxHashSet;

pub mod builder;
mod builtin_traits;
mod dyn_ty;
mod env_elaborator;
mod generalize;
pub mod program_clauses;
Expand Down Expand Up @@ -198,76 +199,20 @@ fn program_clauses_that_could_match<I: Interner>(
}
}

// If the self type `S` is a `dyn trait` type, we wish to generate program-clauses
// that indicates that it implements its own traits. For example, a `dyn Write` type
// implements `Write` and so on.
// If the self type is a `dyn trait` type, generate program-clauses
// that indicates that it implements its own traits.
// FIXME: This is presently rather wasteful, in that we don't check that the
// these program clauses we are generating are actually relevant to the goal
// `goal` that we are actually *trying* to prove (though there is some later
// code that will screen out irrelevant stuff).
//
// To see how this works, consider as an example the type `dyn Fn(&u8)`. This is
// really shorthand for `dyn for<'a> Fn<(&'a u8), Output = ()>`, and we represent
// that type as something like this:
//
// ```
// dyn(exists<T> {
// forall<'a> { Implemented(T: Fn<'a>) },
// forall<'a> { AliasEq(<T as Fn<'a>>::Output, ()) },
// })
// ```
//
// so what we will do is to generate one program clause
// for each of the conditions. Thus we get two program
// clauses:
//
// ```
// forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) }
// ```
//
// and
//
// ```
// forall<'a> { AliasEq(<dyn Fn(&u8) as Fn<'a>>::Output, ()) },
// ```
//
// FIXME. This is presently rather wasteful, in that we
// don't check that the these program clauses we are
// generating are actually relevant to the goal `goal`
// that we are actually *trying* to prove (though there is
// some later code that will screen out irrelevant
// stuff).
//
// In other words, in our example, if we were trying to
// prove `Implemented(dyn Fn(&u8): Clone)`, we would have
// generated two clauses that are totally irrelevant to
// that goal, because they let us prove other things but
// not `Clone`.
// In other words, if we were trying to prove `Implemented(dyn
// Fn(&u8): Clone)`, we would still generate two clauses that are
// totally irrelevant to that goal, because they let us prove other
// things but not `Clone`.
let self_ty = trait_ref.self_type_parameter(interner);
if let TyData::Dyn(dyn_ty) = self_ty.data(interner) {
// In this arm, `self_ty` is the `dyn Fn(&u8)`,
// and `bounded_ty` is the `exists<T> { .. }`
// clauses shown above.

// 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 TyData::Dyn(_) = self_ty.data(interner) {
dyn_ty::build_dyn_self_ty_clauses(db, builder, self_ty.clone())
}

match self_ty.data(interner) {
Expand Down
1 change: 0 additions & 1 deletion chalk-solve/src/clauses/builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ use crate::RustIrDatabase;
use chalk_ir::fold::Fold;
use chalk_ir::interner::{HasInterner, Interner};
use chalk_ir::*;
use chalk_rust_ir::*;
use std::marker::PhantomData;

/// The "clause builder" is a useful tool for building up sets of
Expand Down
Loading

0 comments on commit 2a90671

Please sign in to comment.