/*----------------------------------------------------------------------------
   Copyright 2012-2021, Microsoft Research, Daan Leijen.

   Licensed under the Apache License, Version 2.0 ("The Licence"). You may not
   use this file except in compliance with the License. A copy of the License
   can be found in the LICENSE file at the root of this distribution.
----------------------------------------------------------------------------*/

/* UTC time scales and leap second support.

# UTC time calculation

The world's standard time scale is Universal Coordinated Time ([UTC]).
UTC is directly based on International Atomic Time ([TAI])
(`ts-tai`) and uses standard SI seconds. The UTC time scale differs from
TAI in that UTC stays within 1 second of [UT1](std_time_ut1.html); the
time scale based on the rotation of the Earth. To keep UTC close to UT1
about every 1.5 year a _leap second_ is added to the day (appearing as
a 60th second in the last minute of the day, e.g. 23:59:60h).

In order to calculate SI second durations between time instants, we need to
know when a leap second is inserted. For example, there was a leap second
inserted on 2017-01-01Z, so:
```
time(2017,1,1,0,0,0) - time(2016,12,31,23,0,0)
```
equals 3601 SI seconds to account for the extra leap second. We also need to
know the inserted leap seconds to convert UTC time to TAI which forms the
basis of many other time scales (see [``std/time/astro``](std_time_astro.html)).

The occurrence of leap seconds cannot be reliably predicted though and
the IERS
usually [announces](https://hpiers.obspm.fr/iers/bul/bulc/bulletinc.dat)
leap seconds about half a year in advance. The [IERS leap second][iersl]
table contains a list of all currently announced leap seconds. _As such,
any future duration calculation in UTC is essentially non-deterministic since
it may be off by a number of (as yet unannounced) leap seconds_. This means
in practice:

* You cannot reliably tell how many SI seconds in the future a certain
  UTC time occurs (since there may be leap seconds inserted in the future).
  If you need to store a future date, then
  store it as an ISO calendar date, like ``2020-01-01T12:00:00Z``,
  not as a time stamp.

* Do not use Unix time stamps as those may be ambiguous (see `unix-instant`);
  this library
  already defaults to time stamps as SI seconds since `epoch` which are
  monotonic and unambiguous. If no interaction with the user is needed,
  consider using TAI time and calendar instead.

## Effect types and future leap seconds

Since UTC time calculations depend on a leap second table (`:leaps-table`),
the UTC time scale can only be created from such table (`ts-utc-create`).
For most precise UTC time, you can use [`ts-utc-load`](std_time_download.html#ts_utc_load)
to automatically download and cache the latest IERS leap second information.
This can be somewhat cumbersome though as this is a function with an `:io` effect.

International Time ([TI]) (or _Temps International_) is a proposed time scale
that matches exactly UTC up to some date but with no further leap seconds
added  after that -- which makes time calculations robust and deterministic
with regard to future dates. For this reason, this library defaults to using
TI instead of UTC. The TI time scale (`ts-ti`) is defined
to exactly match UTC before the compiler release date (currently 2019) but
ignores any future leap seconds.

## UTC between 1961 and 1972

UTC only got integral leap seconds after 1972-01-01Z.
Before 1972, the UTC time was broadcast using a combination of
fixed time steps (i.e. _mini leap seconds_) and an offset from the atomic
clock frequency. By adjusting the frequency, UTC time was effectively
running at a linearly adjusted rate relative to TAI. We call this
adjustment _drift_. For example, between 1963-11-01Z and 1964-01-01Z
the frequency offset was -130×10^-10^ which means UTC was running
ahead of TAI by 0.0011232 seconds per day. The drift was then defined as:

&quad;(TAI-UTC) = 1.9458580 + 0.0011232×Δ(1962-01-01)

where the function Δ(_date_) returns the number of days since
_date_. Therefore, the difference started as 2.6972788s (as there were
669 days between 1962-01-01 and 1963-11-01) and increased linearly up to
2.7657940s on 1964-01-01Z. For dates between 1961-01-01Z and 1972-01-01Z
the library calculates the UTC time based on the historical [USNO][dat]
drift data (see Table [#tab-utc]).

Here are some interesting time steps that occurred in this time frame:

* There was a negative time step of -0.1s inserted on 1968-02-01Z:
  ```
  instant(1968,1,31,23,59,59,0.9).time(cal=cal-tai) == "1968-02-01T00:00:06.185682Z TAI"
  instant(1968,2,1).time(cal=cal-tai) == "1968-02-01T00:00:06.185682Z TAI"
  ```
  The only other negative time step was inserted on 1961-08-01Z with a
  duration of -0.05s.

* On the transition to modern UTC at 1972-01-01Z there is a mini leap second of 0.107758s.
  (because the final drift just before 1971-01-01 is 9.892242s)
  ```
  instant(1972,1,1,0,0,9,0.99999999,cal=cal-tai).time.show(6) == "1971-12-31T23:59:60.107758Z"
  instant(1972,1,1,0,0,10,cal=cal-tai).time.show == "1972-01-01T00:00:00Z"
  ```

UTC was only established in 1960 (Arias and Guinot [@Arias:utc]), and the TAI
instant 1961-01-01 00:00:01.422818Z TAI was set to be UTC instant
1961-01-01Z exactly.

## UTC before 1961

The TAI timescale was established with a 1958-01-01Z epoch, where
the difference (UT2 - TAI) was set to be approximately zero[^fn-taiepoch].
In the time frame 1958 up to 1961 the relation between TAI and UTC
is not formally defined.

We can however use the time steps and frequency adjustments as broadcast by
the NIST WWV radio station (see Explanatory Supplement to the Astronomical
Almanac [@Almanac, pages [86--87][astroa]]).  Historically there were
18 20ms time steps from 1958. The frequency offset in the year 1958 is
not clear, and is described in the Supplement as  ".. an offset of _about_
-100×10^-10^ during 1958".  We fixed the offset at -85×10^-10^ in
order to have a zero difference from TAI at exactly 1958-01-01Z.

In the library, this makes UTC coincide with TAI up to 1958-01-01,
interpolated with 'drift' up to 1972-01-01, and using integral leap-seconds
after that.

Interestingly, in the time before 1961, most leap steps occurred at 19:00h
instead of at the last second of the day, for example, on 1959-01-28
there was a 0.02s leap step:
```
instant(1959,1,28,19,0,0,0.50,cal=cal-tai).time.show == "1959-01-28T18:59:60.007866Z"
instant(1959,1,28,19,0,0,0.52,cal=cal-tai).time.show == "1959-01-28T19:00:00.007866Z"
```
showing the seconds at 60 just before 19:00h.

## All historical leap second adjustments

Table [#tab-utc] shows all leap second time steps from 1958 up to 2017. This table
is calculated and uses historical data for time steps before 1972.

~ Begin TableFigure { #tab-utc; caption:"Leap second time steps since 1958. The function \
  Δ(_date_) returns the number of days since _date_. Entries after \
  1972 are based on [IERS data][iersl]. The entries before 1972 are  \
  derived from the _Explanatory Supplement to the Astronomical Almanac_, by \
  P. Kenneth Seidelmann [@Almanac, pages [86--87][astroa]]. Entries before 1961 are based on the \
  time steps broadcast by the NIST [WWV] radio station."}

|-------------------|--------------------------|----------------|----------------|-------------------------------------------------|-----------|
| Date (UTC) &quad; | Time steps &quad; &quad; | (TAI--UTC)     | (TAI--UTC)     | Drift                                           | &quad; Frequency |
|                   |                          | Just before\ \ | On the date&quad; |                                                 | Offset    |
+:------------------|--------------------------|:---------------|:---------------|-------------------------------------------------|----------:+
| 1958-01-01        | +0                       | 0.000000       | 0.000000       | 0.000000s + 0.00073458×Δ(1958-01-01) | -85×10^-10^ |
| 1958-01-15, 19:00 | +0.020                   | 0.010866       | 0.030866       | 0.020000s + 0.00073458×Δ(&quad;&quad;"&quad;&quad;) | -85×10^-10^ |
| 1958-02-05, 19:00 | +0.020                   | 0.046292       | 0.066292       | 0.040000s + 0.00073458×Δ(&quad;&quad;"&quad;&quad;) | -85×10^-10^ |
| 1958-02-19, 19:00 | +0.020                   | 0.076576       | 0.096576       | 0.060000s + 0.00073458×Δ(&quad;&quad;"&quad;&quad;) | -85×10^-10^ |
| 1958-04-09, 19:00 | +0.020                   | 0.132570       | 0.152570       | 0.080000s + 0.00073458×Δ(&quad;&quad;"&quad;&quad;) | -85×10^-10^ |
| 1958-06-11, 19:00 | +0.020                   | 0.198849       | 0.218849       | 0.100000s + 0.00073458×Δ(&quad;&quad;"&quad;&quad;) | -85×10^-10^ |
| 1958-07-02, 19:00 | +0.020                   | 0.234275       | 0.254275       | 0.120000s + 0.00073458×Δ(&quad;&quad;"&quad;&quad;) | -85×10^-10^ |
| 1958-07-16, 19:00 | +0.020                   | 0.264559       | 0.284559       | 0.140000s + 0.00073458×Δ(&quad;&quad;"&quad;&quad;) | -85×10^-10^ |
| 1958-10-22, 19:00 | +0.020                   | 0.356548       | 0.376548       | 0.160000s + 0.00073458×Δ(&quad;&quad;"&quad;&quad;) | -85×10^-10^ |
| 1958-11-26, 19:00 | +0.020                   | 0.402258       | 0.422258       | 0.180000s + 0.00073458×Δ(&quad;&quad;"&quad;&quad;) | -85×10^-10^ |
| 1958-12-24, 19:00 | +0.020                   | 0.442827       | 0.462827       | 0.200000s + 0.00073458×Δ(&quad;&quad;"&quad;&quad;) | -85×10^-10^ |
| 1959-01-01        | +0                       | 0.468122       | 0.468122       | 0.468122s + 0.0008640×Δ(1959-01-01) | -100×10^-10^ |
| 1959-01-28, 19:00 | +0.020                   | 0.492134       | 0.512134       | 0.488122s + 0.0008640×Δ(&quad;&quad;"&quad;&quad;) | -100×10^-10^ |
| 1959-02-25, 19:00 | +0.020                   | 0.536326       | 0.556326       | 0.508122s + 0.0008640×Δ(&quad;&quad;"&quad;&quad;) | -100×10^-10^ |
| 1959-04-05, 19:00 | +0.020                   | 0.590022       | 0.610022       | 0.528122s + 0.0008640×Δ(&quad;&quad;"&quad;&quad;) | -100×10^-10^ |
| 1959-08-26, 19:00 | +0.020                   | 0.733574       | 0.753574       | 0.548122s + 0.0008640×Δ(&quad;&quad;"&quad;&quad;) | -100×10^-10^ |
| 1959-09-30, 19:00 | +0.020                   | 0.783814       | 0.803814       | 0.568122s + 0.0008640×Δ(&quad;&quad;"&quad;&quad;) | -100×10^-10^ |
| 1959-11-04, 19:00 | +0.020                   | 0.834054       | 0.854054       | 0.588122s + 0.0008640×Δ(&quad;&quad;"&quad;&quad;) | -100×10^-10^ |
| 1959-11-18, 19:00 | +0.020                   | 0.866150       | 0.886150       | 0.608122s + 0.0008640×Δ(&quad;&quad;"&quad;&quad;) | -100×10^-10^ |
| 1959-12-16, 19:00 | +0.020                   | 0.910342       | 0.930342       | 0.628122s + 0.0008640×Δ(&quad;&quad;"&quad;&quad;) | -100×10^-10^ |
| \                 |                          |                |                   |                                                                 |                    |
| 1960-01-01        | +0                       | 0.943482       | 0.943482       | 0.943482s + 0.0012960×Δ(1960-01-01) | -150×10^-10^ |
| 1961-01-01        | +0.005                   | 1.417818       | 1.422818       | 1.422818s + 0.0012960×Δ(1961-01-01) | -150×10^-10^ |
| 1961-08-01        | -0.050                   | 1.697570       | 1.647570       | 1.372818s + 0.0012960×Δ(&quad;&quad;"&quad;&quad;) | -150×10^-10^ |
| 1962-01-01        | +0                       | 1.845858       | 1.845858       | 1.845858s + 0.0011232×Δ(1962-01-01) | -130×10^-10^ |
| 1963-11-01        | +0.100                   | 2.597279       | 2.697279       | 1.945858s + 0.0011232×Δ(&quad;&quad;"&quad;&quad;) | -130×10^-10^ |
| 1964-01-01        | +0                       | 2.765794       | 2.765794       | 3.240130s + 0.0012960×Δ(1965-01-01) | -150×10^-10^ |
| 1964-04-01        | +0.100                   | 2.883730       | 2.983730       | 3.340130s + 0.0012960×Δ(&quad;&quad;"&quad;&quad;) | -150×10^-10^ |
| 1964-09-01        | +0.100                   | 3.182018       | 3.282018       | 3.440130s + 0.0012960×Δ(&quad;&quad;"&quad;&quad;) | -150×10^-10^ |
| 1965-01-01        | +0.100                   | 3.440130       | 3.540130       | 3.540130s + 0.0012960×Δ(&quad;&quad;"&quad;&quad;) | -150×10^-10^ |
| 1965-03-01        | +0.100                   | 3.616594       | 3.716594       | 3.640130s + 0.0012960×Δ(&quad;&quad;"&quad;&quad;) | -150×10^-10^ |
| 1965-07-01        | +0.100                   | 3.874706       | 3.974706       | 3.740130s + 0.0012960×Δ(&quad;&quad;"&quad;&quad;) | -150×10^-10^ |
| 1965-09-01        | +0.100                   | 4.055058       | 4.155058       | 3.840130s + 0.0012960×Δ(&quad;&quad;"&quad;&quad;) | -150×10^-10^ |
| 1966-01-01        | +0                       | 4.313170       | 4.313170       | 4.313170s + 0.0025920×Δ(1966-01-01) | -300×10^-10^ |
| 1968-02-01        | -0.100                   | 6.285682       | 6.185682       | 4.213170s + 0.0025920×Δ(&quad;&quad;"&quad;&quad;) | -300×10^-10^ |
| \                 |                          |                |                   |                                                                 |                    |
| 1972-01-01        | +0.107758                | 9.892242       | 10             |                                                 |            |
| 1972-07-01        | +1                       | 10             | 11             |                                                 |            |
| 1973-01-01        | +1                       | 11             | 12             |                                                 |            |
| 1974-01-01        | +1                       | 12             | 13             |                                                 |            |
| 1975-01-01        | +1                       | 13             | 14             |                                                 |            |
| 1976-01-01        | +1                       | 14             | 15             |                                                 |            |
| 1977-01-01        | +1                       | 15             | 16             |                                                 |            |
| 1978-01-01        | +1                       | 16             | 17             |                                                 |            |
| 1979-01-01        | +1                       | 17             | 18             |                                                 |            |
| 1980-01-01        | +1                       | 18             | 19             |                                                 |            |
| 1981-07-01        | +1                       | 19             | 20             |                                                 |            |
| 1982-07-01        | +1                       | 20             | 21             |                                                 |            |
| 1983-07-01        | +1                       | 21             | 22             |                                                 |            |
| 1985-07-01        | +1                       | 22             | 23             |                                                 |            |
| 1988-01-01        | +1                       | 23             | 24             |                                                 |            |
| 1990-01-01        | +1                       | 24             | 25             |                                                 |            |
| 1991-01-01        | +1                       | 25             | 26             |                                                 |            |
| 1992-07-01        | +1                       | 26             | 27             |                                                 |            |
| 1993-07-01        | +1                       | 27             | 28             |                                                 |            |
| 1994-07-01        | +1                       | 28             | 29             |                                                 |            |
| 1996-01-01        | +1                       | 29             | 30             |                                                 |            |
| 1997-07-01        | +1                       | 30             | 31             |                                                 |            |
| 1999-01-01        | +1                       | 31             | 32             |                                                 |            |
| 2006-01-01        | +1                       | 32             | 33             |                                                 |            |
| 2009-01-01        | +1                       | 33             | 34             |                                                 |            |
| 2012-07-01        | +1                       | 34             | 35             |                                                 |            |
| 2015-07-01        | +1                       | 35             | 36             |                                                 |            |
| 2017-01-01        | +1                       | 36             | 37             |                                                 |            |
|-------------------|--------------------------|----------------|----------------|-------------------------------------------------|-----------|
{white-space:nowrap; col-2-padding-left:1em; .sans-serif; }

~ End TableFigure

-- Daan Leijen, 2016.

## References { - }

~ Begin Bibliography { caption:"9" }

~~ BibItem { #Arias:utc; bibitem-label:"[1]"; searchterm:"Arias+Coordinated+universal+time+UTC+historical+background+perspectives" }
E.F.\ Arias and B.\ Guinot.
_Coordinated universal time UTC: historical background and perspectives_.
Journées Systèmes de Référence Spatio-Temporels. 2004.
[pdf][utchistory].
~~

~~ BibItem { #Almanac; bibitem-label:"[2]"; searchterm:"Explanatory+Supplement+to+the+Astronomical+Almanac" }
P.K.\ Seidelmann.
_Explanatory Supplement to the Astronomical Almanac_.
University Science Books, 1992. [book][astroa]
~~

~~ BibItem { #taiepoch; bibitem-label:"[3]"; searchterm:"History+of+the+Bureau+International+lHeure+Guinot" }
B.\ Guinot.
_	History of the Bureau International de l'Heure_.
In "Polar Motion: Historical and Scientific Problems", ASP Conference Series, Vol. 208,
Edited by Steven Dick, Dennis McCarthy, and Brian Luzum.
ISBN: 1-58381-039-0, 2000., p.175.
[pdf][taiepoch]
~~

~~ BibItem { #byear; bibitem-label:"[4]"; searchterm:"Besselian+Year+Precession+Matrix+Based+on+IAU+Lieske" }
Jay\ Lieske.
_Precession Matrix Based on IAU_ (1976).
System of Astronomical Constants, Astronomy \& Astrophysics, Vol. 73, pages 282--284. 1979.
[wikipedia](https://en.wikipedia.org/wiki/Year#Besselian_year)
~~

~ End Bibliography

[^fn-taiepoch]: The difference TAI-UT2 was supposed to be zero on 1958-01-01Z TAI but different
    observatories used their own versions of UT2 leading to longitude errors
    of a "few 0.01s" [@taiepoch]. At 1958-01-01 TAI the ΔT = TT - UT1 was 31.166s ± 0.003s
    (see [historical ΔT](https://maia.usno.navy.mil/ser7/historic_deltat.data)),
    which equals 1958-01-01T00:00:00.018 UT1 time.
    When we calculate UT2 using the current definition [@Almanac, page 85]:

    > UT2 = UT1 + 0.022·sin(2πτ) - 0.012·cos(2πτ) - 0.006·sin(4πτ) + 0.007·cos(4πτ)

    where τ is the fraction of the Besselian year [@byear]:

    > τ = 1900.0 + (JD~TT~ - 2415020.31352) / 365.242198781

    we get 1958-01-01T00:00:00.013023922Z UT2. A difference of about 0.013s with TAI.

[iersl]: https://hpiers.obspm.fr/iers/bul/bulc/ntp/leap-seconds.list
[dat]: https://maia.usno.navy.mil/ser7/tai-utc.dat
[astroa]: https://books.google.com/books?id=uJ4JhGJANb4C&lpg=PA87&vq=wwv&pg=PA87#v=onepage&q=wwv&f=false
[utchistory]: https://syrte.obspm.fr/journees2004/pdf/Arias2.pdf
[taiepoch]:https://articles.adsabs.harvard.edu/cgi-bin/nph-iarticle_query?2000ASPC..208..175G&data_type=PDF_HIGH&whole_paper=YES&type=PRINTER&filetype=.pdf
[WWV]: https://www.nist.gov/time-and-frequency-services/nist-radio-stations/wwv
[UTC]: std_time_astro.html
[TAI]: std_time_astro.html
[TI]: std_time_astro.html
[TIpropose]: https://syrte.obspm.fr/journees2004/pdf/McCarthy2.pdf#page=4
\/
*/
module std/time/utcstd/time/utc

