Skip to content

Commit f4977ab

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #470 from Mcat12/feature/integer-float-kinds
Integer and float variable kinds
2 parents a9e2e0b + d6c5b78 commit f4977ab

27 files changed

+405
-89
lines changed

‎book/src/engine/logic.md

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ As either `Answer`s are found for the selected `Table`, entries on the stack are
3434

3535
As mentioned before, whenever a new `Goal` is encounted, a new [`Table`] is
3636
created to store current and future answers. First, the [`Goal`] is converted into
37-
an [`HhGoal`]. If it can be simplified, then a `Strand` with one or more
37+
an `HhGoal`. If it can be simplified, then a `Strand` with one or more
3838
subgoals will be generated and can be followed as above. Otherwise, if it is a
3939
`DomainGoal` (see above), then
4040
[`program_clauses`](https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html#tymethod.program_clauses)
@@ -123,7 +123,6 @@ For much more in-depth
123123

124124
[`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html
125125
[`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html
126-
[`HhGoal`]: https://rust-lang.github.io/chalk/chalk_engine/hh/enum.HhGoal.html
127126
[`Stack`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.Stack.html
128127
[`StackEntry`]: https://rust-lang.github.io/chalk/chalk_engine/stack/struct.StackEntry.html
129128
[`Table`]: https://rust-lang.github.io/chalk/chalk_engine/table/struct.Table.html

‎book/src/engine/major_concepts.md

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,7 @@ opaque to the engine internals. Functions in the trait are agnostic to specific
1616
program or environment details, since they lack a `&self` argument.
1717

1818
To give an example, there is an associated [`Goal`] type. However, Chalk doesn't
19-
know how to solve this. Instead, it has to be converted an [`HhGoal`] via the
19+
know how to solve this. Instead, it has to be converted an `HhGoal` via the
2020
`Context::into_hh_goal` function. This will be coverted more in the `Goals`
2121
section.
2222

@@ -38,7 +38,7 @@ change the state of the logic itself.
3838
## Goals
3939

4040
A "goal" in Chalk can be thought of as "something we want to prove". The engine
41-
itself understands [`HhGoal`]s. `HHGoal`s consist of the most basic logic,
41+
itself understands `HhGoal`s. `HHGoal`s consist of the most basic logic,
4242
such as introducing Binders (`Forall` or `Exists`) or combining goals (`All`).
4343
On the other hand, `Context::Goal` represents an opaque goal generated
4444
externally. As such, it may contain any extra information or may be interned.
@@ -111,7 +111,6 @@ stack).
111111
[`Context`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html
112112
[`ContextOps`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.ContextOps.html
113113
[`InferenceTable`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.InferenceTable.html
114-
[`HhGoal`]: https://rust-lang.github.io/chalk/chalk_engine/hh/enum.HhGoal.html
115114
[`Solution`]: https://rust-lang.github.io/chalk/chalk_engine/context/trait.Context.html#associatedtype.Solution
116115
[`ExClause`]: https://rust-lang.github.io/chalk/chalk_engine/struct.ExClause.html
117116
[`Strand`]: https://rust-lang.github.io/chalk/chalk_engine/strand/struct.Strand.html

‎chalk-integration/src/lowering.rs

Lines changed: 20 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,18 @@ 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+
),
728+
VariableKind::FloatTy(n) => chalk_ir::WithKind::new(
729+
chalk_ir::VariableKind::Ty(chalk_ir::TyKind::Float),
730+
n.str.clone(),
731+
),
723732
VariableKind::Lifetime(n) => {
724733
chalk_ir::WithKind::new(chalk_ir::VariableKind::Lifetime, n.str.clone())
725734
}
@@ -1290,7 +1299,7 @@ impl LowerTy for Ty {
12901299
bounds: env.in_binders(
12911300
// FIXME: Figure out a proper name for this type parameter
12921301
Some(chalk_ir::WithKind::new(
1293-
chalk_ir::VariableKind::Ty,
1302+
chalk_ir::VariableKind::Ty(TyKind::General),
12941303
Atom::from(FIXME_SELF),
12951304
)),
12961305
|env| {
@@ -1820,6 +1829,8 @@ impl Kinded for VariableKind {
18201829
fn kind(&self) -> Kind {
18211830
match *self {
18221831
VariableKind::Ty(_) => Kind::Ty,
1832+
VariableKind::IntegerTy(_) => Kind::Ty,
1833+
VariableKind::FloatTy(_) => Kind::Ty,
18231834
VariableKind::Lifetime(_) => Kind::Lifetime,
18241835
VariableKind::Const(_) => Kind::Const,
18251836
}
@@ -1829,7 +1840,7 @@ impl Kinded for VariableKind {
18291840
impl Kinded for chalk_ir::VariableKind<ChalkIr> {
18301841
fn kind(&self) -> Kind {
18311842
match self {
1832-
chalk_ir::VariableKind::Ty => Kind::Ty,
1843+
chalk_ir::VariableKind::Ty(_) => Kind::Ty,
18331844
chalk_ir::VariableKind::Lifetime => Kind::Lifetime,
18341845
chalk_ir::VariableKind::Const(_) => Kind::Const,
18351846
}

‎chalk-ir/src/debug.rs

Lines changed: 12 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -179,7 +179,9 @@ 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),
184+
TyData::InferenceVar(var, TyKind::Float) => write!(fmt, "{:?}f", var),
183185
TyData::Apply(apply) => write!(fmt, "{:?}", apply),
184186
TyData::Alias(alias) => write!(fmt, "{:?}", alias),
185187
TyData::Placeholder(index) => write!(fmt, "{:?}", index),
@@ -276,7 +278,9 @@ impl<'a, I: Interner> Debug for VariableKindsInnerDebug<'a, I> {
276278
write!(fmt, ", ")?;
277279
}
278280
match binder {
279-
VariableKind::Ty => write!(fmt, "type")?,
281+
VariableKind::Ty(TyKind::General) => write!(fmt, "type")?,
282+
VariableKind::Ty(TyKind::Integer) => write!(fmt, "integer type")?,
283+
VariableKind::Ty(TyKind::Float) => write!(fmt, "float type")?,
280284
VariableKind::Lifetime => write!(fmt, "lifetime")?,
281285
VariableKind::Const(ty) => write!(fmt, "const: {:?}", ty)?,
282286
}
@@ -765,7 +769,9 @@ impl<I: Interner> Debug for GenericArgData<I> {
765769
impl<I: Interner> Debug for VariableKind<I> {
766770
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
767771
match self {
768-
VariableKind::Ty => write!(fmt, "type"),
772+
VariableKind::Ty(TyKind::General) => write!(fmt, "type"),
773+
VariableKind::Ty(TyKind::Integer) => write!(fmt, "integer type"),
774+
VariableKind::Ty(TyKind::Float) => write!(fmt, "float type"),
769775
VariableKind::Lifetime => write!(fmt, "lifetime"),
770776
VariableKind::Const(ty) => write!(fmt, "const: {:?}", ty),
771777
}
@@ -776,7 +782,9 @@ impl<I: Interner, T: Debug> Debug for WithKind<I, T> {
776782
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
777783
let value = self.skip_kind();
778784
match &self.kind {
779-
VariableKind::Ty => write!(fmt, "{:?} with kind type", value),
785+
VariableKind::Ty(TyKind::General) => write!(fmt, "{:?} with kind type", value),
786+
VariableKind::Ty(TyKind::Integer) => write!(fmt, "{:?} with kind integer type", value),
787+
VariableKind::Ty(TyKind::Float) => write!(fmt, "{:?} with kind float type", value),
780788
VariableKind::Lifetime => write!(fmt, "{:?} with kind lifetime", value),
781789
VariableKind::Const(ty) => write!(fmt, "{:?} with kind {:?}", value, ty),
782790
}

‎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: 52 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,32 @@ 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+
360+
/// Returns true if this is a `FloatTy`
361+
pub fn is_float(&self, interner: &I) -> bool {
362+
match self.data(interner) {
363+
TyData::Apply(ApplicationTy {
364+
name: TypeName::Scalar(Scalar::Float(_)),
365+
..
366+
}) => true,
367+
_ => false,
368+
}
369+
}
370+
345371
/// True if this type contains "bound" types/lifetimes, and hence
346372
/// needs to be shifted across binders. This is a very inefficient
347373
/// check, intended only for debug assertions, because I am lazy.
@@ -390,7 +416,7 @@ pub enum TyData<I: Interner> {
390416
BoundVar(BoundVar),
391417

392418
/// Inference variable defined in the current inference context.
393-
InferenceVar(InferenceVar),
419+
InferenceVar(InferenceVar, TyKind),
394420
}
395421

396422
impl<I: Interner> TyData<I> {
@@ -682,8 +708,8 @@ impl InferenceVar {
682708
self.index
683709
}
684710

685-
pub fn to_ty<I: Interner>(self, interner: &I) -> Ty<I> {
686-
TyData::<I>::InferenceVar(self).intern(interner)
711+
pub fn to_ty<I: Interner>(self, interner: &I, kind: TyKind) -> Ty<I> {
712+
TyData::<I>::InferenceVar(self, kind).intern(interner)
687713
}
688714

689715
pub fn to_lifetime<I: Interner>(self, interner: &I) -> Lifetime<I> {
@@ -910,17 +936,34 @@ impl<I: Interner> ApplicationTy<I> {
910936
}
911937
}
912938

939+
/// Represents some extra knowledge we may have about the type variable.
940+
/// ```ignore
941+
/// let x: &[u32];
942+
/// let i = 1;
943+
/// x[i]
944+
/// ```
945+
/// In this example, `i` is known to be some type of integer. We can infer that
946+
/// it is `usize` because that is the only integer type that slices have an
947+
/// `Index` impl for. `i` would have a `TyKind` of `Integer` to guide the
948+
/// inference process.
949+
#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)]
950+
pub enum TyKind {
951+
General,
952+
Integer,
953+
Float,
954+
}
955+
913956
#[derive(Clone, PartialEq, Eq, Hash)]
914957
pub enum VariableKind<I: Interner> {
915-
Ty,
958+
Ty(TyKind),
916959
Lifetime,
917960
Const(Ty<I>),
918961
}
919962

920963
impl<I: Interner> VariableKind<I> {
921964
fn to_bound_variable(&self, interner: &I, bound_var: BoundVar) -> GenericArg<I> {
922965
match self {
923-
VariableKind::Ty => {
966+
VariableKind::Ty(_) => {
924967
GenericArgData::Ty(TyData::BoundVar(bound_var).intern(interner)).intern(interner)
925968
}
926969
VariableKind::Lifetime => {
@@ -1524,7 +1567,7 @@ impl<T: HasInterner> Binders<T> {
15241567
// The new variable is at the front and everything afterwards is shifted up by 1
15251568
let new_var = TyData::BoundVar(BoundVar::new(DebruijnIndex::INNERMOST, 0)).intern(interner);
15261569
let value = op(new_var);
1527-
let binders = VariableKinds::from(interner, iter::once(VariableKind::Ty));
1570+
let binders = VariableKinds::from(interner, iter::once(VariableKind::Ty(TyKind::General)));
15281571
Binders { binders, value }
15291572
}
15301573

@@ -1940,7 +1983,7 @@ impl<T: HasInterner> UCanonical<T> {
19401983
.map(|(index, pk)| {
19411984
let bound_var = BoundVar::new(DebruijnIndex::INNERMOST, index);
19421985
match &pk.kind {
1943-
VariableKind::Ty => {
1986+
VariableKind::Ty(_) => {
19441987
GenericArgData::Ty(TyData::BoundVar(bound_var).intern(interner))
19451988
.intern(interner)
19461989
}

‎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: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,8 @@ pub struct OpaqueTyDefn {
100100
#[derive(Clone, PartialEq, Eq, Debug)]
101101
pub enum VariableKind {
102102
Ty(Identifier),
103+
IntegerTy(Identifier),
104+
FloatTy(Identifier),
103105
Lifetime(Identifier),
104106
Const(Identifier),
105107
}

‎chalk-parse/src/parser.lalrpop

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -201,6 +201,8 @@ VariableKind: VariableKind = {
201201
Id => VariableKind::Ty(<>),
202202
LifetimeId => VariableKind::Lifetime(<>),
203203
"const" <id:Id> => VariableKind::Const(id),
204+
"int" <id:Id> => VariableKind::IntegerTy(id),
205+
"float" <id:Id> => VariableKind::FloatTy(id),
204206
};
205207

206208
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
_ => {}
@@ -462,7 +462,7 @@ fn match_ty<I: Interner>(
462462
.map(|ty| match_ty(builder, environment, &ty))
463463
.collect::<Result<_, Floundered>>()?;
464464
}
465-
TyData::BoundVar(_) | TyData::InferenceVar(_) => return Err(Floundered),
465+
TyData::BoundVar(_) | TyData::InferenceVar(_, _) => return Err(Floundered),
466466
TyData::Dyn(_) => {}
467467
})
468468
}

‎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)