0 | module Text.Quantity
 1 |
 2 | %default total
 3 |
 4 | ||| A quantity bounded by a minimum and, optionally, a maximum.
 5 | ||| It can be used in certain lexers or parsers to specify
 6 | ||| how many times an item is expected to appear.
 7 | public export
 8 | record Quantity where
 9 |   constructor Qty
10 |   ||| Minimum number of occurrences.
11 |   min : Nat
12 |   ||| Optional maximum number of occurrences.
13 |   max : Maybe Nat
14 |
15 | public export
16 | Show Quantity where
17 |   show (Qty Z Nothing) = "*"
18 |   show (Qty Z (Just (S Z))) = "?"
19 |   show (Qty (S Z) Nothing) = "+"
20 |   show (Qty min max) = "{" ++ show min ++ showMax ++ "}"
21 |     where
22 |       showMax : String
23 |       showMax = case max of
24 |                      Nothing => ","
25 |                      Just max' => if min == max'
26 |                                      then ""
27 |                                      else "," ++ show max'
28 |
29 | ||| Create a `Quantity` with the given lower and upper bounds. {min,max}
30 | public export
31 | between : Nat -> Nat -> Quantity
32 | between min max = Qty min (Just max)
33 |
34 | ||| Create a `Quantity` with only a lower bound. {min,}
35 | public export
36 | atLeast : Nat -> Quantity
37 | atLeast min = Qty min Nothing
38 |
39 | ||| Create a `Quantity` from zero to the given upper bound. {0,max}
40 | public export
41 | atMost : Nat -> Quantity
42 | atMost max = Qty 0 (Just max)
43 |
44 | ||| Create a `Quantity` requiring an exact number of occurrences. {n}
45 | public export
46 | exactly : Nat -> Quantity
47 | exactly n = Qty n (Just n)
48 |
49 | ||| Check whether a `Quantity`'s bounds are well-formed, i.e. min <= max.
50 | public export
51 | inOrder : Quantity -> Bool
52 | inOrder (Qty min Nothing) = True
53 | inOrder (Qty min (Just max)) = min <= max
54 |