import std/num/float64std/num/float64
import std/num/ddoublestd/num/ddouble
import std/text/parsestd/text/parse
import std/time/timestampstd/time/timestamp
import std/time/durationstd/time/duration
import std/time/instantstd/time/instant

// Return the UTC timescale with the latest leap second information.
pubstd/time/utc/utc: (E, V) -> V effect fun utcstd/time/utc/utc: (E, V) -> V() : timescalestd/time/instant/timescale: V

pub fun @default-utc( actionaction: () -> <utc|$2034> $2033 : () -> <utcstd/time/utc/utc: (E, V) -> V|std/core/types/effect-extend: (X, E) -> Eee: E> aa: V)result: -> 2098 2097 : ee: E aa: V
  withhandler: (() -> <utc|$2034> $2033) -> $2034 $2033 fun utcutc: () -> $2034 timescale() { ts-tistd/time/utc/ts-ti: timescale }
  actionaction: () -> <utc|$2034> $2033()

/*----------------------------------------------------------------------------
  Unix and NTP timestamps
----------------------------------------------------------------------------*/

/* Given a Unix time stamp in (fractional) seconds (`secs`) and an optional separate
fraction of seconds `frac` (for increased precision for nanosecond timestamps), return an `:instant`.
that is `secs + frac` seconds after the Unix epoch (``1970-01-01Z``).

Unfortunately, Unix time stamps are [ambigious](https://en.wikipedia.org/wiki/Unix_time).
The seconds `secs` are interpreted as: `val days = secs / 86400` and `val dsecs = secs % 86400`,
where `days` is the number of days since ``1970-01-01Z`` and `dsecs` is the SI seconds into
the day. This means that one cannot represent a possible extra leap second since it
will look as the first second of the next day. For example, here is how the time stamps look
around the leap second of ``1973-01-01Z``:
````
> instant(1972,12,31,23,59,59).unix-timestamp
94694399

> instant(1972,12,31,23,59,60).unix-timestamp
94694400

> instant(1973,1,1).unix-timestamp
94694400
````

Internally, this library uses proper `:timestamp`s that _can_ keep track of leap seconds.
To indicate a time in a leap second, you can use a fraction `frac` that is larger than `1.0`. For example:
````
> unix-instant(94694399.0).time
1972-12-31T23:59:59Z

> unix-instant(94694399.0,1.0).time
1972-12-31T23:59:60Z

> unix-instant(94694400.0).time
1973-01-01T00:00:00Z
````

This works well for systems that support [``CLOCK_UTC``](https://www.madore.org/~david/computers/unix-leap-seconds.html).
*/
pub fun float64/unix-instantstd/time/utc/float64/unix-instant: (u : float64, frac : ? float64, ts : ? timescale) -> instant( uu: float64 : float64std/core/types/float64: V, fracfrac: ? float64 : float64std/core/types/float64: V = 0.0literal: float64
hex64= 0x0p+0, tsts: ? timescale : timescalestd/time/instant/timescale: V = ts-tistd/time/utc/ts-ti: timescale )result: -> total instant : instantstd/time/instant/instant: V
  val tt: timespan    = timespanstd/time/timestamp/tuple64/timespan: (secs : float64, frac : float64) -> timespan(uu: float64,fracfrac: float64.fractionstd/num/float64/fraction: (d : float64) -> float64)
  val leapleap: int = fracfrac: float64.truncatestd/num/float64/truncate: (d : float64) -> float64.intstd/num/float64/int: (f : float64) -> int
  unix-instantstd/time/utc/timespan/unix-instant: (t : timespan, leap : ? int, ts : ? timescale) -> instant(tt: timespan,leapleap: int,tsts: timescale)

// Create an instant from raw unix seconds since the unix epoch (1970-01-01T00:00:10 TAI)
// Use a fraction `> 1` to indicate a time inside a leap second.
pub fun int/unix-instantstd/time/utc/int/unix-instant: (u : int, frac : ? float64, ts : ? timescale) -> instant( uu: int : intstd/core/types/int: V, fracfrac: ? float64 : float64std/core/types/float64: V = 0.0literal: float64
hex64= 0x0p+0, tsts: ? timescale : timescalestd/time/instant/timescale: V = ts-tistd/time/utc/ts-ti: timescale )result: -> total instant : instantstd/time/instant/instant: V
  val tt: timespan    = timespanstd/time/timestamp/ddouble/timespan: (secs : ddouble) -> timespan(uu: int.ddoublestd/num/ddouble/int/ddouble: (i : int) -> ddouble +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble fracfrac: float64.fractionstd/num/float64/fraction: (d : float64) -> float64.ddoublestd/num/ddouble/float64/ddouble: (d : float64) -> ddouble)
  val leapleap: int = fracfrac: float64.truncatestd/num/float64/truncate: (d : float64) -> float64.intstd/num/float64/int: (f : float64) -> int
  unix-instantstd/time/utc/timespan/unix-instant: (t : timespan, leap : ? int, ts : ? timescale) -> instant(tt: timespan,leapleap: int,tsts: timescale)

// Create an instant from raw unix seconds since the unix epoch (1970-01-01T00:00:10 TAI)
// and optional leap seconds to designate instants inside a leap seconds.
pub fun timespan/unix-instantstd/time/utc/timespan/unix-instant: (t : timespan, leap : ? int, ts : ? timescale) -> instant( tt: timespan : timespanstd/time/timestamp/timespan: V, leapleap: ? int : intstd/core/types/int: V = 0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000, tsts: ? timescale : timescalestd/time/instant/timescale: V = ts-tistd/time/utc/ts-ti: timescale )result: -> total instant : instantstd/time/instant/instant: V
  ts-tistd/time/utc/ts-ti: timescale.instantstd/time/instant/timescale/instant: (ts : timescale, t : timestamp) -> instant( timestampstd/time/timestamp/timestamp: (t : timespan, leap : ? int) -> timestamp(tt: timespan -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> ddouble unix2000std/time/utc/unix2000: timespan, leapleap: int) ).use-timescalestd/time/instant/use-timescale: (i : instant, tscale : timescale) -> instant(tsts: timescale)


