hare

[hare] The Hare programming language
git clone https://git.torresjrjr.com/hare.git
Log | Files | Refs | README | LICENSE

timescale.ha (6472B)


      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.
      6 export type timescale = struct {
      7 	name: str,
      8 	abbr: str,
      9 	to_tai: *ts_converter,
     10 	from_tai: *ts_converter,
     11 };
     12 
     13 // Converts one [[time::instant]] from one [[timescale]] to another.
     14 export type ts_converter = fn(i: time::instant) (time::instant | time::error);
     15 
     16 // International Atomic Time
     17 //
     18 // The realisation of proper time on Earth's geoid.
     19 // Continuous (no leap seconds).
     20 export const tai: timescale = timescale {
     21 	name = "International Atomic Time",
     22 	abbr = "TAI",
     23 	to_tai = &conv_tai_tai,
     24 	from_tai = &conv_tai_tai,
     25 };
     26 
     27 fn conv_tai_tai(i: time::instant) (time::instant | time::error) = {
     28 	return i;
     29 };
     30 
     31 
     32 // TODO: Write proper conversion functions for all timescales.
     33 //
     34 // Ticket: https://todo.sr.ht/~sircmpwn/hare/642
     35 //
     36 // For UTC, conversion functions are to return two or no instants, depending on
     37 // any leap second events, and use a proper leap second table. See leapsec.ha.
     38 
     39 
     40 // Coordinated Universal Time
     41 //
     42 // Used as the basis of civil timekeeping.
     43 // Based on TAI; time-dependent offset.
     44 // Discontinuous (has leap seconds).
     45 export const utc: timescale = timescale {
     46 	name = "Coordinated Universal Time",
     47 	abbr = "UTC",
     48 	to_tai = &conv_utc_tai,
     49 	from_tai = &conv_tai_utc,
     50 };
     51 
     52 fn conv_tai_utc(a: time::instant) (time::instant | time::error) = {
     53 	const idx = lookup_leaps(&utc_leapsecs, time::unix(a));
     54 	const ofst = utc_leapsecs[idx].1;
     55 
     56 	if (time::unix(a) == utc_leapsecs[idx].0) {
     57 		void;
     58 	};
     59 
     60 	const b = time::instant {
     61 		sec = a.sec - 37,
     62 		nsec = a.nsec,
     63 	};
     64 	return b;
     65 };
     66 
     67 fn conv_utc_tai(a: time::instant) (time::instant | time::error) = {
     68 	const idx = lookup_leaps(&utc_leapsecs, time::unix(a));
     69 	const ofst = utc_leapsecs[idx].1;
     70 
     71 	if (time::unix(a) == utc_leapsecs[idx].0) {
     72 		void;
     73 	};
     74 
     75 	const b = time::instant {
     76 		sec = a.sec + ofst,
     77 		nsec = a.nsec,
     78 	};
     79 	return b;
     80 };
     81 
     82 fn lookup_leaps(list: *[](i64, i64), t: i64) size = {
     83 	let lo = 0z, hi = len(list);
     84 	for (hi - lo > 1) {
     85 		const mid = lo + (hi - lo) / 2;
     86 		const middle = list[mid].0;
     87 		const cmp = time::compare(
     88 			time::from_unix(t),
     89 			time::from_unix(middle),
     90 		);
     91 		switch (cmp) {
     92 		case -1 =>
     93 			hi = mid;
     94 		case 0 =>
     95 			lo = mid; break;
     96 		case 1 =>
     97 			lo = mid;
     98 		case =>
     99 			abort("Unreachable");
    100 		};
    101 	};
    102 	return lo;
    103 };
    104 
    105 
    106 // Global Positioning System Time
    107 //
    108 // Used for GPS coordination.
    109 // Based on TAI; constant -19 second offset.
    110 // Continuous (no leap seconds).
    111 export const gps: timescale = timescale {
    112 	name = "Global Positioning System Time",
    113 	abbr = "GPS",
    114 	to_tai = &conv_utc_tai,
    115 	from_tai = &conv_tai_utc,
    116 };
    117 
    118 // The constant offset between GPS-Time (Global Positioning System Time) and TAI
    119 // (International Atomic Time). Used by [[gps]].
    120 def GPS_OFFSET: time::duration = -19 * time::SECOND;
    121 
    122 fn conv_tai_gps(a: time::instant) (time::instant | time::error) = {
    123 	return time::add(a, +GPS_OFFSET);
    124 };
    125 
    126 fn conv_gps_tai(a: time::instant) (time::instant | time::error) = {
    127 	return time::add(a, -GPS_OFFSET);
    128 };
    129 
    130 
    131 // Terrestrial Time
    132 //
    133 // Used for astronomical timekeeping.
    134 // Based on TAI; constant +32.184 offset.
    135 // Continuous (no leap seconds).
    136 export const tt: timescale = timescale {
    137 	name = "Terrestrial Time",
    138 	abbr = "TT",
    139 	to_tai = &conv_tt_tai,
    140 	from_tai = &conv_tai_tt,
    141 };
    142 
    143 // The constant offset between TT (Terrestrial Time) and TAI (International
    144 // Atomic Time). Used by [[tt]].
    145 def TT_OFFSET: time::duration = 32184 * time::MILLISECOND; // 32.184 seconds
    146 
    147 fn conv_tai_tt(a: time::instant) (time::instant | time::error) = {
    148 	return time::add(a, +TT_OFFSET);
    149 };
    150 
    151 fn conv_tt_tai(a: time::instant) (time::instant | time::error) = {
    152 	return time::add(a, -TT_OFFSET);
    153 };
    154 
    155 
    156 // Arthur David Olson had expressed support for Martian time in his timezone
    157 // database project <https://data.iana.org/time-zones/theory.html>:
    158 //
    159 // > The tz database does not currently support Mars time, but it is documented
    160 // > here in the hopes that support will be added eventually.
    161 
    162 // Coordinated Mars Time
    163 //
    164 // Used for timekeeping on Mars.
    165 // Based on TT; constant factor.
    166 // Continuous (no leap seconds).
    167 export const mtc: timescale = timescale {
    168 	name = "Coordinated Mars Time",
    169 	abbr = "MTC",
    170 	to_tai = &conv_mtc_tai,
    171 	from_tai = &conv_tai_mtc,
    172 };
    173 
    174 // Factor f, where Martian-time * f == Earth-time.
    175 def FACTOR_TERRESTRIAL_MARTIAN: f64 = 1.0274912517;
    176 
    177 // [[time::duration]] in Earth-time between the Unix epoch of 1970 Jan 1st
    178 // midnight, and the Earth-Mars convergence date of 2000 Jan 6th midnight.
    179 def DELTA_UNIXEPOCH_JANSIX: time::duration = 10962 * 24 * time::HOUR;
    180 
    181 // [[time::duration]] in Mars-time between the Mars Sol Date epoch corresponding
    182 // to the Gregorian Earth date 1873 Dec 29th, and the Earth-Mars convergence
    183 // date of 2000 Jan 6.
    184 def DELTA_MARSEPOCH_JANSIX: time::duration = 44796 * 24 * time::HOUR;
    185 
    186 // [[time::duration]] in Mars-time between the midnights of 2000 Jan 6th on
    187 // Earth and Mars. Earth's midnight occurred first.
    188 def DELTA_JANSIX_ADJUSTMENT: time::duration = 82944 * time::MILLISECOND;
    189 
    190 fn conv_tai_mtc(a: time::instant) (time::instant | time::error) = {
    191 	// Get the "Terrestrial Time".
    192 	// '!' since TT and TAI are continuous.
    193 	const b = tt.from_tai(a)!;
    194 
    195 	// Change epoch from the Unix epoch 1970 Jan 1st (Terrestrial Time)
    196 	// to the Earth-Mars convergence date 2000 Jan 6th midnight.
    197 	const b = time::add(b, -DELTA_UNIXEPOCH_JANSIX);
    198 
    199 	// Scale from Earth-time to Mars-time.
    200 	const b = time::mult(b, 1.0 / FACTOR_TERRESTRIAL_MARTIAN);
    201 
    202 	// Slightly adjust epoch for the actual Martian midnight.
    203 	// Earth's midnight occurred before Mars'.
    204 	const b = time::add(b, -DELTA_JANSIX_ADJUSTMENT);
    205 
    206 	// Change epoch to that of the Mars Sol Date.
    207 	const b = time::add(b, +DELTA_MARSEPOCH_JANSIX);
    208 
    209 	return b;
    210 };
    211 
    212 fn conv_mtc_tai(a: time::instant) (time::instant | time::error) = {
    213 	// Change epoch from that of the Mars Sol Date
    214 	// to the Earth-Mars convergence date 2000 Jan 6th.
    215 	const b = time::add(a, -DELTA_MARSEPOCH_JANSIX);
    216 
    217 	// Slightly adjust epoch for the actual Martian midnight.
    218 	// Earth's midnight occurred before Mars'.
    219 	const b = time::add(b, +DELTA_JANSIX_ADJUSTMENT);
    220 
    221 	// Scale from Mars-time to Earth-time.
    222 	const b = time::mult(b, FACTOR_TERRESTRIAL_MARTIAN);
    223 
    224 	// Change epoch to the Unix epoch 1970 Jan 1st (Terrestrial Time).
    225 	const b = time::add(b, +DELTA_UNIXEPOCH_JANSIX);
    226 
    227 	// Get the TAI time.
    228 	// '!' since TT and TAI are continuous.
    229 	const b = tt.from_tai(b)!;
    230 
    231 	return b;
    232 };