Representation of a TAI64 label with full precision

Construct a TAI64 from seconds, nanoseconds and attoseconds

Seconds of real time.

Integer s refers to

  * the TAI second beginning exactly 2^62 - s seconds before the
    beginning of 1970 TAI, if s is between 0 inclusive and 2^62 exclusive;
  * or the TAI second beginning exactly s - 2^62 seconds after the
    beginning of 1970 TAI, if s is between 2^62 inclusive and 2^63
    exclusive.

Integers 2^63 and larger are reserved for future extensions. Under many
cosmological theories, the integers under 2^63 are adequate to cover the
entire expected lifetime of the universe; in this case no extensions will
be necessary.

Nanoseconds [0 .. 999999999]

Attoseconds [0 .. 999999999]

addTAI64 a b = a + b

Properties:

\d (PicosecondResolution t) -> addTAI64 d t === fromAbsoluteTime (addAbsoluteTime d (toAbsoluteTime t))

diffTAI64 a b = a - b

Properties:

\(PicosecondResolution a) (PicosecondResolution b) -> b <= a && toAbsoluteTime b >= taiEpoch ==> diffTAI64 a b === diffAbsoluteTime (toAbsoluteTime a) (toAbsoluteTime b)

sumTAI64 a b = a + b

Properties:

sumTAI64 a b >= a

sumTAI64 a minBound === a

sumTAI64 b a === sumTAI64 a b

(a `sumTAI64` b) `sumTAI64` c === a `sumTAI64` (b `sumTAI64` c)

subTAI64 a b = a - b

Properties:

subTAI64 a b <= a

b >= a ==> subTAI64 a b === minBound

subTAI64 a minBound === a

Convert a TAI64 label to AbsoluteTime.

Note that AbsoluteTime has only picosecond resolution, hence the conversion is lossy.

Properties:

\(PicosecondResolution x) -> (fromAbsoluteTime . toAbsoluteTime) x === x

Obtain a TAI64 label from AbsoluteTime.

Properties:

(toAbsoluteTime . fromAbsoluteTime) x === x

Represents a TAI64 label obtained by ignoring leap seconds, and offset from 1970-01-01 00:00:00 UTC by 10.0000005s

Tag a TAI64 value as being created by a libtai-compatible program.

Note that this lowers precision to nanoseconds.

Obtain a proper TAI64 from Libtai

Note that this is relatively expensive, as it needs to convert to UTCTime first before applying the LeapSecondTable.

Obtain the current time as Libtai.

This is (bug-)compatible with the function of the same name from libtai: we just obtain the current POSIXTime and apply an offset of 10.0000005s.

Obtain the local time corresponding to Libtai.

This is compatible with the program of the same name from the daemontools suite.

>>> let tai64n  = "4000000057693ef01cf4d1a4" -- generated by 'tai64n' from 'daemontools'
>>> let Right t = libtai <$> fromText tai64n
>>> let cest    = TimeZone (60 * 2) True "CEST"
>>> utcToZonedTime cest (libtaiToUTC t)
2016-06-21 15:19:34.4858065 CEST

Obtain the UTCTime used to generate Libtai.

Obtain the POSIXTime used to generate Libtai.

Obtain a Label for Libtai. Note that this is always TAI64N.

>>> let tai64n  = "4000000057693ef01cf4d1a4" -- generated by 'tai64n' from 'daemontools'
>>> toText . libtaiLabel . libtai <$> fromText tai64n
Right "4000000057693ef01cf4d1a4"

Addition of Libtai values.

Subtraction of Libtai values.

Add DiffTime to Libtai.

Subtraction of Libtai values, yielding DiffTime.

A TAI64 label with precision as denoted by the data constructor. This is used to render the "external" (cf. toText, toByteString) respectively binary representation.

Get the TAI64 stamp from the Label, truncated to the precision as denoted by the Label's data constructor.

Render a textual (ie. hexadecimal) representation of the external TAI64{N,NA} format of the given Label

Properties:

(fromText . toText) x === Right (fromLabel x)

Parse a TAI64 label from it's textual (hexadecimal) representation.

Properties:

let x' = toText x in fromText x' === fromText ("@" <> x')

Render a textual (ie. hexadecimal) representation of the external TAI64{N,NA} format of the given Label

Properties:

(fromByteString . toByteString) x === Right (fromLabel x)

Parse a TAI64 label from it's textual (hexadecimal) representation.

Properties:

let x' = toByteString x in fromByteString x' === fromByteString ("@" <> x')

Attoparsec parser for the textual TAI64 format, generalized so it works for both Text and ByteString input.

Type-specialisation of parse

Type-specialisation of parse