timescale.ha (19094B)
1 // SPDX-License-Identifier: MPL-2.0 2 // (c) Hare authors <https://harelang.org> 3 4 use time; 5 6 // Represents a scale of time; a time standard. See [[convert]]. 7 export type timescale = struct { 8 name: str, 9 abbr: str, 10 convto: *tsconverter, 11 convfrom: *tsconverter, 12 }; 13 14 export type tsconverter = fn(ts: *timescale, i: time::instant) ([]time::instant | void); 15 16 // A discontinuity between two [[timescale]]s caused a one-to-one 17 // [[time::instant]] conversion to fail. 18 export type discontinuity = !void; 19 20 // The analytical result of a [[time::instant]] conversion between two 21 // [[timescale]]s at a point of [[discontinuity]]. 22 // 23 // An empty slice represents a nonexistent conversion result. 24 // A populated (>1) slice represents an ambiguous conversion result. 25 export type analytical = ![]time::instant; 26 27 // Converts a [[time::instant]] from one [[timescale]] to the next exhaustively. 28 // The final conversion result is returned. For each active pair of timescales, 29 // if neither implements conversion from the first to the second, a two-step 30 // intermediary TAI conversion will occur. If given zero or one timescales, the 31 // given instant is returned. 32 export fn convert(i: time::instant, tscs: *timescale...) (time::instant | analytical) = { 33 let ts: []time::instant = [i]; 34 let tmps: []time::instant = []; 35 36 for (let j = 1z; j < len(tscs); j += 1) { 37 let a = tscs[j - 1]; 38 let b = tscs[j]; 39 40 for (let k = 0z; k < len(ts); k += 1) { 41 const t = ts[k]; 42 43 // try .convto 44 match (a.convto(b, t)) { 45 case let convs: []time::instant => 46 append(tmps, convs...); 47 continue; 48 case void => void; 49 }; 50 51 // try .convfrom 52 match (b.convfrom(a, t)) { 53 case let convs: []time::instant => 54 append(tmps, convs...); 55 continue; 56 case void => void; 57 }; 58 59 // default to TAI intermediary 60 const convs = a.convto(&tai, t) as []time::instant; 61 62 for (let conv .. convs) { 63 append(tmps, ( 64 b.convfrom(&tai, conv) as []time::instant 65 )...); 66 }; 67 }; 68 69 // TODO: sort and deduplicate 'ts' here 70 ts = tmps; 71 tmps = []; 72 }; 73 74 return if (len(ts) == 1) ts[0] else ts; 75 }; 76 77 78 // International Atomic Time 79 // 80 // The realisation of proper time on Earth's geoid. 81 // Continuous (no leap seconds). 82 export const tai: timescale = timescale { 83 name = "International Atomic Time", 84 abbr = "TAI", 85 convto = &tai_conv, 86 convfrom = &tai_conv, 87 }; 88 89 fn tai_conv(ts: *timescale, i: time::instant) ([]time::instant | void) = { 90 let ret: []time::instant = []; 91 switch (ts) { 92 case &tai => 93 append(ret, i); 94 return ret; 95 case => 96 return void; 97 }; 98 }; 99 100 101 // Coordinated Universal Time 102 // 103 // Used as the basis of civil timekeeping. 104 // Based on TAI; time-dependent offset. 105 // Discontinuous (has leap seconds). 106 // 107 // During a program's initialization, this timescale initializes by loading its 108 // UTC/TAI leap second data from [[UTC_LEAPSECS_PATH]]; otherwise, fails 109 // silently. If failed, any attempt to consult UTC leapsec data (e.g. calling 110 // [[convert]] on UTC) causes an abort. This includes [[in]]. 111 export const utc: timescale = timescale { 112 name = "Coordinated Universal Time", 113 abbr = "UTC", 114 convto = &utc_convto, 115 convfrom = &utc_convfrom, 116 }; 117 118 fn utc_convto(ts: *timescale, i: time::instant) ([]time::instant | void) = { 119 let ret: []time::instant = []; 120 switch (ts) { 121 case &utc => 122 append(ret, i); 123 return ret; 124 case &tai => 125 if (!utc_isinitialized) { 126 match (init_utc_leapsecs()) { 127 case void => 128 utc_isinitialized = true; 129 case => 130 abort("Failed to initialize UTC timescale"); 131 }; 132 }; 133 134 const firstleap = utc_leapsecs[0]; // TODO: no leapsecs loaded 135 if (time::compare(i, time::from_unix(firstleap.0)) < 0) { 136 append(ret, time::instant { 137 sec = i.sec + firstleap.1, 138 nsec = i.nsec, 139 }); 140 return ret; 141 }; 142 143 for (let idx = len(utc_leapsecs) - 1; idx >= 0 ; idx -= 1) { 144 const leap = utc_leapsecs[idx]; 145 const leapsecond = time::from_unix(leap.0); 146 const leapoffset = leap.1; 147 const diff = time::diff(leapsecond, i); 148 149 const prevleapoffset = 150 if (idx == 0) 0i64 else utc_leapsecs[idx - 1].1; 151 const offsetdiff = 152 (leapoffset - prevleapoffset) * time::SECOND; 153 154 // case of positive leap second (UTC repeats a second) 155 if (offsetdiff >= 0) { 156 if (diff >= 0) { 157 append(ret, time::instant { 158 sec = i.sec + leapoffset, 159 nsec = i.nsec, 160 }); 161 return ret; 162 }; 163 164 if (diff >= -offsetdiff && diff < 0) { 165 append(ret, [ 166 time::instant { 167 sec = i.sec + prevleapoffset, 168 nsec = i.nsec, 169 }, 170 time::instant { 171 sec = i.sec + leapoffset, 172 nsec = i.nsec, 173 }, 174 ]...); 175 return ret; 176 }; 177 178 continue; 179 }; 180 181 // case of negative leap second (UTC skips a second) 182 if (offsetdiff < 0) { 183 if (diff >= 0) { 184 append(ret, time::instant { 185 sec = i.sec + leapoffset, 186 nsec = i.nsec, 187 }); 188 return ret; 189 }; 190 191 if (diff >= offsetdiff && diff < 0) { 192 return ret; 193 }; 194 195 continue; 196 }; 197 }; 198 case => 199 return void; 200 }; 201 }; 202 203 fn utc_convfrom(ts: *timescale, i: time::instant) ([]time::instant | void) = { 204 let ret: []time::instant = []; 205 switch (ts) { 206 case &utc => 207 append(ret, i); 208 return ret; 209 case &tai => 210 if (!utc_isinitialized) { 211 match (init_utc_leapsecs()) { 212 case void => 213 utc_isinitialized = true; 214 case => 215 abort("Failed to initialize UTC timescale"); 216 }; 217 }; 218 219 const firstleap = utc_leapsecs[0]; // TODO: no leapsecs loaded 220 if (time::compare(i, time::from_unix(firstleap.0 + firstleap.1)) < 0) { 221 append(ret, time::instant { 222 sec = i.sec - firstleap.1, 223 nsec = i.nsec, 224 }); 225 return ret; 226 }; 227 228 for (let idx = len(utc_leapsecs) - 1; idx >= 0 ; idx -= 1) { 229 const leap = utc_leapsecs[idx]; 230 const leapsecond = time::from_unix(leap.0 + leap.1); 231 const leapoffset = leap.1; 232 const diff = time::diff(leapsecond, i); 233 234 const prevleapoffset = 235 if (idx == 0) 10i64 else utc_leapsecs[idx - 1].1; 236 const offsetdiff 237 = (leapoffset - prevleapoffset) * time::SECOND; 238 239 // case of positive leap second (UTC repeats a second) 240 if (offsetdiff >= 0) { 241 if (diff >= -offsetdiff) { 242 append(ret, time::instant { 243 sec = i.sec - leapoffset, 244 nsec = i.nsec, 245 }); 246 return ret; 247 }; 248 249 continue; 250 }; 251 252 // case of negative leap second (UTC skips a second) 253 if (offsetdiff < 0) { 254 if (diff >= 0) { 255 append(ret, time::instant { 256 sec = i.sec - leapoffset, 257 nsec = i.nsec, 258 }); 259 return ret; 260 }; 261 262 continue; 263 }; 264 }; 265 case => 266 return void; 267 }; 268 }; 269 270 271 // Global Positioning System Time 272 // 273 // Used for GPS coordination. 274 // Based on TAI; constant -19 second offset. 275 // Continuous (no leap seconds). 276 export const gps: timescale = timescale { 277 name = "Global Positioning System Time", 278 abbr = "GPS", 279 convto = &gps_convto, 280 convfrom = &gps_convfrom, 281 }; 282 283 // The constant offset between GPS-Time (Global Positioning System Time) and TAI 284 // (International Atomic Time). Used by [[gps]]. 285 def GPS_OFFSET: time::duration = -19 * time::SECOND; 286 287 fn gps_convto(ts: *timescale, i: time::instant) ([]time::instant | void) = { 288 let ret: []time::instant = []; 289 switch (ts) { 290 case &gps => 291 append(ret, i); 292 return ret; 293 case &tai => 294 append(ret, time::add(i, -GPS_OFFSET)); 295 return ret; 296 case => 297 return void; 298 }; 299 }; 300 301 fn gps_convfrom(ts: *timescale, i: time::instant) ([]time::instant | void) = { 302 let ret: []time::instant = []; 303 switch (ts) { 304 case &gps => 305 append(ret, i); 306 return ret; 307 case &tai => 308 append(ret, time::add(i, GPS_OFFSET)); 309 return ret; 310 case => 311 return void; 312 }; 313 }; 314 315 316 // Terrestrial Time 317 // 318 // Used for astronomical timekeeping. 319 // Based on TAI; constant +32.184 offset. 320 // Continuous (no leap seconds). 321 export const tt: timescale = timescale { 322 name = "Terrestrial Time", 323 abbr = "TT", 324 convto = &tt_convto, 325 convfrom = &tt_convfrom, 326 }; 327 328 // The constant offset between TT (Terrestrial Time) and TAI (International 329 // Atomic Time). Used by [[tt]]. 330 def TT_OFFSET: time::duration = 32184 * time::MILLISECOND; // 32.184 seconds 331 332 fn tt_convto(ts: *timescale, i: time::instant) ([]time::instant | void) = { 333 let ret: []time::instant = []; 334 switch (ts) { 335 case &tt => 336 append(ret, i); 337 return ret; 338 case &tai => 339 append(ret, time::add(i, -TT_OFFSET)); 340 return ret; 341 case => 342 return void; 343 }; 344 }; 345 346 347 fn tt_convfrom(ts: *timescale, i: time::instant) ([]time::instant | void) = { 348 let ret: []time::instant = []; 349 switch (ts) { 350 case &tt => 351 append(ret, i); 352 return ret; 353 case &tai => 354 append(ret, time::add(i, TT_OFFSET)); 355 return ret; 356 case => 357 return void; 358 }; 359 }; 360 361 // Arthur David Olson had expressed support for Martian time in his timezone 362 // database project <https://data.iana.org/time-zones/theory.html>: 363 // 364 // > The tz database does not currently support Mars time, but it is documented 365 // > here in the hopes that support will be added eventually. 366 367 // Coordinated Mars Time 368 // 369 // Used for timekeeping on Mars. 370 // Based on TT; constant factor. 371 // Continuous (no leap seconds). 372 export const mtc: timescale = timescale { 373 name = "Coordinated Mars Time", 374 abbr = "MTC", 375 convto = &mtc_convto, 376 convfrom = &mtc_convfrom, 377 }; 378 379 // Factor f, where Martian-time * f == Earth-time. 380 def FACTOR_TERRESTRIAL_MARTIAN: f64 = 1.0274912517; 381 382 // [[time::duration]] in Earth-time between the Unix epoch of 1970 Jan 1st 383 // midnight, and the Earth-Mars convergence date of 2000 Jan 6th midnight. 384 def DELTA_UNIXEPOCH_JANSIX: time::duration = 10962 * 24 * time::HOUR; 385 386 // [[time::duration]] in Mars-time between the Mars Sol Date epoch corresponding 387 // to the Gregorian Earth date 1873 Dec 29th, and the Earth-Mars convergence 388 // date of 2000 Jan 6. 389 def DELTA_MARSEPOCH_JANSIX: time::duration = 44796 * 24 * time::HOUR; 390 391 // [[time::duration]] in Mars-time between the midnights of 2000 Jan 6th on 392 // Earth and Mars. Earth's midnight occurred first. 393 def DELTA_JANSIX_ADJUSTMENT: time::duration = 82944 * time::MILLISECOND; 394 395 fn mtc_convto(ts: *timescale, i: time::instant) ([]time::instant | void) = { 396 let ret: []time::instant = []; 397 switch (ts) { 398 case &mtc => 399 append(ret, i); 400 return ret; 401 case &tai => 402 // Change epoch from that of the Mars Sol Date 403 // to the Earth-Mars convergence date 2000 Jan 6th. 404 let i = time::add(i, -DELTA_MARSEPOCH_JANSIX); 405 406 // Slightly adjust epoch for the actual Martian midnight. 407 // Earth's midnight occurred before Mars'. 408 i = time::add(i, DELTA_JANSIX_ADJUSTMENT); 409 410 // Scale from Mars-time to Earth-time. 411 i = time::mult(i, FACTOR_TERRESTRIAL_MARTIAN); 412 413 // Change epoch to the Unix epoch 1970 Jan 1st (Terrestrial Time). 414 i = time::add(i, DELTA_UNIXEPOCH_JANSIX); 415 416 // Get the TAI time. 417 // assertion since TT and TAI are continuous. 418 append(ret, (tt.convto(&tai, i) as []time::instant)[0]); 419 return ret; 420 case => 421 return void; 422 }; 423 }; 424 425 fn mtc_convfrom(ts: *timescale, i: time::instant) ([]time::instant | void) = { 426 let ret: []time::instant = []; 427 switch (ts) { 428 case &mtc => 429 append(ret, i); 430 return ret; 431 case &tai => 432 // Get the "Terrestrial Time". 433 // assertion since TT and TAI are continuous. 434 let i = (tt.convfrom(&tai, i) as []time::instant)[0]; 435 436 // Change epoch from the Unix epoch 1970 Jan 1st (Terrestrial Time) 437 // to the Earth-Mars convergence date 2000 Jan 6th midnight. 438 i = time::add(i, -DELTA_UNIXEPOCH_JANSIX); 439 440 // Scale from Earth-time to Mars-time. 441 i = time::mult(i, 1.0 / FACTOR_TERRESTRIAL_MARTIAN); 442 443 // Slightly adjust epoch for the actual Martian midnight. 444 // Earth's midnight occurred before Mars'. 445 i = time::add(i, -DELTA_JANSIX_ADJUSTMENT); 446 447 // Change epoch to that of the Mars Sol Date. 448 append(ret, time::add(i, DELTA_MARSEPOCH_JANSIX)); 449 return ret; 450 case => 451 return void; 452 }; 453 }; 454 455 456 @test fn utc_convto_tai() void = { 457 // TODO: skip test if no leapsec data available (!utc_isinitialized) 458 // TODO: test negative leapsecs somehow 459 let testcases: []( 460 (i64, i64), // give 461 (void | [0](i64, i64) | [1](i64, i64) | [2](i64, i64)) // expect 462 ) = [ 463 ((- 1000i64, 0i64), [(- 990i64, 0i64)]), 464 (( 0i64, 0i64), [( 10i64, 0i64)]), 465 (( 1000i64, 0i64), [( 1010i64, 0i64)]), 466 // 1970 Jan 01 467 (( 63071998i64, 0i64), [( 63072008i64, 0i64)]), 468 (( 63071998i64, 500000000i64), [( 63072008i64, 500000000i64)]), 469 (( 63071999i64, 0i64), [( 63072009i64, 0i64)]), 470 (( 63071999i64, 500000000i64), [( 63072009i64, 500000000i64)]), 471 (( 63072000i64, 0i64), [( 63072010i64, 0i64)]), 472 (( 63072000i64, 500000000i64), [( 63072010i64, 500000000i64)]), 473 (( 63072001i64, 0i64), [( 63072011i64, 0i64)]), 474 (( 63072001i64, 500000000i64), [( 63072011i64, 500000000i64)]), 475 (( 63072002i64, 0i64), [( 63072012i64, 0i64)]), 476 // 1981 Jul 01 477 (( 362793598i64, 0i64), [( 362793617i64, 0i64)]), 478 (( 362793598i64, 500000000i64), [( 362793617i64, 500000000i64)]), 479 (( 362793599i64, 0i64), [ 480 ( 362793618i64, 0i64), 481 ( 362793619i64, 0i64), 482 ]), 483 (( 362793599i64, 500000000i64), [ 484 ( 362793618i64, 500000000i64), 485 ( 362793619i64, 500000000i64), 486 ]), 487 (( 362793600i64, 0i64), [( 362793620i64, 0i64)]), 488 (( 362793600i64, 500000000i64), [( 362793620i64, 500000000i64)]), 489 (( 362793601i64, 0i64), [( 362793621i64, 0i64)]), 490 (( 362793601i64, 500000000i64), [( 362793621i64, 500000000i64)]), 491 (( 362793602i64, 0i64), [( 362793622i64, 0i64)]), 492 // 2017 Jan 01 493 (( 1483228798i64, 0i64), [( 1483228834i64, 0i64)]), 494 (( 1483228798i64, 500000000i64), [( 1483228834i64, 500000000i64)]), 495 (( 1483228799i64, 0i64), [ 496 ( 1483228835i64, 0i64), 497 ( 1483228836i64, 0i64), 498 ]), 499 (( 1483228799i64, 500000000i64), [ 500 ( 1483228835i64, 500000000i64), 501 ( 1483228836i64, 500000000i64), 502 ]), 503 (( 1483228800i64, 0i64), [( 1483228837i64, 0i64)]), 504 (( 1483228800i64, 500000000i64), [( 1483228837i64, 500000000i64)]), 505 (( 1483228801i64, 0i64), [( 1483228838i64, 0i64)]), 506 (( 1483228801i64, 500000000i64), [( 1483228838i64, 500000000i64)]), 507 (( 1483228802i64, 0i64), [( 1483228839i64, 0i64)]), 508 ]; 509 510 for (let testcase .. testcases) { 511 let params = testcase.0; 512 let param = time::instant{ sec = params.0, nsec = params.1 }; 513 let expect = testcase.1; 514 let actual = utc_convto(&tai, param); 515 516 match (expect) { 517 case void => 518 assert(actual is void); 519 520 case [0](i64, i64) => 521 assert(actual is []time::instant); 522 const actual = actual as []time::instant; 523 assert(len(actual) == 0); 524 525 case let insts: [1](i64, i64) => 526 assert(actual is []time::instant); 527 const actual = actual as []time::instant; 528 assert(len(actual) == 1); 529 assert(0 == time::compare( 530 actual[0], 531 time::instant{ 532 sec = insts[0].0, 533 nsec = insts[0].1, 534 }, 535 )); 536 537 case let insts: [2](i64, i64) => 538 assert(actual is []time::instant); 539 const actual = actual as []time::instant; 540 assert(len(actual) == 2); 541 assert(0 == time::compare( 542 actual[0], 543 time::instant{ 544 sec = insts[0].0, 545 nsec = insts[0].1, 546 }, 547 )); 548 assert(0 == time::compare( 549 actual[1], 550 time::instant{ 551 sec = insts[1].0, 552 nsec = insts[1].1, 553 }, 554 )); 555 }; 556 }; 557 }; 558 559 @test fn utc_convfrom_tai() void = { 560 // TODO: skip test if no leapsec data available (!utc_isinitialized) 561 // TODO: test negative leapsecs somehow 562 let testcases: []( 563 (i64, i64), // give 564 (void | [0](i64, i64) | [1](i64, i64) | [2](i64, i64)) // expect 565 ) = [ 566 ((- 990i64, 0i64), [(- 1000i64, 0i64)]), 567 (( 10i64, 0i64), [( 0i64, 0i64)]), 568 (( 1010i64, 0i64), [( 1000i64, 0i64)]), 569 // 1970 Jan 01 570 (( 63072008i64, 0i64), [( 63071998i64, 0i64)]), 571 (( 63072008i64, 500000000i64), [( 63071998i64, 500000000i64)]), 572 (( 63072009i64, 0i64), [( 63071999i64, 0i64)]), 573 (( 63072009i64, 500000000i64), [( 63071999i64, 500000000i64)]), 574 (( 63072010i64, 0i64), [( 63072000i64, 0i64)]), 575 (( 63072010i64, 500000000i64), [( 63072000i64, 500000000i64)]), 576 (( 63072011i64, 0i64), [( 63072001i64, 0i64)]), 577 (( 63072011i64, 500000000i64), [( 63072001i64, 500000000i64)]), 578 (( 63072012i64, 0i64), [( 63072002i64, 0i64)]), 579 // 1981 Jul 01 580 (( 362793617i64, 0i64), [( 362793598i64, 0i64)]), 581 (( 362793617i64, 500000000i64), [( 362793598i64, 500000000i64)]), 582 (( 362793618i64, 0i64), [( 362793599i64, 0i64)]), 583 (( 362793618i64, 500000000i64), [( 362793599i64, 500000000i64)]), 584 (( 362793619i64, 0i64), [( 362793599i64, 0i64)]), 585 (( 362793619i64, 500000000i64), [( 362793599i64, 500000000i64)]), 586 (( 362793620i64, 0i64), [( 362793600i64, 0i64)]), 587 (( 362793620i64, 500000000i64), [( 362793600i64, 500000000i64)]), 588 (( 362793621i64, 0i64), [( 362793601i64, 0i64)]), 589 (( 362793621i64, 500000000i64), [( 362793601i64, 500000000i64)]), 590 (( 362793622i64, 0i64), [( 362793602i64, 0i64)]), 591 // 2017 Jan 01 592 (( 1483228834i64, 0i64), [( 1483228798i64, 0i64)]), 593 (( 1483228834i64, 500000000i64), [( 1483228798i64, 500000000i64)]), 594 (( 1483228835i64, 0i64), [( 1483228799i64, 0i64)]), 595 (( 1483228835i64, 500000000i64), [( 1483228799i64, 500000000i64)]), 596 (( 1483228836i64, 0i64), [( 1483228799i64, 0i64)]), 597 (( 1483228836i64, 500000000i64), [( 1483228799i64, 500000000i64)]), 598 (( 1483228837i64, 0i64), [( 1483228800i64, 0i64)]), 599 (( 1483228837i64, 500000000i64), [( 1483228800i64, 500000000i64)]), 600 (( 1483228838i64, 0i64), [( 1483228801i64, 0i64)]), 601 (( 1483228838i64, 500000000i64), [( 1483228801i64, 500000000i64)]), 602 (( 1483228839i64, 0i64), [( 1483228802i64, 0i64)]), 603 ]; 604 605 for (let testcase .. testcases) { 606 let params = testcase.0; 607 let param = time::instant{ sec = params.0, nsec = params.1 }; 608 let expect = testcase.1; 609 let actual = utc_convfrom(&tai, param); 610 611 match (expect) { 612 case void => 613 assert(actual is void); 614 615 case [0](i64, i64) => 616 assert(actual is []time::instant); 617 const actual = actual as []time::instant; 618 assert(len(actual) == 0); 619 620 case let insts: [1](i64, i64) => 621 assert(actual is []time::instant); 622 const actual = actual as []time::instant; 623 assert(len(actual) == 1); 624 assert(0 == time::compare( 625 actual[0], 626 time::instant{ 627 sec = insts[0].0, 628 nsec = insts[0].1, 629 }, 630 )); 631 632 case let insts: [2](i64, i64) => 633 assert(actual is []time::instant); 634 const actual = actual as []time::instant; 635 assert(len(actual) == 2); 636 assert(0 == time::compare( 637 actual[0], 638 time::instant{ 639 sec = insts[0].0, 640 nsec = insts[0].1, 641 }, 642 )); 643 assert(0 == time::compare( 644 actual[1], 645 time::instant{ 646 sec = insts[1].0, 647 nsec = insts[1].1, 648 }, 649 )); 650 }; 651 }; 652 };