Skip to content

Commit c0daff5

Browse files
basil-cowbasil-cow
committed
const implementation mvp
1 parent 944c643 commit c0daff5

31 files changed

+1021
-213
lines changed

‎chalk-integration/src/error.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,7 @@ impl std::error::Error for ChalkError {}
5656
pub enum RustIrError {
5757
InvalidTypeName(Identifier),
5858
InvalidLifetimeName(Identifier),
59+
InvalidConstName(Identifier),
5960
NotTrait(Identifier),
6061
NotStruct(Identifier),
6162
DuplicateOrShadowedParameters,
@@ -98,6 +99,7 @@ impl std::fmt::Display for RustIrError {
9899
match self {
99100
RustIrError::InvalidTypeName(name) => write!(f, "invalid type name `{}`", name),
100101
RustIrError::InvalidLifetimeName(name) => write!(f, "invalid lifetime name `{}`", name),
102+
RustIrError::InvalidConstName(name) => write!(f, "invalid const name `{}`", name),
101103
RustIrError::NotTrait(name) => write!(
102104
f,
103105
"expected a trait, found `{}`, which is not a trait",

‎chalk-integration/src/lowering.rs

Lines changed: 47 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,10 @@ enum LifetimeLookup {
7878
Parameter(BoundVar),
7979
}
8080

81+
enum ConstLookup {
82+
Parameter(BoundVar),
83+
}
84+
8185
const SELF: &str = "Self";
8286
const FIXME_SELF: &str = "__FIXME_SELF__";
8387

@@ -134,6 +138,17 @@ impl<'k> Env<'k> {
134138
Err(RustIrError::InvalidLifetimeName(name))
135139
}
136140

141+
fn lookup_const(&self, name: Identifier) -> LowerResult<ConstLookup> {
142+
if let Some(k) = self
143+
.parameter_map
144+
.get(&chalk_ir::ParameterKind::Const(name.str))
145+
{
146+
return Ok(ConstLookup::Parameter(*k));
147+
}
148+
149+
Err(RustIrError::InvalidConstName(name))
150+
}
151+
137152
fn struct_kind(&self, id: chalk_ir::StructId<ChalkIr>) -> &TypeKind {
138153
&self.struct_kinds[&id]
139154
}
@@ -583,6 +598,7 @@ impl LowerParameterKind for ParameterKind {
583598
match *self {
584599
ParameterKind::Ty(ref n) => chalk_ir::ParameterKind::Ty(n.str),
585600
ParameterKind::Lifetime(ref n) => chalk_ir::ParameterKind::Lifetime(n.str),
601+
ParameterKind::Const(ref n) => chalk_ir::ParameterKind::Const(n.str),
586602
}
587603
}
588604
}
@@ -781,6 +797,11 @@ impl LowerLeafGoal for LeafGoal {
781797
b: b.lower(env)?.cast(interner),
782798
}
783799
.cast::<chalk_ir::Goal<ChalkIr>>(interner),
800+
LeafGoal::UnifyConsts { ref a, ref b } => chalk_ir::EqGoal {
801+
a: a.lower(env)?.cast(interner),
802+
b: b.lower(env)?.cast(interner),
803+
}
804+
.cast::<chalk_ir::Goal<ChalkIr>>(interner),
784805
})
785806
}
786807
}
@@ -1216,6 +1237,28 @@ impl LowerParameter for Parameter {
12161237
match *self {
12171238
Parameter::Ty(ref t) => Ok(t.lower(env)?.cast(interner)),
12181239
Parameter::Lifetime(ref l) => Ok(l.lower(env)?.cast(interner)),
1240+
Parameter::Const(ref c) => Ok(c.lower(env)?.cast(interner)),
1241+
}
1242+
}
1243+
}
1244+
1245+
trait LowerConst {
1246+
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::Const<ChalkIr>>;
1247+
}
1248+
1249+
impl LowerConst for Const {
1250+
fn lower(&self, env: &Env) -> LowerResult<chalk_ir::Const<ChalkIr>> {
1251+
let interner = env.interner();
1252+
match *self {
1253+
Const::Id { name } => match env.lookup_const(name)? {
1254+
ConstLookup::Parameter(d) => Ok(chalk_ir::ConstData::BoundVar(d).intern(interner)),
1255+
},
1256+
Const::Value { value } => {
1257+
Ok(
1258+
chalk_ir::ConstData::Concrete(chalk_ir::ConcreteConst { interned: value })
1259+
.intern(interner),
1260+
)
1261+
}
12191262
}
12201263
}
12211264
}
@@ -1527,6 +1570,7 @@ impl Kinded for ParameterKind {
15271570
match *self {
15281571
ParameterKind::Ty(_) => Kind::Ty,
15291572
ParameterKind::Lifetime(_) => Kind::Lifetime,
1573+
ParameterKind::Const(_) => Kind::Const,
15301574
}
15311575
}
15321576
}
@@ -1536,15 +1580,17 @@ impl Kinded for Parameter {
15361580
match *self {
15371581
Parameter::Ty(_) => Kind::Ty,
15381582
Parameter::Lifetime(_) => Kind::Lifetime,
1583+
Parameter::Const(_) => Kind::Const,
15391584
}
15401585
}
15411586
}
15421587

