Skip to content

Add ProjectionTerm #745

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

Closed
wants to merge 14 commits into from
12 changes: 6 additions & 6 deletions chalk-engine/src/slg.rs
Original file line number Diff line number Diff line change
Expand Up @@ -306,15 +306,15 @@ impl<I: Interner> MayInvalidate<I> {

fn aggregate_projection_tys(
&mut self,
new: &ProjectionTy<I>,
current: &ProjectionTy<I>,
new: &ProjectionTerm<I>,
current: &ProjectionTerm<I>,
) -> bool {
let ProjectionTy {
associated_ty_id: new_name,
let ProjectionTerm {
associated_term_id: new_name,
substitution: new_substitution,
} = new;
let ProjectionTy {
associated_ty_id: current_name,
let ProjectionTerm {
associated_term_id: current_name,
substitution: current_substitution,
} = current;

Expand Down
18 changes: 9 additions & 9 deletions chalk-engine/src/slg/aggregate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -382,23 +382,23 @@ impl<I: Interner> AntiUnifier<'_, I> {

fn aggregate_projection_tys(
&mut self,
proj1: &ProjectionTy<I>,
proj2: &ProjectionTy<I>,
proj1: &ProjectionTerm<I>,
proj2: &ProjectionTerm<I>,
) -> Ty<I> {
let interner = self.interner;
let ProjectionTy {
associated_ty_id: name1,
let ProjectionTerm {
associated_term_id: name1,
substitution: substitution1,
} = proj1;
let ProjectionTy {
associated_ty_id: name2,
let ProjectionTerm {
associated_term_id: name2,
substitution: substitution2,
} = proj2;

self.aggregate_name_and_substs(name1, substitution1, name2, substitution2)
.map(|(&associated_ty_id, substitution)| {
TyKind::Alias(AliasTy::Projection(ProjectionTy {
associated_ty_id,
.map(|(&associated_term_id, substitution)| {
TyKind::Alias(AliasTy::Projection(ProjectionTerm {
associated_term_id,
substitution,
}))
.intern(interner)
Expand Down
22 changes: 11 additions & 11 deletions chalk-integration/src/db.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,15 +7,15 @@ use crate::{
tls, SolverChoice,
};
use chalk_ir::{
AdtId, AssocTypeId, Binders, Canonical, CanonicalVarKinds, ClosureId, ConstrainedSubst,
AdtId, AssocItemId, Binders, Canonical, CanonicalVarKinds, ClosureId, ConstrainedSubst,
Environment, FnDefId, GeneratorId, GenericArg, Goal, ImplId, InEnvironment, OpaqueTyId,
ProgramClause, ProgramClauses, Substitution, TraitId, Ty, TyKind, UCanonical,
UnificationDatabase, Variances,
};
use chalk_solve::rust_ir::{
AdtDatum, AdtRepr, AdtSizeAlign, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId,
ClosureKind, FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum,
ImplDatum, OpaqueTyDatum, TraitDatum, WellKnownTrait,
AdtDatum, AdtRepr, AdtSizeAlign, AssociatedTermDatum, AssociatedTermValue,
AssociatedTermValueId, ClosureKind, FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum,
GeneratorWitnessDatum, ImplDatum, OpaqueTyDatum, TraitDatum, WellKnownTrait,
};
use chalk_solve::{RustIrDatabase, Solution, SubstitutionResult};
use salsa::Database;
Expand Down Expand Up @@ -87,8 +87,8 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
self.program_ir().unwrap().custom_clauses()
}

fn associated_ty_data(&self, ty: AssocTypeId<ChalkIr>) -> Arc<AssociatedTyDatum<ChalkIr>> {
self.program_ir().unwrap().associated_ty_data(ty)
fn associated_term_data(&self, ty: AssocItemId<ChalkIr>) -> Arc<AssociatedTermDatum<ChalkIr>> {
self.program_ir().unwrap().associated_term_data(ty)
}

fn trait_datum(&self, id: TraitId<ChalkIr>) -> Arc<TraitDatum<ChalkIr>> {
Expand All @@ -99,11 +99,11 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
self.program_ir().unwrap().impl_datum(id)
}

fn associated_ty_value(
fn associated_term_value(
&self,
id: AssociatedTyValueId<ChalkIr>,
) -> Arc<AssociatedTyValue<ChalkIr>> {
self.program_ir().unwrap().associated_ty_values[&id].clone()
id: AssociatedTermValueId<ChalkIr>,
) -> Arc<AssociatedTermValue<ChalkIr>> {
self.program_ir().unwrap().associated_term_values[&id].clone()
}

fn opaque_ty_data(&self, id: OpaqueTyId<ChalkIr>) -> Arc<OpaqueTyDatum<ChalkIr>> {
Expand Down Expand Up @@ -235,7 +235,7 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
self.program_ir().unwrap().adt_name(struct_id)
}

fn assoc_type_name(&self, assoc_ty_id: AssocTypeId<ChalkIr>) -> String {
fn assoc_type_name(&self, assoc_ty_id: AssocItemId<ChalkIr>) -> String {
self.program_ir().unwrap().assoc_type_name(assoc_ty_id)
}

Expand Down
8 changes: 4 additions & 4 deletions chalk-integration/src/interner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,9 +4,9 @@ use chalk_ir::{
TyKind,
};
use chalk_ir::{
AdtId, AliasTy, AssocTypeId, CanonicalVarKind, CanonicalVarKinds, ConstData, Constraint,
AdtId, AliasTy, AssocItemId, CanonicalVarKind, CanonicalVarKinds, ConstData, Constraint,
Constraints, FnDefId, Goals, InEnvironment, Lifetime, OpaqueTy, OpaqueTyId,
ProgramClauseImplication, ProgramClauses, ProjectionTy, QuantifiedWhereClauses,
ProgramClauseImplication, ProgramClauses, ProjectionTerm, QuantifiedWhereClauses,
SeparatorTraitRef, Substitution, TraitId, Ty, TyData, VariableKind, VariableKinds, Variances,
};
use chalk_ir::{
Expand Down Expand Up @@ -91,7 +91,7 @@ impl Interner for ChalkIr {
}

fn debug_assoc_type_id(
id: AssocTypeId<ChalkIr>,
id: AssocItemId<ChalkIr>,
fmt: &mut fmt::Formatter<'_>,
) -> Option<fmt::Result> {
tls::with_current_program(|prog| Some(prog?.debug_assoc_type_id(id, fmt)))
Expand All @@ -113,7 +113,7 @@ impl Interner for ChalkIr {
}

fn debug_projection_ty(
proj: &ProjectionTy<ChalkIr>,
proj: &ProjectionTerm<ChalkIr>,
fmt: &mut fmt::Formatter<'_>,
) -> Option<fmt::Result> {
tls::with_current_program(|prog| Some(prog?.debug_projection_ty(proj, fmt)))
Expand Down
87 changes: 56 additions & 31 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ impl Lower for Program {
.map(|_| lowerer.next_item_id())
.collect::<Vec<_>>();

lowerer.extract_associated_types(self, &raw_ids)?;
lowerer.extract_associated_terms(self, &raw_ids)?;
lowerer.extract_ids(self, &raw_ids)?;
lowerer.lower(self, &raw_ids)
}
Expand Down Expand Up @@ -164,10 +164,10 @@ impl LowerWithEnv for WhereClause {
WhereClause::Implemented { trait_ref } => {
vec![chalk_ir::WhereClause::Implemented(trait_ref.lower(env)?)]
}
WhereClause::ProjectionEq { projection, ty } => vec![
WhereClause::ProjectionEq { projection, term } => vec![
chalk_ir::WhereClause::AliasEq(chalk_ir::AliasEq {
alias: chalk_ir::AliasTy::Projection(projection.lower(env)?),
ty: ty.lower(env)?,
term: term.lower(env)?,
}),
chalk_ir::WhereClause::Implemented(projection.trait_ref.lower(env)?),
],
Expand Down Expand Up @@ -216,10 +216,10 @@ impl LowerWithEnv for DomainGoal {
.into_iter()
.casted(interner)
.collect(),
DomainGoal::Normalize { projection, ty } => {
DomainGoal::Normalize { projection, term } => {
vec![chalk_ir::DomainGoal::Normalize(chalk_ir::Normalize {
alias: chalk_ir::AliasTy::Projection(projection.lower(env)?),
ty: ty.lower(env)?,
term: term.lower(env)?,
})]
}
DomainGoal::TyWellFormed { ty } => vec![chalk_ir::DomainGoal::WellFormed(
Expand Down Expand Up @@ -495,7 +495,7 @@ impl LowerWithEnv for AliasEqBound {

fn lower(&self, env: &Env) -> LowerResult<Self::Lowered> {
let trait_bound = self.trait_bound.lower(env)?;
let lookup = env.lookup_associated_ty(trait_bound.trait_id, &self.name)?;
let lookup = env.lookup_associated_term(trait_bound.trait_id, &self.name)?;
let args: Vec<_> = self
.args
.iter()
Expand Down Expand Up @@ -618,11 +618,11 @@ impl Lower for TraitFlags {
}
}

impl LowerWithEnv for ProjectionTy {
type Lowered = chalk_ir::ProjectionTy<ChalkIr>;
impl LowerWithEnv for ProjectionTerm {
type Lowered = chalk_ir::ProjectionTerm<ChalkIr>;

fn lower(&self, env: &Env) -> LowerResult<Self::Lowered> {
let ProjectionTy {
let ProjectionTerm {
ref trait_ref,
ref name,
ref args,
Expand All @@ -632,7 +632,7 @@ impl LowerWithEnv for ProjectionTy {
trait_id,
substitution: trait_substitution,
} = trait_ref.lower(env)?;
let lookup = env.lookup_associated_ty(trait_id, name)?;
let lookup = env.lookup_associated_term(trait_id, name)?;
let mut args: Vec<_> = args
.iter()
.map(|a| a.lower(env))
Expand All @@ -658,8 +658,8 @@ impl LowerWithEnv for ProjectionTy {

args.extend(trait_substitution.iter(interner).cloned());

Ok(chalk_ir::ProjectionTy {
associated_ty_id: lookup.id,
Ok(chalk_ir::ProjectionTerm {
associated_term_id: lookup.id,
substitution: chalk_ir::Substitution::from_iter(interner, args),
})
}
Expand Down Expand Up @@ -846,6 +846,17 @@ impl LowerWithEnv for Const {
}
}

impl LowerWithEnv for Term {
type Lowered = chalk_ir::Term<ChalkIr>;

fn lower(&self, env: &Env) -> LowerResult<Self::Lowered> {
Ok(match self {
Term::Ty(t) => chalk_ir::Term::Ty(t.lower(env)?),
Term::Const(c) => chalk_ir::Term::Const(c.lower(env)?),
})
}
}

impl LowerWithEnv for GenericArg {
type Lowered = chalk_ir::GenericArg<ChalkIr>;

Expand Down Expand Up @@ -892,11 +903,11 @@ impl LowerWithEnv for Lifetime {
}
}

impl LowerWithEnv for (&Impl, ImplId<ChalkIr>, &AssociatedTyValueIds) {
impl LowerWithEnv for (&Impl, ImplId<ChalkIr>, &AssociatedTermValueIds) {
type Lowered = rust_ir::ImplDatum<ChalkIr>;

fn lower(&self, env: &Env) -> LowerResult<Self::Lowered> {
let (impl_, impl_id, associated_ty_value_ids) = self;
let (impl_, impl_id, associated_term_value_ids) = self;

let polarity = impl_.polarity.lower();
let binders = env.in_binders(impl_.all_parameters(), |env| {
Expand All @@ -917,22 +928,28 @@ impl LowerWithEnv for (&Impl, ImplId<ChalkIr>, &AssociatedTyValueIds) {
})
})?;

// lookup the ids for each of the "associated type values"
// lookup the ids for each of the "associated term values"
// within the impl, which should have already assigned and
// stored in the map
let associated_ty_value_ids = impl_
let assoc_const_values = impl_
.assoc_const_values
.iter()
.map(|av| associated_term_value_ids[&(*impl_id, av.name.str.clone())]);

let associated_term_value_ids = impl_
.assoc_ty_values
.iter()
.map(|atv| associated_ty_value_ids[&(*impl_id, atv.name.str.clone())])
.map(|av| associated_term_value_ids[&(*impl_id, av.name.str.clone())])
.chain(assoc_const_values)
.collect();

debug!(?associated_ty_value_ids);
debug!(?associated_term_value_ids);

Ok(rust_ir::ImplDatum {
polarity,
binders,
impl_type: impl_.impl_type.lower(),
associated_ty_value_ids,
associated_term_value_ids,
})
}
}
Expand Down Expand Up @@ -1000,17 +1017,25 @@ impl LowerWithEnv for (&TraitDefn, chalk_ir::TraitId<ChalkIr>) {
})
})?;

let associated_ty_ids: Vec<_> = trait_defn
.assoc_ty_defns
.iter()
.map(|defn| env.lookup_associated_ty(*trait_id, &defn.name).unwrap().id)
.collect();
let assoc_ct_ids = trait_defn.assoc_const_defns.iter().map(|defn| {
env.lookup_associated_term(*trait_id, &defn.name)
.unwrap()
.id
});

let assoc_ty_ids = trait_defn.assoc_ty_defns.iter().map(|defn| {
env.lookup_associated_term(*trait_id, &defn.name)
.unwrap()
.id
});

let associated_term_ids: Vec<_> = assoc_ty_ids.chain(assoc_ct_ids).collect();

let trait_datum = rust_ir::TraitDatum {
id: *trait_id,
binders,
flags: trait_defn.flags.lower(),
associated_ty_ids,
associated_term_ids,
well_known: trait_defn.well_known.map(|def| def.lower()),
};

Expand All @@ -1022,17 +1047,17 @@ impl LowerWithEnv for (&TraitDefn, chalk_ir::TraitId<ChalkIr>) {

pub fn lower_goal(goal: &Goal, program: &LoweredProgram) -> LowerResult<chalk_ir::Goal<ChalkIr>> {
let interner = ChalkIr;
let associated_ty_lookups: BTreeMap<_, _> = program
.associated_ty_data
let associated_term_lookups: BTreeMap<_, _> = program
.associated_term_data
.iter()
.map(|(&associated_ty_id, datum)| {
.map(|(&associated_term_id, datum)| {
let trait_datum = &program.trait_data[&datum.trait_id];
let num_trait_params = trait_datum.binders.len(interner);
let num_addl_params = datum.binders.len(interner) - num_trait_params;
let addl_variable_kinds =
datum.binders.binders.as_slice(interner)[..num_addl_params].to_owned();
let lookup = AssociatedTyLookup {
id: associated_ty_id,
let lookup = AssociatedTermLookup {
id: associated_term_id,
addl_variable_kinds,
};
((datum.trait_id, datum.name.clone()), lookup)
Expand All @@ -1058,7 +1083,7 @@ pub fn lower_goal(goal: &Goal, program: &LoweredProgram) -> LowerResult<chalk_ir
closure_kinds: &program.closure_kinds,
trait_kinds: &program.trait_kinds,
opaque_ty_kinds: &program.opaque_ty_kinds,
associated_ty_lookups: &associated_ty_lookups,
associated_term_lookups: &associated_term_lookups,
foreign_ty_ids: &program.foreign_ty_ids,
parameter_map: BTreeMap::new(),
auto_traits: &auto_traits,
Expand Down
Loading