@@ -3,24 +3,21 @@ module Text.Lexer
3import public Text.Lexer.Core
3import public Text.Lexer.Core
5%default total
5%default total
7||| Recognise a specific character
8||| Recognise a specific character
9is : Char -> Lexer
9is : Char -> Lexer
10is x = pred (==x)
10is x = pred (==x)
12||| Recognise anything but the given character
12||| Recognise anything but the given character
14isNot : Char -> Lexer
13isNot : Char -> Lexer
15isNot x = pred (/=x)
14isNot x = pred (/=x)
17||| Recognise a character case-insensitively
16||| Recognise a character case-insensitively
19like : Char -> Lexer
17like : Char -> Lexer
20like x = pred (\y => toUpper x == toUpper y)
18like x = pred (\y => toUpper x == toUpper y)
22||| Recognise anything but the given character case-insensitively
20||| Recognise anything but the given character case-insensitively
24notLike : Char -> Lexer
21notLike : Char -> Lexer
25notLike x = pred (\y => toUpper x /= toUpper y)
22notLike x = pred (\y => toUpper x /= toUpper y)
@@ -40,38 +37,32 @@ approx str = case map like (unpack str) of
41||| Recognise a lexer or recognise no input. This is not guaranteed
38||| Recognise a lexer or recognise no input. This is not guaranteed
42||| to consume input
39||| to consume input
44opt : Lexer -> Recognise False
40opt : Lexer -> Recognise False
45opt l = l <|> empty
41opt l = l <|> empty
47||| Recognise a sequence of at least one sub-lexers
43||| Recognise a sequence of at least one sub-lexers
49some : Lexer -> Lexer
44some : Lexer -> Lexer
50some l = l <+> opt (some l)
45some l = l <+> opt (some l)
52||| Recognise a sequence of at zero or more sub-lexers. This is not
47||| Recognise a sequence of at zero or more sub-lexers. This is not
53||| guaranteed to consume input
48||| guaranteed to consume input
55many : Lexer -> Recognise False
49many : Lexer -> Recognise False
56many l = opt (some l)
50many l = opt (some l)
58||| Recognise the first matching lexer from a Foldable. Always consumes input
52||| Recognise the first matching lexer from a Foldable. Always consumes input
59||| if one of the options succeeds. Fails if the foldable is empty.
53||| if one of the options succeeds. Fails if the foldable is empty.
61choice : Foldable t => t Lexer -> Lexer
54choice : Foldable t => t Lexer -> Lexer
62choice xs = foldr (<|>) fail xs
55choice xs = foldr (<|>) fail xs
64||| Repeat the sub-lexer `l` zero or more times until the lexer
57||| Repeat the sub-lexer `l` zero or more times until the lexer
65||| `stopBefore` is encountered. `stopBefore` will not be consumed.
58||| `stopBefore` is encountered. `stopBefore` will not be consumed.
66||| Not guaranteed to consume input.
59||| Not guaranteed to consume input.
68manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
60manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
69manyUntil stopBefore l = many (reject stopBefore <+> l)
61manyUntil stopBefore l = many (reject stopBefore <+> l)
71||| Repeat the sub-lexer `l` zero or more times until the lexer
63||| Repeat the sub-lexer `l` zero or more times until the lexer
72||| `stopAfter` is encountered, and consume it. Guaranteed to
64||| `stopAfter` is encountered, and consume it. Guaranteed to
73||| consume if `stopAfter` consumes.
65||| consume if `stopAfter` consumes.
75manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
66manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
76manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
67manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
@@ -79,7 +70,6 @@ manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
79||| encountered.
70||| encountered.
81||| Useful for defining comments.
72||| Useful for defining comments.
83manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
73manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
84manyTill l end = end <|> opt (l <+> manyTill l end)
74manyTill l end = end <|> opt (l <+> manyTill l end)
85%deprecate manyTill
75%deprecate manyTill
@@ -87,21 +77,18 @@ manyTill l end = end <|> opt (l <+> manyTill l end)
88||| Recognise a sub-lexer at least `min` times. Consumes input unless
78||| Recognise a sub-lexer at least `min` times. Consumes input unless
89||| min is zero.
79||| min is zero.
91atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)
80atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)
92atLeast Z l = many l
81atLeast Z l = many l
93atLeast (S min) l = l <+> atLeast min l
82atLeast (S min) l = l <+> atLeast min l
95||| Recognise a sub-lexer at most `max` times. Not guaranteed to
84||| Recognise a sub-lexer at most `max` times. Not guaranteed to
96||| consume input.
85||| consume input.
98atMost : (max : Nat) -> (l : Lexer) -> Recognise False
86atMost : (max : Nat) -> (l : Lexer) -> Recognise False
99atMost Z _ = empty
87atMost Z _ = empty
100atMost (S k) l = atMost k l <+> opt l
88atMost (S k) l = atMost k l <+> opt l
102||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
90||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
103||| if the inputs are out of order. Consumes input unless min is zero.
91||| if the inputs are out of order. Consumes input unless min is zero.
105between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
92between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
106between Z max l = atMost max l
93between Z max l = atMost max l
107between (S min) Z _ = fail
94between (S min) Z _ = fail
@@ -109,166 +96,135 @@ between (S min) (S max) l = l <+> between min max l
110||| Recognise exactly `count` repeated occurrences of a sub-lexer.
97||| Recognise exactly `count` repeated occurrences of a sub-lexer.
111||| Consumes input unless count is zero.
98||| Consumes input unless count is zero.
113exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
99exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
114exactly n l = between n n l
100exactly n l = between n n l
116||| Recognise any character
102||| Recognise any character
118any : Lexer
103any : Lexer
119any = pred (const True)
104any = pred (const True)
121||| Recognise any character if the sub-lexer `l` fails.
106||| Recognise any character if the sub-lexer `l` fails.
123non : (l : Lexer) -> Lexer
107non : (l : Lexer) -> Lexer
124non l = reject l <+> any
108non l = reject l <+> any
126||| Recognise any of the characters in the given string
110||| Recognise any of the characters in the given string
128oneOf : String -> Lexer
111oneOf : String -> Lexer
129oneOf cs = pred (\x => x `elem` unpack cs)
112oneOf cs = pred (\x => x `elem` unpack cs)
131||| Recognise a character range [`a`-`b`]. Also works in reverse!
114||| Recognise a character range [`a`-`b`]. Also works in reverse!
133range : (start : Char) -> (end : Char) -> Lexer
115range : (start : Char) -> (end : Char) -> Lexer
134range start end = pred (\x => (x >= min start end)
116range start end = pred (\x => (x >= min start end)
135 && (x <= max start end))
117 && (x <= max start end))
137||| Recognise a single digit 0-9
119||| Recognise a single digit 0-9
139digit : Lexer
120digit : Lexer
140digit = pred isDigit
121digit = pred isDigit
142||| Recognise one or more digits
123||| Recognise one or more digits
144digits : Lexer
124digits : Lexer
145digits = some digit
125digits = some digit
147||| Recognise a single hexidecimal digit
127||| Recognise a single hexidecimal digit
149hexDigit : Lexer
128hexDigit : Lexer
150hexDigit = pred isHexDigit
129hexDigit = pred isHexDigit
152||| Recognise one or more hexidecimal digits
131||| Recognise one or more hexidecimal digits
154hexDigits : Lexer
132hexDigits : Lexer
155hexDigits = some hexDigit
133hexDigits = some hexDigit
157||| Recognise a single alpha character
135||| Recognise a single alpha character
159alpha : Lexer
136alpha : Lexer
160alpha = pred isAlpha
137alpha = pred isAlpha
162||| Recognise one or more alpha characters
139||| Recognise one or more alpha characters
164alphas : Lexer
140alphas : Lexer
165alphas = some alpha
141alphas = some alpha
167||| Recognise a lowercase alpha character
143||| Recognise a lowercase alpha character
169lower : Lexer
144lower : Lexer
170lower = pred isLower
145lower = pred isLower
172||| Recognise one or more lowercase alpha characters
147||| Recognise one or more lowercase alpha characters
174lowers : Lexer
148lowers : Lexer
175lowers = some lower
149lowers = some lower
177||| Recognise an uppercase alpha character
151||| Recognise an uppercase alpha character
179upper : Lexer
152upper : Lexer
180upper = pred isUpper
153upper = pred isUpper
182||| Recognise one or more uppercase alpha characters
155||| Recognise one or more uppercase alpha characters
184uppers : Lexer
156uppers : Lexer
185uppers = some upper
157uppers = some upper
187||| Recognise an alphanumeric character
159||| Recognise an alphanumeric character
189alphaNum : Lexer
160alphaNum : Lexer
190alphaNum = pred isAlphaNum
161alphaNum = pred isAlphaNum
192||| Recognise one or more alphanumeric characters
163||| Recognise one or more alphanumeric characters
194alphaNums : Lexer
164alphaNums : Lexer
195alphaNums = some alphaNum
165alphaNums = some alphaNum
197||| Recognise a single whitespace character
167||| Recognise a single whitespace character
199space : Lexer
168space : Lexer
200space = pred isSpace
169space = pred isSpace
202||| Recognise one or more whitespace characters
171||| Recognise one or more whitespace characters
204spaces : Lexer
172spaces : Lexer
205spaces = some space
173spaces = some space
207||| Recognise a single newline sequence. Understands CRLF, CR, and LF
175||| Recognise a single newline sequence. Understands CRLF, CR, and LF
209newline : Lexer
176newline : Lexer
210newline = let crlf = "\r\n" in
177newline = let crlf = "\r\n" in
211 exact crlf <|> oneOf crlf
178 exact crlf <|> oneOf crlf
213||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
180||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
215newlines : Lexer
181newlines : Lexer
216newlines = some newline
182newlines = some newline
218||| Recognise a single non-whitespace, non-alphanumeric character
184||| Recognise a single non-whitespace, non-alphanumeric character
220symbol : Lexer
185symbol : Lexer
221symbol = pred (\x => not (isSpace x || isAlphaNum x))
186symbol = pred (\x => not (isSpace x || isAlphaNum x))
223||| Recognise one or more non-whitespace, non-alphanumeric characters
188||| Recognise one or more non-whitespace, non-alphanumeric characters
225symbols : Lexer
189symbols : Lexer
226symbols = some symbol
190symbols = some symbol
228||| Recognise zero or more occurrences of a sub-lexer between
192||| Recognise zero or more occurrences of a sub-lexer between
229||| delimiting lexers
193||| delimiting lexers
231surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
194surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
232surround start end l = start <+> manyThen end l
195surround start end l = start <+> manyThen end l
234||| Recognise zero or more occurrences of a sub-lexer surrounded
197||| Recognise zero or more occurrences of a sub-lexer surrounded
235||| by the same quote lexer on both sides (useful for strings)
198||| by the same quote lexer on both sides (useful for strings)
237quote : (q : Lexer) -> (l : Lexer) -> Lexer
199quote : (q : Lexer) -> (l : Lexer) -> Lexer
238quote q l = surround q q l
200quote q l = surround q q l
240||| Recognise an escape character (often '\\') followed by a sub-lexer
202||| Recognise an escape character (often '\\') followed by a sub-lexer
242escape : (esc : Char) -> Lexer -> Lexer
203escape : (esc : Char) -> Lexer -> Lexer
243escape esc l = is esc <+> l
204escape esc l = is esc <+> l
245||| Recognise a string literal, including escaped characters.
206||| Recognise a string literal, including escaped characters.
246||| (Note: doesn't yet handle escape sequences such as \123)
207||| (Note: doesn't yet handle escape sequences such as \123)
248stringLit : Lexer
208stringLit : Lexer
249stringLit = quote (is '"') (escape '\\' any <|> any)
209stringLit = quote (is '"') (escape '\\' any <|> any)
251||| Recognise a character literal, including escaped characters.
211||| Recognise a character literal, including escaped characters.
252||| (Note: doesn't yet handle escape sequences such as \123)
212||| (Note: doesn't yet handle escape sequences such as \123)
254charLit : Lexer
213charLit : Lexer
255charLit = let q = '\'' in
214charLit = let q = '\'' in
256 is q <+> (escape '\\' any <|> isNot q) <+> is q
215 is q <+> (escape '\\' any <|> isNot q) <+> is q
258||| Recognise an integer literal (possibly with a '-' prefix)
217||| Recognise an integer literal (possibly with a '-' prefix)
260intLit : Lexer
218intLit : Lexer
261intLit = opt (is '-') <+> digits
219intLit = opt (is '-') <+> digits
263||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
221||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
265hexLit : Lexer
222hexLit : Lexer
266hexLit = approx "0x" <+> hexDigits
223hexLit = approx "0x" <+> hexDigits
268||| Recognise `start`, then recognise all input until a newline is encountered,
225||| Recognise `start`, then recognise all input until a newline is encountered,
269||| and consume the newline. Will succeed if end-of-input is encountered before
226||| and consume the newline. Will succeed if end-of-input is encountered before
270||| a newline.
227||| a newline.
272lineComment : (start : Lexer) -> Lexer
228lineComment : (start : Lexer) -> Lexer
273lineComment start = start <+> manyUntil newline any <+> opt newline
229lineComment start = start <+> manyUntil newline any <+> opt newline
@@ -277,7 +233,6 @@ lineComment start = start <+> manyUntil newline any <+> opt newline
278||| For block comments that don't support nesting (such as C-style comments),
234||| For block comments that don't support nesting (such as C-style comments),
279||| use `surround`.
235||| use `surround`.
281blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
236blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
282blockComment start end = start <+> middle <+> end
237blockComment start end = start <+> middle <+> end