// Get a standard Unix timestamp in fractional seconds since the Unix epoch (1970-01-01Z).
// Since Unix time stamps are ambigioous,
// instants inside a leap seconds show as occurring in the second after that.
pub fun unix-timestampstd/time/utc/unix-timestamp: (i : instant) -> ddouble( ii: instant :instantstd/time/instant/instant: V )result: -> total ddouble : ddoublestd/num/ddouble/ddouble: V
  (unix2000std/time/utc/unix2000: timespan +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble ii: instant.timestamp-instd/time/instant/timestamp-in: (i : instant, tscale : timescale) -> timestamp(ts-tistd/time/utc/ts-ti: timescale).unsafe-timespan-withleapstd/time/timestamp/unsafe-timespan-withleap: (ts : timestamp) -> timespan)

val unix2000std/time/utc/unix2000: timespan = timespanstd/time/timestamp/int/timespan: (seconds : int, frac : ? float64) -> timespan(946684800literal: int
dec  = 946684800
hex32= 0x386D4380
bit32= 0b00111000011011010100001110000000)

// Convert an NTP time in seconds since the NTP epoch (1900-01-01Z) to an instant.
// Also takes an optional `leap` argument if the NTP time is inside a leap second.
pub fun ntp-instantstd/time/utc/ntp-instant: (ntp : ddouble, leap : ? int) -> instant( ntpntp: ddouble : ddoublestd/num/ddouble/ddouble: V, leapleap: ? int : intstd/core/types/int: V = 0literal: int
dec  = 0
hex8 = 0x00
bit8 = 0b00000000 )result: -> total instant : instantstd/time/instant/instant: V
  ts-ntpstd/time/utc/ts-ntp: timescale.instantstd/time/instant/timescale/instant: (ts : timescale, t : timestamp) -> instant( timestampstd/time/timestamp/timestamp: (t : timespan, leap : ? int) -> timestamp(ntpntp: ddouble,leapleap: int) -std/time/timestamp/(-): (ts : timestamp, t : timespan) -> timestamp ntp2000std/time/utc/ntp2000: timespan )

// Return the NTP time of an instant since the NTP epoch (1900-01-01)
// Since NTP time stamps are ambigious, times inside a leap second show
// as occurring in the second after the leap second.
pub fun ntp-timestampstd/time/utc/ntp-timestamp: (i : instant) -> ddouble( ii: instant : instantstd/time/instant/instant: V )result: -> total ddouble : ddoublestd/num/ddouble/ddouble: V
  ntp2000std/time/utc/ntp2000: timespan +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble ii: instant.timestamp-instd/time/instant/timestamp-in: (i : instant, tscale : timescale) -> timestamp(ts-ntpstd/time/utc/ts-ntp: timescale).unsafe-timespan-withleapstd/time/timestamp/unsafe-timespan-withleap: (ts : timestamp) -> timespan

val ntp2000std/time/utc/ntp2000: timespan = timespanstd/time/timestamp/int/timespan: (seconds : int, frac : ? float64) -> timespan(3155673600literal: int
dec  = 3155673600
hex64= 0x00000000BC17C200
bit64= 0b0000000000000000000000000000000010111100000101111100001000000000)   // 2000-01-01 - 1900-01-01 in NTP seconds; = (100*365 + 24)*(24*3600)  (24 leap days)

/*----------------------------------------------------------------------------
  Timescale creation
----------------------------------------------------------------------------*/

// Create a new time scale based on UTC seconds with a given `name`
// and a leap second table.
pub fun utc-timescalestd/time/utc/utc-timescale: (name : string, leaps : leaps-table) -> timescale( namename: string : stringstd/core/types/string: V, leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V )result: -> total timescale : timescalestd/time/instant/timescale: V
  fun from-taifrom-tai: (tai : duration) -> timestamp(taitai: duration:durationstd/time/duration/duration: V)result: -> total timestamp       { utc-from-taistd/time/utc/utc-from-tai: (leaps : leaps-table, tai-since : duration) -> timestamp(leapsleaps: leaps-table,taitai: duration) }
  fun to-taito-tai: (utc : timestamp) -> duration(utcutc: timestamp:timestampstd/time/timestamp/timestamp: V)result: -> total duration        { utc-to-taistd/time/utc/utc-to-tai: (leaps : leaps-table, utc : timestamp) -> duration(leapsleaps: leaps-table,utcutc: timestamp) }
  fun seconds-in-dayseconds-in-day: (utc : timestamp) -> timespan(utcutc: timestamp:timestampstd/time/timestamp/timestamp: V)result: -> total timespan{ utc-seconds-in-daystd/time/utc/utc-seconds-in-day: (leaps : leaps-table, utc : timestamp) -> timespan(leapsleaps: leaps-table,utcutc: timestamp) }
  fun to-mjdto-mjd: (utc : timestamp, tzdelta : timespan) -> ddouble(utcutc: timestamp:timestampstd/time/timestamp/timestamp: V,tzdeltatzdelta: timespan:timespanstd/time/timestamp/timespan: V)result: -> total ddouble{ utc-to-mjdstd/time/utc/utc-to-mjd: (leaps : leaps-table, utc : utc-timestamp, tzdelta : timespan) -> ddouble(leapsleaps: leaps-table,utcutc: timestamp,tzdeltatzdelta: timespan) }
  fun from-mjdfrom-mjd: (days : int, frac : ddouble) -> utc-timestamp(daysdays: int:intstd/core/types/int: V,fracfrac: ddouble:ddoublestd/num/ddouble/ddouble: V)result: -> total utc-timestamp{ utc-from-mjdstd/time/utc/utc-from-mjd: (leaps : leaps-table, days : int, frac : ddouble) -> utc-timestamp(leapsleaps: leaps-table,daysdays: int,fracfrac: ddouble) }
  timescalestd/time/instant/timescale: (name : string, from-tai : (duration) -> timestamp, to-tai : (timestamp) -> duration, unit : ? string, seconds-in-day : ? (maybe<(timestamp) -> timespan>), to-mjd2000 : ? (maybe<(t : timestamp, tzdelta : timespan) -> ddouble>), from-mjd2000 : ? (maybe<(days : int, frac : ddouble) -> timestamp>)) -> timescale(
    namename: string,
    from-taifrom-tai: (tai : duration) -> timestamp,
    to-taito-tai: (utc : timestamp) -> duration,
    "UTC"literal: string
count= 3,
    Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(seconds-in-dayseconds-in-day: (utc : timestamp) -> timespan),
    Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(to-mjdto-mjd: (utc : timestamp, tzdelta : timespan) -> ddouble),
    Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(from-mjdfrom-mjd: (days : int, frac : ddouble) -> utc-timestamp)
  )

// The UTC time scale.
pub fun ts-utc-createstd/time/utc/ts-utc-create: (leaps : leaps-table) -> timescale( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V )result: -> total timescale : timescalestd/time/instant/timescale: V
  utc-timescalestd/time/utc/utc-timescale: (name : string, leaps : leaps-table) -> timescale( "UTC"literal: string
count= 3, leapsleaps: leaps-table )

// [Unix](https://en.wikipedia.org/wiki/Unix_time) time scale is equal
// to the UTC time scale (`ts-utc`).
pub fun ts-unix-createstd/time/utc/ts-unix-create: (leaps : leaps-table) -> timescale( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V )result: -> total timescale : timescalestd/time/instant/timescale: V
  ts-utc-createstd/time/utc/ts-utc-create: (leaps : leaps-table) -> timescale(leapsleaps: leaps-table) // utc-timescale( "UNIX", leaps )


// [NTP](https://en.wikipedia.org/wiki/Network_Time_Protocol) time scale is equal
// to the UTC time scale (`ts-utc`).
pub fun ts-ntp-createstd/time/utc/ts-ntp-create: (leaps : leaps-table) -> timescale( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V )result: -> total timescale : timescalestd/time/instant/timescale: V
  ts-utc-createstd/time/utc/ts-utc-create: (leaps : leaps-table) -> timescale(leapsleaps: leaps-table)


/* The [TI] (_International Time_) time scale with a 2000-01-01Z UTC epoch.
This is the default time scale used in this library. It was a
[proposed][TIpropose] time scale at the 2004 ITU-R meeting as a replacement of UTC
without future leap seconds. In this library, we define TI to match
exactly UTC up to the compiler release date (currently 2017) but ignore any
possible future leap seconds after that date. This is the preferred time scale
in this library as it guarantees deterministic time calculations for any
future date, i.e. before 2017-01-01Z, TI == UTC, while after that, TI == TAI - 37s.
*/
pub val ts-tistd/time/utc/ts-ti: timescale : timescalestd/time/instant/timescale: V = utc-timescalestd/time/utc/utc-timescale: (name : string, leaps : leaps-table) -> timescale( ""literal: string
count= 0, leaps-table-tistd/time/utc/leaps-table-ti: leaps-table )

// [Unix](https://en.wikipedia.org/wiki/Unix_time) time scale based on Unix seconds.
// It equals the `ts-ti` time scale.
pub val ts-unixstd/time/utc/ts-unix: timescale : timescalestd/time/instant/timescale: V = ts-tistd/time/utc/ts-ti: timescale // utc-timescale( "UNIX-TI", leaps-table-ti )

// [NTP](https://en.wikipedia.org/wiki/Network_Time_Protocol) time scale.
// It equals the `ts-ti` time scale.
pub val ts-ntpstd/time/utc/ts-ntp: timescale : timescalestd/time/instant/timescale: V = ts-tistd/time/utc/ts-ti: timescale // utc-timescale( "NTP-TI", leaps-table-ti )


// Create a new smooted leap second time scale with an optional period during
// which smoothing takes place. This is 1000s for `ts-utc-sls`.
fun utc-sls-timescalestd/time/utc/utc-sls-timescale: (name : string, leaps : leaps-table, smooth : ? timespan) -> timescale( namename: string : stringstd/core/types/string: V, leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, smoothsmooth: ? timespan : timespanstd/time/timestamp/timespan: V = 1000literal: int
dec  = 1000
hex16= 0x03E8
bit16= 0b0000001111101000.timespanstd/time/timestamp/int/timespan: (seconds : int, frac : ? float64) -> timespan )result: -> total timescale : timescalestd/time/instant/timescale: V
  fun from-taifrom-tai: (tai : duration) -> timestamp(taitai: duration:durationstd/time/duration/duration: V)result: -> total timestamp { utc-sls-from-taistd/time/utc/utc-sls-from-tai: (leaps : leaps-table, smooth : timespan, tai-since : duration) -> timestamp(leapsleaps: leaps-table,smoothsmooth: timespan,taitai: duration) }
  fun to-taito-tai: (utc : timestamp) -> duration(utcutc: timestamp:timestampstd/time/timestamp/timestamp: V)result: -> total duration  { utc-sls-to-taistd/time/utc/utc-sls-to-tai: (leaps : leaps-table, smooth : timespan, sls : utc-timestamp) -> duration(leapsleaps: leaps-table,smoothsmooth: timespan,utcutc: timestamp) }
  timescalestd/time/instant/timescale: (name : string, from-tai : (duration) -> timestamp, to-tai : (timestamp) -> duration, unit : ? string, seconds-in-day : ? (maybe<(timestamp) -> timespan>), to-mjd2000 : ? (maybe<(t : timestamp, tzdelta : timespan) -> ddouble>), from-mjd2000 : ? (maybe<(days : int, frac : ddouble) -> timestamp>)) -> timescale(
    namename: string,
    from-taifrom-tai: (tai : duration) -> timestamp,
    to-taito-tai: (utc : timestamp) -> duration,
    "UTC-SLS"literal: string
count= 7
  )


// Create a new UTC-SLS time scale from a provided leap second table `leaps`.
// Implements a UTC time scale except without ever showing leap seconds.
// UTC-SLS is equivalent to UTC except for the last 1000 seconds of a day where
// a leap second occurs. On such day, the leap second time step (positive or negative)
// is distributed over the last 1000 seconds of the day. On the full hour, UTC
// and UTC-SLS are equal again.
//
// This is a recommended time scale to use for time stamps or communication
// with other services since it avoids any potential trouble
// with leap seconds while still being quite precise.
// See also: <https://www.cl.cam.ac.uk/~mgk25/time/utc-sls>.
//
// You can create a UTC-SLS time scale based on the latest IERS leap second
// data using [`cal-utc-sls-load`](std_time_download.html#cal_utc_sls_load).
pub fun ts-utc-sls-createstd/time/utc/ts-utc-sls-create: (leaps : leaps-table) -> timescale( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V )result: -> total timescale : timescalestd/time/instant/timescale: V
  utc-sls-timescalestd/time/utc/utc-sls-timescale: (name : string, leaps : leaps-table, smooth : ? timespan) -> timescale( "UTC-SLS"literal: string
count= 7, leapsleaps: leaps-table )

