on master help sign in
Text.Lexer: add newline and comment lexers

Adds `newline`, `newlines`. They recognise "\r\n", "\r", or "\n" as a newline. Adds `blockComment` and `lineComment`.

commit7c2148d88ae5439f9cb146e8ce6a78aeb3017c22 authorMichael Morgan <morgan.michael@me.com> dateSun 3 Sep 2017, 12:57 (9 years ago) parent7e604f8
1 file changed+30
libs/contrib/Text/Lexer.idr+30
libs/contrib/Text/Lexer.idr+30
@@ -291,6 +291,17 @@ export
291291spaces : Lexer
292292spaces = some space
293293
294+||| Recognise a single newline sequence. Understands CRLF, CR, and LF
295+export
296+newline : Lexer
297+newline = let crlf = "\r\n" in
298+ exact crlf <|> oneOf crlf
299+
300+||| Recognise one or more newline sequences. Understands CRLF, CR, and LF
301+export
302+newlines : Lexer
303+newlines = some newline
304+
294305||| Recognise a single non-whitespace, non-alphanumeric character
295306export
296307symbol : Lexer
@@ -341,6 +352,25 @@ export
341352hexLit : Lexer
342353hexLit = approx "0x" <+> hexDigits
343354
355+||| Recognise `start`, then recognise all input until a newline is encountered,
356+||| and consume the newline. Will succeed if end-of-input is encountered before
357+||| a newline.
358+export
359+lineComment : (start : Lexer) -> Lexer
360+lineComment start = start <+> manyUntil newline any <+> opt newline
361+
362+||| Recognise all input between `start` and `end` lexers.
363+||| Supports balanced nesting.
364+|||
365+||| For block comments that don't support nesting (such as C-style comments),
366+||| use `surround`.
367+export
368+blockComment : (start : Lexer) -> (end : Lexer) -> Lexer
369+blockComment start end = start <+> middle <+> end
370+ where
371+ middle : Recognise False
372+ middle = manyUntil end (blockComment start end <|> any)
373+
344374||| A mapping from lexers to the tokens they produce.
345375||| This is a list of pairs `(Lexer, String -> tokenType)`
346376||| For each Lexer in the list, if a substring in the input matches, run