modify #[variable] to take kind explicitly

The `variable` parser method is now simpler
and just returns a variable; this also lets
`Variable` implement `Parse`.

We now have the helper `variable_of_kind`.

This is all useful in Dada which wants to parse variables
in slightly more flexible ways and in particular
*doesn't* want to force them to be downcasted.

Overall it seems more obvious.

Author: nikomatsakis

crates/formality-core/src/language.rs

@@ -1,7 +1,6 @@
 use crate::cast::UpcastFrom;
 use crate::term::CoreTerm;
 use crate::variable::{CoreBoundVar, CoreExistentialVar, CoreUniversalVar, CoreVariable};
-use crate::DowncastTo;
 use std::fmt::Debug;
 use std::hash::Hash;
 
@@ -21,8 +20,7 @@ pub trait Language: 'static + Copy + Ord + Hash + Debug + Default {
         + UpcastFrom<CoreVariable<Self>>
         + UpcastFrom<CoreUniversalVar<Self>>
         + UpcastFrom<CoreExistentialVar<Self>>
-        + UpcastFrom<CoreBoundVar<Self>>
-        + DowncastTo<CoreVariable<Self>>;
+        + UpcastFrom<CoreBoundVar<Self>>;
 
     /// The token (typically `<`) used to open binders.
     const BINDING_OPEN: char;

crates/formality-core/src/lib.rs

