test(tests/playground/parser1): minor

This commit is contained in:
Leonardo de Moura 2019-06-19 14:17:55 -07:00
parent 401de35b6c
commit 86e1af2066

View file

@ -10,6 +10,10 @@ def mkPairsKind : IO SyntaxNodeKind := nextKind `pairs
@[init mkPairsKind]
constant pairsKind : SyntaxNodeKind := default _
def mkFunKind : IO SyntaxNodeKind := nextKind `fun
@[init mkFunKind]
constant funKind : SyntaxNodeKind := default _
local infixl `>>`:50 := Lean.Parser.andthen
def pairParser : Parser :=
@ -20,10 +24,16 @@ attribute [builtinTestParser] pairParser
def pairsParser : Parser :=
node pairsKind $
"{" >> many testParser >> "}"
"{" >> many1 testParser >> "}"
attribute [builtinTestParser] pairsParser
def functionParser : Parser :=
node funKind $
"fun" >> ident >> "," >> testParser
attribute [builtinTestParser] functionParser
def testParser (input : String) : IO Unit :=
do
env ← mkEmptyEnvironment,
@ -34,4 +44,4 @@ IO.println stx
def main (xs : List String) : IO Unit :=
do
testParser "(10, hello)",
testParser "{ (10, hello) /- comment -/ (20, world) { } { (30, foo) } }"
testParser "{ (10, hello) /- comment -/ (20, world) { fun x, (10, hello) } { (30, foo) } }"