// TI time scale with smoothed leap seconds.\
// Implements a TI time scale (`ts-ti`) except without ever showing leap seconds.
// TI-SLS is equivalent to TI except for the last 1000 seconds of a day where
// a leap second occurs. On such day, the leap second time step (positive or negative)
// is distributed over the last 1000 seconds of the day. On the full hour, TI
// and TI-SLS are equal again.
pub val ts-ti-slsstd/time/utc/ts-ti-sls: timescale : timescalestd/time/instant/timescale: V = utc-sls-timescalestd/time/utc/utc-sls-timescale: (name : string, leaps : leaps-table, smooth : ? timespan) -> timescale( "TI-SLS"literal: string
count= 6, leaps-table-tistd/time/utc/leaps-table-ti: leaps-table )

/*----------------------------------------------------------------------------
  UTC to TAI conversion
----------------------------------------------------------------------------*/

fun utc-to-taistd/time/utc/utc-to-tai: (leaps : leaps-table, utc : timestamp) -> duration( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, utcutc: timestamp : timestampstd/time/timestamp/timestamp: V )result: -> total duration : durationstd/time/duration/duration: V
  val dtaidtai: timespan = utc-to-delta-taistd/time/utc/utc-to-delta-tai: (leaps : leaps-table, utc : utc-timestamp) -> timespan(leapsleaps: leaps-table,utcutc: timestamp)
  (utcutc: timestamp +std/time/timestamp/(+): (ts : timestamp, t : timespan) -> timestamp dtaidtai: timespan).unsafe-durationstd/time/duration/unsafe-duration: (t : timestamp) -> duration  // ok, because TAI seconds now


/* Converting TAI time back to UTC is not straigtforward as
we need to estimate UTC at first as the leap table goes from UTC-to-TAI.
Moreover, we need to detect if we crossed over a leap second, or are
inside a leap step. Take for example the leap second of 2006-01-01
to +33. This looks like:

UTC-to-TAI-delta:                        ... +32   |   +33 ...

UTC timestamp          189388799   189388799+1  189388800
UTC 2005-12-31T23:59:     59          60   leap    00
                 ---------|-----------|xxxxxxxxxxxx|-------------
                          |           |            |
TAI 2006-01-01T00:00:     31          32           33
TAI timestamp:         189388831   189388832    189388833

In the code below, suppose `tai` is `189388832.5`.
Then we estimate at first the delta `dtai0` to +33, so our
estimate `utc0` is `189388799.5` (just before the leap step!).
We then use `utc0` to get delta-TAI at that time, +32 and
set the difference `diff` to `(33-32) == 1` -- the time of the
leap second we crossed. (usually, `diff` is zero of course).
If the difference is positive, we then check if `utc0` is in the
leap period itself (instead of before it): that is the case if
the delta-TAI at `utc0+diff` equals `dtai0` again.
If we are not in a leap second, the final utc time is the
estimate plus the time of the leap period if we crossed over it, `utc0+diff`.
Otherwise, the same holds but we need to add `diff` as leap seconds,
in the example ending up as `189388799.5+1`.
*/
fun utc-from-taistd/time/utc/utc-from-tai: (leaps : leaps-table, tai-since : duration) -> timestamp( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, tai-sincetai-since: duration : durationstd/time/duration/duration: V )result: -> total timestamp : timestampstd/time/timestamp/timestamp: V
  val taitai: timestamp   = tai-sincetai-since: duration.timestampstd/time/duration/timestamp: (d : duration) -> timestamp
  // take tai==utc for an initial estimate
  val dtai0dtai0: timespan = utc-to-delta-taistd/time/utc/utc-to-delta-tai: (leaps : leaps-table, utc : utc-timestamp) -> timespan(leapsleaps: leaps-table,taitai: timestamp)
  val utc0utc0: timestamp  = taitai: timestamp -std/time/timestamp/(-): (ts : timestamp, t : timespan) -> timestamp dtai0dtai0: timespan
  // get delta-tai at the estimate
  val dtai1dtai1: timespan = utc-to-delta-taistd/time/utc/utc-to-delta-tai: (leaps : leaps-table, utc : utc-timestamp) -> timespan(leapsleaps: leaps-table,utc0utc0: timestamp)
  // check if we crossed over a leap-second moment
  val diffdiff: ddouble  = (dtai0dtai0: timespan -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> ddouble dtai1dtai1: timespan)
  // `inleap` is `True` if this time falls in the leap second gap itself
  val hasgaphasgap: bool = (diffdiff: ddouble.round-to-precstd/num/ddouble/round-to-prec: (x : ddouble, prec : int) -> ddouble(3literal: int
dec  = 3
hex8 = 0x03
bit8 = 0b00000011).is-posstd/num/ddouble/is-pos: (x : ddouble) -> bool)  // round to disregard a difference due to `drift`
  val inleapinleap: bool = (hasgaphasgap: bool &&std/core/types/(&&): (x : bool, y : bool) -> bool utc-to-delta-taistd/time/utc/utc-to-delta-tai: (leaps : leaps-table, utc : utc-timestamp) -> timespan(leapsleaps: leaps-table,utc0utc0: timestamp +std/time/timestamp/(+): (ts : timestamp, t : timespan) -> timestamp diffdiff: ddouble) !=std/num/ddouble/(!=): (x : ddouble, y : ddouble) -> bool dtai1dtai1: timespan)

  if !std/core/types/bool/(!): (b : bool) -> boolinleapinleap: bool then utc0utc0: timestamp +std/time/timestamp/(+): (ts : timestamp, t : timespan) -> timestamp diffdiff: ddouble else utc0utc0: timestamp.add-leap-secondsstd/time/timestamp/add-leap-seconds: (ts : timestamp, leaps : timespan) -> timestamp(diffdiff: ddouble)

// Return `Just(start,diff)` if a leap second occurred in the given day
// (`days` after 2000-01-01) with the start time and leap second gap (`diff`)
fun utc-leap-in-daystd/time/utc/utc-leap-in-day: (leaps : leaps-table, days : int) -> maybe<(timestamp, timespan)>( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, daysdays: int : intstd/core/types/int: V )result: -> total maybe<(timestamp, timespan)> : maybestd/core/types/maybe: V -> V<(std/core/types/tuple2: (V, V) -> Vtimestampstd/time/timestamp/timestamp: V,timespanstd/time/timestamp/timespan: V)>
  // check if there is a leap second in the day
  val utc0utc0: timestamp  = timestamp-daysstd/time/timestamp/timestamp-days: (days : int, secs : ? timespan, leap : ? int) -> timestamp(daysdays: int)
  val utc1utc1: timestamp  = timestamp-daysstd/time/timestamp/timestamp-days: (days : int, secs : ? timespan, leap : ? int) -> timestamp(daysdays: int +std/core/int/(+): (x : int, y : int) -> int 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001)
  val la1la1: leap-adjust   = utc-to-leap-adjuststd/time/utc/utc-to-leap-adjust: (leaps : leaps-table, utc : utc-timestamp) -> leap-adjust(leapsleaps: leaps-table,utc1utc1: timestamp)
  if la1la1: leap-adjust.utc-startstd/time/utc/leap-adjust/utc-start: (leap-adjust) -> utc-timestamp <std/time/timestamp/(<): (i : timestamp, j : timestamp) -> bool utc0utc0: timestamp then returnreturn: maybe<(timestamp, timespan)> Nothingstd/core/types/Nothing: forall<a> maybe<a>

  // if so, find the start and the timespan of the leap second
  val dtai0dtai0: timespan = utc-to-delta-taistd/time/utc/utc-to-delta-tai: (leaps : leaps-table, utc : utc-timestamp) -> timespan(leapsleaps: leaps-table,utc0utc0: timestamp)
  val dtai1dtai1: timespan = la1la1: leap-adjust.delta-taistd/time/utc/delta-tai: (la : leap-adjust, utc : utc-timestamp) -> timespan(utc1utc1: timestamp)
  val diffdiff: ddouble  = (dtai1dtai1: timespan -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> ddouble dtai0dtai0: timespan).round-to-precstd/num/ddouble/round-to-prec: (x : ddouble, prec : int) -> ddouble(3literal: int
dec  = 3
hex8 = 0x03
bit8 = 0b00000011)  // round to not take drift into account
  Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)la1la1: leap-adjust.utc-startstd/time/utc/leap-adjust/utc-start: (leap-adjust) -> utc-timestamp, diffdiff: ddouble)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b))

// The UTC seconds in a day
fun utc-seconds-in-daystd/time/utc/utc-seconds-in-day: (leaps : leaps-table, utc : timestamp) -> timespan( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, utcutc: timestamp : timestampstd/time/timestamp/timestamp: V )result: -> total timespan : timespanstd/time/timestamp/timespan: V
  match(utc-leap-in-daystd/time/utc/utc-leap-in-day: (leaps : leaps-table, days : int) -> maybe<(timestamp, timespan)>(leapsleaps: leaps-table,utcutc: timestamp.daysstd/time/timestamp/days: (ts : timestamp) -> int))
    Nothingstd/core/types/Nothing: forall<a> maybe<a> -> solar-secs-per-daystd/time/timestamp/solar-secs-per-day: timespan
    Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)_,diffdiff: timespan)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)) -> solar-secs-per-daystd/time/timestamp/solar-secs-per-day: timespan +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble diffdiff: timespan


// Return the modified julian day since 2000-01-01 taking leap seconds into
// account that happen any time during the day
fun utc-to-mjdstd/time/utc/utc-to-mjd: (leaps : leaps-table, utc : utc-timestamp, tzdelta : timespan) -> ddouble( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, utcutc: utc-timestamp : utc-timestampstd/time/utc/utc-timestamp: V, tzdeltatzdelta: timespan : timespanstd/time/timestamp/timespan: V )result: -> total ddouble : ddoublestd/num/ddouble/ddouble: V
  val (std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)days1days1: int,secs1secs1: ddouble)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b) = (utcutc: utc-timestamp +std/time/timestamp/(+): (ts : timestamp, t : timespan) -> timestamp tzdeltatzdelta: timespan).days-secondsstd/time/timestamp/days-seconds: (ts : timestamp) -> (int, ddouble)
  val fracfrac: ddouble = match(utc-leap-in-daystd/time/utc/utc-leap-in-day: (leaps : leaps-table, days : int) -> maybe<(timestamp, timespan)>(leapsleaps: leaps-table,utcutc: utc-timestamp.daysstd/time/timestamp/days: (ts : timestamp) -> int))
               Nothingstd/core/types/Nothing: forall<a> maybe<a> -> (secs1secs1: ddouble +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble utcutc: utc-timestamp.leapstd/time/timestamp/leap: (t : timestamp) -> int.ddoublestd/num/ddouble/int/ddouble: (i : int) -> ddouble) /std/num/ddouble/(/): (x : ddouble, y : ddouble) -> ddouble solar-secs-per-daystd/time/timestamp/solar-secs-per-day: timespan
               Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)startstart: timestamp,diffdiff: timespan)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)) ->
                 val secs-in-daysecs-in-day: ddouble = solar-secs-per-daystd/time/timestamp/solar-secs-per-day: timespan +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble diffdiff: timespan
                 val secssecs: ddouble = if utcutc: utc-timestamp <std/time/timestamp/(<): (i : timestamp, j : timestamp) -> bool startstart: timestamp then secs1secs1: ddouble +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble utcutc: utc-timestamp.leapstd/time/timestamp/leap: (t : timestamp) -> int.ddoublestd/num/ddouble/int/ddouble: (i : int) -> ddouble
                                             else secs1secs1: ddouble +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble diffdiff: timespan
                 (secssecs: ddouble /std/num/ddouble/(/): (x : ddouble, y : ddouble) -> ddouble secs-in-daysecs-in-day: ddouble)

  (days1days1: int.ddoublestd/num/ddouble/int/ddouble: (i : int) -> ddouble +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble fracfrac: ddouble)

// Return UTC from the modified julian day since 2000-01-01 taking leap seconds into
// account that happen any time during the day
fun utc-from-mjdstd/time/utc/utc-from-mjd: (leaps : leaps-table, days : int, frac : ddouble) -> utc-timestamp( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, daysdays: int : intstd/core/types/int: V, fracfrac: ddouble : ddoublestd/num/ddouble/ddouble: V )result: -> total utc-timestamp : utc-timestampstd/time/utc/utc-timestamp: V
  match(utc-leap-in-daystd/time/utc/utc-leap-in-day: (leaps : leaps-table, days : int) -> maybe<(timestamp, timespan)>(leapsleaps: leaps-table,daysdays: int))
    Nothingstd/core/types/Nothing: forall<a> maybe<a> -> timestamp-daysstd/time/timestamp/timestamp-days: (days : int, secs : ? timespan, leap : ? int) -> timestamp( daysdays: int, fracfrac: ddouble*std/num/ddouble/(*): (x : ddouble, y : ddouble) -> ddoublesolar-secs-per-daystd/time/timestamp/solar-secs-per-day: timespan)
    Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)startstart: timestamp,diffdiff: timespan)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)) ->
      val secssecs: ddouble = fracfrac: ddouble*std/num/ddouble/(*): (x : ddouble, y : ddouble) -> ddouble(solar-secs-per-daystd/time/timestamp/solar-secs-per-day: timespan +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble diffdiff: timespan)
      val utcutc: timestamp  = timestamp-daysstd/time/timestamp/timestamp-days: (days : int, secs : ? timespan, leap : ? int) -> timestamp(daysdays: int,secssecs: ddouble)
      if utcutc: timestamp <std/time/timestamp/(<): (i : timestamp, j : timestamp) -> bool startstart: timestamp then utcutc: timestamp
      elif utcutc: timestamp >std/time/timestamp/(>): (i : timestamp, j : timestamp) -> bool startstart: timestamp +std/time/timestamp/(+): (ts : timestamp, t : timespan) -> timestamp diffdiff: timespan then utcutc: timestamp -std/time/timestamp/(-): (ts : timestamp, t : timespan) -> timestamp diffdiff: timespan
      else (utcutc: timestamp -std/time/timestamp/(-): (ts : timestamp, t : timespan) -> timestamp diffdiff: timespan).add-leap-secondsstd/time/timestamp/add-leap-seconds: (ts : timestamp, leaps : timespan) -> timestamp(diffdiff: timespan)



