From fd1f74c421356c49e82dd059bc38ca41ca513ec0 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 9 Dec 2020 12:55:02 +0100 Subject: [PATCH] feat: extend `sepBy` syntax syntax --- src/Lean/Elab/Syntax.lean | 17 +++++++++++++++++ src/Lean/Parser/Syntax.lean | 2 ++ 2 files changed, 19 insertions(+) diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 5fa960ef79..0eb6107de7 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Elab.Command +import Lean.Parser.Syntax namespace Lean.Elab.Term /- @@ -90,6 +91,22 @@ partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := withRef s let d₁ ← withNestedParser $ toParserDescrAux stx[2] let d₂ ← withNestedParser $ toParserDescrAux stx[4] `(ParserDescr.binary $(quote aliasName) $d₁ $d₂) + else if kind == `Lean.Parser.Syntax.sepBy then + let p ← withNestedParser $ toParserDescrAux stx[1] + let sep := stx[3] + let psep ← if stx[4].isNone then `(ParserDescr.symbol $sep) else toParserDescrAux stx[4][1] + let allowTrailingSep := !stx[5].isNone + --`(ParserDescr.sepBy $p $sep $psep $(quote allowTrailingSep)) + let sepBy := if allowTrailingSep then `sepByT else `sepBy + `(ParserDescr.binary $(quote sepBy) $p $psep) + else if kind == `Lean.Parser.Syntax.sepBy1 then + let p ← withNestedParser $ toParserDescrAux stx[1] + let sep := stx[3] + let psep ← if stx[4].isNone then `(ParserDescr.symbol $sep) else toParserDescrAux stx[4][1] + let allowTrailingSep := !stx[5].isNone + --`(ParserDescr.sepBy1 $p $sep $psep $(quote allowTrailingSep)) + let sepBy := if allowTrailingSep then `sepBy1T else `sepBy1 + `(ParserDescr.binary $(quote sepBy) $p $psep) else if kind == `Lean.Parser.Syntax.cat then let cat := stx[0].getId.eraseMacroScopes let prec? : Option Nat := expandOptPrecedence stx[1] diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 52a05056df..ef5d19a3c5 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -29,6 +29,8 @@ namespace Syntax @[builtinSyntaxParser] def cat := parser! ident >> optPrecedence @[builtinSyntaxParser] def unary := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")" @[builtinSyntaxParser] def binary := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ", " >> many1 syntaxParser >> ")" +@[builtinSyntaxParser] def sepBy := parser! "sepBy(" >> many1 syntaxParser >> ", " >> strLit >> optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep") >> ")" +@[builtinSyntaxParser] def sepBy1 := parser! "sepBy1(" >> many1 syntaxParser >> ", " >> strLit >> optional (", " >> many1 syntaxParser) >> optional (", " >> nonReservedSymbol "allowTrailingSep") >> ")" @[builtinSyntaxParser] def atom := parser! strLit @[builtinSyntaxParser] def nonReserved := parser! "&" >> strLit