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

feat: extend sepBy syntax syntax

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-09 12:55:02 +01:00
parent fdf5c3280e
commit fd1f74c421
2 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/Lean/Elab/Syntax.lean
View file

@ -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]

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

@ -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