From 68e8faeef1c94b35614e8a35479039977c58cb0c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 13 Apr 2019 07:56:35 -0700
Subject: [PATCH] test(tests/playground/parser/parser): add `sepBy` and
 `sepBy1`

---
 tests/playground/parser/parser.lean | 51 +++++++++++++++++++++++++++--
 1 file changed, 49 insertions(+), 2 deletions(-)

diff --git a/tests/playground/parser/parser.lean b/tests/playground/parser/parser.lean
index 73b11a477a..0d3fbf3dbf 100644
--- a/tests/playground/parser/parser.lean
+++ b/tests/playground/parser/parser.lean
@@ -140,8 +140,8 @@ match d with
 λ s d,
   let iniSz  := d.stackSize in
   let iniPos := d.pos in
-  let d := p s d in
-  let d := if d.hasError then d.restore iniSz iniPos else d in
+  let d      := p s d in
+  let d      := if d.hasError then d.restore iniSz iniPos else d in
   d.mkNode nullKind iniSz
 
 def ParserData.mkError (d : ParserData) (msg : String) : ParserData :=
@@ -166,6 +166,47 @@ d.mkError "end of input"
   let d := manyAux p s d in
   d.mkNode nullKind iniSz
 
+@[specialize] private partial def sepByFnAux (p : ParserFn) (sep : ParserFn) (allowTrailingSep : Bool) (iniSz : Nat) : Bool → ParserFn
+| pOpt s d :=
+  let sz  := d.stackSize in
+  let pos := d.pos in
+  let d   := p s d in
+  if d.hasError then
+    let d := d.restore sz pos in
+    if pOpt then
+      d.mkNode nullKind iniSz
+    else
+      -- append `Syntax.missing` to make clear that List is incomplete
+      let d := d.pushSyntax Syntax.missing in
+      d.mkNode nullKind iniSz
+  else
+    let sz  := d.stackSize in
+    let pos := d.pos in
+    let d   := sep s d in
+    if d.hasError then
+      let d := d.restore sz pos in
+      d.mkNode nullKind iniSz
+    else
+      sepByFnAux allowTrailingSep s d
+
+@[specialize] def sepByFn (allowTrailingSep : Bool) (p : ParserFn) (sep : ParserFn) : ParserFn
+| s d :=
+  let iniSz := d.stackSize in
+  sepByFnAux p sep allowTrailingSep iniSz true s d
+
+@[specialize] def sepBy1Fn (allowTrailingSep : Bool) (p : ParserFn) (sep : ParserFn) : ParserFn
+| s d :=
+  let iniSz := d.stackSize in
+  sepByFnAux p sep allowTrailingSep iniSz false s d
+
+@[noinline] def sepByInfo (p sep : ParserInfo) : ParserInfo :=
+{ updateTokens := sep.updateTokens ∘ p.updateTokens,
+  firstToken   := none }
+
+@[noinline] def sepBy1Info (p sep : ParserInfo) : ParserInfo :=
+{ updateTokens := sep.updateTokens ∘ p.updateTokens,
+  firstToken   := p.firstToken }
+
 @[specialize] partial def satisfyFn (p : Char → Bool) (errorMsg : String := "unexpected character") : ParserFn
 | s d :=
   let i := d.pos in
@@ -534,6 +575,12 @@ mapParser noFirstTokenInfo optionalFn
 @[inline] def many1 {ρ : Type} [ParserFnLift ρ] (p : AbsParser ρ) : AbsParser ρ :=
 andthen p (many p)
 
+@[inline] def sepBy {ρ : Type} [ParserFnLift ρ] (p sep : AbsParser ρ) (allowTrailingSep : Bool := false) : AbsParser ρ :=
+mapParser₂ sepByInfo (sepByFn allowTrailingSep) p sep
+
+@[inline] def sepBy1 {ρ : Type} [ParserFnLift ρ] (p sep : AbsParser ρ) (allowTrailingSep : Bool := false) : AbsParser ρ :=
+mapParser₂ sepBy1Info (sepBy1Fn allowTrailingSep) p sep
+
 abbrev BasicParserFn : Type          := EnvParserFn ParserConfig ParserFn
 abbrev BasicParser : Type            := AbsParser BasicParserFn
 abbrev CmdParserFn (ρ : Type) : Type := EnvParserFn ρ (RecParserFn Unit ParserFn)