automatically reject variable names

When one variant is tagged as `#[variable]`,
we now automatically reject variable names from
other variants. This means we can use `#[precedence]`
just to encode true *precedence* (i.e., of operators).
This was important since there was a conflict where
variables wanted to be the same *precedence* as other
identifiers in a logical sense.

Author: nikomatsakis

crates/formality-core/src/language.rs

@@ -1,6 +1,7 @@
 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;
 
@@ -20,7 +21,8 @@ pub trait Language: 'static + Copy + Ord + Hash + Debug + Default {
         + UpcastFrom<CoreVariable<Self>>
         + UpcastFrom<CoreUniversalVar<Self>>
         + UpcastFrom<CoreExistentialVar<Self>>
-        + UpcastFrom<CoreBoundVar<Self>>;
+        + UpcastFrom<CoreBoundVar<Self>>
+        + DowncastTo<CoreVariable<Self>>;
 
     /// The token (typically `<`) used to open binders.
     const BINDING_OPEN: char;

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

@@ -3,7 +3,9 @@ use std::str::FromStr;
 
 use crate::{
     language::{CoreParameter, HasKind, Language},
-    set, Downcast, DowncastFrom, Set, Upcast,
+    set,
+    variable::CoreVariable,
+    Downcast, DowncastFrom, Set, Upcast,
 };
 
 use super::{CoreParse, ParseError, ParseResult, Scope, SuccessfulParse, TokenResult};
@@ -471,6 +473,21 @@ where
         result
     }
 
+    /// Returns an error if an in-scope variable name is found.
+    /// The derive automatically inserts calls to this for all other variants
+    /// if any variant is declared `#[variable]`.
+    pub fn reject_variable(&self) -> Result<(), Set<ParseError<'t>>> {
+        self.reject::<CoreVariable<L>>(
+            |p| p.variable(),
+            |var| {
+                ParseError::at(
+                    self.text,
+                    format!("found unexpected in-scope variable {:?}", var),
+                )
+            },
+        )
+    }
+
     /// Parses the next identifier as a variable in scope
     /// with the kind appropriate for the return type `R`.
     ///

crates/formality-macros/src/parse.rs

@@ -37,10 +37,17 @@ pub(crate) fn derive_parse_with_spec(
         }
     }
 
+    // Determine whether *any* variant is marked as `#[variable]`.
+    // If so, all *other* variants will automatically reject in-scope variable names.
+    let any_variable_variant = s
+        .variants()
+        .iter()
+        .any(|v| has_variable_attr(v.ast().attrs));
+
     let mut parse_variants = TokenStream::new();
     for variant in s.variants() {
         let variant_name = Literal::string(&format!("{}::{}", s.ast().ident, variant.ast().ident));
-        let v = parse_variant(variant, external_spec)?;
+        let v = parse_variant(variant, external_spec, any_variable_variant)?;
         let precedence = precedence(&variant.ast().attrs)?.literal();
         parse_variants.extend(quote_spanned!(
             variant.ast().ident.span() =>
@@ -66,17 +73,27 @@ pub(crate) fn derive_parse_with_spec(
 fn parse_variant(
     variant: &synstructure::VariantInfo,
     external_spec: Option<&FormalitySpec>,
+    any_variable_variant: bool,
 ) -> syn::Result<TokenStream> {
     let ast = variant.ast();
+    let has_variable_attr = has_variable_attr(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 {
+        stream.extend(quote_spanned!(ast.ident.span() => __p.reject_variable()?;));
+    }
 
     // When invoked like `#[term(foo)]`, use the spec from `foo`
     if let Some(spec) = external_spec {
-        return parse_variant_with_attr(variant, spec);
+        return parse_variant_with_attr(variant, spec, stream);
     }
 
     // Else, look for a `#[grammar]` attribute on the variant
     if let Some(attr) = get_grammar_attr(ast.attrs) {
-        return parse_variant_with_attr(variant, &attr?);
+        return parse_variant_with_attr(variant, &attr?, stream);
     }
 
     // If no `#[grammar(...)]` attribute is provided, then we provide default behavior.
@@ -85,44 +102,46 @@ fn parse_variant(
         // No bindings (e.g., `Foo`) -- just parse a keyword `foo`
         let literal = Literal::string(&to_parse_ident(ast.ident));
         let construct = variant.construct(|_, _| quote! {});
-        Ok(quote_spanned! {
+        stream.extend(quote_spanned! {
             ast.ident.span() =>
             __p.expect_keyword(#literal)?;
             Ok(#construct)
-        })
-    } else if has_variable_attr(variant.ast().attrs) {
+        });
+    } else if has_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.
-        Ok(quote_spanned! {
+        stream.extend(quote_spanned! {
             ast.ident.span() =>
             let v = __p.variable()?;
             Ok(v)
-        })
+        });
     } else if has_cast_attr(variant.ast().attrs) {
         // Has the `#[cast]` attribute -- just parse the bindings (comma separated, if needed)
         let build: Vec<TokenStream> = parse_bindings(variant.bindings());
         let construct = variant.construct(field_ident);
-        Ok(quote_spanned! {
+        stream.extend(quote_spanned! {
             ast.ident.span() =>
             __p.mark_as_cast_variant();
             #(#build)*
             Ok(#construct)
-        })
+        });
     } else {
         // Otherwise -- parse `variant(binding0, ..., bindingN)`
         let literal = Literal::string(&to_parse_ident(ast.ident));
         let build: Vec<TokenStream> = parse_bindings(variant.bindings());
         let construct = variant.construct(field_ident);
-        Ok(quote_spanned! {
+        stream.extend(quote_spanned! {
             ast.ident.span() =>
             __p.expect_keyword(#literal)?;
             __p.expect_char('(')?;
             #(#build)*
             __p.skip_trailing_comma();
             __p.expect_char(')')?;
             Ok(#construct)
-        })
+        });
     }
+
+    Ok(stream)
 }
 
 /// When a type is given a formality attribute, we use that to guide parsing:
@@ -144,9 +163,8 @@ fn parse_variant(
 fn parse_variant_with_attr(
     variant: &synstructure::VariantInfo,
     spec: &FormalitySpec,
+    mut stream: TokenStream,
 ) -> syn::Result<TokenStream> {
-    let mut stream = TokenStream::new();
-
     for symbol in &spec.symbols {
         stream.extend(match symbol {
             spec::FormalitySpecSymbol::Field { name, mode } => {

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

@@ -46,7 +46,6 @@ pub enum ConstData {
     Value(ValTree, Ty),
 
     #[variable]
-    #[precedence(1)]
     Variable(Variable),
 }
 

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

@@ -107,7 +107,6 @@ pub enum TyData {
     #[cast]
     PredicateTy(PredicateTy),
     #[variable]
-    #[precedence(1)]
     Variable(Variable),
 }
 

crates/formality-types/src/lib.rs

@@ -16,8 +16,9 @@ formality_core::declare_language! {
             "enum",
             "union",
             "const",
-            "ty",
-            "lt",
+            "true",
+            "false",
+            "static",
         ];
     }
 }