@@ -192,22 +192,22 @@ lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
192||| Recognise a specific character
192||| Recognise a specific character
194is : Char -> Lexer
194is : Char -> Lexer
195−is x = Pred (==x)
195+is x = pred (==x)
197||| Recognise anything but the given character
197||| Recognise anything but the given character
199isNot : Char -> Lexer
199isNot : Char -> Lexer
200−isNot x = Pred (/=x)
200+isNot x = pred (/=x)
202||| Recognise a character case-insensitively
202||| Recognise a character case-insensitively
204like : Char -> Lexer
204like : Char -> Lexer
205−like x = Pred (\y => toUpper x == toUpper y)
205+like x = pred (\y => toUpper x == toUpper y)
207||| Recognise anything but the given character case-insensitively
207||| Recognise anything but the given character case-insensitively
209notLike : Char -> Lexer
209notLike : Char -> Lexer
210−notLike x = Pred (\y => toUpper x /= toUpper y)
210+notLike x = pred (\y => toUpper x /= toUpper y)
212||| Recognise a specific string.
212||| Recognise a specific string.
213||| Fails if the string is empty.
213||| Fails if the string is empty.
@@ -227,7 +227,7 @@ approx str = case map like (unpack str) of
227||| to consume input
227||| to consume input
229opt : Lexer -> Recognise False
229opt : Lexer -> Recognise False
230−opt l = l <|> Empty
230+opt l = l <|> empty
232||| Recognise a sequence of at least one sub-lexers
232||| Recognise a sequence of at least one sub-lexers
@@ -244,7 +244,7 @@ many l = opt (some l)
244||| if one of the options succeeds. Fails if the foldable is empty.
244||| if one of the options succeeds. Fails if the foldable is empty.
246choice : Foldable t => t Lexer -> Lexer
246choice : Foldable t => t Lexer -> Lexer
247−choice xs = foldr Alt Fail xs
247+choice xs = foldr (<|>) fail xs
249||| Repeat the sub-lexer `l` zero or more times until the lexer
249||| Repeat the sub-lexer `l` zero or more times until the lexer
250||| `stopBefore` is encountered. `stopBefore` will not be consumed.
250||| `stopBefore` is encountered. `stopBefore` will not be consumed.
@@ -281,7 +281,7 @@ atLeast (S min) l = l <+> atLeast min l
281||| consume input.
281||| consume input.
283atMost : (max : Nat) -> (l : Lexer) -> Recognise False
283atMost : (max : Nat) -> (l : Lexer) -> Recognise False
284−atMost Z _ = Empty
284+atMost Z _ = empty
285atMost (S k) l = atMost k l <+> opt l
285atMost (S k) l = atMost k l <+> opt l
287||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
287||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
@@ -289,7 +289,7 @@ atMost (S k) l = atMost k l <+> opt l
290between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
290between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
291between Z max l = atMost max l
291between Z max l = atMost max l
292−between (S min) Z _ = Fail
292+between (S min) Z _ = fail
293between (S min) (S max) l = l <+> between min max l
293between (S min) (S max) l = l <+> between min max l
295||| Recognise exactly `count` repeated occurrences of a sub-lexer.
295||| Recognise exactly `count` repeated occurrences of a sub-lexer.
@@ -301,7 +301,7 @@ exactly n l = between n n l
301||| Recognise any character
301||| Recognise any character
303any : Lexer
303any : Lexer
304−any = Pred (const True)
304+any = pred (const True)
306||| Recognise any character if the sub-lexer `l` fails.
306||| Recognise any character if the sub-lexer `l` fails.