Skip to content

Commit 9586104

Browse files
JulianKnodtJulianKnodt
committed
Add const eq where clauses
1 parent 8075c30 commit 9586104

File tree

9 files changed

+103
-17
lines changed

9 files changed

+103
-17
lines changed

‎chalk-integration/src/lowering.rs‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -171,6 +171,12 @@ impl LowerWithEnv for WhereClause {
171171
}),
172172
chalk_ir::WhereClause::Implemented(projection.trait_ref.lower(env)?),
173173
],
174+
WhereClause::ConstProjectionEq { projection, val } => {
175+
vec![chalk_ir::WhereClause::ConstEq(chalk_ir::ConstEq {
176+
term: chalk_ir::AliasTy::Projection(projection.lower(env)?),
177+
ct: val.lower(env)?,
178+
})]
179+
}
174180
WhereClause::LifetimeOutlives { a, b } => {
175181
vec![chalk_ir::WhereClause::LifetimeOutlives(
176182
chalk_ir::LifetimeOutlives {

‎chalk-integration/src/lowering/env.rs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,8 @@ pub type AssociatedTyLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), Ass
2929
pub type AssociatedTyValueIds =
3030
BTreeMap<(chalk_ir::ImplId<ChalkIr>, Ident), AssociatedTyValueId<ChalkIr>>;
3131

32-
pub type AssociatedConstLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedConstLookup>;
32+
pub type AssociatedConstLookups =
33+
BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedConstLookup>;
3334
pub type AssociatedConstValueIds =
3435
BTreeMap<(chalk_ir::ImplId<ChalkIr>, Ident), AssociatedConstValueId<ChalkIr>>;
3536
pub type ForeignIds = BTreeMap<Ident, chalk_ir::ForeignDefId<ChalkIr>>;

‎chalk-integration/src/lowering/program_lowerer.rs‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -361,15 +361,17 @@ impl ProgramLowerer {
361361
}
362362

363363
for acv in &impl_defn.assoc_const_values {
364-
let acv_id = self.associated_const_value_ids[&(impl_id, acv.name.str.clone())];
365-
let lookup = &self.associated_const_lookups[&(trait_id, acv.name.str.clone())];
364+
let acv_id =
365+
self.associated_const_value_ids[&(impl_id, acv.name.str.clone())];
366+
let lookup =
367+
&self.associated_const_lookups[&(trait_id, acv.name.str.clone())];
366368

367369
associated_const_values.insert(
368-
acv_id,
369-
Arc::new(rust_ir::AssociatedConstValue {
370-
impl_id,
371-
associated_const_id: lookup.id,
372-
}),
370+
acv_id,
371+
Arc::new(rust_ir::AssociatedConstValue {
372+
impl_id,
373+
associated_const_id: lookup.id,
374+
}),
373375
);
374376
}
375377
}

‎chalk-integration/src/program.rs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -9,10 +9,10 @@ use chalk_ir::{
99
Substitution, TraitId, Ty, TyKind, UintTy, Variances,
1010
};
1111
use chalk_solve::rust_ir::{
12-
AdtDatum, AdtRepr, AdtSizeAlign, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId,
13-
AssociatedConstValue, AssociatedConstValueId,
14-
ClosureKind, FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum,
15-
ImplDatum, ImplType, OpaqueTyDatum, TraitDatum, WellKnownTrait,
12+
AdtDatum, AdtRepr, AdtSizeAlign, AssociatedConstValue, AssociatedConstValueId,
13+
AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ClosureKind, FnDefDatum,
14+
FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum, ImplDatum, ImplType,
15+
OpaqueTyDatum, TraitDatum, WellKnownTrait,
1616
};
1717
use chalk_solve::split::Split;
1818
use chalk_solve::RustIrDatabase;

‎chalk-ir/src/debug.rs‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -786,11 +786,18 @@ impl<I: Interner> Debug for AliasEq<I> {
786786
}
787787
}
788788

789+
impl<I: Interner> Debug for ConstEq<I> {
790+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
791+
write!(fmt, "ConstEq(const {:?} = {:?})", self.term, self.ct)
792+
}
793+
}
794+
789795
impl<I: Interner> Debug for WhereClause<I> {
790796
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
791797
match self {
792798
WhereClause::Implemented(tr) => write!(fmt, "Implemented({:?})", tr.with_colon()),
793799
WhereClause::AliasEq(a) => write!(fmt, "{:?}", a),
800+
WhereClause::ConstEq(a) => write!(fmt, "{:?}", a),
794801
WhereClause::LifetimeOutlives(l_o) => write!(fmt, "{:?}", l_o),
795802
WhereClause::TypeOutlives(t_o) => write!(fmt, "{:?}", t_o),
796803
}

‎chalk-ir/src/lib.rs‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -728,6 +728,26 @@ impl<I: Interner> TyKind<I> {
728728
dyn_flags |= alias_eq.alias.compute_flags(interner);
729729
dyn_flags |= alias_eq.ty.data(interner).flags;
730730
}
731+
WhereClause::ConstEq(ct_eq) => {
732+
// TODO it's not a type projection but is that fine?
733+
// TODO do I need to add other flags here?
734+
dyn_flags |= TypeFlags::HAS_TY_PROJECTION;
735+
let const_data = ct_eq.ct.data(interner);
736+
dyn_flags |= const_data.ty.data(interner).flags
737+
| match const_data.value {
738+
ConstValue::BoundVar(_) | ConstValue::Concrete(_) => {
739+
TypeFlags::empty()
740+
}
741+
ConstValue::InferenceVar(_) => {
742+
TypeFlags::HAS_CT_INFER
743+
| TypeFlags::STILL_FURTHER_SPECIALIZABLE
744+
}
745+
ConstValue::Placeholder(_) => {
746+
TypeFlags::HAS_CT_PLACEHOLDER
747+
| TypeFlags::STILL_FURTHER_SPECIALIZABLE
748+
}
749+
}
750+
}
731751
WhereClause::LifetimeOutlives(lifetime_outlives) => {
732752
dyn_flags |= lifetime_outlives.a.compute_flags(interner)
733753
| lifetime_outlives.b.compute_flags(interner);
@@ -1743,13 +1763,16 @@ pub enum WhereClause<I: Interner> {
17431763
LifetimeOutlives(LifetimeOutlives<I>),
17441764
/// Type outlives a lifetime.
17451765
TypeOutlives(TypeOutlives<I>),
1766+
/// Const is equal to another const
1767+
ConstEq(ConstEq<I>),
17461768
}
17471769

17481770
impl<I: Interner> Copy for WhereClause<I>
17491771
where
17501772
I::InternedSubstitution: Copy,
17511773
I::InternedLifetime: Copy,
17521774
I::InternedType: Copy,
1775+
I::InternedConst: Copy,
17531776
{
17541777
}
17551778

@@ -1908,6 +1931,7 @@ where
19081931
I::InternedSubstitution: Copy,
19091932
I::InternedLifetime: Copy,
19101933
I::InternedType: Copy,
1934+
I::InternedConst: Copy,
19111935
{
19121936
}
19131937

@@ -1939,6 +1963,7 @@ impl<I: Interner> WhereClause<I> {
19391963
match self {
19401964
WhereClause::Implemented(trait_ref) => Some(trait_ref.trait_id),
19411965
WhereClause::AliasEq(_) => None,
1966+
WhereClause::ConstEq(_) => None,
19421967
WhereClause::LifetimeOutlives(_) => None,
19431968
WhereClause::TypeOutlives(_) => None,
19441969
}
@@ -2046,6 +2071,26 @@ impl<I: Interner> HasInterner for AliasEq<I> {
20462071
type Interner = I;
20472072
}
20482073

2074+
/// Proves **equality** between an alias and a type.
2075+
#[derive(Clone, PartialEq, Eq, Hash, Fold, Visit, Zip)]
2076+
#[allow(missing_docs)]
2077+
pub struct ConstEq<I: Interner> {
2078+
/// The id for the associated type member.
2079+
pub term: AssocItemId<I>,
2080+
2081+
pub ct: Const<I>,
2082+
}
2083+
impl<I: Interner> Copy for ConstEq<I>
2084+
where
2085+
I::InternedSubstitution: Copy,
2086+
I::InternedConst: Copy,
2087+
{
2088+
}
2089+
2090+
impl<I: Interner> HasInterner for ConstEq<I> {
2091+
type Interner = I;
2092+
}
2093+
20492094
/// Indicates that the `value` is universally quantified over `N`
20502095
/// parameters of the given kinds, where `N == self.binders.len()`. A
20512096
/// variable with depth `i < N` refers to the value at
@@ -2610,6 +2655,7 @@ pub enum GoalData<I: Interner> {
26102655
impl<I: Interner> Copy for GoalData<I>
26112656
where
26122657
I::InternedType: Copy,
2658+
I::InternedConst: Copy,
26132659
I::InternedLifetime: Copy,
26142660
I::InternedGenericArg: Copy,
26152661
I::InternedSubstitution: Copy,

‎chalk-parse/src/ast.rs‎

Lines changed: 20 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -455,10 +455,26 @@ impl fmt::Display for Identifier {
455455

456456
#[derive(Clone, PartialEq, Eq, Debug)]
457457
pub enum WhereClause {
458-
Implemented { trait_ref: TraitRef },
459-
ProjectionEq { projection: ProjectionTerm, ty: Ty },
460-
LifetimeOutlives { a: Lifetime, b: Lifetime },
461-
TypeOutlives { ty: Ty, lifetime: Lifetime },
458+
Implemented {
459+
trait_ref: TraitRef,
460+
},
461+
ProjectionEq {
462+
projection: ProjectionTerm,
463+
ty: Ty,
464+
},
465+
ConstProjectionEq {
466+
projection: ProjectionTerm,
467+
val: Const,
468+
},
469+
470+
LifetimeOutlives {
471+
a: Lifetime,
472+
b: Lifetime,
473+
},
474+
TypeOutlives {
475+
ty: Ty,
476+
lifetime: Lifetime,
477+
},
462478
}
463479

464480
#[derive(Clone, PartialEq, Eq, Debug)]

‎chalk-parse/src/parser.lalrpop‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -588,6 +588,14 @@ InlineClause: Clause = {
588588
WhereClause: WhereClause = {
589589
<t:TraitRef<":">> => WhereClause::Implemented { trait_ref: t },
590590

591+
<s:Ty> ":" <t:Id> "<" "const" <name:Id> "=" <val: Const> ">" => {
592+
let args = vec![GenericArg::Ty(s)];
593+
let trait_ref = TraitRef { trait_name: t, args: args };
594+
let projection = ProjectionTerm { trait_ref, name, args: vec![] };
595+
596+
WhereClause::ConstProjectionEq { projection, val }
597+
},
598+
591599
// `T: Foo<U = Bar>` -- projection equality
592600
<s:Ty> ":" <t:Id> "<" <a:(<Comma<GenericArg>> ",")?> <name:Id> <a2:Angle<GenericArg>>
593601
"=" <ty:Ty> ">" =>

‎tests/test/projection.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1116,7 +1116,7 @@ fn const_projection() {
11161116
const ID: usize;
11171117
}
11181118
trait OtherTrait {}
1119-
impl OtherTrait for U where U: ConstTrait<ID = 3> {}
1119+
impl OtherTrait for U where U: ConstTrait<const ID = 3> {}
11201120
impl ConstTrait for () {
11211121
const ID: usize = 3;
11221122
}

0 commit comments

Comments
 (0)