use #[term] for Const

Author: nikomatsakis

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

@@ -1,11 +1,12 @@
 mod valtree;
 
 use super::{Parameter, Ty, Variable};
-use formality_core::{term, DowncastTo, Upcast, UpcastFrom, Visit};
+use formality_core::{term, DowncastTo, Upcast, UpcastFrom};
 use std::sync::Arc;
 pub use valtree::*;
 
-#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
+#[term]
+#[cast]
 pub struct Const {
     data: Arc<ConstData>,
 }
@@ -39,16 +40,14 @@ impl Const {
     }
 }
 
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
+#[term]
+#[customize(parse)]
 pub enum ConstData {
     Value(ValTree, Ty),
-    Variable(Variable),
-}
 
-impl UpcastFrom<Self> for ConstData {
-    fn upcast_from(term: Self) -> Self {
-        term
-    }
+    #[variable]
+    #[precedence(1)]
+    Variable(Variable),
 }
 
 impl DowncastTo<ConstData> for Const {
@@ -81,15 +80,16 @@ pub enum Bool {
     False,
 }
 
-impl UpcastFrom<Bool> for Const {
+impl UpcastFrom<Bool> for ConstData {
     fn upcast_from(term: Bool) -> Self {
-        Self::new(ConstData::Value(term.upcast(), Ty::bool()))
+        ConstData::Value(term.upcast(), Ty::bool())
     }
 }
 
-impl UpcastFrom<Variable> for ConstData {
-    fn upcast_from(v: Variable) -> Self {
-        Self::Variable(v)
+impl UpcastFrom<Bool> for Const {
+    fn upcast_from(term: Bool) -> Self {
+        let c: ConstData = term.upcast();
+        Const::new(c)
     }
 }
 

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

@@ -1,10 +1 @@
-use crate::grammar::Const;
 
-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, ty) => write!(f, "{valtree:?}_{ty:?}"),
-            crate::grammar::ConstData::Variable(r) => write!(f, "{r:?}"),
-        }
-    }
-}

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

@@ -4,7 +4,9 @@ use formality_core::parse::{ActiveVariant, CoreParse, ParseError, ParseResult, P
 use formality_core::Upcast;
 use formality_core::{seq, Set};
 
-use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RefKind, RigidName, Scalar, TraitId};
+use crate::grammar::{
+    AdtId, AssociatedItemId, Bool, ConstData, RefKind, RigidName, Scalar, TraitId, ValTree,
+};
 
 use super::{AliasTy, AssociatedTyName, Lt, Parameter, RigidTy, ScalarId, Ty};
 
@@ -106,22 +108,21 @@ fn parse_parameters<'t>(
 
 // For consts, we invest some effort into parsing them decently because it makes
 // writing tests so much more pleasant.
-impl CoreParse<Rust> for Const {
+impl CoreParse<Rust> for ConstData {
     fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
-        let mut parser: Parser<'_, '_, Const, Rust> = Parser::new(scope, text, "Ty");
-        parser.parse_variant_cast::<Bool>(1);
+        let mut parser: Parser<'_, '_, ConstData, Rust> = Parser::new(scope, text, "Ty");
+
         parser.parse_variant("Variable", 1, |p| p.variable());
-        parser.parse_variant("Int", 0, |p| p.nonterminal_with(parse_int));
+
+        parser.parse_variant_cast::<Bool>(1);
+
+        parser.parse_variant("Int", 0, |p| {
+            let n: u128 = p.number()?;
+            p.expect_char('_')?;
+            let ty: Ty = p.nonterminal()?;
+            Ok(ConstData::Value(Scalar::new(n).upcast(), ty))
+        });
+
         parser.finish()
     }
 }
-
-#[tracing::instrument(level = "trace", ret)]
-fn parse_int<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Const> {
-    Parser::single_variant(scope, text, "Ty", |p| {
-        let n: u128 = p.number()?;
-        p.expect_char('_')?;
-        let ty: Ty = p.nonterminal()?;
-        Ok(Const::valtree(Scalar::new(n), ty))
-    })
-}

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

@@ -17,22 +17,6 @@ impl formality_core::language::HasKind<FormalityLang> for Parameter {
     }
 }
 
-impl CoreFold<FormalityLang> for Const {
-    fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self {
-        match self.data() {
-            ConstData::Value(v, ty) => Self::valtree(
-                v.substitute(substitution_fn),
-                ty.substitute(substitution_fn),
-            ),
-            ConstData::Variable(v) => match substitution_fn(*v) {
-                None => self.clone(),
-                Some(Parameter::Const(c)) => c,
-                Some(param) => panic!("ill-kinded substitute: expected const, got {param:?}"),
-            },
-        }
-    }
-}
-
 impl CoreFold<FormalityLang> for ValTree {
     fn substitute(&self, _substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self {
         self.clone()

tests/ui/consts/mismatch.stderr

@@ -1,4 +1,4 @@
-Error: check_trait_impl(impl <> Foo < const 42_(rigid (scalar u32)) > for (rigid (scalar u32)) where [] { })
+Error: check_trait_impl(impl <> Foo < const value(42, (rigid (scalar u32))) > for (rigid (scalar u32)) where [] { })
 
 Caused by:
-    failed to prove {Foo((rigid (scalar u32)), const 42_(rigid (scalar u32)))} given {}, got {}
+    failed to prove {Foo((rigid (scalar u32)), const value(42, (rigid (scalar u32))))} given {}, got {}

tests/ui/consts/nonsense_rigid_const_bound.stderr

@@ -1,5 +1,5 @@
 Error: check_trait(Foo)
 
 Caused by:
-    0: prove_where_clause_well_formed(type_of_const 0_(rigid (scalar bool)) is (rigid (scalar u32)))
-    1: failed to prove {(rigid (scalar u32)) = (rigid (scalar bool))} given {@ ConstHasType(0_(rigid (scalar bool)) , (rigid (scalar u32)))}, got {}
+    0: prove_where_clause_well_formed(type_of_const value(0, (rigid (scalar bool))) is (rigid (scalar u32)))
+    1: failed to prove {(rigid (scalar u32)) = (rigid (scalar bool))} given {@ ConstHasType(value(0, (rigid (scalar bool))) , (rigid (scalar u32)))}, got {}