fix: prefer resolving parser alias over declaration

This commit is contained in:
Sebastian Ullrich 2023-06-02 16:29:16 +02:00
parent af6c7cdbe0
commit 97cffd4711
2 changed files with 25 additions and 8 deletions

View file

@ -191,26 +191,31 @@ where
return (stx, stackSz)
processNullaryOrCat (stx : Syntax) := do
match (← elabParserName? stx[0]) with
let ident := stx[0]
let id := ident.getId.eraseMacroScopes
-- run when parser is neither a decl nor a cat
let default := do
if (← Parser.isParserAlias id) then
ensureNoPrec stx
return (← processAlias ident #[])
throwError "unknown parser declaration/category/alias '{id}'"
match (← elabParserName? ident) with
| some (.parser c (isDescr := true)) =>
ensureNoPrec stx
-- `syntax _ :=` at least enforces this
let stackSz := 1
return (mkIdentFrom stx c, stackSz)
| some (.parser c (isDescr := false)) =>
if (← Parser.getParserAliasInfo id).declName == c then
-- prefer parser alias over base declaration because it has more metadata, #2249
return (← default)
ensureNoPrec stx
-- as usual, we assume that people using `Parser` know what they are doing
let stackSz := 1
return (← `(ParserDescr.parser $(quote c)), stackSz)
| some (.category _) =>
processParserCategory stx
| none =>
let id := stx[0].getId.eraseMacroScopes
if (← Parser.isParserAlias id) then
ensureNoPrec stx
processAlias stx[0] #[]
else
throwError "unknown parser declaration/category/alias '{id}'"
| none => default
processSepBy (stx : Syntax) := do
let p ← ensureUnaryOutput <$> withNestedParser do process stx[1]

12
tests/lean/run/2249.lean Normal file
View file

@ -0,0 +1,12 @@
import Lean
macro (name := fooParser) "foo" x:(ppSpace ident)* : term =>
`([$(x.map (Lean.mkIdent ·.getId)),*])
namespace Lean.Parser.Term
macro (name := barParser) "bar" x:(ppSpace ident)* : term =>
`([$(x.map (Lean.mkIdent ·.getId)),*])
variable (a : Nat)
#check foo a -- ok
#check bar a -- ok (used to be: unknown identifier '[anonymous]')