@@ -119,6 +119,20 @@ choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
119choice (x :: []) = x
119choice (x :: []) = x
120choice (x :: xs@(_ :: _)) = x <|> choice xs
120choice (x :: xs@(_ :: _)) = x <|> choice xs
122+||| Repeat the sub-lexer `l` zero or more times until the lexer
123+||| `stopBefore` is encountered. `stopBefore` will not be consumed.
124+||| Not guaranteed to consume input.
126+manyUntil : (stopBefore : Recognise c) -> (l : Lexer) -> Recognise False
127+manyUntil stopBefore l = many (reject stopBefore <+> l)
129+||| Repeat the sub-lexer `l` zero or more times until the lexer
130+||| `stopAfter` is encountered, and consume it. Guaranteed to
131+||| consume if `stopAfter` consumes.
133+manyThen : (stopAfter : Recognise c) -> (l : Lexer) -> Recognise c
134+manyThen stopAfter l = manyUntil stopAfter l <+> stopAfter
122||| Recognise many instances of `l` until an instance of `end` is
136||| Recognise many instances of `l` until an instance of `end` is
123||| encountered.
137||| encountered.
@@ -126,6 +140,8 @@ choice (x :: xs@(_ :: _)) = x <|> choice xs
127manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
141manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
128manyTill l end = end <|> opt (l <+> manyTill l end)
142manyTill l end = end <|> opt (l <+> manyTill l end)
144+ "Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."
130||| Recognise any character
146||| Recognise any character
@@ -220,7 +236,7 @@ digits = some digit
220||| Recognise a single hexidecimal digit
236||| Recognise a single hexidecimal digit
222hexDigit : Lexer
238hexDigit : Lexer
223−hexDigit = digit <|> oneOf "abcdefABCDEF"
239+hexDigit = pred isHexDigit
225||| Recognise one or more hexidecimal digits
241||| Recognise one or more hexidecimal digits
@@ -277,6 +293,17 @@ export
277spaces : Lexer
293spaces : Lexer
278spaces = some space
294spaces = some space
296+||| Recognise a single newline sequence. Understands CRLF, CR, and LF
299+newline = let crlf = "\r\n" in
300+ exact crlf <|> oneOf crlf
302+||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
305+newlines = some newline
280||| Recognise a single non-whitespace, non-alphanumeric character
307||| Recognise a single non-whitespace, non-alphanumeric character
282symbol : Lexer
309symbol : Lexer
@@ -291,7 +318,7 @@ symbols = some symbol
291||| delimiting lexers
318||| delimiting lexers
293surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
320surround : (start : Lexer) -> (end : Lexer) -> (l : Lexer) -> Lexer
294−surround start end l = start <+> manyTill l end
321+surround start end l = start <+> manyThen end l
296||| Recognise zero or more occurrences of a sub-lexer surrounded
323||| Recognise zero or more occurrences of a sub-lexer surrounded
297||| by the same quote lexer on both sides (useful for strings)
324||| by the same quote lexer on both sides (useful for strings)
@@ -325,7 +352,26 @@ intLit = opt (is '-') <+> digits
325||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
352||| Recognise a hexidecimal literal, prefixed by "0x" or "0X"
327hexLit : Lexer
354hexLit : Lexer
328−hexLit = is '0' <+> oneOf "xX" <+> hexDigits
355+hexLit = approx "0x" <+> hexDigits
357+||| Recognise `start`, then recognise all input until a newline is encountered,
358+||| and consume the newline. Will succeed if end-of-input is encountered before
361+lineComment : (start : Lexer) -> Lexer
362+lineComment start = start <+> manyUntil newline any <+> opt newline
364+||| Recognise all input between `start` and `end` lexers.
365+||| Supports balanced nesting.
367+||| For block comments that don't support nesting (such as C-style comments),
370+blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
371+blockComment start end = start <+> middle <+> end
373+ middle : Recognise False
374+ middle = manyUntil end (blockComment start end <|> any)
330||| A mapping from lexers to the tokens they produce.
376||| A mapping from lexers to the tokens they produce.
331||| This is a list of pairs `(Lexer, String -> tokenType)`
377||| This is a list of pairs `(Lexer, String -> tokenType)`