1543-
impl<T, L> Kinded for chalk_ir::ParameterKind<T, L> {
1588+
impl<T, L, C> Kinded for chalk_ir::ParameterKind<T, L, C> {
15441589
fn kind(&self) -> Kind {
15451590
match *self {
15461591
chalk_ir::ParameterKind::Ty(_) => Kind::Ty,
15471592
chalk_ir::ParameterKind::Lifetime(_) => Kind::Lifetime,
1593+
chalk_ir::ParameterKind::Const(_) => Kind::Const,
15481594
}
15491595
}
15501596
}

‎chalk-ir/src/cast.rs

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,7 @@ macro_rules! reflexive_impl {
7676

7777
reflexive_impl!(for(I: Interner) TyData<I>);
7878
reflexive_impl!(for(I: Interner) LifetimeData<I>);
79+
reflexive_impl!(for(I: Interner) ConstData<I>);
7980
reflexive_impl!(for(I: Interner) TraitRef<I>);
8081
reflexive_impl!(for(I: Interner) DomainGoal<I>);
8182
reflexive_impl!(for(I: Interner) Goal<I>);
@@ -174,6 +175,12 @@ impl<I: Interner> CastTo<Parameter<I>> for Lifetime<I> {
174175
}
175176
}
176177

178+
impl<I: Interner> CastTo<Parameter<I>> for Const<I> {
179+
fn cast_to(self, interner: &I) -> Parameter<I> {
180+
Parameter::new(interner, ParameterKind::Const(self))
181+
}
182+
}
183+
177184
impl<I: Interner> CastTo<Parameter<I>> for Parameter<I> {
178185
fn cast_to(self, _interner: &I) -> Parameter<I> {
179186
self

‎chalk-ir/src/could_match.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,10 @@ where
4848
Ok(())
4949
}
5050

51+
fn zip_consts(&mut self, _: &Const<I>, _: &Const<I>) -> Fallible<()> {
52+
Ok(())
53+
}
54+
5155
fn zip_binders<T>(&mut self, a: &Binders<T>, b: &Binders<T>) -> Fallible<()>
5256
where
5357
T: HasInterner + Zip<I>,

‎chalk-ir/src/debug.rs

Lines changed: 27 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,18 @@ impl<I: Interner> Debug for Lifetime<I> {
3333
}
3434
}
3535

36+
impl<I: Interner> Debug for Const<I> {
37+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
38+
I::debug_const(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
39+
}
40+
}
41+
42+
impl<I: Interner> Debug for ConcreteConst<I> {
43+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
44+
write!(fmt, "{:?}", self.interned)
45+
}
46+
}
47+
3648
impl<I: Interner> Debug for Parameter<I> {
3749
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
3850
I::debug_parameter(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
@@ -253,12 +265,24 @@ impl<'a, I: Interner> Debug for ParameterKindsInnerDebug<'a, I> {
253265
match *binder {
254266
ParameterKind::Ty(()) => write!(fmt, "type")?,
255267
ParameterKind::Lifetime(()) => write!(fmt, "lifetime")?,
268+
ParameterKind::Const(()) => write!(fmt, "const")?,
256269
}
257270
}
258271
write!(fmt, ">")
259272
}
260273
}
261274

