Skip to content

Commit

Permalink
Emit EqGoals for projections / simplify
Browse files Browse the repository at this point in the history
  • Loading branch information
nathanwhit committed Aug 19, 2020
1 parent 593c636 commit 497e5fe
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 37 deletions.
37 changes: 14 additions & 23 deletions chalk-solve/src/clauses/env_elaborator.rs
Original file line number Diff line number Diff line change
@@ -1,13 +1,11 @@
use super::program_clauses::ToProgramClauses;
use crate::clauses::builder::ClauseBuilder;
use crate::clauses::{match_alias_ty, match_type_name};
use crate::AliasEq;
use crate::DomainGoal;
use crate::FromEnv;
use crate::ProgramClause;
use crate::RustIrDatabase;
use crate::Ty;
use crate::WhereClause;
use crate::{debug_span, TyData};
use chalk_ir::interner::Interner;
use chalk_ir::visit::{Visit, Visitor};
Expand Down Expand Up @@ -85,32 +83,25 @@ impl<'me, I: Interner> Visitor<'me, I> for EnvElaborator<'me, I> {
}

fn visit_domain_goal(&mut self, domain_goal: &DomainGoal<I>, outer_binder: DebruijnIndex) {
match domain_goal {
DomainGoal::FromEnv(from_env) => {
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);
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(&mut self.builder, self.environment);
trait_datum.to_program_clauses(&mut 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(&mut 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(&mut self.builder, self.environment);
}
FromEnv::Ty(ty) => ty.visit_with(self, outer_binder),
}
FromEnv::Ty(ty) => ty.visit_with(self, outer_binder),
}
DomainGoal::Holds(WhereClause::AliasEq(AliasEq { alias, ty })) => {
match_alias_ty(&mut self.builder, self.environment, alias);
ty.visit_with(self, outer_binder);
}
_ => {}
}
}
}
16 changes: 2 additions & 14 deletions chalk-solve/src/clauses/syntactic_eq.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ use chalk_ir::{
cast::Cast,
fold::{shift::Shift, Fold, Folder, SuperFold},
interner::Interner,
AliasEq, AliasTy, Binders, BoundVar, DebruijnIndex, EqGoal, Fallible, Goal, GoalData, Goals,
AliasTy, Binders, BoundVar, DebruijnIndex, EqGoal, Fallible, Goal, GoalData, Goals,
ProgramClause, ProgramClauseData, ProgramClauseImplication, QuantifierKind, Ty, TyData, TyKind,
VariableKind, VariableKinds,
};
Expand Down Expand Up @@ -50,19 +50,7 @@ impl<'i, I: Interner> Folder<'i, I> for SynEqFolder<'i, I> {

let new_ty = TyData::BoundVar(bound_var).intern(interner);
match ty.data(interner) {
TyData::Alias(alias @ AliasTy::Projection(_)) => {
self.new_params.push(VariableKind::Ty(TyKind::General));
self.new_goals.push(
AliasEq {
alias: alias.clone(),
ty: new_ty.clone(),
}
.cast(interner),
);
self.binders_len += 1;
Ok(new_ty)
}
TyData::Function(_) => {
TyData::Alias(AliasTy::Projection(_)) | TyData::Function(_) => {
self.new_params.push(VariableKind::Ty(TyKind::General));
self.new_goals.push(
EqGoal {
Expand Down

0 comments on commit 497e5fe

Please sign in to comment.