@@ -164,7 +164,7 @@ macro_rules! declare_language {
             where
                 T: Parse,
             {
-                term_with(None::<(String, $param)>, text)
+                term_with(None::<(String, grammar::Variable)>, text)
             }
 
             /// Parses `text` as a term with the given bindings in scope.
@@ -175,7 +175,7 @@ macro_rules! declare_language {
             pub fn term_with<T, B>(bindings: impl IntoIterator<Item = B>, text: &str) -> $crate::Fallible<T>
             where
                 T: Parse,
-                B: $crate::Upcast<(String, <FormalityLang as Language>::Parameter)>,
+                B: $crate::Upcast<(String, grammar::Variable)>,
             {
                 $crate::parse::core_term_with::<FormalityLang, T, B>(bindings, text)
             }

crates/formality-core/src/parse.rs

@@ -3,10 +3,10 @@ use std::sync::Arc;
 use crate::{
     binder::CoreBinder,
     collections::Set,
-    language::{CoreKind, CoreParameter, Language},
+    language::{CoreKind, Language},
     set,
     term::CoreTerm,
-    variable::CoreBoundVar,
+    variable::{CoreBoundVar, CoreVariable},
     Fallible, Upcast, UpcastFrom, Upcasted,
 };
 use std::fmt::Debug;
@@ -35,7 +35,7 @@ pub fn core_term_with<L, T, B>(bindings: impl IntoIterator<Item = B>, text: &str
 where
     T: CoreParse<L>,
     L: Language,
-    B: Upcast<(String, CoreParameter<L>)>,
+    B: Upcast<(String, CoreVariable<L>)>,
 {
     let scope = Scope::new(bindings.into_iter().map(|b| b.upcast()));
     let parse = match T::parse(&scope, text) {
@@ -170,19 +170,19 @@ pub type TokenResult<'t, T> = Result<(T, &'t str), Set<ParseError<'t>>>;
 /// Tracks the variables in scope at this point in parsing.
 #[derive(Clone, Debug, Default)]
 pub struct Scope<L: Language> {
-    bindings: Vec<(String, CoreParameter<L>)>,
+    bindings: Vec<(String, CoreVariable<L>)>,
 }
 
 impl<L: Language> Scope<L> {
     /// Creates a new scope with the given set of bindings.
-    pub fn new(bindings: impl IntoIterator<Item = (String, CoreParameter<L>)>) -> Self {
+    pub fn new(bindings: impl IntoIterator<Item = (String, CoreVariable<L>)>) -> Self {
         Self {
             bindings: bindings.into_iter().collect(),
         }
     }
 
     /// Look for a variable with the given name.
-    pub fn lookup(&self, name: &str) -> Option<CoreParameter<L>> {
+    pub fn lookup(&self, name: &str) -> Option<CoreVariable<L>> {
         self.bindings
             .iter()
             .rev()
@@ -193,7 +193,7 @@ impl<L: Language> Scope<L> {
     /// Create a new scope that extends `self` with `bindings`.
     pub fn with_bindings(
         &self,
-        bindings: impl IntoIterator<Item = impl Upcast<(String, CoreParameter<L>)>>,
+        bindings: impl IntoIterator<Item = impl Upcast<(String, CoreVariable<L>)>>,
     ) -> Self {
         let mut s = self.clone();
         s.bindings.extend(bindings.into_iter().upcasted());
@@ -367,3 +367,9 @@ impl<L: Language, A: CoreParse<L>, B: CoreParse<L>, C: CoreParse<L>> CoreParse<L
         })
     }
 }
+
+impl<L: Language> CoreParse<L> for CoreVariable<L> {
+    fn parse<'t>(scope: &Scope<L>, text: &'t str) -> ParseResult<'t, Self> {
+        Parser::single_variant(scope, text, "variable", |p| p.variable())
+    }
+}

crates/formality-core/src/parse/parser.rs

@@ -2,11 +2,11 @@ use std::fmt::Debug;
 use std::str::FromStr;
 
 use crate::{
-    language::{CoreParameter, HasKind, Language},
+    language::Language,
     parse::parser::left_recursion::{CurrentState, LeftRight},
     set,
     variable::CoreVariable,
-    Downcast, DowncastFrom, Set, Upcast,
+    Set, Upcast,
 };
 
 use super::{CoreParse, ParseError, ParseResult, Scope, SuccessfulParse, TokenResult};
@@ -406,6 +406,11 @@ where
         self.current_text
     }
 
+    /// Return the set of variables in scope
+    pub fn scope(&self) -> &Scope<L> {
+        &self.scope
+    }
+
     /// Skips whitespace in the input, producing no reduction.
     pub fn skip_whitespace(&mut self) {
         self.current_text = skip_whitespace(self.current_text);
@@ -616,53 +621,48 @@ where
         )
     }
 
-    /// Parses the next identifier as a variable in scope
-    /// with the kind appropriate for the return type `R`.
+    /// Parses the next identifier as a variable in scope.
     ///
     /// **NB:** This departs from the limits of context-free
     /// grammars -- the scope is a piece of context that affects how
     /// our parsing proceeds!
-    ///
-    /// Variables don't implement Parse themselves
-    /// because you can't parse a variable into a *variable*,
-    /// instead, you parse it into a `Parameter`.
-    /// The parsing code then downcasts that parameter into the
-    /// type it wants (e.g., in Rust, a `Ty`).
-    /// This downcast will fail if the `Parameter` is not of the appropriate
-    /// kind (which will result in a parse error).
-    ///
-    /// This avoids "miskinding", i.e., parsing a `Ty` that contains
-    /// a lifetime variable.
-    ///
-    /// It also allows parsing where you use variables to stand for
-    /// more complex parameters, which is kind of combining parsing
-    /// and substitution and can be convenient in tests.
     #[tracing::instrument(level = "trace", skip(self), ret)]
-    pub fn variable<R>(&mut self) -> Result<R, Set<ParseError<'t>>>
-    where
-        R: Debug + DowncastFrom<CoreParameter<L>>,
-    {
+    pub fn variable(&mut self) -> Result<CoreVariable<L>, Set<ParseError<'t>>> {
         self.skip_whitespace();
-        let type_name = std::any::type_name::<R>();
         let text0 = self.current_text;
         let id = self.identifier()?;
         match self.scope.lookup(&id) {
-            Some(parameter) => match parameter.downcast() {
-                Some(v) => Ok(v),
-                None => Err(ParseError::at(
-                    text0,
-                    format!(
-                        "wrong kind, expected a {}, found `{:?}`, which is a `{:?}`",
-                        type_name,
-                        parameter,
-                        parameter.kind()
-                    ),
-                )),
-            },
+            Some(v) => Ok(v),
             None => Err(ParseError::at(text0, format!("unrecognized variable"))),
         }
     }
 
+    /// Parses the next identifier as a [variable in scope](`Self::variable`)
+    /// and checks that it has the right kind. This is a useful
+    /// helper method to avoid mis-kinding variables.
+    #[tracing::instrument(level = "trace", skip(self), ret)]
+    pub fn variable_of_kind(
+        &mut self,
+        kind: L::Kind,
+    ) -> Result<CoreVariable<L>, Set<ParseError<'t>>> {
+        self.skip_whitespace();
+        let text0 = self.current_text;
+        let v = self.variable()?;
+        if v.kind() == kind {
+            Ok(v)
+        } else {
+            Err(ParseError::at(
+                text0,
+                format!(
+                    "expected a variable of kind `{:?}`, found `{:?}`, which has kind `{:?}`",
+                    kind,
+                    v,
+                    v.kind()
+                ),
+            ))
+        }
+    }
+
     /// Extract a number from the input, erroring if the input does not start with a number.
     #[tracing::instrument(level = "trace", skip(self), ret)]
     pub fn number<T>(&mut self) -> Result<T, Set<ParseError<'t>>>

crates/formality-macros/src/attrs.rs

@@ -2,7 +2,7 @@
 
 use syn::{spanned::Spanned, Attribute, DeriveInput};
 
-use crate::{custom::Customize, precedence::Precedence};
+use crate::{custom::Customize, precedence::Precedence, variable::Variable};
 
 /// Checks for any kind of attribute that indicates an "is-a" relationship,
 /// e.g. `#[cast]` and `#[variable]`.
@@ -39,6 +39,11 @@ pub(crate) fn has_variable_attr(attrs: &[Attribute]) -> bool {
     attrs.iter().any(|a| a.path().is_ident("variable"))
 }
 
+/// Extract a `#[variable]` attribute (if any)
+pub(crate) fn variable(attrs: &[Attribute]) -> syn::Result<Option<Variable>> {
+    parse_attr_named(attrs, "variable")
+}
+
 /// Extract a `#[precedence]` level, defaults to 0
 pub(crate) fn precedence(attrs: &[Attribute]) -> syn::Result<Precedence> {
     Ok(parse_attr_named(attrs, "precedence")?.unwrap_or_default())

crates/formality-macros/src/lib.rs

@@ -18,6 +18,7 @@ mod precedence;
 mod spec;
 mod term;
 mod test;
+mod variable;
 mod visit;
 
 // synstructure::decl_derive!([Fold] => fold::derive_fold);

crates/formality-macros/src/parse.rs

@@ -7,8 +7,9 @@ use syn::{spanned::Spanned, Attribute};
 use synstructure::BindingInfo;
 
 use crate::{
-    attrs::{has_cast_attr, has_variable_attr, precedence},
+    attrs::{has_cast_attr, has_variable_attr, precedence, variable},
     spec::{self, FieldMode, FormalitySpec},
+    variable::Variable,
 };
 
 /// Derive the `Parse` impl, using an optional grammar supplied "from the outside".
@@ -76,13 +77,13 @@ fn parse_variant(
     any_variable_variant: bool,
 ) -> syn::Result<TokenStream> {
     let ast = variant.ast();
-    let has_variable_attr = has_variable_attr(ast.attrs);
+    let variable_attr = variable(ast.attrs)?;
     let mut stream = TokenStream::default();
 
     // If there are variable variants -- but this is not one -- then we always begin by rejecting
     // variable names. This avoids ambiguity in a case like `for<ty X> { X : Debug }`, where we
     // want to parse `X` as a type variable.
-    if any_variable_variant && !has_variable_attr {
+    if any_variable_variant && variable_attr.is_none() {
         stream.extend(quote_spanned!(ast.ident.span() => __p.reject_variable()?;));
     }
 
@@ -107,13 +108,22 @@ fn parse_variant(
             __p.expect_keyword(#literal)?;
             Ok(#construct)
         });
-    } else if has_variable_attr {
+    } else if let Some(Variable { kind }) = variable_attr {
         // Has the `#[variable]` attribute -- parse an identifier and then check to see if it is present
         // in the scope. If so, downcast it and check that it has the correct kind.
+        if variant.bindings().len() != 1 {
+            return Err(syn::Error::new(
+                variant.ast().ident.span(),
+                "can only automatically parse variable variants with one binding",
+            ));
+        }
+        let v0_binding = &variant.bindings()[0];
+        let v0 = field_ident(v0_binding.ast(), 0);
+        let construct = variant.construct(field_ident);
         stream.extend(quote_spanned! {
             ast.ident.span() =>
-            let v = __p.variable()?;
-            Ok(v)
+            let #v0 = __p.variable_of_kind(#kind)?;
+            Ok(#construct)
         });
     } else if has_cast_attr(variant.ast().attrs) {
         // Has the `#[cast]` attribute -- just parse the bindings (comma separated, if needed)

crates/formality-macros/src/variable.rs

@@ -0,0 +1,20 @@
+use proc_macro2::TokenStream;
+
+/// The contents of a `#[variable]` attribute. Currently just a kind.
+pub struct Variable {
+    pub kind: syn::Expr,
+}
+
+impl syn::parse::Parse for Variable {
+    fn parse(input: syn::parse::ParseStream) -> syn::Result<Self> {
+        let kind: syn::Expr = input.parse()?;
+
+        let tokens: TokenStream = input.parse()?;
+        let mut tokens = tokens.into_iter();
+        if let Some(token) = tokens.next() {
+            return Err(syn::Error::new(token.span(), "extra tokens"));
+        }
+
+        Ok(Variable { kind })
+    }
+}

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

@@ -107,7 +107,7 @@ pub enum TyData {
     AliasTy(AliasTy),
     #[cast]
     PredicateTy(PredicateTy),
-    #[variable]
+    #[variable(ParameterKind::Ty)]
     Variable(Variable),
 }
 
@@ -339,7 +339,7 @@ impl DowncastTo<LtData> for Lt {
 pub enum LtData {
     Static,
 
-    #[variable]
+    #[variable(ParameterKind::Lt)]
     Variable(Variable),
 }
 

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

@@ -10,7 +10,7 @@ use crate::grammar::{
     AdtId, AssociatedItemId, Bool, ConstData, RefKind, RigidName, Scalar, TraitId,
 };
 
-use super::{AliasTy, AssociatedTyName, Lt, Parameter, RigidTy, ScalarId, Ty};
+use super::{AliasTy, AssociatedTyName, Lt, Parameter, ParameterKind, RigidTy, ScalarId, Ty};
 
 use crate::rust::FormalityLang as Rust;
 
@@ -124,7 +124,9 @@ fn parse_parameters<'t>(
 impl CoreParse<Rust> for ConstData {
     fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
         Parser::multi_variant(scope, text, "ConstData", |parser| {
-            parser.parse_variant("Variable", Precedence::default(), |p| p.variable());
+            parser.parse_variant("Variable", Precedence::default(), |p| {
+                p.variable_of_kind(ParameterKind::Const).upcast()
+            });
 
             parser.parse_variant_cast::<Bool>(Precedence::default());