275+
impl<I: Interner> Debug for ConstData<I> {
276+
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
277+
match self {
278+
ConstData::BoundVar(db) => write!(fmt, "{:?}", db),
279+
ConstData::InferenceVar(var) => write!(fmt, "{:?}", var),
280+
ConstData::Placeholder(index) => write!(fmt, "{:?}", index),
281+
ConstData::Concrete(evaluated) => write!(fmt, "{:?}", evaluated),
282+
}
283+
}
284+
}
285+
262286
impl<I: Interner> Debug for GoalData<I> {
263287
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
264288
match self {
@@ -314,6 +338,7 @@ impl<'a, I: Interner> Debug for ParameterDataInnerDebug<'a, I> {
314338
match self.0 {
315339
ParameterKind::Ty(n) => write!(fmt, "{:?}", n),
316340
ParameterKind::Lifetime(n) => write!(fmt, "{:?}", n),
341+
ParameterKind::Const(n) => write!(fmt, "{:?}", n),
317342
}
318343
}
319344
}
@@ -713,11 +738,12 @@ impl<'a, T: HasInterner + Display> Display for CanonicalDisplay<'a, T> {
713738
}
714739
}
715740

716-
impl<T: Debug, L: Debug> Debug for ParameterKind<T, L> {
741+
impl<T: Debug, L: Debug, C: Debug> Debug for ParameterKind<T, L, C> {
717742
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
718743
match *self {
719744
ParameterKind::Ty(ref n) => write!(fmt, "Ty({:?})", n),
720745
ParameterKind::Lifetime(ref n) => write!(fmt, "Lifetime({:?})", n),
746+
ParameterKind::Const(ref n) => write!(fmt, "Const({:?})", n),
721747
}
722748
}
723749
}

‎chalk-ir/src/fold.rs

Lines changed: 111 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -87,7 +87,7 @@ where
8787
/// Top-level callback: invoked for each `Lifetime<I>` that is
8888
/// encountered when folding. By default, invokes
8989
/// `super_fold_with`, which will in turn invoke the more
90-
/// specialized folding methods below, like `fold_free_lifetime_ty`.
90+
/// specialized folding methods below, like `fold_free_var_lifetime`.
9191
fn fold_lifetime(
9292
&mut self,
9393
lifetime: &Lifetime<I>,
@@ -96,6 +96,18 @@ where
9696
lifetime.super_fold_with(self.as_dyn(), outer_binder)
9797
}
9898

99+
/// Top-level callback: invoked for each `Const<I>` that is
100+
/// encountered when folding. By default, invokes
101+
/// `super_fold_with`, which will in turn invoke the more
102+
/// specialized folding methods below, like `fold_free_var_const`.
103+
fn fold_const(
104+
&mut self,
105+
constant: &Const<I>,
106+
outer_binder: DebruijnIndex,
107+
) -> Fallible<Const<TI>> {
108+
constant.super_fold_with(self.as_dyn(), outer_binder)
109+
}
110+
99111
/// Invoked for every program clause. By default, recursively folds the goals contents.
100112
fn fold_program_clause(
101113
&mut self,
@@ -159,8 +171,24 @@ where
159171
}
160172
}
161173

162-
/// If overriden to return true, we will panic when a free
163-
/// placeholder type/lifetime is encountered.
174+
fn fold_free_var_const(
175+
&mut self,
176+
bound_var: BoundVar,
177+
outer_binder: DebruijnIndex,
178+
) -> Fallible<Const<TI>> {
179+
if self.forbid_free_vars() {
180+
panic!(
181+
"unexpected free variable with depth `{:?}` with outer binder {:?}",
182+
bound_var, outer_binder
183+
)
184+
} else {
185+
let bound_var = bound_var.shifted_in_from(outer_binder);
186+
Ok(ConstData::<TI>::BoundVar(bound_var).intern(self.target_interner()))
187+
}
188+
}
189+
190+
/// If overridden to return true, we will panic when a free
191+
/// placeholder type/lifetime/const is encountered.
164192
fn forbid_free_placeholders(&self) -> bool {
165193
false
166194
}
@@ -199,6 +227,19 @@ where
199227
}
200228
}
201229

