git.iko.soy/Idris-dev
on master help sign in
Text.Lexer, Text.Parser: add `choiceMap`
59ac463Michael Morgan
libs/contrib/Text/Lexer.idr+15−4
compare with master
unifiedsplit
@@ -1,5 +1,7 @@
1module Text.Lexer
1module Text.Lexer
2
2
3+import Data.Bool.Extra
4+
3import public Text.Lexer.Core
5import public Text.Lexer.Core
4
6
5%default total
7%default total
@@ -18,10 +20,19 @@ opt l = l <|> empty
18non : (l : Lexer) -> Lexer
20non : (l : Lexer) -> Lexer
19non l = reject l <+> any
21non l = reject l <+> any
20
22
21−||| Recognise the first matching lexer in a container. Always consumes input
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
22−||| if an option succeeds. Fails if the container is empty.
25+||| recognisers. Fails if the container is empty.
23−choice : Foldable t => t Lexer -> Lexer
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)
24−choice xs = foldr (<|>) fail xs
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
25
36
26||| Sequence a list of recognisers. Guaranteed to consume input if the list is
37||| Sequence a list of recognisers. Guaranteed to consume input if the list is
27||| non-empty and the recognisers consume.
38||| non-empty and the recognisers consume.
libs/contrib/Text/Parser.idr+13−5
@@ -29,14 +29,22 @@ choose : (l : Grammar tok c1 a) ->
29 Grammar tok (c1 && c2) (Either a b)
29 Grammar tok (c1 && c2) (Either a b)
30choose l r = map Left l <|> map Right r
30choose l r = map Left l <|> map Right r
31
31
32+||| Produce a grammar by applying a function to each element of a container,
33+||| then try each resulting grammar until the first one succeeds. Fails if the
34+||| container is empty.
35+choiceMap : {c : Bool} ->
36+ (a -> Grammar tok c b) ->
37+ Foldable t => t a ->
38+ Grammar tok c b
39+choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
40+ f x <|> acc)
41+ (fail "No more options") xs
42+
32||| Try each grammar in a container until the first one succeeds.
43||| Try each grammar in a container until the first one succeeds.
33||| Fails if the container is empty.
44||| Fails if the container is empty.
34−choice : {c : Bool} ->
35− Foldable t => t (Grammar tok c a) ->
45+choice : Foldable t => t (Grammar tok c a) ->
36 Grammar tok c a
46 Grammar tok c a
37−choice {c} xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
47+choice = choiceMap id
38− x <|> acc)
39− (fail "No more options") xs
40
48
41mutual
49mutual
42 ||| Parse one or more things
50 ||| Parse one or more things