From 5a401f772ad3800d262cc956cd87d21444eddd66 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Thu, 16 Jan 2025 12:40:28 -0300 Subject: [PATCH] fix: negative timestamps and dates before 1970 --- src/Std/Time/DateTime/PlainDateTime.lean | 54 ++++++---------- src/Std/Time/Duration.lean | 16 +++-- src/Std/Time/Internal/UnitVal.lean | 11 +++- tests/lean/run/timeAPI.lean | 4 +- tests/lean/run/timeNegative.lean | 82 ++++++++++++++++++++++++ tests/lean/run/timeParse.lean | 6 +- 6 files changed, 126 insertions(+), 47 deletions(-) create mode 100644 tests/lean/run/timeNegative.lean diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index b97ca53c3f14..787238ce9fb5 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -53,7 +53,7 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do let nanos := stamp.toNanosecondsSinceUnixEpoch let secs : Second.Offset := nanos.ediv 1000000000 - let daysSinceEpoch : Day.Offset := secs.ediv 86400 + let daysSinceEpoch : Day.Offset := secs.tdiv 86400 let boundedDaysSinceEpoch := daysSinceEpoch let mut rawDays := boundedDaysSinceEpoch - leapYearEpoch @@ -315,16 +315,26 @@ resulting month. def subYearsClip (dt : PlainDateTime) (years : Year.Offset) : PlainDateTime := { dt with date := dt.date.subYearsClip years } +/-- +Adds a `Nanosecond.Offset` to a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds overflow. +-/ +@[inline] +def addNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime := + ofTimestampAssumingUTC (dt.toTimestampAssumingUTC + nanos) + +/-- +Subtracts a `Nanosecond.Offset` from a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds underflow. +-/ +@[inline] +def subNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime := + addNanoseconds dt (-nanos) /-- Adds an `Hour.Offset` to a `PlainDateTime`, adjusting the date if the hour overflows. -/ @[inline] def addHours (dt : PlainDateTime) (hours : Hour.Offset) : PlainDateTime := - let totalSeconds := dt.time.toSeconds + hours.toSeconds - let days := totalSeconds.ediv 86400 - let newTime := dt.time.addSeconds (hours.toSeconds) - { dt with date := dt.date.addDays days, time := newTime } + addNanoseconds dt hours.toNanoseconds /-- Subtracts an `Hour.Offset` from a `PlainDateTime`, adjusting the date if the hour underflows. @@ -338,10 +348,7 @@ Adds a `Minute.Offset` to a `PlainDateTime`, adjusting the hour and date if the -/ @[inline] def addMinutes (dt : PlainDateTime) (minutes : Minute.Offset) : PlainDateTime := - let totalSeconds := dt.time.toSeconds + minutes.toSeconds - let days := totalSeconds.ediv 86400 - let newTime := dt.time.addSeconds (minutes.toSeconds) - { dt with date := dt.date.addDays days, time := newTime } + addNanoseconds dt minutes.toNanoseconds /-- Subtracts a `Minute.Offset` from a `PlainDateTime`, adjusting the hour and date if the minutes underflow. @@ -355,10 +362,7 @@ Adds a `Second.Offset` to a `PlainDateTime`, adjusting the minute, hour, and dat -/ @[inline] def addSeconds (dt : PlainDateTime) (seconds : Second.Offset) : PlainDateTime := - let totalSeconds := dt.time.toSeconds + seconds - let days := totalSeconds.ediv 86400 - let newTime := dt.time.addSeconds seconds - { dt with date := dt.date.addDays days, time := newTime } + addNanoseconds dt seconds.toNanoseconds /-- Subtracts a `Second.Offset` from a `PlainDateTime`, adjusting the minute, hour, and date if the seconds underflow. @@ -372,10 +376,7 @@ Adds a `Millisecond.Offset` to a `PlainDateTime`, adjusting the second, minute, -/ @[inline] def addMilliseconds (dt : PlainDateTime) (milliseconds : Millisecond.Offset) : PlainDateTime := - let totalMilliseconds := dt.time.toMilliseconds + milliseconds - let days := totalMilliseconds.ediv 86400000 -- 86400000 ms in a day - let newTime := dt.time.addMilliseconds milliseconds - { dt with date := dt.date.addDays days, time := newTime } + addNanoseconds dt milliseconds.toNanoseconds /-- Subtracts a `Millisecond.Offset` from a `PlainDateTime`, adjusting the second, minute, hour, and date if the milliseconds underflow. @@ -384,25 +385,6 @@ Subtracts a `Millisecond.Offset` from a `PlainDateTime`, adjusting the second, m def subMilliseconds (dt : PlainDateTime) (milliseconds : Millisecond.Offset) : PlainDateTime := addMilliseconds dt (-milliseconds) -/-- -Adds a `Nanosecond.Offset` to a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds overflow. --/ -@[inline] -def addNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime := - let nano := Nanosecond.Offset.ofInt dt.time.nanosecond.val - let totalNanos := nano + nanos - let extraSeconds := totalNanos.ediv 1000000000 - let nanosecond := Bounded.LE.byEmod totalNanos.val 1000000000 (by decide) - let newTime := dt.time.addSeconds extraSeconds - { dt with time := { newTime with nanosecond } } - -/-- -Subtracts a `Nanosecond.Offset` from a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds underflow. --/ -@[inline] -def subNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime := - addNanoseconds dt (-nanos) - /-- Getter for the `Year` inside of a `PlainDateTime`. -/ diff --git a/src/Std/Time/Duration.lean b/src/Std/Time/Duration.lean index 54d6d0364340..8560ae61244f 100644 --- a/src/Std/Time/Duration.lean +++ b/src/Std/Time/Duration.lean @@ -82,15 +82,21 @@ def ofSeconds (s : Second.Offset) : Duration := by Creates a new `Duration` out of `Nanosecond.Offset`. -/ def ofNanoseconds (s : Nanosecond.Offset) : Duration := by - refine ⟨s.ediv 1000000000, Bounded.LE.byMod s.val 1000000000 (by decide), ?_⟩ + refine ⟨s.tdiv 1000000000, Bounded.LE.byMod s.val 1000000000 (by decide), ?_⟩ + cases Int.le_total s.val 0 - next n => exact Or.inr (And.intro (Int.ediv_le_ediv (by decide) n) (mod_nonpos 1000000000 n (by decide))) - next n => exact Or.inl (And.intro (Int.ediv_nonneg n (by decide)) (Int.tmod_nonneg 1000000000 n)) + next n => exact Or.inr (And.intro (tdiv_neg n (by decide)) (mod_nonpos 1000000000 n (by decide))) + next n => exact Or.inl (And.intro (Int.tdiv_nonneg n (by decide)) (Int.tmod_nonneg 1000000000 n)) where mod_nonpos : ∀ {a : Int} (b : Int), (a ≤ 0) → (b ≥ 0) → 0 ≥ a.tmod b | .negSucc m, .ofNat n, _, _ => Int.neg_le_neg (Int.tmod_nonneg (↑n) (Int.ofNat_le.mpr (Nat.zero_le (m + 1)))) | 0, n, _, _ => Int.eq_iff_le_and_ge.mp (Int.zero_tmod n) |>.left + tdiv_neg {a b : Int} (Ha : a ≤ 0) (Hb : 0 ≤ b) : a.tdiv b ≤ 0 := + match a, b, Ha with + | .negSucc _, .ofNat _, _ => Int.neg_le_neg (Int.ofNat_le.mpr (Nat.zero_le _)) + | 0, n, _ => Int.eq_iff_le_and_ge.mp (Int.zero_tdiv n) |>.left + /-- Creates a new `Duration` out of `Millisecond.Offset`. -/ @@ -142,14 +148,14 @@ Converts a `Duration` to a `Minute.Offset` -/ @[inline] def toMinutes (tm : Duration) : Minute.Offset := - tm.second.ediv 60 + tm.second.tdiv 60 /-- Converts a `Duration` to a `Day.Offset` -/ @[inline] def toDays (tm : Duration) : Day.Offset := - tm.second.ediv 86400 + tm.second.tdiv 86400 /-- Normalizes `Second.Offset` and `NanoSecond.span` in order to build a new `Duration` out of it. diff --git a/src/Std/Time/Internal/UnitVal.lean b/src/Std/Time/Internal/UnitVal.lean index 782b5c28d456..2013bbaf3b42 100644 --- a/src/Std/Time/Internal/UnitVal.lean +++ b/src/Std/Time/Internal/UnitVal.lean @@ -59,12 +59,21 @@ def mul (unit : UnitVal a) (factor : Int) : UnitVal (a / factor) := ⟨unit.val * factor⟩ /-- -Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio. +Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio. Using the +E-rounding convention (euclidean division) -/ @[inline] def ediv (unit : UnitVal a) (divisor : Int) : UnitVal (a * divisor) := ⟨unit.val.ediv divisor⟩ +/-- +Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio. Using the +"T-rounding" (Truncation-rounding) convention +-/ +@[inline] +def tdiv (unit : UnitVal a) (divisor : Int) : UnitVal (a * divisor) := + ⟨unit.val.tdiv divisor⟩ + /-- Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio. -/ diff --git a/tests/lean/run/timeAPI.lean b/tests/lean/run/timeAPI.lean index 8c99c1fc2624..0bdf95d92006 100644 --- a/tests/lean/run/timeAPI.lean +++ b/tests/lean/run/timeAPI.lean @@ -804,8 +804,8 @@ info: 1997-03-19T02:03:04.000000000[America/Sao_Paulo] 1997-03-23T02:03:04.000000000[America/Sao_Paulo] 1997-01-18T02:03:04.000000000[America/Sao_Paulo] 1997-01-18T02:03:04.000000000[America/Sao_Paulo] -0001-03-17T02:03:04.000000000[America/Sao_Paulo] -0001-03-17T02:03:04.000000000[America/Sao_Paulo] +0001-03-18T02:03:04.000000000[America/Sao_Paulo] +0001-03-18T02:03:04.000000000[America/Sao_Paulo] 97 1997 1997 1997 97 1997 1997 97 M false 77 diff --git a/tests/lean/run/timeNegative.lean b/tests/lean/run/timeNegative.lean new file mode 100644 index 000000000000..66e3bb88b07f --- /dev/null +++ b/tests/lean/run/timeNegative.lean @@ -0,0 +1,82 @@ +import Std.Time +import Init +open Std.Time + +/-- +info: Timestamp.ofNanosecondsSinceUnixEpoch -999999999 +-/ +#guard_msgs in +#eval datetime("1969-12-31T23:59:59.000000001").toTimestampAssumingUTC + +/-- +info: Timestamp.ofNanosecondsSinceUnixEpoch -1000000000 +-/ +#guard_msgs in +#eval datetime("1969-12-31T23:59:59.000000000").toTimestampAssumingUTC + +/-- +info: datetime("1969-12-31T23:59:59.000000001") +-/ +#guard_msgs in +#eval datetime("1969-12-31T23:59:59.000000001").toTimestampAssumingUTC.toPlainDateTimeAssumingUTC + +/-- +info: datetime("1969-12-31T23:59:59.000000000") +-/ +#guard_msgs in +#eval datetime("1969-12-31T23:59:59.000000000").toTimestampAssumingUTC.toPlainDateTimeAssumingUTC + +/-- +info: datetime("1969-12-31T23:59:59.000000001") +-/ +#guard_msgs in +#eval datetime("1969-12-31T23:59:59.000000000") + (1 : Nanosecond.Offset) + +/-- +info: datetime("1970-01-01T00:00:00.000000000") +-/ +#guard_msgs in +#eval datetime("1969-12-31T23:59:59.999999999") + (1 : Nanosecond.Offset) + +/-- +info: datetime("1970-01-01T00:00:01.000000000") +-/ +#guard_msgs in +#eval datetime("1970-01-01T00:00:00.999999999") + (1 : Nanosecond.Offset) + +/-- +info: Timestamp.ofNanosecondsSinceUnixEpoch -1 +-/ +#guard_msgs in +#eval datetime("1969-12-31T23:59:59.999999999").toTimestampAssumingUTC + +/-- +info: Timestamp.ofNanosecondsSinceUnixEpoch 0 +-/ +#guard_msgs in +#eval datetime("1969-12-31T23:59:59.999999999").toTimestampAssumingUTC + (1 : Nanosecond.Offset) + + +/-- +info: datetime("1970-01-01T00:00:00.000000000") +-/ +#guard_msgs in +#eval PlainDateTime.ofTimestampAssumingUTC 0 + +/-- +info: 121 +-/ +#guard_msgs in +#eval datetime("1804-04-30T23:59:59.999999999").dayOfYear + +/-- +info: 35 +-/ +#guard_msgs in +#eval datetime("1906-08-27T23:59:59.999999999").weekOfYear + +/-- +info: datetime("1906-08-27T23:59:59.999999999") +-/ +#guard_msgs in +#eval datetime("1906-08-27T23:59:59.999999999").toTimestampAssumingUTC.toPlainDateTimeAssumingUTC diff --git a/tests/lean/run/timeParse.lean b/tests/lean/run/timeParse.lean index fcd7b6be0b77..b7d630ad240b 100644 --- a/tests/lean/run/timeParse.lean +++ b/tests/lean/run/timeParse.lean @@ -84,7 +84,7 @@ info: "2024-08-16T01:28:00.000000000Z" ISO8601UTC.format t.toDateTime /-- -info: "0000-12-30T22:28:12.000000000+09:00" +info: "0000-12-31T22:28:12.000000000+09:00" -/ #guard_msgs in #eval @@ -92,11 +92,11 @@ info: "0000-12-30T22:28:12.000000000+09:00" ISO8601UTC.format (t.toDateTime.convertTimeZone jpTZ) /-- -info: "0000-12-29T21:28:12.000000000-03:00" +info: "0000-12-31T00:00:00.000000000-03:00" -/ #guard_msgs in #eval - let t1 : ZonedDateTime := Time12Hour.parse! "12:28:12 AM" + let t1 : ZonedDateTime := Time12Hour.parse! "03:00:00 AM" ISO8601UTC.format (t1.toDateTime.convertTimeZone brTZ) /--