230+
#[allow(unused_variables)]
231+
fn fold_free_placeholder_const(
232+
&mut self,
233+
universe: PlaceholderIndex,
234+
outer_binder: DebruijnIndex,
235+
) -> Fallible<Const<TI>> {
236+
if self.forbid_free_placeholders() {
237+
panic!("unexpected placeholder const `{:?}`", universe)
238+
} else {
239+
Ok(universe.to_const(self.target_interner()))
240+
}
241+
}
242+
202243
/// If overridden to return true, inference variables will trigger
203244
/// panics when folded. Used when inference variables are
204245
/// unexpected.
@@ -240,6 +281,19 @@ where
240281
}
241282
}
242283

284+
#[allow(unused_variables)]
285+
fn fold_inference_const(
286+
&mut self,
287+
var: InferenceVar,
288+
outer_binder: DebruijnIndex,
289+
) -> Fallible<Const<TI>> {
290+
if self.forbid_inference_vars() {
291+
panic!("unexpected inference const `{:?}`", var)
292+
} else {
293+
Ok(var.to_const(self.target_interner()))
294+
}
295+
}
296+
243297
fn interner(&self) -> &'i I;
244298

245299
fn target_interner(&self) -> &'i TI;
@@ -419,6 +473,60 @@ where
419473
}
420474
}
421475

476+
/// "Folding" a const invokes the `fold_const` method on the folder; this
477+
/// usually (in turn) invokes `super_fold_const` to fold the individual
478+
/// parts.
479+
impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Const<I> {
480+
type Result = Const<TI>;
481+
482+
fn fold_with<'i>(
483+
&self,
484+
folder: &mut dyn Folder<'i, I, TI>,
485+
outer_binder: DebruijnIndex,
486+
) -> Fallible<Self::Result>
487+
where
488+
I: 'i,
489+
TI: 'i,
490+
{
491+
folder.fold_const(self, outer_binder)
492+
}
493+
}
494+
495+
impl<I, TI> SuperFold<I, TI> for Const<I>
496+
where
497+
I: Interner,
498+
TI: TargetInterner<I>,
499+
{
500+
fn super_fold_with<'i>(
501+
&self,
502+
folder: &mut dyn Folder<'i, I, TI>,
503+
outer_binder: DebruijnIndex,
504+
) -> Fallible<Const<TI>>
505+
where
506+
I: 'i,
507+
TI: 'i,
508+
{
509+
let interner = folder.interner();
510+
match self.data(interner) {
511+
ConstData::BoundVar(bound_var) => {
512+
if let Some(bound_var1) = bound_var.shifted_out_to(outer_binder) {
513+
folder.fold_free_var_const(bound_var1, outer_binder)
514+
} else {
515+
Ok(ConstData::<TI>::BoundVar(*bound_var).intern(folder.target_interner()))
516+
}
517+
}
518+
ConstData::InferenceVar(var) => folder.fold_inference_const(*var, outer_binder),
519+
ConstData::Placeholder(universe) => {
520+
folder.fold_free_placeholder_const(*universe, outer_binder)
521+
}
522+
ConstData::Concrete(ev) => Ok(ConstData::Concrete(ConcreteConst {
523+
interned: folder.target_interner().transfer_const(&ev.interned),
524+
})
525+
.intern(folder.target_interner())),
526+
}
527+
}
528+
}
529+
422530
/// Folding a goal invokes the `fold_goal` callback (which will, by
423531
/// default, invoke super-fold).
424532
impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goal<I> {

‎chalk-ir/src/fold/boring_impls.rs

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -331,12 +331,13 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for PhantomData<I> {
331331
}
332332
}
333333

334-
impl<I: Interner, TI: TargetInterner<I>, T, L> Fold<I, TI> for ParameterKind<T, L>
334+
impl<I: Interner, TI: TargetInterner<I>, T, L, C> Fold<I, TI> for ParameterKind<T, L, C>
335335
where
336336
T: Fold<I, TI>,
337337
L: Fold<I, TI>,
338+
C: Fold<I, TI>,
338339
{
339-
type Result = ParameterKind<T::Result, L::Result>;
340+
type Result = ParameterKind<T::Result, L::Result, C::Result>;
340341

341342
fn fold_with<'i>(
342343
&self,
@@ -352,6 +353,7 @@ where
352353
ParameterKind::Lifetime(a) => {
353354
Ok(ParameterKind::Lifetime(a.fold_with(folder, outer_binder)?))
354355
}
356+
ParameterKind::Const(a) => Ok(ParameterKind::Const(a.fold_with(folder, outer_binder)?)),
355357
}
356358
}
357359
}

0 commit comments

Comments
 (0)