@@ -23,6 +23,11 @@ non l = reject l <+> any
2323choice : Foldable t => t Lexer -> Lexer
2424choice xs = foldr (<|>) fail xs
2525
26+||| Sequence a list of recognisers. Guaranteed to consume input if the list is
27+||| non-empty and the recognisers consume.
28+concat : (xs : List (Recognise c)) -> Recognise (c && isCons xs)
29+concat = concatMap id
30+
2631||| Recognise a specific character.
2732is : Char -> Lexer
2833is x = pred (==x)
@@ -42,16 +47,16 @@ notLike x = pred (\y => toUpper x /= toUpper y)
4247||| Recognise a specific string.
4348||| Fails if the string is empty.
4449exact : String -> Lexer
45−exact str = case map is (unpack str) of
50+exact str = case unpack str of
4651 [] => fail
47− (x :: xs) => concat (x :: xs)
52+ (x :: xs) => concatMap is (x :: xs)
4853
4954||| Recognise a specific string (case-insensitive).
5055||| Fails if the string is empty.
5156approx : String -> Lexer
52−approx str = case map like (unpack str) of
57+approx str = case unpack str of
5358 [] => fail
54− (x :: xs) => concat (x :: xs)
59+ (x :: xs) => concatMap like (x :: xs)
5560
5661||| Recognise any of the characters in the given string
5762oneOf : String -> Lexer