@@ -48,18 +48,24 @@ export
4848isNot : Char -> Lexer
4949isNot x = Pred (/=x)
5050
51+||| Recognise a lexer or recognise no input. This is not guaranteed
52+||| to consume input
53+export
54+opt : Lexer -> Recognise False
55+opt l = l <|> Empty
56+
5157||| Recognise a sequence of at least one sub-lexers
5258export
5359some : Lexer -> Lexer
54−some l = l <+> (some l <|> Empty)
60+some l = l <+> opt (some l)
5561
5662||| Recognise a sequence of at zero or more sub-lexers. This is not
5763||| guaranteed to consume input
5864export
5965many : Lexer -> Recognise False
60−many l = some l <|> Empty
66+many l = opt (some l)
6167
62−||| Recognize the first matching lexer from a non-empty list.
68+||| Recognise the first matching lexer from a non-empty list.
6369export
6470choice : (xs : List Lexer) -> {auto ok : NonEmpty xs} -> Lexer
6571choice (x :: []) = x
@@ -70,11 +76,8 @@ choice (x :: xs@(_ :: _)) = x <|> choice xs
7076|||
7177||| Useful for defining comments.
7278export
73−manyTill : (l : Lexer)
74− -> (end : Lexer) -> Recognise False
75−manyTill l end = end
76− <|> (l <+> manyTill l end)
77− <|> Empty
79+manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
80+manyTill l end = end <|> opt (l <+> manyTill l end)
7881
7982||| Recognise any character
8083export
@@ -182,7 +185,7 @@ charLit = is '\'' <+> strChar <+> is '\''
182185||| Recognise an integer literal (possibly with a '-' prefix)
183186export
184187intLit : Lexer
185−intLit = (is '-' <|> Empty) <+> digits
188+intLit = opt (is '-') <+> digits
186189
187190||| A mapping from lexers to the tokens they produce.
188191||| This is a list of pairs `(Lexer, String -> tokenType)`