/*----------------------------------------------------------------------------
  UTC-SLS to TAI conversion
----------------------------------------------------------------------------*/
fun utc-sls-leap-in-daystd/time/utc/utc-sls-leap-in-day: (leaps : leaps-table, smooth : timespan, utc : utc-timestamp) -> maybe<(timestamp, timestamp, timespan, timespan)>( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, smoothsmooth: timespan : timespanstd/time/timestamp/timespan: V, utcutc: utc-timestamp : utc-timestampstd/time/utc/utc-timestamp: V )result: -> total maybe<(timestamp, timestamp, timespan, timespan)> : maybestd/core/types/maybe: V -> V<(std/core/types/tuple4: (V, V, V, V) -> Vtimestampstd/time/timestamp/timestamp: V,timestampstd/time/timestamp/timestamp: V,timespanstd/time/timestamp/timespan: V,timespanstd/time/timestamp/timespan: V)>
  match(utc-leap-in-daystd/time/utc/utc-leap-in-day: (leaps : leaps-table, days : int) -> maybe<(timestamp, timespan)>(leapsleaps: leaps-table, utcutc: utc-timestamp.daysstd/time/timestamp/days: (ts : timestamp) -> int))
    Nothingstd/core/types/Nothing: forall<a> maybe<a> -> Nothingstd/core/types/Nothing: forall<a> maybe<a> // on non-leap days, utc-sls == utc
    Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)startstart: timestamp,diffdiff: timespan)std/core/types/Tuple2: forall<a,b> (fst : a, snd : b) -> (a, b)) ->
      val smooth-startsmooth-start: timestamp = (startstart: timestamp -std/time/timestamp/(-): (ts : timestamp, t : timespan) -> timestamp smoothsmooth: timespan) +std/time/timestamp/(+): (ts : timestamp, t : timespan) -> timestamp diffdiff: timespan
      val smooth-endsmooth-end: timestamp   = startstart: timestamp.add-leap-secondsstd/time/timestamp/add-leap-seconds: (ts : timestamp, leaps : timespan) -> timestamp(diffdiff: timespan)
      if utcutc: utc-timestamp <=std/time/timestamp/(<=): (i : timestamp, j : timestamp) -> bool smooth-startsmooth-start: timestamp then Nothingstd/core/types/Nothing: forall<a> maybe<a> // before the smoothing
      elif utcutc: utc-timestamp >std/time/timestamp/(>): (i : timestamp, j : timestamp) -> bool smooth-endsmooth-end: timestamp then Nothingstd/core/types/Nothing: forall<a> maybe<a> // after the leap second
      else
        val smooth-totalsmooth-total: ddouble = smooth-endsmooth-end: timestamp.timespan-noleapstd/time/timestamp/timespan-noleap: (ts : timestamp) -> timespan -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> ddouble smooth-startsmooth-start: timestamp.timespan-noleapstd/time/timestamp/timespan-noleap: (ts : timestamp) -> timespan
        val dtdt: ddouble = (utcutc: utc-timestamp.unsafe-timespan-withleapstd/time/timestamp/unsafe-timespan-withleap: (ts : timestamp) -> timespan -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> ddouble smooth-startsmooth-start: timestamp.timespan-noleapstd/time/timestamp/timespan-noleap: (ts : timestamp) -> timespan)
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)startstart: timestamp,smooth-startsmooth-start: timestamp,smooth-totalsmooth-total: ddouble,dtdt: ddouble)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d))



fun utc-sls-from-taistd/time/utc/utc-sls-from-tai: (leaps : leaps-table, smooth : timespan, tai-since : duration) -> timestamp( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, smoothsmooth: timespan : timespanstd/time/timestamp/timespan: V, tai-sincetai-since: duration : durationstd/time/duration/duration: V )result: -> total timestamp : timestampstd/time/timestamp/timestamp: V
  val utcutc: timestamp = utc-from-taistd/time/utc/utc-from-tai: (leaps : leaps-table, tai-since : duration) -> timestamp(leapsleaps: leaps-table,tai-sincetai-since: duration)
  match(utc-sls-leap-in-daystd/time/utc/utc-sls-leap-in-day: (leaps : leaps-table, smooth : timespan, utc : utc-timestamp) -> maybe<(timestamp, timestamp, timespan, timespan)>(leapsleaps: leaps-table, smoothsmooth: timespan, utcutc: timestamp))
    Nothingstd/core/types/Nothing: forall<a> maybe<a> -> utcutc: timestamp // outside smooth zone: utc-sls == utc
    Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)_start,smooth-startsmooth-start: timestamp,smooth-totalsmooth-total: timespan,dtdt: timespan)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)) ->
      val fracfrac: ddouble = dtdt: timespan /std/num/ddouble/(/): (x : ddouble, y : ddouble) -> ddouble smoothsmooth: timespan
      smooth-startsmooth-start: timestamp +std/time/timestamp/(+): (ts : timestamp, t : timespan) -> timestamp (fracfrac: ddouble *std/num/ddouble/(*): (x : ddouble, y : ddouble) -> ddouble smooth-totalsmooth-total: timespan)


fun utc-sls-to-taistd/time/utc/utc-sls-to-tai: (leaps : leaps-table, smooth : timespan, sls : utc-timestamp) -> duration( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, smoothsmooth: timespan : timespanstd/time/timestamp/timespan: V, slssls: utc-timestamp : utc-timestampstd/time/utc/utc-timestamp: V )result: -> total duration : durationstd/time/duration/duration: V
  val utcutc: utc-timestamp = match(utc-sls-leap-in-daystd/time/utc/utc-sls-leap-in-day: (leaps : leaps-table, smooth : timespan, utc : utc-timestamp) -> maybe<(timestamp, timestamp, timespan, timespan)>(leapsleaps: leaps-table,smoothsmooth: timespan,slssls: utc-timestamp))  // sls ~ utc
    Nothingstd/core/types/Nothing: forall<a> maybe<a> -> slssls: utc-timestamp  // utc == utc-sls outside smooth zone
    Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)startstart: timestamp,smooth-startsmooth-start: timestamp,smooth-totalsmooth-total: timespan,dtdt: timespan)std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)) ->
      val fracfrac: ddouble  = dtdt: timespan /std/num/ddouble/(/): (x : ddouble, y : ddouble) -> ddouble smooth-totalsmooth-total: timespan
      val utc0utc0: timestamp  = smooth-startsmooth-start: timestamp +std/time/timestamp/(+): (ts : timestamp, t : timespan) -> timestamp (fracfrac: ddouble *std/num/ddouble/(*): (x : ddouble, y : ddouble) -> ddouble smoothsmooth: timespan)
      if utc0utc0: timestamp <=std/time/timestamp/(<=): (i : timestamp, j : timestamp) -> bool startstart: timestamp then utc0utc0: timestamp else
        val ldiffldiff: ddouble = utc0utc0: timestamp.timespan-noleapstd/time/timestamp/timespan-noleap: (ts : timestamp) -> timespan -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> ddouble startstart: timestamp.timespan-noleapstd/time/timestamp/timespan-noleap: (ts : timestamp) -> timespan
        startstart: timestamp.add-leap-secondsstd/time/timestamp/add-leap-seconds: (ts : timestamp, leaps : timespan) -> timestamp(ldiffldiff: ddouble)


  utc-to-taistd/time/utc/utc-to-tai: (leaps : leaps-table, utc : timestamp) -> duration(leapsleaps: leaps-table,utcutc: utc-timestamp)


// -----------------------------------------------------------
// Leap second table
// -----------------------------------------------------------

// `:utc-timestamp` is UTC time since 2000-01-01
pub alias utc-timestampstd/time/utc/utc-timestamp: V = timestampstd/time/timestamp/timestamp: V

// A leap second table describes when UTC leap seconds occur.
abstract struct leaps-tablestd/time/utc/leaps-table: V(
  pub expirestd/time/utc/leaps-table/expire: (leaps-table) -> instant : instantstd/time/instant/instant: V,
  // List of adjustments, ordered from most recent to oldest (decreasing `utc-start`)
  // Each entry gives the start instant and integer leap second adjustment.
  adjustsstd/time/utc/leaps-table/adjusts: (leaps-table) -> list<leap-adjust>: liststd/core/types/list: V -> V<leap-adjuststd/time/utc/leap-adjust: V>
)

// Leap second adjustments. For an instant `i` after `start`:\
// ``TAI-offset = offset + (drift * days(i - drift-start))``
abstract struct leap-adjuststd/time/utc/leap-adjust: V(
  utc-startutc-start: utc-timestamp  : utc-timestampstd/time/utc/utc-timestamp: V,  // start time in NTP seconds since epoch (2000-01-01)
  offsetoffset: timespan     : timespanstd/time/timestamp/timespan: V,       // base offset
  drift-startdrift-start: utc-timestamp: utc-timestampstd/time/utc/utc-timestamp: V = timestamp0std/time/timestamp/timestamp0: timestamp,   // start of drift adjustment
  driftdrift: ddouble      : ddoublestd/num/ddouble/ddouble: V = ddouble/zerostd/num/ddouble/zero: ddouble
)

val leaps-table0std/time/utc/leaps-table0: leaps-table = Leaps-tablestd/time/utc/Leaps-table: (expire : instant, adjusts : list<leap-adjust>) -> leaps-table(epochstd/time/instant/epoch: instant,[std/core/types/Nil: forall<a> list<a>]std/core/types/Nil: forall<a> list<a>)
val zerostd/time/utc/zero: leap-adjust : leap-adjuststd/time/utc/leap-adjust: V = Leap-adjust(timestamp0std/time/timestamp/timestamp0: timestamp,timespan0std/time/timestamp/timespan0: timespan,timestamp0std/time/timestamp/timestamp0: timestamp,zerostd/num/ddouble/zero: ddouble)

fun is-zerostd/time/utc/is-zero: (la : leap-adjust) -> bool( lala: leap-adjust : leap-adjuststd/time/utc/leap-adjust: V )result: -> total bool : boolstd/core/types/bool: V
  lala: leap-adjust.offsetstd/time/utc/leap-adjust/offset: (leap-adjust) -> timespan.is-zerostd/num/ddouble/is-zero: (x : ddouble) -> bool &&std/core/types/(&&): (x : bool, y : bool) -> bool lala: leap-adjust.driftstd/time/utc/leap-adjust/drift: (leap-adjust) -> ddouble.is-zerostd/num/ddouble/is-zero: (x : ddouble) -> bool

pub fun leap-adjust/showstd/time/utc/leap-adjust/show: (l : leap-adjust) -> string( ll: leap-adjust : leap-adjuststd/time/utc/leap-adjust: V )result: -> total string : stringstd/core/types/string: V
  [std/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>ll: leap-adjust.utc-startstd/time/utc/leap-adjust/utc-start: (leap-adjust) -> utc-timestamp.showstd/time/instant/timestamp/show: (t : timestamp, max-prec : ? int, secs-width : ? int, unit : ? string) -> string,": offset: "literal: string
count= 10,ll: leap-adjust.offsetstd/time/utc/leap-adjust/offset: (leap-adjust) -> timespan.showstd/num/ddouble/show: (x : ddouble, prec : ? int) -> string,", drift-start: "literal: string
count= 15,ll: leap-adjust.drift-startstd/time/utc/leap-adjust/drift-start: (leap-adjust) -> utc-timestamp.showstd/time/instant/timestamp/show: (t : timestamp, max-prec : ? int, secs-width : ? int, unit : ? string) -> string,", drift: "literal: string
count= 9,ll: leap-adjust.driftstd/time/utc/leap-adjust/drift: (leap-adjust) -> ddouble.showstd/num/ddouble/show: (x : ddouble, prec : ? int) -> string]std/core/types/Nil: forall<a> list<a>.joinstd/core/list/join: (xs : list<string>) -> string

pub fun leaps-table/showstd/time/utc/leaps-table/show: (t : leaps-table) -> string( tt: leaps-table : leaps-tablestd/time/utc/leaps-table: V )result: -> total string : stringstd/core/types/string: V
  tt: leaps-table.adjustsstd/time/utc/leaps-table/adjusts: (leaps-table) -> list<leap-adjust>.mapstd/core/list/map: (xs : list<leap-adjust>, f : (leap-adjust) -> string) -> list<string>(showstd/time/utc/leap-adjust/show: (l : leap-adjust) -> string).unlinesstd/core/list/unlines: (xs : list<string>) -> string

