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>
This commit is contained in:
Sofia Rodrigues
GitHub
parent
d055778913
commit
f67ea44b6a
19 changed files with 585 additions and 284 deletions
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
312
src/Std/Time/DateTime/WallTime.lean
Normal file
312
src/Std/Time/DateTime/WallTime.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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`.
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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`
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
/--
|
||||
|
|
|
|||
|
|
@ -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")
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue