max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab/timeParse.lean
Sofia Rodrigues f67ea44b6a
feat: add WallTime and simplify Timestamp API (#13675) 
This PR adds a `WallTime` type representing a point in time as
nanoseconds since `1970-01-01T00:00:00` local time. It also removes the
`sinceUNIXEpoch` and `AssumingUTC` suffixes because `Timestamp` implies
UTC, and `WallTime` implies it is based on the WallTime epoch (defined
in the comment as `1970-01-01T00:00:00`).

---------

Co-authored-by: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
2026-05-11 23:26:19 +00:00

204 lines
5.6 KiB
Text
Raw Permalink Blame History

import Std.Time
open Std.Time
def ISO8601UTC : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSXXX")
def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ")
def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu")
def LongDate : GenericFormat .any := datespec("MMMM D, uuuu")
def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss")
def LongDateTime : GenericFormat .any := datespec("MMMM dd, uuuu hh:mm aa")
def Time24Hour : GenericFormat .any := datespec("HH:mm:ss")
def Time12Hour : GenericFormat .any := datespec("hh:mm:ss aa")
def FullDayTimeZone : GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ")
def CustomDayTime : GenericFormat .any := datespec("EEE dd MMM uuuu HH:mm")
def Full12HourWrong : GenericFormat .any := datespec("MM/dd/uuuu hh:mm:ss aa XXX")
-- Dates
def brTZ : TimeZone := timezone("America/Sao_Paulo -03:00")
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")
/--
info: "2014-06-16T03:03:03.000000100-03:00"
-/
#guard_msgs in
#eval
let t : ZonedDateTime := ISO8601UTC.parse! "2014-06-16T03:03:03.000000100-03:00"
ISO8601UTC.format t.toDateTime
def tm := date₁.toTimestamp
def date₂ := DateTime.ofTimestamp tm brTZ
/--
info: "2014-06-16T03:03:03.000000000-03:00"
-/
#guard_msgs in
#eval
let t : ZonedDateTime := RFC1123.parse! "Mon, 16 Jun 2014 03:03:03 -0300"
ISO8601UTC.format t.toDateTime
def tm₃ := date₁.toTimestamp
def date₃ := DateTime.ofTimestamp tm₃ brTZ
/--
info: "2014-06-16T00:00:00.000000000Z"
-/
#guard_msgs in
#eval
let t : ZonedDateTime := ShortDate.parse! "06/16/2014"
ISO8601UTC.format t.toDateTime
-- the timestamp is always related to UTC.
/--
Timestamp: 1723739292
GMT: Thursday, 15 August 2024 16:28:12
BR: 15 August 2024 13:28:12 GMT-03:00
-/
def tm₄ : Second.Offset := 1723739292
def dateBR := DateTime.ofTimestamp (Timestamp.ofSecondsSinceUnixEpoch tm₄) brTZ
def dateJP := DateTime.ofTimestamp (Timestamp.ofSecondsSinceUnixEpoch tm₄) jpTZ
def dateUTC := DateTime.ofTimestamp (Timestamp.ofSecondsSinceUnixEpoch tm₄) .UTC
/--
info: "2024-08-15T13:28:12.000000000-03:00"
-/
#guard_msgs in
#eval
let t := FullDayTimeZone.parse! "Thursday, August 15, 2024 13:28:12 -0300"
ISO8601UTC.format t.toDateTime
/--
info: "2024-08-16T01:28:00.000000000Z"
-/
#guard_msgs in
#eval
let t : ZonedDateTime := LongDateTime.parse! "August 16, 2024 01:28 AM"
ISO8601UTC.format t.toDateTime
/--
info: "0000-12-31T22:28:12.000000000+09:00"
-/
#guard_msgs in
#eval
let t : ZonedDateTime := Time24Hour.parse! "13:28:12"
ISO8601UTC.format (t.toDateTime.convertTimeZone jpTZ)
/--
info: "0000-12-31T00:00:00.000000000-03:00"
-/
#guard_msgs in
#eval
let t1 : ZonedDateTime := Time12Hour.parse! "03:00:00 AM"
ISO8601UTC.format (t1.toDateTime.convertTimeZone brTZ)
/--
info: "Thu 15 Aug 2024 16:28"
-/
#guard_msgs in
#eval
let t2 : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 16:28:12 -0000"
CustomDayTime.format t2.toDateTime
/--
info: "2024-08-16T13:28:00.000000000Z"
-/
#guard_msgs in
#eval
let t5 : ZonedDateTime := CustomDayTime.parse! "Thu 16 Aug 2024 13:28"
ISO8601UTC.format t5.toDateTime
/--
info: "2024-08-16T01:28:12.000000000+09:00"
-/
#guard_msgs in
#eval
let t6 : ZonedDateTime := FullDayTimeZone.parse! "Friday, August 16, 2024 01:28:12 +0900"
ISO8601UTC.format (t6.toDateTime.convertTimeZone jpTZ)
/--
info: "2024-08-16T01:28:12.000000000+09:00"
-/
#guard_msgs in
#eval
let t7 : ZonedDateTime := FullDayTimeZone.parse! "Friday, August 16, 2024 01:28:12 +0900"
ISO8601UTC.format (t7.toDateTime.convertTimeZone jpTZ)
/--
TM: 1723730627
GMT: Thursday, 15 August 2024 14:03:47
Your time zone: 15 August 2024 11:03:47 GMT-03:00
-/
def localTm : Second.Offset := 1723730627
/--
This PlainDate is relative to the local time.
-/
def PlainDate : PlainDateTime := PlainDateTime.ofWallTime (WallTime.ofSeconds localTm)
def dateBR₁ := DateTime.ofPlainDateTime PlainDate brTZ
def dateJP₁ := DateTime.ofPlainDateTime PlainDate jpTZ
def dateUTC₁ := DateTime.ofPlainDateTime PlainDate .UTC
/--
info: "2024-08-15T14:03:47.000000000-03:00"
-/
#guard_msgs in
#eval
let t : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 14:03:47 -0300"
ISO8601UTC.format t.toDateTime
/--
info: "2024-08-15T14:03:47.000000000+09:00"
-/
#guard_msgs in
#eval
let t1 : ZonedDateTime := FullDayTimeZone.parse! "Thursday, August 15, 2024 14:03:47 +0900"
ISO8601UTC.format t1.toDateTime
/--
info: "2014-06-16T03:03:03.000000000-03:00"
-/
#guard_msgs in
#eval
let t2 : ZonedDateTime := FullDayTimeZone.parse! "Monday, June 16, 2014 03:03:03 -0300"
ISO8601UTC.format t2.toDateTime
/--
info: Except.ok "1993-05-10T10:30:23.000000000+03:00"
-/
#guard_msgs in
#eval
let t2 := Full12HourWrong.parse "05/10/1993 10:30:23 AM +03:00"
(ISO8601UTC.format ·.toDateTime) <$> t2
/--
info: Except.ok "1993-05-10T22:30:23.000000000+03:00"
-/
#guard_msgs in
#eval
let t2 := Full12HourWrong.parse "05/10/1993 10:30:23 PM +03:00"
(ISO8601UTC.format ·.toDateTime) <$> t2
/--
info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
-/
#guard_msgs in
#eval
let t2 := Full12HourWrong.parse "05/10/1993 20:30:23 AM +03:00"
(ISO8601UTC.format ·.toDateTime) <$> t2
/--
info: Except.error "offset 13: need a natural number in the interval of 1 to 12"
-/
#guard_msgs in
#eval
let t2 := Full12HourWrong.parse "05/10/1993 20:30:23 PM +03:00"
(ISO8601UTC.format ·.toDateTime) <$> t2
Reference in a new issue View git blame Copy permalink