make Lt use #[term]

Author: nikomatsakis

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

@@ -281,7 +281,8 @@ pub enum Variance {
     Invariant,
 }
 
-#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+#[term]
+#[cast]
 pub struct Lt {
     data: Arc<LtData>,
 }
@@ -321,22 +322,12 @@ impl DowncastTo<LtData> for Lt {
     }
 }
 
-impl UpcastFrom<LtData> for Parameter {
-    fn upcast_from(v: LtData) -> Self {
-        Lt::new(v).upcast()
-    }
-}
-
-#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
+#[term]
 pub enum LtData {
     Static,
-    Variable(Variable),
-}
 
-impl UpcastFrom<LtData> for LtData {
-    fn upcast_from(term: LtData) -> Self {
-        term
-    }
+    #[variable]
+    Variable(Variable),
 }
 
 impl UpcastFrom<Variable> for Parameter {
@@ -375,11 +366,10 @@ cast_impl!((BoundVar) <: (Variable) <: (Ty));
 cast_impl!((UniversalVar) <: (Variable) <: (Parameter));
 cast_impl!((ExistentialVar) <: (Variable) <: (Parameter));
 cast_impl!((BoundVar) <: (Variable) <: (Parameter));
-cast_impl!(Lt);
-cast_impl!(LtData::Variable(Variable));
 cast_impl!((ExistentialVar) <: (Variable) <: (LtData));
 cast_impl!((UniversalVar) <: (Variable) <: (LtData));
 cast_impl!((BoundVar) <: (Variable) <: (LtData));
 cast_impl!((UniversalVar) <: (LtData) <: (Lt));
 cast_impl!((ExistentialVar) <: (LtData) <: (Lt));
 cast_impl!((BoundVar) <: (LtData) <: (Lt));
+cast_impl!((LtData) <: (Lt) <: (Parameter));

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

@@ -8,12 +8,3 @@ impl std::fmt::Debug for Const {
         }
     }
 }
-
-impl std::fmt::Debug for super::Lt {
-    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        match self.data() {
-            super::LtData::Static => write!(f, "static"),
-            super::LtData::Variable(v) => write!(f, "{:?}", v),
-        }
-    }
-}

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

@@ -6,7 +6,7 @@ use formality_core::{seq, Set};
 
 use crate::grammar::{AdtId, AssociatedItemId, Bool, Const, RefKind, RigidName, Scalar, TraitId};
 
-use super::{AliasTy, AssociatedTyName, Lt, LtData, Parameter, RigidTy, ScalarId, Ty};
+use super::{AliasTy, AssociatedTyName, Lt, Parameter, RigidTy, ScalarId, Ty};
 
 use crate::rust::FormalityLang as Rust;
 
@@ -104,18 +104,6 @@ fn parse_parameters<'t>(
     Ok(parameters)
 }
 
-impl CoreParse<Rust> for Lt {
-    fn parse<'t>(scope: &Scope<Rust>, text0: &'t str) -> ParseResult<'t, Self> {
-        let mut parser = Parser::new(scope, text0, "Lt");
-        parser.parse_variant("static", 0, |p| {
-            p.expect_keyword("static")?;
-            Ok(Lt::new(LtData::Static))
-        });
-        parser.parse_variant("variable", 0, |p| p.variable());
-        parser.finish()
-    }
-}
-
 // For consts, we invest some effort into parsing them decently because it makes
 // writing tests so much more pleasant.
 impl CoreParse<Rust> for Const {

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

@@ -1,43 +1,12 @@
-use crate::grammar::{Const, ConstData, Lt, LtData, Parameter, ValTree};
-use crate::rust::Variable;
+use crate::grammar::{Const, ConstData, Parameter, ValTree};
 use crate::FormalityLang;
 use formality_core::{
     fold::{CoreFold, SubstitutionFn},
     language::CoreKind,
-    visit::CoreVisit,
 };
 
 use super::ParameterKind;
 
-impl CoreVisit<FormalityLang> for LtData {
-    fn free_variables(&self) -> Vec<Variable> {
-        match self {
-            LtData::Variable(v) => {
-                if v.is_free() {
-                    vec![*v]
-                } else {
-                    vec![]
-                }
-            }
-            LtData::Static => vec![],
-        }
-    }
-
-    fn size(&self) -> usize {
-        match self {
-            LtData::Variable(v) => v.size(),
-            LtData::Static => 1,
-        }
-    }
-
-    fn assert_valid(&self) {
-        match self {
-            LtData::Variable(v) => v.assert_valid(),
-            LtData::Static => (),
-        }
-    }
-}
-
 impl formality_core::language::HasKind<FormalityLang> for Parameter {
     fn kind(&self) -> CoreKind<FormalityLang> {
         match self {
@@ -69,30 +38,3 @@ impl CoreFold<FormalityLang> for ValTree {
         self.clone()
     }
 }
-
-impl CoreFold<FormalityLang> for Lt {
-    fn substitute(&self, substitution_fn: SubstitutionFn<'_, FormalityLang>) -> Self {
-        match self.data() {
-            LtData::Static => self.clone(),
-            LtData::Variable(v) => match substitution_fn(*v) {
-                None => self.clone(),
-                Some(Parameter::Lt(t)) => t,
-                Some(param) => panic!("ill-kinded substitute: expected lifetime, got {param:?}"),
-            },
-        }
-    }
-}
-
-impl CoreVisit<FormalityLang> for Lt {
-    fn free_variables(&self) -> Vec<Variable> {
-        self.data().free_variables()
-    }
-
-    fn size(&self) -> usize {
-        self.data().size()
-    }
-
-    fn assert_valid(&self) {
-        self.data().assert_valid()
-    }
-}