Skip to content

Commit c978057

Browse files
committed
Implement float type variables
Adds new notation for float inference variables, just like what was added for integers. - `?0f` is a float inference variable - `float N` is the notation for float variables in goals, for example: ``` exists<float N> { ... } ```
1 parent bc5391f commit c978057

File tree

7 files changed

+52
-4
lines changed

7 files changed

+52
-4
lines changed

chalk-integration/src/lowering.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -725,6 +725,10 @@ impl LowerVariableKind for VariableKind {
725725
chalk_ir::VariableKind::Ty(chalk_ir::TyKind::Integer),
726726
n.str.clone(),
727727
),
728+
VariableKind::FloatTy(n) => chalk_ir::WithKind::new(
729+
chalk_ir::VariableKind::Ty(chalk_ir::TyKind::Float),
730+
n.str.clone(),
731+
),
728732
VariableKind::Lifetime(n) => {
729733
chalk_ir::WithKind::new(chalk_ir::VariableKind::Lifetime, n.str.clone())
730734
}
@@ -1826,6 +1830,7 @@ impl Kinded for VariableKind {
18261830
match *self {
18271831
VariableKind::Ty(_) => Kind::Ty,
18281832
VariableKind::IntegerTy(_) => Kind::Ty,
1833+
VariableKind::FloatTy(_) => Kind::Ty,
18291834
VariableKind::Lifetime(_) => Kind::Lifetime,
18301835
VariableKind::Const(_) => Kind::Const,
18311836
}

chalk-ir/src/debug.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -181,6 +181,7 @@ impl<I: Interner> Debug for TyData<I> {
181181
TyData::Dyn(clauses) => write!(fmt, "{:?}", clauses),
182182
TyData::InferenceVar(var, TyKind::General) => write!(fmt, "{:?}", var),
183183
TyData::InferenceVar(var, TyKind::Integer) => write!(fmt, "{:?}i", var),
184+
TyData::InferenceVar(var, TyKind::Float) => write!(fmt, "{:?}f", var),
184185
TyData::Apply(apply) => write!(fmt, "{:?}", apply),
185186
TyData::Alias(alias) => write!(fmt, "{:?}", alias),
186187
TyData::Placeholder(index) => write!(fmt, "{:?}", index),
@@ -279,6 +280,7 @@ impl<'a, I: Interner> Debug for VariableKindsInnerDebug<'a, I> {
279280
match binder {
280281
VariableKind::Ty(TyKind::General) => write!(fmt, "type")?,
281282
VariableKind::Ty(TyKind::Integer) => write!(fmt, "integer type")?,
283+
VariableKind::Ty(TyKind::Float) => write!(fmt, "float type")?,
282284
VariableKind::Lifetime => write!(fmt, "lifetime")?,
283285
VariableKind::Const(ty) => write!(fmt, "const: {:?}", ty)?,
284286
}
@@ -769,6 +771,7 @@ impl<I: Interner> Debug for VariableKind<I> {
769771
match self {
770772
VariableKind::Ty(TyKind::General) => write!(fmt, "type"),
771773
VariableKind::Ty(TyKind::Integer) => write!(fmt, "integer type"),
774+
VariableKind::Ty(TyKind::Float) => write!(fmt, "float type"),
772775
VariableKind::Lifetime => write!(fmt, "lifetime"),
773776
VariableKind::Const(ty) => write!(fmt, "const: {:?}", ty),
774777
}
@@ -781,6 +784,7 @@ impl<I: Interner, T: Debug> Debug for WithKind<I, T> {
781784
match &self.kind {
782785
VariableKind::Ty(TyKind::General) => write!(fmt, "{:?} with kind type", value),
783786
VariableKind::Ty(TyKind::Integer) => write!(fmt, "{:?} with kind integer type", value),
787+
VariableKind::Ty(TyKind::Float) => write!(fmt, "{:?} with kind float type", value),
784788
VariableKind::Lifetime => write!(fmt, "{:?} with kind lifetime", value),
785789
VariableKind::Const(ty) => write!(fmt, "{:?} with kind {:?}", value, ty),
786790
}

chalk-ir/src/lib.rs

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -357,6 +357,17 @@ impl<I: Interner> Ty<I> {
357357
}
358358
}
359359

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+
360371
/// True if this type contains "bound" types/lifetimes, and hence
361372
/// needs to be shifted across binders. This is a very inefficient
362373
/// check, intended only for debug assertions, because I am lazy.
@@ -925,7 +936,7 @@ impl<I: Interner> ApplicationTy<I> {
925936
}
926937
}
927938

928-
/// Represents some extra knowledge we may have about the variable.
939+
/// Represents some extra knowledge we may have about the type variable.
929940
/// ```ignore
930941
/// let x: &[u32];
931942
/// let i = 1;
@@ -939,6 +950,7 @@ impl<I: Interner> ApplicationTy<I> {
939950
pub enum TyKind {
940951
General,
941952
Integer,
953+
Float,
942954
}
943955

944956
#[derive(Clone, PartialEq, Eq, Hash)]

chalk-parse/src/ast.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -101,6 +101,7 @@ pub struct OpaqueTyDefn {
101101
pub enum VariableKind {
102102
Ty(Identifier),
103103
IntegerTy(Identifier),
104+
FloatTy(Identifier),
104105
Lifetime(Identifier),
105106
Const(Identifier),
106107
}

chalk-parse/src/parser.lalrpop

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,7 @@ VariableKind: VariableKind = {
202202
LifetimeId => VariableKind::Lifetime(<>),
203203
"const" <id:Id> => VariableKind::Const(id),
204204
"int" <id:Id> => VariableKind::IntegerTy(id),
205+
"float" <id:Id> => VariableKind::FloatTy(id),
205206
};
206207

207208
AssocTyValue: AssocTyValue = {

chalk-solve/src/infer/unify.rs

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -140,10 +140,13 @@ impl<'t, I: Interner> Unifier<'t, I> {
140140
=> {
141141
let ty = ty_data.clone().intern(interner);
142142

143-
match (kind, ty.is_integer(interner)) {
144-
(TyKind::General, _)
143+
match (kind, ty.is_integer(interner), ty.is_float(interner)) {
144+
// General inference variables can unify with any type
145+
(TyKind::General, _, _)
145146
// Integer inference variables can only unify with integer types
146-
| (TyKind::Integer, true) => self.unify_var_ty(var, &ty),
147+
| (TyKind::Integer, true, _)
148+
// Float inference variables can only unify with float types
149+
| (TyKind::Float, _, true) => self.unify_var_ty(var, &ty),
147150
_ => Err(NoSolution),
148151
}
149152
}

tests/test/numerics.rs

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,3 +55,25 @@ fn integer_kind_trait() {
5555
}
5656
}
5757
}
58+
59+
/// The `integer_kind_trait` test, but for floats
60+
#[test]
61+
fn float_kind_trait() {
62+
test! {
63+
program {
64+
trait Foo {}
65+
struct Bar {}
66+
67+
impl Foo for f32 {}
68+
impl Foo for Bar {}
69+
}
70+
71+
goal {
72+
exists<float N> {
73+
N: Foo
74+
}
75+
} yields {
76+
"Unique; substitution [?0 := Float(F32)]"
77+
}
78+
}
79+
}

0 commit comments

Comments
 (0)