@@ -5,19 +5,37 @@ import public Text.Lexer.Core
55%default total
66%access export
77
8−||| Recognise a specific character
8+||| Recognise any character
9+any : Lexer
10+any = pred (const True)
11+
12+||| Recognise a lexer or recognise no input. This is not guaranteed
13+||| to consume input
14+opt : Lexer -> Recognise False
15+opt l = l <|> empty
16+
17+||| Recognise any character if the sub-lexer `l` fails.
18+non : (l : Lexer) -> Lexer
19+non l = reject l <+> any
20+
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
25+
26+||| Recognise a specific character.
927is : Char -> Lexer
1028is x = pred (==x)
1129
12−||| Recognise anything but the given character
30+||| Recognise anything but the given character.
1331isNot : Char -> Lexer
1432isNot x = pred (/=x)
1533
16−||| Recognise a character case-insensitively
34+||| Recognise a specific character (case-insensitive).
1735like : Char -> Lexer
1836like x = pred (\y => toUpper x == toUpper y)
1937
20−||| Recognise anything but the given character case-insensitively
38+||| Recognise anything but the given character (case-insensitive).
2139notLike : Char -> Lexer
2240notLike x = pred (\y => toUpper x /= toUpper y)
2341
@@ -35,24 +53,24 @@ approx str = case map like (unpack str) of
3553 [] => fail
3654 (x :: xs) => concat (x :: xs)
3755
38−||| Recognise a lexer or recognise no input. This is not guaranteed
39−||| to consume input
40−opt : Lexer -> Recognise False
41−opt l = l <|> empty
56+||| Recognise any of the characters in the given string
57+oneOf : String -> Lexer
58+oneOf cs = pred (\x => x `elem` unpack cs)
4259
43−||| Recognise a sequence of at least one sub-lexers
44−some : Lexer -> Lexer
45−some l = l <+> opt (some l)
60+||| Recognise a character range [`a`-`b`]. Also works in reverse!
61+range : (start : Char) -> (end : Char) -> Lexer
62+range start end = pred (\x => (x >= min start end)
63+ && (x <= max start end))
4664
47−||| Recognise a sequence of at zero or more sub-lexers. This is not
48−||| guaranteed to consume input
49−many : Lexer -> Recognise False
50−many l = opt (some l)
65+mutual
66+ ||| Recognise a sequence of at least one sub-lexers
67+ some : Lexer -> Lexer
68+ some l = l <+> many l
5169
52−||| Recognise the first matching lexer from a Foldable. Always consumes input
53−||| if one of the options succeeds. Fails if the foldable is empty.
54−choice : Foldable t => t Lexer -> Lexer
55−choice xs = foldr (<|>) fail xs
70+ ||| Recognise a sequence of at zero or more sub-lexers. This is not
71+ ||| guaranteed to consume input
72+ many : Lexer -> Recognise False
73+ many l = opt (some l)
5674
5775||| Repeat the sub-lexer `l` zero or more times until the lexer
5876||| `stopBefore` is encountered. `stopBefore` will not be consumed.
@@ -99,23 +117,6 @@ between (S min) (S max) l = l <+> between min max l
99117exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
100118exactly n l = between n n l
101119
102−||| Recognise any character
103−any : Lexer
104−any = pred (const True)
105−
106−||| Recognise any character if the sub-lexer `l` fails.
107−non : (l : Lexer) -> Lexer
108−non l = reject l <+> any
109−
110−||| Recognise any of the characters in the given string
111−oneOf : String -> Lexer
112−oneOf cs = pred (\x => x `elem` unpack cs)
113−
114−||| Recognise a character range [`a`-`b`]. Also works in reverse!
115−range : (start : Char) -> (end : Char) -> Lexer
116−range start end = pred (\x => (x >= min start end)
117− && (x <= max start end))
118−
119120||| Recognise a single digit 0-9
120121digit : Lexer
121122digit = pred isDigit