/*----------------------------------------------------------------------------
  delta-TAI == TAI - UTC
----------------------------------------------------------------------------*/

val utc1958std/time/utc/utc1958: timestamp = timestampstd/time/timestamp/int/timestamp: (t : int, frac : ? float64, leap : ? int) -> timestamp(-1325376000literal: int
dec  = -1325376000
hex32= 0xB1005E00
bit32= 0b10110001000000000101111000000000) // 2000-01-01 - 1958-01-01 in NTP seconds

fun utc-to-delta-taistd/time/utc/utc-to-delta-tai: (leaps : leaps-table, utc : utc-timestamp) -> timespan( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, utcutc: utc-timestamp : utc-timestampstd/time/utc/utc-timestamp: V )result: -> total timespan : timespanstd/time/timestamp/timespan: V
  utc-to-leap-adjuststd/time/utc/utc-to-leap-adjust: (leaps : leaps-table, utc : utc-timestamp) -> leap-adjust(leapsleaps: leaps-table,utcutc: utc-timestamp).delta-taistd/time/utc/delta-tai: (la : leap-adjust, utc : utc-timestamp) -> timespan(utcutc: utc-timestamp)

fun utc-to-leap-adjuststd/time/utc/utc-to-leap-adjust: (leaps : leaps-table, utc : utc-timestamp) -> leap-adjust( leapsleaps: leaps-table : leaps-tablestd/time/utc/leaps-table: V, utcutc: utc-timestamp : utc-timestampstd/time/utc/utc-timestamp: V )result: -> total leap-adjust : leap-adjuststd/time/utc/leap-adjust: V
  if utcutc: utc-timestamp <std/time/timestamp/(<): (i : timestamp, j : timestamp) -> bool utc1958std/time/utc/utc1958: timestamp
   then zerostd/time/utc/zero: leap-adjust
   else find-leap-adjuststd/time/utc/find-leap-adjust: (utc : utc-timestamp, leaps : list<leap-adjust>) -> leap-adjust(utcutc: utc-timestamp,leapsleaps: leaps-table.adjustsstd/time/utc/leaps-table/adjusts: (leaps-table) -> list<leap-adjust>)

fun find-leap-adjuststd/time/utc/find-leap-adjust: (utc : utc-timestamp, leaps : list<leap-adjust>) -> leap-adjust( utcutc: utc-timestamp : utc-timestampstd/time/utc/utc-timestamp: V, leapsleaps: list<leap-adjust> : liststd/core/types/list: V -> V<leap-adjuststd/time/utc/leap-adjust: V> )result: -> total leap-adjust : leap-adjuststd/time/utc/leap-adjust: V
  match leapsleaps: list<leap-adjust>
    Nilstd/core/types/Nil: forall<a> list<a> -> zerostd/time/utc/zero: leap-adjust // should never happen
    Consstd/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(lala: leap-adjust,earlierearlier: list<leap-adjust>) ->
      if lala: leap-adjust.utc-startstd/time/utc/leap-adjust/utc-start: (leap-adjust) -> utc-timestamp >std/time/timestamp/(>): (i : timestamp, j : timestamp) -> bool utcutc: utc-timestamp
       then find-leap-adjuststd/time/utc/find-leap-adjust: (utc : utc-timestamp, leaps : list<leap-adjust>) -> leap-adjust(utcutc: utc-timestamp,earlierearlier: list<leap-adjust>)
       else lala: leap-adjust


// Get the leap-second adjustment _delta-tai_ (= TAI - UTC).
// Needs the timestamp to handle _drift_.
fun delta-taistd/time/utc/delta-tai: (la : leap-adjust, utc : utc-timestamp) -> timespan( lala: leap-adjust : leap-adjuststd/time/utc/leap-adjust: V, utcutc: utc-timestamp : utc-timestampstd/time/utc/utc-timestamp: V )result: -> total timespan : timespanstd/time/timestamp/timespan: V
  if lala: leap-adjust.driftstd/time/utc/leap-adjust/drift: (leap-adjust) -> ddouble.is-zerostd/num/ddouble/is-zero: (x : ddouble) -> bool then lala: leap-adjust.offsetstd/time/utc/leap-adjust/offset: (leap-adjust) -> timespan else
    // pre 1972 is a rubber leap second
    val daysdays: ddouble = (utcutc: utc-timestamp.timespan-noleapstd/time/timestamp/timespan-noleap: (ts : timestamp) -> timespan -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> ddouble lala: leap-adjust.drift-startstd/time/utc/leap-adjust/drift-start: (leap-adjust) -> utc-timestamp.timespan-noleapstd/time/timestamp/timespan-noleap: (ts : timestamp) -> timespan) /std/num/ddouble/(/): (x : ddouble, y : ddouble) -> ddouble solar-secs-per-daystd/time/timestamp/solar-secs-per-day: timespan
    lala: leap-adjust.offsetstd/time/utc/leap-adjust/offset: (leap-adjust) -> timespan +std/num/ddouble/(+): (x : ddouble, y : ddouble) -> ddouble (lala: leap-adjust.driftstd/time/utc/leap-adjust/drift: (leap-adjust) -> ddouble *std/num/ddouble/(*): (x : ddouble, y : ddouble) -> ddouble daysdays: ddouble)


/*----------------------------------------------------------------------------
  Default leap tables
----------------------------------------------------------------------------*/

// Leap second table upto (but not including) 1972-01-01 UTC
pub val leaps-table-pre1972std/time/utc/leaps-table-pre1972: leaps-table : leaps-tablestd/time/utc/leaps-table: V =
  parse-leap-seconds-datstd/time/utc/parse-leap-seconds-dat: (leaps : string) -> leaps-table( default-leap-seconds-pre72std/time/utc/default-leap-seconds-pre72: string )

// Default TI leaps table has leap second information up to the compiler release (currently `leaps-table-y2017`).
pub val leaps-table-tistd/time/utc/leaps-table-ti: leaps-table : leaps-tablestd/time/utc/leaps-table: V =
  val post72post72: leaps-table = parse-leap-secondsstd/time/utc/parse-leap-seconds: (leaps : string) -> leaps-table( default-iers-leap-secondsstd/time/utc/default-iers-leap-seconds: string )
  post72post72: leaps-table.extendstd/time/utc/extend: (leap1 : leaps-table, leap2 : leaps-table) -> leaps-table(leaps-table-pre1972std/time/utc/leaps-table-pre1972: leaps-table)

// Leap second table up to 2017-01-01Z.
pub val leaps-table-y2017std/time/utc/leaps-table-y2017: leaps-table : leaps-tablestd/time/utc/leaps-table: V = leaps-table-tistd/time/utc/leaps-table-ti: leaps-table.uptostd/time/utc/upto: (lt : leaps-table, end : utc-timestamp) -> leaps-table(536544000literal: int
dec  = 536544000
hex32= 0x1FFB0300
bit32= 0b00011111111110110000001100000000.timestampstd/time/timestamp/int/timestamp: (t : int, frac : ? float64, leap : ? int) -> timestamp)  // == instant(2017,1,1).timestamp(ts-ti)

pub fun extendstd/time/utc/extend: (leap1 : leaps-table, leap2 : leaps-table) -> leaps-table(leap1leap1: leaps-table : leaps-tablestd/time/utc/leaps-table: V, leap2leap2: leaps-table : leaps-tablestd/time/utc/leaps-table: V)result: -> total leaps-table : leaps-tablestd/time/utc/leaps-table: V
  match leap1leap1: leaps-table.adjustsstd/time/utc/leaps-table/adjusts: (leaps-table) -> list<leap-adjust>.reversestd/core/list/reverse: (xs : list<leap-adjust>) -> list<leap-adjust>
    Nilstd/core/types/Nil: forall<a> list<a> -> leap2leap2: leaps-table
    Consstd/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(lala: leap-adjust,_) ->
      leap1leap1: leaps-table( adjusts = leap1leap1: leaps-table.adjustsstd/time/utc/leaps-table/adjusts: (leaps-table) -> list<leap-adjust> ++std/core/list/(++): (xs : list<leap-adjust>, ys : list<leap-adjust>) -> list<leap-adjust> leap2leap2: leaps-table.uptostd/time/utc/upto: (lt : leaps-table, end : utc-timestamp) -> leaps-table(lala: leap-adjust.utc-startstd/time/utc/leap-adjust/utc-start: (leap-adjust) -> utc-timestamp -std/time/timestamp/(-): (ts : timestamp, t : timespan) -> timestamp 1literal: int
dec  = 1
hex8 = 0x01
bit8 = 0b00000001.timespanstd/time/timestamp/int/timespan: (seconds : int, frac : ? float64) -> timespan).adjustsstd/time/utc/leaps-table/adjusts: (leaps-table) -> list<leap-adjust> )


fun uptostd/time/utc/upto: (lt : leaps-table, end : utc-timestamp) -> leaps-table( ltlt: leaps-table : leaps-tablestd/time/utc/leaps-table: V, endend: utc-timestamp : utc-timestampstd/time/utc/utc-timestamp: V )result: -> total leaps-table : leaps-tablestd/time/utc/leaps-table: V
  ltlt: leaps-table( adjusts = ltlt: leaps-table.adjustsstd/time/utc/leaps-table/adjusts: (leaps-table) -> list<leap-adjust>.drop-whilestd/core/list/drop-while: (xs : list<leap-adjust>, predicate : (leap-adjust) -> bool) -> list<leap-adjust>(fnfn: (la : leap-adjust) -> bool(lala: leap-adjust) { lala: leap-adjust.utc-startstd/time/utc/leap-adjust/utc-start: (leap-adjust) -> utc-timestamp >std/time/timestamp/(>): (i : timestamp, j : timestamp) -> bool endend: utc-timestamp }) )

// Get a list of leap second steps in a triple, NTP start time, offset just before, and the new offset at that time,
// the base offset, the drift start date and the drift rate.
pub fun get-leap-stepsstd/time/utc/get-leap-steps: (table : ? leaps-table) -> list<(utc-timestamp, timespan, timespan, (timespan, utc-timestamp, ddouble))>( tabletable: ? leaps-table : leaps-tablestd/time/utc/leaps-table: V = leaps-table-tistd/time/utc/leaps-table-ti: leaps-table )result: -> total list<(utc-timestamp, timespan, timespan, (timespan, utc-timestamp, ddouble))> : liststd/core/types/list: V -> V<(std/core/types/tuple4: (V, V, V, V) -> Vutc-timestampstd/time/utc/utc-timestamp: V,timespanstd/time/timestamp/timespan: V,timespanstd/time/timestamp/timespan: V,(std/core/types/tuple3: (V, V, V) -> Vtimespanstd/time/timestamp/timespan: V,utc-timestampstd/time/utc/utc-timestamp: V,ddoublestd/num/ddouble/ddouble: V))>
  val adjustsadjusts: list<leap-adjust> = tabletable: leaps-table.adjustsstd/time/utc/leaps-table/adjusts: (leaps-table) -> list<leap-adjust>.reversestd/core/list/reverse: (xs : list<leap-adjust>) -> list<leap-adjust>
  zipstd/core/list/zip: (xs : list<leap-adjust>, ys : list<leap-adjust>) -> list<(leap-adjust, leap-adjust)>(Consstd/core/types/Cons: forall<a> (head : a, tail : list<a>) -> list<a>(utc/zerostd/time/utc/zero: leap-adjust,adjustsadjusts: list<leap-adjust>),adjustsadjusts: list<leap-adjust>).mapstd/core/list/map: (xs : list<(leap-adjust, leap-adjust)>, f : ((leap-adjust, leap-adjust)) -> (utc-timestamp, timespan, timespan, (timespan, utc-timestamp, ddouble))) -> list<(utc-timestamp, timespan, timespan, (timespan, utc-timestamp, ddouble))> fnfn: (las : (leap-adjust, leap-adjust)) -> (utc-timestamp, timespan, timespan, (timespan, utc-timestamp, ddouble))(laslas: (leap-adjust, leap-adjust))
    val startstart: utc-timestamp = laslas: (leap-adjust, leap-adjust).sndstd/core/types/tuple2/snd: (tuple2 : (leap-adjust, leap-adjust)) -> leap-adjust.utc-startstd/time/utc/leap-adjust/utc-start: (leap-adjust) -> utc-timestamp
    val ofs1ofs1: timespan = laslas: (leap-adjust, leap-adjust).fststd/core/types/tuple2/fst: (tuple2 : (leap-adjust, leap-adjust)) -> leap-adjust.delta-taistd/time/utc/delta-tai: (la : leap-adjust, utc : utc-timestamp) -> timespan(startstart: utc-timestamp)
    val ofs2ofs2: timespan = laslas: (leap-adjust, leap-adjust).sndstd/core/types/tuple2/snd: (tuple2 : (leap-adjust, leap-adjust)) -> leap-adjust.delta-taistd/time/utc/delta-tai: (la : leap-adjust, utc : utc-timestamp) -> timespan(startstart: utc-timestamp)
    (std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)startstart: utc-timestamp,ofs1ofs1: timespan,ofs2ofs2: timespan,(std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)laslas: (leap-adjust, leap-adjust).sndstd/core/types/tuple2/snd: (tuple2 : (leap-adjust, leap-adjust)) -> leap-adjust.offsetstd/time/utc/leap-adjust/offset: (leap-adjust) -> timespan,laslas: (leap-adjust, leap-adjust).sndstd/core/types/tuple2/snd: (tuple2 : (leap-adjust, leap-adjust)) -> leap-adjust.drift-startstd/time/utc/leap-adjust/drift-start: (leap-adjust) -> utc-timestamp,laslas: (leap-adjust, leap-adjust).sndstd/core/types/tuple2/snd: (tuple2 : (leap-adjust, leap-adjust)) -> leap-adjust.driftstd/time/utc/leap-adjust/drift: (leap-adjust) -> ddouble)std/core/types/Tuple3: forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c))std/core/types/Tuple4: forall<a,b,c,d> (fst : a, snd : b, thd : c, field4 : d) -> (a, b, c, d)


