summaryrefslogtreecommitdiffstats
path: root/vendor/chalk-solve-0.87.0/src/clauses/dyn_ty.rs
diff options
context:
space:
mode:
Diffstat (limited to 'vendor/chalk-solve-0.87.0/src/clauses/dyn_ty.rs')
-rw-r--r--vendor/chalk-solve-0.87.0/src/clauses/dyn_ty.rs81
1 files changed, 81 insertions, 0 deletions
diff --git a/vendor/chalk-solve-0.87.0/src/clauses/dyn_ty.rs b/vendor/chalk-solve-0.87.0/src/clauses/dyn_ty.rs
new file mode 100644
index 000000000..505da43f9
--- /dev/null
+++ b/vendor/chalk-solve-0.87.0/src/clauses/dyn_ty.rs
@@ -0,0 +1,81 @@
+use super::{builder::ClauseBuilder, generalize};
+use crate::RustIrDatabase;
+use chalk_ir::{cast::Cast, interner::Interner, Ty, TyKind, WhereClause};
+
+/// If the self type `S` of an `Implemented` goal 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.
+///
+/// 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:
+///
+/// ```ignore
+/// 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:
+///
+/// ```ignore
+/// forall<'a> { Implemented(dyn Fn(&u8): Fn<(&'a u8)>) }
+/// ```
+///
+/// and
+///
+/// ```ignore
+/// forall<'a> { AliasEq(<dyn Fn(&u8) as Fn<'a>>::Output, ()) },
+/// ```
+pub(super) fn build_dyn_self_ty_clauses<I: Interner>(
+ db: &dyn RustIrDatabase<I>,
+ builder: &mut ClauseBuilder<'_, I>,
+ self_ty: Ty<I>,
+) {
+ let interner = db.interner();
+ let dyn_ty = match self_ty.kind(interner) {
+ TyKind::Dyn(dyn_ty) => dyn_ty.clone(),
+ _ => return,
+ };
+ let generalized_dyn_ty = generalize::Generalize::apply(db.interner(), dyn_ty);
+
+ // Here, `self_ty` is the `dyn Fn(&u8)`, and `dyn_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>`.
+
+ 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
+ .cloned()
+ .substitute(interner, &[self_ty.clone().cast(interner)]);
+
+ builder.push_binders(qwc, |builder, bound| match &bound {
+ // For the implemented traits, we need to elaborate super traits and add where clauses from the trait
+ WhereClause::Implemented(trait_ref) => {
+ super::super_traits::push_trait_super_clauses(
+ builder.db,
+ builder,
+ trait_ref.clone(),
+ )
+ }
+ // FIXME: Associated item bindings are just taken as facts (?)
+ WhereClause::AliasEq(_) => builder.push_fact(bound),
+ WhereClause::LifetimeOutlives(..) => {}
+ WhereClause::TypeOutlives(..) => {}
+ });
+ }
+ });
+}