Attach types to value constants

Author: oli-obk

crates/formality-types/src/fold.rs

@@ -76,7 +76,10 @@ impl Fold for Ty {
 impl Fold for Const {
     fn substitute(&self, substitution_fn: SubstitutionFn<'_>) -> Self {
         match self.data() {
-            ConstData::Value(v) => Self::new(v.substitute(substitution_fn)),
+            ConstData::Value(v, ty) => Self::valtree(
+                v.substitute(substitution_fn),
+                ty.substitute(substitution_fn),
+            ),
             ConstData::Variable(v) => match substitution_fn(v.clone()) {
                 None => self.clone(),
                 Some(Parameter::Const(c)) => c,

crates/formality-types/src/grammar/consts.rs

@@ -2,7 +2,7 @@ mod valtree;
 
 use crate::cast::{Upcast, UpcastFrom};
 
-use super::{Parameter, Variable};
+use super::{Parameter, Ty, Variable};
 use formality_macros::{term, Visit};
 use std::sync::Arc;
 pub use valtree::*;
@@ -21,20 +21,31 @@ impl Const {
             data: Arc::new(data.upcast()),
         }
     }
+
+    pub fn valtree(vt: impl Upcast<ValTree>, ty: impl Upcast<Ty>) -> Self {
+        Self::new(ConstData::Value(vt.upcast(), ty.upcast()))
+    }
+
     pub fn as_variable(&self) -> Option<Variable> {
         match self.data() {
-            ConstData::Value(_) => None,
+            ConstData::Value(_, _) => None,
             ConstData::Variable(var) => Some(var.clone()),
         }
     }
 }
 
 #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
 pub enum ConstData {
-    Value(ValTree),
+    Value(ValTree, Ty),
     Variable(Variable),
 }
 
+impl UpcastFrom<Self> for ConstData {
+    fn upcast_from(term: Self) -> Self {
+        term
+    }
+}
+
 #[term]
 pub enum Bool {
     #[grammar(true)]
@@ -45,13 +56,7 @@ pub enum Bool {
 
 impl UpcastFrom<Bool> for Const {
     fn upcast_from(term: Bool) -> Self {
-        Self::new(ValTree::upcast_from(term))
-    }
-}
-
-impl UpcastFrom<ValTree> for ConstData {
-    fn upcast_from(v: ValTree) -> Self {
-        Self::Value(v)
+        Self::new(ConstData::Value(term.upcast(), Ty::bool()))
     }
 }
 

crates/formality-types/src/grammar/consts/valtree.rs

@@ -2,7 +2,7 @@ use formality_macros::Visit;
 
 use crate::cast::{Upcast, UpcastFrom};
 
-use super::{Bool, ConstData};
+use super::Bool;
 
 #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
 pub enum ValTree {
@@ -48,9 +48,9 @@ impl UpcastFrom<Scalar> for ValTree {
     }
 }
 
-impl UpcastFrom<Scalar> for ConstData {
-    fn upcast_from(s: Scalar) -> Self {
-        ValTree::upcast_from(s).upcast()
+impl UpcastFrom<Self> for ValTree {
+    fn upcast_from(s: Self) -> Self {
+        s
     }
 }
 

crates/formality-types/src/grammar/ty.rs

@@ -80,6 +80,14 @@ impl Ty {
             vec![l.to::<Parameter>(), self.to::<Parameter>()],
         )
     }
+
+    pub fn bool() -> Ty {
+        RigidTy {
+            name: RigidName::ScalarId(ScalarId::Bool),
+            parameters: vec![],
+        }
+        .upcast()
+    }
 }
 
 impl UpcastFrom<TyData> for Ty {

crates/formality-types/src/grammar/ty/debug_impls.rs

@@ -14,7 +14,7 @@ impl std::fmt::Debug for super::Ty {
 impl std::fmt::Debug for Const {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         match self.data() {
-            crate::grammar::ConstData::Value(valtree) => write!(f, "{valtree:?}"),
+            crate::grammar::ConstData::Value(valtree, ty) => write!(f, "{valtree:?}_{ty:?}"),
             crate::grammar::ConstData::Variable(r) => write!(f, "{r:?}"),
         }
     }

crates/formality-types/src/grammar/ty/parse_impls.rs

@@ -215,13 +215,15 @@ impl Parse for Const {
 
 #[tracing::instrument(level = "trace", ret)]
 fn parse_int<'t>(scope: &crate::parse::Scope, text: &'t str) -> ParseResult<'t, Const> {
-    let (pos, _) = text
-        .match_indices(|c: char| !c.is_numeric())
-        .next()
-        .unwrap_or((text.len(), text));
-    let (num, text) = text.split_at(pos);
+    let (num, text) = text.split_once('_').ok_or_else(|| {
+        ParseError::at(
+            text,
+            format!("numeric constants must be followed by an `_` and their type"),
+        )
+    })?;
     let n: u128 = num
         .parse()
         .map_err(|err| ParseError::at(num, format!("could not parse number: {err}")))?;
-    Ok((Const::new(Scalar::new(n)), text))
+    let (ty, text) = Ty::parse(scope, text)?;
+    Ok((Const::valtree(Scalar::new(n), ty), text))
 }

tests/consts.rs

@@ -25,8 +25,8 @@ fn test_holds() {
     expect_test::expect![[r#"
         Err(
             Error {
-                context: "check_trait_impl(impl <> Foo < const 0 > for (rigid (scalar u32)) where [] { })",
-                source: "failed to prove {Foo((rigid (scalar u32)), const 0)} given {}, got {}",
+                context: "check_trait_impl(impl <> Foo < const 0_(rigid (scalar bool)) > for (rigid (scalar u32)) where [] { })",
+                source: "failed to prove {Foo((rigid (scalar u32)), const 0_(rigid (scalar bool)))} given {}, got {}",
             },
         )
     "#]]
@@ -46,8 +46,8 @@ fn test_mismatch() {
     expect_test::expect![[r#"
         Err(
             Error {
-                context: "check_trait_impl(impl <> Foo < const 42 > for (rigid (scalar u32)) where [] { })",
-                source: "failed to prove {Foo((rigid (scalar u32)), const 42)} given {}, got {}",
+                context: "check_trait_impl(impl <> Foo < const 42_(rigid (scalar u32)) > for (rigid (scalar u32)) where [] { })",
+                source: "failed to prove {Foo((rigid (scalar u32)), const 42_(rigid (scalar u32)))} given {}, got {}",
             },
         )
     "#]]
@@ -56,7 +56,7 @@ fn test_mismatch() {
             crate Foo {
                 trait Foo<const C> where [type_of_const C is bool] {}
 
-                impl<> Foo<const 42> for u32 where [] {}
+                impl<> Foo<const 42_u32> for u32 where [] {}
             }
         ]",
     ));