@@ -12,16 +12,19 @@ import public Text.Token
1212toTokenMap : List (Lexer, k) -> TokenMap (Token k)
1313toTokenMap = map $ \(l, kind) => (l, Tok kind)
1414
15−||| Recognise any character
15+||| Recognise any character.
16+||| /./
1617any : Lexer
1718any = pred (const True)
1819
1920||| Recognise a lexer or recognise no input. This is not guaranteed
20−||| to consume input
21−opt : Lexer -> Recognise False
21+||| to consume input.
22+||| /`l`?/
23+opt : (l : Lexer) -> Recognise False
2224opt l = l <|> empty
2325
2426||| Recognise any character if the sub-lexer `l` fails.
27+||| /(?!`l`)./
2528non : (l : Lexer) -> Lexer
2629non l = reject l <+> any
2730
@@ -45,63 +48,75 @@ concat : (xs : List (Recognise c)) -> Recognise (c && isCons xs)
4548concat = concatMap id
4649
4750||| Recognise a specific character.
48−is : Char -> Lexer
51+||| /[`x`]/
52+is : (x : Char) -> Lexer
4953is x = pred (==x)
5054
5155||| Recognise anything but the given character.
52−isNot : Char -> Lexer
56+||| /[\^`x`]/
57+isNot : (x : Char) -> Lexer
5358isNot x = pred (/=x)
5459
5560||| Recognise a specific character (case-insensitive).
56−like : Char -> Lexer
61+||| /[`x`]/i
62+like : (x : Char) -> Lexer
5763like x = pred (\y => toUpper x == toUpper y)
5864
5965||| Recognise anything but the given character (case-insensitive).
60−notLike : Char -> Lexer
66+||| /[\^`x`]/i
67+notLike : (x : Char) -> Lexer
6168notLike x = pred (\y => toUpper x /= toUpper y)
6269
6370||| Recognise a specific string.
6471||| Fails if the string is empty.
65−exact : String -> Lexer
72+||| /`str`/
73+exact : (str : String) -> Lexer
6674exact str = case unpack str of
6775 [] => fail
6876 (x :: xs) => concatMap is (x :: xs)
6977
7078||| Recognise a specific string (case-insensitive).
7179||| Fails if the string is empty.
72−approx : String -> Lexer
80+||| /`str`/i
81+approx : (str : String) -> Lexer
7382approx str = case unpack str of
7483 [] => fail
7584 (x :: xs) => concatMap like (x :: xs)
7685
77−||| Recognise any of the characters in the given string
78−oneOf : String -> Lexer
79−oneOf cs = pred (\x => x `elem` unpack cs)
86+||| Recognise any of the characters in the given string.
87+||| /[`chars`]/
88+oneOf : (chars : String) -> Lexer
89+oneOf chars = pred (\x => x `elem` unpack chars)
8090
81−||| Recognise a character range [`a`-`b`]. Also works in reverse!
91+||| Recognise a character range. Also works in reverse!
92+||| /[`start`-`end`]/
8293range : (start : Char) -> (end : Char) -> Lexer
8394range start end = pred (\x => (x >= min start end)
8495 && (x <= max start end))
8596
8697mutual
8798 ||| Recognise a sequence of at least one sub-lexers
99+ ||| /`l`+/
88100 some : Lexer -> Lexer
89101 some l = l <+> many l
90102
91103 ||| Recognise a sequence of at zero or more sub-lexers. This is not
92104 ||| guaranteed to consume input
105+ ||| /`l`\*/
93106 many : Lexer -> Recognise False
94107 many l = opt (some l)
95108
96109||| Repeat the sub-lexer `l` zero or more times until the lexer
97110||| `stopBefore` is encountered. `stopBefore` will not be consumed.
98111||| Not guaranteed to consume input.
112+||| /((?!`stopBefore`)`l`)\*/
99113manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
100114manyUntil stopBefore l = many (reject stopBefore <+> l)
101115
102116||| Repeat the sub-lexer `l` zero or more times until the lexer
103117||| `stopAfter` is encountered, and consume it. Guaranteed to
104118||| consume if `stopAfter` consumes.
119+||| /`l`\*?`stopAfter`/
105120manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
106121manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
107122
@@ -116,6 +131,7 @@ manyTill l end = end <|> opt (l <+> manyTill l end)
116131
117132||| Recognise a sub-lexer repeated as specified by `q`. Fails if `q` has
118133||| `min` and `max` in the wrong order. Consumes input unless `min q` is zero.
134+||| /`l`{`q`}/
119135count : (q : Quantity) -> (l : Lexer) -> Recognise (isSucc (min q))
120136count (Qty Z Nothing) l = many l
121137count (Qty Z (Just Z)) _ = empty
@@ -125,122 +141,150 @@ count (Qty (S min) (Just Z)) _ = fail
125141count (Qty (S min) (Just (S max))) l = l <+> count (between min max) l
126142
127143||| Recognise a single digit 0-9
144+||| /[0-9]/
128145digit : Lexer
129146digit = pred isDigit
130147
131−||| Recognise one or more digits
148+||| Recognise one or more digits
149+||| /[0-9]+/
132150digits : Lexer
133151digits = some digit
134152
135153||| Recognise a single hexidecimal digit
154+||| /[0-9A-Fa-f]/
136155hexDigit : Lexer
137156hexDigit = pred isHexDigit
138157
139158||| Recognise one or more hexidecimal digits
159+||| /[0-9A-Fa-f]+/
140160hexDigits : Lexer
141161hexDigits = some hexDigit
142162
143163||| Recognise a single alpha character
164+||| /[A-Za-z]/
144165alpha : Lexer
145166alpha = pred isAlpha
146167
147168||| Recognise one or more alpha characters
169+||| /[A-Za-z]+/
148170alphas : Lexer
149171alphas = some alpha
150172
151173||| Recognise a lowercase alpha character
174+||| /[a-z]/
152175lower : Lexer
153176lower = pred isLower
154177
155178||| Recognise one or more lowercase alpha characters
179+||| /[a-z]+/
156180lowers : Lexer
157181lowers = some lower
158182
159183||| Recognise an uppercase alpha character
184+||| /[A-Z]/
160185upper : Lexer
161186upper = pred isUpper
162187
163188||| Recognise one or more uppercase alpha characters
189+||| /[A-Z]+/
164190uppers : Lexer
165191uppers = some upper
166192
167193||| Recognise an alphanumeric character
194+||| /[A-Za-z0-9]/
168195alphaNum : Lexer
169196alphaNum = pred isAlphaNum
170197
171198||| Recognise one or more alphanumeric characters
199+||| /[A-Za-z0-9]+/
172200alphaNums : Lexer
173201alphaNums = some alphaNum
174202
175203||| Recognise a single whitespace character
204+||| /\\s/
176205space : Lexer
177206space = pred isSpace
178207
179208||| Recognise one or more whitespace characters
209+||| /\\s+/
180210spaces : Lexer
181211spaces = some space
182212
183213||| Recognise a single newline sequence. Understands CRLF, CR, and LF
214+||| /\\r\\n|[\\r\\n]/
184215newline : Lexer
185216newline = let crlf = "\r\n" in
186217 exact crlf <|> oneOf crlf
187218
188219||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
220+||| /(\\r\\n|[\\r\\n])+)/
189221newlines : Lexer
190222newlines = some newline
191223
192224||| Recognise a single non-whitespace, non-alphanumeric character
225+||| /[\^\\sA-Za-z0-9]/
193226symbol : Lexer
194227symbol = pred (\x => not (isSpace x || isAlphaNum x))
195228
196229||| Recognise one or more non-whitespace, non-alphanumeric characters
230+||| /[\^\\sA-Za-z0-9]+/
197231symbols : Lexer
198232symbols = some symbol
199233
200234||| Recognise a single control character
235+||| /[\\x00-\\x1f\\x7f-\\x9f]/
201236control : Lexer
202237control = pred isControl
203238
204239||| Recognise one or more control characters
240+||| /[\\x00-\\x1f\\x7f-\\x9f]+/
205241controls : Lexer
206242controls = some control
207243
208244||| Recognise zero or more occurrences of a sub-lexer between
209245||| delimiting lexers
246+||| /`start`(`l`)\*?`end`/
210247surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
211248surround start end l = start <+> manyThen end l
212249
213250||| Recognise zero or more occurrences of a sub-lexer surrounded
214251||| by the same quote lexer on both sides (useful for strings)
252+||| /`q`(`l`)\*?`q`/
215253quote : (q : Lexer) -> (l : Lexer) -> Lexer
216254quote q l = surround q q l
217255
218256||| Recognise an escape character (often '\\') followed by a sub-lexer
257+||| /[`esc`]`l`/
219258escape : (esc : Char) -> Lexer -> Lexer
220259escape esc l = is esc <+> l
221260
222261||| Recognise a string literal, including escaped characters.
223262||| (Note: doesn't yet handle escape sequences such as \123)
263+||| /"(\\\\.|.)\*?"/
224264stringLit : Lexer
225265stringLit = quote (is '"') (escape '\\' any <|> any)
226266
227267||| Recognise a character literal, including escaped characters.
228268||| (Note: doesn't yet handle escape sequences such as \123)
269+||| /'(\\\\.|[\^'])'/
229270charLit : Lexer
230271charLit = let q = '\'' in
231272 is q <+> (escape '\\' any <|> isNot q) <+> is q
232273
233274||| Recognise an integer literal (possibly with a '-' prefix)
275+||| /-?[0-9]+/
234276intLit : Lexer
235277intLit = opt (is '-') <+> digits
236278
237279||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
280+||| /0[Xx][0-9A-Fa-f]+/
238281hexLit : Lexer
239282hexLit = approx "0x" <+> hexDigits
240283
241284||| Recognise `start`, then recognise all input until a newline is encountered,
242285||| and consume the newline. Will succeed if end-of-input is encountered before
243286||| a newline.
287+||| /`start`[\^\\r\\n]+(\\r\\n|[\\r\\n])?/
244288lineComment : (start : Lexer) -> Lexer
245289lineComment start = start <+> manyUntil newline any <+> opt newline
246290
@@ -248,7 +292,7 @@ lineComment start = start <+> manyUntil newline any <+> opt newline
248292||| Supports balanced nesting.
249293|||
250294||| For block comments that don't support nesting (such as C-style comments),
251−||| use `surround`.
295+||| use `surround`
252296blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
253297blockComment start end = start <+> middle <+> end
254298 where