timescale.ha (9837B)
1 // License: MPL-2.0 2 // (c) 2021-2022 Byron Torres <b@torresjrjr.com> 3 use time; 4 5 // Represents a scale of time; a time standard. See [[convert]]. 6 export type timescale = struct { 7 name: str, 8 abbr: str, 9 convto: *tsconverter, 10 convfrom: *tsconverter, 11 }; 12 13 export type tsconverter = fn(ts: *timescale, i: time::instant) ([]time::instant | void); 14 15 // A discontinuity between two [[timescale]]s caused a one-to-one 16 // [[time::instant]] conversion to fail. 17 export type discontinuity = !void; 18 19 // The analytical result of a [[time::instant]] conversion between two 20 // [[timescale]]s at a point of [[discontinuity]]. 21 // 22 // An empty slice represents a nonexistent conversion result. 23 // A populated (>1) slice represents an ambiguous conversion result. 24 export type analytical = ![]time::instant; 25 26 // Converts a [[time::instant]] from one [[timescale]] to the next exhaustively. 27 // The final conversion result is returned. For each active pair of timescales, 28 // if neither implements conversion from the first to the second, a two-step 29 // intermediary TAI conversion will occur. If given zero or one timescales, the 30 // given instant is returned. 31 export fn convert(i: time::instant, tscs: *timescale...) (time::instant | analytical) = { 32 let ts: []time::instant = [i]; 33 let tmps: []time::instant = []; 34 35 for (let j = 1z; j < len(tscs); j += 1) { 36 let a = tscs[j - 1]; 37 let b = tscs[j]; 38 39 for (let k = 0z; k < len(ts); k += 1) { 40 const t = ts[k]; 41 42 // try .convto 43 match (a.convto(b, t)) { 44 case let convs: []time::instant => 45 append(tmps, convs...); 46 continue; 47 case void => void; 48 }; 49 50 // try .convfrom 51 match (b.convfrom(a, t)) { 52 case let convs: []time::instant => 53 append(tmps, convs...); 54 continue; 55 case void => void; 56 }; 57 58 // default to TAI intermediary 59 const convs = a.convto(&tai, t) as []time::instant; 60 for (let l = 0z; l < len(convs); l += 1) { 61 append(tmps, ( 62 b.convfrom(&tai, convs[l]) as []time::instant 63 )...); 64 }; 65 }; 66 67 // TODO: sort and deduplicate 'ts' here 68 ts = tmps; 69 tmps = []; 70 }; 71 72 return if (len(ts) == 1) ts[0] else ts; 73 }; 74 75 76 // International Atomic Time 77 // 78 // The realisation of proper time on Earth's geoid. 79 // Continuous (no leap seconds). 80 export const tai: timescale = timescale { 81 name = "International Atomic Time", 82 abbr = "TAI", 83 convto = &tai_convto, 84 convfrom = &tai_convfrom, 85 }; 86 87 fn tai_convto(ts: *timescale, i: time::instant) ([]time::instant | void) = { 88 switch (ts) { 89 case &tai => 90 return [i]; 91 case => 92 return void; 93 }; 94 }; 95 96 97 fn tai_convfrom(ts: *timescale, i: time::instant) ([]time::instant | void) = { 98 switch (ts) { 99 case &tai => 100 return [i]; 101 case => 102 return void; 103 }; 104 }; 105 106 107 // TODO: Write proper conversion functions for all timescales. 108 // 109 // Ticket: https://todo.sr.ht/~sircmpwn/hare/642 110 // 111 // For UTC, conversion functions are to return two or no instants, depending on 112 // any leap second events, and use a proper leap second table. See leapsec.ha. 113 114 115 // Coordinated Universal Time 116 // 117 // Used as the basis of civil timekeeping. 118 // Based on TAI; time-dependent offset. 119 // Discontinuous (has leap seconds). 120 // 121 // During a program's initialization, this timescale initializes by loading its 122 // UTC/TAI leap second data from [[UTC_LEAPSECS_FILE]]; otherwise, fails 123 // silently. If failed, any attempt to consult UTC leapsec data (e.g. calling 124 // [[convert]] on UTC) causes an abort. This includes [[in]]. 125 export const utc: timescale = timescale { 126 name = "Coordinated Universal Time", 127 abbr = "UTC", 128 convto = &utc_convto, 129 convfrom = &utc_convfrom, 130 }; 131 132 fn utc_convto(ts: *timescale, i: time::instant) ([]time::instant | void) = { 133 switch (ts) { 134 case &utc => 135 return [i]; 136 case &tai => 137 if (!utc_isinitialized) { 138 match (init_utc_leapsecs()) { 139 case void => 140 utc_isinitialized = true; 141 case => 142 abort("utc timescale uninitialized"); 143 }; 144 }; 145 146 const idx = lookup_leaps(&utc_leapsecs, time::unix(i)); 147 const ofst = utc_leapsecs[idx].1; 148 149 if (time::unix(i) == utc_leapsecs[idx].0) { 150 void; 151 }; 152 153 const i = time::instant { 154 sec = i.sec + 37, 155 nsec = i.nsec, 156 }; 157 158 return [i]; 159 case => 160 return void; 161 }; 162 }; 163 164 fn utc_convfrom(ts: *timescale, i: time::instant) ([]time::instant | void) = { 165 switch (ts) { 166 case &utc => 167 return [i]; 168 case &tai => 169 if (!utc_isinitialized) { 170 match (init_utc_leapsecs()) { 171 case void => 172 utc_isinitialized = true; 173 case => 174 abort("utc timescale uninitialized"); 175 }; 176 }; 177 178 const idx = lookup_leaps(&utc_leapsecs, time::unix(i)); 179 const ofst = utc_leapsecs[idx].1; 180 181 if (time::unix(i) == utc_leapsecs[idx].0) { 182 void; 183 }; 184 185 const i = time::instant { 186 sec = i.sec - 37, 187 nsec = i.nsec, 188 }; 189 190 return [i]; 191 case => 192 return void; 193 }; 194 }; 195 196 fn lookup_leaps(list: *[](i64, i64), t: i64) size = { 197 let lo = 0z, hi = len(list); 198 for (hi - lo > 1) { 199 const mid = lo + (hi - lo) / 2; 200 const middle = list[mid].0; 201 const cmp = time::compare( 202 time::from_unix(t), 203 time::from_unix(middle), 204 ); 205 switch (cmp) { 206 case -1 => 207 hi = mid; 208 case 0 => 209 lo = mid; break; 210 case 1 => 211 lo = mid; 212 case => 213 abort("Unreachable"); 214 }; 215 }; 216 return lo; 217 }; 218 219 220 // Global Positioning System Time 221 // 222 // Used for GPS coordination. 223 // Based on TAI; constant -19 second offset. 224 // Continuous (no leap seconds). 225 export const gps: timescale = timescale { 226 name = "Global Positioning System Time", 227 abbr = "GPS", 228 convto = &gps_convto, 229 convfrom = &gps_convfrom, 230 }; 231 232 // The constant offset between GPS-Time (Global Positioning System Time) and TAI 233 // (International Atomic Time). Used by [[gps]]. 234 def GPS_OFFSET: time::duration = -19 * time::SECOND; 235 236 fn gps_convto(ts: *timescale, i: time::instant) ([]time::instant | void) = { 237 switch (ts) { 238 case &gps => 239 return [i]; 240 case &tai => 241 return [time::add(i, -GPS_OFFSET)]; 242 case => 243 void; 244 }; 245 }; 246 247 fn gps_convfrom(ts: *timescale, i: time::instant) ([]time::instant | void) = { 248 switch (ts) { 249 case &gps => 250 return [i]; 251 case &tai => 252 return [time::add(i, GPS_OFFSET)]; 253 case => 254 void; 255 }; 256 }; 257 258 259 // Terrestrial Time 260 // 261 // Used for astronomical timekeeping. 262 // Based on TAI; constant +32.184 offset. 263 // Continuous (no leap seconds). 264 export const tt: timescale = timescale { 265 name = "Terrestrial Time", 266 abbr = "TT", 267 convto = &tt_convto, 268 convfrom = &tt_convfrom, 269 }; 270 271 // The constant offset between TT (Terrestrial Time) and TAI (International 272 // Atomic Time). Used by [[tt]]. 273 def TT_OFFSET: time::duration = 32184 * time::MILLISECOND; // 32.184 seconds 274 275 fn tt_convto(ts: *timescale, i: time::instant) ([]time::instant | void) = { 276 switch (ts) { 277 case &tt => 278 return [i]; 279 case &tai => 280 return [time::add(i, -TT_OFFSET)]; 281 case => 282 void; 283 }; 284 }; 285 286 287 fn tt_convfrom(ts: *timescale, i: time::instant) ([]time::instant | void) = { 288 switch (ts) { 289 case &tt => 290 return [i]; 291 case &tai => 292 return [time::add(i, TT_OFFSET)]; 293 case => 294 void; 295 }; 296 }; 297 298 // Arthur David Olson had expressed support for Martian time in his timezone 299 // database project <https://data.iana.org/time-zones/theory.html>: 300 // 301 // > The tz database does not currently support Mars time, but it is documented 302 // > here in the hopes that support will be added eventually. 303 304 // Coordinated Mars Time 305 // 306 // Used for timekeeping on Mars. 307 // Based on TT; constant factor. 308 // Continuous (no leap seconds). 309 export const mtc: timescale = timescale { 310 name = "Coordinated Mars Time", 311 abbr = "MTC", 312 convto = &mtc_convto, 313 convfrom = &mtc_convfrom, 314 }; 315 316 // Factor f, where Martian-time * f == Earth-time. 317 def FACTOR_TERRESTRIAL_MARTIAN: f64 = 1.0274912517; 318 319 // [[time::duration]] in Earth-time between the Unix epoch of 1970 Jan 1st 320 // midnight, and the Earth-Mars convergence date of 2000 Jan 6th midnight. 321 def DELTA_UNIXEPOCH_JANSIX: time::duration = 10962 * 24 * time::HOUR; 322 323 // [[time::duration]] in Mars-time between the Mars Sol Date epoch corresponding 324 // to the Gregorian Earth date 1873 Dec 29th, and the Earth-Mars convergence 325 // date of 2000 Jan 6. 326 def DELTA_MARSEPOCH_JANSIX: time::duration = 44796 * 24 * time::HOUR; 327 328 // [[time::duration]] in Mars-time between the midnights of 2000 Jan 6th on 329 // Earth and Mars. Earth's midnight occurred first. 330 def DELTA_JANSIX_ADJUSTMENT: time::duration = 82944 * time::MILLISECOND; 331 332 fn mtc_convto(ts: *timescale, i: time::instant) ([]time::instant | void) = { 333 switch (ts) { 334 case &mtc => 335 return [i]; 336 case &tai => 337 // Change epoch from that of the Mars Sol Date 338 // to the Earth-Mars convergence date 2000 Jan 6th. 339 let i = time::add(i, -DELTA_MARSEPOCH_JANSIX); 340 341 // Slightly adjust epoch for the actual Martian midnight. 342 // Earth's midnight occurred before Mars'. 343 i = time::add(i, DELTA_JANSIX_ADJUSTMENT); 344 345 // Scale from Mars-time to Earth-time. 346 i = time::mult(i, FACTOR_TERRESTRIAL_MARTIAN); 347 348 // Change epoch to the Unix epoch 1970 Jan 1st (Terrestrial Time). 349 i = time::add(i, DELTA_UNIXEPOCH_JANSIX); 350 351 // Get the TAI time. 352 // assertion since TT and TAI are continuous. 353 const ts = tt.convto(&tai, i) as []time::instant; 354 355 return ts; 356 case => 357 void; 358 }; 359 360 }; 361 362 fn mtc_convfrom(ts: *timescale, i: time::instant) ([]time::instant | void) = { 363 switch (ts) { 364 case &mtc => 365 return [i]; 366 case &tai => 367 // Get the "Terrestrial Time". 368 // assertion since TT and TAI are continuous. 369 let i = (tt.convfrom(&tai, i) as []time::instant)[0]; 370 371 // Change epoch from the Unix epoch 1970 Jan 1st (Terrestrial Time) 372 // to the Earth-Mars convergence date 2000 Jan 6th midnight. 373 i = time::add(i, -DELTA_UNIXEPOCH_JANSIX); 374 375 // Scale from Earth-time to Mars-time. 376 i = time::mult(i, 1.0 / FACTOR_TERRESTRIAL_MARTIAN); 377 378 // Slightly adjust epoch for the actual Martian midnight. 379 // Earth's midnight occurred before Mars'. 380 i = time::add(i, -DELTA_JANSIX_ADJUSTMENT); 381 382 // Change epoch to that of the Mars Sol Date. 383 i = time::add(i, DELTA_MARSEPOCH_JANSIX); 384 385 return [i]; 386 case => 387 void; 388 }; 389 390 };