From 3e68695fd37396357b0f9a2395f30946960f0d5a Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Mon, 25 Nov 2024 23:57:47 -0300 Subject: [PATCH 01/17] fix: linux fallback directories and trim of the path of localdb in linux --- src/Std/Time/Zoned/Database/TZdb.lean | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/src/Std/Time/Zoned/Database/TZdb.lean b/src/Std/Time/Zoned/Database/TZdb.lean index 40fe0f7fd13e..179ed9c93fbc 100644 --- a/src/Std/Time/Zoned/Database/TZdb.lean +++ b/src/Std/Time/Zoned/Database/TZdb.lean @@ -27,10 +27,10 @@ structure TZdb where localPath : System.FilePath := "/etc/localtime" /-- - The path to the directory containing all available time zone files. These files define various + All the possible paths to the directories containing all available time zone files. These files define various time zones and their rules. -/ - zonesPath : System.FilePath := "/usr/share/zoneinfo/" + zonesPaths : Array System.FilePath := #["/usr/share/zoneinfo", "/share/zoneinfo", "/etc/zoneinfo", "/usr/share/lib/zoneinfo"] namespace TZdb open TimeZone @@ -64,8 +64,8 @@ def idFromPath (path : System.FilePath) : Option String := do let last₁ ← res.get? (res.size - 2) if last₁ = some "zoneinfo" - then last - else last₁ ++ "/" ++ last + then last.trim + else last₁.trim ++ "/" ++ last.trim /-- Retrieves the timezone rules from the local timezone data file. @@ -89,4 +89,11 @@ def readRulesFromDisk (path : System.FilePath) (id : String) : IO ZoneRules := d instance : Std.Time.Database TZdb where getLocalZoneRules db := localRules db.localPath - getZoneRules db id := readRulesFromDisk db.zonesPath id + + getZoneRules db id := do + for path in db.zonesPaths do + if ← System.FilePath.pathExists path then + let result ← readRulesFromDisk path id + return result + + throw <| IO.userError s!"cannot find {id} in the local timezone database" From 41784ab19b216de46962df071ffc89fd48838742 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Tue, 26 Nov 2024 09:44:23 -0300 Subject: [PATCH 02/17] feat: read TZDIR if it's in the environment --- src/Std/Time/Zoned/Database/TZdb.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Std/Time/Zoned/Database/TZdb.lean b/src/Std/Time/Zoned/Database/TZdb.lean index 179ed9c93fbc..617444cefdcf 100644 --- a/src/Std/Time/Zoned/Database/TZdb.lean +++ b/src/Std/Time/Zoned/Database/TZdb.lean @@ -91,6 +91,12 @@ instance : Std.Time.Database TZdb where getLocalZoneRules db := localRules db.localPath getZoneRules db id := do + let env ← IO.getEnv "TZDIR" + + if let some path := env then + let result ← readRulesFromDisk path id + return result + for path in db.zonesPaths do if ← System.FilePath.pathExists path then let result ← readRulesFromDisk path id From 7f758308fee301848df084dc0591666508e71d83 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Tue, 26 Nov 2024 10:30:00 -0300 Subject: [PATCH 03/17] fix: improve error message of parseTZIfFromDisk --- src/Std/Time/Zoned/Database/TZdb.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Time/Zoned/Database/TZdb.lean b/src/Std/Time/Zoned/Database/TZdb.lean index 617444cefdcf..5c0d49bafbad 100644 --- a/src/Std/Time/Zoned/Database/TZdb.lean +++ b/src/Std/Time/Zoned/Database/TZdb.lean @@ -52,7 +52,7 @@ def parseTZif (bin : ByteArray) (id : String) : Except String ZoneRules := do Reads a TZif file from disk and retrieves the zone rules for the specified timezone ID. -/ def parseTZIfFromDisk (path : System.FilePath) (id : String) : IO ZoneRules := do - let binary ← try IO.FS.readBinFile path catch _ => throw <| IO.userError s!"cannot find {id} in the local timezone database" + let binary ← try IO.FS.readBinFile path catch _ => throw <| IO.userError s!"unable to locate {id} in the local timezone database at '{path}'" IO.ofExcept (parseTZif binary id) /-- From 1e82e8a266d65b3f8f008d4e13e50a6889f255d7 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Tue, 17 Dec 2024 19:10:01 -0300 Subject: [PATCH 04/17] fix: timestamp repr --- src/Std/Time/DateTime/Timestamp.lean | 4 ++-- tests/lean/run/timeAPI.lean | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Std/Time/DateTime/Timestamp.lean b/src/Std/Time/DateTime/Timestamp.lean index 8ba43cc11892..ff503ce59819 100644 --- a/src/Std/Time/DateTime/Timestamp.lean +++ b/src/Std/Time/DateTime/Timestamp.lean @@ -38,10 +38,10 @@ instance : OfNat Timestamp n where ofNat := ⟨OfNat.ofNat n⟩ instance : ToString Timestamp where - toString s := toString s.val.toMilliseconds + toString s := toString s.val.toSeconds instance : Repr Timestamp where - reprPrec s := reprPrec (toString s) + reprPrec s := reprPrec s.val.toSeconds namespace Timestamp diff --git a/tests/lean/run/timeAPI.lean b/tests/lean/run/timeAPI.lean index 1509c573cf7d..8c99c1fc2624 100644 --- a/tests/lean/run/timeAPI.lean +++ b/tests/lean/run/timeAPI.lean @@ -587,7 +587,7 @@ Std.Time.Weekday.friday 2023-06-09 2023-06-09 19517 -1686268800000 +1686268800 1970-01-02 -/ @@ -667,7 +667,7 @@ Std.Time.Weekday.tuesday 12 3 9938 -858650584000 +858650584 1970-01-02T00:00:00.000000000 -/ @@ -741,7 +741,7 @@ Std.Time.Weekday.thursday 37 2 19978 -1726117262000 +1726117262 1970-01-02T00:00:00.000000000Z -/ @@ -816,7 +816,7 @@ Std.Time.Weekday.tuesday 12 3 9938 -858661384000 +858661384 -/ #guard_msgs in From 7d9cca48cbdc5b6677fe4e3edf5174f9451f5b95 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Wed, 18 Dec 2024 14:56:19 -0300 Subject: [PATCH 05/17] fix: now PlainTime takes leap seconds as argument --- src/Std/Time/DateTime.lean | 12 +-- src/Std/Time/DateTime/PlainDateTime.lean | 91 ++++++++++-------- src/Std/Time/Duration.lean | 4 +- src/Std/Time/Format.lean | 52 +++++----- src/Std/Time/Format/Basic.lean | 16 ++-- src/Std/Time/Notation.lean | 8 +- src/Std/Time/Time/PlainTime.lean | 116 +++++++++++++---------- src/Std/Time/Zoned.lean | 15 +-- src/Std/Time/Zoned/DateTime.lean | 14 +-- src/Std/Time/Zoned/ZonedDateTime.lean | 18 ++-- tests/lean/run/timeAPI.lean | 12 +-- tests/lean/run/timeClassOperations.lean | 2 +- tests/lean/run/timeFormats.lean | 18 ++-- tests/lean/run/timeLocalDateTime.lean | 3 +- tests/lean/run/timeOperations.lean | 2 +- tests/lean/run/timeParse.lean | 4 +- tests/lean/run/timeSet.lean | 4 +- 17 files changed, 206 insertions(+), 185 deletions(-) diff --git a/src/Std/Time/DateTime.lean b/src/Std/Time/DateTime.lean index ec83e83f0790..50b278327107 100644 --- a/src/Std/Time/DateTime.lean +++ b/src/Std/Time/DateTime.lean @@ -50,7 +50,7 @@ def toPlainDateAssumingUTC (timestamp : Timestamp) : PlainDate := Converts a `Timestamp` to a `PlainTime` -/ @[inline] -def getTimeAssumingUTC (timestamp : Timestamp) : PlainTime := +def getTimeAssumingUTC (timestamp : Timestamp) : PlainTime α := let nanos := timestamp.toNanosecondsSinceUnixEpoch PlainTime.ofNanoseconds nanos @@ -75,7 +75,7 @@ Converts a `PlainDate` to a `Timestamp` -/ @[inline] def ofPlainDate (date : PlainDate) : PlainDateTime := - { date, time := PlainTime.midnight } + { date, time := Sigma.mk true (PlainTime.midnight) } /-- Converts a `PlainDateTime` to a `PlainDate` @@ -88,15 +88,15 @@ def toPlainDate (pdt : PlainDateTime) : PlainDate := Converts a `PlainTime` to a `PlainDateTime` -/ @[inline] -def ofPlainTime (time : PlainTime) : PlainDateTime := - { date := ⟨1, 1, 1, by decide⟩, time } +def ofPlainTime (time : PlainTime α) : PlainDateTime := + { date := ⟨1, 1, 1, by decide⟩, time := Sigma.mk α time } /-- Converts a `PlainDateTime` to a `PlainTime` -/ @[inline] -def toPlainTime (pdt : PlainDateTime) : PlainTime := - pdt.time +def toPlainTime (pdt : PlainDateTime) : PlainTime pdt.time.fst := + pdt.time.snd instance : HSub PlainDateTime PlainDateTime Duration where hSub x y := x.toTimestampAssumingUTC - y.toTimestampAssumingUTC diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index 7949c9930b5b..0629bf993c6c 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -28,9 +28,16 @@ structure PlainDateTime where /-- The `Time` component of a `PlainTime` -/ - time : PlainTime + time : Sigma PlainTime + + deriving Repr + +instance : Inhabited PlainDateTime where + default := { + date := Inhabited.default, + time := Sigma.mk true Inhabited.default + } - deriving Inhabited, BEq, Repr namespace PlainDateTime @@ -39,8 +46,8 @@ Converts a `PlainDateTime` to a `Timestamp` -/ def toTimestampAssumingUTC (dt : PlainDateTime) : Timestamp := let days := dt.date.toDaysSinceUNIXEpoch - let nanos := days.toSeconds + dt.time.toSeconds |>.mul 1000000000 - let nanos := nanos.val + dt.time.nanosecond.val + let nanos := days.toSeconds + dt.time.snd.toSeconds |>.mul 1000000000 + let nanos := nanos.val + dt.time.snd.nanosecond.val Timestamp.ofNanosecondsSinceUnixEpoch (Nanosecond.Offset.ofInt nanos) /-- @@ -123,7 +130,7 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do return { date := PlainDate.ofYearMonthDayClip year hmon (Day.Ordinal.ofFin (Fin.succ mday)) - time := PlainTime.ofHourMinuteSecondsNano (leap := false) (hour.expandTop (by decide)) minute second nano + time := Sigma.mk false (PlainTime.ofHourMinuteSecondsNano (hour.expandTop (by decide)) minute second nano) } /-- @@ -137,8 +144,8 @@ def toDaysSinceUNIXEpoch (pdt : PlainDateTime) : Day.Offset := Converts a `PlainDateTime` to the number of days since the UNIX epoch. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) : PlainDateTime := - PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) time +def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime α) : PlainDateTime := + PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) (Sigma.mk α time) /-- Sets the `PlainDateTime` to the specified `desiredWeekday`. @@ -199,35 +206,35 @@ Creates a new `PlainDateTime` by adjusting the `hour` component of its `time` to -/ @[inline] def withHours (dt : PlainDateTime) (hour : Hour.Ordinal) : PlainDateTime := - { dt with time := { dt.time with hour := hour } } + { dt with time := Sigma.mk dt.time.fst { dt.time.snd with hour := hour } } /-- Creates a new `PlainDateTime` by adjusting the `minute` component of its `time` to the given value. -/ @[inline] def withMinutes (dt : PlainDateTime) (minute : Minute.Ordinal) : PlainDateTime := - { dt with time := { dt.time with minute := minute } } + { dt with time := Sigma.mk dt.time.fst { dt.time.snd with minute := minute } } /-- Creates a new `PlainDateTime` by adjusting the `second` component of its `time` to the given value. -/ @[inline] -def withSeconds (dt : PlainDateTime) (second : Sigma Second.Ordinal) : PlainDateTime := - { dt with time := { dt.time with second := second } } +def withSeconds (dt : PlainDateTime) (second : Second.Ordinal α) : PlainDateTime := + { dt with time := Sigma.mk α { dt.time.snd with second := second } } /-- Creates a new `PlainDateTime` by adjusting the milliseconds component inside the `nano` component of its `time` to the given value. -/ @[inline] def withMilliseconds (dt : PlainDateTime) (millis : Millisecond.Ordinal) : PlainDateTime := - { dt with time := dt.time.withMilliseconds millis } + { dt with time := Sigma.mk dt.time.fst (dt.time.snd.withMilliseconds millis) } /-- Creates a new `PlainDateTime` by adjusting the `nano` component of its `time` to the given value. -/ @[inline] def withNanoseconds (dt : PlainDateTime) (nano : Nanosecond.Ordinal) : PlainDateTime := - { dt with time := dt.time.withNanoseconds nano } + { dt with time := Sigma.mk dt.time.fst (dt.time.snd.withNanoseconds nano) } /-- Adds a `Day.Offset` to a `PlainDateTime`. @@ -322,10 +329,10 @@ Adds an `Hour.Offset` to a `PlainDateTime`, adjusting the date if the hour overf -/ @[inline] def addHours (dt : PlainDateTime) (hours : Hour.Offset) : PlainDateTime := - let totalSeconds := dt.time.toSeconds + hours.toSeconds + let totalSeconds := dt.time.snd.toSeconds + hours.toSeconds let days := totalSeconds.ediv 86400 - let newTime := dt.time.addSeconds (hours.toSeconds) - { dt with date := dt.date.addDays days, time := newTime } + let newTime := dt.time.snd.addSeconds (hours.toSeconds) + { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime } /-- Subtracts an `Hour.Offset` from a `PlainDateTime`, adjusting the date if the hour underflows. @@ -339,10 +346,10 @@ 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 totalSeconds := dt.time.snd.toSeconds + minutes.toSeconds let days := totalSeconds.ediv 86400 - let newTime := dt.time.addSeconds (minutes.toSeconds) - { dt with date := dt.date.addDays days, time := newTime } + let newTime := dt.time.snd.addSeconds (minutes.toSeconds) + { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime } /-- Subtracts a `Minute.Offset` from a `PlainDateTime`, adjusting the hour and date if the minutes underflow. @@ -356,10 +363,10 @@ 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 totalSeconds := dt.time.snd.toSeconds + seconds let days := totalSeconds.ediv 86400 - let newTime := dt.time.addSeconds seconds - { dt with date := dt.date.addDays days, time := newTime } + let newTime := dt.time.snd.addSeconds seconds + { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime } /-- Subtracts a `Second.Offset` from a `PlainDateTime`, adjusting the minute, hour, and date if the seconds underflow. @@ -373,10 +380,10 @@ 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 totalMilliseconds := dt.time.snd.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 } + let newTime := dt.time.snd.addMilliseconds milliseconds + { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime } /-- Subtracts a `Millisecond.Offset` from a `PlainDateTime`, adjusting the second, minute, hour, and date if the milliseconds underflow. @@ -390,12 +397,12 @@ Adds a `Nanosecond.Offset` to a `PlainDateTime`, adjusting the seconds, minutes, -/ @[inline] def addNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime := - let nano := Nanosecond.Offset.ofInt dt.time.nanosecond.val + let nano := Nanosecond.Offset.ofInt dt.time.snd.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 } } + let newTime := dt.time.snd.addSeconds extraSeconds + { dt with time := Sigma.mk dt.time.fst { newTime with nanosecond } } /-- Subtracts a `Nanosecond.Offset` from a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds underflow. @@ -437,35 +444,35 @@ Getter for the `Hour` inside of a `PlainDateTime`. -/ @[inline] def hour (dt : PlainDateTime) : Hour.Ordinal := - dt.time.hour + dt.time.snd.hour /-- Getter for the `Minute` inside of a `PlainDateTime`. -/ @[inline] def minute (dt : PlainDateTime) : Minute.Ordinal := - dt.time.minute + dt.time.snd.minute /-- Getter for the `Millisecond` inside of a `PlainDateTime`. -/ @[inline] def millisecond (dt : PlainDateTime) : Millisecond.Ordinal := - dt.time.millisecond + dt.time.snd.millisecond /-- Getter for the `Second` inside of a `PlainDateTime`. -/ @[inline] -def second (dt : PlainDateTime) : Second.Ordinal dt.time.second.fst := - dt.time.second.snd +def second (dt : PlainDateTime) : Second.Ordinal dt.time.fst := + dt.time.snd.second /-- Getter for the `Nanosecond.Ordinal` inside of a `PlainDateTime`. -/ @[inline] def nanosecond (dt : PlainDateTime) : Nanosecond.Ordinal := - dt.time.nanosecond + dt.time.snd.nanosecond /-- Determines the era of the given `PlainDateTime` based on its year. @@ -521,15 +528,15 @@ def quarter (date : PlainDateTime) : Bounded.LE 1 4 := Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`. -/ @[inline] -def atTime : PlainDate → PlainTime → PlainDateTime := - PlainDateTime.mk +def atTime : PlainDate → PlainTime α → PlainDateTime := + (PlainDateTime.mk · <| Sigma.mk α ·) /-- Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`. -/ @[inline] -def atDate (time: PlainTime) (date: PlainDate) : PlainDateTime := - PlainDateTime.mk date time +def atDate (time: PlainTime α) (date: PlainDate) : PlainDateTime := + PlainDateTime.mk date (Sigma.mk α time) instance : HAdd PlainDateTime Day.Offset PlainDateTime where hAdd := addDays @@ -583,8 +590,8 @@ namespace PlainDate Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`. -/ @[inline] -def atTime : PlainDate → PlainTime → PlainDateTime := - PlainDateTime.mk +def atTime : PlainDate → PlainTime α → PlainDateTime := + (PlainDateTime.mk · <| Sigma.mk α ·) end PlainDate namespace PlainTime @@ -593,8 +600,8 @@ namespace PlainTime Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`. -/ @[inline] -def atDate (time: PlainTime) (date: PlainDate) : PlainDateTime := - PlainDateTime.mk date time +def atDate (time: PlainTime α) (date: PlainDate) : PlainDateTime := + PlainDateTime.mk date (Sigma.mk α time) end PlainTime end Time diff --git a/src/Std/Time/Duration.lean b/src/Std/Time/Duration.lean index 54d6d0364340..de32e8138f68 100644 --- a/src/Std/Time/Duration.lean +++ b/src/Std/Time/Duration.lean @@ -350,10 +350,10 @@ instance : HMul Int Duration Duration where instance : HMul Duration Int Duration where hMul d i := Duration.ofNanoseconds <| Nanosecond.Offset.ofInt (d.toNanoseconds.val * i) -instance : HAdd PlainTime Duration PlainTime where +instance : HAdd (PlainTime α) Duration (PlainTime α) where hAdd pt d := PlainTime.ofNanoseconds (d.toNanoseconds + pt.toNanoseconds) -instance : HSub PlainTime Duration PlainTime where +instance : HSub (PlainTime α) Duration (PlainTime α) where hSub pt d := PlainTime.ofNanoseconds (d.toNanoseconds - pt.toNanoseconds) end Duration diff --git a/src/Std/Time/Format.lean b/src/Std/Time/Format.lean index 6d4b31c3af37..2987321a931f 100644 --- a/src/Std/Time/Format.lean +++ b/src/Std/Time/Format.lean @@ -254,7 +254,7 @@ namespace PlainTime /-- Formats a `PlainTime` using a specific format. -/ -def format (time : PlainTime) (format : String) : String := +def format (time : PlainTime α) (format : String) : String := let format : Except String (GenericFormat .any) := GenericFormat.spec format match format with | .error err => s!"error: {err}" @@ -264,7 +264,7 @@ def format (time : PlainTime) (format : String) : String := | .k _ => some (time.hour.shiftTo1BasedHour) | .m _ => some time.minute | .n _ => some time.nanosecond - | .s _ => some time.second + | .s _ => some (Sigma.mk α time.second) | .a _ => some (HourMarker.ofOrdinal time.hour) | .h _ => some time.hour.toRelative | .K _ => some (time.hour.emod 12 (by decide)) @@ -279,55 +279,55 @@ def format (time : PlainTime) (format : String) : String := /-- Parses a time string in the 24-hour format (`HH:mm:ss`) and returns a `PlainTime`. -/ -def fromTime24Hour (input : String) : Except String PlainTime := - Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s.snd)) input +def fromTime24Hour (input : String) : Except String (Sigma PlainTime) := + Formats.time24Hour.parseBuilder (fun h m s => some (Sigma.mk s.fst (PlainTime.ofHourMinuteSeconds h m s.snd))) input /-- Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss`). -/ -def toTime24Hour (input : PlainTime) : String := - Formats.time24Hour.formatBuilder input.hour input.minute input.second +def toTime24Hour (input : PlainTime α) : String := + Formats.time24Hour.formatBuilder input.hour input.minute (Sigma.mk α input.second) /-- Parses a time string in the lean 24-hour format (`HH:mm:ss.SSSSSSSSS` or `HH:mm:ss`) and returns a `PlainTime`. -/ -def fromLeanTime24Hour (input : String) : Except String PlainTime := - Formats.leanTime24Hour.parseBuilder (fun h m s n => some (PlainTime.ofHourMinuteSecondsNano h m s.snd n)) input - <|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSecondsNano h m s.snd 0)) input +def fromLeanTime24Hour (input : String) : Except String (Sigma PlainTime) := + Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| Sigma.mk s.fst (PlainTime.ofHourMinuteSecondsNano h m s.snd n)) input + <|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some <| Sigma.mk s.fst (PlainTime.ofHourMinuteSecondsNano h m s.snd 0)) input /-- Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss.SSSSSSSSS`). -/ -def toLeanTime24Hour (input : PlainTime) : String := - Formats.leanTime24Hour.formatBuilder input.hour input.minute input.second input.nanosecond +def toLeanTime24Hour (input : PlainTime α) : String := + Formats.leanTime24Hour.formatBuilder input.hour input.minute (Sigma.mk α input.second) input.nanosecond /-- Parses a time string in the 12-hour format (`hh:mm:ss aa`) and returns a `PlainTime`. -/ -def fromTime12Hour (input : String) : Except String PlainTime := do - let builder h m s a : Option PlainTime := do +def fromTime12Hour (input : String) : Except String (Sigma PlainTime) := do + let builder h m s a : Option (Sigma PlainTime) := do let value ← Internal.Bounded.ofInt? h.val - some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s.snd + some <| Sigma.mk s.fst <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s.snd Formats.time12Hour.parseBuilder builder input /-- Formats a `PlainTime` value into a 12-hour format string (`hh:mm:ss aa`). -/ -def toTime12Hour (input : PlainTime) : String := - Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute input.second (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am) +def toTime12Hour (input : PlainTime α) : String := + Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute (Sigma.mk α input.second) (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am) /-- Parses a `String` in the `Time12Hour` or `Time24Hour` format and returns a `PlainTime`. -/ -def parse (input : String) : Except String PlainTime := +def parse (input : String) : Except String (Sigma PlainTime) := fromTime12Hour input <|> fromTime24Hour input -instance : ToString PlainTime where +instance : ToString (PlainTime α) where toString := toLeanTime24Hour -instance : Repr PlainTime where +instance : Repr (PlainTime α) where reprPrec data := Repr.addAppParen ("time(\"" ++ toLeanTime24Hour data ++ "\")") end PlainTime @@ -409,12 +409,12 @@ def fromLeanDateTimeWithIdentifierString (input : String) : Except String ZonedD Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation. -/ def toLeanDateTimeWithZoneString (zdt : ZonedDateTime) : String := - Formats.leanDateTimeWithZone.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.offset + Formats.leanDateTimeWithZone.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute (Sigma.mk zdt.date.get.time.fst zdt.date.get.time.snd.second) zdt.nanosecond zdt.offset /-- Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation with the timezone identifier. -/ def toLeanDateTimeWithIdentifierString (zdt : ZonedDateTime) : String := - Formats.leanDateTimeWithIdentifierAndNanos.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.timezone.name + Formats.leanDateTimeWithIdentifierAndNanos.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute (Sigma.mk zdt.date.get.time.fst zdt.date.get.time.snd.second) zdt.nanosecond zdt.timezone.name /-- Parses a `String` in the `ISO8601`, `RFC822` or `RFC850` format and returns a `ZonedDateTime`. @@ -461,13 +461,13 @@ def format (date : PlainDateTime) (format : String) : String := | .k _ => some date.hour.shiftTo1BasedHour | .m _ => some date.minute | .n _ => some date.nanosecond - | .s _ => some date.time.second + | .s _ => some (Sigma.mk date.time.fst date.time.snd.second) | .a _ => some (HourMarker.ofOrdinal date.hour) | .h _ => some date.hour.toRelative | .K _ => some (date.hour.emod 12 (by decide)) | .S _ => some date.nanosecond - | .A _ => some date.time.toMilliseconds - | .N _ => some date.time.toNanoseconds + | .A _ => some date.time.snd.toMilliseconds + | .N _ => some date.time.snd.toNanoseconds | _ => none match res with | some res => res @@ -510,7 +510,7 @@ def fromDateTimeString (input : String) : Except String PlainDateTime := Formats a `PlainDateTime` value into a `DateTime` format string. -/ def toDateTimeString (pdt : PlainDateTime) : String := - Formats.dateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond + Formats.dateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute (Sigma.mk pdt.time.fst pdt.time.snd.second) pdt.nanosecond /-- Parses a `String` in the `DateTime` format and returns a `PlainDateTime`. @@ -523,7 +523,7 @@ def fromLeanDateTimeString (input : String) : Except String PlainDateTime := Formats a `PlainDateTime` value into a `DateTime` format string. -/ def toLeanDateTimeString (pdt : PlainDateTime) : String := - Formats.leanDateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond + Formats.leanDateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute (Sigma.mk pdt.time.fst pdt.time.snd.second) pdt.nanosecond /-- Parses a `String` in the `AscTime` or `LongDate` format and returns a `PlainDateTime`. diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean index 0ecde2581c55..5b9c390b5d98 100644 --- a/src/Std/Time/Format/Basic.lean +++ b/src/Std/Time/Format/Basic.lean @@ -736,12 +736,12 @@ private def toSigned (data : Int) : String := private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bool) (colon : Bool) : String := let (sign, time) := if offset.second.val ≥ 0 then ("+", offset.second) else ("-", -offset.second) - let time := PlainTime.ofSeconds time + let time : PlainTime true := PlainTime.ofSeconds time let pad := leftPad 2 '0' ∘ toString let data := s!"{sign}{pad time.hour.val}" let data := if withMinutes then s!"{data}{if colon then ":" else ""}{pad time.minute.val}" else data - let data := if withSeconds ∧ time.second.snd.val ≠ 0 then s!"{data}{if colon then ":" else ""}{pad time.second.snd.val}" else data + let data := if withSeconds ∧ time.second.val ≠ 0 then s!"{data}{if colon then ":" else ""}{pad time.second.val}" else data data @@ -913,11 +913,11 @@ private def dateFromModifier (date : DateTime tz) : TypeFormat modifier := | .k _ => date.hour.shiftTo1BasedHour | .H _ => date.hour | .m _ => date.minute - | .s _ => date.date.get.time.second + | .s _ => Sigma.mk date.date.get.time.fst date.date.get.time.snd.second | .S _ => date.nanosecond - | .A _ => date.date.get.time.toMilliseconds + | .A _ => date.date.get.time.snd.toMilliseconds | .n _ => date.nanosecond - | .N _ => date.date.get.time.toNanoseconds + | .N _ => date.date.get.time.snd.toNanoseconds | .V => tz.name | .z .short => tz.abbreviation | .z .full => tz.name @@ -1338,15 +1338,15 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type := let second := builder.s |>.getD ⟨false, 0⟩ let nano := (builder.n <|> builder.S) |>.getD 0 - let time : PlainTime + let time : PlainTime second.fst := PlainTime.ofNanoseconds <$> builder.N <|> PlainTime.ofMilliseconds <$> builder.A - |>.getD (PlainTime.mk hour minute second nano) + |>.getD (PlainTime.mk hour minute second.snd nano) let datetime : Option PlainDateTime := if valid : year.Valid month day then let date : PlainDate := { year, month, day, valid } - some { date, time } + some { date, time := Sigma.mk second.fst time } else none diff --git a/src/Std/Time/Notation.lean b/src/Std/Time/Notation.lean index b8b5e35bcfdb..7bc34a2e2984 100644 --- a/src/Std/Time/Notation.lean +++ b/src/Std/Time/Notation.lean @@ -125,11 +125,11 @@ private def convertTimezone (tz : Std.Time.TimeZone) : MacroM (TSyntax `term) := private def convertPlainDate (d : Std.Time.PlainDate) : MacroM (TSyntax `term) := do `(Std.Time.PlainDate.ofYearMonthDayClip $(← syntaxInt d.year) $(← syntaxBounded d.month.val) $(← syntaxBounded d.day.val)) -private def convertPlainTime (d : Std.Time.PlainTime) : MacroM (TSyntax `term) := do - `(Std.Time.PlainTime.mk $(← syntaxBounded d.hour.val) $(← syntaxBounded d.minute.val) ⟨true, $(← syntaxBounded d.second.snd.val)⟩ $(← syntaxBounded d.nanosecond.val)) +private def convertPlainTime (d : Std.Time.PlainTime α) : MacroM (TSyntax `term) := do + `(Std.Time.PlainTime.mk $(← syntaxBounded d.hour.val) $(← syntaxBounded d.minute.val) $(← syntaxBounded d.second.val) $(← syntaxBounded d.nanosecond.val)) private def convertPlainDateTime (d : Std.Time.PlainDateTime) : MacroM (TSyntax `term) := do - `(Std.Time.PlainDateTime.mk $(← convertPlainDate d.date) $(← convertPlainTime d.time)) + `(Std.Time.PlainDateTime.mk $(← convertPlainDate d.date) (Sigma.mk true $(← convertPlainTime (d.time.snd)))) private def convertZonedDateTime (d : Std.Time.ZonedDateTime) (identifier := false) : MacroM (TSyntax `term) := do let plain ← convertPlainDateTime d.toPlainDateTime @@ -232,7 +232,7 @@ macro_rules | `(time( $time:str )) => do match PlainTime.fromLeanTime24Hour time.getString with - | .ok res => return ← convertPlainTime res + | .ok res => return ← convertPlainTime res.snd | .error res => Macro.throwErrorAt time s!"error: {res}" | `(offset( $offset:str )) => do diff --git a/src/Std/Time/Time/PlainTime.lean b/src/Std/Time/Time/PlainTime.lean index 3c0b2d3e0061..67af9129c12e 100644 --- a/src/Std/Time/Time/PlainTime.lean +++ b/src/Std/Time/Time/PlainTime.lean @@ -15,7 +15,7 @@ set_option linter.all true /-- Represents a specific point in a day, including hours, minutes, seconds, and nanoseconds. -/ -structure PlainTime where +structure PlainTime (leap : Bool) where /-- `Hour` component of the `PlainTime` @@ -30,7 +30,7 @@ structure PlainTime where /-- `Second` component of the `PlainTime` -/ - second : Sigma Second.Ordinal + second : Second.Ordinal leap /-- `Nanoseconds` component of the `PlainTime` @@ -38,120 +38,132 @@ structure PlainTime where nanosecond : Nanosecond.Ordinal deriving Repr -instance : Inhabited PlainTime where - default := ⟨0, 0, Sigma.mk false 0, 0, by decide⟩ +/-- +COMMENT +-/ +def LeapTime := PlainTime True + +instance : Inhabited (PlainTime x) where + default := ⟨0, 0, 0, 0, by decide⟩ -instance : BEq PlainTime where +instance : BEq (PlainTime x) where beq x y := x.hour.val == y.hour.val && x.minute == y.minute - && x.second.snd.val == y.second.snd.val && x.nanosecond == y.nanosecond + && x.second.val == y.second.val && x.nanosecond == y.nanosecond namespace PlainTime /-- Creates a `PlainTime` value representing midnight (00:00:00.000000000). -/ -def midnight : PlainTime := - ⟨0, 0, ⟨true, 0⟩, 0⟩ +def midnight : PlainTime α := + ⟨0, 0, 0, 0⟩ /-- Creates a `PlainTime` value from the provided hours, minutes, seconds and nanoseconds components. -/ @[inline] -def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) (nano : Nanosecond.Ordinal) : PlainTime := - ⟨hour, minute, Sigma.mk leap second, nano⟩ +def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal α) (nano : Nanosecond.Ordinal) : PlainTime α := + ⟨hour, minute, second, nano⟩ /-- Creates a `PlainTime` value from the provided hours, minutes, and seconds. -/ @[inline] -def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) : PlainTime := +def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal α) : PlainTime α := ofHourMinuteSecondsNano hour minute second 0 /-- Converts a `PlainTime` value to the total number of milliseconds. -/ -def toMilliseconds (time : PlainTime) : Millisecond.Offset := +def toMilliseconds (time : PlainTime α) : Millisecond.Offset := time.hour.toOffset.toMilliseconds + time.minute.toOffset.toMilliseconds + - time.second.snd.toOffset.toMilliseconds + + time.second.toOffset.toMilliseconds + time.nanosecond.toOffset.toMilliseconds /-- Converts a `PlainTime` value to the total number of nanoseconds. -/ -def toNanoseconds (time : PlainTime) : Nanosecond.Offset := +def toNanoseconds (time : PlainTime α) : Nanosecond.Offset := time.hour.toOffset.toNanoseconds + time.minute.toOffset.toNanoseconds + - time.second.snd.toOffset.toNanoseconds + + time.second.toOffset.toNanoseconds + time.nanosecond.toOffset /-- Converts a `PlainTime` value to the total number of seconds. -/ -def toSeconds (time : PlainTime) : Second.Offset := +def toSeconds (time : PlainTime α) : Second.Offset := time.hour.toOffset.toSeconds + time.minute.toOffset.toSeconds + - time.second.snd.toOffset + time.second.toOffset /-- Converts a `PlainTime` value to the total number of minutes. -/ -def toMinutes (time : PlainTime) : Minute.Offset := +def toMinutes (time : PlainTime α) : Minute.Offset := time.hour.toOffset.toMinutes + time.minute.toOffset + - time.second.snd.toOffset.toMinutes + time.second.toOffset.toMinutes /-- Converts a `PlainTime` value to the total number of hours. -/ -def toHours (time : PlainTime) : Hour.Offset := +def toHours (time : PlainTime α) : Hour.Offset := time.hour.toOffset /-- Creates a `PlainTime` value from a total number of nanoseconds. -/ -def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime := +def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime α := have totalSeconds := nanos.ediv 1000000000 have remainingNanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide) have hours := Bounded.LE.byEmod (totalSeconds.val / 3600) 24 (by decide) have minutes := (Bounded.LE.byEmod totalSeconds.val 3600 (by decide)).ediv 60 (by decide) + have seconds := Bounded.LE.byEmod totalSeconds.val 60 (by decide) + + have seconds := + match α with + | true => seconds.expandTop (by decide) + | false => seconds + let nanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide) - PlainTime.mk hours minutes (Sigma.mk false seconds) nanos + PlainTime.mk hours minutes seconds nanos /-- Creates a `PlainTime` value from a total number of millisecond. -/ @[inline] -def ofMilliseconds (millis : Millisecond.Offset) : PlainTime := +def ofMilliseconds (millis : Millisecond.Offset) : PlainTime α := ofNanoseconds millis.toNanoseconds /-- Creates a `PlainTime` value from a total number of seconds. -/ @[inline] -def ofSeconds (secs : Second.Offset) : PlainTime := +def ofSeconds (secs : Second.Offset) : PlainTime α := ofNanoseconds secs.toNanoseconds /-- Creates a `PlainTime` value from a total number of minutes. -/ @[inline] -def ofMinutes (secs : Minute.Offset) : PlainTime := +def ofMinutes (secs : Minute.Offset) : PlainTime α := ofNanoseconds secs.toNanoseconds /-- Creates a `PlainTime` value from a total number of hours. -/ @[inline] -def ofHours (hour : Hour.Offset) : PlainTime := +def ofHours (hour : Hour.Offset) : PlainTime α := ofNanoseconds hour.toNanoseconds /-- Adds seconds to a `PlainTime`. -/ @[inline] -def addSeconds (time : PlainTime) (secondsToAdd : Second.Offset) : PlainTime := +def addSeconds (time : PlainTime α) (secondsToAdd : Second.Offset) : PlainTime α := let totalSeconds := time.toNanoseconds + secondsToAdd.toNanoseconds ofNanoseconds totalSeconds @@ -159,14 +171,14 @@ def addSeconds (time : PlainTime) (secondsToAdd : Second.Offset) : PlainTime := Subtracts seconds from a `PlainTime`. -/ @[inline] -def subSeconds (time : PlainTime) (secondsToSub : Second.Offset) : PlainTime := +def subSeconds (time : PlainTime α) (secondsToSub : Second.Offset) : PlainTime α := addSeconds time (-secondsToSub) /-- Adds minutes to a `PlainTime`. -/ @[inline] -def addMinutes (time : PlainTime) (minutesToAdd : Minute.Offset) : PlainTime := +def addMinutes (time : PlainTime α) (minutesToAdd : Minute.Offset) : PlainTime α := let total := time.toNanoseconds + minutesToAdd.toNanoseconds ofNanoseconds total @@ -174,14 +186,14 @@ def addMinutes (time : PlainTime) (minutesToAdd : Minute.Offset) : PlainTime := Subtracts minutes from a `PlainTime`. -/ @[inline] -def subMinutes (time : PlainTime) (minutesToSub : Minute.Offset) : PlainTime := +def subMinutes (time : PlainTime α) (minutesToSub : Minute.Offset) : PlainTime α := addMinutes time (-minutesToSub) /-- Adds hours to a `PlainTime`. -/ @[inline] -def addHours (time : PlainTime) (hoursToAdd : Hour.Offset) : PlainTime := +def addHours (time : PlainTime α) (hoursToAdd : Hour.Offset) : PlainTime α := let total := time.toNanoseconds + hoursToAdd.toNanoseconds ofNanoseconds total @@ -189,54 +201,54 @@ def addHours (time : PlainTime) (hoursToAdd : Hour.Offset) : PlainTime := Subtracts hours from a `PlainTime`. -/ @[inline] -def subHours (time : PlainTime) (hoursToSub : Hour.Offset) : PlainTime := +def subHours (time : PlainTime α) (hoursToSub : Hour.Offset) : PlainTime α := addHours time (-hoursToSub) /-- Adds nanoseconds to a `PlainTime`. -/ -def addNanoseconds (time : PlainTime) (nanosToAdd : Nanosecond.Offset) : PlainTime := +def addNanoseconds (time : PlainTime α) (nanosToAdd : Nanosecond.Offset) : PlainTime α := let total := time.toNanoseconds + nanosToAdd ofNanoseconds total /-- Subtracts nanoseconds from a `PlainTime`. -/ -def subNanoseconds (time : PlainTime) (nanosToSub : Nanosecond.Offset) : PlainTime := +def subNanoseconds (time : PlainTime α) (nanosToSub : Nanosecond.Offset) : PlainTime α := addNanoseconds time (-nanosToSub) /-- Adds milliseconds to a `PlainTime`. -/ -def addMilliseconds (time : PlainTime) (millisToAdd : Millisecond.Offset) : PlainTime := +def addMilliseconds (time : PlainTime α) (millisToAdd : Millisecond.Offset) : PlainTime α := let total := time.toMilliseconds + millisToAdd ofMilliseconds total /-- Subtracts milliseconds from a `PlainTime`. -/ -def subMilliseconds (time : PlainTime) (millisToSub : Millisecond.Offset) : PlainTime := +def subMilliseconds (time : PlainTime α) (millisToSub : Millisecond.Offset) : PlainTime α := addMilliseconds time (-millisToSub) /-- Creates a new `PlainTime` by adjusting the `second` component to the given value. -/ @[inline] -def withSeconds (pt : PlainTime) (second : Sigma Second.Ordinal) : PlainTime := +def withSeconds (pt : PlainTime α) (second : Second.Ordinal α) : PlainTime α := { pt with second := second } /-- Creates a new `PlainTime` by adjusting the `minute` component to the given value. -/ @[inline] -def withMinutes (pt : PlainTime) (minute : Minute.Ordinal) : PlainTime := +def withMinutes (pt : PlainTime α) (minute : Minute.Ordinal) : PlainTime α := { pt with minute := minute } /-- Creates a new `PlainTime` by adjusting the milliseconds component inside the `nano` component of its `time` to the given value. -/ @[inline] -def withMilliseconds (pt : PlainTime) (millis : Millisecond.Ordinal) : PlainTime := +def withMilliseconds (pt : PlainTime α) (millis : Millisecond.Ordinal) : PlainTime α := let minorPart := pt.nanosecond.emod 1000 (by decide) let majorPart := millis.mul_pos 1000000 (by decide) |>.addBounds minorPart { pt with nanosecond := majorPart |>.expandTop (by decide) } @@ -245,51 +257,51 @@ def withMilliseconds (pt : PlainTime) (millis : Millisecond.Ordinal) : PlainTime Creates a new `PlainTime` by adjusting the `nano` component to the given value. -/ @[inline] -def withNanoseconds (pt : PlainTime) (nano : Nanosecond.Ordinal) : PlainTime := +def withNanoseconds (pt : PlainTime α) (nano : Nanosecond.Ordinal) : PlainTime α := { pt with nanosecond := nano } /-- Creates a new `PlainTime` by adjusting the `hour` component to the given value. -/ @[inline] -def withHours (pt : PlainTime) (hour : Hour.Ordinal) : PlainTime := +def withHours (pt : PlainTime α) (hour : Hour.Ordinal) : PlainTime α := { pt with hour := hour } /-- `Millisecond` component of the `PlainTime` -/ @[inline] -def millisecond (pt : PlainTime) : Millisecond.Ordinal := +def millisecond (pt : PlainTime α) : Millisecond.Ordinal := pt.nanosecond.ediv 1000000 (by decide) -instance : HAdd PlainTime Nanosecond.Offset PlainTime where +instance : HAdd (PlainTime α) Nanosecond.Offset (PlainTime α) where hAdd := addNanoseconds -instance : HSub PlainTime Nanosecond.Offset PlainTime where +instance : HSub (PlainTime α) Nanosecond.Offset (PlainTime α) where hSub := subNanoseconds -instance : HAdd PlainTime Millisecond.Offset PlainTime where +instance : HAdd (PlainTime α) Millisecond.Offset (PlainTime α) where hAdd := addMilliseconds -instance : HSub PlainTime Millisecond.Offset PlainTime where +instance : HSub (PlainTime α) Millisecond.Offset (PlainTime α) where hSub := subMilliseconds -instance : HAdd PlainTime Second.Offset PlainTime where +instance : HAdd (PlainTime α) Second.Offset (PlainTime α) where hAdd := addSeconds -instance : HSub PlainTime Second.Offset PlainTime where +instance : HSub (PlainTime α) Second.Offset (PlainTime α) where hSub := subSeconds -instance : HAdd PlainTime Minute.Offset PlainTime where +instance : HAdd (PlainTime α) Minute.Offset (PlainTime α) where hAdd := addMinutes -instance : HSub PlainTime Minute.Offset PlainTime where +instance : HSub (PlainTime α) Minute.Offset (PlainTime α) where hSub := subMinutes -instance : HAdd PlainTime Hour.Offset PlainTime where +instance : HAdd (PlainTime α) Hour.Offset (PlainTime α) where hAdd := addHours -instance : HSub PlainTime Hour.Offset PlainTime where +instance : HSub (PlainTime α) Hour.Offset (PlainTime α) where hSub := subHours end PlainTime diff --git a/src/Std/Time/Zoned.lean b/src/Std/Time/Zoned.lean index 570007ce5ecb..c41edee345d2 100644 --- a/src/Std/Time/Zoned.lean +++ b/src/Std/Time/Zoned.lean @@ -45,8 +45,9 @@ namespace PlainTime Get the current time. -/ @[inline] -def now : IO PlainTime := - PlainDateTime.time <$> PlainDateTime.now +def now : IO (Sigma PlainTime) := do + let res ← PlainDateTime.time <$> PlainDateTime.now + return res end PlainTime @@ -70,8 +71,8 @@ def toPlainDate (dt : DateTime tz) : PlainDate := Converts a `DateTime` to a `PlainTime` -/ @[inline] -def toPlainTime (dt : DateTime tz) : PlainTime := - dt.date.get.time +def toPlainTime (dt : DateTime tz) : PlainTime dt.date.get.time.fst := + dt.date.get.time.snd end DateTime namespace DateTime @@ -110,14 +111,14 @@ Converts a `PlainDate` to a `ZonedDateTime`. -/ @[inline] def ofPlainDate (pd : PlainDate) (zr : TimeZone.ZoneRules) : ZonedDateTime := - ZonedDateTime.ofPlainDateTime (pd.atTime PlainTime.midnight) zr + ZonedDateTime.ofPlainDateTime (pd.atTime (α := true) 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) + ZonedDateTime.ofPlainDateTime (pd.atTime (α := true) PlainTime.midnight) (TimeZone.ZoneRules.ofTimeZone zr) /-- Converts a `ZonedDateTime` to a `PlainDate` @@ -130,7 +131,7 @@ def toPlainDate (dt : ZonedDateTime) : PlainDate := Converts a `ZonedDateTime` to a `PlainTime` -/ @[inline] -def toPlainTime (dt : ZonedDateTime) : PlainTime := +def toPlainTime (dt : ZonedDateTime) : Sigma PlainTime := dt.toPlainDateTime.time /-- diff --git a/src/Std/Time/Zoned/DateTime.lean b/src/Std/Time/Zoned/DateTime.lean index 4f69cda6ce62..ddac17ec35c8 100644 --- a/src/Std/Time/Zoned/DateTime.lean +++ b/src/Std/Time/Zoned/DateTime.lean @@ -305,7 +305,7 @@ def withMinutes (dt : DateTime tz) (minute : Minute.Ordinal) : DateTime tz := Creates a new `DateTime tz` by adjusting the `second` component. -/ @[inline] -def withSeconds (dt : DateTime tz) (second : Sigma Second.Ordinal) : DateTime tz := +def withSeconds (dt : DateTime tz) (second : Second.Ordinal α) : DateTime tz := ofPlainDateTime (dt.date.get.withSeconds second) tz /-- @@ -368,7 +368,7 @@ def minute (dt : DateTime tz) : Minute.Ordinal := Getter for the `Second` inside of a `DateTime` -/ @[inline] -def second (dt : DateTime tz) : Second.Ordinal dt.date.get.time.second.fst := +def second (dt : DateTime tz) : Second.Ordinal dt.date.get.time.fst := dt.date.get.second /-- @@ -376,14 +376,14 @@ Getter for the `Milliseconds` inside of a `DateTime` -/ @[inline] def millisecond (dt : DateTime tz) : Millisecond.Ordinal := - dt.date.get.time.nanosecond.emod 1000 (by decide) + dt.date.get.time.snd.nanosecond.emod 1000 (by decide) /-- Getter for the `Nanosecond` inside of a `DateTime` -/ @[inline] def nanosecond (dt : DateTime tz) : Nanosecond.Ordinal := - dt.date.get.time.nanosecond + dt.date.get.time.snd.nanosecond /-- Gets the `Weekday` of a DateTime. @@ -449,14 +449,14 @@ def quarter (date : DateTime tz) : Bounded.LE 1 4 := Getter for the `PlainTime` inside of a `DateTime` -/ @[inline] -def time (zdt : DateTime tz) : PlainTime := - zdt.date.get.time +def time (zdt : DateTime tz) : PlainTime zdt.date.get.time.fst := + zdt.date.get.time.snd /-- Converts a `DateTime` to the number of days since the UNIX epoch. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (tz : TimeZone) : DateTime tz := +def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime α) (tz : TimeZone) : DateTime tz := DateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) tz instance : HAdd (DateTime tz) (Day.Offset) (DateTime tz) where diff --git a/src/Std/Time/Zoned/ZonedDateTime.lean b/src/Std/Time/Zoned/ZonedDateTime.lean index b7b3d1f94382..f537d97a291e 100644 --- a/src/Std/Time/Zoned/ZonedDateTime.lean +++ b/src/Std/Time/Zoned/ZonedDateTime.lean @@ -137,8 +137,8 @@ def toDateTime (dt : ZonedDateTime) : DateTime dt.timezone := Getter for the `PlainTime` inside of a `ZonedDateTime` -/ @[inline] -def time (zdt : ZonedDateTime) : PlainTime := - zdt.date.get.time +def time (zdt : ZonedDateTime) : PlainTime zdt.date.get.time.fst := + zdt.date.get.time.snd /-- Getter for the `Year` inside of a `ZonedDateTime` @@ -166,7 +166,7 @@ Getter for the `Hour` inside of a `ZonedDateTime` -/ @[inline] def hour (zdt : ZonedDateTime) : Hour.Ordinal := - zdt.date.get.time.hour + zdt.date.get.time.snd.hour /-- Getter for the `Minute` inside of a `ZonedDateTime` @@ -179,22 +179,22 @@ def minute (zdt : ZonedDateTime) : Minute.Ordinal := Getter for the `Second` inside of a `ZonedDateTime` -/ @[inline] -def second (zdt : ZonedDateTime) : Second.Ordinal zdt.date.get.time.second.fst := - zdt.date.get.time.second.snd +def second (zdt : ZonedDateTime) : Second.Ordinal zdt.date.get.time.fst := + zdt.date.get.time.snd.second /-- Getter for the `Millisecond` inside of a `ZonedDateTime`. -/ @[inline] def millisecond (dt : ZonedDateTime) : Millisecond.Ordinal := - dt.date.get.time.millisecond + dt.date.get.time.snd.millisecond /-- Getter for the `Nanosecond` inside of a `ZonedDateTime` -/ @[inline] def nanosecond (zdt : ZonedDateTime) : Nanosecond.Ordinal := - zdt.date.get.time.nanosecond + zdt.date.get.time.snd.nanosecond /-- Getter for the `TimeZone.Offset` inside of a `ZonedDateTime` @@ -493,7 +493,7 @@ Creates a new `ZonedDateTime` by adjusting the `second` component. @[inline] def withSeconds (dt : ZonedDateTime) (second : Sigma Second.Ordinal) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withSeconds second) dt.rules + ZonedDateTime.ofPlainDateTime (date.withSeconds second.snd) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the `nano` component with a new `millis` that will set @@ -528,7 +528,7 @@ def toDaysSinceUNIXEpoch (date : ZonedDateTime) : Day.Offset := Converts a `ZonedDateTime` to the number of days since the UNIX epoch. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (zt : TimeZone.ZoneRules) : ZonedDateTime := +def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime α) (zt : TimeZone.ZoneRules) : ZonedDateTime := ZonedDateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) zt instance : HAdd ZonedDateTime Day.Offset ZonedDateTime where diff --git a/tests/lean/run/timeAPI.lean b/tests/lean/run/timeAPI.lean index 8c99c1fc2624..8ab5aa783672 100644 --- a/tests/lean/run/timeAPI.lean +++ b/tests/lean/run/timeAPI.lean @@ -709,7 +709,7 @@ Std.Time.Weekday.tuesday println! plaindatetime.toDaysSinceUNIXEpoch println! plaindatetime.toTimestampAssumingUTC - println! PlainDateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight + println! PlainDateTime.ofDaysSinceUNIXEpoch (α := True) 1 PlainTime.midnight /-- info: 2024-09-13T02:01:02.000000000-03:00 @@ -783,7 +783,7 @@ Std.Time.Weekday.thursday println! zoned.toDaysSinceUNIXEpoch println! zoned.toTimestamp - println! DateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC + println! DateTime.ofDaysSinceUNIXEpoch (α := True) 1 PlainTime.midnight .UTC /-- info: 1997-03-19T02:03:04.000000000[America/Sao_Paulo] @@ -867,8 +867,8 @@ info: 2023-06-09T00:00:00.000000000 #guard_msgs in #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.ofPlainTime (α := True) time("12:32:43") + println! PlainDateTime.ofDaysSinceUNIXEpoch (α := True) 23332 time("12:32:43") /-- info: 1970-01-02T00:00:00.000000000Z @@ -880,7 +880,7 @@ info: 1970-01-02T00:00:00.000000000Z -/ #guard_msgs in #eval do - println! DateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC + println! DateTime.ofDaysSinceUNIXEpoch (α := true) 1 PlainTime.midnight .UTC println! DateTime.ofPlainDate 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 @@ -898,7 +898,7 @@ info: 1970-01-02T00:00:00.000000000[UTC] -/ #guard_msgs in #eval do - println! ZonedDateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC + println! ZonedDateTime.ofDaysSinceUNIXEpoch (α := True) 1 PlainTime.midnight .UTC println! ZonedDateTime.ofPlainDate date("1997-03-18") .UTC println! ZonedDateTime.ofPlainDateWithZone date("1997-03-18") .UTC println! ZonedDateTime.ofPlainDateTime datetime("1997-03-18T00:01:02") .UTC diff --git a/tests/lean/run/timeClassOperations.lean b/tests/lean/run/timeClassOperations.lean index 39f1967df911..adaa472119a6 100644 --- a/tests/lean/run/timeClassOperations.lean +++ b/tests/lean/run/timeClassOperations.lean @@ -65,7 +65,7 @@ info: datetime("2000-01-19T03:02:01.000000000") #guard_msgs in #eval datetime - (1 : Day.Offset) -def time := time("13:02:01") +def time : PlainTime true := time("13:02:01") /-- info: time("14:02:01.000000000") diff --git a/tests/lean/run/timeFormats.lean b/tests/lean/run/timeFormats.lean index 31be8b6faf55..d3a2341af5f6 100644 --- a/tests/lean/run/timeFormats.lean +++ b/tests/lean/run/timeFormats.lean @@ -20,8 +20,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00") def date₁ := zoned("2014-06-16T03:03:03-03:00") -def time₁ := time("14:11:01") -def time₂ := time("03:11:01") +def time₁ : PlainTime true := time("14:11:01") +def time₂ : PlainTime true := time("03:11:01") /-- info: "Monday, June 16, 2014 03:03:03 -0300" @@ -178,9 +178,9 @@ info: "Monday, June 16, 2014 03:03:03 -0300" info: "14:11:01" -/ #guard_msgs in -#eval Time24Hour.formatBuilder time₁.hour time₁.minute time₁.second +#eval Time24Hour.formatBuilder time₁.hour time₁.minute ⟨true, time₁.second⟩ -def l := Time12Hour.formatBuilder time₁.hour.toRelative time₁.minute time₁.second (if time₁.hour.val > 12 then HourMarker.pm else HourMarker.am) +def l := Time12Hour.formatBuilder time₁.hour.toRelative time₁.minute ⟨true, time₁.second⟩ (if time₁.hour.val > 12 then HourMarker.pm else HourMarker.am) /-- info: "02:11:01 PM" @@ -191,7 +191,7 @@ info: "02:11:01 PM" info: "03:11:01 AM" -/ #guard_msgs in -#eval Time12Hour.formatBuilder time₂.hour.toRelative time₂.minute time₂.second (if time₂.hour.val > 12 then HourMarker.pm else HourMarker.am) +#eval Time12Hour.formatBuilder time₂.hour.toRelative time₂.minute ⟨true, time₂.second⟩ (if time₂.hour.val > 12 then HourMarker.pm else HourMarker.am) /-- info: "06/16/2014" @@ -245,7 +245,7 @@ info: date("2002-07-14") info: time("14:13:12.000000000") -/ #guard_msgs in -#eval time("14:13:12") +#eval (time("14:13:12") : PlainTime true) /-- info: zoned("2002-07-14T14:13:12.000000000Z") @@ -275,9 +275,9 @@ info: "14-13-12" Format -/ -def time₄ := time("23:13:12.324354679") +def time₄ := (time("23:13:12.324354679") : PlainTime true) def date₄ := date("2002-07-14") -def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (PlainTime.mk 12 23 ⟨false, 12⟩ 0) +def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (Sigma.mk true <| PlainTime.mk 12 23 12 0) def datetime₄ := datetime("2002-07-14T23:13:12.324354679") def zoned₄ := zoned("2002-07-14T23:13:12.324354679+09:00") def zoned₅ := zoned("2002-07-14T23:13:12.324354679+00:00") @@ -806,7 +806,7 @@ info: ("19343232432-01-04T01:04:03.000000000", -/ #guard_msgs in #eval - let r := (PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (PlainTime.mk 25 64 ⟨true, 3⟩ 0)) + let r := (PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (Sigma.mk true <| PlainTime.mk 25 64 3 0)) let s := r.toLeanDateTimeString let r := PlainDateTime.parse s (s, r, datetime("1932-01-02T05:04:03.000000000")) diff --git a/tests/lean/run/timeLocalDateTime.lean b/tests/lean/run/timeLocalDateTime.lean index 4863a638729a..6da164c55639 100644 --- a/tests/lean/run/timeLocalDateTime.lean +++ b/tests/lean/run/timeLocalDateTime.lean @@ -5,7 +5,8 @@ open Std.Time def ShortDateTime : GenericFormat .any := datespec("dd/MM/uuuu HH:mm:ss") def ShortDate : GenericFormat .any := datespec("dd/MM/uuuu") -def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.hour PlainDate.minute PlainDate.time.second +def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.snd.hour PlainDate.minute ⟨PlainDate.time.fst, PlainDate.time.snd.second⟩ + def format₂ (PlainDate : PlainDate) : String := ShortDate.formatBuilder PlainDate.day PlainDate.month PlainDate.year def date₁ := datetime("1993-11-19T09:08:07") diff --git a/tests/lean/run/timeOperations.lean b/tests/lean/run/timeOperations.lean index 2aee656f9121..ab1c68a01c53 100644 --- a/tests/lean/run/timeOperations.lean +++ b/tests/lean/run/timeOperations.lean @@ -131,7 +131,7 @@ info: datetime("1999-01-20T03:02:01.000000000") #guard_msgs in #eval datetime.subYearsRollOver 1 -def time := time("13:02:01") +def time : PlainTime true := time("13:02:01") /-- info: time("14:02:01.000000000") diff --git a/tests/lean/run/timeParse.lean b/tests/lean/run/timeParse.lean index fcd7b6be0b77..03815a200b91 100644 --- a/tests/lean/run/timeParse.lean +++ b/tests/lean/run/timeParse.lean @@ -21,8 +21,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00") def date₁ := zoned("2014-06-16T03:03:03-03:00") -def time₁ := time("14:11:01") -def time₂ := time("03:11:01") +def time₁ : PlainTime true := time("14:11:01") +def time₂ : PlainTime true := time("03:11:01") /-- info: "2014-06-16T03:03:03.000000100-03:00" diff --git a/tests/lean/run/timeSet.lean b/tests/lean/run/timeSet.lean index 4f179d506132..55a93c03baef 100644 --- a/tests/lean/run/timeSet.lean +++ b/tests/lean/run/timeSet.lean @@ -21,8 +21,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00") def date₁ := zoned("2014-06-16T10:03:03-03:00") -def time₁ := time("14:11:01") -def time₂ := time("03:11:01") +def time₁ : PlainTime true := time("14:11:01") +def time₂ : PlainTime true := time("03:11:01") /-- info: "2014-06-16T10:03:03.000000100-03:00" From 9d548b454c85dd38d9c9f1b2cfed4fb7b7e45531 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Wed, 18 Dec 2024 15:39:14 -0300 Subject: [PATCH 06/17] fix: change readlink -f to realpath --- src/Std/Time/Zoned/Database/TZdb.lean | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/src/Std/Time/Zoned/Database/TZdb.lean b/src/Std/Time/Zoned/Database/TZdb.lean index 5c0d49bafbad..4a5ebd2deb37 100644 --- a/src/Std/Time/Zoned/Database/TZdb.lean +++ b/src/Std/Time/Zoned/Database/TZdb.lean @@ -71,12 +71,7 @@ def idFromPath (path : System.FilePath) : Option String := do Retrieves the timezone rules from the local timezone data file. -/ def localRules (path : System.FilePath) : IO ZoneRules := do - let localTimePath ← - try - IO.Process.run { cmd := "readlink", args := #["-f", path.toString] } - catch _ => - throw <| IO.userError "cannot find the local timezone database" - + let localTimePath ← IO.FS.realPath path if let some id := idFromPath localTimePath then parseTZIfFromDisk path id else throw (IO.userError "cannot read the id of the path.") From 32a25d84bb588570c5aaa52a61f1282eb36fb9ab Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Thu, 2 Jan 2025 17:42:01 -0300 Subject: [PATCH 07/17] refactor: update src/Std/Time/Time/PlainTime.lean Co-authored-by: Mac Malone --- src/Std/Time/Time/PlainTime.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Time/Time/PlainTime.lean b/src/Std/Time/Time/PlainTime.lean index 67af9129c12e..8e2ba2c4490e 100644 --- a/src/Std/Time/Time/PlainTime.lean +++ b/src/Std/Time/Time/PlainTime.lean @@ -41,7 +41,7 @@ structure PlainTime (leap : Bool) where /-- COMMENT -/ -def LeapTime := PlainTime True +abbrev LeapTime := PlainTime True instance : Inhabited (PlainTime x) where default := ⟨0, 0, 0, 0, by decide⟩ From b8630b587eb9065f9a2c93601f5e6ec603a4cd8e Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Thu, 2 Jan 2025 18:09:14 -0300 Subject: [PATCH 08/17] chore: fix type variable names --- src/Std/Time/DateTime.lean | 6 +- src/Std/Time/DateTime/PlainDateTime.lean | 20 +++--- src/Std/Time/Duration.lean | 4 +- src/Std/Time/Format.lean | 20 +++--- src/Std/Time/Format/Basic.lean | 2 +- src/Std/Time/Notation.lean | 2 +- src/Std/Time/Time/PlainTime.lean | 84 ++++++++++++------------ src/Std/Time/Zoned.lean | 4 +- src/Std/Time/Zoned/DateTime.lean | 2 +- src/Std/Time/Zoned/ZonedDateTime.lean | 2 +- tests/lean/run/timeAPI.lean | 12 ++-- tests/lean/run/timeClassOperations.lean | 2 +- tests/lean/run/timeFormats.lean | 8 +-- tests/lean/run/timeOperations.lean | 2 +- tests/lean/run/timeParse.lean | 4 +- tests/lean/run/timeSet.lean | 4 +- 16 files changed, 89 insertions(+), 89 deletions(-) diff --git a/src/Std/Time/DateTime.lean b/src/Std/Time/DateTime.lean index 50b278327107..8f223bd0a1ef 100644 --- a/src/Std/Time/DateTime.lean +++ b/src/Std/Time/DateTime.lean @@ -50,7 +50,7 @@ def toPlainDateAssumingUTC (timestamp : Timestamp) : PlainDate := Converts a `Timestamp` to a `PlainTime` -/ @[inline] -def getTimeAssumingUTC (timestamp : Timestamp) : PlainTime α := +def getTimeAssumingUTC (timestamp : Timestamp) : PlainTime leap := let nanos := timestamp.toNanosecondsSinceUnixEpoch PlainTime.ofNanoseconds nanos @@ -88,8 +88,8 @@ def toPlainDate (pdt : PlainDateTime) : PlainDate := Converts a `PlainTime` to a `PlainDateTime` -/ @[inline] -def ofPlainTime (time : PlainTime α) : PlainDateTime := - { date := ⟨1, 1, 1, by decide⟩, time := Sigma.mk α time } +def ofPlainTime (time : PlainTime leap) : PlainDateTime := + { date := ⟨1, 1, 1, by decide⟩, time := Sigma.mk leap time } /-- Converts a `PlainDateTime` to a `PlainTime` diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index 0629bf993c6c..ddc5a2643a27 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -144,8 +144,8 @@ def toDaysSinceUNIXEpoch (pdt : PlainDateTime) : Day.Offset := Converts a `PlainDateTime` to the number of days since the UNIX epoch. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime α) : PlainDateTime := - PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) (Sigma.mk α time) +def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime leap) : PlainDateTime := + PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) (Sigma.mk leap time) /-- Sets the `PlainDateTime` to the specified `desiredWeekday`. @@ -528,15 +528,15 @@ def quarter (date : PlainDateTime) : Bounded.LE 1 4 := Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`. -/ @[inline] -def atTime : PlainDate → PlainTime α → PlainDateTime := - (PlainDateTime.mk · <| Sigma.mk α ·) +def atTime : PlainDate → PlainTime leap → PlainDateTime := + (PlainDateTime.mk · <| Sigma.mk leap ·) /-- Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`. -/ @[inline] -def atDate (time: PlainTime α) (date: PlainDate) : PlainDateTime := - PlainDateTime.mk date (Sigma.mk α time) +def atDate (time: PlainTime leap) (date: PlainDate) : PlainDateTime := + PlainDateTime.mk date (Sigma.mk leap time) instance : HAdd PlainDateTime Day.Offset PlainDateTime where hAdd := addDays @@ -590,8 +590,8 @@ namespace PlainDate Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`. -/ @[inline] -def atTime : PlainDate → PlainTime α → PlainDateTime := - (PlainDateTime.mk · <| Sigma.mk α ·) +def atTime : PlainDate → PlainTime leap → PlainDateTime := + (PlainDateTime.mk · <| Sigma.mk leap ·) end PlainDate namespace PlainTime @@ -600,8 +600,8 @@ namespace PlainTime Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`. -/ @[inline] -def atDate (time: PlainTime α) (date: PlainDate) : PlainDateTime := - PlainDateTime.mk date (Sigma.mk α time) +def atDate (time: PlainTime leap) (date: PlainDate) : PlainDateTime := + PlainDateTime.mk date (Sigma.mk leap time) end PlainTime end Time diff --git a/src/Std/Time/Duration.lean b/src/Std/Time/Duration.lean index de32e8138f68..51f828cca906 100644 --- a/src/Std/Time/Duration.lean +++ b/src/Std/Time/Duration.lean @@ -350,10 +350,10 @@ instance : HMul Int Duration Duration where instance : HMul Duration Int Duration where hMul d i := Duration.ofNanoseconds <| Nanosecond.Offset.ofInt (d.toNanoseconds.val * i) -instance : HAdd (PlainTime α) Duration (PlainTime α) where +instance : HAdd (PlainTime leap) Duration (PlainTime leap) where hAdd pt d := PlainTime.ofNanoseconds (d.toNanoseconds + pt.toNanoseconds) -instance : HSub (PlainTime α) Duration (PlainTime α) where +instance : HSub (PlainTime leap) Duration (PlainTime leap) where hSub pt d := PlainTime.ofNanoseconds (d.toNanoseconds - pt.toNanoseconds) end Duration diff --git a/src/Std/Time/Format.lean b/src/Std/Time/Format.lean index 2987321a931f..1345fb368070 100644 --- a/src/Std/Time/Format.lean +++ b/src/Std/Time/Format.lean @@ -254,7 +254,7 @@ namespace PlainTime /-- Formats a `PlainTime` using a specific format. -/ -def format (time : PlainTime α) (format : String) : String := +def format (time : PlainTime leap) (format : String) : String := let format : Except String (GenericFormat .any) := GenericFormat.spec format match format with | .error err => s!"error: {err}" @@ -264,7 +264,7 @@ def format (time : PlainTime α) (format : String) : String := | .k _ => some (time.hour.shiftTo1BasedHour) | .m _ => some time.minute | .n _ => some time.nanosecond - | .s _ => some (Sigma.mk α time.second) + | .s _ => some (Sigma.mk leap time.second) | .a _ => some (HourMarker.ofOrdinal time.hour) | .h _ => some time.hour.toRelative | .K _ => some (time.hour.emod 12 (by decide)) @@ -285,8 +285,8 @@ def fromTime24Hour (input : String) : Except String (Sigma PlainTime) := /-- Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss`). -/ -def toTime24Hour (input : PlainTime α) : String := - Formats.time24Hour.formatBuilder input.hour input.minute (Sigma.mk α input.second) +def toTime24Hour (input : PlainTime leap) : String := + Formats.time24Hour.formatBuilder input.hour input.minute (Sigma.mk leap input.second) /-- Parses a time string in the lean 24-hour format (`HH:mm:ss.SSSSSSSSS` or `HH:mm:ss`) and returns a `PlainTime`. @@ -298,8 +298,8 @@ def fromLeanTime24Hour (input : String) : Except String (Sigma PlainTime) := /-- Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss.SSSSSSSSS`). -/ -def toLeanTime24Hour (input : PlainTime α) : String := - Formats.leanTime24Hour.formatBuilder input.hour input.minute (Sigma.mk α input.second) input.nanosecond +def toLeanTime24Hour (input : PlainTime leap) : String := + Formats.leanTime24Hour.formatBuilder input.hour input.minute (Sigma.mk leap input.second) input.nanosecond /-- Parses a time string in the 12-hour format (`hh:mm:ss aa`) and returns a `PlainTime`. @@ -314,8 +314,8 @@ def fromTime12Hour (input : String) : Except String (Sigma PlainTime) := do /-- Formats a `PlainTime` value into a 12-hour format string (`hh:mm:ss aa`). -/ -def toTime12Hour (input : PlainTime α) : String := - Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute (Sigma.mk α input.second) (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am) +def toTime12Hour (input : PlainTime leap) : String := + Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute (Sigma.mk leap input.second) (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am) /-- Parses a `String` in the `Time12Hour` or `Time24Hour` format and returns a `PlainTime`. @@ -324,10 +324,10 @@ def parse (input : String) : Except String (Sigma PlainTime) := fromTime12Hour input <|> fromTime24Hour input -instance : ToString (PlainTime α) where +instance : ToString (PlainTime leap) where toString := toLeanTime24Hour -instance : Repr (PlainTime α) where +instance : Repr (PlainTime leap) where reprPrec data := Repr.addAppParen ("time(\"" ++ toLeanTime24Hour data ++ "\")") end PlainTime diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean index 5b9c390b5d98..b3941bb446ee 100644 --- a/src/Std/Time/Format/Basic.lean +++ b/src/Std/Time/Format/Basic.lean @@ -736,7 +736,7 @@ private def toSigned (data : Int) : String := private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bool) (colon : Bool) : String := let (sign, time) := if offset.second.val ≥ 0 then ("+", offset.second) else ("-", -offset.second) - let time : PlainTime true := PlainTime.ofSeconds time + let time : LeapTime := PlainTime.ofSeconds time let pad := leftPad 2 '0' ∘ toString let data := s!"{sign}{pad time.hour.val}" diff --git a/src/Std/Time/Notation.lean b/src/Std/Time/Notation.lean index 7bc34a2e2984..bdf39a69e834 100644 --- a/src/Std/Time/Notation.lean +++ b/src/Std/Time/Notation.lean @@ -125,7 +125,7 @@ private def convertTimezone (tz : Std.Time.TimeZone) : MacroM (TSyntax `term) := private def convertPlainDate (d : Std.Time.PlainDate) : MacroM (TSyntax `term) := do `(Std.Time.PlainDate.ofYearMonthDayClip $(← syntaxInt d.year) $(← syntaxBounded d.month.val) $(← syntaxBounded d.day.val)) -private def convertPlainTime (d : Std.Time.PlainTime α) : MacroM (TSyntax `term) := do +private def convertPlainTime (d : Std.Time.PlainTime leap) : MacroM (TSyntax `term) := do `(Std.Time.PlainTime.mk $(← syntaxBounded d.hour.val) $(← syntaxBounded d.minute.val) $(← syntaxBounded d.second.val) $(← syntaxBounded d.nanosecond.val)) private def convertPlainDateTime (d : Std.Time.PlainDateTime) : MacroM (TSyntax `term) := do diff --git a/src/Std/Time/Time/PlainTime.lean b/src/Std/Time/Time/PlainTime.lean index 8e2ba2c4490e..7ce514c801d7 100644 --- a/src/Std/Time/Time/PlainTime.lean +++ b/src/Std/Time/Time/PlainTime.lean @@ -39,9 +39,9 @@ structure PlainTime (leap : Bool) where deriving Repr /-- -COMMENT +Defines `LeapTime` as a shorthand for a `PlainTime` that can contain leap seconds. -/ -abbrev LeapTime := PlainTime True +abbrev LeapTime := PlainTime true instance : Inhabited (PlainTime x) where default := ⟨0, 0, 0, 0, by decide⟩ @@ -55,27 +55,27 @@ namespace PlainTime /-- Creates a `PlainTime` value representing midnight (00:00:00.000000000). -/ -def midnight : PlainTime α := +def midnight : PlainTime leap := ⟨0, 0, 0, 0⟩ /-- Creates a `PlainTime` value from the provided hours, minutes, seconds and nanoseconds components. -/ @[inline] -def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal α) (nano : Nanosecond.Ordinal) : PlainTime α := +def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) (nano : Nanosecond.Ordinal) : PlainTime leap := ⟨hour, minute, second, nano⟩ /-- Creates a `PlainTime` value from the provided hours, minutes, and seconds. -/ @[inline] -def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal α) : PlainTime α := +def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) : PlainTime leap := ofHourMinuteSecondsNano hour minute second 0 /-- Converts a `PlainTime` value to the total number of milliseconds. -/ -def toMilliseconds (time : PlainTime α) : Millisecond.Offset := +def toMilliseconds (time : PlainTime leap) : Millisecond.Offset := time.hour.toOffset.toMilliseconds + time.minute.toOffset.toMilliseconds + time.second.toOffset.toMilliseconds + @@ -84,7 +84,7 @@ def toMilliseconds (time : PlainTime α) : Millisecond.Offset := /-- Converts a `PlainTime` value to the total number of nanoseconds. -/ -def toNanoseconds (time : PlainTime α) : Nanosecond.Offset := +def toNanoseconds (time : PlainTime leap) : Nanosecond.Offset := time.hour.toOffset.toNanoseconds + time.minute.toOffset.toNanoseconds + time.second.toOffset.toNanoseconds + @@ -93,7 +93,7 @@ def toNanoseconds (time : PlainTime α) : Nanosecond.Offset := /-- Converts a `PlainTime` value to the total number of seconds. -/ -def toSeconds (time : PlainTime α) : Second.Offset := +def toSeconds (time : PlainTime leap) : Second.Offset := time.hour.toOffset.toSeconds + time.minute.toOffset.toSeconds + time.second.toOffset @@ -101,7 +101,7 @@ def toSeconds (time : PlainTime α) : Second.Offset := /-- Converts a `PlainTime` value to the total number of minutes. -/ -def toMinutes (time : PlainTime α) : Minute.Offset := +def toMinutes (time : PlainTime leap) : Minute.Offset := time.hour.toOffset.toMinutes + time.minute.toOffset + time.second.toOffset.toMinutes @@ -109,13 +109,13 @@ def toMinutes (time : PlainTime α) : Minute.Offset := /-- Converts a `PlainTime` value to the total number of hours. -/ -def toHours (time : PlainTime α) : Hour.Offset := +def toHours (time : PlainTime leap) : Hour.Offset := time.hour.toOffset /-- Creates a `PlainTime` value from a total number of nanoseconds. -/ -def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime α := +def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime leap := have totalSeconds := nanos.ediv 1000000000 have remainingNanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide) have hours := Bounded.LE.byEmod (totalSeconds.val / 3600) 24 (by decide) @@ -124,7 +124,7 @@ def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime α := have seconds := Bounded.LE.byEmod totalSeconds.val 60 (by decide) have seconds := - match α with + match leap with | true => seconds.expandTop (by decide) | false => seconds @@ -135,35 +135,35 @@ def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime α := Creates a `PlainTime` value from a total number of millisecond. -/ @[inline] -def ofMilliseconds (millis : Millisecond.Offset) : PlainTime α := +def ofMilliseconds (millis : Millisecond.Offset) : PlainTime leap := ofNanoseconds millis.toNanoseconds /-- Creates a `PlainTime` value from a total number of seconds. -/ @[inline] -def ofSeconds (secs : Second.Offset) : PlainTime α := +def ofSeconds (secs : Second.Offset) : PlainTime leap := ofNanoseconds secs.toNanoseconds /-- Creates a `PlainTime` value from a total number of minutes. -/ @[inline] -def ofMinutes (secs : Minute.Offset) : PlainTime α := +def ofMinutes (secs : Minute.Offset) : PlainTime leap := ofNanoseconds secs.toNanoseconds /-- Creates a `PlainTime` value from a total number of hours. -/ @[inline] -def ofHours (hour : Hour.Offset) : PlainTime α := +def ofHours (hour : Hour.Offset) : PlainTime leap := ofNanoseconds hour.toNanoseconds /-- Adds seconds to a `PlainTime`. -/ @[inline] -def addSeconds (time : PlainTime α) (secondsToAdd : Second.Offset) : PlainTime α := +def addSeconds (time : PlainTime leap) (secondsToAdd : Second.Offset) : PlainTime leap := let totalSeconds := time.toNanoseconds + secondsToAdd.toNanoseconds ofNanoseconds totalSeconds @@ -171,14 +171,14 @@ def addSeconds (time : PlainTime α) (secondsToAdd : Second.Offset) : PlainTime Subtracts seconds from a `PlainTime`. -/ @[inline] -def subSeconds (time : PlainTime α) (secondsToSub : Second.Offset) : PlainTime α := +def subSeconds (time : PlainTime leap) (secondsToSub : Second.Offset) : PlainTime leap := addSeconds time (-secondsToSub) /-- Adds minutes to a `PlainTime`. -/ @[inline] -def addMinutes (time : PlainTime α) (minutesToAdd : Minute.Offset) : PlainTime α := +def addMinutes (time : PlainTime leap) (minutesToAdd : Minute.Offset) : PlainTime leap := let total := time.toNanoseconds + minutesToAdd.toNanoseconds ofNanoseconds total @@ -186,14 +186,14 @@ def addMinutes (time : PlainTime α) (minutesToAdd : Minute.Offset) : PlainTime Subtracts minutes from a `PlainTime`. -/ @[inline] -def subMinutes (time : PlainTime α) (minutesToSub : Minute.Offset) : PlainTime α := +def subMinutes (time : PlainTime leap) (minutesToSub : Minute.Offset) : PlainTime leap := addMinutes time (-minutesToSub) /-- Adds hours to a `PlainTime`. -/ @[inline] -def addHours (time : PlainTime α) (hoursToAdd : Hour.Offset) : PlainTime α := +def addHours (time : PlainTime leap) (hoursToAdd : Hour.Offset) : PlainTime leap := let total := time.toNanoseconds + hoursToAdd.toNanoseconds ofNanoseconds total @@ -201,54 +201,54 @@ def addHours (time : PlainTime α) (hoursToAdd : Hour.Offset) : PlainTime α := Subtracts hours from a `PlainTime`. -/ @[inline] -def subHours (time : PlainTime α) (hoursToSub : Hour.Offset) : PlainTime α := +def subHours (time : PlainTime leap) (hoursToSub : Hour.Offset) : PlainTime leap := addHours time (-hoursToSub) /-- Adds nanoseconds to a `PlainTime`. -/ -def addNanoseconds (time : PlainTime α) (nanosToAdd : Nanosecond.Offset) : PlainTime α := +def addNanoseconds (time : PlainTime leap) (nanosToAdd : Nanosecond.Offset) : PlainTime leap := let total := time.toNanoseconds + nanosToAdd ofNanoseconds total /-- Subtracts nanoseconds from a `PlainTime`. -/ -def subNanoseconds (time : PlainTime α) (nanosToSub : Nanosecond.Offset) : PlainTime α := +def subNanoseconds (time : PlainTime leap) (nanosToSub : Nanosecond.Offset) : PlainTime leap := addNanoseconds time (-nanosToSub) /-- Adds milliseconds to a `PlainTime`. -/ -def addMilliseconds (time : PlainTime α) (millisToAdd : Millisecond.Offset) : PlainTime α := +def addMilliseconds (time : PlainTime leap) (millisToAdd : Millisecond.Offset) : PlainTime leap := let total := time.toMilliseconds + millisToAdd ofMilliseconds total /-- Subtracts milliseconds from a `PlainTime`. -/ -def subMilliseconds (time : PlainTime α) (millisToSub : Millisecond.Offset) : PlainTime α := +def subMilliseconds (time : PlainTime leap) (millisToSub : Millisecond.Offset) : PlainTime leap := addMilliseconds time (-millisToSub) /-- Creates a new `PlainTime` by adjusting the `second` component to the given value. -/ @[inline] -def withSeconds (pt : PlainTime α) (second : Second.Ordinal α) : PlainTime α := +def withSeconds (pt : PlainTime leap) (second : Second.Ordinal leap) : PlainTime leap := { pt with second := second } /-- Creates a new `PlainTime` by adjusting the `minute` component to the given value. -/ @[inline] -def withMinutes (pt : PlainTime α) (minute : Minute.Ordinal) : PlainTime α := +def withMinutes (pt : PlainTime leap) (minute : Minute.Ordinal) : PlainTime leap := { pt with minute := minute } /-- Creates a new `PlainTime` by adjusting the milliseconds component inside the `nano` component of its `time` to the given value. -/ @[inline] -def withMilliseconds (pt : PlainTime α) (millis : Millisecond.Ordinal) : PlainTime α := +def withMilliseconds (pt : PlainTime leap) (millis : Millisecond.Ordinal) : PlainTime leap := let minorPart := pt.nanosecond.emod 1000 (by decide) let majorPart := millis.mul_pos 1000000 (by decide) |>.addBounds minorPart { pt with nanosecond := majorPart |>.expandTop (by decide) } @@ -257,51 +257,51 @@ def withMilliseconds (pt : PlainTime α) (millis : Millisecond.Ordinal) : PlainT Creates a new `PlainTime` by adjusting the `nano` component to the given value. -/ @[inline] -def withNanoseconds (pt : PlainTime α) (nano : Nanosecond.Ordinal) : PlainTime α := +def withNanoseconds (pt : PlainTime leap) (nano : Nanosecond.Ordinal) : PlainTime leap := { pt with nanosecond := nano } /-- Creates a new `PlainTime` by adjusting the `hour` component to the given value. -/ @[inline] -def withHours (pt : PlainTime α) (hour : Hour.Ordinal) : PlainTime α := +def withHours (pt : PlainTime leap) (hour : Hour.Ordinal) : PlainTime leap := { pt with hour := hour } /-- `Millisecond` component of the `PlainTime` -/ @[inline] -def millisecond (pt : PlainTime α) : Millisecond.Ordinal := +def millisecond (pt : PlainTime leap) : Millisecond.Ordinal := pt.nanosecond.ediv 1000000 (by decide) -instance : HAdd (PlainTime α) Nanosecond.Offset (PlainTime α) where +instance : HAdd (PlainTime leap) Nanosecond.Offset (PlainTime leap) where hAdd := addNanoseconds -instance : HSub (PlainTime α) Nanosecond.Offset (PlainTime α) where +instance : HSub (PlainTime leap) Nanosecond.Offset (PlainTime leap) where hSub := subNanoseconds -instance : HAdd (PlainTime α) Millisecond.Offset (PlainTime α) where +instance : HAdd (PlainTime leap) Millisecond.Offset (PlainTime leap) where hAdd := addMilliseconds -instance : HSub (PlainTime α) Millisecond.Offset (PlainTime α) where +instance : HSub (PlainTime leap) Millisecond.Offset (PlainTime leap) where hSub := subMilliseconds -instance : HAdd (PlainTime α) Second.Offset (PlainTime α) where +instance : HAdd (PlainTime leap) Second.Offset (PlainTime leap) where hAdd := addSeconds -instance : HSub (PlainTime α) Second.Offset (PlainTime α) where +instance : HSub (PlainTime leap) Second.Offset (PlainTime leap) where hSub := subSeconds -instance : HAdd (PlainTime α) Minute.Offset (PlainTime α) where +instance : HAdd (PlainTime leap) Minute.Offset (PlainTime leap) where hAdd := addMinutes -instance : HSub (PlainTime α) Minute.Offset (PlainTime α) where +instance : HSub (PlainTime leap) Minute.Offset (PlainTime leap) where hSub := subMinutes -instance : HAdd (PlainTime α) Hour.Offset (PlainTime α) where +instance : HAdd (PlainTime leap) Hour.Offset (PlainTime leap) where hAdd := addHours -instance : HSub (PlainTime α) Hour.Offset (PlainTime α) where +instance : HSub (PlainTime leap) Hour.Offset (PlainTime leap) where hSub := subHours end PlainTime diff --git a/src/Std/Time/Zoned.lean b/src/Std/Time/Zoned.lean index c41edee345d2..e1500adc6784 100644 --- a/src/Std/Time/Zoned.lean +++ b/src/Std/Time/Zoned.lean @@ -111,14 +111,14 @@ Converts a `PlainDate` to a `ZonedDateTime`. -/ @[inline] def ofPlainDate (pd : PlainDate) (zr : TimeZone.ZoneRules) : ZonedDateTime := - ZonedDateTime.ofPlainDateTime (pd.atTime (α := true) PlainTime.midnight) zr + ZonedDateTime.ofPlainDateTime (pd.atTime (leap := true) PlainTime.midnight) zr /-- Converts a `PlainDate` to a `ZonedDateTime` using `TimeZone`. -/ @[inline] def ofPlainDateWithZone (pd : PlainDate) (zr : TimeZone) : ZonedDateTime := - ZonedDateTime.ofPlainDateTime (pd.atTime (α := true) PlainTime.midnight) (TimeZone.ZoneRules.ofTimeZone zr) + ZonedDateTime.ofPlainDateTime (pd.atTime (leap := true) PlainTime.midnight) (TimeZone.ZoneRules.ofTimeZone zr) /-- Converts a `ZonedDateTime` to a `PlainDate` diff --git a/src/Std/Time/Zoned/DateTime.lean b/src/Std/Time/Zoned/DateTime.lean index ddac17ec35c8..2a743b921e7c 100644 --- a/src/Std/Time/Zoned/DateTime.lean +++ b/src/Std/Time/Zoned/DateTime.lean @@ -456,7 +456,7 @@ def time (zdt : DateTime tz) : PlainTime zdt.date.get.time.fst := Converts a `DateTime` to the number of days since the UNIX epoch. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime α) (tz : TimeZone) : DateTime tz := +def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime leap) (tz : TimeZone) : DateTime tz := DateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) tz instance : HAdd (DateTime tz) (Day.Offset) (DateTime tz) where diff --git a/src/Std/Time/Zoned/ZonedDateTime.lean b/src/Std/Time/Zoned/ZonedDateTime.lean index f537d97a291e..fed4c5680a64 100644 --- a/src/Std/Time/Zoned/ZonedDateTime.lean +++ b/src/Std/Time/Zoned/ZonedDateTime.lean @@ -528,7 +528,7 @@ def toDaysSinceUNIXEpoch (date : ZonedDateTime) : Day.Offset := Converts a `ZonedDateTime` to the number of days since the UNIX epoch. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime α) (zt : TimeZone.ZoneRules) : ZonedDateTime := +def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime leap) (zt : TimeZone.ZoneRules) : ZonedDateTime := ZonedDateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) zt instance : HAdd ZonedDateTime Day.Offset ZonedDateTime where diff --git a/tests/lean/run/timeAPI.lean b/tests/lean/run/timeAPI.lean index 8ab5aa783672..7e311b489850 100644 --- a/tests/lean/run/timeAPI.lean +++ b/tests/lean/run/timeAPI.lean @@ -709,7 +709,7 @@ Std.Time.Weekday.tuesday println! plaindatetime.toDaysSinceUNIXEpoch println! plaindatetime.toTimestampAssumingUTC - println! PlainDateTime.ofDaysSinceUNIXEpoch (α := True) 1 PlainTime.midnight + println! PlainDateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight /-- info: 2024-09-13T02:01:02.000000000-03:00 @@ -783,7 +783,7 @@ Std.Time.Weekday.thursday println! zoned.toDaysSinceUNIXEpoch println! zoned.toTimestamp - println! DateTime.ofDaysSinceUNIXEpoch (α := True) 1 PlainTime.midnight .UTC + println! DateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight .UTC /-- info: 1997-03-19T02:03:04.000000000[America/Sao_Paulo] @@ -867,8 +867,8 @@ info: 2023-06-09T00:00:00.000000000 #guard_msgs in #eval do println! PlainDateTime.ofPlainDate date("2023-06-09") - println! PlainDateTime.ofPlainTime (α := True) time("12:32:43") - println! PlainDateTime.ofDaysSinceUNIXEpoch (α := True) 23332 time("12:32:43") + println! PlainDateTime.ofPlainTime (leap := True) time("12:32:43") + println! PlainDateTime.ofDaysSinceUNIXEpoch (leap := True) 23332 time("12:32:43") /-- info: 1970-01-02T00:00:00.000000000Z @@ -880,7 +880,7 @@ info: 1970-01-02T00:00:00.000000000Z -/ #guard_msgs in #eval do - println! DateTime.ofDaysSinceUNIXEpoch (α := true) 1 PlainTime.midnight .UTC + println! DateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight .UTC println! DateTime.ofPlainDate 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 @@ -898,7 +898,7 @@ info: 1970-01-02T00:00:00.000000000[UTC] -/ #guard_msgs in #eval do - println! ZonedDateTime.ofDaysSinceUNIXEpoch (α := True) 1 PlainTime.midnight .UTC + println! ZonedDateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight .UTC println! ZonedDateTime.ofPlainDate date("1997-03-18") .UTC println! ZonedDateTime.ofPlainDateWithZone date("1997-03-18") .UTC println! ZonedDateTime.ofPlainDateTime datetime("1997-03-18T00:01:02") .UTC diff --git a/tests/lean/run/timeClassOperations.lean b/tests/lean/run/timeClassOperations.lean index adaa472119a6..c2d738a434ee 100644 --- a/tests/lean/run/timeClassOperations.lean +++ b/tests/lean/run/timeClassOperations.lean @@ -65,7 +65,7 @@ info: datetime("2000-01-19T03:02:01.000000000") #guard_msgs in #eval datetime - (1 : Day.Offset) -def time : PlainTime true := time("13:02:01") +def time : LeapTime := time("13:02:01") /-- info: time("14:02:01.000000000") diff --git a/tests/lean/run/timeFormats.lean b/tests/lean/run/timeFormats.lean index d3a2341af5f6..930889fd3afe 100644 --- a/tests/lean/run/timeFormats.lean +++ b/tests/lean/run/timeFormats.lean @@ -20,8 +20,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00") def date₁ := zoned("2014-06-16T03:03:03-03:00") -def time₁ : PlainTime true := time("14:11:01") -def time₂ : PlainTime true := time("03:11:01") +def time₁ : LeapTime := time("14:11:01") +def time₂ : LeapTime := time("03:11:01") /-- info: "Monday, June 16, 2014 03:03:03 -0300" @@ -245,7 +245,7 @@ info: date("2002-07-14") info: time("14:13:12.000000000") -/ #guard_msgs in -#eval (time("14:13:12") : PlainTime true) +#eval (time("14:13:12") : LeapTime ) /-- info: zoned("2002-07-14T14:13:12.000000000Z") @@ -275,7 +275,7 @@ info: "14-13-12" Format -/ -def time₄ := (time("23:13:12.324354679") : PlainTime true) +def time₄ := (time("23:13:12.324354679") : LeapTime ) def date₄ := date("2002-07-14") def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (Sigma.mk true <| PlainTime.mk 12 23 12 0) def datetime₄ := datetime("2002-07-14T23:13:12.324354679") diff --git a/tests/lean/run/timeOperations.lean b/tests/lean/run/timeOperations.lean index ab1c68a01c53..37fe808b8e95 100644 --- a/tests/lean/run/timeOperations.lean +++ b/tests/lean/run/timeOperations.lean @@ -131,7 +131,7 @@ info: datetime("1999-01-20T03:02:01.000000000") #guard_msgs in #eval datetime.subYearsRollOver 1 -def time : PlainTime true := time("13:02:01") +def time : LeapTime := time("13:02:01") /-- info: time("14:02:01.000000000") diff --git a/tests/lean/run/timeParse.lean b/tests/lean/run/timeParse.lean index 03815a200b91..72af186a45ed 100644 --- a/tests/lean/run/timeParse.lean +++ b/tests/lean/run/timeParse.lean @@ -21,8 +21,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00") def date₁ := zoned("2014-06-16T03:03:03-03:00") -def time₁ : PlainTime true := time("14:11:01") -def time₂ : PlainTime true := time("03:11:01") +def time₁ : LeapTime := time("14:11:01") +def time₂ : LeapTime := time("03:11:01") /-- info: "2014-06-16T03:03:03.000000100-03:00" diff --git a/tests/lean/run/timeSet.lean b/tests/lean/run/timeSet.lean index 55a93c03baef..23b165273438 100644 --- a/tests/lean/run/timeSet.lean +++ b/tests/lean/run/timeSet.lean @@ -21,8 +21,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00") def date₁ := zoned("2014-06-16T10:03:03-03:00") -def time₁ : PlainTime true := time("14:11:01") -def time₂ : PlainTime true := time("03:11:01") +def time₁ : LeapTime := time("14:11:01") +def time₂ : LeapTime := time("03:11:01") /-- info: "2014-06-16T10:03:03.000000100-03:00" From 51975f630c88359470f66121e842128505c95a74 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Wed, 8 Jan 2025 14:45:28 -0300 Subject: [PATCH 09/17] feat: update src/Std/Time/Zoned/DateTime.lean Co-authored-by: Markus Himmel --- src/Std/Time/Zoned/DateTime.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Time/Zoned/DateTime.lean b/src/Std/Time/Zoned/DateTime.lean index 2a743b921e7c..f1022f5fceed 100644 --- a/src/Std/Time/Zoned/DateTime.lean +++ b/src/Std/Time/Zoned/DateTime.lean @@ -305,7 +305,7 @@ def withMinutes (dt : DateTime tz) (minute : Minute.Ordinal) : DateTime tz := Creates a new `DateTime tz` by adjusting the `second` component. -/ @[inline] -def withSeconds (dt : DateTime tz) (second : Second.Ordinal α) : DateTime tz := +def withSeconds (dt : DateTime tz) (second : Second.Ordinal leap) : DateTime tz := ofPlainDateTime (dt.date.get.withSeconds second) tz /-- From 6a8831ecfffc3a43af866e04241816dafb758fa0 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Wed, 8 Jan 2025 14:45:37 -0300 Subject: [PATCH 10/17] feat: update tests/lean/run/timeAPI.lean Co-authored-by: Markus Himmel --- tests/lean/run/timeAPI.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/timeAPI.lean b/tests/lean/run/timeAPI.lean index 7e311b489850..989c33cf6617 100644 --- a/tests/lean/run/timeAPI.lean +++ b/tests/lean/run/timeAPI.lean @@ -709,7 +709,7 @@ Std.Time.Weekday.tuesday println! plaindatetime.toDaysSinceUNIXEpoch println! plaindatetime.toTimestampAssumingUTC - println! PlainDateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight + println! PlainDateTime.ofDaysSinceUNIXEpoch (leap := true) 1 PlainTime.midnight /-- info: 2024-09-13T02:01:02.000000000-03:00 From 6e635f133cc07bfdccdd1b1360525e9dc0fad406 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Thu, 9 Jan 2025 18:48:54 -0300 Subject: [PATCH 11/17] revert: reverted the changes in the PlainTime structure to a better API --- src/Std/Time/DateTime.lean | 12 +-- src/Std/Time/DateTime/PlainDateTime.lean | 85 +++++++++++---------- src/Std/Time/Duration.lean | 4 +- src/Std/Time/Format.lean | 52 ++++++------- src/Std/Time/Format/Basic.lean | 28 +++---- src/Std/Time/Notation.lean | 6 +- src/Std/Time/Time/PlainTime.lean | 94 ++++++++++++------------ src/Std/Time/Time/Unit/Second.lean | 6 +- src/Std/Time/Zoned.lean | 12 +-- src/Std/Time/Zoned/DateTime.lean | 14 ++-- src/Std/Time/Zoned/ZonedDateTime.lean | 20 ++--- tests/lean/run/timeAPI.lean | 20 ++--- tests/lean/run/timeFormats.lean | 10 +-- tests/lean/run/timeLocalDateTime.lean | 2 +- tests/lean/run/timeSet.lean | 2 +- 15 files changed, 181 insertions(+), 186 deletions(-) diff --git a/src/Std/Time/DateTime.lean b/src/Std/Time/DateTime.lean index 8f223bd0a1ef..ec83e83f0790 100644 --- a/src/Std/Time/DateTime.lean +++ b/src/Std/Time/DateTime.lean @@ -50,7 +50,7 @@ def toPlainDateAssumingUTC (timestamp : Timestamp) : PlainDate := Converts a `Timestamp` to a `PlainTime` -/ @[inline] -def getTimeAssumingUTC (timestamp : Timestamp) : PlainTime leap := +def getTimeAssumingUTC (timestamp : Timestamp) : PlainTime := let nanos := timestamp.toNanosecondsSinceUnixEpoch PlainTime.ofNanoseconds nanos @@ -75,7 +75,7 @@ Converts a `PlainDate` to a `Timestamp` -/ @[inline] def ofPlainDate (date : PlainDate) : PlainDateTime := - { date, time := Sigma.mk true (PlainTime.midnight) } + { date, time := PlainTime.midnight } /-- Converts a `PlainDateTime` to a `PlainDate` @@ -88,15 +88,15 @@ def toPlainDate (pdt : PlainDateTime) : PlainDate := Converts a `PlainTime` to a `PlainDateTime` -/ @[inline] -def ofPlainTime (time : PlainTime leap) : PlainDateTime := - { date := ⟨1, 1, 1, by decide⟩, time := Sigma.mk leap time } +def ofPlainTime (time : PlainTime) : PlainDateTime := + { date := ⟨1, 1, 1, by decide⟩, time } /-- Converts a `PlainDateTime` to a `PlainTime` -/ @[inline] -def toPlainTime (pdt : PlainDateTime) : PlainTime pdt.time.fst := - pdt.time.snd +def toPlainTime (pdt : PlainDateTime) : PlainTime := + pdt.time instance : HSub PlainDateTime PlainDateTime Duration where hSub x y := x.toTimestampAssumingUTC - y.toTimestampAssumingUTC diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index ddc5a2643a27..d873635279fb 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -28,17 +28,16 @@ structure PlainDateTime where /-- The `Time` component of a `PlainTime` -/ - time : Sigma PlainTime + time : PlainTime deriving Repr instance : Inhabited PlainDateTime where default := { date := Inhabited.default, - time := Sigma.mk true Inhabited.default + time := Inhabited.default } - namespace PlainDateTime /-- @@ -46,8 +45,8 @@ Converts a `PlainDateTime` to a `Timestamp` -/ def toTimestampAssumingUTC (dt : PlainDateTime) : Timestamp := let days := dt.date.toDaysSinceUNIXEpoch - let nanos := days.toSeconds + dt.time.snd.toSeconds |>.mul 1000000000 - let nanos := nanos.val + dt.time.snd.nanosecond.val + let nanos := days.toSeconds + dt.time.toSeconds |>.mul 1000000000 + let nanos := nanos.val + dt.time.nanosecond.val Timestamp.ofNanosecondsSinceUnixEpoch (Nanosecond.Offset.ofInt nanos) /-- @@ -130,7 +129,7 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do return { date := PlainDate.ofYearMonthDayClip year hmon (Day.Ordinal.ofFin (Fin.succ mday)) - time := Sigma.mk false (PlainTime.ofHourMinuteSecondsNano (hour.expandTop (by decide)) minute second nano) + time := PlainTime.ofHourMinuteSecondsNano (hour.expandTop (by decide)) minute (second.expandTop (by decide)) nano } /-- @@ -144,8 +143,8 @@ def toDaysSinceUNIXEpoch (pdt : PlainDateTime) : Day.Offset := Converts a `PlainDateTime` to the number of days since the UNIX epoch. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime leap) : PlainDateTime := - PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) (Sigma.mk leap time) +def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) : PlainDateTime := + PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) (time) /-- Sets the `PlainDateTime` to the specified `desiredWeekday`. @@ -206,35 +205,35 @@ Creates a new `PlainDateTime` by adjusting the `hour` component of its `time` to -/ @[inline] def withHours (dt : PlainDateTime) (hour : Hour.Ordinal) : PlainDateTime := - { dt with time := Sigma.mk dt.time.fst { dt.time.snd with hour := hour } } + { dt with time := { dt.time with hour } } /-- Creates a new `PlainDateTime` by adjusting the `minute` component of its `time` to the given value. -/ @[inline] def withMinutes (dt : PlainDateTime) (minute : Minute.Ordinal) : PlainDateTime := - { dt with time := Sigma.mk dt.time.fst { dt.time.snd with minute := minute } } + { dt with time := { dt.time with minute := minute } } /-- Creates a new `PlainDateTime` by adjusting the `second` component of its `time` to the given value. -/ @[inline] -def withSeconds (dt : PlainDateTime) (second : Second.Ordinal α) : PlainDateTime := - { dt with time := Sigma.mk α { dt.time.snd with second := second } } +def withSeconds (dt : PlainDateTime) (second : Second.Ordinal true) : PlainDateTime := + { dt with time := { dt.time with second := second } } /-- Creates a new `PlainDateTime` by adjusting the milliseconds component inside the `nano` component of its `time` to the given value. -/ @[inline] def withMilliseconds (dt : PlainDateTime) (millis : Millisecond.Ordinal) : PlainDateTime := - { dt with time := Sigma.mk dt.time.fst (dt.time.snd.withMilliseconds millis) } + { dt with time := (dt.time.withMilliseconds millis) } /-- Creates a new `PlainDateTime` by adjusting the `nano` component of its `time` to the given value. -/ @[inline] def withNanoseconds (dt : PlainDateTime) (nano : Nanosecond.Ordinal) : PlainDateTime := - { dt with time := Sigma.mk dt.time.fst (dt.time.snd.withNanoseconds nano) } + { dt with time := (dt.time.withNanoseconds nano) } /-- Adds a `Day.Offset` to a `PlainDateTime`. @@ -329,10 +328,10 @@ Adds an `Hour.Offset` to a `PlainDateTime`, adjusting the date if the hour overf -/ @[inline] def addHours (dt : PlainDateTime) (hours : Hour.Offset) : PlainDateTime := - let totalSeconds := dt.time.snd.toSeconds + hours.toSeconds + let totalSeconds := dt.time.toSeconds + hours.toSeconds let days := totalSeconds.ediv 86400 - let newTime := dt.time.snd.addSeconds (hours.toSeconds) - { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime } + let newTime := dt.time.addSeconds (hours.toSeconds) + { dt with date := dt.date.addDays days, time := newTime } /-- Subtracts an `Hour.Offset` from a `PlainDateTime`, adjusting the date if the hour underflows. @@ -346,10 +345,10 @@ 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.snd.toSeconds + minutes.toSeconds + let totalSeconds := dt.time.toSeconds + minutes.toSeconds let days := totalSeconds.ediv 86400 - let newTime := dt.time.snd.addSeconds (minutes.toSeconds) - { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime } + let newTime := dt.time.addSeconds (minutes.toSeconds) + { dt with date := dt.date.addDays days, time := newTime } /-- Subtracts a `Minute.Offset` from a `PlainDateTime`, adjusting the hour and date if the minutes underflow. @@ -363,10 +362,10 @@ 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.snd.toSeconds + seconds + let totalSeconds := dt.time.toSeconds + seconds let days := totalSeconds.ediv 86400 - let newTime := dt.time.snd.addSeconds seconds - { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime } + let newTime := dt.time.addSeconds seconds + { dt with date := dt.date.addDays days, time := newTime } /-- Subtracts a `Second.Offset` from a `PlainDateTime`, adjusting the minute, hour, and date if the seconds underflow. @@ -380,10 +379,10 @@ Adds a `Millisecond.Offset` to a `PlainDateTime`, adjusting the second, minute, -/ @[inline] def addMilliseconds (dt : PlainDateTime) (milliseconds : Millisecond.Offset) : PlainDateTime := - let totalMilliseconds := dt.time.snd.toMilliseconds + milliseconds + let totalMilliseconds := dt.time.toMilliseconds + milliseconds let days := totalMilliseconds.ediv 86400000 -- 86400000 ms in a day - let newTime := dt.time.snd.addMilliseconds milliseconds - { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime } + let newTime := dt.time.addMilliseconds milliseconds + { dt with date := dt.date.addDays days, time := newTime } /-- Subtracts a `Millisecond.Offset` from a `PlainDateTime`, adjusting the second, minute, hour, and date if the milliseconds underflow. @@ -397,12 +396,12 @@ Adds a `Nanosecond.Offset` to a `PlainDateTime`, adjusting the seconds, minutes, -/ @[inline] def addNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime := - let nano := Nanosecond.Offset.ofInt dt.time.snd.nanosecond.val + 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.snd.addSeconds extraSeconds - { dt with time := Sigma.mk dt.time.fst { newTime with nanosecond } } + 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. @@ -444,35 +443,35 @@ Getter for the `Hour` inside of a `PlainDateTime`. -/ @[inline] def hour (dt : PlainDateTime) : Hour.Ordinal := - dt.time.snd.hour + dt.time.hour /-- Getter for the `Minute` inside of a `PlainDateTime`. -/ @[inline] def minute (dt : PlainDateTime) : Minute.Ordinal := - dt.time.snd.minute + dt.time.minute /-- Getter for the `Millisecond` inside of a `PlainDateTime`. -/ @[inline] def millisecond (dt : PlainDateTime) : Millisecond.Ordinal := - dt.time.snd.millisecond + dt.time.millisecond /-- Getter for the `Second` inside of a `PlainDateTime`. -/ @[inline] -def second (dt : PlainDateTime) : Second.Ordinal dt.time.fst := - dt.time.snd.second +def second (dt : PlainDateTime) : Second.Ordinal true := + dt.time.second /-- Getter for the `Nanosecond.Ordinal` inside of a `PlainDateTime`. -/ @[inline] def nanosecond (dt : PlainDateTime) : Nanosecond.Ordinal := - dt.time.snd.nanosecond + dt.time.nanosecond /-- Determines the era of the given `PlainDateTime` based on its year. @@ -528,15 +527,15 @@ def quarter (date : PlainDateTime) : Bounded.LE 1 4 := Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`. -/ @[inline] -def atTime : PlainDate → PlainTime leap → PlainDateTime := - (PlainDateTime.mk · <| Sigma.mk leap ·) +def atTime : PlainDate → PlainTime → PlainDateTime := + (PlainDateTime.mk · <| ·) /-- Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`. -/ @[inline] -def atDate (time: PlainTime leap) (date: PlainDate) : PlainDateTime := - PlainDateTime.mk date (Sigma.mk leap time) +def atDate (time: PlainTime) (date: PlainDate) : PlainDateTime := + PlainDateTime.mk date (time) instance : HAdd PlainDateTime Day.Offset PlainDateTime where hAdd := addDays @@ -590,8 +589,8 @@ namespace PlainDate Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`. -/ @[inline] -def atTime : PlainDate → PlainTime leap → PlainDateTime := - (PlainDateTime.mk · <| Sigma.mk leap ·) +def atTime : PlainDate → PlainTime → PlainDateTime := + PlainDateTime.mk end PlainDate namespace PlainTime @@ -600,8 +599,8 @@ namespace PlainTime Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`. -/ @[inline] -def atDate (time: PlainTime leap) (date: PlainDate) : PlainDateTime := - PlainDateTime.mk date (Sigma.mk leap time) +def atDate (time: PlainTime) (date: PlainDate) : PlainDateTime := + PlainDateTime.mk date time end PlainTime end Time diff --git a/src/Std/Time/Duration.lean b/src/Std/Time/Duration.lean index 51f828cca906..54d6d0364340 100644 --- a/src/Std/Time/Duration.lean +++ b/src/Std/Time/Duration.lean @@ -350,10 +350,10 @@ instance : HMul Int Duration Duration where instance : HMul Duration Int Duration where hMul d i := Duration.ofNanoseconds <| Nanosecond.Offset.ofInt (d.toNanoseconds.val * i) -instance : HAdd (PlainTime leap) Duration (PlainTime leap) where +instance : HAdd PlainTime Duration PlainTime where hAdd pt d := PlainTime.ofNanoseconds (d.toNanoseconds + pt.toNanoseconds) -instance : HSub (PlainTime leap) Duration (PlainTime leap) where +instance : HSub PlainTime Duration PlainTime where hSub pt d := PlainTime.ofNanoseconds (d.toNanoseconds - pt.toNanoseconds) end Duration diff --git a/src/Std/Time/Format.lean b/src/Std/Time/Format.lean index 1345fb368070..72efd2b17c39 100644 --- a/src/Std/Time/Format.lean +++ b/src/Std/Time/Format.lean @@ -254,7 +254,7 @@ namespace PlainTime /-- Formats a `PlainTime` using a specific format. -/ -def format (time : PlainTime leap) (format : String) : String := +def format (time : PlainTime) (format : String) : String := let format : Except String (GenericFormat .any) := GenericFormat.spec format match format with | .error err => s!"error: {err}" @@ -264,7 +264,7 @@ def format (time : PlainTime leap) (format : String) : String := | .k _ => some (time.hour.shiftTo1BasedHour) | .m _ => some time.minute | .n _ => some time.nanosecond - | .s _ => some (Sigma.mk leap time.second) + | .s _ => some time.second | .a _ => some (HourMarker.ofOrdinal time.hour) | .h _ => some time.hour.toRelative | .K _ => some (time.hour.emod 12 (by decide)) @@ -279,55 +279,55 @@ def format (time : PlainTime leap) (format : String) : String := /-- Parses a time string in the 24-hour format (`HH:mm:ss`) and returns a `PlainTime`. -/ -def fromTime24Hour (input : String) : Except String (Sigma PlainTime) := - Formats.time24Hour.parseBuilder (fun h m s => some (Sigma.mk s.fst (PlainTime.ofHourMinuteSeconds h m s.snd))) input +def fromTime24Hour (input : String) : Except String PlainTime := + Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s)) input /-- Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss`). -/ -def toTime24Hour (input : PlainTime leap) : String := - Formats.time24Hour.formatBuilder input.hour input.minute (Sigma.mk leap input.second) +def toTime24Hour (input : PlainTime) : String := + Formats.time24Hour.formatBuilder input.hour input.minute input.second /-- Parses a time string in the lean 24-hour format (`HH:mm:ss.SSSSSSSSS` or `HH:mm:ss`) and returns a `PlainTime`. -/ -def fromLeanTime24Hour (input : String) : Except String (Sigma PlainTime) := - Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| Sigma.mk s.fst (PlainTime.ofHourMinuteSecondsNano h m s.snd n)) input - <|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some <| Sigma.mk s.fst (PlainTime.ofHourMinuteSecondsNano h m s.snd 0)) input +def fromLeanTime24Hour (input : String) : Except String PlainTime := + Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| PlainTime.ofHourMinuteSecondsNano h m s n) input + <|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some <| PlainTime.ofHourMinuteSecondsNano h m s 0) input /-- Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss.SSSSSSSSS`). -/ -def toLeanTime24Hour (input : PlainTime leap) : String := - Formats.leanTime24Hour.formatBuilder input.hour input.minute (Sigma.mk leap input.second) input.nanosecond +def toLeanTime24Hour (input : PlainTime) : String := + Formats.leanTime24Hour.formatBuilder input.hour input.minute input.second input.nanosecond /-- Parses a time string in the 12-hour format (`hh:mm:ss aa`) and returns a `PlainTime`. -/ -def fromTime12Hour (input : String) : Except String (Sigma PlainTime) := do - let builder h m s a : Option (Sigma PlainTime) := do +def fromTime12Hour (input : String) : Except String PlainTime := do + let builder h m s a : Option PlainTime := do let value ← Internal.Bounded.ofInt? h.val - some <| Sigma.mk s.fst <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s.snd + some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s Formats.time12Hour.parseBuilder builder input /-- Formats a `PlainTime` value into a 12-hour format string (`hh:mm:ss aa`). -/ -def toTime12Hour (input : PlainTime leap) : String := - Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute (Sigma.mk leap input.second) (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am) +def toTime12Hour (input : PlainTime) : String := + Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute input.second (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am) /-- Parses a `String` in the `Time12Hour` or `Time24Hour` format and returns a `PlainTime`. -/ -def parse (input : String) : Except String (Sigma PlainTime) := +def parse (input : String) : Except String PlainTime := fromTime12Hour input <|> fromTime24Hour input -instance : ToString (PlainTime leap) where +instance : ToString PlainTime where toString := toLeanTime24Hour -instance : Repr (PlainTime leap) where +instance : Repr PlainTime where reprPrec data := Repr.addAppParen ("time(\"" ++ toLeanTime24Hour data ++ "\")") end PlainTime @@ -409,12 +409,12 @@ def fromLeanDateTimeWithIdentifierString (input : String) : Except String ZonedD Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation. -/ def toLeanDateTimeWithZoneString (zdt : ZonedDateTime) : String := - Formats.leanDateTimeWithZone.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute (Sigma.mk zdt.date.get.time.fst zdt.date.get.time.snd.second) zdt.nanosecond zdt.offset + Formats.leanDateTimeWithZone.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.offset /-- Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation with the timezone identifier. -/ def toLeanDateTimeWithIdentifierString (zdt : ZonedDateTime) : String := - Formats.leanDateTimeWithIdentifierAndNanos.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute (Sigma.mk zdt.date.get.time.fst zdt.date.get.time.snd.second) zdt.nanosecond zdt.timezone.name + Formats.leanDateTimeWithIdentifierAndNanos.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.timezone.name /-- Parses a `String` in the `ISO8601`, `RFC822` or `RFC850` format and returns a `ZonedDateTime`. @@ -461,13 +461,13 @@ def format (date : PlainDateTime) (format : String) : String := | .k _ => some date.hour.shiftTo1BasedHour | .m _ => some date.minute | .n _ => some date.nanosecond - | .s _ => some (Sigma.mk date.time.fst date.time.snd.second) + | .s _ => some date.time.second | .a _ => some (HourMarker.ofOrdinal date.hour) | .h _ => some date.hour.toRelative | .K _ => some (date.hour.emod 12 (by decide)) | .S _ => some date.nanosecond - | .A _ => some date.time.snd.toMilliseconds - | .N _ => some date.time.snd.toNanoseconds + | .A _ => some date.time.toMilliseconds + | .N _ => some date.time.toNanoseconds | _ => none match res with | some res => res @@ -510,7 +510,7 @@ def fromDateTimeString (input : String) : Except String PlainDateTime := Formats a `PlainDateTime` value into a `DateTime` format string. -/ def toDateTimeString (pdt : PlainDateTime) : String := - Formats.dateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute (Sigma.mk pdt.time.fst pdt.time.snd.second) pdt.nanosecond + Formats.dateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond /-- Parses a `String` in the `DateTime` format and returns a `PlainDateTime`. @@ -523,7 +523,7 @@ def fromLeanDateTimeString (input : String) : Except String PlainDateTime := Formats a `PlainDateTime` value into a `DateTime` format string. -/ def toLeanDateTimeString (pdt : PlainDateTime) : String := - Formats.leanDateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute (Sigma.mk pdt.time.fst pdt.time.snd.second) pdt.nanosecond + Formats.leanDateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond /-- Parses a `String` in the `AscTime` or `LongDate` format and returns a `PlainDateTime`. diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean index b3941bb446ee..b0d302481965 100644 --- a/src/Std/Time/Format/Basic.lean +++ b/src/Std/Time/Format/Basic.lean @@ -764,7 +764,7 @@ private def TypeFormat : Modifier → Type | .k _ => Bounded.LE 1 24 | .H _ => Hour.Ordinal | .m _ => Minute.Ordinal - | .s _ => Sigma Second.Ordinal + | .s _ => Second.Ordinal true | .S _ => Nanosecond.Ordinal | .A _ => Millisecond.Offset | .n _ => Nanosecond.Ordinal @@ -835,10 +835,10 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin | .narrow => formatMarkerNarrow data | .h format => pad format.padding (data.val % 12) | .K format => pad format.padding (data.val % 12) - | .k format => pad format.padding (data.val) - | .H format => pad format.padding (data.val) - | .m format => pad format.padding (data.val) - | .s format => pad format.padding (data.snd.val) + | .k format => pad format.padding data.val + | .H format => pad format.padding data.val + | .m format => pad format.padding data.val + | .s format => pad format.padding data.val | .S format => match format with | .nano => pad 9 data.val @@ -913,11 +913,11 @@ private def dateFromModifier (date : DateTime tz) : TypeFormat modifier := | .k _ => date.hour.shiftTo1BasedHour | .H _ => date.hour | .m _ => date.minute - | .s _ => Sigma.mk date.date.get.time.fst date.date.get.time.snd.second + | .s _ => date.date.get.time.second | .S _ => date.nanosecond - | .A _ => date.date.get.time.snd.toMilliseconds + | .A _ => date.date.get.time.toMilliseconds | .n _ => date.nanosecond - | .N _ => date.date.get.time.snd.toNanoseconds + | .N _ => date.date.get.time.toNanoseconds | .V => tz.name | .z .short => tz.abbreviation | .z .full => tz.name @@ -1167,7 +1167,7 @@ private def parseWith : (mod : Modifier) → Parser (TypeFormat mod) | .k format => parseNatToBounded (parseAtLeastNum format.padding) | .H format => parseNatToBounded (parseAtLeastNum format.padding) | .m format => parseNatToBounded (parseAtLeastNum format.padding) - | .s format => Sigma.mk true <$> (parseNatToBounded (parseAtLeastNum format.padding)) + | .s format => parseNatToBounded (parseAtLeastNum format.padding) | .S format => match format with | .nano => parseNatToBounded (parseAtLeastNum 9) @@ -1249,7 +1249,7 @@ private structure DateBuilder where k : Option (Bounded.LE 1 24) := none H : Option Hour.Ordinal := none m : Option Minute.Ordinal := none - s : Option (Sigma Second.Ordinal) := none + s : Option (Second.Ordinal true) := none S : Option Nanosecond.Ordinal := none A : Option Millisecond.Offset := none n : Option Nanosecond.Ordinal := none @@ -1335,18 +1335,18 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type := |>.getD ⟨0, by decide⟩ let minute := builder.m |>.getD 0 - let second := builder.s |>.getD ⟨false, 0⟩ + let second := builder.s |>.getD 0 let nano := (builder.n <|> builder.S) |>.getD 0 - let time : PlainTime second.fst + let time := PlainTime.ofNanoseconds <$> builder.N <|> PlainTime.ofMilliseconds <$> builder.A - |>.getD (PlainTime.mk hour minute second.snd nano) + |>.getD (PlainTime.mk hour minute second nano) let datetime : Option PlainDateTime := if valid : year.Valid month day then let date : PlainDate := { year, month, day, valid } - some { date, time := Sigma.mk second.fst time } + some { date, time } else none diff --git a/src/Std/Time/Notation.lean b/src/Std/Time/Notation.lean index bdf39a69e834..d59f9588dba6 100644 --- a/src/Std/Time/Notation.lean +++ b/src/Std/Time/Notation.lean @@ -125,11 +125,11 @@ private def convertTimezone (tz : Std.Time.TimeZone) : MacroM (TSyntax `term) := private def convertPlainDate (d : Std.Time.PlainDate) : MacroM (TSyntax `term) := do `(Std.Time.PlainDate.ofYearMonthDayClip $(← syntaxInt d.year) $(← syntaxBounded d.month.val) $(← syntaxBounded d.day.val)) -private def convertPlainTime (d : Std.Time.PlainTime leap) : MacroM (TSyntax `term) := do +private def convertPlainTime (d : Std.Time.PlainTime) : MacroM (TSyntax `term) := do `(Std.Time.PlainTime.mk $(← syntaxBounded d.hour.val) $(← syntaxBounded d.minute.val) $(← syntaxBounded d.second.val) $(← syntaxBounded d.nanosecond.val)) private def convertPlainDateTime (d : Std.Time.PlainDateTime) : MacroM (TSyntax `term) := do - `(Std.Time.PlainDateTime.mk $(← convertPlainDate d.date) (Sigma.mk true $(← convertPlainTime (d.time.snd)))) + `(Std.Time.PlainDateTime.mk $(← convertPlainDate d.date) $(← convertPlainTime d.time)) private def convertZonedDateTime (d : Std.Time.ZonedDateTime) (identifier := false) : MacroM (TSyntax `term) := do let plain ← convertPlainDateTime d.toPlainDateTime @@ -232,7 +232,7 @@ macro_rules | `(time( $time:str )) => do match PlainTime.fromLeanTime24Hour time.getString with - | .ok res => return ← convertPlainTime res.snd + | .ok res => return ← convertPlainTime res | .error res => Macro.throwErrorAt time s!"error: {res}" | `(offset( $offset:str )) => do diff --git a/src/Std/Time/Time/PlainTime.lean b/src/Std/Time/Time/PlainTime.lean index 7ce514c801d7..aae20957f860 100644 --- a/src/Std/Time/Time/PlainTime.lean +++ b/src/Std/Time/Time/PlainTime.lean @@ -15,7 +15,7 @@ set_option linter.all true /-- Represents a specific point in a day, including hours, minutes, seconds, and nanoseconds. -/ -structure PlainTime (leap : Bool) where +structure PlainTime where /-- `Hour` component of the `PlainTime` @@ -30,7 +30,7 @@ structure PlainTime (leap : Bool) where /-- `Second` component of the `PlainTime` -/ - second : Second.Ordinal leap + second : Second.Ordinal true /-- `Nanoseconds` component of the `PlainTime` @@ -41,12 +41,12 @@ structure PlainTime (leap : Bool) where /-- Defines `LeapTime` as a shorthand for a `PlainTime` that can contain leap seconds. -/ -abbrev LeapTime := PlainTime true +abbrev LeapTime := PlainTime -instance : Inhabited (PlainTime x) where +instance : Inhabited PlainTime where default := ⟨0, 0, 0, 0, by decide⟩ -instance : BEq (PlainTime x) where +instance : BEq PlainTime where beq x y := x.hour.val == y.hour.val && x.minute == y.minute && x.second.val == y.second.val && x.nanosecond == y.nanosecond @@ -55,27 +55,27 @@ namespace PlainTime /-- Creates a `PlainTime` value representing midnight (00:00:00.000000000). -/ -def midnight : PlainTime leap := +def midnight : PlainTime := ⟨0, 0, 0, 0⟩ /-- Creates a `PlainTime` value from the provided hours, minutes, seconds and nanoseconds components. -/ @[inline] -def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) (nano : Nanosecond.Ordinal) : PlainTime leap := +def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) (nano : Nanosecond.Ordinal) : PlainTime := ⟨hour, minute, second, nano⟩ /-- Creates a `PlainTime` value from the provided hours, minutes, and seconds. -/ @[inline] -def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) : PlainTime leap := +def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) : PlainTime := ofHourMinuteSecondsNano hour minute second 0 /-- Converts a `PlainTime` value to the total number of milliseconds. -/ -def toMilliseconds (time : PlainTime leap) : Millisecond.Offset := +def toMilliseconds (time : PlainTime) : Millisecond.Offset := time.hour.toOffset.toMilliseconds + time.minute.toOffset.toMilliseconds + time.second.toOffset.toMilliseconds + @@ -84,7 +84,7 @@ def toMilliseconds (time : PlainTime leap) : Millisecond.Offset := /-- Converts a `PlainTime` value to the total number of nanoseconds. -/ -def toNanoseconds (time : PlainTime leap) : Nanosecond.Offset := +def toNanoseconds (time : PlainTime) : Nanosecond.Offset := time.hour.toOffset.toNanoseconds + time.minute.toOffset.toNanoseconds + time.second.toOffset.toNanoseconds + @@ -93,7 +93,7 @@ def toNanoseconds (time : PlainTime leap) : Nanosecond.Offset := /-- Converts a `PlainTime` value to the total number of seconds. -/ -def toSeconds (time : PlainTime leap) : Second.Offset := +def toSeconds (time : PlainTime) : Second.Offset := time.hour.toOffset.toSeconds + time.minute.toOffset.toSeconds + time.second.toOffset @@ -101,7 +101,7 @@ def toSeconds (time : PlainTime leap) : Second.Offset := /-- Converts a `PlainTime` value to the total number of minutes. -/ -def toMinutes (time : PlainTime leap) : Minute.Offset := +def toMinutes (time : PlainTime) : Minute.Offset := time.hour.toOffset.toMinutes + time.minute.toOffset + time.second.toOffset.toMinutes @@ -109,24 +109,20 @@ def toMinutes (time : PlainTime leap) : Minute.Offset := /-- Converts a `PlainTime` value to the total number of hours. -/ -def toHours (time : PlainTime leap) : Hour.Offset := +def toHours (time : PlainTime) : Hour.Offset := time.hour.toOffset /-- Creates a `PlainTime` value from a total number of nanoseconds. -/ -def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime leap := +def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime := have totalSeconds := nanos.ediv 1000000000 have remainingNanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide) have hours := Bounded.LE.byEmod (totalSeconds.val / 3600) 24 (by decide) have minutes := (Bounded.LE.byEmod totalSeconds.val 3600 (by decide)).ediv 60 (by decide) have seconds := Bounded.LE.byEmod totalSeconds.val 60 (by decide) - - have seconds := - match leap with - | true => seconds.expandTop (by decide) - | false => seconds + have seconds := seconds.expandTop (by decide) let nanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide) PlainTime.mk hours minutes seconds nanos @@ -135,35 +131,35 @@ def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime leap := Creates a `PlainTime` value from a total number of millisecond. -/ @[inline] -def ofMilliseconds (millis : Millisecond.Offset) : PlainTime leap := +def ofMilliseconds (millis : Millisecond.Offset) : PlainTime := ofNanoseconds millis.toNanoseconds /-- Creates a `PlainTime` value from a total number of seconds. -/ @[inline] -def ofSeconds (secs : Second.Offset) : PlainTime leap := +def ofSeconds (secs : Second.Offset) : PlainTime := ofNanoseconds secs.toNanoseconds /-- Creates a `PlainTime` value from a total number of minutes. -/ @[inline] -def ofMinutes (secs : Minute.Offset) : PlainTime leap := +def ofMinutes (secs : Minute.Offset) : PlainTime := ofNanoseconds secs.toNanoseconds /-- Creates a `PlainTime` value from a total number of hours. -/ @[inline] -def ofHours (hour : Hour.Offset) : PlainTime leap := +def ofHours (hour : Hour.Offset) : PlainTime := ofNanoseconds hour.toNanoseconds /-- Adds seconds to a `PlainTime`. -/ @[inline] -def addSeconds (time : PlainTime leap) (secondsToAdd : Second.Offset) : PlainTime leap := +def addSeconds (time : PlainTime) (secondsToAdd : Second.Offset) : PlainTime := let totalSeconds := time.toNanoseconds + secondsToAdd.toNanoseconds ofNanoseconds totalSeconds @@ -171,14 +167,14 @@ def addSeconds (time : PlainTime leap) (secondsToAdd : Second.Offset) : PlainTim Subtracts seconds from a `PlainTime`. -/ @[inline] -def subSeconds (time : PlainTime leap) (secondsToSub : Second.Offset) : PlainTime leap := +def subSeconds (time : PlainTime) (secondsToSub : Second.Offset) : PlainTime := addSeconds time (-secondsToSub) /-- Adds minutes to a `PlainTime`. -/ @[inline] -def addMinutes (time : PlainTime leap) (minutesToAdd : Minute.Offset) : PlainTime leap := +def addMinutes (time : PlainTime) (minutesToAdd : Minute.Offset) : PlainTime := let total := time.toNanoseconds + minutesToAdd.toNanoseconds ofNanoseconds total @@ -186,14 +182,14 @@ def addMinutes (time : PlainTime leap) (minutesToAdd : Minute.Offset) : PlainTim Subtracts minutes from a `PlainTime`. -/ @[inline] -def subMinutes (time : PlainTime leap) (minutesToSub : Minute.Offset) : PlainTime leap := +def subMinutes (time : PlainTime) (minutesToSub : Minute.Offset) : PlainTime := addMinutes time (-minutesToSub) /-- Adds hours to a `PlainTime`. -/ @[inline] -def addHours (time : PlainTime leap) (hoursToAdd : Hour.Offset) : PlainTime leap := +def addHours (time : PlainTime) (hoursToAdd : Hour.Offset) : PlainTime := let total := time.toNanoseconds + hoursToAdd.toNanoseconds ofNanoseconds total @@ -201,54 +197,54 @@ def addHours (time : PlainTime leap) (hoursToAdd : Hour.Offset) : PlainTime leap Subtracts hours from a `PlainTime`. -/ @[inline] -def subHours (time : PlainTime leap) (hoursToSub : Hour.Offset) : PlainTime leap := +def subHours (time : PlainTime) (hoursToSub : Hour.Offset) : PlainTime := addHours time (-hoursToSub) /-- Adds nanoseconds to a `PlainTime`. -/ -def addNanoseconds (time : PlainTime leap) (nanosToAdd : Nanosecond.Offset) : PlainTime leap := +def addNanoseconds (time : PlainTime) (nanosToAdd : Nanosecond.Offset) : PlainTime := let total := time.toNanoseconds + nanosToAdd ofNanoseconds total /-- Subtracts nanoseconds from a `PlainTime`. -/ -def subNanoseconds (time : PlainTime leap) (nanosToSub : Nanosecond.Offset) : PlainTime leap := +def subNanoseconds (time : PlainTime) (nanosToSub : Nanosecond.Offset) : PlainTime := addNanoseconds time (-nanosToSub) /-- Adds milliseconds to a `PlainTime`. -/ -def addMilliseconds (time : PlainTime leap) (millisToAdd : Millisecond.Offset) : PlainTime leap := +def addMilliseconds (time : PlainTime) (millisToAdd : Millisecond.Offset) : PlainTime := let total := time.toMilliseconds + millisToAdd ofMilliseconds total /-- Subtracts milliseconds from a `PlainTime`. -/ -def subMilliseconds (time : PlainTime leap) (millisToSub : Millisecond.Offset) : PlainTime leap := +def subMilliseconds (time : PlainTime) (millisToSub : Millisecond.Offset) : PlainTime := addMilliseconds time (-millisToSub) /-- Creates a new `PlainTime` by adjusting the `second` component to the given value. -/ @[inline] -def withSeconds (pt : PlainTime leap) (second : Second.Ordinal leap) : PlainTime leap := +def withSeconds (pt : PlainTime) (second : Second.Ordinal true) : PlainTime := { pt with second := second } /-- Creates a new `PlainTime` by adjusting the `minute` component to the given value. -/ @[inline] -def withMinutes (pt : PlainTime leap) (minute : Minute.Ordinal) : PlainTime leap := +def withMinutes (pt : PlainTime) (minute : Minute.Ordinal) : PlainTime := { pt with minute := minute } /-- Creates a new `PlainTime` by adjusting the milliseconds component inside the `nano` component of its `time` to the given value. -/ @[inline] -def withMilliseconds (pt : PlainTime leap) (millis : Millisecond.Ordinal) : PlainTime leap := +def withMilliseconds (pt : PlainTime) (millis : Millisecond.Ordinal) : PlainTime := let minorPart := pt.nanosecond.emod 1000 (by decide) let majorPart := millis.mul_pos 1000000 (by decide) |>.addBounds minorPart { pt with nanosecond := majorPart |>.expandTop (by decide) } @@ -257,51 +253,51 @@ def withMilliseconds (pt : PlainTime leap) (millis : Millisecond.Ordinal) : Plai Creates a new `PlainTime` by adjusting the `nano` component to the given value. -/ @[inline] -def withNanoseconds (pt : PlainTime leap) (nano : Nanosecond.Ordinal) : PlainTime leap := +def withNanoseconds (pt : PlainTime) (nano : Nanosecond.Ordinal) : PlainTime := { pt with nanosecond := nano } /-- Creates a new `PlainTime` by adjusting the `hour` component to the given value. -/ @[inline] -def withHours (pt : PlainTime leap) (hour : Hour.Ordinal) : PlainTime leap := +def withHours (pt : PlainTime) (hour : Hour.Ordinal) : PlainTime := { pt with hour := hour } /-- `Millisecond` component of the `PlainTime` -/ @[inline] -def millisecond (pt : PlainTime leap) : Millisecond.Ordinal := +def millisecond (pt : PlainTime) : Millisecond.Ordinal := pt.nanosecond.ediv 1000000 (by decide) -instance : HAdd (PlainTime leap) Nanosecond.Offset (PlainTime leap) where +instance : HAdd PlainTime Nanosecond.Offset PlainTime where hAdd := addNanoseconds -instance : HSub (PlainTime leap) Nanosecond.Offset (PlainTime leap) where +instance : HSub PlainTime Nanosecond.Offset PlainTime where hSub := subNanoseconds -instance : HAdd (PlainTime leap) Millisecond.Offset (PlainTime leap) where +instance : HAdd PlainTime Millisecond.Offset PlainTime where hAdd := addMilliseconds -instance : HSub (PlainTime leap) Millisecond.Offset (PlainTime leap) where +instance : HSub PlainTime Millisecond.Offset PlainTime where hSub := subMilliseconds -instance : HAdd (PlainTime leap) Second.Offset (PlainTime leap) where +instance : HAdd PlainTime Second.Offset PlainTime where hAdd := addSeconds -instance : HSub (PlainTime leap) Second.Offset (PlainTime leap) where +instance : HSub PlainTime Second.Offset PlainTime where hSub := subSeconds -instance : HAdd (PlainTime leap) Minute.Offset (PlainTime leap) where +instance : HAdd PlainTime Minute.Offset PlainTime where hAdd := addMinutes -instance : HSub (PlainTime leap) Minute.Offset (PlainTime leap) where +instance : HSub PlainTime Minute.Offset PlainTime where hSub := subMinutes -instance : HAdd (PlainTime leap) Hour.Offset (PlainTime leap) where +instance : HAdd PlainTime Hour.Offset PlainTime where hAdd := addHours -instance : HSub (PlainTime leap) Hour.Offset (PlainTime leap) where +instance : HSub PlainTime Hour.Offset PlainTime where hSub := subHours end PlainTime diff --git a/src/Std/Time/Time/Unit/Second.lean b/src/Std/Time/Time/Unit/Second.lean index 39c409f56056..4c4ef3cc5157 100644 --- a/src/Std/Time/Time/Unit/Second.lean +++ b/src/Std/Time/Time/Unit/Second.lean @@ -30,7 +30,7 @@ instance : LE (Ordinal leap) where instance : LT (Ordinal leap) where lt x y := LT.lt x.val y.val -instance : Repr (Ordinal l) where +instance : Repr (Ordinal leap) where reprPrec r := reprPrec r.val instance : OfNat (Ordinal leap) n := by @@ -39,10 +39,10 @@ instance : OfNat (Ordinal leap) n := by · exact inst · exact ⟨inst.ofNat.expandTop (by decide)⟩ -instance {x y : Ordinal l} : Decidable (x ≤ y) := +instance {x y : Ordinal leap} : Decidable (x ≤ y) := inferInstanceAs (Decidable (x.val ≤ y.val)) -instance {x y : Ordinal l} : Decidable (x < y) := +instance {x y : Ordinal leap} : Decidable (x < y) := inferInstanceAs (Decidable (x.val < y.val)) /-- diff --git a/src/Std/Time/Zoned.lean b/src/Std/Time/Zoned.lean index e1500adc6784..e01e19710090 100644 --- a/src/Std/Time/Zoned.lean +++ b/src/Std/Time/Zoned.lean @@ -45,7 +45,7 @@ namespace PlainTime Get the current time. -/ @[inline] -def now : IO (Sigma PlainTime) := do +def now : IO PlainTime := do let res ← PlainDateTime.time <$> PlainDateTime.now return res @@ -71,8 +71,8 @@ def toPlainDate (dt : DateTime tz) : PlainDate := Converts a `DateTime` to a `PlainTime` -/ @[inline] -def toPlainTime (dt : DateTime tz) : PlainTime dt.date.get.time.fst := - dt.date.get.time.snd +def toPlainTime (dt : DateTime tz) : PlainTime := + dt.date.get.time end DateTime namespace DateTime @@ -111,14 +111,14 @@ Converts a `PlainDate` to a `ZonedDateTime`. -/ @[inline] def ofPlainDate (pd : PlainDate) (zr : TimeZone.ZoneRules) : ZonedDateTime := - ZonedDateTime.ofPlainDateTime (pd.atTime (leap := true) PlainTime.midnight) zr + 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 (leap := true) PlainTime.midnight) (TimeZone.ZoneRules.ofTimeZone zr) + ZonedDateTime.ofPlainDateTime (pd.atTime PlainTime.midnight) (TimeZone.ZoneRules.ofTimeZone zr) /-- Converts a `ZonedDateTime` to a `PlainDate` @@ -131,7 +131,7 @@ def toPlainDate (dt : ZonedDateTime) : PlainDate := Converts a `ZonedDateTime` to a `PlainTime` -/ @[inline] -def toPlainTime (dt : ZonedDateTime) : Sigma PlainTime := +def toPlainTime (dt : ZonedDateTime) : PlainTime := dt.toPlainDateTime.time /-- diff --git a/src/Std/Time/Zoned/DateTime.lean b/src/Std/Time/Zoned/DateTime.lean index 2a743b921e7c..e016ba424d46 100644 --- a/src/Std/Time/Zoned/DateTime.lean +++ b/src/Std/Time/Zoned/DateTime.lean @@ -305,7 +305,7 @@ def withMinutes (dt : DateTime tz) (minute : Minute.Ordinal) : DateTime tz := Creates a new `DateTime tz` by adjusting the `second` component. -/ @[inline] -def withSeconds (dt : DateTime tz) (second : Second.Ordinal α) : DateTime tz := +def withSeconds (dt : DateTime tz) (second : Second.Ordinal true) : DateTime tz := ofPlainDateTime (dt.date.get.withSeconds second) tz /-- @@ -368,7 +368,7 @@ def minute (dt : DateTime tz) : Minute.Ordinal := Getter for the `Second` inside of a `DateTime` -/ @[inline] -def second (dt : DateTime tz) : Second.Ordinal dt.date.get.time.fst := +def second (dt : DateTime tz) : Second.Ordinal true := dt.date.get.second /-- @@ -376,14 +376,14 @@ Getter for the `Milliseconds` inside of a `DateTime` -/ @[inline] def millisecond (dt : DateTime tz) : Millisecond.Ordinal := - dt.date.get.time.snd.nanosecond.emod 1000 (by decide) + dt.date.get.time.nanosecond.emod 1000 (by decide) /-- Getter for the `Nanosecond` inside of a `DateTime` -/ @[inline] def nanosecond (dt : DateTime tz) : Nanosecond.Ordinal := - dt.date.get.time.snd.nanosecond + dt.date.get.time.nanosecond /-- Gets the `Weekday` of a DateTime. @@ -449,14 +449,14 @@ def quarter (date : DateTime tz) : Bounded.LE 1 4 := Getter for the `PlainTime` inside of a `DateTime` -/ @[inline] -def time (zdt : DateTime tz) : PlainTime zdt.date.get.time.fst := - zdt.date.get.time.snd +def time (zdt : DateTime tz) : PlainTime := + zdt.date.get.time /-- Converts a `DateTime` to the number of days since the UNIX epoch. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime leap) (tz : TimeZone) : DateTime tz := +def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (tz : TimeZone) : DateTime tz := DateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) tz instance : HAdd (DateTime tz) (Day.Offset) (DateTime tz) where diff --git a/src/Std/Time/Zoned/ZonedDateTime.lean b/src/Std/Time/Zoned/ZonedDateTime.lean index fed4c5680a64..42e446801657 100644 --- a/src/Std/Time/Zoned/ZonedDateTime.lean +++ b/src/Std/Time/Zoned/ZonedDateTime.lean @@ -137,8 +137,8 @@ def toDateTime (dt : ZonedDateTime) : DateTime dt.timezone := Getter for the `PlainTime` inside of a `ZonedDateTime` -/ @[inline] -def time (zdt : ZonedDateTime) : PlainTime zdt.date.get.time.fst := - zdt.date.get.time.snd +def time (zdt : ZonedDateTime) : PlainTime := + zdt.date.get.time /-- Getter for the `Year` inside of a `ZonedDateTime` @@ -166,7 +166,7 @@ Getter for the `Hour` inside of a `ZonedDateTime` -/ @[inline] def hour (zdt : ZonedDateTime) : Hour.Ordinal := - zdt.date.get.time.snd.hour + zdt.date.get.time.hour /-- Getter for the `Minute` inside of a `ZonedDateTime` @@ -179,22 +179,22 @@ def minute (zdt : ZonedDateTime) : Minute.Ordinal := Getter for the `Second` inside of a `ZonedDateTime` -/ @[inline] -def second (zdt : ZonedDateTime) : Second.Ordinal zdt.date.get.time.fst := - zdt.date.get.time.snd.second +def second (zdt : ZonedDateTime) : Second.Ordinal true := + zdt.date.get.time.second /-- Getter for the `Millisecond` inside of a `ZonedDateTime`. -/ @[inline] def millisecond (dt : ZonedDateTime) : Millisecond.Ordinal := - dt.date.get.time.snd.millisecond + dt.date.get.time.millisecond /-- Getter for the `Nanosecond` inside of a `ZonedDateTime` -/ @[inline] def nanosecond (zdt : ZonedDateTime) : Nanosecond.Ordinal := - zdt.date.get.time.snd.nanosecond + zdt.date.get.time.nanosecond /-- Getter for the `TimeZone.Offset` inside of a `ZonedDateTime` @@ -491,9 +491,9 @@ def withMinutes (dt : ZonedDateTime) (minute : Minute.Ordinal) : ZonedDateTime : Creates a new `ZonedDateTime` by adjusting the `second` component. -/ @[inline] -def withSeconds (dt : ZonedDateTime) (second : Sigma Second.Ordinal) : ZonedDateTime := +def withSeconds (dt : ZonedDateTime) (second : Second.Ordinal true) : ZonedDateTime := let date := dt.date.get - ZonedDateTime.ofPlainDateTime (date.withSeconds second.snd) dt.rules + ZonedDateTime.ofPlainDateTime (date.withSeconds second) dt.rules /-- Creates a new `ZonedDateTime` by adjusting the `nano` component with a new `millis` that will set @@ -528,7 +528,7 @@ def toDaysSinceUNIXEpoch (date : ZonedDateTime) : Day.Offset := Converts a `ZonedDateTime` to the number of days since the UNIX epoch. -/ @[inline] -def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime leap) (zt : TimeZone.ZoneRules) : ZonedDateTime := +def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (zt : TimeZone.ZoneRules) : ZonedDateTime := ZonedDateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) zt instance : HAdd ZonedDateTime Day.Offset ZonedDateTime where diff --git a/tests/lean/run/timeAPI.lean b/tests/lean/run/timeAPI.lean index 7e311b489850..a23d13f9166a 100644 --- a/tests/lean/run/timeAPI.lean +++ b/tests/lean/run/timeAPI.lean @@ -493,7 +493,7 @@ example : Week.Offset.ofNat 1 = (1 : Week.Offset) := rfl example := Nanosecond.Ordinal.ofInt 1 (by decide) example := Millisecond.Ordinal.ofInt 1 (by decide) example := Second.Ordinal.ofInt (leap := false) 59 (by decide) -example := Second.Ordinal.ofInt (leap := true) 60 (by decide) +example := Second.Ordinal.ofInt (leap := True) 60 (by decide) example := Minute.Ordinal.ofInt 1 (by decide) example := Hour.Ordinal.ofInt 1 (by decide) example := Day.Ordinal.ofInt 1 (by decide) @@ -502,7 +502,7 @@ example := Week.Ordinal.ofInt 1 (by decide) example := Nanosecond.Ordinal.ofFin 1 example := Millisecond.Ordinal.ofFin 1 example := Second.Ordinal.ofFin (leap := false) 37 -example := Second.Ordinal.ofFin (leap := true) 37 +example := Second.Ordinal.ofFin (leap := True) 37 example := Minute.Ordinal.ofFin 1 example := Hour.Ordinal.ofFin 1 example := Day.Ordinal.ofFin 1 @@ -511,7 +511,7 @@ example := Week.Ordinal.ofFin 1 example := Nanosecond.Ordinal.ofNat 1 example := Millisecond.Ordinal.ofNat 1 example := Second.Ordinal.ofNat (leap := false) 1 -example := Second.Ordinal.ofNat (leap := true) 1 +example := Second.Ordinal.ofNat (leap := True) 1 example := Minute.Ordinal.ofNat 1 example := Hour.Ordinal.ofNat 1 example := Day.Ordinal.ofNat 1 @@ -520,7 +520,7 @@ example := Week.Ordinal.ofNat 1 example := Nanosecond.Ordinal.toOffset 1 example := Millisecond.Ordinal.toOffset 1 example := Second.Ordinal.toOffset (leap := false) 1 -example := Second.Ordinal.toOffset (leap := true) 1 +example := Second.Ordinal.toOffset (leap := True) 1 example := Minute.Ordinal.toOffset 1 example := Hour.Ordinal.toOffset 1 example := Day.Ordinal.toOffset 1 @@ -709,7 +709,7 @@ Std.Time.Weekday.tuesday println! plaindatetime.toDaysSinceUNIXEpoch println! plaindatetime.toTimestampAssumingUTC - println! PlainDateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight + println! PlainDateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight /-- info: 2024-09-13T02:01:02.000000000-03:00 @@ -783,7 +783,7 @@ Std.Time.Weekday.thursday println! zoned.toDaysSinceUNIXEpoch println! zoned.toTimestamp - println! DateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight .UTC + println! DateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC /-- info: 1997-03-19T02:03:04.000000000[America/Sao_Paulo] @@ -867,8 +867,8 @@ info: 2023-06-09T00:00:00.000000000 #guard_msgs in #eval do println! PlainDateTime.ofPlainDate date("2023-06-09") - println! PlainDateTime.ofPlainTime (leap := True) time("12:32:43") - println! PlainDateTime.ofDaysSinceUNIXEpoch (leap := True) 23332 time("12:32:43") + println! PlainDateTime.ofPlainTime time("12:32:43") + println! PlainDateTime.ofDaysSinceUNIXEpoch 23332 time("12:32:43") /-- info: 1970-01-02T00:00:00.000000000Z @@ -880,7 +880,7 @@ info: 1970-01-02T00:00:00.000000000Z -/ #guard_msgs in #eval do - println! DateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight .UTC + println! DateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC println! DateTime.ofPlainDate 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 @@ -898,7 +898,7 @@ info: 1970-01-02T00:00:00.000000000[UTC] -/ #guard_msgs in #eval do - println! ZonedDateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight .UTC + 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.ofPlainDateTime datetime("1997-03-18T00:01:02") .UTC diff --git a/tests/lean/run/timeFormats.lean b/tests/lean/run/timeFormats.lean index 930889fd3afe..1d2d0c9607ec 100644 --- a/tests/lean/run/timeFormats.lean +++ b/tests/lean/run/timeFormats.lean @@ -178,9 +178,9 @@ info: "Monday, June 16, 2014 03:03:03 -0300" info: "14:11:01" -/ #guard_msgs in -#eval Time24Hour.formatBuilder time₁.hour time₁.minute ⟨true, time₁.second⟩ +#eval Time24Hour.formatBuilder time₁.hour time₁.minute time₁.second -def l := Time12Hour.formatBuilder time₁.hour.toRelative time₁.minute ⟨true, time₁.second⟩ (if time₁.hour.val > 12 then HourMarker.pm else HourMarker.am) +def l := Time12Hour.formatBuilder time₁.hour.toRelative time₁.minute time₁.second (if time₁.hour.val > 12 then HourMarker.pm else HourMarker.am) /-- info: "02:11:01 PM" @@ -191,7 +191,7 @@ info: "02:11:01 PM" info: "03:11:01 AM" -/ #guard_msgs in -#eval Time12Hour.formatBuilder time₂.hour.toRelative time₂.minute ⟨true, time₂.second⟩ (if time₂.hour.val > 12 then HourMarker.pm else HourMarker.am) +#eval Time12Hour.formatBuilder time₂.hour.toRelative time₂.minute time₂.second (if time₂.hour.val > 12 then HourMarker.pm else HourMarker.am) /-- info: "06/16/2014" @@ -277,7 +277,7 @@ Format def time₄ := (time("23:13:12.324354679") : LeapTime ) def date₄ := date("2002-07-14") -def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (Sigma.mk true <| PlainTime.mk 12 23 12 0) +def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (PlainTime.mk 12 23 12 0) def datetime₄ := datetime("2002-07-14T23:13:12.324354679") def zoned₄ := zoned("2002-07-14T23:13:12.324354679+09:00") def zoned₅ := zoned("2002-07-14T23:13:12.324354679+00:00") @@ -806,7 +806,7 @@ info: ("19343232432-01-04T01:04:03.000000000", -/ #guard_msgs in #eval - let r := (PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (Sigma.mk true <| PlainTime.mk 25 64 3 0)) + let r := PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (PlainTime.mk 25 64 3 0) let s := r.toLeanDateTimeString let r := PlainDateTime.parse s (s, r, datetime("1932-01-02T05:04:03.000000000")) diff --git a/tests/lean/run/timeLocalDateTime.lean b/tests/lean/run/timeLocalDateTime.lean index 6da164c55639..ad2521a85ab3 100644 --- a/tests/lean/run/timeLocalDateTime.lean +++ b/tests/lean/run/timeLocalDateTime.lean @@ -5,7 +5,7 @@ open Std.Time def ShortDateTime : GenericFormat .any := datespec("dd/MM/uuuu HH:mm:ss") def ShortDate : GenericFormat .any := datespec("dd/MM/uuuu") -def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.snd.hour PlainDate.minute ⟨PlainDate.time.fst, PlainDate.time.snd.second⟩ +def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.hour PlainDate.minute PlainDate.time.second def format₂ (PlainDate : PlainDate) : String := ShortDate.formatBuilder PlainDate.day PlainDate.month PlainDate.year diff --git a/tests/lean/run/timeSet.lean b/tests/lean/run/timeSet.lean index 23b165273438..581e6f08c381 100644 --- a/tests/lean/run/timeSet.lean +++ b/tests/lean/run/timeSet.lean @@ -91,7 +91,7 @@ info: zoned("2014-06-16T10:03:03.000000000-03:00") info: zoned("2014-06-16T10:03:59.000000000-03:00") -/ #guard_msgs in -#eval date₁.withSeconds ⟨true, 59⟩ +#eval date₁.withSeconds 59 /-- info: zoned("2014-06-16T10:03:03.000000002-03:00") From e21f70d770f704bd39c3d6848e1796786d2c9ecb Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Thu, 9 Jan 2025 18:56:21 -0300 Subject: [PATCH 12/17] feat: remove small diffs --- src/Std/Time/DateTime/PlainDateTime.lean | 8 ++++---- src/Std/Time/Format/Basic.lean | 2 +- tests/lean/run/timeClassOperations.lean | 2 +- tests/lean/run/timeFormats.lean | 8 ++++---- tests/lean/run/timeOperations.lean | 2 +- tests/lean/run/timeParse.lean | 4 ++-- tests/lean/run/timeSet.lean | 4 ++-- 7 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index d873635279fb..1c7b09f30afa 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -144,7 +144,7 @@ Converts a `PlainDateTime` to the number of days since the UNIX epoch. -/ @[inline] def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) : PlainDateTime := - PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) (time) + PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) time /-- Sets the `PlainDateTime` to the specified `desiredWeekday`. @@ -226,14 +226,14 @@ Creates a new `PlainDateTime` by adjusting the milliseconds component inside the -/ @[inline] def withMilliseconds (dt : PlainDateTime) (millis : Millisecond.Ordinal) : PlainDateTime := - { dt with time := (dt.time.withMilliseconds millis) } + { dt with time := dt.time.withMilliseconds millis } /-- Creates a new `PlainDateTime` by adjusting the `nano` component of its `time` to the given value. -/ @[inline] def withNanoseconds (dt : PlainDateTime) (nano : Nanosecond.Ordinal) : PlainDateTime := - { dt with time := (dt.time.withNanoseconds nano) } + { dt with time := dt.time.withNanoseconds nano } /-- Adds a `Day.Offset` to a `PlainDateTime`. @@ -528,7 +528,7 @@ Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`. -/ @[inline] def atTime : PlainDate → PlainTime → PlainDateTime := - (PlainDateTime.mk · <| ·) + PlainDateTime.mk /-- Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`. diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean index b0d302481965..7b14a3cc7c3f 100644 --- a/src/Std/Time/Format/Basic.lean +++ b/src/Std/Time/Format/Basic.lean @@ -736,7 +736,7 @@ private def toSigned (data : Int) : String := private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bool) (colon : Bool) : String := let (sign, time) := if offset.second.val ≥ 0 then ("+", offset.second) else ("-", -offset.second) - let time : LeapTime := PlainTime.ofSeconds time + let time := PlainTime.ofSeconds time let pad := leftPad 2 '0' ∘ toString let data := s!"{sign}{pad time.hour.val}" diff --git a/tests/lean/run/timeClassOperations.lean b/tests/lean/run/timeClassOperations.lean index c2d738a434ee..39f1967df911 100644 --- a/tests/lean/run/timeClassOperations.lean +++ b/tests/lean/run/timeClassOperations.lean @@ -65,7 +65,7 @@ info: datetime("2000-01-19T03:02:01.000000000") #guard_msgs in #eval datetime - (1 : Day.Offset) -def time : LeapTime := time("13:02:01") +def time := time("13:02:01") /-- info: time("14:02:01.000000000") diff --git a/tests/lean/run/timeFormats.lean b/tests/lean/run/timeFormats.lean index 1d2d0c9607ec..7eba5d5c274c 100644 --- a/tests/lean/run/timeFormats.lean +++ b/tests/lean/run/timeFormats.lean @@ -20,8 +20,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00") def date₁ := zoned("2014-06-16T03:03:03-03:00") -def time₁ : LeapTime := time("14:11:01") -def time₂ : LeapTime := time("03:11:01") +def time₁ := time("14:11:01") +def time₂ := time("03:11:01") /-- info: "Monday, June 16, 2014 03:03:03 -0300" @@ -245,7 +245,7 @@ info: date("2002-07-14") info: time("14:13:12.000000000") -/ #guard_msgs in -#eval (time("14:13:12") : LeapTime ) +#eval time("14:13:12") /-- info: zoned("2002-07-14T14:13:12.000000000Z") @@ -275,7 +275,7 @@ info: "14-13-12" Format -/ -def time₄ := (time("23:13:12.324354679") : LeapTime ) +def time₄ := (time("23:13:12.324354679") : PlainTime ) def date₄ := date("2002-07-14") def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (PlainTime.mk 12 23 12 0) def datetime₄ := datetime("2002-07-14T23:13:12.324354679") diff --git a/tests/lean/run/timeOperations.lean b/tests/lean/run/timeOperations.lean index 37fe808b8e95..2aee656f9121 100644 --- a/tests/lean/run/timeOperations.lean +++ b/tests/lean/run/timeOperations.lean @@ -131,7 +131,7 @@ info: datetime("1999-01-20T03:02:01.000000000") #guard_msgs in #eval datetime.subYearsRollOver 1 -def time : LeapTime := time("13:02:01") +def time := time("13:02:01") /-- info: time("14:02:01.000000000") diff --git a/tests/lean/run/timeParse.lean b/tests/lean/run/timeParse.lean index 72af186a45ed..fcd7b6be0b77 100644 --- a/tests/lean/run/timeParse.lean +++ b/tests/lean/run/timeParse.lean @@ -21,8 +21,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00") def date₁ := zoned("2014-06-16T03:03:03-03:00") -def time₁ : LeapTime := time("14:11:01") -def time₂ : LeapTime := time("03:11:01") +def time₁ := time("14:11:01") +def time₂ := time("03:11:01") /-- info: "2014-06-16T03:03:03.000000100-03:00" diff --git a/tests/lean/run/timeSet.lean b/tests/lean/run/timeSet.lean index 581e6f08c381..22339fb98ac8 100644 --- a/tests/lean/run/timeSet.lean +++ b/tests/lean/run/timeSet.lean @@ -21,8 +21,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00") def date₁ := zoned("2014-06-16T10:03:03-03:00") -def time₁ : LeapTime := time("14:11:01") -def time₂ : LeapTime := time("03:11:01") +def time₁ := time("14:11:01") +def time₂ := time("03:11:01") /-- info: "2014-06-16T10:03:03.000000100-03:00" From ed09e63e7508816b171b5d99771beafbe52125c9 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Thu, 9 Jan 2025 19:09:35 -0300 Subject: [PATCH 13/17] fix: small typos --- tests/lean/run/timeAPI.lean | 8 ++++---- tests/lean/run/timeFormats.lean | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/lean/run/timeAPI.lean b/tests/lean/run/timeAPI.lean index a23d13f9166a..8c99c1fc2624 100644 --- a/tests/lean/run/timeAPI.lean +++ b/tests/lean/run/timeAPI.lean @@ -493,7 +493,7 @@ example : Week.Offset.ofNat 1 = (1 : Week.Offset) := rfl example := Nanosecond.Ordinal.ofInt 1 (by decide) example := Millisecond.Ordinal.ofInt 1 (by decide) example := Second.Ordinal.ofInt (leap := false) 59 (by decide) -example := Second.Ordinal.ofInt (leap := True) 60 (by decide) +example := Second.Ordinal.ofInt (leap := true) 60 (by decide) example := Minute.Ordinal.ofInt 1 (by decide) example := Hour.Ordinal.ofInt 1 (by decide) example := Day.Ordinal.ofInt 1 (by decide) @@ -502,7 +502,7 @@ example := Week.Ordinal.ofInt 1 (by decide) example := Nanosecond.Ordinal.ofFin 1 example := Millisecond.Ordinal.ofFin 1 example := Second.Ordinal.ofFin (leap := false) 37 -example := Second.Ordinal.ofFin (leap := True) 37 +example := Second.Ordinal.ofFin (leap := true) 37 example := Minute.Ordinal.ofFin 1 example := Hour.Ordinal.ofFin 1 example := Day.Ordinal.ofFin 1 @@ -511,7 +511,7 @@ example := Week.Ordinal.ofFin 1 example := Nanosecond.Ordinal.ofNat 1 example := Millisecond.Ordinal.ofNat 1 example := Second.Ordinal.ofNat (leap := false) 1 -example := Second.Ordinal.ofNat (leap := True) 1 +example := Second.Ordinal.ofNat (leap := true) 1 example := Minute.Ordinal.ofNat 1 example := Hour.Ordinal.ofNat 1 example := Day.Ordinal.ofNat 1 @@ -520,7 +520,7 @@ example := Week.Ordinal.ofNat 1 example := Nanosecond.Ordinal.toOffset 1 example := Millisecond.Ordinal.toOffset 1 example := Second.Ordinal.toOffset (leap := false) 1 -example := Second.Ordinal.toOffset (leap := True) 1 +example := Second.Ordinal.toOffset (leap := true) 1 example := Minute.Ordinal.toOffset 1 example := Hour.Ordinal.toOffset 1 example := Day.Ordinal.toOffset 1 diff --git a/tests/lean/run/timeFormats.lean b/tests/lean/run/timeFormats.lean index 7eba5d5c274c..8c36f2c28464 100644 --- a/tests/lean/run/timeFormats.lean +++ b/tests/lean/run/timeFormats.lean @@ -275,7 +275,7 @@ info: "14-13-12" Format -/ -def time₄ := (time("23:13:12.324354679") : PlainTime ) +def time₄ := time("23:13:12.324354679") def date₄ := date("2002-07-14") def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (PlainTime.mk 12 23 12 0) def datetime₄ := datetime("2002-07-14T23:13:12.324354679") From 77e7d9618c922afe66b478e3f74d004ecf5d6e38 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 10 Jan 2025 19:20:54 -0300 Subject: [PATCH 14/17] fix: representaiton of timestamp --- src/Std/Time/DateTime/Timestamp.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Std/Time/DateTime/Timestamp.lean b/src/Std/Time/DateTime/Timestamp.lean index ff503ce59819..9986c26afd37 100644 --- a/src/Std/Time/DateTime/Timestamp.lean +++ b/src/Std/Time/DateTime/Timestamp.lean @@ -41,7 +41,7 @@ instance : ToString Timestamp where toString s := toString s.val.toSeconds instance : Repr Timestamp where - reprPrec s := reprPrec s.val.toSeconds + reprPrec s := Repr.addAppParen ("Timestamp.ofNanosecondsSinceUnixEpoch " ++ repr s.val.toNanoseconds) namespace Timestamp From 572bae9e67e8673d006e61b3a9c0d9fcb430d62f Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 10 Jan 2025 19:24:50 -0300 Subject: [PATCH 15/17] fix: small corrections to make the code better --- src/Std/Time/DateTime/PlainDateTime.lean | 10 ++-------- src/Std/Time/Time/PlainTime.lean | 5 ----- src/Std/Time/Zoned.lean | 5 ++--- 3 files changed, 4 insertions(+), 16 deletions(-) diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index 1c7b09f30afa..bbfe331812e1 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -30,13 +30,7 @@ structure PlainDateTime where -/ time : PlainTime - deriving Repr - -instance : Inhabited PlainDateTime where - default := { - date := Inhabited.default, - time := Inhabited.default - } + deriving Repr, Inhabited namespace PlainDateTime @@ -535,7 +529,7 @@ Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`. -/ @[inline] def atDate (time: PlainTime) (date: PlainDate) : PlainDateTime := - PlainDateTime.mk date (time) + PlainDateTime.mk date time instance : HAdd PlainDateTime Day.Offset PlainDateTime where hAdd := addDays diff --git a/src/Std/Time/Time/PlainTime.lean b/src/Std/Time/Time/PlainTime.lean index aae20957f860..cb299a60bd82 100644 --- a/src/Std/Time/Time/PlainTime.lean +++ b/src/Std/Time/Time/PlainTime.lean @@ -38,11 +38,6 @@ structure PlainTime where nanosecond : Nanosecond.Ordinal deriving Repr -/-- -Defines `LeapTime` as a shorthand for a `PlainTime` that can contain leap seconds. --/ -abbrev LeapTime := PlainTime - instance : Inhabited PlainTime where default := ⟨0, 0, 0, 0, by decide⟩ diff --git a/src/Std/Time/Zoned.lean b/src/Std/Time/Zoned.lean index e01e19710090..570007ce5ecb 100644 --- a/src/Std/Time/Zoned.lean +++ b/src/Std/Time/Zoned.lean @@ -45,9 +45,8 @@ namespace PlainTime Get the current time. -/ @[inline] -def now : IO PlainTime := do - let res ← PlainDateTime.time <$> PlainDateTime.now - return res +def now : IO PlainTime := + PlainDateTime.time <$> PlainDateTime.now end PlainTime From 4870cb155ee4f518522dafe98840b71956fbec05 Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 10 Jan 2025 19:31:55 -0300 Subject: [PATCH 16/17] revert: change in plaindatetime derivings --- src/Std/Time/DateTime/PlainDateTime.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index bbfe331812e1..dd6fc91cc785 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -30,7 +30,8 @@ structure PlainDateTime where -/ time : PlainTime - deriving Repr, Inhabited + deriving Inhabited, BEq, Repr + namespace PlainDateTime From c0a5e5badb5992fc813f4abda97c9cc8e6f63cbb Mon Sep 17 00:00:00 2001 From: Sofia Rodrigues Date: Fri, 10 Jan 2025 19:46:21 -0300 Subject: [PATCH 17/17] chore: remove useless lines --- src/Std/Time/DateTime/PlainDateTime.lean | 2 -- tests/lean/run/timeLocalDateTime.lean | 1 - 2 files changed, 3 deletions(-) diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index dd6fc91cc785..b97ca53c3f14 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -29,10 +29,8 @@ structure PlainDateTime where The `Time` component of a `PlainTime` -/ time : PlainTime - deriving Inhabited, BEq, Repr - namespace PlainDateTime /-- diff --git a/tests/lean/run/timeLocalDateTime.lean b/tests/lean/run/timeLocalDateTime.lean index ad2521a85ab3..4863a638729a 100644 --- a/tests/lean/run/timeLocalDateTime.lean +++ b/tests/lean/run/timeLocalDateTime.lean @@ -6,7 +6,6 @@ def ShortDateTime : GenericFormat .any := datespec("dd/MM/uuuu HH:mm:ss") def ShortDate : GenericFormat .any := datespec("dd/MM/uuuu") def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.hour PlainDate.minute PlainDate.time.second - def format₂ (PlainDate : PlainDate) : String := ShortDate.formatBuilder PlainDate.day PlainDate.month PlainDate.year def date₁ := datetime("1993-11-19T09:08:07")