track reduction-kind and give appr preference

resolves the parsing challenges :)

Author: nikomatsakis

crates/formality-core/src/lib.rs

@@ -214,6 +214,14 @@ macro_rules! id {
                 }
             }
 
+            impl From<String> for $n {
+                fn from(s: String) -> Self {
+                    $n {
+                        data: std::sync::Arc::new(s),
+                    }
+                }
+            }
+
             impl std::ops::Deref for $n {
                 type Target = String;
 
@@ -248,10 +256,7 @@ macro_rules! id {
                     scope: &parse::Scope<crate::FormalityLang>,
                     text: &'t str,
                 ) -> parse::ParseResult<'t, Self> {
-                    $crate::parse::Parser::single_variant(scope, text, stringify!($n), |p| {
-                        let string = p.identifier()?;
-                        Ok($n::new(&string))
-                    })
+                    $crate::parse::Parser::identifier(scope, text, stringify!($n))
                 }
             }
 

crates/formality-core/src/parse.rs

@@ -75,21 +75,68 @@ pub struct SuccessfulParse<'t, T> {
     /// given `enum Expr { #[cast] Base(BaseExpr), ... }`, only the reductions
     /// from `BaseExpr` would be recorded, there would be no `Expr::Base`
     /// reduction.
-    reductions: Vec<&'static str>,
+    reductions: Vec<(&'static str, ReductionKind)>,
 
     /// The precedence of this parse, which is derived from the value given
     /// to `parse_variant`.
     precedence: Precedence,
 
-    /// Did this result from parsing an in-scope variable? If so,
-    /// we prefer this parse to other parses that consumed the same set of
-    /// input tokens.
-    is_in_scope_var: bool,
-
     /// The value produced.
     value: T,
 }
 
+#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Default)]
+pub enum ReductionKind {
+    #[default]
+    Normal,
+
+    /// A "cast" reduction is created by invoking `Parser::parse_variant_cast`
+    /// or from the `#[cast]` variants in an enum. This kind of reduction
+    /// represents an "is-a" relationship and does not add semantic meaning.
+    ///
+    /// Cast variants interact differently with ambiguity detection.
+    /// Consider this grammar:
+    ///
+    /// ```text
+    /// X = Y | Z // X has two variants
+    /// Y = A     // Y has 1 variant
+    /// Z = A B   // Z has 1 variant
+    /// A = "a"   // A has 1 variant
+    /// B = "b"   // B has 1 variant
+    /// ```
+    ///
+    /// If you mark the two `X` variants (`X = Y` and `X = Z`)
+    /// as cast variants, then the input `"a b"` is considered
+    /// unambiguous and is parsed as `X = (Z = (A = "a') (B = "b))`
+    /// with no remainder.
+    ///
+    /// If you don't mark those variants as cast variants,
+    /// then we consider this *ambiguous*, because
+    /// it could be that you want `X = (Y = (A = "a"))` with
+    /// a remainder of `"b"`. This is appropriate
+    /// if choosing Y vs Z has different semantic meaning.
+    Cast,
+
+    /// A "variable" reduction results from invoking
+    /// `Parser::parse_variant_variable` to parse an in-scope variable
+    /// or from a `#[variable]` variant in an enum.
+    ///
+    /// In general we prefer to interpret
+    /// an identifier as an in-scope variable if there is one
+    /// (see the test `parser-var-id-ambiguity` for examples).
+    Variable,
+
+    /// A "identifier" reduction results from invoking
+    /// `Parser::parse_variant_identifier` to parse an identifier
+    /// or from parsing a type declared with the `formality_core::id!`
+    /// macro.
+    ///
+    /// In general we prefer to interpret
+    /// an identifier as an in-scope variable if there is one
+    /// (see the test `parser-var-id-ambiguity` for examples).
+    Identifier,
+}
+
 impl<'t, T> SuccessfulParse<'t, T> {
     /// Extract the value parsed and the remaining text,
     /// ignoring the reductions.
@@ -104,7 +151,6 @@ impl<'t, T> SuccessfulParse<'t, T> {
             text: self.text,
             reductions: self.reductions,
             precedence: self.precedence,
-            is_in_scope_var: self.is_in_scope_var,
             value: op(self.value),
         }
     }
@@ -120,7 +166,6 @@ where
             text: term.text,
             reductions: term.reductions,
             precedence: term.precedence,
-            is_in_scope_var: term.is_in_scope_var,
             value: term.value.upcast(),
         }
     }

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

