Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make dyn Trait implement its super traits as well #415

Merged
merged 1 commit into from
May 4, 2020
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
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 {
flodiebold marked this conversation as resolved.
Show resolved Hide resolved
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>>
flodiebold marked this conversation as resolved.
Show resolved Hide resolved
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>>> {
flodiebold marked this conversation as resolved.
Show resolved Hide resolved
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