From 6b53700d6072410529c041adbedcd93eabff9abe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 13 Apr 2019 08:15:56 -0700
Subject: [PATCH] test(tests/playground/parser/test1): improve

---
 tests/playground/parser/parser.lean |  3 +++
 tests/playground/parser/test1.lean  | 27 +++++++++++++++++++--------
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/tests/playground/parser/parser.lean b/tests/playground/parser/parser.lean
index 32f27197bd..e962d12b09 100644
--- a/tests/playground/parser/parser.lean
+++ b/tests/playground/parser/parser.lean
@@ -707,6 +707,9 @@ def strLitFn : BasicParserFn
 @[inline] def strLit : BasicParser :=
 { fn := numberFn }
 
+instance string2basic : HasCoe String BasicParser :=
+⟨symbol⟩
+
 def mkFrontendConfig (filename input : String) : FrontendConfig :=
 { filename := filename,
   input    := input,
diff --git a/tests/playground/parser/test1.lean b/tests/playground/parser/test1.lean
index 4341215277..4338507344 100644
--- a/tests/playground/parser/test1.lean
+++ b/tests/playground/parser/test1.lean
@@ -3,16 +3,24 @@ open Parser
 local infix ` ; `:10 := Parser.andthen
 local infix ` || `:5 := Parser.orelse
 
-def mkTestKind : IO SyntaxNodeKind := nextKind `test
-@[init mkTestKind] constant testKind : SyntaxNodeKind := default _
+def mkNumPairKind : IO SyntaxNodeKind := nextKind `numPair
+@[init mkNumPairKind] constant numPairKind : SyntaxNodeKind := default _
+
+def mkNumSetKind : IO SyntaxNodeKind := nextKind `numSet
+@[init mkNumSetKind] constant numSetKind : SyntaxNodeKind := default _
 
 @[inline2]
 def numPair : BasicParser :=
-node testKind $
-  symbol "("; number; symbol ","; number; symbol ")"
+node numPairKind $
+  "("; number; ","; number; ")"
 
-def numPairs : BasicParser :=
-many numPair
+@[inline2]
+def numSet : BasicParser :=
+node numSetKind $
+  "{"; sepBy number ","; "}"
+
+def testParser : BasicParser :=
+many (numPair || numSet)
 
 @[noinline] def test (p : BasicParser) (s : String) : IO Unit :=
 match p.run s with
@@ -21,8 +29,11 @@ match p.run s with
 
 def mkNumPairString : Nat → String → String
 | 0     s := s
-| (n+1) s := mkNumPairString n (s ++ "(" ++ toString n ++ ", " ++ toString n ++ ") -- comment\n")
+| (n+1) s := mkNumPairString n $
+  s ++ "{} /- /- comment2 -/ -/ "
+  ++ "{" ++ toString n ++ "," ++ toString (n+1) ++ ",   " ++ toString (n+2) ++ "}"
+  ++ "(" ++ toString n ++ ", " ++ toString n ++ ") -- comment\n"
 
 def main (xs : List String) : IO Unit :=
 let s := mkNumPairString xs.head.toNat "" in
-test numPairs s
+test testParser s