@@ -12,16 +12,19 @@ import public Text.Token
12toTokenMap : List (Lexer, k) -> TokenMap (Token k)
12toTokenMap : List (Lexer, k) -> TokenMap (Token k)
13toTokenMap = map $ \(l, kind) => (l, Tok kind)
13toTokenMap = map $ \(l, kind) => (l, Tok kind)
15−||| Recognise any character
15+||| Recognise any character.
16any : Lexer
17any : Lexer
17any = pred (const True)
18any = pred (const True)
19||| Recognise a lexer or recognise no input. This is not guaranteed
20||| Recognise a lexer or recognise no input. This is not guaranteed
20−||| to consume input
21+||| to consume input.
21−opt : Lexer -> Recognise False
23+opt : (l : Lexer) -> Recognise False
22opt l = l <|> empty
24opt l = l <|> empty
24||| Recognise any character if the sub-lexer `l` fails.
26||| Recognise any character if the sub-lexer `l` fails.
25non : (l : Lexer) -> Lexer
28non : (l : Lexer) -> Lexer
26non l = reject l <+> any
29non l = reject l <+> any
@@ -45,63 +48,75 @@ concat : (xs : List (Recognise c)) -> Recognise (c && isCons xs)
45concat = concatMap id
48concat = concatMap id
47||| Recognise a specific character.
50||| Recognise a specific character.
48−is : Char -> Lexer
52+is : (x : Char) -> Lexer
49is x = pred (==x)
53is x = pred (==x)
51||| Recognise anything but the given character.
55||| Recognise anything but the given character.
52−isNot : Char -> Lexer
57+isNot : (x : Char) -> Lexer
53isNot x = pred (/=x)
58isNot x = pred (/=x)
55||| Recognise a specific character (case-insensitive).
60||| Recognise a specific character (case-insensitive).
56−like : Char -> Lexer
62+like : (x : Char) -> Lexer
57like x = pred (\y => toUpper x == toUpper y)
63like x = pred (\y => toUpper x == toUpper y)
59||| Recognise anything but the given character (case-insensitive).
65||| Recognise anything but the given character (case-insensitive).
60−notLike : Char -> Lexer
67+notLike : (x : Char) -> Lexer
61notLike x = pred (\y => toUpper x /= toUpper y)
68notLike x = pred (\y => toUpper x /= toUpper y)
63||| Recognise a specific string.
70||| Recognise a specific string.
64||| Fails if the string is empty.
71||| Fails if the string is empty.
65−exact : String -> Lexer
73+exact : (str : String) -> Lexer
66exact str = case unpack str of
74exact str = case unpack str of
67 [] => fail
75 [] => fail
68 (x :: xs) => concatMap is (x :: xs)
76 (x :: xs) => concatMap is (x :: xs)
70||| Recognise a specific string (case-insensitive).
78||| Recognise a specific string (case-insensitive).
71||| Fails if the string is empty.
79||| Fails if the string is empty.
72−approx : String -> Lexer
81+approx : (str : String) -> Lexer
73approx str = case unpack str of
82approx str = case unpack str of
74 [] => fail
83 [] => fail
75 (x :: xs) => concatMap like (x :: xs)
84 (x :: xs) => concatMap like (x :: xs)
77−||| Recognise any of the characters in the given string
86+||| Recognise any of the characters in the given string.
78−oneOf : String -> Lexer
88+oneOf : (chars : String) -> Lexer
79−oneOf cs = pred (\x => x `elem` unpack cs)
89+oneOf chars = pred (\x => x `elem` unpack chars)
81−||| Recognise a character range [`a`-`b`]. Also works in reverse!
91+||| Recognise a character range. Also works in reverse!
82range : (start : Char) -> (end : Char) -> Lexer
93range : (start : Char) -> (end : Char) -> Lexer
83range start end = pred (\x => (x >= min start end)
94range start end = pred (\x => (x >= min start end)
84 && (x <= max start end))
95 && (x <= max start end))
87 ||| Recognise a sequence of at least one sub-lexers
98 ||| Recognise a sequence of at least one sub-lexers
88 some : Lexer -> Lexer
100 some : Lexer -> Lexer
89 some l = l <+> many l
101 some l = l <+> many l
91 ||| Recognise a sequence of at zero or more sub-lexers. This is not
103 ||| Recognise a sequence of at zero or more sub-lexers. This is not
92 ||| guaranteed to consume input
104 ||| guaranteed to consume input
93 many : Lexer -> Recognise False
106 many : Lexer -> Recognise False
94 many l = opt (some l)
107 many l = opt (some l)
96||| Repeat the sub-lexer `l` zero or more times until the lexer
109||| Repeat the sub-lexer `l` zero or more times until the lexer
97||| `stopBefore` is encountered. `stopBefore` will not be consumed.
110||| `stopBefore` is encountered. `stopBefore` will not be consumed.
98||| Not guaranteed to consume input.
111||| Not guaranteed to consume input.
112+||| /((?!`stopBefore`)`l`)\*/
99manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
113manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
100manyUntil stopBefore l = many (reject stopBefore <+> l)
114manyUntil stopBefore l = many (reject stopBefore <+> l)
102||| Repeat the sub-lexer `l` zero or more times until the lexer
116||| Repeat the sub-lexer `l` zero or more times until the lexer
103||| `stopAfter` is encountered, and consume it. Guaranteed to
117||| `stopAfter` is encountered, and consume it. Guaranteed to
104||| consume if `stopAfter` consumes.
118||| consume if `stopAfter` consumes.
119+||| /`l`\*?`stopAfter`/
105manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
120manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
106manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
121manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
@@ -116,6 +131,7 @@ manyTill l end = end <|> opt (l <+> manyTill l end)
117||| Recognise a sub-lexer repeated as specified by `q`. Fails if `q` has
132||| Recognise a sub-lexer repeated as specified by `q`. Fails if `q` has
118||| `min` and `max` in the wrong order. Consumes input unless `min q` is zero.
133||| `min` and `max` in the wrong order. Consumes input unless `min q` is zero.
119count : (q : Quantity) -> (l : Lexer) -> Recognise (isSucc (min q))
135count : (q : Quantity) -> (l : Lexer) -> Recognise (isSucc (min q))
120count (Qty Z Nothing) l = many l
136count (Qty Z Nothing) l = many l
121count (Qty Z (Just Z)) _ = empty
137count (Qty Z (Just Z)) _ = empty
@@ -125,122 +141,150 @@ count (Qty (S min) (Just Z)) _ = fail
125count (Qty (S min) (Just (S max))) l = l <+> count (between min max) l
141count (Qty (S min) (Just (S max))) l = l <+> count (between min max) l
127||| Recognise a single digit 0-9
143||| Recognise a single digit 0-9
128digit : Lexer
145digit : Lexer
129digit = pred isDigit
146digit = pred isDigit
131−||| Recognise one or more digits
148+||| Recognise one or more digits
132digits : Lexer
150digits : Lexer
133digits = some digit
151digits = some digit
135||| Recognise a single hexidecimal digit
153||| Recognise a single hexidecimal digit
136hexDigit : Lexer
155hexDigit : Lexer
137hexDigit = pred isHexDigit
156hexDigit = pred isHexDigit
139||| Recognise one or more hexidecimal digits
158||| Recognise one or more hexidecimal digits
140hexDigits : Lexer
160hexDigits : Lexer
141hexDigits = some hexDigit
161hexDigits = some hexDigit
143||| Recognise a single alpha character
163||| Recognise a single alpha character
144alpha : Lexer
165alpha : Lexer
145alpha = pred isAlpha
166alpha = pred isAlpha
147||| Recognise one or more alpha characters
168||| Recognise one or more alpha characters
148alphas : Lexer
170alphas : Lexer
149alphas = some alpha
171alphas = some alpha
151||| Recognise a lowercase alpha character
173||| Recognise a lowercase alpha character
152lower : Lexer
175lower : Lexer
153lower = pred isLower
176lower = pred isLower
155||| Recognise one or more lowercase alpha characters
178||| Recognise one or more lowercase alpha characters
156lowers : Lexer
180lowers : Lexer
157lowers = some lower
181lowers = some lower
159||| Recognise an uppercase alpha character
183||| Recognise an uppercase alpha character
160upper : Lexer
185upper : Lexer
161upper = pred isUpper
186upper = pred isUpper
163||| Recognise one or more uppercase alpha characters
188||| Recognise one or more uppercase alpha characters
164uppers : Lexer
190uppers : Lexer
165uppers = some upper
191uppers = some upper
167||| Recognise an alphanumeric character
193||| Recognise an alphanumeric character
168alphaNum : Lexer
195alphaNum : Lexer
169alphaNum = pred isAlphaNum
196alphaNum = pred isAlphaNum
171||| Recognise one or more alphanumeric characters
198||| Recognise one or more alphanumeric characters
172alphaNums : Lexer
200alphaNums : Lexer
173alphaNums = some alphaNum
201alphaNums = some alphaNum
175||| Recognise a single whitespace character
203||| Recognise a single whitespace character
176space : Lexer
205space : Lexer
177space = pred isSpace
206space = pred isSpace
179||| Recognise one or more whitespace characters
208||| Recognise one or more whitespace characters
180spaces : Lexer
210spaces : Lexer
181spaces = some space
211spaces = some space
183||| Recognise a single newline sequence. Understands CRLF, CR, and LF
213||| Recognise a single newline sequence. Understands CRLF, CR, and LF
214+||| /\\r\\n|[\\r\\n]/
184newline : Lexer
215newline : Lexer
185newline = let crlf = "\r\n" in
216newline = let crlf = "\r\n" in
186 exact crlf <|> oneOf crlf
217 exact crlf <|> oneOf crlf
188||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
219||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
220+||| /(\\r\\n|[\\r\\n])+)/
189newlines : Lexer
221newlines : Lexer
190newlines = some newline
222newlines = some newline
192||| Recognise a single non-whitespace, non-alphanumeric character
224||| Recognise a single non-whitespace, non-alphanumeric character
225+||| /[\^\\sA-Za-z0-9]/
193symbol : Lexer
226symbol : Lexer
194symbol = pred (\x => not (isSpace x || isAlphaNum x))
227symbol = pred (\x => not (isSpace x || isAlphaNum x))
196||| Recognise one or more non-whitespace, non-alphanumeric characters
229||| Recognise one or more non-whitespace, non-alphanumeric characters
230+||| /[\^\\sA-Za-z0-9]+/
197symbols : Lexer
231symbols : Lexer
198symbols = some symbol
232symbols = some symbol
200||| Recognise a single control character
234||| Recognise a single control character
235+||| /[\\x00-\\x1f\\x7f-\\x9f]/
201control : Lexer
236control : Lexer
202control = pred isControl
237control = pred isControl
204||| Recognise one or more control characters
239||| Recognise one or more control characters
240+||| /[\\x00-\\x1f\\x7f-\\x9f]+/
205controls : Lexer
241controls : Lexer
206controls = some control
242controls = some control
208||| Recognise zero or more occurrences of a sub-lexer between
244||| Recognise zero or more occurrences of a sub-lexer between
209||| delimiting lexers
245||| delimiting lexers
246+||| /`start`(`l`)\*?`end`/
210surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
247surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
211surround start end l = start <+> manyThen end l
248surround start end l = start <+> manyThen end l
213||| Recognise zero or more occurrences of a sub-lexer surrounded
250||| Recognise zero or more occurrences of a sub-lexer surrounded
214||| by the same quote lexer on both sides (useful for strings)
251||| by the same quote lexer on both sides (useful for strings)
215quote : (q : Lexer) -> (l : Lexer) -> Lexer
253quote : (q : Lexer) -> (l : Lexer) -> Lexer
216quote q l = surround q q l
254quote q l = surround q q l
218||| Recognise an escape character (often '\\') followed by a sub-lexer
256||| Recognise an escape character (often '\\') followed by a sub-lexer
219escape : (esc : Char) -> Lexer -> Lexer
258escape : (esc : Char) -> Lexer -> Lexer
220escape esc l = is esc <+> l
259escape esc l = is esc <+> l
222||| Recognise a string literal, including escaped characters.
261||| Recognise a string literal, including escaped characters.
223||| (Note: doesn't yet handle escape sequences such as \123)
262||| (Note: doesn't yet handle escape sequences such as \123)
224stringLit : Lexer
264stringLit : Lexer
225stringLit = quote (is '"') (escape '\\' any <|> any)
265stringLit = quote (is '"') (escape '\\' any <|> any)
227||| Recognise a character literal, including escaped characters.
267||| Recognise a character literal, including escaped characters.
228||| (Note: doesn't yet handle escape sequences such as \123)
268||| (Note: doesn't yet handle escape sequences such as \123)
269+||| /'(\\\\.|[\^'])'/
229charLit : Lexer
270charLit : Lexer
230charLit = let q = '\'' in
271charLit = let q = '\'' in
231 is q <+> (escape '\\' any <|> isNot q) <+> is q
272 is q <+> (escape '\\' any <|> isNot q) <+> is q
233||| Recognise an integer literal (possibly with a '-' prefix)
274||| Recognise an integer literal (possibly with a '-' prefix)
234intLit : Lexer
276intLit : Lexer
235intLit = opt (is '-') <+> digits
277intLit = opt (is '-') <+> digits
237||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
279||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
280+||| /0[Xx][0-9A-Fa-f]+/
238hexLit : Lexer
281hexLit : Lexer
239hexLit = approx "0x" <+> hexDigits
282hexLit = approx "0x" <+> hexDigits
241||| Recognise `start`, then recognise all input until a newline is encountered,
284||| Recognise `start`, then recognise all input until a newline is encountered,
242||| and consume the newline. Will succeed if end-of-input is encountered before
285||| and consume the newline. Will succeed if end-of-input is encountered before
243||| a newline.
286||| a newline.
287+||| /`start`[\^\\r\\n]+(\\r\\n|[\\r\\n])?/
244lineComment : (start : Lexer) -> Lexer
288lineComment : (start : Lexer) -> Lexer
245lineComment start = start <+> manyUntil newline any <+> opt newline
289lineComment start = start <+> manyUntil newline any <+> opt newline
@@ -248,7 +292,7 @@ lineComment start = start <+> manyUntil newline any <+> opt newline
248||| Supports balanced nesting.
292||| Supports balanced nesting.
250||| For block comments that don't support nesting (such as C-style comments),
294||| For block comments that don't support nesting (such as C-style comments),
251−||| use `surround`.
295+||| use `surround`
252blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
296blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
253blockComment start end = start <+> middle <+> end
297blockComment start end = start <+> middle <+> end