0 | module IotaTime.Time.Component
  1 |
  2 | import public Data.So
  3 |
  4 | %default total
  5 |
  6 | ||| Whether an integer is in the inclusive hour range 0 through 23.
  7 | public export
  8 | isValidHour : Integer -> Bool
  9 | isValidHour value = value >= 0 && value < 24
 10 |
 11 | ||| An hour of day constrained to the inclusive range 0 through 23.
 12 | export
 13 | record Hour where
 14 |   constructor MkHour
 15 |   integerValue : Integer
 16 |
 17 | namespace Hour
 18 |   ||| Construct an hour when its range proof is available statically.
 19 |   public export
 20 |   fromInteger : (value : Integer) -> {auto 0 valid : So (isValidHour value)} -> Hour
 21 |   fromInteger value = MkHour value
 22 |
 23 | ||| Return the integer hour of day.
 24 | public export
 25 | hourValue : Hour -> Integer
 26 | hourValue (MkHour value) = value
 27 |
 28 | public export
 29 | Eq Hour where
 30 |   left == right = hourValue left == hourValue right
 31 |
 32 | public export
 33 | Show Hour where
 34 |   show = show . hourValue
 35 |
 36 | ||| A runtime hour value outside the inclusive range 0 through 23.
 37 | public export
 38 | data HourError = HourOutOfRange Integer
 39 |
 40 | ||| Refine an untrusted integer into an hour or return a typed range error.
 41 | public export
 42 | refineHour : (value : Integer) -> Either HourError Hour
 43 | refineHour value = case choose (isValidHour value) of
 44 |   Left valid => Right (Hour.fromInteger value @{valid})
 45 |   Right _ => Left (HourOutOfRange value)
 46 |
 47 | ||| Whether an integer is in the inclusive minute range 0 through 59.
 48 | public export
 49 | isValidMinute : Integer -> Bool
 50 | isValidMinute value = value >= 0 && value < 60
 51 |
 52 | ||| A minute of hour constrained to the inclusive range 0 through 59.
 53 | export
 54 | record Minute where
 55 |   constructor MkMinute
 56 |   integerValue : Integer
 57 |
 58 | namespace Minute
 59 |   ||| Construct a minute when its range proof is available statically.
 60 |   public export
 61 |   fromInteger : (value : Integer) -> {auto 0 valid : So (isValidMinute value)} -> Minute
 62 |   fromInteger value = MkMinute value
 63 |
 64 | ||| Return the integer minute of hour.
 65 | public export
 66 | minuteValue : Minute -> Integer
 67 | minuteValue (MkMinute value) = value
 68 |
 69 | public export
 70 | Eq Minute where
 71 |   left == right = minuteValue left == minuteValue right
 72 |
 73 | public export
 74 | Show Minute where
 75 |   show = show . minuteValue
 76 |
 77 | ||| A runtime minute value outside the inclusive range 0 through 59.
 78 | public export
 79 | data MinuteError = MinuteOutOfRange Integer
 80 |
 81 | ||| Refine an untrusted integer into a minute or return a typed range error.
 82 | public export
 83 | refineMinute : (value : Integer) -> Either MinuteError Minute
 84 | refineMinute value = case choose (isValidMinute value) of
 85 |   Left valid => Right (Minute.fromInteger value @{valid})
 86 |   Right _ => Left (MinuteOutOfRange value)
 87 |
 88 | ||| Whether an integer is in the inclusive second range 0 through 59.
 89 | public export
 90 | isValidSecond : Integer -> Bool
 91 | isValidSecond value = value >= 0 && value < 60
 92 |
 93 | ||| A second of minute constrained to the inclusive range 0 through 59.
 94 | export
 95 | record Second where
 96 |   constructor MkSecond
 97 |   integerValue : Integer
 98 |
 99 | namespace Second
100 |   ||| Construct a second when its range proof is available statically.
101 |   public export
102 |   fromInteger : (value : Integer) -> {auto 0 valid : So (isValidSecond value)} -> Second
103 |   fromInteger value = MkSecond value
104 |
105 | ||| Return the integer second of minute.
106 | public export
107 | secondValue : Second -> Integer
108 | secondValue (MkSecond value) = value
109 |
110 | public export
111 | Eq Second where
112 |   left == right = secondValue left == secondValue right
113 |
114 | public export
115 | Show Second where
116 |   show = show . secondValue
117 |
118 | ||| A runtime second value outside the inclusive range 0 through 59.
119 | public export
120 | data SecondError = SecondOutOfRange Integer
121 |
122 | ||| Refine an untrusted integer into a second or return a typed range error.
123 | public export
124 | refineSecond : (value : Integer) -> Either SecondError Second
125 | refineSecond value = case choose (isValidSecond value) of
126 |   Left valid => Right (Second.fromInteger value @{valid})
127 |   Right _ => Left (SecondOutOfRange value)
128 |
129 | ||| Whether an integer is in the nanosecond range 0 through 999,999,999.
130 | public export
131 | isValidNanosecond : Integer -> Bool
132 | isValidNanosecond value = value >= 0 && value < 1000000000
133 |
134 | ||| A nanosecond of second constrained to 0 through 999,999,999.
135 | export
136 | record Nanosecond where
137 |   constructor MkNanosecond
138 |   integerValue : Integer
139 |
140 | namespace Nanosecond
141 |   ||| Construct a nanosecond when its range proof is available statically.
142 |   public export
143 |   fromInteger : (value : Integer) ->
144 |                 {auto 0 valid : So (isValidNanosecond value)} -> Nanosecond
145 |   fromInteger value = MkNanosecond value
146 |
147 | ||| Return the integer nanosecond of second.
148 | public export
149 | nanosecondValue : Nanosecond -> Integer
150 | nanosecondValue (MkNanosecond value) = value
151 |
152 | public export
153 | Eq Nanosecond where
154 |   left == right = nanosecondValue left == nanosecondValue right
155 |
156 | public export
157 | Show Nanosecond where
158 |   show = show . nanosecondValue
159 |
160 | ||| A runtime nanosecond value outside 0 through 999,999,999.
161 | public export
162 | data NanosecondError = NanosecondOutOfRange Integer
163 |
164 | ||| Refine an untrusted integer into a nanosecond or return a typed range error.
165 | public export
166 | refineNanosecond : (value : Integer) -> Either NanosecondError Nanosecond
167 | refineNanosecond value = case choose (isValidNanosecond value) of
168 |   Left valid => Right (Nanosecond.fromInteger value @{valid})
169 |   Right _ => Left (NanosecondOutOfRange value)