max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: align stx precedence in syntax to the new one in macro

Browse source
This commit is contained in:
Sebastian Ullrich 2021-08-18 13:16:36 +02:00 • committed by Leonardo de Moura
parent 97764b58b2
commit e632c14f3f
3 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser/Syntax.lean
View file

@ -69,7 +69,7 @@ def optKind : Parser := optional ("(" >> nonReservedSymbol "kind" >> ":=" >> ide
def notationItem := ppSpace >> withAntiquot (mkAntiquot "notationItem" `Lean.Parser.Command.notationItem) (strLit <|> identPrec)
@[builtinCommandParser] def «notation» := leading_parser Term.attrKind >> "notation" >> optPrecedence >> optNamedName >> optNamedPrio >> many notationItem >> darrow >> termParser
@[builtinCommandParser] def «macro_rules» := suppressInsideQuot (leading_parser optional docComment >> Term.attrKind >> "macro_rules" >> optKind >> Term.matchAlts)
@[builtinCommandParser] def «syntax» := leading_parser optional docComment >> Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def «syntax» := leading_parser optional docComment >> Term.attrKind >> "syntax " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 (syntaxParser argPrec) >> " : " >> ident
@[builtinCommandParser] def syntaxAbbrev := leading_parser "syntax " >> ident >> " := " >> many1 syntaxParser
@[builtinCommandParser] def syntaxCat := leading_parser "declare_syntax_cat " >> ident
def macroArg := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec

3
tests/lean/syntaxPrec.lean Normal file
View file

@ -0,0 +1,3 @@
syntax "foo" term <|> "bar" term : term -- should not compile
set_option trace.Elab.command true
syntax "foo" ("*" <|> term,+) : term

8
tests/lean/syntaxPrec.lean.expected.out Normal file
View file

@ -0,0 +1,8 @@
syntaxPrec.lean:1:18: error: expected ':'
[Elab.command] syntax "foo"("*" <|> term,+) : term
[Elab.command] @[termParser 1000]
def «termFoo*_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `«termFoo*_» 1022
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo")
(ParserDescr.binary✝ `orelse (ParserDescr.symbol✝ "*")
(ParserDescr.sepBy1✝ (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ") Bool.false✝)))