@@ -107,11 +107,11 @@ export
107107many : Lexer -> Recognise False
108108many l = opt (some l)
109109
110−||| Recognise the first matching lexer from a non-empty list.
110+||| Recognise the first matching lexer from a Foldable. Always consumes input
111+||| if one of the options succeeds. Fails if the foldable is empty.
111112export
112−choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
113−choice (x :: []) = x
114−choice (x :: xs@(_ :: _)) = x <|> choice xs
113+choice : Foldable t => t Lexer -> Lexer
114+choice xs = foldr Alt Fail xs
115115
116116||| Repeat the sub-lexer `l` zero or more times until the lexer
117117||| `stopBefore` is encountered. `stopBefore` will not be consumed.
@@ -137,6 +137,34 @@ manyTill l end = end <|> opt (l <+> manyTill l end)
137137%deprecate manyTill
138138 "Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."
139139
140+||| Recognise a sub-lexer at least `min` times. Consumes input unless
141+||| min is zero.
142+export
143+atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)
144+atLeast Z l = many l
145+atLeast (S min) l = l <+> atLeast min l
146+
147+||| Recognise a sub-lexer at most `max` times. Not guaranteed to
148+||| consume input.
149+export
150+atMost : (max : Nat) -> (l : Lexer) -> Recognise False
151+atMost Z _ = Empty
152+atMost (S k) l = atMost k l <+> opt l
153+
154+||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
155+||| if the inputs are out of order. Consumes input unless min is zero.
156+export
157+between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
158+between Z max l = atMost max l
159+between (S min) Z _ = Fail
160+between (S min) (S max) l = l <+> between min max l
161+
162+||| Recognise exactly `count` repeated occurrences of a sub-lexer.
163+||| Consumes input unless count is zero.
164+export
165+exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
166+exactly n l = between n n l
167+
140168||| Recognise any character
141169export
142170any : Lexer