diff options
Diffstat (limited to 'vendor/chalk-solve-0.87.0/src/clauses/env_elaborator.rs')
-rw-r--r-- | vendor/chalk-solve-0.87.0/src/clauses/env_elaborator.rs | 107 |
1 files changed, 107 insertions, 0 deletions
diff --git a/vendor/chalk-solve-0.87.0/src/clauses/env_elaborator.rs b/vendor/chalk-solve-0.87.0/src/clauses/env_elaborator.rs new file mode 100644 index 000000000..29032a7ad --- /dev/null +++ b/vendor/chalk-solve-0.87.0/src/clauses/env_elaborator.rs @@ -0,0 +1,107 @@ +use super::program_clauses::ToProgramClauses; +use crate::clauses::builder::ClauseBuilder; +use crate::clauses::{match_alias_ty, match_ty}; +use crate::DomainGoal; +use crate::FromEnv; +use crate::ProgramClause; +use crate::RustIrDatabase; +use crate::Ty; +use crate::{debug_span, TyKind}; +use chalk_ir::interner::Interner; +use chalk_ir::visit::{TypeVisitable, TypeVisitor}; +use chalk_ir::{DebruijnIndex, Environment}; +use rustc_hash::FxHashSet; +use std::ops::ControlFlow; +use tracing::instrument; + +/// When proving a `FromEnv` goal, we elaborate all `FromEnv` goals +/// found in the environment. +/// +/// For example, when `T: Clone` is in the environment, we can prove +/// `T: Copy` by adding the clauses from `trait Clone`, which includes +/// the rule `FromEnv(T: Copy) :- FromEnv(T: Clone) +pub(super) fn elaborate_env_clauses<I: Interner>( + db: &dyn RustIrDatabase<I>, + in_clauses: &[ProgramClause<I>], + out: &mut FxHashSet<ProgramClause<I>>, + environment: &Environment<I>, +) { + let mut this_round = vec![]; + let builder = &mut ClauseBuilder::new(db, &mut this_round); + let mut elaborater = EnvElaborator { + db, + builder, + environment, + }; + in_clauses.visit_with(&mut elaborater, DebruijnIndex::INNERMOST); + out.extend(this_round); +} + +struct EnvElaborator<'me, 'builder, I: Interner> { + db: &'me dyn RustIrDatabase<I>, + builder: &'builder mut ClauseBuilder<'me, I>, + environment: &'me Environment<I>, +} + +impl<'me, 'builder, I: Interner> TypeVisitor<I> for EnvElaborator<'me, 'builder, I> { + type BreakTy = (); + + fn as_dyn(&mut self) -> &mut dyn TypeVisitor<I, BreakTy = Self::BreakTy> { + self + } + + fn interner(&self) -> I { + self.db.interner() + } + #[instrument(level = "debug", skip(self, _outer_binder))] + fn visit_ty(&mut self, ty: &Ty<I>, _outer_binder: DebruijnIndex) -> ControlFlow<()> { + match ty.kind(self.interner()) { + TyKind::Alias(alias_ty) => match_alias_ty(self.builder, self.environment, alias_ty), + TyKind::Placeholder(_) => {} + + // FIXME(#203) -- We haven't fully figured out the implied + // bounds story around `dyn Trait` types. + TyKind::Dyn(_) => (), + + TyKind::Function(_) | TyKind::BoundVar(_) | TyKind::InferenceVar(_, _) => (), + + _ => { + // This shouldn't fail because of the above clauses + match_ty(self.builder, self.environment, ty) + .map_err(|_| ()) + .unwrap() + } + } + ControlFlow::Continue(()) + } + + fn visit_domain_goal( + &mut self, + domain_goal: &DomainGoal<I>, + outer_binder: DebruijnIndex, + ) -> ControlFlow<()> { + if let DomainGoal::FromEnv(from_env) = domain_goal { + debug_span!("visit_domain_goal", ?from_env); + match from_env { + FromEnv::Trait(trait_ref) => { + let trait_datum = self.db.trait_datum(trait_ref.trait_id); + + trait_datum.to_program_clauses(self.builder, self.environment); + + // If we know that `T: Iterator`, then we also know + // things about `<T as Iterator>::Item`, so push those + // implied bounds too: + for &associated_ty_id in &trait_datum.associated_ty_ids { + self.db + .associated_ty_data(associated_ty_id) + .to_program_clauses(self.builder, self.environment); + } + ControlFlow::Continue(()) + } + FromEnv::Ty(ty) => ty.visit_with(self, outer_binder), + } + } else { + ControlFlow::Continue(()) + } + } +} |