@@ -1,5 +1,7 @@
11module Text.Lexer
22
3+import Data.Bool.Extra
4+
35import public Text.Lexer.Core
46
57%default total
@@ -18,10 +20,19 @@ opt l = l <|> empty
1820non : (l : Lexer) -> Lexer
1921non l = reject l <+> any
2022
21−||| Recognise the first matching lexer in a container. Always consumes input
22−||| if an option succeeds. Fails if the container is empty.
23−choice : Foldable t => t Lexer -> Lexer
24−choice xs = foldr (<|>) fail xs
23+||| Produce recognisers by applying a function to elements of a container, and
24+||| recognise the first match. Consumes input if the function produces consuming
25+||| recognisers. Fails if the container is empty.
26+choiceMap : {c : Bool} ->
27+ Foldable t => (a -> Recognise c) -> t a -> Recognise c
28+choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
29+ f x <|> acc)
30+ fail xs
31+
32+||| Recognise the first matching recogniser in a container. Consumes input if
33+||| recognisers in the list consume. Fails if the container is empty.
34+choice : Foldable t => t (Recognise c) -> Recognise c
35+choice = choiceMap id
2536
2637||| Sequence a list of recognisers. Guaranteed to consume input if the list is
2738||| non-empty and the recognisers consume.