@@ -127,6 +127,34 @@ export
127manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
127manyTill : (l : Lexer) -> (end : Lexer) -> Recognise False
128manyTill l end = end <|> opt (l <+> manyTill l end)
128manyTill l end = end <|> opt (l <+> manyTill l end)
130+||| Recognise a sub-lexer at least `min` times. Consumes input unless
133+atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)
135+atLeast (S min) l = l <+> atLeast min l
137+||| Recognise a sub-lexer at most `max` times. Not guaranteed to
140+atMost : (max : Nat) -> (l : Lexer) -> Recognise False
142+atMost (S k) l = atMost k l <+> opt l
144+||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
145+||| if the inputs are out of order. Consumes input unless min is zero.
147+between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
148+between Z max l = atMost max l
149+between (S min) Z _ = Fail
150+between (S min) (S max) l = l <+> between min max l
152+||| Recognise exactly `count` repeated occurrences of a sub-lexer.
153+||| Consumes input unless count is zero.
155+exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
156+exactly n l = between n n l
130||| Recognise any character
158||| Recognise any character
132any : Lexer
160any : Lexer