@@ -9,7 +9,9 @@ use crate::{
     Set, Upcast,
 };
 
-use super::{CoreParse, ParseError, ParseResult, Scope, SuccessfulParse, TokenResult};
+use super::{
+    CoreParse, ParseError, ParseResult, ReductionKind, Scope, SuccessfulParse, TokenResult,
+};
 
 mod left_recursion;
 
@@ -151,9 +153,8 @@ where
     scope: &'s Scope<L>,
     start_text: &'t str,
     current_text: &'t str,
-    reductions: Vec<&'static str>,
-    is_cast_variant: bool,
-    is_in_scope_var: bool,
+    reductions: Vec<(&'static str, ReductionKind)>,
+    variant_kind: ReductionKind,
 
     /// A variant is 'committed' when we have seen enough success
     is_committed: bool,
@@ -218,6 +219,20 @@ where
         })
     }
 
+    pub fn identifier(
+        scope: &'s Scope<L>,
+        text: &'t str,
+        nonterminal_name: &'static str,
+    ) -> ParseResult<'t, T>
+    where
+        String: Into<T>,
+    {
+        Self::single_variant(scope, text, nonterminal_name, |p| {
+            p.mark_as_identifier();
+            Ok(p.identifier()?.into())
+        })
+    }
+
     /// Shorthand for `parse_variant` where the parsing operation is to
     /// parse the type `V` and then upcast it to the desired result type.
     /// Also marks the variant as a cast variant.
@@ -289,15 +304,14 @@ where
             Ok(value) => {
                 // Subtle: for cast variants, don't record the variant name in the reduction list,
                 // as it doesn't carry semantic weight. See `mark_as_cast_variant` for more details.
-                if !active_variant.is_cast_variant {
-                    active_variant.reductions.push(variant_name);
-                }
+                active_variant
+                    .reductions
+                    .push((variant_name, active_variant.variant_kind));
 
                 self.successes.push(SuccessfulParse {
                     text: active_variant.current_text,
                     reductions: active_variant.reductions,
                     precedence: variant_precedence,
-                    is_in_scope_var: active_variant.is_in_scope_var,
                     value: value.upcast(),
                 });
                 tracing::trace!("success: {:?}", self.successes.last().unwrap());
@@ -380,14 +394,42 @@ where
     }
 
     fn is_preferable(s_i: &SuccessfulParse<T>, s_j: &SuccessfulParse<T>) -> bool {
-        fn has_prefix<T: Eq>(l1: &[T], l2: &[T]) -> bool {
-            l1.len() > l2.len() && (0..l2.len()).all(|i| l1[i] == l2[i])
+        let mut reductions_i = s_i.reductions.iter().peekable();
+        let mut reductions_j = s_j.reductions.iter().peekable();
+
+        loop {
+            match (reductions_i.peek(), reductions_j.peek()) {
+                // Drop casts from left or right if we see them, as they
+                // are not significant. (See `ReductionKind::Cast`)
+                (Some((_, ReductionKind::Cast)), _) => {
+                    reductions_i.next();
+                }
+                (_, Some((_, ReductionKind::Cast))) => {
+                    reductions_j.next();
+                }
+                (Some((_, ReductionKind::Variable)), Some((_, ReductionKind::Identifier))) => {
+                    // at some point, s_i parsed an in-scope variable and s_j parsed an identifier;
+                    // we tilt in favor of in-scope variables in this kind of case
+                    return true;
+                }
+                (Some(_), None) => {
+                    // s_j is a prefix of s_i -- prefer s_i
+                    return true;
+                }
+                (None, Some(_)) | (None, None) => {
+                    // s_i is a prefix of s_j or they are equal -- do NOT prefer s_i
+                    return false;
+                }
+                (Some(reduction_i), Some(reduction_j)) => {
+                    if reduction_i == reduction_j {
+                        reductions_i.next();
+                        reductions_j.next();
+                    } else {
+                        return false;
+                    }
+                }
+            }
         }
-
-        has_prefix(&s_i.reductions, &s_j.reductions)
-            || (s_i.is_in_scope_var
-                && !s_j.is_in_scope_var
-                && skip_whitespace(s_i.text) == skip_whitespace(s_j.text))
     }
 }
 
@@ -403,8 +445,7 @@ where
             start_text,
             current_text: start_text,
             reductions: vec![],