// -----------------------------------------------------------
// Parsing UTC leap second tables
// -----------------------------------------------------------

// Parse a leap second table from text `leaps` in the  [IERS leap second][iersl]
// file format.

pub fun parse-leap-secondsstd/time/utc/parse-leap-seconds: (leaps : string) -> leaps-table( leapsleaps: string : stringstd/core/types/string: V )result: -> total leaps-table : leaps-tablestd/time/utc/leaps-table: V
  val adjustsadjusts: list<leap-adjust> = leapsleaps: string.linesstd/core/list/lines: (s : string) -> list<string>.flatmap-maybestd/core/list/flatmap-maybe: (xs : list<string>, f : (string) -> maybe<leap-adjust>) -> list<leap-adjust>(parse-leapstd/time/utc/parse-leap: (line : string) -> maybe<leap-adjust>).reversestd/core/list/reverse: (xs : list<leap-adjust>) -> list<leap-adjust>
  val expireexpire: instant = parse-leap-expirestd/time/utc/parse-leap-expire: (leaps : string, adjusts : list<leap-adjust>) -> instant(leapsleaps: string,adjustsadjusts: list<leap-adjust>)
  Leaps-tablestd/time/utc/Leaps-table: (expire : instant, adjusts : list<leap-adjust>) -> leaps-table(expireexpire: instant,adjustsadjusts: list<leap-adjust>)

fun parse-leapstd/time/utc/parse-leap: (line : string) -> maybe<leap-adjust>( lineline: string : stringstd/core/types/string: V )result: -> total maybe<leap-adjust> : maybestd/core/types/maybe: V -> V<leap-adjuststd/time/utc/leap-adjust: V>
  if (lineline: string.trim-leftstd/core/sslice/trim-left: (s : string, sub : string) -> string(" "literal: string
count= 1).starts-withstd/core/sslice/starts-with: (s : string, pre : string) -> maybe<sslice>("#"literal: string
count= 1).is-juststd/core/types/is-just: (maybe : maybe<sslice>) -> bool)
   then Nothingstd/core/types/Nothing: forall<a> maybe<a>
   else lineline: string.slicestd/core/sslice/slice: (s : string) -> sslice.parsestd/text/parse/parse: (input0 : sslice, p : () -> parse leap-adjust) -> parse-error<leap-adjust>(pleapstd/time/utc/pleap: () -> parse leap-adjust).maybestd/text/parse/maybe: (perr : parse-error<leap-adjust>) -> maybe<leap-adjust>

fun pleapstd/time/utc/pleap: () -> parse leap-adjust()result: -> parse leap-adjust : parsestd/text/parse/parse: (E, V) -> V leap-adjuststd/time/utc/leap-adjust: V
  whitespace0std/text/parse/whitespace0: () -> parse string()
  val ntpsecsntpsecs: int = pintstd/text/parse/pint: () -> parse int()
  whitespacestd/text/parse/whitespace: () -> parse string()
  val adjustadjust: int = pintstd/text/parse/pint: () -> parse int()
  // trace("leap entry: " ++ adjust.show ++ " - " ++ ntpsecs.show )
  Leap-adjust(timestampstd/time/timestamp/timestamp: (t : timespan, leap : ? int) -> parse timestamp(ntpsecsntpsecs: int.timespanstd/time/timestamp/int/timespan: (seconds : int, frac : ? float64) -> parse timespan -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> parse ddouble ntp2000std/time/utc/ntp2000: timespan), adjustadjust: int.timespanstd/time/timestamp/int/timespan: (seconds : int, frac : ? float64) -> parse timespan, timestamp0std/time/timestamp/timestamp0: timestamp, timespan0std/time/timestamp/timespan0: timespan)

/*
pub fun parse-leap-seconds( leaps : string ) : leaps-table
  // get leap second adjustments
  val adjusts = leaps.find-all(rxleap).map fn(cap)
    val ntpsecs = cap.groups[1].parse-int-default(0)
    val adjust  = cap.groups[2].parse-int-default(0)
    // trace("leap entry: " ++ adjust.show ++ " - " ++ ntpsecs.show )
    Leap-adjust(timestamp(ntpsecs.timespan - ntp2000), adjust.timespan, timestamp0, timespan0)
  }.reverse

  val expire = parse-leap-expire(leaps,adjusts)
  val table = Leaps-table(expire,adjusts)
  table

val rxleap   = regex(r"^[ \t]*(\d+)[ \t]+(\d+)[ \t]*(?:#.*)?$",multiLine=True)
*/

// IERS leap second data valid until 2024-12-28
val default-iers-leap-secondsstd/time/utc/default-iers-leap-seconds: string = "\n  # From: https://hpiers.obspm.fr/iers/bul/bulc/ntp/leap-seconds.list\n  #\tUpdated through IERS Bulletin C (https://hpiers.obspm.fr/iers/bul/bulc/bulletinc.dat)\n  # File expires on:  28 December 2024\n  #\n  #@\t3944332800\n  #\n  2272060800  10  # 1 Jan 1972\n  2287785600  11  # 1 Jul 1972\n  2303683200  12  # 1 Jan 1973\n  2335219200  13  # 1 Jan 1974\n  2366755200  14  # 1 Jan 1975\n  2398291200  15  # 1 Jan 1976\n  2429913600  16  # 1 Jan 1977\n  2461449600  17  # 1 Jan 1978\n  2492985600  18  # 1 Jan 1979\n  2524521600  19  # 1 Jan 1980\n  2571782400  20  # 1 Jul 1981\n  2603318400  21  # 1 Jul 1982\n  2634854400  22  # 1 Jul 1983\n  2698012800  23  # 1 Jul 1985\n  2776982400  24  # 1 Jan 1988\n  2840140800  25  # 1 Jan 1990\n  2871676800  26  # 1 Jan 1991\n  2918937600  27  # 1 Jul 1992\n  2950473600  28  # 1 Jul 1993\n  2982009600  29  # 1 Jul 1994\n  3029443200  30  # 1 Jan 1996\n  3076704000  31  # 1 Jul 1997\n  3124137600  32  # 1 Jan 1999\n  3345062400  33  # 1 Jan 2006\n  3439756800  34  # 1 Jan 2009\n  3550089600  35  # 1 Jul 2012\n  3644697600  36  # 1 Jul 2015\n  3692217600  37  # 1 Jan 2017\n  // 3723753600  35  # 1 Jan 2018"literal: string
count= 1125 //testing negative 2 seconds

// -----------------------------------------------------------
// Parsing TAI 'continuous' leap second tables from before 1972
// -----------------------------------------------------------

val jd-epoch-shiftstd/time/utc/jd-epoch-shift: timespan     = 2400000.5literal: float64
hex64= 0x1.24f804p21.timespanstd/time/timestamp/float64/timespan: (secs : float64) -> timespan  // JD to MJD
val mjd-epoch-shiftstd/time/utc/mjd-epoch-shift: timespan    = 51544literal: int
dec  = 51544
hex32= 0x0000C958
bit32= 0b00000000000000001100100101011000.timespanstd/time/timestamp/int/timespan: (seconds : int, frac : ? float64) -> timespan // 2000-01-01Z - 1858-11-17Z modified julian date epoch

// Parse the standard UTC leap second adjustment file in the "old" .dat format as
// in <https://maia.usno.navy.mil/ser7/tai-utc.dat>, where entries have the shape
// ````
// 1961 JAN  1 =JD 2437300.5  TAI-UTC=   1.4228180 S + (MJD - 37300.) X 0.001296 S
// ````
// which specifies the start time (`JD 2437300.5`), new TAI-UTC offset
// (`1.4228180`s), and the drift, starting at `37300` MJD of 0.001296s per day.
// Lines that start with ``#`` are comments. As an extension you can have an
// expiration date on a line that starts with ``#@`` followed by seconds since
// the NTP epoch (1900-01-01). Just as in a standard IERS leap second file.
pub fun parse-leap-seconds-datstd/time/utc/parse-leap-seconds-dat: (leaps : string) -> leaps-table( leapsleaps: string : stringstd/core/types/string: V  )result: -> total leaps-table : leaps-tablestd/time/utc/leaps-table: V
  val adjustsadjusts: list<leap-adjust> = leapsleaps: string.linesstd/core/list/lines: (s : string) -> list<string>.flatmap-maybestd/core/list/flatmap-maybe: (xs : list<string>, f : (string) -> maybe<leap-adjust>) -> list<leap-adjust>(parse-taiadjuststd/time/utc/parse-taiadjust: (line : string) -> maybe<leap-adjust>).reversestd/core/list/reverse: (xs : list<leap-adjust>) -> list<leap-adjust>
  val expireexpire: instant = parse-leap-expirestd/time/utc/parse-leap-expire: (leaps : string, adjusts : list<leap-adjust>) -> instant(leapsleaps: string,adjustsadjusts: list<leap-adjust>)
  Leaps-tablestd/time/utc/Leaps-table: (expire : instant, adjusts : list<leap-adjust>) -> leaps-table(expireexpire: instant,adjustsadjusts: list<leap-adjust>)

fun parse-leap-expirestd/time/utc/parse-leap-expire: (leaps : string, adjusts : list<leap-adjust>) -> instant( leapsleaps: string : stringstd/core/types/string: V, adjustsadjusts: list<leap-adjust> : liststd/core/types/list: V -> V<leap-adjuststd/time/utc/leap-adjust: V>)result: -> total instant : instantstd/time/instant/instant: V
  // get expiration date
  val la-finalla-final: leap-adjust    = adjustsadjusts: list<leap-adjust>.headstd/core/list/head: (xs : list<leap-adjust>) -> maybe<leap-adjust>.defaultstd/core/maybe/default: (m : maybe<leap-adjust>, nothing : leap-adjust) -> leap-adjust(zerostd/time/utc/zero: leap-adjust)
  val utc-expiresutc-expires: list<timestamp> = leapsleaps: string.linesstd/core/list/lines: (s : string) -> list<string>.flatmap-maybestd/core/list/flatmap-maybe: (xs : list<string>, f : (string) -> maybe<timestamp>) -> list<timestamp>(parse-expirestd/time/utc/parse-expire: (line : string) -> maybe<timestamp>)
  val utc-expireutc-expire: timestamp  = utc-expiresutc-expires: list<timestamp>.headstd/core/list/head: (xs : list<timestamp>) -> maybe<timestamp>.defaultstd/core/maybe/default: (m : maybe<timestamp>, nothing : timestamp) -> timestamp(la-finalla-final: leap-adjust.utc-startstd/time/utc/leap-adjust/utc-start: (leap-adjust) -> utc-timestamp +std/time/timestamp/(+): (ts : timestamp, t : timespan) -> timestamp (182literal: int
dec  = 182
hex16= 0x00B6
bit16= 0b0000000010110110*std/core/int/(*): (int, int) -> intisolar-secs-per-daystd/time/timestamp/isolar-secs-per-day: int).timespanstd/time/timestamp/int/timespan: (seconds : int, frac : ? float64) -> timespan)  // default: 6 months after last leap second
  ts-taistd/time/instant/ts-tai: timescale.instantstd/time/instant/timescale/instant: (ts : timescale, t : timestamp) -> instant( utc-expireutc-expire: timestamp -std/time/timestamp/(-): (ts : timestamp, t : timespan) -> timestamp ntp2000std/time/utc/ntp2000: timespan +std/time/timestamp/(+): (ts : timestamp, t : timespan) -> timestamp la-finalla-final: leap-adjust.offsetstd/time/utc/leap-adjust/offset: (leap-adjust) -> timespan ) // interpret as TAI to avoid recursion.

// val rxexpire = regex(r"^[ \t]*#@[ \t]*(\d+)[ \t]*(?:#.*)?$", multiLine=True)
fun parse-expirestd/time/utc/parse-expire: (line : string) -> maybe<timestamp>( lineline: string : stringstd/core/types/string: V )result: -> total maybe<timestamp> : maybestd/core/types/maybe: V -> V<timestampstd/time/timestamp/timestamp: V>
  if (lineline: string.trim-leftstd/core/sslice/trim-left: (s : string, sub : string) -> string(" "literal: string
count= 1).starts-withstd/core/sslice/starts-with: (s : string, pre : string) -> maybe<sslice>("#@"literal: string
count= 2).is-juststd/core/types/is-just: (maybe : maybe<sslice>) -> bool)
   then lineline: string.slicestd/core/sslice/slice: (s : string) -> sslice.parsestd/text/parse/parse: (input0 : sslice, p : () -> parse timestamp) -> parse-error<timestamp>(pexpirestd/time/utc/pexpire: () -> parse timestamp).maybestd/text/parse/maybe: (perr : parse-error<timestamp>) -> maybe<timestamp>
   else Nothingstd/core/types/Nothing: forall<a> maybe<a>

