fix: syntax match should not ignore tokens in <|>

leanprover · Oct 17, 2022 · 6cab36f · 6cab36f
1 parent 7d44b71
commit 6cab36f
Show file tree

Hide file tree

Showing 4 changed files with 38 additions and 8 deletions.
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
@@ -168,16 +168,25 @@ where
     let aliasName := id.getId.eraseMacroScopes
     let info ← Parser.getParserAliasInfo aliasName
     addAliasInfo id info
-    let args ← args.mapM (withNestedParser ∘ process)
-    let (args, stackSz) := if let some stackSz := info.stackSz? then
+    let args' ← args.mapM (withNestedParser ∘ process)
+    -- wrap lone string literals in `<|>` in dedicated node (#1275)
+    let args' ← if aliasName == `orelse then  -- TODO: generalize if necessary
+      args.zip args' |>.mapM fun (arg, arg') => do
+        if arg.getNumArgs == 1 && arg[0].isOfKind ``Lean.Parser.Syntax.atom then
+          if let some sym := arg[0][0].isStrLit? then
+            return (← `(ParserDescr.nodeWithAntiquot $(quote sym) $(quote (`token ++ sym)) $(arg'.1)), 1)
+        return arg'
+    else
+      pure args'
+    let (args', stackSz) := if let some stackSz := info.stackSz? then
       if !info.autoGroupArgs then
-        (args.map (·.1), stackSz)
+        (args'.map (·.1), stackSz)
       else
-        (args.map ensureUnaryOutput, stackSz)
+        (args'.map ensureUnaryOutput, stackSz)
     else
-      let (args, stackSzs) := args.unzip
-      (args, stackSzs.foldl (· + ·) 0)
-    let stx ← match args with
+      let (args', stackSzs) := args'.unzip
+      (args', stackSzs.foldl (· + ·) 0)
+    let stx ← match args' with
       | #[]       => Parser.ensureConstantParserAlias aliasName; ``(ParserDescr.const $(quote aliasName))
       | #[p1]     => Parser.ensureUnaryParserAlias aliasName; ``(ParserDescr.unary $(quote aliasName) $p1)
       | #[p1, p2] => Parser.ensureBinaryParserAlias aliasName; ``(ParserDescr.binary $(quote aliasName) $p1 $p2)

diff --git a/tests/lean/1275.lean b/tests/lean/1275.lean
@@ -0,0 +1,12 @@
+import Lean open Lean
+
+syntax "👉" (ident <|> "_") : term
+#check `(👉 $_)
+#eval match Unhygienic.run `(👉 _) with
+  | `(👉 $_:ident) => false
+  | `(👉 _) => true
+  | _ => false
+#eval match Unhygienic.run `(👉 x) with
+  | `(👉 _) => false
+  | `(👉 $_:ident) => true
+  | _ => false
diff --git a/tests/lean/1275.lean.expected.out b/tests/lean/1275.lean.expected.out
@@ -0,0 +1,9 @@
+do
+  let info ← MonadRef.mkInfoFromRefPos
+  let scp ← getCurrMacroScope
+  let mainModule ← getMainModule
+  pure
+      { raw :=
+          Syntax.node2 info `term👉__ (Syntax.atom info "👉") (?m info scp mainModule).raw } : ?m (TSyntax `term)
+true
+true
diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out
@@ -4,6 +4,6 @@ syntaxPrec.lean:1:18: error: expected ':'
     def «termFoo*_» : Lean.ParserDescr✝ :=
       ParserDescr.node✝ `«termFoo*_» 1022
         (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo")
-          (ParserDescr.binary✝ `orelse (ParserDescr.symbol✝ "*")
+          (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "*" `token.«*» (ParserDescr.symbol✝ "*"))
             ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) ","
               (ParserDescr.symbol✝ ", ") Bool.false✝)))