0 | module Text.Quantity
 1 |
 2 | %default total
 3 |
 4 | public export
 5 | record Quantity where
 6 |   constructor Qty
 7 |   min : Nat
 8 |   max : Maybe Nat
 9 |
10 | public export
11 | Show Quantity where
12 |   show (Qty Z Nothing) = "*"
13 |   show (Qty Z (Just (S Z))) = "?"
14 |   show (Qty (S Z) Nothing) = "+"
15 |   show (Qty min max) = "{" ++ show min ++ showMax ++ "}"
16 |     where
17 |       showMax : String
18 |       showMax = case max of
19 |                      Nothing => ","
20 |                      Just max' => if min == max'
21 |                                      then ""
22 |                                      else "," ++ show max'
23 |
24 | public export
25 | between : Nat -> Nat -> Quantity
26 | between min max = Qty min (Just max)
27 |
28 | public export
29 | atLeast : Nat -> Quantity
30 | atLeast min = Qty min Nothing
31 |
32 | public export
33 | atMost : Nat -> Quantity
34 | atMost max = Qty 0 (Just max)
35 |
36 | public export
37 | exactly : Nat -> Quantity
38 | exactly n = Qty n (Just n)
39 |
40 | public export
41 | inOrder : Quantity -> Bool
42 | inOrder (Qty min Nothing) = True
43 | inOrder (Qty min (Just max)) = min <= max
44 |