Skip to content

Commit bc5391f

Browse files
AzureMarkerAzureMarker
committed
Implement integer type variables
This introduces a new notation to distinguish integer inference variables from general inference variables: ?0i. The "i" represents that it is an integer variable. Another new notation is for integer variables in goals. Similar to consts, integer variables are notated as `int N`, for example: ``` exists<int N> { ... } ```
1 parent e5aaf83 commit bc5391f

File tree

26 files changed

+226
-99
lines changed

26 files changed

+226
-99
lines changed

‎chalk-integration/src/lowering.rs

Lines changed: 15 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ use chalk_ir::cast::{Cast, Caster};
33
use chalk_ir::interner::HasInterner;
44
use chalk_ir::{
55
self, AdtId, AssocTypeId, BoundVar, ClausePriority, DebruijnIndex, FnDefId, ImplId, OpaqueTyId,
6-
QuantifiedWhereClauses, Substitution, ToGenericArg, TraitId,
6+
QuantifiedWhereClauses, Substitution, ToGenericArg, TraitId, TyKind,
77
};
88
use chalk_parse::ast::*;
99
use chalk_solve::rust_ir::{
@@ -90,7 +90,7 @@ impl<'k> Env<'k> {
9090
if let Some(p) = self.parameter_map.get(&name.str) {
9191
let b = p.skip_kind();
9292
return match &p.kind {
93-
chalk_ir::VariableKind::Ty => Ok(chalk_ir::TyData::BoundVar(*b)
93+
chalk_ir::VariableKind::Ty(_) => Ok(chalk_ir::TyData::BoundVar(*b)
9494
.intern(interner)
9595
.cast(interner)),
9696
chalk_ir::VariableKind::Lifetime => Ok(chalk_ir::LifetimeData::BoundVar(*b)
@@ -506,7 +506,7 @@ impl LowerProgram for Program {
506506
let bounds: chalk_ir::Binders<Vec<chalk_ir::Binders<_>>> = env
507507
.in_binders(
508508
Some(chalk_ir::WithKind::new(
509-
chalk_ir::VariableKind::Ty,
509+
chalk_ir::VariableKind::Ty(TyKind::General),
510510
Atom::from(FIXME_SELF),
511511
)),
512512
|env1| {
@@ -681,7 +681,7 @@ impl LowerParameterMap for AssocTyValue {
681681
impl LowerParameterMap for TraitDefn {
682682
fn synthetic_parameters(&self) -> Option<chalk_ir::WithKind<ChalkIr, Ident>> {
683683
Some(chalk_ir::WithKind::new(
684-
chalk_ir::VariableKind::Ty,
684+
chalk_ir::VariableKind::Ty(TyKind::General),
685685
Atom::from(SELF),
686686
))
687687
}
@@ -717,9 +717,14 @@ trait LowerVariableKind {
717717
impl LowerVariableKind for VariableKind {
718718
fn lower(&self) -> chalk_ir::WithKind<ChalkIr, Ident> {
719719
match self {
720-
VariableKind::Ty(n) => {
721-
chalk_ir::WithKind::new(chalk_ir::VariableKind::Ty, n.str.clone())
722-
}
720+
VariableKind::Ty(n) => chalk_ir::WithKind::new(
721+
chalk_ir::VariableKind::Ty(chalk_ir::TyKind::General),
722+
n.str.clone(),
723+
),
724+
VariableKind::IntegerTy(n) => chalk_ir::WithKind::new(
725+
chalk_ir::VariableKind::Ty(chalk_ir::TyKind::Integer),
726+
n.str.clone(),
727+
),
723728
VariableKind::Lifetime(n) => {
724729
chalk_ir::WithKind::new(chalk_ir::VariableKind::Lifetime, n.str.clone())
725730
}
@@ -1290,7 +1295,7 @@ impl LowerTy for Ty {
12901295
bounds: env.in_binders(
12911296
// FIXME: Figure out a proper name for this type parameter
12921297
Some(chalk_ir::WithKind::new(
1293-
chalk_ir::VariableKind::Ty,
1298+
chalk_ir::VariableKind::Ty(TyKind::General),
12941299
Atom::from(FIXME_SELF),
12951300
)),
12961301
|env| {
@@ -1820,6 +1825,7 @@ impl Kinded for VariableKind {
18201825
fn kind(&self) -> Kind {
18211826
match *self {
18221827
VariableKind::Ty(_) => Kind::Ty,
1828+
VariableKind::IntegerTy(_) => Kind::Ty,
18231829
VariableKind::Lifetime(_) => Kind::Lifetime,
18241830
VariableKind::Const(_) => Kind::Const,
18251831
}
@@ -1829,7 +1835,7 @@ impl Kinded for VariableKind {
18291835
impl Kinded for chalk_ir::VariableKind<ChalkIr> {
18301836
fn kind(&self) -> Kind {
18311837
match self {
1832-
chalk_ir::VariableKind::Ty => Kind::Ty,
1838+
chalk_ir::VariableKind::Ty(_) => Kind::Ty,
18331839
chalk_ir::VariableKind::Lifetime => Kind::Lifetime,
18341840
chalk_ir::VariableKind::Const(_) => Kind::Const,
18351841
}

‎chalk-ir/src/debug.rs

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -179,7 +179,8 @@ impl<I: Interner> Debug for TyData<I> {
179179
match self {
180180
TyData::BoundVar(db) => write!(fmt, "{:?}", db),
181181
TyData::Dyn(clauses) => write!(fmt, "{:?}", clauses),
182-
TyData::InferenceVar(var) => write!(fmt, "{:?}", var),
182+
TyData::InferenceVar(var, TyKind::General) => write!(fmt, "{:?}", var),
183+
TyData::InferenceVar(var, TyKind::Integer) => write!(fmt, "{:?}i", var),
183184
TyData::Apply(apply) => write!(fmt, "{:?}", apply),
184185
TyData::Alias(alias) => write!(fmt, "{:?}", alias),
185186
TyData::Placeholder(index) => write!(fmt, "{:?}", index),
@@ -276,7 +277,8 @@ impl<'a, I: Interner> Debug for VariableKindsInnerDebug<'a, I> {
276277
write!(fmt, ", ")?;
277278
}
278279
match binder {
279-
VariableKind::Ty => write!(fmt, "type")?,
280+
VariableKind::Ty(TyKind::General) => write!(fmt, "type")?,
281+
VariableKind::Ty(TyKind::Integer) => write!(fmt, "integer type")?,
280282
VariableKind::Lifetime => write!(fmt, "lifetime")?,
281283
VariableKind::Const(ty) => write!(fmt, "const: {:?}", ty)?,
282284
}
@@ -765,7 +767,8 @@ impl<I: Interner> Debug for GenericArgData<I> {
765767
impl<I: Interner> Debug for VariableKind<I> {
766768
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
767769
match self {
768-
VariableKind::Ty => write!(fmt, "type"),
770+
VariableKind::Ty(TyKind::General) => write!(fmt, "type"),
771+
VariableKind::Ty(TyKind::Integer) => write!(fmt, "integer type"),
769772
VariableKind::Lifetime => write!(fmt, "lifetime"),
770773
VariableKind::Const(ty) => write!(fmt, "const: {:?}", ty),
771774
}
@@ -776,7 +779,8 @@ impl<I: Interner, T: Debug> Debug for WithKind<I, T> {
776779
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
777780
let value = self.skip_kind();
778781
match &self.kind {
779-
VariableKind::Ty => write!(fmt, "{:?} with kind type", value),
782+
VariableKind::Ty(TyKind::General) => write!(fmt, "{:?} with kind type", value),
783+
VariableKind::Ty(TyKind::Integer) => write!(fmt, "{:?} with kind integer type", value),
780784
VariableKind::Lifetime => write!(fmt, "{:?} with kind lifetime", value),
781785
VariableKind::Const(ty) => write!(fmt, "{:?} with kind {:?}", value, ty),
782786
}

‎chalk-ir/src/fold.rs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -267,12 +267,13 @@ where
267267
fn fold_inference_ty(
268268
&mut self,
269269
var: InferenceVar,
270+
kind: TyKind,
270271
outer_binder: DebruijnIndex,
271272
) -> Fallible<Ty<TI>> {
272273
if self.forbid_inference_vars() {
273274
panic!("unexpected inference type `{:?}`", var)
274275
} else {
275-
Ok(var.to_ty(self.target_interner()))
276+
Ok(var.to_ty(self.target_interner(), kind))
276277
}
277278
}
278279

@@ -416,7 +417,7 @@ where
416417
}
417418
TyData::Dyn(clauses) => Ok(TyData::Dyn(clauses.fold_with(folder, outer_binder)?)
418419
.intern(folder.target_interner())),
419-
TyData::InferenceVar(var) => folder.fold_inference_ty(*var, outer_binder),
420+
TyData::InferenceVar(var, kind) => folder.fold_inference_ty(*var, *kind, outer_binder),
420421
TyData::Apply(apply) => Ok(TyData::Apply(apply.fold_with(folder, outer_binder)?)
421422
.intern(folder.target_interner())),
422423
TyData::Placeholder(ui) => Ok(folder.fold_free_placeholder_ty(*ui, outer_binder)?),

‎chalk-ir/src/lib.rs

Lines changed: 40 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -320,7 +320,7 @@ impl<I: Interner> Ty<I> {
320320

321321
/// If this is a `TyData::InferenceVar(d)`, returns `Some(d)` else `None`.
322322
pub fn inference_var(&self, interner: &I) -> Option<InferenceVar> {
323-
if let TyData::InferenceVar(depth) = self.data(interner) {
323+
if let TyData::InferenceVar(depth, _) = self.data(interner) {
324324
Some(*depth)
325325
} else {
326326
None
@@ -330,7 +330,7 @@ impl<I: Interner> Ty<I> {
330330
/// Returns true if this is a `BoundVar` or `InferenceVar`.
331331
pub fn is_var(&self, interner: &I) -> bool {
332332
match self.data(interner) {
333-
TyData::BoundVar(_) | TyData::InferenceVar(_) => true,
333+
TyData::BoundVar(_) | TyData::InferenceVar(_, _) => true,
334334
_ => false,
335335
}
336336
}
@@ -342,6 +342,21 @@ impl<I: Interner> Ty<I> {
342342
}
343343
}
344344

345+
/// Returns true if this is an `IntTy` or `UintTy`
346+
pub fn is_integer(&self, interner: &I) -> bool {
347+
match self.data(interner) {
348+
TyData::Apply(ApplicationTy {
349+
name: TypeName::Scalar(Scalar::Int(_)),
350+
..
351+
})
352+
| TyData::Apply(ApplicationTy {
353+
name: TypeName::Scalar(Scalar::Uint(_)),
354+
..
355+
}) => true,
356+
_ => false,
357+
}
358+
}
359+
345360
/// True if this type contains "bound" types/lifetimes, and hence
346361
/// needs to be shifted across binders. This is a very inefficient
347362
/// check, intended only for debug assertions, because I am lazy.
@@ -390,7 +405,7 @@ pub enum TyData<I: Interner> {
390405
BoundVar(BoundVar),
391406

392407
/// Inference variable defined in the current inference context.
393-
InferenceVar(InferenceVar),
408+
InferenceVar(InferenceVar, TyKind),
394409
}
395410

396411
impl<I: Interner> TyData<I> {
@@ -682,8 +697,8 @@ impl InferenceVar {
682697
self.index
683698
}
684699

685-
pub fn to_ty<I: Interner>(self, interner: &I) -> Ty<I> {
686-
TyData::<I>::InferenceVar(self).intern(interner)
700+
pub fn to_ty<I: Interner>(self, interner: &I, kind: TyKind) -> Ty<I> {
701+
TyData::<I>::InferenceVar(self, kind).intern(interner)
687702
}
688703

689704
pub fn to_lifetime<I: Interner>(self, interner: &I) -> Lifetime<I> {
@@ -910,17 +925,33 @@ impl<I: Interner> ApplicationTy<I> {
910925
}
911926
}
912927

928+
/// Represents some extra knowledge we may have about the variable.
929+
/// ```ignore
930+
/// let x: &[u32];
931+
/// let i = 1;
932+
/// x[i]
933+
/// ```
934+
/// In this example, `i` is known to be some type of integer. We can infer that
935+
/// it is `usize` because that is the only integer type that slices have an
936+
/// `Index` impl for. `i` would have a `TyKind` of `Integer` to guide the
937+
/// inference process.
938+
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
939+
pub enum TyKind {
940+
General,
941+
Integer,
942+
}
943+
913944
#[derive(Clone, PartialEq, Eq, Hash)]
914945
pub enum VariableKind<I: Interner> {
915-
Ty,
946+
Ty(TyKind),
916947
Lifetime,
917948
Const(Ty<I>),
918949
}
919950

920951
impl<I: Interner> VariableKind<I> {
921952
fn to_bound_variable(&self, interner: &I, bound_var: BoundVar) -> GenericArg<I> {
922953
match self {
923-
VariableKind::Ty => {
954+
VariableKind::Ty(_) => {
924955
GenericArgData::Ty(TyData::BoundVar(bound_var).intern(interner)).intern(interner)
925956
}
926957
VariableKind::Lifetime => {
@@ -1524,7 +1555,7 @@ impl<T: HasInterner> Binders<T> {
15241555
// The new variable is at the front and everything afterwards is shifted up by 1
15251556
let new_var = TyData::BoundVar(BoundVar::new(DebruijnIndex::INNERMOST, 0)).intern(interner);
15261557
let value = op(new_var);
1527-
let binders = VariableKinds::from(interner, iter::once(VariableKind::Ty));
1558+
let binders = VariableKinds::from(interner, iter::once(VariableKind::Ty(TyKind::General)));
15281559
Binders { binders, value }
15291560
}
15301561

@@ -1940,7 +1971,7 @@ impl<T: HasInterner> UCanonical<T> {
19401971
.map(|(index, pk)| {
19411972
let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, index);
19421973
match &pk.kind {
1943-
VariableKind::Ty => {
1974+
VariableKind::Ty(_) => {
19441975
GenericArgData::Ty(TyData::BoundVar(bound_var).intern(interner))
19451976
.intern(interner)
19461977
}

‎chalk-ir/src/visit.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -273,7 +273,7 @@ where
273273
}
274274
}
275275
TyData::Dyn(clauses) => clauses.visit_with(visitor, outer_binder),
276-
TyData::InferenceVar(var) => visitor.visit_inference_var(*var, outer_binder),
276+
TyData::InferenceVar(var, _) => visitor.visit_inference_var(*var, outer_binder),
277277
TyData::Apply(apply) => apply.visit_with(visitor, outer_binder),
278278
TyData::Placeholder(ui) => visitor.visit_free_placeholder(*ui, outer_binder),
279279
TyData::Alias(proj) => proj.visit_with(visitor, outer_binder),

‎chalk-ir/src/zip.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -308,14 +308,14 @@ impl<I: Interner> Zip<I> for VariableKind<I> {
308308
I: 'i,
309309
{
310310
match (a, b) {
311-
(VariableKind::Ty, VariableKind::Ty) => Ok(()),
311+
(VariableKind::Ty(a), VariableKind::Ty(b)) if a == b => Ok(()),
312312
(VariableKind::Lifetime, VariableKind::Lifetime) => Ok(()),
313313
(VariableKind::Const(ty_a), VariableKind::Const(ty_b)) => {
314314
Zip::zip_with(zipper, ty_a, ty_b)
315315
}
316-
(VariableKind::Ty, _) | (VariableKind::Lifetime, _) | (VariableKind::Const(_), _) => {
317-
panic!("zipping things of mixed kind")
318-
}
316+
(VariableKind::Ty(_), _)
317+
| (VariableKind::Lifetime, _)
318+
| (VariableKind::Const(_), _) => panic!("zipping things of mixed kind"),
319319
}
320320
}
321321
}

‎chalk-parse/src/ast.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,7 @@ pub struct OpaqueTyDefn {
100100
#[derive(Clone, PartialEq, Eq, Debug)]
101101
pub enum VariableKind {
102102
Ty(Identifier),
103+
IntegerTy(Identifier),
103104
Lifetime(Identifier),
104105
Const(Identifier),
105106
}

‎chalk-parse/src/parser.lalrpop

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -201,6 +201,7 @@ VariableKind: VariableKind = {
201201
Id => VariableKind::Ty(<>),
202202
LifetimeId => VariableKind::Lifetime(<>),
203203
"const" <id:Id> => VariableKind::Const(id),
204+
"int" <id:Id> => VariableKind::IntegerTy(id),
204205
};
205206

206207
AssocTyValue: AssocTyValue = {

‎chalk-solve/src/clauses.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,7 @@ fn program_clauses_that_could_match<I: Interner>(
260260
}
261261
_ => {}
262262
},
263-
TyData::InferenceVar(_) | TyData::BoundVar(_) => {
263+
TyData::InferenceVar(_, _) | TyData::BoundVar(_) => {
264264
return Err(Floundered);
265265
}
266266
_ => {}
@@ -459,7 +459,7 @@ fn match_ty<I: Interner>(
459459
.map(|ty| match_ty(builder, environment, &ty))
460460
.collect::<Result<_, Floundered>>()?;
461461
}
462-
TyData::BoundVar(_) | TyData::InferenceVar(_) => return Err(Floundered),
462+
TyData::BoundVar(_) | TyData::InferenceVar(_, _) => return Err(Floundered),
463463
TyData::Dyn(_) => {}
464464
})
465465
}

‎chalk-solve/src/clauses/builder.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ impl<'me, I: Interner> ClauseBuilder<'me, I> {
149149
pub fn push_bound_ty(&mut self, op: impl FnOnce(&mut Self, Ty<I>)) {
150150
let interner = self.interner();
151151
let binders = Binders::new(
152-
VariableKinds::from(interner, iter::once(VariableKind::Ty)),
152+
VariableKinds::from(interner, iter::once(VariableKind::Ty(TyKind::General))),
153153
PhantomData::<I>,
154154
);
155155
self.push_binders(&binders, |this, PhantomData| {

0 commit comments

Comments
 (0)