Time library

Time, clocks and calendars. Port of the haskell time library to Lean 4.

SystemTime

SystemTime is time returned by system clock functions. It has a precision of one nanosecond.

structure SystemTime where
  sec  : Int
  nsec : UInt32

-- ⊢ IO IO.FS.SystemTime
#eval getSystemTime
-- { sec := 1680959011, nsec := 928622514 }

DiffTime

DiffTime is a length of time, as measured by a clock. It has a precision of one nanosecond (Fixed 9).

structure Fixed (precision : Nat) where
  val : Int

structure DiffTime where
  val : Fixed 9

-- ⊢ Sign → ℕ → ℕ → DiffTime
#eval DiffTime.fromSecNsec Sign.Nonneg 1680959011 928622514
-- { val := { val := 1680959011928622514 } }

UTCTime

UTCTime is a representation of UTC. It consists of the day number, and a time offset from midnight.

structure UTCTime where
  utctDay : Day
  utctDayTime : DiffTime

-- ⊢ IO.FS.SystemTime → UTCTime
#eval UTCTime.toUTCTime { sec := 1680959011, nsec := 928622514 }
-- { utctDay := { modifiedJulianDay := 60042 },
--   utctDayTime := { val := { val := 47011928622514  } } }

Day

The Day data type is an abstract way of referring to a calendar date. The toGregorian and fromGregorian functions will construct and deconstruct a Day from the usual year-month-day format.

structure Day where
  modifiedJulianDay : Int

-- ⊢ ℤ → ℤ → ℤ → Day
#eval fromGregorian 2023 2 12
-- { modifiedJulianDay := 59987 }

OrdinalDate

OrdinalDate is an ISO 8601 Ordinal Date.

inductive DayOfYear where
  | common : Time.Icc 1 365 -> DayOfYear
  | leap : Time.Icc 1 366 -> DayOfYear

structure OrdinalDate where
  year : Int
  dayOfYear : DayOfYear
  isValid : match dayOfYear with
            | .common _ => isLeapYear year = false
            | .leap _ => isLeapYear year = true

-- ⊢ Day → OrdinalDate
#eval toOrdinalDate { modifiedJulianDay := 59987 }
-- { year := 2023, dayOfYear := Time.DayOfYear.common 43, isValid := __ }

Date

The Date is a calendar date in the proleptic Gregorian calendar.

structure Date where
  Year : Int
  Month : Time.Icc 1 12
  Day : Time.Icc 1 31
  IsValid : ∃ m ∈ monthLengths (isLeapYear Year), m.1 = Month ∧ Day ≤ m.2

-- ⊢ Day → Date
#eval toGregorian { modifiedJulianDay := 59987 }
-- { Year := 2023, Month := 2, Day := 12, IsValid := _ }

open Time.Notation
#eval date# 2023-2-12
-- { Year := 2023, Month := 2, Day := 12, IsValid := _ }

TimeOfDay

TimeOfDay consists of an hour of the day, a minute of the hour, and a second of the minute, including fractions of a second up to a resolution of one nanosecond.

structure TimeOfDay where
  Hour : Time.Ico 0 24
  Minute : Time.Ico 0 60
  Second : Time.Ico ⟨0⟩ ⟨60000000000⟩

-- ⊢ DiffTime → TimeOfDay
#eval TimeOfDay.timeToTimeOfDay { val := { val := 47011928622514  } }
-- { Hour := 13, Minute := 3, Second := { val := 31928622514 } }

open Time.Notation
#eval time# 13:3:31.928622514
-- { Hour := 13, Minute := 3, Second := { val := 31928622514 } }

TimeZone

A TimeZone represents an offset from UTC measured in minutes.

structure TimeZone where
  timeZoneMinutes : Int
  timeZoneSummerOnly : Bool
  timeZoneName : String

-- ⊢ IO TimeZone
#eval TimeZone.getTimeZone
-- { timeZoneMinutes := 120, timeZoneSummerOnly := true, timeZoneName := "CEST" }

LocalTime

A Day with a TimeOfDay forms a LocalTime.

structure LocalTime where
  localDay : Day
  localTimeOfDay : TimeOfDay

-- ⊢ LocalTime
#eval (⟨Time.fromGregorianDate (date% 2024-2-10), time% 12:30⟩ : LocalTime)
-- { localDay := { modifiedJulianDay := 60350 },
--   localTimeOfDay := { Hour := 12, Minute := 30, Second := { val := 0 } } }

ZonedTime

A ZonedTime is a LocalTime together with a TimeZone.

structure ZonedTime where
  localTime : LocalTime
  timeZone : TimeZone

-- ⊢ LocalTime → TimeZone → ZonedTime
#eval ZonedTime.mk
  { localDay := { modifiedJulianDay := 60042 },
    localTimeOfDay := { Hour := ⟨15, (by simp)⟩, Minute := ⟨3, (by simp)⟩,
                        Second := ⟨⟨31928622514⟩, (by simp)⟩ } }
  { timeZoneMinutes := 120, timeZoneSummerOnly := true, timeZoneName := "CEST" }
-- { localTime :=
--      { localDay := { modifiedJulianDay := 60042 },
--        localTimeOfDay := { Hour := 15, Minute := 3, Second := { val := 31928622514 } } },
--   timeZone := { timeZoneMinutes := 120, timeZoneSummerOnly := true, timeZoneName := "CEST" } }

Parse

Parse a time value (i.e. instance of Time.ParseTime) given a format string.

#eval (parse .defaultTimeLocale "%Y-%m-%dT%H:%M:%S" "2023-02-12T12:24:30"
        : Option LocalTime)
-- some
--   { localDay := { modifiedJulianDay := 59987 },
--     localTimeOfDay := { Hour := 12, Minute := 24,
--                         Second := { val := 30000000000 } } }

Format

Format a time value (i.e. instance of Time.ToISO8601) to ISO8601.

#eval toISO8601 (default : ZonedTime)
-- "1858-11-17T00:00:00+00:00"