-            is_cast_variant: false,
-            is_in_scope_var: false,
+            variant_kind: ReductionKind::default(),
             is_committed: true,
         }
     }
@@ -470,45 +511,22 @@ where
         self.current_text = skip_trailing_comma(self.current_text);
     }
 
-    /// Marks this variant as an cast variant,
-    /// which means there is no semantic difference
-    /// between the thing you parsed and the reduced form.
-    /// We do this automatically for enum variants marked
-    /// as `#[cast]` or calls to `parse_variant_cast`.
-    ///
-    /// Cast variants interact differently with ambiguity detection.
-    /// Consider this grammar:
-    ///
-    /// ```text
-    /// X = Y | Z // X has two variants
-    /// Y = A     // Y has 1 variant
-    /// Z = A B   // Z has 1 variant
-    /// A = "a"   // A has 1 variant
-    /// B = "b"   // B has 1 variant
-    /// ```
-    ///
-    /// If you mark the two `X` variants (`X = Y` and `X = Z`)
-    /// as cast variants, then the input `"a b"` is considered
-    /// unambiguous and is parsed as `X = (Z = (A = "a') (B = "b))`
-    /// with no remainder.
-    ///
-    /// If you don't mark those variants as cast variants,
-    /// then we consider this *ambiguous*, because
-    /// it could be that you want `X = (Y = (A = "a"))` with
-    /// a remainder of `"b"`. This is appropriate
-    /// if choosing Y vs Z has different semantic meaning.
+    /// Marks this variant as an cast variant.
+    /// See [`ReductionKind::Cast`].
     pub fn mark_as_cast_variant(&mut self) {
-        self.is_cast_variant = true;
+        self.variant_kind = ReductionKind::Cast;
     }
 
     /// Indicates that this variant is parsing *only* an in-scope variable.
-    /// We have special treatment for disambiguation such that if a variant marked
-    /// as parsing an "in-scope variable" and some other variant both consume the
-    /// same part of the input string, we prefer the variable. This method is automatically
-    /// invoked on `#[variable]` variants by the generated parser code and you generally
-    /// wouldn't want to call it yourself.
+    /// See [`ReducgionKind::Variable`].
     pub fn mark_as_in_scope_var(&mut self) {
-        self.is_in_scope_var = true;
+        self.variant_kind = ReductionKind::Variable;
+    }
+
+    /// Indicates that this variant is parsing *only* an identifier.
+    /// See [`ReducgionKind::Identifier`].
+    pub fn mark_as_identifier(&mut self) {
+        self.variant_kind = ReductionKind::Identifier;
     }
 
     /// Expect *exactly* the given text (after skipping whitespace)
@@ -598,8 +616,7 @@ where
             current_text: self.current_text,
             reductions: vec![],
             scope: self.scope,
-            is_cast_variant: false,
-            is_in_scope_var: false,
+            variant_kind: ReductionKind::default(),
             is_committed: true,
         };
 
@@ -659,8 +676,7 @@ where
             start_text: self.start_text,
             current_text: self.current_text,
             reductions: vec![],
-            is_cast_variant: false,
-            is_in_scope_var: false,
+            variant_kind: ReductionKind::default(),
             is_committed: true,
         };
         let result = op(&mut av);
@@ -890,7 +906,6 @@ where
             text,
             reductions,
             precedence: _,
-            is_in_scope_var: _,
             value,
         } = left_recursion::recurse(self.current_state(), || op(self.scope, self.current_text))?;
 

tests/parser_var_id_ambiguity.rs

@@ -147,19 +147,20 @@ fn parse_assoc() {
 /// and then integrate that into the type, but we could also parse
 /// P as a type itself.
 #[test]
-#[should_panic] // FIXME
 fn parse_apply() {
     let value: Binder<Ty> = ptt::term("<perm P> P i32");
     expect_test::expect![[r#"
         Binder {
             kinds: [
-                Ty,
+                Perm,
             ],
-            term: Assoc(
+            term: Apply(
+                Variable(
+                    ^perm0_0,
+                ),
                 Id(
                     i32,
                 ),
-                T,
             ),
         }
     "#]]
@@ -171,7 +172,6 @@ fn parse_apply() {
 /// and then integrate that into the type, but we could also parse
 /// P as a type itself.
 #[test]
-#[should_panic] // FIXME
 fn parse_parameter() {
     let value: Binder<Parameter> = ptt::term("<perm P> P");
     expect_test::expect![[r#"