fix: negative timestamps and PlainDateTimes before 1970 (#6668)

This PR fixes negative timestamps and `PlainDateTime`s before 1970.

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`.
 -/

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.

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.
 -/

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

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

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)
 
 /--