From f67ea44b6aa5edba78f297de44327b01ca93e7a4 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Mon, 11 May 2026 20:26:19 -0300 Subject: [PATCH] feat: add `WallTime` and simplify `Timestamp` API (#13675) This PR adds a `WallTime` type representing a point in time as nanoseconds since `1970-01-01T00:00:00` local time. It also removes the `sinceUNIXEpoch` and `AssumingUTC` suffixes because `Timestamp` implies UTC, and `WallTime` implies it is based on the WallTime epoch (defined in the comment as `1970-01-01T00:00:00`). --------- Co-authored-by: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com> --- src/Std/Time.lean | 4 + src/Std/Time/Date/PlainDate.lean | 18 +- src/Std/Time/DateTime.lean | 107 +++++--- src/Std/Time/DateTime/PlainDateTime.lean | 32 +-- src/Std/Time/DateTime/Timestamp.lean | 32 ++- src/Std/Time/DateTime/WallTime.lean | 312 +++++++++++++++++++++++ src/Std/Time/Format.lean | 4 +- src/Std/Time/Notation.lean | 2 - src/Std/Time/Zoned.lean | 26 +- src/Std/Time/Zoned/DateTime.lean | 59 ++--- src/Std/Time/Zoned/ZoneRules.lean | 22 ++ src/Std/Time/Zoned/ZonedDateTime.lean | 153 ++++------- tests/elab/timeAPI.lean | 36 ++- tests/elab/timeClassOperations.lean | 4 +- tests/elab/timeFormats.lean | 14 +- tests/elab/timeLimits.lean | 2 +- tests/elab/timeLocalDateTime.lean | 16 +- tests/elab/timeNegative.lean | 24 +- tests/elab/timeParse.lean | 2 +- 19 files changed, 585 insertions(+), 284 deletions(-) create mode 100644 src/Std/Time/DateTime/WallTime.lean diff --git a/src/Std/Time.lean b/src/Std/Time.lean index e8b32b8963..d59a5f4633 100644 --- a/src/Std/Time.lean +++ b/src/Std/Time.lean @@ -111,6 +111,10 @@ Combines date and time into a single representation, useful for precise timestam - **`PlainDateTime`**: Represents both date and time in the format `YYYY-MM-DDTHH:mm:ss,sssssssss`. - **`Timestamp`**: Represents a specific point in time with nanosecond precision. Its zero value corresponds to the UNIX epoch. This type should be used when sending or receiving timestamps between systems. +- **`WallTime`**: Represents the local civil time shown by a clock in some timezone, stored as a `Duration` +since `1970-01-01T00:00:00` in local time. Unlike `Timestamp`, it is not tied to UTC; converting between +the two requires a timezone. It is convenient for performing arithmetic directly on local times without +first resolving to an absolute instant. ## Zoned date and times. Combines date, time and time zones. diff --git a/src/Std/Time/Date/PlainDate.lean b/src/Std/Time/Date/PlainDate.lean index 0a486e0262..66b83834be 100644 --- a/src/Std/Time/Date/PlainDate.lean +++ b/src/Std/Time/Date/PlainDate.lean @@ -92,9 +92,9 @@ def ofYearOrdinal (year : Year.Offset) (ordinal : Day.Ordinal.OfYear year.isLeap ⟨year, month, day, proof⟩ /-- -Creates a `PlainDate` from the number of days since the UNIX epoch (January 1st, 1970). +Creates a `PlainDate` from the number of days since January 1st, 1970. -/ -def ofDaysSinceUNIXEpoch (day : Day.Offset) : PlainDate := +def ofEpochDay (day : Day.Offset) : PlainDate := let z := day.toInt + 719468 let era := (if z ≥ 0 then z else z - 146096).tdiv 146097 let doe := z - era * 146097 @@ -140,9 +140,9 @@ def inLeapYear (date : PlainDate) : Bool := date.year.isLeap /-- -Converts a `PlainDate` to the number of days since the UNIX epoch. +Converts a `PlainDate` to the number of days since 1970-01-01T00:00:00. -/ -def toDaysSinceUNIXEpoch (date : PlainDate) : Day.Offset := +def toEpochDay (date : PlainDate) : Day.Offset := let y : Int := if date.month.toInt > 2 then date.year else date.year.toInt - 1 let era : Int := (if y ≥ 0 then y else y - 399).tdiv 400 let yoe : Int := y - era * 400 @@ -158,8 +158,8 @@ Adds a given number of days to a `PlainDate`. -/ @[inline] def addDays (date : PlainDate) (days : Day.Offset) : PlainDate := - let dateDays := date.toDaysSinceUNIXEpoch - ofDaysSinceUNIXEpoch (dateDays + days) + let dateDays := date.toEpochDay + ofEpochDay (dateDays + days) /-- Subtracts a given number of days from a `PlainDate`. @@ -173,9 +173,9 @@ Adds a given number of weeks to a `PlainDate`. -/ @[inline] def addWeeks (date : PlainDate) (weeks : Week.Offset) : PlainDate := - let dateDays := date.toDaysSinceUNIXEpoch + let dateDays := date.toEpochDay let daysToAdd := weeks.toDays - ofDaysSinceUNIXEpoch (dateDays + daysToAdd) + ofEpochDay (dateDays + daysToAdd) /-- Subtracts a given number of weeks from a `PlainDate`. @@ -301,7 +301,7 @@ def withMonthRollOver (dt : PlainDate) (month : Month.Ordinal) : PlainDate := Calculates the `Weekday` of a given `PlainDate` using Zeller's Congruence for the Gregorian calendar. -/ def weekday (date : PlainDate) : Weekday := - let days := date.toDaysSinceUNIXEpoch.val + let days := date.toEpochDay.val let res := if days ≥ -4 then (days + 4) % 7 else (days + 5) % 7 + 6 .ofOrdinal (Bounded.LE.ofNatWrapping res (by decide)) diff --git a/src/Std/Time/DateTime.lean b/src/Std/Time/DateTime.lean index dd7df4504e..b40797da81 100644 --- a/src/Std/Time/DateTime.lean +++ b/src/Std/Time/DateTime.lean @@ -6,6 +6,8 @@ Authors: Sofia Rodrigues module prelude +public import Std.Time.Zoned.Offset +public import Std.Time.DateTime.WallTime public import Std.Time.DateTime.Timestamp public import Std.Time.DateTime.PlainDateTime import all Std.Time.Date.Unit.Month @@ -15,95 +17,116 @@ public section namespace Std namespace Time -namespace Timestamp - set_option linter.all true -/-- -Converts a `PlainDateTime` to a `Timestamp` --/ -@[inline] -def ofPlainDateTimeAssumingUTC (pdt : PlainDateTime) : Timestamp := - pdt.toTimestampAssumingUTC +namespace Timestamp /-- -Converts a `Timestamp` to a `PlainDateTime` +Converts a `Timestamp` to a `WallTime` for a given timezone `offset`. The result is the local +civil time: `wall = UTC + offset`. -/ @[inline] -def toPlainDateTimeAssumingUTC (timestamp : Timestamp) : PlainDateTime := - PlainDateTime.ofTimestampAssumingUTC timestamp +def toWallTime (ts : Timestamp) (offset : TimeZone.Offset) : WallTime := + WallTime.ofDuration (ts.val + offset.second) /-- -Converts a `PlainDate` to a `Timestamp` +Creates a `Timestamp` from a `WallTime` and a timezone `offset`. Assumes the `WallTime` represents +civil time at the given offset: `UTC = wall − offset`. -/ @[inline] -def ofPlainDateAssumingUTC (pd : PlainDate) : Timestamp := - let days := pd.toDaysSinceUNIXEpoch - let secs := days.toSeconds - Timestamp.ofSecondsSinceUnixEpoch secs - -/-- -Converts a `Timestamp` to a `PlainDate` --/ -@[inline] -def toPlainDateAssumingUTC (timestamp : Timestamp) : PlainDate := - let secs := timestamp.toSecondsSinceUnixEpoch - let days := Day.Offset.ofSeconds secs - PlainDate.ofDaysSinceUNIXEpoch days - -/-- -Converts a `Timestamp` to a `PlainTime` --/ -@[inline] -def getTimeAssumingUTC (timestamp : Timestamp) : PlainTime := - let nanos := timestamp.toNanosecondsSinceUnixEpoch - PlainTime.ofNanoseconds nanos +def ofWallTime (wt : WallTime) (offset : TimeZone.Offset) : Timestamp := + Timestamp.ofDurationSinceUnixEpoch (wt.val - offset.second) end Timestamp + +namespace WallTime + +/-- +Converts a `WallTime` to a `Timestamp` given a timezone `offset`. The `WallTime` is treated as +civil time at the given offset: `UTC = wall − offset`. +-/ +@[inline] +def toTimestamp (wt : WallTime) (offset : TimeZone.Offset) : Timestamp := + Timestamp.ofWallTime wt offset + +/-- +Creates a `WallTime` from a `Timestamp` given a timezone `offset`. The result is the local +civil time: `wall = UTC + offset`. +-/ +@[inline] +def ofTimestamp (ts : Timestamp) (offset : TimeZone.Offset) : WallTime := + Timestamp.toWallTime ts offset + +end WallTime + namespace PlainDate /-- -Converts a `PlainDate` to a `Timestamp` +Converts a `PlainDate` to a `WallTime`. -/ @[inline] -def toTimestampAssumingUTC (pdt : PlainDate) : Timestamp := - Timestamp.ofPlainDateAssumingUTC pdt +def toWallTime (pd : PlainDate) : WallTime := + WallTime.ofSeconds pd.toEpochDay.toSeconds + +/-- +Converts a `WallTime` to a `PlainDate`. +-/ +@[inline] +def ofWallTime (wt : WallTime) : PlainDate := + PlainDate.ofEpochDay wt.toDays instance : HSub PlainDate PlainDate Duration where - hSub x y := x.toTimestampAssumingUTC - y.toTimestampAssumingUTC + hSub x y := x.toWallTime - y.toWallTime end PlainDate +namespace PlainTime + +/-- +Converts a `PlainTime` to a `WallTime`. +-/ +@[inline] +def toWallTime (pt : PlainTime) : WallTime := + WallTime.ofNanoseconds pt.toNanoseconds + +/-- +Converts a `WallTime` to a `PlainTime`. +-/ +@[inline] +def ofWallTime (wt : WallTime) : PlainTime := + PlainTime.ofNanoseconds wt.toNanoseconds + +end PlainTime namespace PlainDateTime /-- -Converts a `PlainDate` to a `Timestamp` +Wraps a `PlainDate` in a `PlainDateTime` with midnight as the time component. -/ @[inline] def ofPlainDate (date : PlainDate) : PlainDateTime := { date, time := PlainTime.midnight } /-- -Converts a `PlainDateTime` to a `PlainDate` +Extracts the `PlainDate` component from a `PlainDateTime`. -/ @[inline] def toPlainDate (pdt : PlainDateTime) : PlainDate := pdt.date /-- -Converts a `PlainTime` to a `PlainDateTime` +Wraps a `PlainTime` in a `PlainDateTime` with year 1, month 1, day 1 as the date component. -/ @[inline] def ofPlainTime (time : PlainTime) : PlainDateTime := { date := ⟨1, 1, 1, by decide⟩, time } /-- -Converts a `PlainDateTime` to a `PlainTime` +Extracts the `PlainTime` component from a `PlainDateTime`. -/ @[inline] def toPlainTime (pdt : PlainDateTime) : PlainTime := pdt.time instance : HSub PlainDateTime PlainDateTime Duration where - hSub x y := x.toTimestampAssumingUTC - y.toTimestampAssumingUTC + hSub x y := x.toWallTime - y.toWallTime end PlainDateTime diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index 4f14a41981..a7d7c1725c 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -6,7 +6,7 @@ Authors: Sofia Rodrigues module prelude -public import Std.Time.DateTime.Timestamp +public import Std.Time.DateTime.WallTime public section @@ -51,24 +51,24 @@ instance : LawfulEqOrd PlainDateTime where namespace PlainDateTime /-- -Converts a `PlainDateTime` to a `Timestamp` +Converts a `PlainDateTime` to a `WallTime`. -/ -def toTimestampAssumingUTC (dt : PlainDateTime) : Timestamp := - let days := dt.date.toDaysSinceUNIXEpoch +def toWallTime (dt : PlainDateTime) : WallTime := + let days := dt.date.toEpochDay let nanos := days.toSeconds + dt.time.toSeconds |>.mul 1000000000 let nanos := nanos.val + dt.time.nanosecond.val - Timestamp.ofNanosecondsSinceUnixEpoch (Nanosecond.Offset.ofInt nanos) + WallTime.ofNanoseconds (Nanosecond.Offset.ofInt nanos) /-- -Converts a `Timestamp` to a `PlainDateTime`. +Converts a `WallTime` to a `PlainDateTime`. -/ -def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do +def ofWallTime (stamp : WallTime) : PlainDateTime := Id.run do let leapYearEpoch := 11017 let daysPer400Y := 365 * 400 + 97 let daysPer100Y := 365 * 100 + 24 let daysPer4Y := 365 * 4 + 1 - let nanos := stamp.toNanosecondsSinceUnixEpoch + let nanos := stamp.toNanoseconds let secs : Second.Offset := nanos.toSeconds let remNano := Bounded.LE.byMod nanos.val 1000000000 (by decide) @@ -152,21 +152,21 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do } /-- -Converts a `PlainDateTime` to the number of days since the UNIX epoch. +Returns the local (civil) date of the `PlainDateTime` as a `Day.Offset` relative to 1970-01-01. -/ @[inline] -def toDaysSinceUNIXEpoch (pdt : PlainDateTime) : Day.Offset := - pdt.date.toDaysSinceUNIXEpoch +def toEpochDay (pdt : PlainDateTime) : Day.Offset := + pdt.date.toEpochDay /-- -Converts a `PlainDateTime` to the number of days since the UNIX epoch. +Converts the number of days relative to 1970-01-01 as a `PlainDateTime`. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) : PlainDateTime := - PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) time +def ofEpochDay (days : Day.Offset) (time : PlainTime) : PlainDateTime := + PlainDateTime.mk (PlainDate.ofEpochDay days) time /-- -Sets the `PlainDateTime` to the specified `desiredWeekday`. +Sets the `PlainDateTime` to the specified `Weekday`. -/ def withWeekday (dt : PlainDateTime) (desiredWeekday : Weekday) : PlainDateTime := { dt with date := PlainDate.withWeekday dt.date desiredWeekday } @@ -346,7 +346,7 @@ Adds a `Nanosecond.Offset` to a `PlainDateTime`, adjusting the seconds, minutes, -/ @[inline] def addNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime := - ofTimestampAssumingUTC (dt.toTimestampAssumingUTC + nanos) + ofWallTime (dt.toWallTime + nanos) /-- Subtracts a `Nanosecond.Offset` from a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds underflow. diff --git a/src/Std/Time/DateTime/Timestamp.lean b/src/Std/Time/DateTime/Timestamp.lean index 9f95861d94..67a43bd884 100644 --- a/src/Std/Time/DateTime/Timestamp.lean +++ b/src/Std/Time/DateTime/Timestamp.lean @@ -22,6 +22,7 @@ Represents an exact point in time as a UNIX Epoch timestamp. -/ @[ext] structure Timestamp where + private mk :: /-- Duration since the unix epoch. @@ -41,14 +42,11 @@ instance : LT Timestamp where instance { x y : Timestamp } : Decidable (x < y) := inferInstanceAs (Decidable (x.val < y.val)) -instance : OfNat Timestamp n where - ofNat := ⟨OfNat.ofNat n⟩ - instance : ToString Timestamp where toString s := toString s.val.toSeconds instance : Repr Timestamp where - reprPrec s := Repr.addAppParen ("Timestamp.ofNanosecondsSinceUnixEpoch " ++ repr s.val.toNanoseconds) + reprPrec s := Repr.addAppParen ("Timestamp.ofNanoseconds " ++ repr s.val.toNanoseconds) instance : Ord Timestamp where compare := compareOn (·.val) @@ -73,42 +71,49 @@ Fetches the current duration from the system. opaque now : IO Timestamp /-- -Converts a `Timestamp` to minutes as `Minute.Offset`. +Converts a `Timestamp` to a `Minute.Offset`. -/ @[inline] -def toMinutes (tm : Timestamp) : Minute.Offset := +def toMinutesSinceUnixEpoch (tm : Timestamp) : Minute.Offset := tm.val.second.toMinutes /-- -Converts a `Timestamp` to days as `Day.Offset`. +Converts a `Timestamp` to a `Day.Offset`. -/ @[inline] -def toDays (tm : Timestamp) : Day.Offset := +def toDaysSinceUnixEpoch (tm : Timestamp) : Day.Offset := tm.val.second.toDays /-- -Creates a `Timestamp` from a `Second.Offset` since the Unix epoch. +Creates a `Timestamp` from a `Second.Offset`. -/ @[inline] def ofSecondsSinceUnixEpoch (secs : Second.Offset) : Timestamp := ⟨Duration.ofSeconds secs⟩ /-- -Creates a `Timestamp` from a `Nanosecond.Offset` since the Unix epoch. +Creates a `Timestamp` from a `Nanosecond.Offset`. -/ @[inline] def ofNanosecondsSinceUnixEpoch (nanos : Nanosecond.Offset) : Timestamp := ⟨Duration.ofNanoseconds nanos⟩ /-- -Creates a `Timestamp` from a `Millisecond.Offset` since the Unix epoch. +Creates a `Timestamp` from a `Duration`. +-/ +@[inline] +def ofDurationSinceUnixEpoch (duration : Duration) : Timestamp := + ⟨duration⟩ + +/-- +Creates a `Timestamp` from a `Millisecond.Offset`. -/ @[inline] def ofMillisecondsSinceUnixEpoch (milli : Millisecond.Offset) : Timestamp := ⟨Duration.ofNanoseconds milli.toNanoseconds⟩ /-- -Converts a `Timestamp` to seconds as `Second.Offset`. +Converts a `Timestamp` to a `Second.Offset`. -/ @[inline] def toSecondsSinceUnixEpoch (t : Timestamp) : Second.Offset := @@ -308,4 +313,7 @@ instance : HSub Timestamp Nanosecond.Offset Timestamp where instance : HSub Timestamp Timestamp Duration where hSub x y := x.val - y.val +instance : OfNat Timestamp n where + ofNat := .ofSecondsSinceUnixEpoch (Second.Offset.ofNat n) + end Timestamp diff --git a/src/Std/Time/DateTime/WallTime.lean b/src/Std/Time/DateTime/WallTime.lean new file mode 100644 index 0000000000..53d86441f6 --- /dev/null +++ b/src/Std/Time/DateTime/WallTime.lean @@ -0,0 +1,312 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Init.System.IO +public import Std.Time.Duration + +public section + +namespace Std +namespace Time + +set_option linter.all true + +/-- +A wall-clock time is what a clock shows in a given timezone: the local civil time at some point in +time. It is stored as a `Duration` since `1970-01-01T00:00:00` in local time, equivalent to a +`PlainDateTime` packed into a single offset, which makes arithmetic straightforward. + +Every timezone induces a correspondence between `Timestamp` and `WallTime`: interpreting a +`Timestamp` in a timezone yields the `WallTime` (what a clock in that timezone reads at that +instant), and resolving a `WallTime` in a timezone yields the `Timestamp` (the absolute instant the +clock reading refers to). +-/ +@[ext] +structure WallTime where + private mk :: + + /-- + Duration since `1970-01-01T00:00:00` in local (civil) time. + -/ + val : Duration + deriving Repr, DecidableEq, Inhabited + +instance : LE WallTime where + le x y := x.val ≤ y.val + +instance { x y : WallTime } : Decidable (x ≤ y) := + inferInstanceAs (Decidable (x.val ≤ y.val)) + +instance : LT WallTime where + lt x y := x.val < y.val + +instance { x y : WallTime } : Decidable (x < y) := + inferInstanceAs (Decidable (x.val < y.val)) + +instance : Ord WallTime where + compare := compareOn (·.val) + +instance : ToString WallTime where + toString s := toString s.val.toSeconds + +instance : Repr WallTime where + reprPrec s := Repr.addAppParen ("WallTime.ofNanoseconds " ++ repr s.val.toNanoseconds) + +namespace WallTime + +/-- +Creates a `WallTime` from a `Duration`. The epoch is 1970-01-01 00:00:00 in local +(civil) time, not UTC. +-/ +@[inline] +def ofDuration (duration : Duration) : WallTime := + ⟨duration⟩ + +/-- +Creates a `WallTime` from a `Second.Offset`. The epoch is 1970-01-01 00:00:00 in local +(civil) time, not UTC. +-/ +@[inline] +def ofSeconds (secs : Second.Offset) : WallTime := + ⟨Duration.ofSeconds secs⟩ + +/-- +Creates a `WallTime` from a `Nanosecond.Offset`. The epoch is 1970-01-01 00:00:00 in local +(civil) time, not UTC. +-/ +@[inline] +def ofNanoseconds (nanos : Nanosecond.Offset) : WallTime := + ⟨Duration.ofNanoseconds nanos⟩ + +/-- +Converts a `WallTime` to a `Second.Offset`. The epoch is 1970-01-01 00:00:00 in local +(civil) time, not UTC. +-/ +@[inline] +def toSeconds (wt : WallTime) : Second.Offset := + wt.val.second + +/-- +Converts a `WallTime` to a `Nanosecond.Offset`. The epoch is 1970-01-01 00:00:00 in local +(civil) time, not UTC. +-/ +@[inline] +def toNanoseconds (wt : WallTime) : Nanosecond.Offset := + let nanos := wt.toSeconds.mul 1000000000 + let nanos := nanos + (.ofInt wt.val.nano.val) + nanos + +/-- +Converts a `WallTime` to a `Minute.Offset`. The epoch is 1970-01-01 00:00:00 in local +(civil) time, not UTC. +-/ +@[inline] +def toMinutes (tm : WallTime) : Minute.Offset := + tm.val.second.toMinutes + +/-- +Converts a `WallTime` to a `Day.Offset`. The epoch is 1970-01-01 00:00:00 in local +(civil) time, not UTC. +-/ +@[inline] +def toDays (tm : WallTime) : Day.Offset := + tm.val.second.toDays + +/-- +Creates a `WallTime` from a `Millisecond.Offset`. The epoch is 1970-01-01 00:00:00 in local +(civil) time, not UTC. +-/ +@[inline] +def ofMilliseconds (milli : Millisecond.Offset) : WallTime := + ⟨Duration.ofNanoseconds milli.toNanoseconds⟩ + +/-- +Converts a `WallTime` to a `Millisecond.Offset`. The epoch is 1970-01-01 00:00:00 in local +(civil) time, not UTC. +-/ +@[inline] +def toMilliseconds (tm : WallTime) : Millisecond.Offset := + tm.toNanoseconds.toMilliseconds + +/-- +Adds a `Millisecond.Offset` to the given `WallTime`. +-/ +@[inline] +def addMilliseconds (t : WallTime) (s : Millisecond.Offset) : WallTime := + ⟨t.val + s⟩ + +/-- +Subtracts a `Millisecond.Offset` from the given `WallTime`. +-/ +@[inline] +def subMilliseconds (t : WallTime) (s : Millisecond.Offset) : WallTime := + ⟨t.val - s⟩ + +/-- +Adds a `Nanosecond.Offset` to the given `WallTime`. +-/ +@[inline] +def addNanoseconds (t : WallTime) (s : Nanosecond.Offset) : WallTime := + ⟨t.val + s⟩ + +/-- +Subtracts a `Nanosecond.Offset` from the given `WallTime`. +-/ +@[inline] +def subNanoseconds (t : WallTime) (s : Nanosecond.Offset) : WallTime := + ⟨t.val - s⟩ + +/-- +Adds a `Second.Offset` to the given `WallTime`. +-/ +@[inline] +def addSeconds (t : WallTime) (s : Second.Offset) : WallTime := + ⟨t.val + s⟩ + +/-- +Subtracts a `Second.Offset` from the given `WallTime`. +-/ +@[inline] +def subSeconds (t : WallTime) (s : Second.Offset) : WallTime := + ⟨t.val - s⟩ + +/-- +Adds a `Minute.Offset` to the given `WallTime`. +-/ +@[inline] +def addMinutes (t : WallTime) (m : Minute.Offset) : WallTime := + ⟨t.val + m⟩ + +/-- +Subtracts a `Minute.Offset` from the given `WallTime`. +-/ +@[inline] +def subMinutes (t : WallTime) (m : Minute.Offset) : WallTime := + ⟨t.val - m⟩ + +/-- +Adds an `Hour.Offset` to the given `WallTime`. +-/ +@[inline] +def addHours (t : WallTime) (h : Hour.Offset) : WallTime := + ⟨t.val + h⟩ + +/-- +Subtracts an `Hour.Offset` from the given `WallTime`. +-/ +@[inline] +def subHours (t : WallTime) (h : Hour.Offset) : WallTime := + ⟨t.val - h⟩ + +/-- +Adds a `Day.Offset` to the given `WallTime`. +-/ +@[inline] +def addDays (t : WallTime) (d : Day.Offset) : WallTime := + ⟨t.val + d⟩ + +/-- +Subtracts a `Day.Offset` from the given `WallTime`. +-/ +@[inline] +def subDays (t : WallTime) (d : Day.Offset) : WallTime := + ⟨t.val - d⟩ + +/-- +Adds a `Week.Offset` to the given `WallTime`. +-/ +@[inline] +def addWeeks (t : WallTime) (d : Week.Offset) : WallTime := + ⟨t.val + d⟩ + +/-- +Subtracts a `Week.Offset` from the given `WallTime`. +-/ +@[inline] +def subWeeks (t : WallTime) (d : Week.Offset) : WallTime := + ⟨t.val - d⟩ + +/-- +Adds a `Duration` to the given `WallTime`. +-/ +@[inline] +def addDuration (t : WallTime) (d : Duration) : WallTime := + ⟨t.val + d⟩ + +/-- +Subtracts a `Duration` from the given `WallTime`. +-/ +@[inline] +def subDuration (t : WallTime) (d : Duration) : WallTime := + ⟨t.val - d⟩ + +/-- +Converts a `WallTime` to a `Duration`. The epoch is 1970-01-01 00:00:00 in local +(civil) time, not UTC. +-/ +@[inline] +def toDuration (wt : WallTime) : Duration := + wt.val + +instance : HAdd WallTime Duration WallTime where + hAdd := addDuration + +instance : HSub WallTime Duration WallTime where + hSub := subDuration + +instance : HAdd WallTime Day.Offset WallTime where + hAdd := addDays + +instance : HSub WallTime Day.Offset WallTime where + hSub := subDays + +instance : HAdd WallTime Week.Offset WallTime where + hAdd := addWeeks + +instance : HSub WallTime Week.Offset WallTime where + hSub := subWeeks + +instance : HAdd WallTime Hour.Offset WallTime where + hAdd := addHours + +instance : HSub WallTime Hour.Offset WallTime where + hSub := subHours + +instance : HAdd WallTime Minute.Offset WallTime where + hAdd := addMinutes + +instance : HSub WallTime Minute.Offset WallTime where + hSub := subMinutes + +instance : HAdd WallTime Second.Offset WallTime where + hAdd := addSeconds + +instance : HSub WallTime Second.Offset WallTime where + hSub := subSeconds + +instance : HAdd WallTime Millisecond.Offset WallTime where + hAdd := addMilliseconds + +instance : HSub WallTime Millisecond.Offset WallTime where + hSub := subMilliseconds + +instance : HAdd WallTime Nanosecond.Offset WallTime where + hAdd := addNanoseconds + +instance : HSub WallTime Nanosecond.Offset WallTime where + hSub := subNanoseconds + +instance : HSub WallTime WallTime Duration where + hSub x y := x.val - y.val + +instance : OfNat WallTime n where + ofNat := .ofSeconds (Second.Offset.ofNat n) + +end WallTime +end Time +end Std diff --git a/src/Std/Time/Format.lean b/src/Std/Time/Format.lean index 846dce68f3..be7cb48cf4 100644 --- a/src/Std/Time/Format.lean +++ b/src/Std/Time/Format.lean @@ -489,7 +489,7 @@ def fromAscTimeString (input : String) : Except String PlainDateTime := Formats a `PlainDateTime` value into an AscTime format string. -/ def toAscTimeString (pdt : PlainDateTime) : String := - Formats.ascTime.format (DateTime.ofPlainDateTimeAssumingUTC pdt .UTC) + Formats.ascTime.format (DateTime.ofPlainDateTime pdt .UTC) /-- Parses a `String` in the `LongDateFormat` and returns a `PlainDateTime` object in the GMT time zone. @@ -502,7 +502,7 @@ def fromLongDateFormatString (input : String) : Except String PlainDateTime := Formats a `PlainDateTime` value into a LongDateFormat string. -/ def toLongDateFormatString (pdt : PlainDateTime) : String := - Formats.longDateFormat.format (DateTime.ofPlainDateTimeAssumingUTC pdt .UTC) + Formats.longDateFormat.format (DateTime.ofPlainDateTime pdt .UTC) /-- Parses a `String` in the `DateTime` format and returns a `PlainDateTime`. diff --git a/src/Std/Time/Notation.lean b/src/Std/Time/Notation.lean index 9d02a01a9d..82d6790f4b 100644 --- a/src/Std/Time/Notation.lean +++ b/src/Std/Time/Notation.lean @@ -159,7 +159,6 @@ Example: -/ syntax "zoned(" str "," term ")" : term - /-- Defines a syntax for datetime values without timezone. The input should be a string in an ISO8601-like format. @@ -204,7 +203,6 @@ Example: -/ syntax "timezone(" str ")" : term - macro_rules | `(zoned( $date:str )) => do match ZonedDateTime.fromLeanDateTimeWithZoneString date.getString with diff --git a/src/Std/Time/Zoned.lean b/src/Std/Time/Zoned.lean index 77df21dcfe..13df295516 100644 --- a/src/Std/Time/Zoned.lean +++ b/src/Std/Time/Zoned.lean @@ -30,7 +30,7 @@ def now : IO PlainDateTime := do let rules ← Database.defaultGetLocalZoneRules let ltt := rules.findLocalTimeTypeForTimestamp tm - return PlainDateTime.ofTimestampAssumingUTC tm |>.addSeconds ltt.getTimeZone.toSeconds + return PlainDateTime.ofWallTime (WallTime.ofTimestamp tm ltt.getTimeZone.offset) end PlainDateTime @@ -58,18 +58,18 @@ end PlainTime namespace DateTime /-- -Converts a `PlainDate` with a `TimeZone` to a `DateTime` +Converts a `PlainDate` with a `TimeZone` to a `DateTime`. It assumes `PlainDate` is local time. -/ @[inline] -def ofPlainDate (pd : PlainDate) (tz : TimeZone) : DateTime tz := - DateTime.ofTimestamp (Timestamp.ofPlainDateAssumingUTC pd) tz +def ofLocalDate (pd : PlainDate) (tz : TimeZone) : DateTime tz := + DateTime.ofPlainDateTime (PlainDateTime.ofPlainDate pd) tz /-- -Converts a `DateTime` to a `PlainDate` +Converts a `DateTime` to a `PlainDate`. -/ @[inline] def toPlainDate (dt : DateTime tz) : PlainDate := - Timestamp.toPlainDateAssumingUTC dt.toTimestamp + dt.toPlainDateTime.toPlainDate /-- Converts a `DateTime` to a `PlainTime` @@ -111,15 +111,15 @@ def nowAt (id : String) : IO ZonedDateTime := do Converts a `PlainDate` to a `ZonedDateTime`. -/ @[inline] -def ofPlainDate (pd : PlainDate) (zr : TimeZone.ZoneRules) : ZonedDateTime := - ZonedDateTime.ofPlainDateTime (pd.atTime PlainTime.midnight) zr +def ofLocalDate (pd : PlainDate) (zr : TimeZone.ZoneRules) : ZonedDateTime := + .ofPlainDateTime (pd.atTime PlainTime.midnight) zr /-- Converts a `PlainDate` to a `ZonedDateTime` using `TimeZone`. -/ @[inline] -def ofPlainDateWithZone (pd : PlainDate) (zr : TimeZone) : ZonedDateTime := - ZonedDateTime.ofPlainDateTime (pd.atTime PlainTime.midnight) (TimeZone.ZoneRules.ofTimeZone zr) +def ofLocalDateWithZone (pd : PlainDate) (zr : TimeZone) : ZonedDateTime := + .ofPlainDateTime (pd.atTime PlainTime.midnight) (TimeZone.ZoneRules.ofTimeZone zr) /-- Converts a `ZonedDateTime` to a `PlainDate` @@ -141,7 +141,7 @@ Creates a new `ZonedDateTime` out of a `PlainDateTime` and a time zone identifie @[inline] def of (pdt : PlainDateTime) (id : String) : IO ZonedDateTime := do let zr ← Database.defaultGetZoneRules id - return ZonedDateTime.ofPlainDateTime pdt zr + return .ofPlainDateTime pdt zr end ZonedDateTime @@ -170,13 +170,13 @@ Converts a `PlainDate` to a `Timestamp` using the `ZoneRules`. -/ @[inline] def toTimestamp (dt : PlainDate) (zr : TimeZone.ZoneRules) : Timestamp := - ZonedDateTime.ofPlainDate dt zr |>.toTimestamp + ZonedDateTime.ofLocalDate dt zr |>.toTimestamp /-- Converts a `PlainDate` to a `Timestamp` using the `TimeZone`. -/ @[inline] def toTimestampWithZone (dt : PlainDate) (tz : TimeZone) : Timestamp := - ZonedDateTime.ofPlainDateWithZone dt tz |>.toTimestamp + ZonedDateTime.ofLocalDateWithZone dt tz |>.toTimestamp end PlainDate diff --git a/src/Std/Time/Zoned/DateTime.lean b/src/Std/Time/Zoned/DateTime.lean index 8049652e01..f5555407ed 100644 --- a/src/Std/Time/Zoned/DateTime.lean +++ b/src/Std/Time/Zoned/DateTime.lean @@ -55,16 +55,16 @@ Creates a new `DateTime` out of a `Timestamp` that is in a `TimeZone`. -/ @[inline] def ofTimestamp (tm : Timestamp) (tz : TimeZone) : DateTime tz := - DateTime.mk tm (Thunk.mk fun _ => tm.toPlainDateTimeAssumingUTC |>.addSeconds tz.toSeconds) + DateTime.mk tm (Thunk.mk fun _ => PlainDateTime.ofWallTime (WallTime.ofTimestamp tm tz.offset)) instance : Inhabited (DateTime tz) where default := ofTimestamp Inhabited.default tz /-- -Converts a `DateTime` to the number of days since the UNIX epoch. +Returns the number of days since the UNIX epoch. -/ -def toDaysSinceUNIXEpoch (date : DateTime tz) : Day.Offset := - date.date.get.toDaysSinceUNIXEpoch +def toEpochDay (date : DateTime tz) : Day.Offset := + date.date.get.toEpochDay /-- Creates a `Timestamp` out of a `DateTime`. @@ -81,120 +81,111 @@ def convertTimeZone (date : DateTime tz) (tz₁ : TimeZone) : DateTime tz₁ := ofTimestamp date.timestamp tz₁ /-- -Creates a new `DateTime` out of a `PlainDateTime`. It assumes that the `PlainDateTime` is relative -to UTC. --/ -@[inline] -def ofPlainDateTimeAssumingUTC (date : PlainDateTime) (tz : TimeZone) : DateTime tz := - let tm := Timestamp.ofPlainDateTimeAssumingUTC date - DateTime.mk tm (Thunk.mk fun _ => date.addSeconds tz.toSeconds) - -/-- -Creates a new `DateTime` from a `PlainDateTime`, assuming that the `PlainDateTime` -is relative to the given `TimeZone`. +Creates a new `DateTime` out of a `PlainDateTime`. It assumes that the `PlainDateTime` is the Local +date time. -/ @[inline] def ofPlainDateTime (date : PlainDateTime) (tz : TimeZone) : DateTime tz := - let tm := date.subSeconds tz.toSeconds - DateTime.mk (Timestamp.ofPlainDateTimeAssumingUTC tm) (Thunk.mk fun _ => date) + let tm := Timestamp.ofWallTime date.toWallTime tz.offset + DateTime.mk tm (Thunk.mk fun _ => date) /-- Add `Hour.Offset` to a `DateTime`. -/ @[inline] def addHours (dt : DateTime tz) (hours : Hour.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.addHours hours) tz + ofTimestamp (dt.timestamp + hours) tz /-- Subtract `Hour.Offset` from a `DateTime`. -/ @[inline] def subHours (dt : DateTime tz) (hours : Hour.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.subHours hours) tz + ofTimestamp (dt.timestamp - hours) tz /-- Add `Minute.Offset` to a `DateTime`. -/ @[inline] def addMinutes (dt : DateTime tz) (minutes : Minute.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.addMinutes minutes) tz + ofTimestamp (dt.timestamp + minutes) tz /-- Subtract `Minute.Offset` from a `DateTime`. -/ @[inline] def subMinutes (dt : DateTime tz) (minutes : Minute.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.subMinutes minutes) tz + ofTimestamp (dt.timestamp - minutes) tz /-- Add `Second.Offset` to a `DateTime`. -/ @[inline] def addSeconds (dt : DateTime tz) (seconds : Second.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.addSeconds seconds) tz + ofTimestamp (dt.timestamp + seconds) tz /-- Subtract `Second.Offset` from a `DateTime`. -/ @[inline] def subSeconds (dt : DateTime tz) (seconds : Second.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.subSeconds seconds) tz + ofTimestamp (dt.timestamp - seconds) tz /-- Add `Millisecond.Offset` to a `DateTime`. -/ @[inline] def addMilliseconds (dt : DateTime tz) (milliseconds : Millisecond.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.addMilliseconds milliseconds) tz + ofTimestamp (dt.timestamp + milliseconds) tz /-- Subtract `Millisecond.Offset` from a `DateTime`. -/ @[inline] def subMilliseconds (dt : DateTime tz) (milliseconds : Millisecond.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.subMilliseconds milliseconds) tz + ofTimestamp (dt.timestamp - milliseconds) tz /-- Add `Nanosecond.Offset` to a `DateTime`. -/ @[inline] def addNanoseconds (dt : DateTime tz) (nanoseconds : Nanosecond.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.addNanoseconds nanoseconds) tz + ofTimestamp (dt.timestamp + nanoseconds) tz /-- Subtract `Nanosecond.Offset` from a `DateTime`. -/ @[inline] def subNanoseconds (dt : DateTime tz) (nanoseconds : Nanosecond.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.subNanoseconds nanoseconds) tz + ofTimestamp (dt.timestamp - nanoseconds) tz /-- Add `Day.Offset` to a `DateTime`. -/ @[inline] def addDays (dt : DateTime tz) (days : Day.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.addDays days) tz + ofTimestamp (dt.timestamp + days) tz /-- Subtracts `Day.Offset` to a `DateTime`. -/ @[inline] def subDays (dt : DateTime tz) (days : Day.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.subDays days) tz + ofTimestamp (dt.timestamp - days) tz /-- Add `Week.Offset` to a `DateTime`. -/ @[inline] def addWeeks (dt : DateTime tz) (weeks : Week.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.addWeeks weeks) tz + ofTimestamp (dt.timestamp + weeks) tz /-- Subtracts `Week.Offset` to a `DateTime`. -/ @[inline] def subWeeks (dt : DateTime tz) (weeks : Week.Offset) : DateTime tz := - ofPlainDateTime (dt.date.get.subWeeks weeks) tz + ofTimestamp (dt.timestamp - weeks) tz /-- Add `Month.Offset` to a `DateTime`, it clips the day to the last valid day of that month. @@ -468,11 +459,11 @@ def time (zdt : DateTime tz) : PlainTime := zdt.date.get.time /-- -Converts a `DateTime` to the number of days since the UNIX epoch. +Creates a `DateTime` from a number of days since the 1970-01-01T00:00:00. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (tz : TimeZone) : DateTime tz := - DateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) tz +def ofEpochDay (days : Day.Offset) (time : PlainTime) (tz : TimeZone) : DateTime tz := + DateTime.ofPlainDateTime (PlainDateTime.ofEpochDay days time) tz instance : HAdd (DateTime tz) (Day.Offset) (DateTime tz) where hAdd := addDays diff --git a/src/Std/Time/Zoned/ZoneRules.lean b/src/Std/Time/Zoned/ZoneRules.lean index f7140be05d..b2d1f78049 100644 --- a/src/Std/Time/Zoned/ZoneRules.lean +++ b/src/Std/Time/Zoned/ZoneRules.lean @@ -129,6 +129,12 @@ structure ZoneRules where namespace Transition +/-- +Returns the transition time as a `Timestamp`. +-/ +def timestamp (t : Transition) : Timestamp := + Timestamp.ofSecondsSinceUnixEpoch t.time + /-- Create a TimeZone from a Transition. -/ @@ -207,6 +213,22 @@ def findLocalTimeTypeForTimestamp (zr : ZoneRules) (timestamp : Timestamp) : Loc |>.map (·.localTimeType) |>.getD zr.initialLocalTimeType +/-- +Finds the `LocalTimeType` for a given wall-clock time (seconds since 1970-01-01T00:00:00 in local time). +Unlike `findLocalTimeTypeForTimestamp`, this compares each transition's UTC time adjusted by the +previous offset — necessary when converting local time to UTC. +-/ +def findLocalTimeTypeForWallTime (zr : ZoneRules) (wallTime : WallTime) : LocalTimeType := Id.run do + let mut ltt := zr.initialLocalTimeType + + for t in zr.transitions do + let localTransitionTime := t.timestamp.toWallTime ltt.gmtOffset + if wallTime < localTransitionTime then + return ltt + ltt := t.localTimeType + + return ltt + /-- Find the current `TimeZone` out of a `Transition` in a `ZoneRules` -/ diff --git a/src/Std/Time/Zoned/ZonedDateTime.lean b/src/Std/Time/Zoned/ZonedDateTime.lean index 062b0a50de..8c18bc5c43 100644 --- a/src/Std/Time/Zoned/ZonedDateTime.lean +++ b/src/Std/Time/Zoned/ZonedDateTime.lean @@ -56,38 +56,18 @@ Creates a new `ZonedDateTime` out of a `Timestamp` and a `ZoneRules`. @[inline] def ofTimestamp (tm : Timestamp) (rules : TimeZone.ZoneRules) : ZonedDateTime := let tz := rules.timezoneAt tm - ZonedDateTime.mk (Thunk.mk fun _ => tm.toPlainDateTimeAssumingUTC.addSeconds tz.toSeconds) tm rules tz + ZonedDateTime.mk (Thunk.mk fun _ => PlainDateTime.ofWallTime (Timestamp.toWallTime tm tz.offset)) tm rules tz /-- -Creates a new `ZonedDateTime` out of a `PlainDateTime` and a `ZoneRules`. +Creates a new `ZonedDateTime` out of a `PlainDateTime` and a `ZoneRules`. It assumes `PlainDateTime` is +the local time. -/ @[inline] def ofPlainDateTime (pdt : PlainDateTime) (zr : TimeZone.ZoneRules) : ZonedDateTime := - let tm := pdt.toTimestampAssumingUTC - - let transition := - let value := tm.toSecondsSinceUnixEpoch - if let some idx := zr.transitions.findFinIdx? (fun t => t.time.val ≥ value.val) - then - let last := zr.transitions[idx.1 - 1] - let next := zr.transitions[idx] - - let utcNext := next.time.sub last.localTimeType.gmtOffset.second.abs - - if utcNext.val > tm.toSecondsSinceUnixEpoch.val - then some last - else some next - - else zr.transitions.back? - - let tz := - transition - |>.map (·.localTimeType) - |>.getD zr.initialLocalTimeType - |>.getTimeZone - - let tm := tm.subSeconds tz.toSeconds - ZonedDateTime.mk (Thunk.mk fun _ => tm.toPlainDateTimeAssumingUTC.addSeconds tz.toSeconds) tm zr tz + let wt := pdt.toWallTime + let ltt := zr.findLocalTimeTypeForWallTime wt + let tz := ltt.getTimeZone + ZonedDateTime.mk (Thunk.mk fun _ => pdt) (wt.toTimestamp tz.offset) zr tz /-- Creates a new `ZonedDateTime` out of a `Timestamp` and a `TimeZone`. @@ -97,7 +77,8 @@ def ofTimestampWithZone (tm : Timestamp) (tz : TimeZone) : ZonedDateTime := ofTimestamp tm (TimeZone.ZoneRules.ofTimeZone tz) /-- -Creates a new `ZonedDateTime` out of a `PlainDateTime` and a `TimeZone`. +Creates a new `ZonedDateTime` out of a `PlainDateTime` and a `TimeZone`. It assumes `PlainDateTime` is +the local time. -/ @[inline] def ofPlainDateTimeWithZone (tm : PlainDateTime) (tz : TimeZone) : ZonedDateTime := @@ -117,14 +98,6 @@ Changes the `ZoneRules` to a new one. def convertZoneRules (date : ZonedDateTime) (tz₁ : TimeZone.ZoneRules) : ZonedDateTime := ofTimestamp date.toTimestamp tz₁ -/-- -Creates a new `ZonedDateTime` out of a `PlainDateTime`. It assumes that the `PlainDateTime` is relative -to UTC. --/ -@[inline] -def ofPlainDateTimeAssumingUTC (date : PlainDateTime) (tz : TimeZone.ZoneRules) : ZonedDateTime := - ofTimestamp date.toTimestampAssumingUTC tz - /-- Converts a `ZonedDateTime` to a `PlainDateTime` -/ @@ -256,158 +229,131 @@ def quarter (date : ZonedDateTime) : Internal.Bounded.LE 1 4 := Add `Day.Offset` to a `ZonedDateTime`. -/ def addDays (dt : ZonedDateTime) (days : Day.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addDays days).toTimestampAssumingUTC dt.rules + .ofTimestamp (dt.timestamp + days) dt.rules /-- Subtract `Day.Offset` from a `ZonedDateTime`. -/ def subDays (dt : ZonedDateTime) (days : Day.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subDays days).toTimestampAssumingUTC dt.rules + .ofTimestamp (dt.timestamp - days) dt.rules /-- Add `Week.Offset` to a `ZonedDateTime`. -/ def addWeeks (dt : ZonedDateTime) (weeks : Week.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addWeeks weeks).toTimestampAssumingUTC dt.rules + .ofTimestamp (dt.timestamp + weeks) dt.rules /-- Subtract `Week.Offset` from a `ZonedDateTime`. -/ def subWeeks (dt : ZonedDateTime) (weeks : Week.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subWeeks weeks).toTimestampAssumingUTC dt.rules + .ofTimestamp (dt.timestamp - weeks) dt.rules /-- Add `Month.Offset` to a `ZonedDateTime`, clipping to the last valid day. -/ def addMonthsClip (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addMonthsClip months).toTimestampAssumingUTC dt.rules + .ofPlainDateTime (dt.toPlainDateTime.addMonthsClip months) dt.rules /-- Subtract `Month.Offset` from a `ZonedDateTime`, clipping to the last valid day. -/ def subMonthsClip (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subMonthsClip months).toTimestampAssumingUTC dt.rules + .ofPlainDateTime (dt.toPlainDateTime.subMonthsClip months) dt.rules /-- Add `Month.Offset` to a `ZonedDateTime`, rolling over excess days. -/ def addMonthsRollOver (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addMonthsRollOver months).toTimestampAssumingUTC dt.rules + .ofPlainDateTime (dt.toPlainDateTime.addMonthsRollOver months) dt.rules /-- Subtract `Month.Offset` from a `ZonedDateTime`, rolling over excess days. -/ def subMonthsRollOver (dt : ZonedDateTime) (months : Month.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subMonthsRollOver months).toTimestampAssumingUTC dt.rules + .ofPlainDateTime (dt.toPlainDateTime.subMonthsRollOver months) dt.rules /-- Add `Year.Offset` to a `ZonedDateTime`, rolling over excess days. -/ def addYearsRollOver (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addYearsRollOver years).toTimestampAssumingUTC dt.rules + .ofPlainDateTime (dt.toPlainDateTime.addYearsRollOver years) dt.rules /-- Add `Year.Offset` to a `ZonedDateTime`, clipping to the last valid day. -/ def addYearsClip (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addYearsClip years).toTimestampAssumingUTC dt.rules + .ofPlainDateTime (dt.toPlainDateTime.addYearsClip years) dt.rules /-- Subtract `Year.Offset` from a `ZonedDateTime`, clipping to the last valid day. -/ def subYearsClip (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subYearsClip years).toTimestampAssumingUTC dt.rules + .ofPlainDateTime (dt.toPlainDateTime.subYearsClip years) dt.rules /-- Subtract `Year.Offset` from a `ZonedDateTime`, rolling over excess days. -/ def subYearsRollOver (dt : ZonedDateTime) (years : Year.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subYearsRollOver years).toTimestampAssumingUTC dt.rules + .ofPlainDateTime (dt.toPlainDateTime.subYearsRollOver years) dt.rules /-- Add `Hour.Offset` to a `ZonedDateTime`. -/ def addHours (dt : ZonedDateTime) (hours : Hour.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addHours hours).toTimestampAssumingUTC dt.rules + .ofTimestamp (dt.timestamp + hours) dt.rules /-- Subtract `Hour.Offset` from a `ZonedDateTime`. -/ def subHours (dt : ZonedDateTime) (hours : Hour.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subHours hours).toTimestampAssumingUTC dt.rules - + .ofTimestamp (dt.timestamp - hours) dt.rules /-- Add `Minute.Offset` to a `ZonedDateTime`. -/ def addMinutes (dt : ZonedDateTime) (minutes : Minute.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addMinutes minutes).toTimestampAssumingUTC dt.rules + .ofTimestamp (dt.timestamp + minutes) dt.rules /-- Subtract `Minute.Offset` from a `ZonedDateTime`. -/ def subMinutes (dt : ZonedDateTime) (minutes : Minute.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subMinutes minutes).toTimestampAssumingUTC dt.rules - + .ofTimestamp (dt.timestamp - minutes) dt.rules /-- Add `Millisecond.Offset` to a `DateTime`. -/ @[inline] def addMilliseconds (dt : ZonedDateTime) (milliseconds : Millisecond.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addMilliseconds milliseconds).toTimestampAssumingUTC dt.rules + .ofTimestamp (dt.timestamp + milliseconds) dt.rules /-- Subtract `Millisecond.Offset` from a `DateTime`. -/ @[inline] def subMilliseconds (dt : ZonedDateTime) (milliseconds : Millisecond.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subMilliseconds milliseconds).toTimestampAssumingUTC dt.rules - + .ofTimestamp (dt.timestamp - milliseconds) dt.rules /-- Add `Second.Offset` to a `ZonedDateTime`. -/ def addSeconds (dt : ZonedDateTime) (seconds : Second.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addSeconds seconds).toTimestampAssumingUTC dt.rules + .ofTimestamp (dt.timestamp + seconds) dt.rules /-- Subtract `Second.Offset` from a `ZonedDateTime`. -/ def subSeconds (dt : ZonedDateTime) (seconds : Second.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subSeconds seconds).toTimestampAssumingUTC dt.rules - + .ofTimestamp (dt.timestamp - seconds) dt.rules /-- Add `Nanosecond.Offset` to a `ZonedDateTime`. -/ def addNanoseconds (dt : ZonedDateTime) (nanoseconds : Nanosecond.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.addNanoseconds nanoseconds).toTimestampAssumingUTC dt.rules + .ofTimestamp (dt.timestamp + nanoseconds) dt.rules /-- Subtract `Nanosecond.Offset` from a `ZonedDateTime`. -/ def subNanoseconds (dt : ZonedDateTime) (nanoseconds : Nanosecond.Offset) : ZonedDateTime := - let date := dt.timestamp.toPlainDateTimeAssumingUTC - ZonedDateTime.ofTimestamp (date.subNanoseconds nanoseconds).toTimestampAssumingUTC dt.rules - + .ofTimestamp (dt.timestamp - nanoseconds) dt.rules /-- Determines the era of the given `ZonedDateTime` based on its year. -/ @@ -420,7 +366,7 @@ Sets the `ZonedDateTime` to the specified `desiredWeekday`. -/ def withWeekday (dt : ZonedDateTime) (desiredWeekday : Weekday) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withWeekday desiredWeekday) dt.rules + .ofPlainDateTime (date.withWeekday desiredWeekday) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the day of the month to the given `days` value, with any @@ -429,7 +375,7 @@ out-of-range days clipped to the nearest valid date. @[inline] def withDaysClip (dt : ZonedDateTime) (days : Day.Ordinal) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withDaysClip days) dt.rules + .ofPlainDateTime (date.withDaysClip days) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the day of the month to the given `days` value, with any @@ -438,7 +384,7 @@ out-of-range days rolled over to the next month or year as needed. @[inline] def withDaysRollOver (dt : ZonedDateTime) (days : Day.Ordinal) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withDaysRollOver days) dt.rules + .ofPlainDateTime (date.withDaysRollOver days) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the month to the given `month` value. @@ -447,7 +393,7 @@ The day remains unchanged, and any invalid days for the new month will be handle @[inline] def withMonthClip (dt : ZonedDateTime) (month : Month.Ordinal) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withMonthClip month) dt.rules + .ofPlainDateTime (date.withMonthClip month) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the month to the given `month` value. @@ -456,7 +402,7 @@ The day is rolled over to the next valid month if necessary. @[inline] def withMonthRollOver (dt : ZonedDateTime) (month : Month.Ordinal) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withMonthRollOver month) dt.rules + .ofPlainDateTime (date.withMonthRollOver month) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the year to the given `year` value. The month and day remain unchanged, @@ -466,7 +412,7 @@ and any invalid days for the new year will be handled according to the `clip` be def withYearClip (dt : ZonedDateTime) (year : Year.Offset) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withYearClip year) dt.rules + .ofPlainDateTime (date.withYearClip year) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the year to the given `year` value. The month and day are rolled @@ -475,7 +421,7 @@ over to the next valid month and day if necessary. @[inline] def withYearRollOver (dt : ZonedDateTime) (year : Year.Offset) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withYearRollOver year) dt.rules + .ofPlainDateTime (date.withYearRollOver year) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the `hour` component. @@ -483,7 +429,7 @@ Creates a new `ZonedDateTime` by adjusting the `hour` component. @[inline] def withHours (dt : ZonedDateTime) (hour : Hour.Ordinal) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withHours hour) dt.rules + .ofPlainDateTime (date.withHours hour) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the `minute` component. @@ -491,7 +437,7 @@ Creates a new `ZonedDateTime` by adjusting the `minute` component. @[inline] def withMinutes (dt : ZonedDateTime) (minute : Minute.Ordinal) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withMinutes minute) dt.rules + .ofPlainDateTime (date.withMinutes minute) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the `second` component. @@ -499,7 +445,7 @@ Creates a new `ZonedDateTime` by adjusting the `second` component. @[inline] def withSeconds (dt : ZonedDateTime) (second : Second.Ordinal true) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withSeconds second) dt.rules + .ofPlainDateTime (date.withSeconds second) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the `nano` component with a new `millis` that will set @@ -508,7 +454,7 @@ in the millisecond scale. @[inline] def withMilliseconds (dt : ZonedDateTime) (millis : Millisecond.Ordinal) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withMilliseconds millis) dt.rules + .ofPlainDateTime (date.withMilliseconds millis) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the `nano` component. @@ -516,7 +462,7 @@ Creates a new `ZonedDateTime` by adjusting the `nano` component. @[inline] def withNanoseconds (dt : ZonedDateTime) (nano : Nanosecond.Ordinal) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withNanoseconds nano) dt.rules + .ofPlainDateTime (date.withNanoseconds nano) dt.rules /-- Checks if the `ZonedDateTime` is in a leap year. @@ -525,17 +471,18 @@ def inLeapYear (date : ZonedDateTime) : Bool := date.year.isLeap /-- -Converts a `ZonedDateTime` to the number of days since the UNIX epoch. +Returns the local (civil) date of the `ZonedDateTime` as a `Day.Offset` relative to 1970-01-01. -/ -def toDaysSinceUNIXEpoch (date : ZonedDateTime) : Day.Offset := - date.date.get.toDaysSinceUNIXEpoch +def toEpochDay (date : ZonedDateTime) : Day.Offset := + date.date.get.toEpochDay /-- -Converts a `ZonedDateTime` to the number of days since the UNIX epoch. +Creates a `ZonedDateTime` from a local date given as a `Day.Offset` relative to 1970-01-01, a +`PlainTime`, and `ZoneRules`. The day offset is interpreted as a local (civil) date, not UTC. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (zt : TimeZone.ZoneRules) : ZonedDateTime := - ZonedDateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) zt +def ofEpochDay (days : Day.Offset) (time : PlainTime) (zt : TimeZone.ZoneRules) : ZonedDateTime := + ZonedDateTime.ofPlainDateTime (PlainDateTime.ofEpochDay days time) zt instance : HAdd ZonedDateTime Day.Offset ZonedDateTime where hAdd := addDays diff --git a/tests/elab/timeAPI.lean b/tests/elab/timeAPI.lean index 0bdf95d920..e5952b29b3 100644 --- a/tests/elab/timeAPI.lean +++ b/tests/elab/timeAPI.lean @@ -633,9 +633,9 @@ Std.Time.Weekday.friday println! date.toLeanDateString println! date.toSQLDateString - println! date.toDaysSinceUNIXEpoch - println! date.toTimestampAssumingUTC - println! PlainDate.ofDaysSinceUNIXEpoch 1 + println! date.toEpochDay + println! date.toWallTime + println! PlainDate.ofEpochDay 1 /-- info: 1997-03-19T02:03:04.000000000 @@ -707,9 +707,9 @@ Std.Time.Weekday.tuesday println! repr plaindatetime.weekOfYear println! repr plaindatetime.weekOfMonth - println! plaindatetime.toDaysSinceUNIXEpoch - println! plaindatetime.toTimestampAssumingUTC - println! PlainDateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight + println! plaindatetime.toEpochDay + println! plaindatetime.toWallTime + println! PlainDateTime.ofEpochDay 1 PlainTime.midnight /-- info: 2024-09-13T02:01:02.000000000-03:00 @@ -747,7 +747,7 @@ Std.Time.Weekday.thursday -/ #guard_msgs in #eval do - let zoned := DateTime.ofPlainDateTimeAssumingUTC datetime("2024-09-12T05:01:02") timezone("America/Sao_Paulo -03:00") + let zoned := DateTime.ofPlainDateTime datetime("2024-09-12T02:01:02") timezone("America/Sao_Paulo -03:00") println! zoned.addDays 1 println! zoned.addWeeks 1 @@ -781,9 +781,9 @@ Std.Time.Weekday.thursday println! repr zoned.weekOfYear println! repr zoned.weekOfMonth - println! zoned.toDaysSinceUNIXEpoch + println! zoned.toEpochDay println! zoned.toTimestamp - println! DateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC + println! DateTime.ofEpochDay 1 PlainTime.midnight .UTC /-- info: 1997-03-19T02:03:04.000000000[America/Sao_Paulo] @@ -856,7 +856,7 @@ Std.Time.Weekday.tuesday println! repr zoned.weekOfYear println! repr zoned.weekOfMonth - println! zoned.toDaysSinceUNIXEpoch + println! zoned.toEpochDay println! zoned.toTimestamp /-- @@ -868,22 +868,20 @@ info: 2023-06-09T00:00:00.000000000 #eval do println! PlainDateTime.ofPlainDate date("2023-06-09") println! PlainDateTime.ofPlainTime time("12:32:43") - println! PlainDateTime.ofDaysSinceUNIXEpoch 23332 time("12:32:43") + println! PlainDateTime.ofEpochDay 23332 time("12:32:43") /-- info: 1970-01-02T00:00:00.000000000Z 1997-03-18T00:00:00.000000000Z 1997-03-18T00:01:02.000000000Z -1997-03-18T00:01:02.000000000Z 2024-02-16T22:07:14.000000000Z -/ #guard_msgs in #eval do - println! DateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC - println! DateTime.ofPlainDate date("1997-03-18") .UTC + println! DateTime.ofEpochDay 1 PlainTime.midnight .UTC + println! DateTime.ofLocalDate date("1997-03-18") .UTC println! DateTime.ofPlainDateTime datetime("1997-03-18T00:01:02") .UTC - println! DateTime.ofPlainDateTimeAssumingUTC datetime("1997-03-18T00:01:02") .UTC println! DateTime.ofTimestamp 1708121234 .UTC /-- @@ -892,17 +890,15 @@ info: 1970-01-02T00:00:00.000000000[UTC] 1997-03-18T00:00:00.000000000[UTC] 1997-03-18T00:01:02.000000000[UTC] 1997-03-18T00:01:02.000000000[UTC] -1997-03-18T00:01:02.000000000[UTC] 2024-02-16T22:07:14.000000000[UTC] 2024-02-16T22:07:14.000000000[UTC] -/ #guard_msgs in #eval do - println! ZonedDateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC - println! ZonedDateTime.ofPlainDate date("1997-03-18") .UTC - println! ZonedDateTime.ofPlainDateWithZone date("1997-03-18") .UTC + println! ZonedDateTime.ofEpochDay 1 PlainTime.midnight .UTC + println! ZonedDateTime.ofLocalDate date("1997-03-18") .UTC + println! ZonedDateTime.ofLocalDateWithZone date("1997-03-18") .UTC println! ZonedDateTime.ofPlainDateTime datetime("1997-03-18T00:01:02") .UTC - println! ZonedDateTime.ofPlainDateTimeAssumingUTC datetime("1997-03-18T00:01:02") .UTC println! ZonedDateTime.ofPlainDateTimeWithZone datetime("1997-03-18T00:01:02") .UTC println! ZonedDateTime.ofTimestamp 1708121234 .UTC println! ZonedDateTime.ofTimestampWithZone 1708121234 .UTC diff --git a/tests/elab/timeClassOperations.lean b/tests/elab/timeClassOperations.lean index 39f1967df9..eccf54401a 100644 --- a/tests/elab/timeClassOperations.lean +++ b/tests/elab/timeClassOperations.lean @@ -165,8 +165,8 @@ info: "3600s" #guard_msgs in #eval zoned("2000-12-20T00:00:00-03:00") - zoned("2000-12-20T00:00:00-02:00") -def now := PlainDateTime.ofTimestampAssumingUTC ⟨1724859638, ⟨907328169, by decide⟩, by decide⟩ -def after := PlainDateTime.ofTimestampAssumingUTC ⟨1724859639, ⟨907641224, by decide⟩, by decide⟩ +def now := PlainDateTime.ofWallTime (WallTime.ofDuration ⟨1724859638, ⟨907328169, by decide⟩, by decide⟩) +def after := PlainDateTime.ofWallTime (WallTime.ofDuration ⟨1724859639, ⟨907641224, by decide⟩, by decide⟩) def duration := after - now /-- diff --git a/tests/elab/timeFormats.lean b/tests/elab/timeFormats.lean index baa6571f87..27f1bbf974 100644 --- a/tests/elab/timeFormats.lean +++ b/tests/elab/timeFormats.lean @@ -132,7 +132,7 @@ def localTm : Second.Offset := 1723730627 /-- This PlainDate is relative to the local time. -/ -def PlainDate : PlainDateTime := Timestamp.toPlainDateTimeAssumingUTC (Timestamp.ofSecondsSinceUnixEpoch localTm) +def PlainDate : PlainDateTime := PlainDateTime.ofWallTime (WallTime.ofSeconds localTm) def dateBR₁ := DateTime.ofPlainDateTime PlainDate brTZ def dateJP₁ := DateTime.ofPlainDateTime PlainDate jpTZ @@ -215,37 +215,37 @@ info: "06/16/2014" info: "0053-06-19" -/ #guard_msgs in -#eval Formats.sqlDate.format (DateTime.ofPlainDate (PlainDate.ofDaysSinceUNIXEpoch ⟨-700000⟩) .UTC) +#eval Formats.sqlDate.format (DateTime.ofLocalDate (PlainDate.ofEpochDay ⟨-700000⟩) .UTC) /-- info: "-0002-09-16" -/ #guard_msgs in -#eval Formats.sqlDate.format (DateTime.ofPlainDate (PlainDate.ofDaysSinceUNIXEpoch ⟨-720000⟩) .UTC) +#eval Formats.sqlDate.format (DateTime.ofLocalDate (PlainDate.ofEpochDay ⟨-720000⟩) .UTC) /-- info: "-0084-07-28" -/ #guard_msgs in -#eval Formats.sqlDate.format (DateTime.ofPlainDate (PlainDate.ofDaysSinceUNIXEpoch ⟨-750000⟩) .UTC) +#eval Formats.sqlDate.format (DateTime.ofLocalDate (PlainDate.ofEpochDay ⟨-750000⟩) .UTC) /-- info: "-0221-09-04" -/ #guard_msgs in -#eval Formats.sqlDate.format (DateTime.ofPlainDate (PlainDate.ofDaysSinceUNIXEpoch ⟨-800000⟩) .UTC) +#eval Formats.sqlDate.format (DateTime.ofLocalDate (PlainDate.ofEpochDay ⟨-800000⟩) .UTC) /-- info: date("-0221-09-04") -/ #guard_msgs in -#eval PlainDate.ofDaysSinceUNIXEpoch ⟨-800000⟩ +#eval PlainDate.ofEpochDay ⟨-800000⟩ /-- info: date("-0221-09-04") -/ #guard_msgs in -#eval PlainDate.ofDaysSinceUNIXEpoch ⟨-800000⟩ +#eval PlainDate.ofEpochDay ⟨-800000⟩ /-- info: date("2002-07-14") diff --git a/tests/elab/timeLimits.lean b/tests/elab/timeLimits.lean index 92b0abe9e7..59df7e4760 100644 --- a/tests/elab/timeLimits.lean +++ b/tests/elab/timeLimits.lean @@ -7,7 +7,7 @@ def ISO8601UTCNot : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSS def ISO8601UTCDef : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ") /-- -info: Except.ok (zoned("2002-07-14T23:14:00.324354679-23:59")) +info: Except.ok (zoned("2002-07-14T23:13:60.324354679-23:59")) -/ #guard_msgs in #eval ISO8601UTCAllow.parse "2002-07-14T23:13:60.324354679-2359" diff --git a/tests/elab/timeLocalDateTime.lean b/tests/elab/timeLocalDateTime.lean index 3ee7341a83..2295ffa317 100644 --- a/tests/elab/timeLocalDateTime.lean +++ b/tests/elab/timeLocalDateTime.lean @@ -32,37 +32,37 @@ info: "09/05/1993 12:59:59" info: 753700087 -/ #guard_msgs in -#eval date₁.toTimestampAssumingUTC.toSecondsSinceUnixEpoch +#eval date₁.toWallTime.toSeconds /-- info: 736952399 -/ #guard_msgs in -#eval date₂.toTimestampAssumingUTC.toSecondsSinceUnixEpoch +#eval date₂.toWallTime.toSeconds /-- info: "09/05/1993 12:59:59" -/ #guard_msgs in -#eval PlainDateTime.ofTimestampAssumingUTC 736952399 |> format +#eval PlainDateTime.ofWallTime 736952399 |> format /-- info: 736952399 -/ #guard_msgs in -#eval PlainDateTime.toTimestampAssumingUTC date₂ |>.toSecondsSinceUnixEpoch +#eval PlainDateTime.toWallTime date₂ |>.toSeconds /-- info: "16/08/2024" -/ #guard_msgs in -#eval PlainDate.ofDaysSinceUNIXEpoch 19951 |> format₂ +#eval PlainDate.ofEpochDay 19951 |> format₂ /-- info: 19951 -/ #guard_msgs in -#eval PlainDate.toDaysSinceUNIXEpoch date₃ +#eval PlainDate.toEpochDay date₃ /-- info: Std.Time.Weekday.friday @@ -79,8 +79,8 @@ info: #[] for i in *...(10000 : Nat) do let i := Int.ofNat i - 999975 - let date := PlainDate.ofDaysSinceUNIXEpoch (Day.Offset.ofInt i) - let num := date.toDaysSinceUNIXEpoch + let date := PlainDate.ofEpochDay (Day.Offset.ofInt i) + let num := date.toEpochDay if i ≠ num.val then res := res.push i diff --git a/tests/elab/timeNegative.lean b/tests/elab/timeNegative.lean index 66e3bb88b0..b70204f0f1 100644 --- a/tests/elab/timeNegative.lean +++ b/tests/elab/timeNegative.lean @@ -3,28 +3,28 @@ import Init open Std.Time /-- -info: Timestamp.ofNanosecondsSinceUnixEpoch -999999999 +info: WallTime.ofNanoseconds -999999999 -/ #guard_msgs in -#eval datetime("1969-12-31T23:59:59.000000001").toTimestampAssumingUTC +#eval datetime("1969-12-31T23:59:59.000000001").toWallTime /-- -info: Timestamp.ofNanosecondsSinceUnixEpoch -1000000000 +info: WallTime.ofNanoseconds -1000000000 -/ #guard_msgs in -#eval datetime("1969-12-31T23:59:59.000000000").toTimestampAssumingUTC +#eval datetime("1969-12-31T23:59:59.000000000").toWallTime /-- info: datetime("1969-12-31T23:59:59.000000001") -/ #guard_msgs in -#eval datetime("1969-12-31T23:59:59.000000001").toTimestampAssumingUTC.toPlainDateTimeAssumingUTC +#eval datetime("1969-12-31T23:59:59.000000001").toWallTime |> PlainDateTime.ofWallTime /-- info: datetime("1969-12-31T23:59:59.000000000") -/ #guard_msgs in -#eval datetime("1969-12-31T23:59:59.000000000").toTimestampAssumingUTC.toPlainDateTimeAssumingUTC +#eval datetime("1969-12-31T23:59:59.000000000").toWallTime |> PlainDateTime.ofWallTime /-- info: datetime("1969-12-31T23:59:59.000000001") @@ -45,23 +45,23 @@ info: datetime("1970-01-01T00:00:01.000000000") #eval datetime("1970-01-01T00:00:00.999999999") + (1 : Nanosecond.Offset) /-- -info: Timestamp.ofNanosecondsSinceUnixEpoch -1 +info: WallTime.ofNanoseconds -1 -/ #guard_msgs in -#eval datetime("1969-12-31T23:59:59.999999999").toTimestampAssumingUTC +#eval datetime("1969-12-31T23:59:59.999999999").toWallTime /-- -info: Timestamp.ofNanosecondsSinceUnixEpoch 0 +info: WallTime.ofNanoseconds 0 -/ #guard_msgs in -#eval datetime("1969-12-31T23:59:59.999999999").toTimestampAssumingUTC + (1 : Nanosecond.Offset) +#eval datetime("1969-12-31T23:59:59.999999999").toWallTime + (1 : Nanosecond.Offset) /-- info: datetime("1970-01-01T00:00:00.000000000") -/ #guard_msgs in -#eval PlainDateTime.ofTimestampAssumingUTC 0 +#eval PlainDateTime.ofWallTime 0 /-- info: 121 @@ -79,4 +79,4 @@ info: 35 info: datetime("1906-08-27T23:59:59.999999999") -/ #guard_msgs in -#eval datetime("1906-08-27T23:59:59.999999999").toTimestampAssumingUTC.toPlainDateTimeAssumingUTC +#eval datetime("1906-08-27T23:59:59.999999999").toWallTime |> PlainDateTime.ofWallTime diff --git a/tests/elab/timeParse.lean b/tests/elab/timeParse.lean index 09de21d9bd..c854972923 100644 --- a/tests/elab/timeParse.lean +++ b/tests/elab/timeParse.lean @@ -141,7 +141,7 @@ def localTm : Second.Offset := 1723730627 /-- This PlainDate is relative to the local time. -/ -def PlainDate : PlainDateTime := Timestamp.toPlainDateTimeAssumingUTC (Timestamp.ofSecondsSinceUnixEpoch localTm) +def PlainDate : PlainDateTime := PlainDateTime.ofWallTime (WallTime.ofSeconds localTm) def dateBR₁ := DateTime.ofPlainDateTime PlainDate brTZ def dateJP₁ := DateTime.ofPlainDateTime PlainDate jpTZ