@@ -21,6 +21,14 @@ optional : (p : Grammar tok c a) ->
2121 Grammar tok False (Maybe a)
2222optional p = option Nothing (map Just p)
2323
24+||| Try to parse one thing or the other, producing a value that indicates
25+||| which option succeeded. If both would succeed, the left option
26+||| takes priority.
27+choose : (l : Grammar tok c1 a) ->
28+ (r : Grammar tok c2 b) ->
29+ Grammar tok (c1 && c2) (Either a b)
30+choose l r = map Left l <|> map Right r
31+
2432||| Try each grammar in a container until the first one succeeds.
2533||| Fails if the container is empty.
2634choice : {c : Bool} ->
@@ -47,6 +55,56 @@ some' : (p : Grammar tok True a) ->
4755 Grammar tok True (xs : List a ** NonEmpty xs)
4856some' p = pure (!p :: !(many p) ** IsNonEmpty)
4957
58+mutual
59+ ||| Parse one or more instances of `p` until `end` succeeds, returning the
60+ ||| list of values from `p`. Guaranteed to consume input.
61+ someTill : {c : Bool} ->
62+ (end : Grammar tok c e) ->
63+ (p : Grammar tok True a) ->
64+ Grammar tok True (List a)
65+ someTill {c} end p = do x <- p
66+ seq (manyTill end p)
67+ (\xs => pure (x :: xs))
68+
69+ ||| Parse zero or more instances of `p` until `end` succeeds, returning the
70+ ||| list of values from `p`. Guaranteed to consume input if `end` consumes.
71+ manyTill : {c : Bool} ->
72+ (end : Grammar tok c e) ->
73+ (p : Grammar tok True a) ->
74+ Grammar tok c (List a)
75+ manyTill {c} end p = rewrite sym (andTrueNeutral c) in
76+ map (const []) end <|> someTill end p
77+
78+||| Parse one or more instances of `p` until `end` succeeds, returning the
79+||| list of values from `p`, along with a proof that the resulting list is
80+||| non-empty.
81+someTill' : {c : Bool} ->
82+ (end : Grammar tok c a) ->
83+ (p : Grammar tok True a) ->
84+ Grammar tok True (xs : List a ** NonEmpty xs)
85+someTill' end p
86+ = do x <- p
87+ seq (manyTill end p)
88+ (\xs => pure (x :: xs ** IsNonEmpty))
89+
90+mutual
91+ ||| Parse one or more instance of `skip` until `p` is encountered,
92+ ||| returning its value.
93+ afterSome : (skip : Grammar tok True s) ->
94+ (p : Grammar tok c a) ->
95+ Grammar tok True a
96+ afterSome skip p = do skip
97+ afterMany skip p
98+
99+ ||| Parse zero or more instance of `skip` until `p` is encountered,
100+ ||| returning its value.
101+ afterMany : {c : Bool} ->
102+ (skip : Grammar tok True s) ->
103+ (p : Grammar tok c a) ->
104+ Grammar tok c a
105+ afterMany {c} skip p = rewrite sym (andTrueNeutral c) in
106+ p <|> afterSome skip p
107+
50108||| Parse one or more things, each separated by another thing.
51109sepBy1 : {c : Bool} ->
52110 (sep : Grammar tok True s) ->
@@ -73,6 +131,54 @@ sepBy1' {c} sep p
73131 seq p (\x => do xs <- many (sep *> p)
74132 pure (x :: xs ** IsNonEmpty))
75133
134+||| Parse one or more instances of `p` separated by and optionally terminated by
135+||| `sep`.
136+sepEndBy1 : {c : Bool} ->
137+ (sep : Grammar tok True s) ->
138+ (p : Grammar tok c a) ->
139+ Grammar tok c (List a)
140+sepEndBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
141+ sepBy1 sep p <* optional sep
142+
143+||| Parse zero or more instances of `p`, separated by and optionally terminated
144+||| by `sep`. Will not match a separator by itself.
145+sepEndBy : (sep : Grammar tok True s) ->
146+ (p : Grammar tok c a) ->
147+ Grammar tok False (List a)
148+sepEndBy sep p = option [] $ sepEndBy1 sep p
149+
150+||| Parse zero or more instances of `p`, separated by and optionally terminated
151+||| by `sep`, returning the parsed items and a proof that the resulting list
152+||| is non-empty.
153+sepEndBy1' : {c : Bool} ->
154+ (sep : Grammar tok True s) ->
155+ (p : Grammar tok c a) ->
156+ Grammar tok c (xs : List a ** NonEmpty xs)
157+sepEndBy1' {c} sep p = rewrite sym (orFalseNeutral c) in
158+ sepBy1' sep p <* optional sep
159+
160+||| Parse one or more instances of `p`, separated and terminated by `sep`.
161+endBy1 : {c : Bool} ->
162+ (sep : Grammar tok True s) ->
163+ (p : Grammar tok c a) ->
164+ Grammar tok True (List a)
165+endBy1 {c} sep p = some $ rewrite sym (orTrueTrue c) in
166+ p <* sep
167+
168+endBy : (sep : Grammar tok True s) ->
169+ (p : Grammar tok c a) ->
170+ Grammar tok False (List a)
171+endBy sep p = option [] $ endBy1 sep p
172+
173+||| Parse zero or more instances of `p`, separated and terminated by `sep`,
174+||| returning the parsed items and a proof that the resulting list is non-empty.
175+endBy1' : {c : Bool} ->
176+ (sep : Grammar tok True s) ->
177+ (p : Grammar tok c a) ->
178+ Grammar tok True (xs : List a ** NonEmpty xs)
179+endBy1' {c} sep p = some' $ rewrite sym (orTrueTrue c) in
180+ p <* sep
181+
76182||| Parse an instance of `p` that is between `left` and `right`.
77183between : (left : Grammar tok True l) ->
78184 (right : Grammar tok True r) ->