diff --git a/src/Lean/Elab/MacroArgUtil.lean b/src/Lean/Elab/MacroArgUtil.lean index 6b051e4dd3..4f605981a2 100644 --- a/src/Lean/Elab/MacroArgUtil.lean +++ b/src/Lean/Elab/MacroArgUtil.lean @@ -45,8 +45,7 @@ where mkSplicePat (kind : SyntaxNodeKind) (stx : TSyntax `stx) (id : Term) (suffix : String) : CommandElabM Term := return ⟨mkNullNode #[mkAntiquotSuffixSpliceNode kind (← mkAntiquotNode stx id) suffix]⟩ mkAntiquotNode : TSyntax `stx → Term → CommandElabM Term - | `(stx| ($stx)), term => mkAntiquotNode stx term - | `(stx| $id:ident$[:$p:prec]?), term => do + | `(stx| $id:ident$[:$_]?), term => do let kind ← match (← Elab.Term.resolveParserName id) with | [(`Lean.Parser.ident, _)] => pure identKind | [(`Lean.Parser.Term.ident, _)] => pure identKind @@ -63,7 +62,18 @@ where else throwError "unknown parser declaration/category/alias '{id}'" pure ⟨Syntax.mkAntiquotNode kind term⟩ - | stx, term => + | stx, term => do + -- can't match against `` `(stx| ($stxs*)) `` as `*` is interpreted as the `stx` operator + if stx.raw.isOfKind ``Parser.Syntax.paren then + -- translate argument `v:(p1 ... pn)` where all but one `pi` produce zero nodes to + -- `v:pi` using that single `pi` + let nonNullaryNodes ← stx.raw[1].getArgs.filterM fun + | `(stx| $id:ident$[:$_]?) | `(stx| $id:ident($_)) => do + let info ← Parser.getParserAliasInfo id.getId + return info.stackSz? != some 0 + | _ => return true + if let #[stx] := nonNullaryNodes then + return (← mkAntiquotNode ⟨stx⟩ term) pure ⟨Syntax.mkAntiquotNode Name.anonymous term (isPseudoKind := true)⟩ end Lean.Elab.Command diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index fa19ed8891..80abaea491 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -19,17 +19,17 @@ open Lean.PrettyPrinter.Parenthesizer open Lean.PrettyPrinter.Formatter builtin_initialize - register_parser_alias "ws" checkWsBefore { stackSz? := none } - register_parser_alias "noWs" checkNoWsBefore { stackSz? := none } - register_parser_alias "linebreak" checkLinebreakBefore { stackSz? := none } + register_parser_alias "ws" checkWsBefore { stackSz? := some 0 } + register_parser_alias "noWs" checkNoWsBefore { stackSz? := some 0 } + register_parser_alias "linebreak" checkLinebreakBefore { stackSz? := some 0 } register_parser_alias (kind := numLitKind) "num" numLit register_parser_alias (kind := strLitKind) "str" strLit register_parser_alias (kind := charLitKind) "char" charLit register_parser_alias (kind := nameLitKind) "name" nameLit register_parser_alias (kind := scientificLitKind) "scientific" scientificLit register_parser_alias (kind := identKind) "ident" ident - register_parser_alias "colGt" checkColGt { stackSz? := none } - register_parser_alias "colGe" checkColGe { stackSz? := none } + register_parser_alias "colGt" checkColGt { stackSz? := some 0 } + register_parser_alias "colGe" checkColGe { stackSz? := some 0 } register_parser_alias lookahead { stackSz? := some 0 } register_parser_alias atomic { stackSz? := none } register_parser_alias many diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index bf5e0c35d1..e365fe6bc6 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -181,17 +181,17 @@ macro_rules builtin_initialize register_parser_alias group { autoGroupArgs := false } - register_parser_alias ppHardSpace { stackSz? := none } - register_parser_alias ppSpace { stackSz? := none } - register_parser_alias ppLine { stackSz? := none } + register_parser_alias ppHardSpace { stackSz? := some 0 } + register_parser_alias ppSpace { stackSz? := some 0 } + register_parser_alias ppLine { stackSz? := some 0 } register_parser_alias ppGroup { stackSz? := none } register_parser_alias ppRealGroup { stackSz? := none } register_parser_alias ppRealFill { stackSz? := none } register_parser_alias ppIndent { stackSz? := none } register_parser_alias ppDedent { stackSz? := none } - register_parser_alias ppAllowUngrouped { stackSz? := none } register_parser_alias ppDedentIfGrouped { stackSz? := none } - register_parser_alias ppHardLineUnlessUngrouped { stackSz? := none } + register_parser_alias ppAllowUngrouped { stackSz? := some 0 } + register_parser_alias ppHardLineUnlessUngrouped { stackSz? := some 0 } end Parser diff --git a/tests/lean/run/1274.lean b/tests/lean/run/1274.lean new file mode 100644 index 0000000000..f80dd81b1f --- /dev/null +++ b/tests/lean/run/1274.lean @@ -0,0 +1,2 @@ +macro "👉" t:(ppSpace ident) : term => `($t) +macro "👈" t:(lookahead(term) ident ppSpace) : term => `($t)