add `choice` combinator for Lexers
The argument to `choice` must be a non-empty `List Lexer`.
commit0e867348cd5634369ac72085533d94135350a4eb
authorMichael Morgan <michael.morgan@mind-over-data.com>
dateSat 26 Aug 2017, 11:05 (9 years ago)
parent0b78de1
libs/contrib/Text/Lexer.idr+6
@@ -59,6 +59,12 @@ export
5959many : Lexer -> Recognise False
6060many l = some l <|> Empty
6161
62+||| Recognize the first matching lexer from a non-empty list.
63+export
64+choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
65+choice (x :: []) = x
66+choice (x :: xs@(_ :: _)) = x <|> choice xs
67+
6268||| Recognise many instances of `l` until an instance of `end` is
6369||| encountered.
6470|||