@@ -3,6 +3,7 @@ module Text.Lexer
33import Data.Bool.Extra
44
55import public Text.Lexer.Core
6+import public Text.Quantity
67
78%default total
89%access export
@@ -109,29 +110,15 @@ manyTill l end = end <|> opt (l <+> manyTill l end)
109110%deprecate manyTill
110111 "Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."
111112
112−||| Recognise a sub-lexer at least `min` times. Consumes input unless
113−||| min is zero.
114−atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)
115−atLeast Z l = many l
116−atLeast (S min) l = l <+> atLeast min l
117−
118−||| Recognise a sub-lexer at most `max` times. Not guaranteed to
119−||| consume input.
120−atMost : (max : Nat) -> (l : Lexer) -> Recognise False
121−atMost Z _ = empty
122−atMost (S k) l = atMost k l <+> opt l
123−
124−||| Recognise a sub-lexer repeated between `min` and `max` times. Fails
125−||| if the inputs are out of order. Consumes input unless min is zero.
126−between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)
127−between Z max l = atMost max l
128−between (S min) Z _ = fail
129−between (S min) (S max) l = l <+> between min max l
130−
131−||| Recognise exactly `count` repeated occurrences of a sub-lexer.
132−||| Consumes input unless count is zero.
133−exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)
134−exactly n l = between n n l
113+||| Recognise a sub-lexer repeated as specified by `q`. Fails if `q` has
114+||| `min` and `max` in the wrong order. Consumes input unless `min q` is zero.
115+count : (q : Quantity) -> (l : Lexer) -> Recognise (isSucc (min q))
116+count (Qty Z Nothing) l = many l
117+count (Qty Z (Just Z)) _ = empty
118+count (Qty Z (Just (S max))) l = opt $ l <+> count (atMost max) l
119+count (Qty (S min) Nothing) l = l <+> count (atLeast min) l
120+count (Qty (S min) (Just Z)) _ = fail
121+count (Qty (S min) (Just (S max))) l = l <+> count (between min max) l
135122
136123||| Recognise a single digit 0-9
137124digit : Lexer