fun pexpirestd/time/utc/pexpire: () -> parse timestamp()result: -> parse timestamp : parsestd/text/parse/parse: (E, V) -> V timestampstd/time/timestamp/timestamp: V
  whitespace0std/text/parse/whitespace0: () -> parse string()
  pstringstd/text/parse/pstring: (s : string) -> parse string("#@"literal: string
count= 2)
  whitespace0std/text/parse/whitespace0: () -> parse string()
  val ntpexntpex: ddouble = pddoublestd/num/ddouble/pddouble: () -> parse ddouble()
  timestampstd/time/timestamp/timestamp: (t : timespan, leap : ? int) -> parse timestamp(ntpexntpex: ddouble.timespanstd/time/timestamp/ddouble/timespan: (secs : ddouble) -> parse timespan -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> parse ddouble ntp2000std/time/utc/ntp2000: timespan)

fun parse-taiadjuststd/time/utc/parse-taiadjust: (line : string) -> maybe<leap-adjust>( lineline: string : stringstd/core/types/string: V )result: -> total maybe<leap-adjust> : maybestd/core/types/maybe: V -> V<leap-adjuststd/time/utc/leap-adjust: V>
  lineline: string.slicestd/core/sslice/slice: (s : string) -> sslice.parse-eofstd/text/parse/parse-eof: (input : sslice, p : () -> parse leap-adjust) -> parse-error<leap-adjust>(ptaiadjuststd/time/utc/ptaiadjust: () -> parse leap-adjust).maybestd/text/parse/maybe: (perr : parse-error<leap-adjust>) -> maybe<leap-adjust>

fun ptaiadjuststd/time/utc/ptaiadjust: () -> parse leap-adjust()result: -> parse leap-adjust : parsestd/text/parse/parse: (E, V) -> V leap-adjuststd/time/utc/leap-adjust: V
  whitespace0std/text/parse/whitespace0: () -> parse string()
  many1std/text/parse/many1: (p : parser<total,char>) -> parse list<char>{ none-ofstd/text/parse/none-of: (chars : string) -> parse char("="literal: string
count= 1) }
  pstringstd/text/parse/pstring: (s : string) -> parse string("=JD"literal: string
count= 3)
  whitespace0std/text/parse/whitespace0: () -> parse string()
  val mjdmjd: ddouble = pddoublestd/num/ddouble/pddouble: () -> parse ddouble() -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> parse ddouble jd-epoch-shiftstd/time/utc/jd-epoch-shift: timespan
  whitespace0std/text/parse/whitespace0: () -> parse string()
  pstringstd/text/parse/pstring: (s : string) -> parse string("TAI-UTC="literal: string
count= 8)
  whitespace0std/text/parse/whitespace0: () -> parse string()
  val ofsofs: ddouble = pddoublestd/num/ddouble/pddouble: () -> parse ddouble()
  many1std/text/parse/many1: (p : parser<total,char>) -> parse list<char>{ no-digitstd/text/parse/no-digit: () -> parse char() }
  val dmjddmjd: ddouble = pddoublestd/num/ddouble/pddouble: () -> parse ddouble()
  many1std/text/parse/many1: (p : parser<total,char>) -> parse list<char>{ no-digitstd/text/parse/no-digit: () -> parse char() }
  val driftdrift: ddouble = pddoublestd/num/ddouble/pddouble: () -> parse ddouble()
  whitespace0std/text/parse/whitespace0: () -> parse string()
  pstringstd/text/parse/pstring: (s : string) -> parse string("S"literal: string
count= 1)
  whitespace0std/text/parse/whitespace0: () -> parse string()
  // round to always start on a whole second
  val startstart: timestamp  = ((mjdmjd: ddouble -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> parse ddouble mjd-epoch-shiftstd/time/utc/mjd-epoch-shift: timespan)*std/num/ddouble/(*): (x : ddouble, y : ddouble) -> parse ddoublesolar-secs-per-daystd/time/timestamp/solar-secs-per-day: timespan).roundstd/num/ddouble/round: (x : ddouble) -> parse ddouble.timestampstd/time/timestamp/timestamp: (t : timespan, leap : ? int) -> parse timestamp
  val dstartdstart: timestamp = ((dmjddmjd: ddouble -std/num/ddouble/(-): (x : ddouble, y : ddouble) -> parse ddouble mjd-epoch-shiftstd/time/utc/mjd-epoch-shift: timespan)*std/num/ddouble/(*): (x : ddouble, y : ddouble) -> parse ddoublesolar-secs-per-daystd/time/timestamp/solar-secs-per-day: timespan).roundstd/num/ddouble/round: (x : ddouble) -> parse ddouble.timestampstd/time/timestamp/timestamp: (t : timespan, leap : ? int) -> parse timestamp
  // trace("pre72 start=" + start.show + ", ofs: " + ofs.show + ", drift: " + drift.show )
  Leap-adjust( startstart: timestamp, ofsofs: ddouble, dstartdstart: timestamp, driftdrift: ddouble )

// TAI leap second adjustments for dates before 1972-01-01Z are linear interpolations.
// TAI started in 1958-01-01Z. The initial official UTC time step in 1961-01-01Z was 1.422818s and before that there
// were small steps of 20ms. See Explanatory Supplement to the Astronomical Almanac, 1992 edition, pages 86--87.
// In 1958, the supplement remarks that WWC operated at an offset of _about_ -100e-10, we
// change it to -85e-10 to end up with TAI-UTC == 0 at 1958-01-01.
// (without a rate change it is a negative -0.0472380s).
// Note the JD dates are at 0.29167 as the time steps were usually at 19:00h instead of midnight.
val default-leap-seconds-pre72std/time/utc/default-leap-seconds-pre72: string = "\n  # from: Explanatory Supplement to the Astronomical Almanac, 1992 edition, pages 86--87.\n  1958 JAN  1 =JD 2436204.5     TAI-UTC= 0.0  S + (MJD - 36204.) X 0.00073458 S\n  1958 JAN 15 =JD 2436219.29167 TAI-UTC= 0.02 S + (MJD - 36204.) X 0.00073458 S\n  1958 FEB  5 =JD 2436240.29167 TAI-UTC= 0.04 S + (MJD - 36204.) X 0.00073458 S\n  1958 FEB 19 =JD 2436254.29167 TAI-UTC= 0.06 S + (MJD - 36204.) X 0.00073458 S\n  1958 APR  9 =JD 2436303.29167 TAI-UTC= 0.08 S + (MJD - 36204.) X 0.00073458 S\n  1958 JUN 11 =JD 2436366.29167 TAI-UTC= 0.10 S + (MJD - 36204.) X 0.00073458 S\n  1958 JUL  2 =JD 2436387.29167 TAI-UTC= 0.12 S + (MJD - 36204.) X 0.00073458 S\n  1958 JUL 16 =JD 2436401.29167 TAI-UTC= 0.14 S + (MJD - 36204.) X 0.00073458 S\n  1958 OCT 22 =JD 2436499.29167 TAI-UTC= 0.16 S + (MJD - 36204.) X 0.00073458 S\n  1958 NOV 26 =JD 2436534.29167 TAI-UTC= 0.18 S + (MJD - 36204.) X 0.00073458 S\n  1958 DEC 24 =JD 2436562.29167 TAI-UTC= 0.20 S + (MJD - 36204.) X 0.00073458 S\n\n  1959 JAN  1 =JD 2436569.5     TAI-UTC= 0.4681220 S + (MJD - 36569.) X 0.000864 S\n  1959 JAN 28 =JD 2436597.29167 TAI-UTC= 0.4881220 S + (MJD - 36569.) X 0.000864 S\n  1959 FEB 25 =JD 2436625.29167 TAI-UTC= 0.5081220 S + (MJD - 36569.) X 0.000864 S\n  1959 APR  5 =JD 2436664.29167 TAI-UTC= 0.5281220 S + (MJD - 36569.) X 0.000864 S\n  1959 AUG 26 =JD 2436807.29167 TAI-UTC= 0.5481220 S + (MJD - 36569.) X 0.000864 S\n  1959 SEP 30 =JD 2436842.29167 TAI-UTC= 0.5681220 S + (MJD - 36569.) X 0.000864 S\n  1959 NOV  4 =JD 2436877.29167 TAI-UTC= 0.5881220 S + (MJD - 36569.) X 0.000864 S\n  1959 NOV 18 =JD 2436891.29167 TAI-UTC= 0.6081220 S + (MJD - 36569.) X 0.000864 S\n  1959 DEC 16 =JD 2436919.29167 TAI-UTC= 0.6281220 S + (MJD - 36569.) X 0.000864 S\n  1960 JAN  1 =JD 2436934.5     TAI-UTC= 0.9434820 S + (MJD - 36934.) X 0.001296 S\n\n  # from: https://maia.usno.navy.mil/ser7/tai-utc.dat\n  1961 JAN  1 =JD 2437300.5  TAI-UTC=   1.4228180 S + (MJD - 37300.) X 0.001296 S\n  1961 AUG  1 =JD 2437512.5  TAI-UTC=   1.3728180 S + (MJD - 37300.) X 0.001296 S\n  1962 JAN  1 =JD 2437665.5  TAI-UTC=   1.8458580 S + (MJD - 37665.) X 0.0011232S\n  1963 NOV  1 =JD 2438334.5  TAI-UTC=   1.9458580 S + (MJD - 37665.) X 0.0011232S\n  1964 JAN  1 =JD 2438395.5  TAI-UTC=   3.2401300 S + (MJD - 38761.) X 0.001296 S\n  1964 APR  1 =JD 2438486.5  TAI-UTC=   3.3401300 S + (MJD - 38761.) X 0.001296 S\n  1964 SEP  1 =JD 2438639.5  TAI-UTC=   3.4401300 S + (MJD - 38761.) X 0.001296 S\n  1965 JAN  1 =JD 2438761.5  TAI-UTC=   3.5401300 S + (MJD - 38761.) X 0.001296 S\n  1965 MAR  1 =JD 2438820.5  TAI-UTC=   3.6401300 S + (MJD - 38761.) X 0.001296 S\n  1965 JUL  1 =JD 2438942.5  TAI-UTC=   3.7401300 S + (MJD - 38761.) X 0.001296 S\n  1965 SEP  1 =JD 2439004.5  TAI-UTC=   3.8401300 S + (MJD - 38761.) X 0.001296 S\n  1966 JAN  1 =JD 2439126.5  TAI-UTC=   4.3131700 S + (MJD - 39126.) X 0.002592 S\n  1968 FEB  1 =JD 2439887.5  TAI-UTC=   4.2131700 S + (MJD - 39126.) X 0.002592 S"literal: string
count= 2922

/*
fun parse-leap-expire( leaps : string, adjusts : list<leap-adjust>) : instant
val la-final    = adjusts.head.default(zero)
val utc-expire  = leaps.find(rxexpire).map fn(cap)
    val ntpex = cap.groups[1].parse-int-default(ntp2000.int)
    timestamp(ntpex.timespan - ntp2000)
  }.default(la-final.utc-start + (182*isolar-secs-per-day).timespan)  // default: 6 months after last leap second
  // trace("expire: " + utc-expire.ts-show)
  ts-tai.instant( utc-expire - ntp2000 + la-final.offset ) // interpret as TAI to avoid recursion.

val rxexpire = regex(r"^[ \t]*#@[ \t]*(\d+)[ \t]*(?:#.*)?$", multiLine=True)
*/

/*
pub fun parse-leap-seconds-dat( leaps : string  ) : leaps-table
  val adjusts = leaps.find-all(rxtaiadjust).map( fn(cap)
    val mjd    = cap.groups[1].parse-ddouble.default(jd-epoch-shift) - jd-epoch-shift
    val ofs    = cap.groups[2].parse-ddouble.default(zero)
    val dmjd   = cap.groups[3].parse-ddouble.default(zero)
    val drift  = cap.groups[4].parse-ddouble.default(zero)
    // round to always start on a whole second
    val start  = ((mjd - mjd-epoch-shift)*solar-secs-per-day).round.timestamp
    val dstart = ((dmjd - mjd-epoch-shift)*solar-secs-per-day).round.timestamp
    // trace("pre72 start=" + start.show + ", ofs: " + ofs.show + ", drift: " + drift.show )
    Leap-adjust( start, ofs, dstart, drift )
  }).reverse
  val expire = parse-leap-expire(leaps,adjusts)
  Leaps-table(expire,adjusts)

val rxtaiadjust = regex(r"^ *\d[^=]*=JD (\d+\.\d+) *TAI-UTC= *(-?\d+(?:\.\d*)?)[^\d]+(\d+(?:\.\d*)?)[^\d]+(\d+\.\d+) *S *$", multiLine=True)
*/