diff options
Diffstat (limited to 'vendor/chalk-solve-0.87.0/src/clauses/program_clauses.rs')
| -rw-r--r-- | vendor/chalk-solve-0.87.0/src/clauses/program_clauses.rs | 921 |
1 files changed, 0 insertions, 921 deletions
diff --git a/vendor/chalk-solve-0.87.0/src/clauses/program_clauses.rs b/vendor/chalk-solve-0.87.0/src/clauses/program_clauses.rs deleted file mode 100644 index 19811ff8b..000000000 --- a/vendor/chalk-solve-0.87.0/src/clauses/program_clauses.rs +++ /dev/null @@ -1,921 +0,0 @@ -use crate::clauses::builder::ClauseBuilder; -use crate::rust_ir::*; -use crate::split::Split; -use chalk_ir::cast::{Cast, Caster}; -use chalk_ir::interner::Interner; -use chalk_ir::*; -use std::iter; -use tracing::instrument; - -/// Trait for lowering a given piece of rust-ir source (e.g., an impl -/// or struct definition) into its associated "program clauses" -- -/// that is, into the lowered, logical rules that it defines. -pub trait ToProgramClauses<I: Interner> { - fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>, environment: &Environment<I>); -} - -impl<I: Interner> ToProgramClauses<I> for ImplDatum<I> { - /// Given `impl<T: Clone> Clone for Vec<T> { ... }`, generate: - /// - /// ```notrust - /// -- Rule Implemented-From-Impl - /// forall<T> { - /// Implemented(Vec<T>: Clone) :- Implemented(T: Clone). - /// } - /// ``` - /// - /// For a negative impl like `impl... !Clone for ...`, however, we - /// generate nothing -- this is just a way to *opt out* from the - /// default auto trait impls, it doesn't have any positive effect - /// on its own. - fn to_program_clauses( - &self, - builder: &mut ClauseBuilder<'_, I>, - _environment: &Environment<I>, - ) { - if self.is_positive() { - let binders = self.binders.clone(); - builder.push_binders( - binders, - |builder, - ImplDatumBound { - trait_ref, - where_clauses, - }| { - builder.push_clause(trait_ref, where_clauses); - }, - ); - } - } -} - -impl<I: Interner> ToProgramClauses<I> for AssociatedTyValue<I> { - /// Given the following trait: - /// - /// ```notrust - /// trait Iterable { - /// type IntoIter<'a>: 'a; - /// } - /// ``` - /// - /// Then for the following impl: - /// ```notrust - /// impl<T> Iterable for Vec<T> where T: Clone { - /// type IntoIter<'a> = Iter<'a, T>; - /// } - /// ``` - /// - /// we generate: - /// - /// ```notrust - /// -- Rule Normalize-From-Impl - /// forall<'a, T> { - /// Normalize(<Vec<T> as Iterable>::IntoIter<'a> -> Iter<'a, T>>) :- - /// Implemented(T: Clone), // (1) - /// Implemented(Iter<'a, T>: 'a). // (2) - /// } - /// ``` - fn to_program_clauses( - &self, - builder: &mut ClauseBuilder<'_, I>, - _environment: &Environment<I>, - ) { - let impl_datum = builder.db.impl_datum(self.impl_id); - let associated_ty = builder.db.associated_ty_data(self.associated_ty_id); - - builder.push_binders(self.value.clone(), |builder, assoc_ty_value| { - let all_parameters = builder.placeholders_in_scope().to_vec(); - - // Get the projection for this associated type: - // - // * `impl_params`: `[!T]` - // * `projection`: `<Vec<!T> as Iterable>::Iter<'!a>` - let (impl_params, projection) = builder - .db - .impl_parameters_and_projection_from_associated_ty_value(&all_parameters, self); - - // Assemble the full list of conditions for projection to be valid. - // This comes in two parts, marked as (1) and (2) in doc above: - // - // 1. require that the where clauses from the impl apply - let interner = builder.db.interner(); - let impl_where_clauses = impl_datum - .binders - .map_ref(|b| &b.where_clauses) - .into_iter() - .map(|wc| wc.cloned().substitute(interner, impl_params)); - - // 2. any where-clauses from the `type` declaration in the trait: the - // parameters must be substituted with those of the impl - let assoc_ty_where_clauses = associated_ty - .binders - .map_ref(|b| &b.where_clauses) - .into_iter() - .map(|wc| wc.cloned().substitute(interner, &projection.substitution)); - - // Create the final program clause: - // - // ```notrust - // -- Rule Normalize-From-Impl - // forall<'a, T> { - // Normalize(<Vec<T> as Iterable>::IntoIter<'a> -> Iter<'a, T>>) :- - // Implemented(T: Clone), // (1) - // Implemented(Iter<'a, T>: 'a). // (2) - // } - // ``` - builder.push_clause( - Normalize { - alias: AliasTy::Projection(projection.clone()), - ty: assoc_ty_value.ty, - }, - impl_where_clauses.chain(assoc_ty_where_clauses), - ); - }); - } -} - -impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> { - /// Given `opaque type T<U>: A + B = HiddenTy where U: C;`, we generate: - /// - /// ```notrust - /// AliasEq(T<U> = HiddenTy) :- Reveal. - /// AliasEq(T<U> = !T<U>). - /// WF(T<U>) :- WF(U: C). - /// Implemented(!T<U>: A). - /// Implemented(!T<U>: B). - /// ``` - /// where `!T<..>` is the placeholder for the unnormalized type `T<..>`. - #[instrument(level = "debug", skip(builder))] - fn to_program_clauses( - &self, - builder: &mut ClauseBuilder<'_, I>, - _environment: &Environment<I>, - ) { - builder.push_binders(self.bound.clone(), |builder, opaque_ty_bound| { - let interner = builder.interner(); - let substitution = builder.substitution_in_scope(); - let alias = AliasTy::Opaque(OpaqueTy { - opaque_ty_id: self.opaque_ty_id, - substitution: substitution.clone(), - }); - - let alias_placeholder_ty = - TyKind::OpaqueType(self.opaque_ty_id, substitution).intern(interner); - - // AliasEq(T<..> = HiddenTy) :- Reveal. - builder.push_clause( - DomainGoal::Holds( - AliasEq { - alias: alias.clone(), - ty: builder.db.hidden_opaque_type(self.opaque_ty_id), - } - .cast(interner), - ), - iter::once(DomainGoal::Reveal), - ); - - // AliasEq(T<..> = !T<..>). - builder.push_fact(DomainGoal::Holds( - AliasEq { - alias, - ty: alias_placeholder_ty.clone(), - } - .cast(interner), - )); - - // WF(!T<..>) :- WF(WC). - builder.push_binders(opaque_ty_bound.where_clauses, |builder, where_clauses| { - builder.push_clause( - WellFormed::Ty(alias_placeholder_ty.clone()), - where_clauses - .into_iter() - .map(|wc| wc.into_well_formed_goal(interner)), - ); - }); - - let substitution = Substitution::from1(interner, alias_placeholder_ty); - for bound in opaque_ty_bound.bounds { - let bound_with_placeholder_ty = bound.substitute(interner, &substitution); - builder.push_binders(bound_with_placeholder_ty, |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(..) => {} - }); - } - }); - } -} - -/// Generates the "well-formed" program clauses for an applicative type -/// with the name `type_name`. For example, given a struct definition: -/// -/// ```ignore -/// struct Foo<T: Eq> { } -/// ``` -/// -/// we would generate the clause: -/// -/// ```notrust -/// forall<T> { -/// WF(Foo<T>) :- WF(T: Eq). -/// } -/// ``` -/// -/// # Parameters -/// - builder -- the clause builder. We assume all the generic types from `Foo` are in scope -/// - type_name -- in our example above, the name `Foo` -/// - where_clauses -- the list of where clauses declared on the type (`T: Eq`, in our example) -fn well_formed_program_clauses<'a, I, Wc>( - builder: &'a mut ClauseBuilder<'_, I>, - ty: Ty<I>, - where_clauses: Wc, -) where - I: Interner, - Wc: Iterator<Item = &'a QuantifiedWhereClause<I>>, -{ - let interner = builder.interner(); - builder.push_clause( - WellFormed::Ty(ty), - where_clauses - .cloned() - .map(|qwc| qwc.into_well_formed_goal(interner)), - ); -} - -/// Generates the "fully visible" program clauses for an applicative type -/// with the name `type_name`. For example, given a struct definition: -/// -/// ```ignore -/// struct Foo<T: Eq> { } -/// ``` -/// -/// we would generate the clause: -/// -/// ```notrust -/// forall<T> { -/// IsFullyVisible(Foo<T>) :- IsFullyVisible(T). -/// } -/// ``` -/// -/// # Parameters -/// -/// - builder -- the clause builder. We assume all the generic types from `Foo` are in scope -/// - type_name -- in our example above, the name `Foo` -fn fully_visible_program_clauses<I>( - builder: &mut ClauseBuilder<'_, I>, - ty: Ty<I>, - subst: &Substitution<I>, -) where - I: Interner, -{ - let interner = builder.interner(); - builder.push_clause( - DomainGoal::IsFullyVisible(ty), - subst - .type_parameters(interner) - .map(|typ| DomainGoal::IsFullyVisible(typ).cast::<Goal<_>>(interner)), - ); -} - -/// Generates the "implied bounds" clauses for an applicative -/// type with the name `type_name`. For example, if `type_name` -/// represents a struct `S` that is declared like: -/// -/// ```ignore -/// struct S<T> where T: Eq { } -/// ``` -/// -/// then we would generate the rule: -/// -/// ```notrust -/// FromEnv(T: Eq) :- FromEnv(S<T>) -/// ``` -/// -/// # Parameters -/// -/// - builder -- the clause builder. We assume all the generic types from `S` are in scope. -/// - type_name -- in our example above, the name `S` -/// - where_clauses -- the list of where clauses declared on the type (`T: Eq`, in our example). -fn implied_bounds_program_clauses<'a, I, Wc>( - builder: &'a mut ClauseBuilder<'_, I>, - ty: &Ty<I>, - where_clauses: Wc, -) where - I: Interner, - Wc: Iterator<Item = &'a QuantifiedWhereClause<I>>, -{ - let interner = builder.interner(); - - for qwc in where_clauses { - builder.push_binders(qwc.clone(), |builder, wc| { - builder.push_clause(wc.into_from_env_goal(interner), Some(ty.clone().from_env())); - }); - } -} - -impl<I: Interner> ToProgramClauses<I> for AdtDatum<I> { - /// Given the following type definition: `struct Foo<T: Eq> { }`, generate: - /// - /// ```notrust - /// -- Rule WellFormed-Type - /// forall<T> { - /// WF(Foo<T>) :- WF(T: Eq). - /// } - /// - /// -- Rule Implied-Bound-From-Type - /// forall<T> { - /// FromEnv(T: Eq) :- FromEnv(Foo<T>). - /// } - /// - /// forall<T> { - /// IsFullyVisible(Foo<T>) :- IsFullyVisible(T). - /// } - /// ``` - /// - /// If the type `Foo` is marked `#[upstream]`, we also generate: - /// - /// ```notrust - /// forall<T> { IsUpstream(Foo<T>). } - /// ``` - /// - /// Otherwise, if the type `Foo` is not marked `#[upstream]`, we generate: - /// ```notrust - /// forall<T> { IsLocal(Foo<T>). } - /// ``` - /// - /// Given an `#[upstream]` type that is also fundamental: - /// - /// ```notrust - /// #[upstream] - /// #[fundamental] - /// struct Box<T, U> {} - /// ``` - /// - /// We generate the following clauses: - /// - /// ```notrust - /// forall<T, U> { IsLocal(Box<T, U>) :- IsLocal(T). } - /// forall<T, U> { IsLocal(Box<T, U>) :- IsLocal(U). } - /// - /// forall<T, U> { IsUpstream(Box<T, U>) :- IsUpstream(T), IsUpstream(U). } - /// - /// // Generated for both upstream and local fundamental types - /// forall<T, U> { DownstreamType(Box<T, U>) :- DownstreamType(T). } - /// forall<T, U> { DownstreamType(Box<T, U>) :- DownstreamType(U). } - /// ``` - /// - #[instrument(level = "debug", skip(builder))] - fn to_program_clauses( - &self, - builder: &mut ClauseBuilder<'_, I>, - _environment: &Environment<I>, - ) { - let interner = builder.interner(); - let binders = self.binders.map_ref(|b| &b.where_clauses).cloned(); - - builder.push_binders(binders, |builder, where_clauses| { - let self_ty = TyKind::Adt(self.id, builder.substitution_in_scope()).intern(interner); - - well_formed_program_clauses(builder, self_ty.clone(), where_clauses.iter()); - - implied_bounds_program_clauses(builder, &self_ty, where_clauses.iter()); - - fully_visible_program_clauses( - builder, - self_ty.clone(), - &builder.substitution_in_scope(), - ); - - // Types that are not marked `#[upstream]` satisfy IsLocal(Ty) - if !self.flags.upstream { - // `IsLocalTy(Ty)` depends *only* on whether the type - // is marked #[upstream] and nothing else - builder.push_fact(DomainGoal::IsLocal(self_ty.clone())); - } else if self.flags.fundamental { - // If a type is `#[upstream]`, but is also - // `#[fundamental]`, it satisfies IsLocal if and only - // if its parameters satisfy IsLocal - for type_param in builder.substitution_in_scope().type_parameters(interner) { - builder.push_clause( - DomainGoal::IsLocal(self_ty.clone()), - Some(DomainGoal::IsLocal(type_param)), - ); - } - builder.push_clause( - DomainGoal::IsUpstream(self_ty.clone()), - builder - .substitution_in_scope() - .type_parameters(interner) - .map(|type_param| DomainGoal::IsUpstream(type_param)), - ); - } else { - // The type is just upstream and not fundamental - builder.push_fact(DomainGoal::IsUpstream(self_ty.clone())); - } - - if self.flags.fundamental { - assert!( - builder - .substitution_in_scope() - .type_parameters(interner) - .count() - >= 1, - "Only fundamental types with type parameters are supported" - ); - for type_param in builder.substitution_in_scope().type_parameters(interner) { - builder.push_clause( - DomainGoal::DownstreamType(self_ty.clone()), - Some(DomainGoal::DownstreamType(type_param)), - ); - } - } - }); - } -} - -impl<I: Interner> ToProgramClauses<I> for FnDefDatum<I> { - /// Given the following function definition: `fn bar<T>() where T: Eq`, generate: - /// - /// ```notrust - /// -- Rule WellFormed-Type - /// forall<T> { - /// WF(bar<T>) :- WF(T: Eq) - /// } - /// - /// -- Rule Implied-Bound-From-Type - /// forall<T> { - /// FromEnv(T: Eq) :- FromEnv(bar<T>). - /// } - /// - /// forall<T> { - /// IsFullyVisible(bar<T>) :- IsFullyVisible(T). - /// } - /// ``` - #[instrument(level = "debug", skip(builder))] - fn to_program_clauses( - &self, - builder: &mut ClauseBuilder<'_, I>, - _environment: &Environment<I>, - ) { - let interner = builder.interner(); - let binders = self.binders.map_ref(|b| &b.where_clauses).cloned(); - - builder.push_binders(binders, |builder, where_clauses| { - let ty = TyKind::FnDef(self.id, builder.substitution_in_scope()).intern(interner); - - well_formed_program_clauses(builder, ty.clone(), where_clauses.iter()); - - implied_bounds_program_clauses(builder, &ty, where_clauses.iter()); - - fully_visible_program_clauses(builder, ty, &builder.substitution_in_scope()); - }); - } -} - -impl<I: Interner> ToProgramClauses<I> for TraitDatum<I> { - /// Given the following trait declaration: `trait Ord<T> where Self: Eq<T> { ... }`, generate: - /// - /// ```notrust - /// -- Rule WellFormed-TraitRef - /// forall<Self, T> { - /// WF(Self: Ord<T>) :- Implemented(Self: Ord<T>), WF(Self: Eq<T>). - /// } - /// ``` - /// - /// and the reverse rules: - /// - /// ```notrust - /// -- Rule Implemented-From-Env - /// forall<Self, T> { - /// (Self: Ord<T>) :- FromEnv(Self: Ord<T>). - /// } - /// - /// -- Rule Implied-Bound-From-Trait - /// forall<Self, T> { - /// FromEnv(Self: Eq<T>) :- FromEnv(Self: Ord<T>). - /// } - /// ``` - /// - /// As specified in the orphan rules, if a trait is not marked `#[upstream]`, the current crate - /// can implement it for any type. To represent that, we generate: - /// - /// ```notrust - /// // `Ord<T>` would not be `#[upstream]` when compiling `std` - /// forall<Self, T> { LocalImplAllowed(Self: Ord<T>). } - /// ``` - /// - /// For traits that are `#[upstream]` (i.e. not in the current crate), the orphan rules dictate - /// that impls are allowed as long as at least one type parameter is local and each type - /// prior to that is fully visible. That means that each type prior to the first local - /// type cannot contain any of the type parameters of the impl. - /// - /// This rule is fairly complex, so we expand it and generate a program clause for each - /// possible case. This is represented as follows: - /// - /// ```notrust - /// // for `#[upstream] trait Foo<T, U, V> where Self: Eq<T> { ... }` - /// forall<Self, T, U, V> { - /// LocalImplAllowed(Self: Foo<T, U, V>) :- IsLocal(Self). - /// } - /// - /// forall<Self, T, U, V> { - /// LocalImplAllowed(Self: Foo<T, U, V>) :- - /// IsFullyVisible(Self), - /// IsLocal(T). - /// } - /// - /// forall<Self, T, U, V> { - /// LocalImplAllowed(Self: Foo<T, U, V>) :- - /// IsFullyVisible(Self), - /// IsFullyVisible(T), - /// IsLocal(U). - /// } - /// - /// forall<Self, T, U, V> { - /// LocalImplAllowed(Self: Foo<T, U, V>) :- - /// IsFullyVisible(Self), - /// IsFullyVisible(T), - /// IsFullyVisible(U), - /// IsLocal(V). - /// } - /// ``` - /// - /// The overlap check uses compatible { ... } mode to ensure that it accounts for impls that - /// may exist in some other *compatible* world. For every upstream trait, we add a rule to - /// account for the fact that upstream crates are able to compatibly add impls of upstream - /// traits for upstream types. - /// - /// ```notrust - /// // For `#[upstream] trait Foo<T, U, V> where Self: Eq<T> { ... }` - /// forall<Self, T, U, V> { - /// Implemented(Self: Foo<T, U, V>) :- - /// Implemented(Self: Eq<T>), // where clauses - /// Compatible, // compatible modality - /// IsUpstream(Self), - /// IsUpstream(T), - /// IsUpstream(U), - /// IsUpstream(V), - /// CannotProve. // returns ambiguous - /// } - /// ``` - /// - /// In certain situations, this is too restrictive. Consider the following code: - /// - /// ```notrust - /// /* In crate std */ - /// trait Sized { } - /// struct str { } - /// - /// /* In crate bar (depends on std) */ - /// trait Bar { } - /// impl Bar for str { } - /// impl<T> Bar for T where T: Sized { } - /// ``` - /// - /// Here, because of the rules we've defined, these two impls overlap. The std crate is - /// upstream to bar, and thus it is allowed to compatibly implement Sized for str. If str - /// can implement Sized in a compatible future, these two impls definitely overlap since the - /// second impl covers all types that implement Sized. - /// - /// The solution we've got right now is to mark Sized as "fundamental" when it is defined. - /// This signals to the Rust compiler that it can rely on the fact that str does not - /// implement Sized in all contexts. A consequence of this is that we can no longer add an - /// implementation of Sized compatibly for str. This is the trade off you make when defining - /// a fundamental trait. - /// - /// To implement fundamental traits, we simply just do not add the rule above that allows - /// upstream types to implement upstream traits. Fundamental traits are not allowed to - /// compatibly do that. - fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>, environment: &Environment<I>) { - let interner = builder.interner(); - let binders = self.binders.map_ref(|b| &b.where_clauses).cloned(); - builder.push_binders(binders, |builder, where_clauses| { - let trait_ref = chalk_ir::TraitRef { - trait_id: self.id, - substitution: builder.substitution_in_scope(), - }; - - builder.push_clause( - trait_ref.clone().well_formed(), - where_clauses - .iter() - .cloned() - .map(|qwc| qwc.into_well_formed_goal(interner)) - .casted::<Goal<_>>(interner) - .chain(Some(trait_ref.clone().cast(interner))), - ); - - // The number of parameters will always be at least 1 - // because of the Self parameter that is automatically - // added to every trait. This is important because - // otherwise the added program clauses would not have any - // conditions. - let type_parameters: Vec<_> = trait_ref.type_parameters(interner).collect(); - - if environment.has_compatible_clause(interner) { - // Note: even though we do check for a `Compatible` clause here, - // we also keep it as a condition for the clauses below, purely - // for logical consistency. But really, it's not needed and could be - // removed. - - // Drop trait can't have downstream implementation because it can only - // be implemented with the same genericity as the struct definition, - // i.e. Drop implementation for `struct S<T: Eq> {}` is forced to be - // `impl Drop<T: Eq> for S<T> { ... }`. That means that orphan rules - // prevent Drop from being implemented in downstream crates. - if self.well_known != Some(WellKnownTrait::Drop) { - // Add all cases for potential downstream impls that could exist - for i in 0..type_parameters.len() { - builder.push_clause( - trait_ref.clone(), - where_clauses - .iter() - .cloned() - .casted(interner) - .chain(iter::once(DomainGoal::Compatible.cast(interner))) - .chain((0..i).map(|j| { - DomainGoal::IsFullyVisible(type_parameters[j].clone()) - .cast(interner) - })) - .chain(iter::once( - DomainGoal::DownstreamType(type_parameters[i].clone()) - .cast(interner), - )) - .chain(iter::once(GoalData::CannotProve.intern(interner))), - ); - } - } - - // Fundamental traits can be reasoned about negatively without any ambiguity, so no - // need for this rule if the trait is fundamental. - if !self.flags.fundamental { - builder.push_clause( - trait_ref.clone(), - where_clauses - .iter() - .cloned() - .casted(interner) - .chain(iter::once(DomainGoal::Compatible.cast(interner))) - .chain( - trait_ref - .type_parameters(interner) - .map(|ty| DomainGoal::IsUpstream(ty).cast(interner)), - ) - .chain(iter::once(GoalData::CannotProve.intern(interner))), - ); - } - } - - // Orphan rules: - if !self.flags.upstream { - // Impls for traits declared locally always pass the impl rules - builder.push_fact(DomainGoal::LocalImplAllowed(trait_ref.clone())); - } else { - // Impls for remote traits must have a local type in the right place - for i in 0..type_parameters.len() { - builder.push_clause( - DomainGoal::LocalImplAllowed(trait_ref.clone()), - (0..i) - .map(|j| DomainGoal::IsFullyVisible(type_parameters[j].clone())) - .chain(Some(DomainGoal::IsLocal(type_parameters[i].clone()))), - ); - } - } - - // Reverse implied bound rules: given (e.g.) `trait Foo: Bar + Baz`, - // we create rules like: - // - // ``` - // FromEnv(T: Bar) :- FromEnv(T: Foo) - // ``` - // - // and - // - // ``` - // FromEnv(T: Baz) :- FromEnv(T: Foo) - // ``` - for qwc in where_clauses { - builder.push_binders(qwc, |builder, wc| { - builder.push_clause( - wc.into_from_env_goal(interner), - Some(trait_ref.clone().from_env()), - ); - }); - } - - // Finally, for every trait `Foo` we make a rule - // - // ``` - // Implemented(T: Foo) :- FromEnv(T: Foo) - // ``` - builder.push_clause(trait_ref.clone(), Some(trait_ref.from_env())); - }); - } -} - -impl<I: Interner> ToProgramClauses<I> for AssociatedTyDatum<I> { - /// For each associated type, we define the "projection - /// equality" rules. There are always two; one for a successful normalization, - /// and one for the "fallback" notion of equality. - /// - /// Given: (here, `'a` and `T` represent zero or more parameters) - /// - /// ```notrust - /// trait Foo { - /// type Assoc<'a, T>: Bounds where WC; - /// } - /// ``` - /// - /// we generate the 'fallback' rule: - /// - /// ```notrust - /// -- Rule AliasEq-Placeholder - /// forall<Self, 'a, T> { - /// AliasEq(<Self as Foo>::Assoc<'a, T> = (Foo::Assoc<'a, T>)<Self>). - /// } - /// ``` - /// - /// and - /// - /// ```notrust - /// -- Rule AliasEq-Normalize - /// forall<Self, 'a, T, U> { - /// AliasEq(<T as Foo>::Assoc<'a, T> = U) :- - /// Normalize(<T as Foo>::Assoc -> U). - /// } - /// ``` - /// - /// We used to generate an "elaboration" rule like this: - /// - /// ```notrust - /// forall<T> { - /// T: Foo :- exists<U> { AliasEq(<T as Foo>::Assoc = U) }. - /// } - /// ``` - /// - /// but this caused problems with the recursive solver. In - /// particular, whenever normalization is possible, we cannot - /// solve that projection uniquely, since we can now elaborate - /// `AliasEq` to fallback *or* normalize it. So instead we - /// handle this kind of reasoning through the `FromEnv` predicate. - /// - /// We also generate rules specific to WF requirements and implied bounds: - /// - /// ```notrust - /// -- Rule WellFormed-AssocTy - /// forall<Self, 'a, T> { - /// WellFormed((Foo::Assoc)<Self, 'a, T>) :- WellFormed(Self: Foo), WellFormed(WC). - /// } - /// - /// -- Rule Implied-WC-From-AssocTy - /// forall<Self, 'a, T> { - /// FromEnv(WC) :- FromEnv((Foo::Assoc)<Self, 'a, T>). - /// } - /// - /// -- Rule Implied-Bound-From-AssocTy - /// forall<Self, 'a, T> { - /// FromEnv(<Self as Foo>::Assoc<'a,T>: Bounds) :- FromEnv(Self: Foo), WC. - /// } - /// - /// -- Rule Implied-Trait-From-AssocTy - /// forall<Self,'a, T> { - /// FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self, 'a,T>). - /// } - /// ``` - fn to_program_clauses( - &self, - builder: &mut ClauseBuilder<'_, I>, - _environment: &Environment<I>, - ) { - let interner = builder.interner(); - let binders = self.binders.clone(); - builder.push_binders( - binders, - |builder, - AssociatedTyDatumBound { - where_clauses, - bounds, - }| { - let substitution = builder.substitution_in_scope(); - - let projection = ProjectionTy { - associated_ty_id: self.id, - substitution: substitution.clone(), - }; - let projection_ty = AliasTy::Projection(projection.clone()).intern(interner); - - // Retrieve the trait ref embedding the associated type - let trait_ref = builder.db.trait_ref_from_projection(&projection); - - // Construct an application from the projection. So if we have `<T as Iterator>::Item`, - // we would produce `(Iterator::Item)<T>`. - let ty = TyKind::AssociatedType(self.id, substitution).intern(interner); - - let projection_eq = AliasEq { - alias: AliasTy::Projection(projection.clone()), - ty: ty.clone(), - }; - - // Fallback rule. The solver uses this to move between the projection - // and placeholder type. - // - // forall<Self> { - // AliasEq(<Self as Foo>::Assoc = (Foo::Assoc)<Self>). - // } - builder.push_fact_with_priority(projection_eq, None, ClausePriority::Low); - - // Well-formedness of projection type. - // - // forall<Self> { - // WellFormed((Foo::Assoc)<Self>) :- WellFormed(Self: Foo), WellFormed(WC). - // } - builder.push_clause( - WellFormed::Ty(ty.clone()), - iter::once(WellFormed::Trait(trait_ref.clone()).cast::<Goal<_>>(interner)) - .chain( - where_clauses - .iter() - .cloned() - .map(|qwc| qwc.into_well_formed_goal(interner)) - .casted(interner), - ), - ); - - // Assuming well-formedness of projection type means we can assume - // the trait ref as well. Mostly used in function bodies. - // - // forall<Self> { - // FromEnv(Self: Foo) :- FromEnv((Foo::Assoc)<Self>). - // } - builder.push_clause(FromEnv::Trait(trait_ref.clone()), Some(ty.from_env())); - - // Reverse rule for where clauses. - // - // forall<Self> { - // FromEnv(WC) :- FromEnv((Foo::Assoc)<Self>). - // } - // - // This is really a family of clauses, one for each where clause. - for qwc in &where_clauses { - builder.push_binders(qwc.clone(), |builder, wc| { - builder.push_clause( - wc.into_from_env_goal(interner), - Some(FromEnv::Ty(ty.clone())), - ); - }); - } - - // Reverse rule for implied bounds. - // - // forall<Self> { - // FromEnv(<Self as Foo>::Assoc: Bounds) :- FromEnv(Self: Foo), WC - // } - for quantified_bound in bounds { - builder.push_binders(quantified_bound, |builder, bound| { - for wc in bound.into_where_clauses(interner, projection_ty.clone()) { - builder.push_clause( - wc.into_from_env_goal(interner), - iter::once( - FromEnv::Trait(trait_ref.clone()).cast::<Goal<_>>(interner), - ) - .chain(where_clauses.iter().cloned().casted(interner)), - ); - } - }); - } - - // add new type parameter U - builder.push_bound_ty(|builder, ty| { - // `Normalize(<T as Foo>::Assoc -> U)` - let normalize = Normalize { - alias: AliasTy::Projection(projection.clone()), - ty: ty.clone(), - }; - - // `AliasEq(<T as Foo>::Assoc = U)` - let projection_eq = AliasEq { - alias: AliasTy::Projection(projection), - ty, - }; - - // Projection equality rule from above. - // - // forall<T, U> { - // AliasEq(<T as Foo>::Assoc = U) :- - // Normalize(<T as Foo>::Assoc -> U). - // } - builder.push_clause(projection_eq, Some(normalize)); - }); - }, - ); - } -} |