@@ -48,18 +48,24 @@ export
48isNot : Char -> Lexer
48isNot : Char -> Lexer
49isNot x = Pred (/=x)
49isNot x = Pred (/=x)
51+||| Recognise a lexer or recognise no input. This is not guaranteed
54+opt : Lexer -> Recognise False
51||| Recognise a sequence of at least one sub-lexers
57||| Recognise a sequence of at least one sub-lexers
53some : Lexer -> Lexer
59some : Lexer -> Lexer
54−some l = l <+> (some l <|> Empty)
60+some l = l <+> opt (some l)
56||| Recognise a sequence of at zero or more sub-lexers. This is not
62||| Recognise a sequence of at zero or more sub-lexers. This is not
57||| guaranteed to consume input
63||| guaranteed to consume input
59many : Lexer -> Recognise False
65many : Lexer -> Recognise False
60−many l = some l <|> Empty
66+many l = opt (some l)
62−||| Recognize the first matching lexer from a non-empty list.
68+||| Recognise the first matching lexer from a non-empty list.
64choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
70choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
65choice (x :: []) = x
71choice (x :: []) = x
@@ -70,11 +76,8 @@ choice (x :: xs@(_ :: _)) = x <|> choice xs
71||| Useful for defining comments.
77||| Useful for defining comments.
73−manyTill : (l : Lexer)
74− -> (end : Lexer) -> Recognise False
79+manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
75−manyTill l end = end
80+manyTill l end = end <|> opt (l <+> manyTill l end)
76− <|> (l <+> manyTill l end)
79||| Recognise any character
82||| Recognise any character
@@ -182,7 +185,7 @@ charLit = is '\'' <+> strChar <+> is '\''
182||| Recognise an integer literal (possibly with a '-' prefix)
185||| Recognise an integer literal (possibly with a '-' prefix)
184intLit : Lexer
187intLit : Lexer
185−intLit = (is '-' <|> Empty) <+> digits
188+intLit = opt (is '-') <+> digits
187||| A mapping from lexers to the tokens they produce.
190||| A mapping from lexers to the tokens they produce.
188||| This is a list of pairs `(Lexer, String -> tokenType)`
191||| This is a list of pairs `(Lexer, String -> tokenType)`