hare

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

commit 9f5e76ca88b1335b633c3543b1ec6a5655a6a189
parent 0f8c679a2a43df23ed3074466df048c173553831
Author: Byron Torres <b@torresjrjr.com>
Date:   Sat,  8 Jan 2022 02:59:01 +0000

introduce martian time

Demonstrative code for Martian time for testing, probably should later
be moved to a third-party martian:: library.

Signed-off-by: Byron Torres <b@torresjrjr.com>

Diffstat:
Mtime/chrono/chronology.ha | 13+++++++++++++
Mtime/chrono/timescales.ha | 62+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-
Mtime/chrono/timezone.ha | 22++++++++++++++++++++--
3 files changed, 94 insertions(+), 3 deletions(-)

diff --git a/time/chrono/chronology.ha b/time/chrono/chronology.ha @@ -11,4 +11,17 @@ export type moment = struct { // 1970-01-01 export type epochal = i64; +// The temporal length of a day on Earth. +// Interpreted with an appropriate timescale like UTC, TAI, GPS. export def EARTH_DAY: time::duration = 86400 * time::SECOND; + +// The following are temporary constants for demonstration of non-terrestrial +// timescales, and should probably be moved to a third-party martian:: library. +// +// TODO: figure out a future-proof naming convention. + +// The temporal length of a solar day on Marth, in Martian seconds +export def MARS_MARTIAN_SOL: time::duration = 86400 * time::SECOND; + +// The temporal length of a solar day on Marth, in Earth (SI) seconds +export def MARS_TERRESTRIAL_SOL: time::duration = 88775.244147 * time::SECOND; diff --git a/time/chrono/timescales.ha b/time/chrono/timescales.ha @@ -95,7 +95,6 @@ fn conv_unix_tai(unix: time::instant) (time::instant | ambiguous | nonexistent) }; - // Global Positioning System Time // // Used for GPS coordination. @@ -122,3 +121,64 @@ fn conv_gps_tai(gps: time::instant) (time::instant | ambiguous | nonexistent) = return tai; }; + +// Terrestrial Time +// +// Used for astronomical timekeeping. +// Based on TAI, with a constant offset. +// Continuous (no leap seconds). +export const TT: timescale = timescale { + to_tai = &conv_tt_tai, + from_tai = &conv_tai_tt, +}; + +def TT_OFFSET: time::duration = 32.184 * time::SECOND; + +fn conv_tai_tt(tai: time::instant) (time::instant | ambiguous | nonexistent) = { + const tt = time::instant { + sec = tai.sec + (TT_OFFSET / time::SECOND), + nsec = tai.nsec + (TT_OFFSET % time::SECOND), + }; + return tt; +}; + +fn conv_tt_tai(tt: time::instant) (time::instant | ambiguous | nonexistent) = { + const tai = time::instant { + sec = tt.sec - (TT_OFFSET / time::SECOND), + nsec = tt.nsec + (TT_OFFSET % time::SECOND), + }; + return tai; +}; + + +// Coordinated Martian Time +// +// Used for local solar time on Mars. +// Based on TT, with a constant factor. +// Continuous (no leap seconds). +export const MTC: timescale = timescale { + to_tai = &conv_mtc_tai, + from_tai = &conv_tai_mtc, +}; + +def FACTOR_TERRESTRIAL_MARTIAN: f64 = 1.0274912517; + +fn conv_tai_mtc(tai: time::instant) (time::instant | ambiguous | nonexistent) = { + // TODO: propagated ambiguous errors, how to reason about? + const tt = TT.from_tai(tai)?; + const mtc = time::instant { + sec = (tt.sec: f64 * FACTOR_TERRESTRIAL_MARTIAN): i64, + nsec = tt.nsec, + }; + return mtc; +}; + +fn conv_mtc_tai(mtc: time::instant) (time::instant | ambiguous | nonexistent) = { + const tt = time::instant { + sec = (mtc.sec: f64 / FACTOR_TERRESTRIAL_MARTIAN): i64, + nsec = mtc.nsec, + }; + // TODO: propagated ambiguous errors, how to reason about? + const tai = TT.to_tai(tt)?; + return tai; +}; diff --git a/time/chrono/timezone.ha b/time/chrono/timezone.ha @@ -95,7 +95,7 @@ const TZ_local: timezone = timezone { transitions = [], }; -// The UTC "Zulu" timezone +// The UTC (Coordinated Universal Time) "Zulu" timezone export const UTC_Z: *timezone = &TZ_UTC; const TZ_UTC: timezone = timezone { @@ -113,7 +113,7 @@ const TZ_UTC: timezone = timezone { transitions = [], }; -// The TAI "Zulu" timezone +// The TAI (International Atomic Time) "Zulu" timezone export const TAI_Z: *timezone = &TZ_TAI; const TZ_TAI: timezone = timezone { @@ -130,3 +130,21 @@ const TZ_TAI: timezone = timezone { ], transitions = [], }; + +// The MTC (Coordinated Martian Time) "Zulu" timezone +export const MTC_Z: *timezone = &TZ_MTC; + +const TZ_MTC: timezone = timezone { + name = "", + timescale = &MTC, + daylength = MARS_MARTIAN_SOL, + zones = [ + zone { + zoffset = 0 * time::SECOND, + name = "Coordinated Martian Time", + abbrev = "MTC", + dst = false, + }, + ], + transitions = [], +};