1 import Base 2 3 type Duration.Error is Data: 4 OutOfRange{} 5 6 type Duration is Data: 7 Duration{days: U32, sod: U32, nanos: U32} 8 9 type Duration.Hms is Data: 10 Hms{hours: U32, minutes: U32, seconds: U32} 11 12 def Duration.zero() -> Duration: 13 Duration{0, 0, 0} 14 15 def Duration.fit(+days: U32, +sod: U32) -> Bool: 16 Bool.or( 17 U32.is_lt(days, 49710), 18 Bool.and(U32.is_eq(days, 49710), U32.is_le(sod, 23295)) 19 ) 20 21 def Duration.to_secs.add( 22 +days: U32, +sod: U32, ok: Bool 23 ) -> Result<&2, &2, Duration.Error, U32>: 24 match ok: 25 case False{}: 26 Fail{OutOfRange{}} 27 case True{}: 28 Done{U32.add(U32.mul(days, 86400), sod)} 29 30 def Duration.to_secs(d: Duration) -> Result<&2, &2, Duration.Error, U32>: 31 match d: 32 case Duration{+days, +sod, _}: 33 Duration.to_secs.add(days, sod, Duration.fit(days, sod)) 34 35 def Duration.from_secs(+secs: U32) -> Duration: 36 Duration{U32.div(secs, 86400), U32.mod(secs, 86400), 0} 37 38 def Duration.from_days(+days: U32) -> Duration: 39 Duration{days, 0, 0} 40 41 def Duration.from_hms.s2( 42 +sec: U32, +s: U32, ok: Bool 43 ) -> Result<&2, &2, Duration.Error, Duration>: 44 match ok: 45 case False{}: 46 Fail{OutOfRange{}} 47 case True{}: 48 Done{Duration.from_secs(U32.add(sec, s))} 49 50 def Duration.from_hms.s( 51 +sec: U32, +s: U32 52 ) -> Result<&2, &2, Duration.Error, Duration>: 53 Duration.from_hms.s2(sec, s, U32.is_le(s, U32.sub(U32.not(0), sec))) 54 55 def Duration.from_hms.hm2( 56 +hsec: U32, +msec: U32, +s: U32, ok: Bool 57 ) -> Result<&2, &2, Duration.Error, Duration>: 58 match ok: 59 case False{}: 60 Fail{OutOfRange{}} 61 case True{}: 62 Duration.from_hms.s(U32.add(hsec, msec), s) 63 64 def Duration.from_hms.hm( 65 +hsec: U32, +mi: U32, +s: U32 66 ) -> Result<&2, &2, Duration.Error, Duration>: 67 +msec = U32.mul(mi, 60) 68 Duration.from_hms.hm2( 69 hsec, msec, s, U32.is_le(msec, U32.sub(U32.not(0), hsec)) 70 ) 71 72 def Duration.from_hms.h( 73 +h: U32, +mi: U32, +s: U32, ok: Bool 74 ) -> Result<&2, &2, Duration.Error, Duration>: 75 match ok: 76 case False{}: 77 Fail{OutOfRange{}} 78 case True{}: 79 Duration.from_hms.hm(U32.mul(h, 3600), mi, s) 80 81 def Duration.from_hms.r( 82 +h: U32, +mi: U32, +s: U32, ok: Bool 83 ) -> Result<&2, &2, Duration.Error, Duration>: 84 match ok: 85 case False{}: 86 Fail{OutOfRange{}} 87 case True{}: 88 Duration.from_hms.h( 89 h, mi, s, U32.is_le(h, U32.div(U32.not(0), 3600)) 90 ) 91 92 def Duration.from_hms( 93 +h: U32, +mi: U32, +s: U32 94 ) -> Result<&2, &2, Duration.Error, Duration>: 95 Duration.from_hms.r( 96 h, mi, s, Bool.and(U32.is_le(mi, 59), U32.is_le(s, 59)) 97 ) 98 99 def Duration.from_hours(+h: U32) -> Result<&2, &2, Duration.Error, Duration>: 100 Duration.from_hms(h, 0, 0) 101 102 def Duration.from_mins.go( 103 +mi: U32, ok: Bool 104 ) -> Result<&2, &2, Duration.Error, Duration>: 105 match ok: 106 case False{}: 107 Fail{OutOfRange{}} 108 case True{}: 109 Done{Duration.from_secs(U32.mul(mi, 60))} 110 111 def Duration.from_mins(+mi: U32) -> Result<&2, &2, Duration.Error, Duration>: 112 Duration.from_mins.go(mi, U32.is_le(mi, U32.div(U32.not(0), 60))) 113 114 def Duration.is_eq(a: Duration, b: Duration) -> Bool: 115 match a b: 116 case Duration{+d1, +s1, +n1} Duration{+d2, +s2, +n2}: 117 Bool.and( 118 U32.is_eq(d1, d2), 119 Bool.and(U32.is_eq(s1, s2), U32.is_eq(n1, n2)) 120 ) 121 122 def Duration.is_lt.n(+n1: U32, +n2: U32, eq_s: Bool, slt: Bool) -> Bool: 123 match eq_s: 124 case False{}: 125 slt 126 case True{}: 127 U32.is_lt(n1, n2) 128 129 def Duration.is_lt.s( 130 +s1: U32, +n1: U32, +s2: U32, +n2: U32, eq_d: Bool, dlt: Bool 131 ) -> Bool: 132 match eq_d: 133 case False{}: 134 dlt 135 case True{}: 136 Duration.is_lt.n(n1, n2, U32.is_eq(s1, s2), U32.is_lt(s1, s2)) 137 138 def Duration.is_lt(a: Duration, b: Duration) -> Bool: 139 match a b: 140 case Duration{+d1, +s1, +n1} Duration{+d2, +s2, +n2}: 141 Duration.is_lt.s( 142 s1, n1, s2, n2, U32.is_eq(d1, d2), U32.is_lt(d1, d2) 143 ) 144 145 def Duration.is_gt(a: Duration, b: Duration) -> Bool: 146 Duration.is_lt(b, a) 147 148 def Duration.is_le(a: Duration, b: Duration) -> Bool: 149 Bool.not(Duration.is_lt(b, a)) 150 151 def Duration.is_ge(a: Duration, b: Duration) -> Bool: 152 Bool.not(Duration.is_lt(a, b)) 153 154 def Duration.add.days( 155 +d1: U32, +d2: U32, +sod: U32, +nanos: U32, carry: U32, ok: Bool 156 ) -> Result<&2, &2, Duration.Error, Duration>: 157 match ok: 158 case False{}: 159 Fail{OutOfRange{}} 160 case True{}: 161 Done{Duration{U32.add(U32.add(d1, d2), carry), sod, nanos}} 162 163 def Duration.add.sod2( 164 +d1: U32, +d2: U32, +sod: U32, +nanos: U32, ge: Bool 165 ) -> Result<&2, &2, Duration.Error, Duration>: 166 match ge: 167 case False{}: 168 Duration.add.days( 169 d1, d2, sod, nanos, 0, U32.is_le(d2, U32.sub(U32.not(0), d1)) 170 ) 171 case True{}: 172 Duration.add.days( 173 d1, d2, U32.sub(sod, 86400), nanos, 1, 174 U32.is_le(U32.add(d2, 1), U32.sub(U32.not(0), d1)) 175 ) 176 177 def Duration.add.sod( 178 +d1: U32, +d2: U32, +s1: U32, +s2: U32, +nanos: U32, nc: U32 179 ) -> Result<&2, &2, Duration.Error, Duration>: 180 +sod = U32.add(U32.add(s1, s2), nc) 181 Duration.add.sod2(d1, d2, sod, nanos, U32.is_ge(sod, 86400)) 182 183 def Duration.add.n2( 184 +d1: U32, +d2: U32, +s1: U32, +s2: U32, +ns: U32, ge: Bool 185 ) -> Result<&2, &2, Duration.Error, Duration>: 186 match ge: 187 case False{}: 188 Duration.add.sod(d1, d2, s1, s2, ns, 0) 189 case True{}: 190 Duration.add.sod(d1, d2, s1, s2, U32.sub(ns, 1000000000), 1) 191 192 def Duration.add.n( 193 +d1: U32, +d2: U32, +s1: U32, +s2: U32, +n1: U32, +n2: U32 194 ) -> Result<&2, &2, Duration.Error, Duration>: 195 +ns = U32.add(n1, n2) 196 Duration.add.n2(d1, d2, s1, s2, ns, U32.is_ge(ns, 1000000000)) 197 198 def Duration.add( 199 a: Duration, b: Duration 200 ) -> Result<&2, &2, Duration.Error, Duration>: 201 match a b: 202 case Duration{d1, s1, n1} Duration{d2, s2, n2}: 203 Duration.add.n(d1, d2, s1, s2, n1, n2) 204 205 def Duration.sub.days( 206 +days: U32, +sod: U32, +nanos: U32, +b_days: U32, ok: Bool 207 ) -> Result<&2, &2, Duration.Error, Duration>: 208 match ok: 209 case False{}: 210 Fail{OutOfRange{}} 211 case True{}: 212 Done{Duration{U32.sub(days, b_days), sod, nanos}} 213 214 def Duration.sub.s2( 215 +days: U32, +sod: U32, +nanos: U32, +b_days: U32, +b_sod: U32, borrow: Bool 216 ) -> Result<&2, &2, Duration.Error, Duration>: 217 match borrow: 218 case False{}: 219 Duration.sub.days(days, U32.sub(sod, b_sod), nanos, b_days, U32.is_ge(days, b_days)) 220 case True{}: 221 Duration.sub.days( 222 U32.sub(days, 1), U32.sub(U32.add(sod, 86400), b_sod), nanos, b_days, 223 U32.is_ge(days, U32.add(b_days, 1)) 224 ) 225 226 def Duration.sub.s( 227 +days: U32, +sod: U32, +nanos: U32, +b_days: U32, +b_sod: U32 228 ) -> Result<&2, &2, Duration.Error, Duration>: 229 Duration.sub.s2(days, sod, nanos, b_days, b_sod, U32.is_lt(sod, b_sod)) 230 231 def Duration.sub.n2( 232 +days: U32, +sod: U32, +n1: U32, +b_days: U32, +b_sod: U32, +b_n: U32, borrow: Bool 233 ) -> Result<&2, &2, Duration.Error, Duration>: 234 match borrow: 235 case False{}: 236 Duration.sub.s(days, sod, U32.sub(n1, b_n), b_days, b_sod) 237 case True{}: 238 Duration.sub.s( 239 days, sod, U32.sub(U32.add(n1, 1000000000), b_n), b_days, b_sod 240 ) 241 242 def Duration.sub.n0( 243 +days: U32, +n1: U32, +b_days: U32, +b_sod: U32, +b_n: U32, zdays: Bool 244 ) -> Result<&2, &2, Duration.Error, Duration>: 245 match zdays: 246 case True{}: 247 Fail{OutOfRange{}} 248 case False{}: 249 Duration.sub.s( 250 U32.sub(days, 1), 86399, U32.sub(U32.add(n1, 1000000000), b_n), 251 b_days, b_sod 252 ) 253 254 def Duration.sub.n2b( 255 +days: U32, +sod: U32, +n1: U32, +b_days: U32, +b_sod: U32, +b_n: U32, borrow: Bool, z: Bool 256 ) -> Result<&2, &2, Duration.Error, Duration>: 257 match borrow z: 258 case True{} True{}: 259 Duration.sub.n0(days, n1, b_days, b_sod, b_n, U32.is_eq(days, 0)) 260 case True{} False{}: 261 Duration.sub.n2(days, U32.sub(sod, 1), n1, b_days, b_sod, b_n, True{}) 262 case False{} True{}: 263 Duration.sub.n2(days, sod, n1, b_days, b_sod, b_n, False{}) 264 case False{} False{}: 265 Duration.sub.n2(days, sod, n1, b_days, b_sod, b_n, False{}) 266 267 def Duration.sub.n( 268 +days: U32, +sod: U32, +n1: U32, +b_days: U32, +b_sod: U32, +b_n: U32 269 ) -> Result<&2, &2, Duration.Error, Duration>: 270 +borrow = U32.is_lt(n1, b_n) 271 Duration.sub.n2b(days, sod, n1, b_days, b_sod, b_n, borrow, U32.is_eq(sod, 0)) 272 273 def Duration.sub.go(a: Duration, b: Duration) -> Result<&2, &2, Duration.Error, Duration>: 274 match a b: 275 case Duration{d1, s1, n1} Duration{d2, s2, n2}: 276 Duration.sub.n(d1, s1, n1, d2, s2, n2) 277 278 def Duration.sub.lt( 279 a: Duration, b: Duration, lt: Bool 280 ) -> Result<&2, &2, Duration.Error, Duration>: 281 match lt: 282 case True{}: 283 Fail{OutOfRange{}} 284 case False{}: 285 Duration.sub.go(a, b) 286 287 def Duration.sub( 288 +a: Duration, +b: Duration 289 ) -> Result<&2, &2, Duration.Error, Duration>: 290 Duration.sub.lt(a, b, Duration.is_lt(a, b)) 291 292 def Duration.to_hms.ok(+days: U32, +sod: U32) -> Bool: 293 +cap = U32.div(U32.not(0), 24) 294 Bool.or( 295 U32.is_lt(days, cap), 296 Bool.and( 297 U32.is_eq(days, cap), 298 U32.is_le(U32.div(sod, 3600), U32.mod(U32.not(0), 24)) 299 ) 300 ) 301 302 def Duration.to_hms.go( 303 +days: U32, +sod: U32, ok: Bool 304 ) -> Result<&2, &2, Duration.Error, Duration.Hms>: 305 match ok: 306 case False{}: 307 Fail{OutOfRange{}} 308 case True{}: 309 Done{ 310 Hms{ 311 U32.add(U32.mul(days, 24), U32.div(sod, 3600)), 312 U32.div(U32.mod(sod, 3600), 60), 313 U32.mod(sod, 60) 314 } 315 } 316 317 def Duration.to_hms( 318 d: Duration 319 ) -> Result<&2, &2, Duration.Error, Duration.Hms>: 320 match d: 321 case Duration{+days, +sod, _}: 322 Duration.to_hms.go(days, sod, Duration.to_hms.ok(days, sod))