diff --git a/src/Std/Time.lean b/src/Std/Time.lean index 29df3af7216d..1fe827970d0b 100644 --- a/src/Std/Time.lean +++ b/src/Std/Time.lean @@ -17,8 +17,7 @@ public import Std.Time.Zoned.Database public section -namespace Std -namespace Time +namespace Std.Time /-! # Time @@ -132,102 +131,128 @@ Represents spans of time and the difference between two points in time. # Formats Format strings are used to convert between `String` representations and date/time types, like `yyyy-MM-dd'T'HH:mm:ss.sssZ`. -The table below shows the available format specifiers. Some specifiers can be repeated to control truncation or offsets. -When a character is repeated `n` times, it usually truncates the value to `n` characters. +The table below shows the available format specifiers. Repeating a pattern character may change the +text style, minimum width, or offset/fraction form, depending on the field. -The `number` type format specifiers, such as `h` and `K`, are parsed based on the number of repetitions. -If the repetition count is one, the format allows values ranging from 1 up to the maximum capacity of -the respective data type. +The current Lean implementation follows Java's pattern language where practical, but it is not fully +locale-sensitive. + +For numeric fields that accept both one- and two-letter forms, the single-letter form parses a +non-padded number and the two-letter form parses a zero-padded width of two. The supported formats include: -- `G`: Represents the era, such as AD (Anno Domini) or BC (Before Christ). - - `G`, `GG`, `GGG` (short): Displays the era in a short format (e.g., "AD"). - - `GGGG` (full): Displays the era in a full format (e.g., "Anno Domini"). - - `GGGGG` (narrow): Displays the era in a narrow format (e.g., "A"). +- `G`: Represents the era, such as BCE (Before Common Era) or CE (Common Era). + - `G`, `GG`, `GGG` (short): Displays the era in a short format (e.g., "CE"). + - `GGGG` (full): Displays the era in a full format (e.g., "Common Era"). + - `GGGGG` (narrow): Displays the era in a narrow format (e.g., "C"). - `y`: Represents the year of the era. - `y`: Represents the year in its full form, without a fixed length. It can handle years of any size, (e.g., "1", "2025", or "12345678"). - `yy`: Displays the year in a two-digit format, showing the last two digits (e.g., "04" for 2004). - `yyyy`: Displays the year in a four-digit format (e.g., "2004"). - `yyyy+`: Extended format for years with more than four digits. +- `Y`: Represents the week-based year (ISO-like behavior around year boundaries). + - `Y`, `YYY`, `YYYY`: Displays the week-based year (e.g., "2017"). + - `YY`: Displays the last two digits of the week-based year (e.g., "17"). + - `YYYYY+`: Extended format for week-based years with more than four digits. - `u`: Represents the year. - `u`: Represents the year in its full form, without a fixed length. It can handle years of any size, (e.g., "1", "2025", or "12345678"). - `uu`: Two-digit year format, showing the last two digits (e.g., "04" for 2004). - `uuuu`: Displays the year in a four-digit format (e.g., "2004" or "-1000"). - `uuuu+`: Extended format for handling years with more than four digits (e.g., "12345" or "-12345"). Useful for historical dates far into the past or future! -- `Y`: Represents the week-based year. This may differ from the calendar year near the start or end of the year — for example, December 29 might belong to week 1 of the following year. Typically used together with `w` (week of week-based year). - - `Y`: Represents the week-based year in its full form, without a fixed length (e.g., "1", "2025", or "12345678"). - - `YY`: Two-digit week-based year, showing the last two digits (e.g., "04" for 2004). - - `YYYY`: Displays the week-based year in a four-digit format (e.g., "2004" or "-1000"). - - `YYYY+`: Extended format for week-based years with more than four digits. - `D`: Represents the day of the year. - `M`: Represents the month of the year, displayed as either a number or text. - `M`, `MM`: Displays the month as a number, with `MM` zero-padded (e.g., "7" for July, "07" for July with padding). - `MMM`: Displays the abbreviated month name (e.g., "Jul"). - `MMMM`: Displays the full month name (e.g., "July"). - `MMMMM`: Displays the month in a narrow form (e.g., "J" for July). +- `L`: Represents the standalone month of the year. + - Supports the same widths as `M`; in the current English data it formats the same values. - `d`: Represents the day of the month. - `Q`: Represents the quarter of the year. - `Q`, `QQ`: Displays the quarter as a number (e.g., "3", "03"). - `QQQ` (short): Displays the quarter as an abbreviated text (e.g., "Q3"). - `QQQQ` (full): Displays the full quarter text (e.g., "3rd quarter"). - `QQQQQ` (narrow): Displays the quarter as a short number (e.g., "3"). +- `q`: Represents the standalone quarter of the year. + - Supports the same widths as `Q`; in the current English data it formats the same values. - `w`: Represents the week of the week-based year, each week starts on Monday (e.g., "27"). -- `W`: Represents the week of the month, each week starts on Monday (e.g., "4"). +- `W`: Represents the week of the month using the library's fixed Monday-first week model (e.g., "2"). - `E`: Represents the day of the week as text. - `E`, `EE`, `EEE`: Displays the abbreviated weekday name (e.g., "Tue"). - `EEEE`: Displays the full day name (e.g., "Tuesday"). - `EEEEE`: Displays the narrow day name (e.g., "T" for Tuesday). + - `EEEEEE`: Displays the short two-letter weekday name (e.g., "Tu"). - `e`: Represents the weekday as number or text. - `e`, `ee`: Displays the weekday as a number, starting from 1 (Monday) to 7 (Sunday). - `eee`, `eeee`, `eeeee`: Displays the weekday as text (same format as `E`). -- `F`: Represents the week of the month that the first week starts on the first day of the month (e.g., "3"). + - `eeeeee`: Displays the short two-letter weekday name (e.g., "Tu"). +- `c`: Standalone weekday. + - `c`: Displays the numeric weekday using the same Monday-to-Sunday numbering as `e`. + - `ccc`, `cccc`, `ccccc`: Display standalone text (same values as `e` in the current English data). + - `cccccc`: Displays the short two-letter weekday name (e.g., "Tu"). +- `F`: Represents the occurrence of the weekday within the month (e.g., the 2nd Sunday formats as `2`). - `a`: Represents the AM or PM designation of the day. - - `a`, `aa`, `aaa`: Displays AM or PM in a concise format (e.g., "PM"). - - `aaaa`: Displays the full AM/PM designation (e.g., "Post Meridium"). + - `a`, `aa`, `aaa`: Displays AM/PM (e.g., "PM"). + - `aaaa`: Displays the full form (e.g., "ante meridiem", "post meridiem"). + - `aaaaa`: Displays the narrow form (e.g., "a", "p"). +- `b`: Represents the day period, extending AM/PM with noon and midnight (TR35 §4, supported in Java 16+). The `B` symbol (flexible day periods) is not supported. + - `b`, `bb`, `bbb`: Displays a short form (e.g., "AM", "PM", "noon", "midnight"). + - `bbbb`: Displays a full form (e.g., "ante meridiem", "post meridiem", "noon", "midnight"); unlike `a`, the AM/PM spellings are lowercase here. + - `bbbbb`: Displays a narrow form (e.g., "a", "p", "n", "mi"). - `h`: Represents the hour of the AM/PM clock (1-12) (e.g., "12"). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. + - `h`, `hh` are supported, matching Java. - `K`: Represents the hour of the AM/PM clock (0-11) (e.g., "0"). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. + - `K`, `KK` are supported, matching Java. - `k`: Represents the hour of the day in a 1-24 format (e.g., "24"). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. + - `k`, `kk` are supported, matching Java. - `H`: Represents the hour of the day in a 0-23 format (e.g., "0"). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. + - `H`, `HH` are supported, matching Java. - `m`: Represents the minute of the hour (e.g., "30"). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. + - `m`, `mm` are supported, matching Java. - `s`: Represents the second of the minute (e.g., "55"). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. + - `s`, `ss` are supported, matching Java. - `S`: Represents a fraction of a second, typically displayed as a decimal number (e.g., "978" for milliseconds). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. + - One or more repetitions of the character truncates to the specified number of most-significant digits; it does not round. - `A`: Represents the millisecond of the day (e.g., "1234"). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. -- `n`: Represents the nanosecond of the second (e.g., "987654321"). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. -- `N`: Represents the nanosecond of the day (e.g., "1234000000"). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. -- `VV`: Represents the time zone ID, which could be a city-based zone (e.g., "America/Los_Angeles"), a UTC marker (`"Z"`), or a specific offset (e.g., "-08:30"). - - One or more repetitions of the character indicates the truncation of the value to the specified number of characters. + - One or more repetitions of the character indicates zero-padding to the specified number of characters (no truncation is applied). +- `n`: Represents the nanosecond of the second (e.g., "987654321"). This is a Lean/Java extension, not a TR35 field. + - One or more repetitions of the character sets a minimum width via zero-padding; the value is not truncated. +- `N`: Represents the nanosecond of the day (e.g., "1234000000"). This is a Lean/Java extension, not a TR35 field. + - One or more repetitions of the character sets a minimum width via zero-padding; the value is not truncated. +- `V`: Time zone ID. + - `VV`: Displays the zone identifier/name. + - Other counts are unsupported, matching Java. - `z`: Represents the time zone name. - - `z`, `zz`, `zzz`: Shows an abbreviated time zone name (e.g., "PST" for Pacific Standard Time). - - `zzzz`: Displays the full time zone name (e.g., "Pacific Standard Time"). + - `z`, `zz`, `zzz`: Shows a short zone name; for offset-only zones this is the numeric offset (e.g., "+09:00"), for UTC this is "UTC", otherwise the abbreviation (e.g., "PST"). + - `zzzz`: Displays the full zone name; for offset-only zones this is the numeric offset (e.g., "+09:00"), for UTC this is "Coordinated Universal Time", otherwise the full zone name (e.g., "Pacific Standard Time"). +- `v`: Generic time zone name. + - `v`: In the current Lean timezone data this displays the stored abbreviation; for offset-only zones this is the numeric offset (e.g., "+09:00"), and for UTC it is normalized to "UTC". + - `vvvv`: In the current Lean timezone data this displays the stored zone name/ID; for offset-only zones this is the numeric offset (e.g., "+09:00"), and for UTC it is normalized to "Coordinated Universal Time". - `O`: Represents the localized zone offset in the format "GMT" followed by the time difference from UTC. - - `O`: Displays the GMT offset in a simple format (e.g., "GMT+8"). - - `OOOO`: Displays the full GMT offset, including hours and minutes (e.g., "GMT+08:00"). + - `O`: Displays the GMT offset in a short format (e.g., "GMT+8"), or "GMT" for UTC. + - `OOOO`: Displays the full GMT offset with padded hour and minutes (e.g., "GMT+08:00"), or "GMT" for UTC. - `X`: Represents the zone offset. It uses 'Z' for UTC and can represent any offset (positive or negative). - - `X`: Displays the hour offset (e.g., "-08"). + - `X`: Displays hour and optional minute offset (e.g., "-08", "-0830", or "Z"). - `XX`: Displays the hour and minute offset without a colon (e.g., "-0830"). - `XXX`: Displays the hour and minute offset with a colon (e.g., "-08:30"). - - `XXXX`: Displays the hour, minute, and second offset without a colon (e.g., "-083045"). - - `XXXXX`: Displays the hour, minute, and second offset with a colon (e.g., "-08:30:45"). -- `x`: Represents the zone offset. Similar to X, but does not display 'Z' for UTC and focuses only on positive offsets. - - `x`: Displays the hour offset (e.g., "+08"). + - `XXXX`: Displays the hour and minute offset without a colon, with optional seconds (e.g., "-0830", "-083045"). + - `XXXXX`: Displays the hour and minute offset with a colon, with optional seconds (e.g., "-08:30", "-08:30:45"). +- `x`: Represents the zone offset. Similar to `X`, but never displays `'Z'` for UTC. + - `x`: Displays hour and optional minute offset (e.g., "+00", "+0530"). - `xx`: Displays the hour and minute offset without a colon (e.g., "+0830"). - `xxx`: Displays the hour and minute offset with a colon (e.g., "+08:30"). - - `xxxx`: Displays the hour, minute, and second offset without a colon (e.g., "+083045"). - - `xxxxx`: Displays the hour, minute, and second offset with a colon (e.g., "+08:30:45"). -- `Z`: Always includes an hour and minute offset and may use 'Z' for UTC, providing clear differentiation between UTC and other time zones. - - `Z`: Displays the hour and minute offset without a colon (e.g., "+0800"). - - `ZZ`: Displays "GMT" followed by the time offset (e.g., "GMT+08:00" or "Z"). - - `ZZZ`: Displays the full hour, minute, and second offset with a colon (e.g., "+08:30:45" or "Z"). + - `xxxx`: Displays the hour and minute offset without a colon, with optional seconds (e.g., "+0830", "+083045"). + - `xxxxx`: Displays the hour and minute offset with a colon, with optional seconds (e.g., "+08:30", "+08:30:45"). +- `Z`: Represents the zone offset in RFC/CLDR `Z` forms. + - `Z`, `ZZ`, `ZZZ`: Displays hour and minute offset without colon, with optional seconds (e.g., "+0800", "+083045"). + - `ZZZZ`: Displays localized GMT form (e.g., "GMT+08:00"). + - `ZZZZZ`: Displays hour and minute offset with a colon and optional seconds, and uses `"Z"` for UTC (e.g., "Z", "+08:30", "+08:30:45"). +# Runtime Parsing + +- `DateTime.parse` parses common zoned date-time formats with explicit offsets, but does not resolve timezone identifiers like `[Europe/Paris]`. +- `DateTime.parseIO` resolves identifier-based inputs via the default timezone database. +- `DateTime.fromLeanDateTimeWithIdentifierString` is pure and does not perform timezone database resolution. +- `DateTime.fromLeanDateTimeWithIdentifierStringIO` resolves identifiers using the default timezone database. # Macros @@ -241,8 +266,10 @@ The `.sssssssss` can be omitted in most cases. - **`offset("+HH:mm")`**: Represents a timezone offset in the format `+HH:mm`, where `+` or `-` indicates the direction from UTC. - **`timezone("NAME/ID ZZZ")`**: Specifies a timezone using a region-based name or ID, along with its associated offset. - **`datespec("FORMAT")`**: Defines a compile-time date format based on the provided string. -- **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssssZZZ")`**: Represents a `DateTime` with a fixed timezone and optional nanosecond precision. +- **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssssZZZZZ")`**: Represents a `DateTime` with a fixed timezone and optional nanosecond precision. - **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssss[IDENTIFIER]")`**: Defines an `IO DateTime`, where the timezone identifier is dynamically retrieved from the default timezone database. - **`zoned("uuuu-MM-ddTHH:mm:ss.sssssssss, timezone")`**: Represents an `IO DateTime`, using a specified `timezone` term and allowing optional nanoseconds. -/ + +end Std.Time diff --git a/src/Std/Time/Date/PlainDate.lean b/src/Std/Time/Date/PlainDate.lean index 433375829fbb..fbd254b50956 100644 --- a/src/Std/Time/Date/PlainDate.lean +++ b/src/Std/Time/Date/PlainDate.lean @@ -334,46 +334,67 @@ def withWeekday (date : PlainDate) (desiredWeekday : Weekday) : PlainDate := date.addDays (Day.Offset.ofInt offset.toInt) +private def localizedDayOfWeek (weekday firstDay : Weekday) : Bounded.LE 0 6 := + weekday.toOrdinal + |>.subBounds firstDay.toOrdinal + |>.emod 7 (by decide) + /-- -Calculates the week of the year for a given date, using `firstDay` as the first day of the week. +Returns the first day of the week-based year for the given `year`, where weeks start on `firstDay` +and the first week must contain at least `minimalDays` days of the new year. -/ -def weekOfYear (date : PlainDate) (firstDay : Weekday := .monday) : Week.OfYear.Ordinal := - let y := date.year - let posInWeek : Bounded.LE 1 7 := - .ofNatWrapping ((date.weekday.toOrdinal.val - firstDay.toOrdinal.val + 7) % 7 + 1) (by decide) - - let w := Bounded.LE.exact 10 - |>.addBounds date.dayOfYear - |>.subBounds posInWeek - |>.ediv 7 (by decide) +def startOfWeekBasedYear (year : Year.Offset) (firstDay : Weekday) (minimalDays : Bounded.LE 0 6) : PlainDate := + let jan1 := PlainDate.ofYearMonthDayClip year 1 1 + let localDay := localizedDayOfWeek jan1.weekday firstDay + let daysInNewYearWeek : Bounded.LE 1 7 := Bounded.LE.exact 7 |>.subBounds localDay + let weekStart := jan1 |>.subDays (Day.Offset.ofNat localDay.toNat) - if h : w.val < 1 then - (y-1).weeks |>.expandBottom (by decide) - else if h₁ : w.val > y.weeks.val then - .ofNat' 1 (by decide) + if daysInNewYearWeek.val >= minimalDays.val then + weekStart else - let h := Int.not_lt.mp h - let h₁ := Int.not_lt.mp h₁ - let w := w.truncateBottom h |>.truncateTop (Int.le_trans h₁ y.weeks.property.right) - w + weekStart.addDays 7 /-- -Returns the week-based year for the given `PlainDate`, using `firstDay` as the start of the week. -The week-based year may differ from the calendar year for dates near the start or end of the year. +Returns the week number within the week-based year for the given `PlainDate`, using `firstDay` as +the start of the week and `minDays` as the minimum number of days required in the first week of the +year (default 4 for ISO 8601). Dates before the first week of the calendar year are counted as part +of the last week of the previous year. -/ -def weekYear (date : PlainDate) (firstDay : Weekday := .monday) : Year.Offset := - let y := date.year - let posInWeek : Bounded.LE 1 7 := - .ofNatWrapping ((date.weekday.toOrdinal.val - firstDay.toOrdinal.val + 7) % 7 + 1) (by decide) +def weekOfYear (date : PlainDate) (firstDay : Weekday := .monday) (minDaysBounded : Bounded.LE 0 6 := .mk 4 (by decide)) : Week.OfYear.Ordinal := + let year := date.year + let thisYearStart := startOfWeekBasedYear year firstDay minDaysBounded - let w := Bounded.LE.exact 10 - |>.addBounds date.dayOfYear - |>.subBounds posInWeek - |>.ediv 7 (by decide) + if date.toEpochDay < thisYearStart.toEpochDay then + let prevYearStart := startOfWeekBasedYear (year - 1) firstDay minDaysBounded + let interval := date.toEpochDay - prevYearStart.toEpochDay + let interval := Bounded.LE.ofNatWrapping interval.val (by decide) (lo := 0) (hi := 370) + let w := interval.ediv 7 (by decide) + w.add 1 + else + let nextYearStart := startOfWeekBasedYear (year + 1) firstDay minDaysBounded + if date.toEpochDay >= nextYearStart.toEpochDay then + 1 + else + let interval := date.toEpochDay - thisYearStart.toEpochDay + let interval := Bounded.LE.ofNatWrapping interval.val (by decide) (lo := 0) (hi := 370) + let w := interval.ediv 7 (by decide) + w.add 1 - if w.val < 1 then y - 1 - else if w.val > y.weeks.val then y + 1 - else y +/-- +Returns the week-based year for the given `PlainDate`, using `firstDay` as the start of the week +and `minDays` as the minimum number of days in the first week of the year (default 4 for ISO 8601). +-/ +def weekYear (date : PlainDate) (firstDay : Weekday := .monday) (minDays : Bounded.LE 0 6 := Bounded.LE.mk 4 (by decide)) : Year.Offset := + let year := date.year + let thisYearStart := startOfWeekBasedYear year firstDay minDays + if date.toEpochDay < thisYearStart.toEpochDay then + year - 1 + else + let nextYearStart := startOfWeekBasedYear (year + 1) firstDay minDays + if date.toEpochDay >= nextYearStart.toEpochDay then + year + 1 + else + year instance : HAdd PlainDate Day.Offset PlainDate where hAdd := addDays diff --git a/src/Std/Time/Date/Unit/Year.lean b/src/Std/Time/Date/Unit/Year.lean index a8fd4b0350e5..7b0670bee07a 100644 --- a/src/Std/Time/Date/Unit/Year.lean +++ b/src/Std/Time/Date/Unit/Year.lean @@ -107,8 +107,8 @@ Calculates the number of days in the specified `year`. -/ def days (year : Offset) : Bounded.LE 365 366 := if year.isLeap - then .ofNatWrapping 366 (by decide) - else .ofNatWrapping 355 (by decide) + then .mk 366 (by decide) + else .mk 365 (by decide) /-- Calculates the number of weeks in the specified `year`. diff --git a/src/Std/Time/DateTime.lean b/src/Std/Time/DateTime.lean index 10e00cffe2e3..f09c5ae455ae 100644 --- a/src/Std/Time/DateTime.lean +++ b/src/Std/Time/DateTime.lean @@ -14,6 +14,8 @@ public section namespace Std namespace Time +open Internal + /-- Represents a date and time with timezone information. -/ @@ -185,19 +187,21 @@ def dayOfYear (date : DateTime) : Day.Ordinal.OfYear date.date.get.date.year.isL ValidDate.dayOfYear ⟨(date.date.get.date.month, date.date.get.date.day), date.date.get.date.valid⟩ /-- -Determines the week of the year for the given `DateTime`, using `firstDay` as the start of the week. +Determines the week of the year for the given `DateTime`, using `firstDay` as the start of the week +and `minDays` as the minimum number of days a week must have in the new year to count as week 1. -/ @[inline] -def weekOfYear (date : DateTime) (firstDay : Weekday := .monday) : Week.OfYear.Ordinal := - date.date.get.weekOfYear firstDay +def weekOfYear (dt : DateTime) (firstDay : Weekday := .monday) (minDays : Bounded.LE 0 6 := Bounded.LE.mk 4 (by decide)) : Week.OfYear.Ordinal := + PlainDate.weekOfYear dt.date.get.date firstDay minDays /-- -Returns the week-based year for the given `DateTime`, using `firstDay` as the start of the week. +Returns the week-based year for the given `DateTime`, using `firstDay` as the start of the week +and `minDays` as the minimum number of days a week must have in the new year to count as week 1. The week-based year may differ from the calendar year for dates near the start or end of the year. -/ @[inline] -def weekYear (date : DateTime) (firstDay : Weekday := .monday) : Year.Offset := - date.date.get.weekYear firstDay +def weekYear (date : DateTime) (firstDay : Weekday := .monday) (minDays : Bounded.LE 0 6 := Bounded.LE.mk 4 (by decide)) : Year.Offset := + date.date.get.weekYear firstDay minDays /-- Returns the aligned week of the month for a `DateTime`. Weeks are fixed 7-day slots diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean index 11995e556c0d..da9dc474f242 100644 --- a/src/Std/Time/DateTime/PlainDateTime.lean +++ b/src/Std/Time/DateTime/PlainDateTime.lean @@ -489,19 +489,21 @@ def inLeapYear (date : PlainDateTime) : Bool := date.year.isLeap /-- -Determines the week of the year for the given `PlainDateTime`, using `firstDay` as the start of the week. +Determines the week of the year for the given `PlainDateTime`, using `firstDay` as the start of the week +and `minDays` as the minimum number of days a week must have in the new year to count as week 1. -/ @[inline] -def weekOfYear (date : PlainDateTime) (firstDay : Weekday := .monday) : Week.OfYear.Ordinal := - date.date.weekOfYear firstDay +def weekOfYear (date : PlainDateTime) (firstDay : Weekday := .monday) (minDays : Bounded.LE 0 6 := Bounded.LE.mk 4 (by decide)) : Week.OfYear.Ordinal := + PlainDate.weekOfYear date.date firstDay minDays /-- -Returns the week-based year for the given `PlainDateTime`, using `firstDay` as the start of the week. +Returns the week-based year for the given `PlainDateTime`, using `firstDay` as the start of the week +and `minDays` as the minimum number of days a week must have in the new year to count as week 1. The week-based year may differ from the calendar year for dates near the start or end of the year. -/ @[inline] -def weekYear (date : PlainDateTime) (firstDay : Weekday := .monday) : Year.Offset := - date.date.weekYear firstDay +def weekYear (date : PlainDateTime) (firstDay : Weekday := .monday) (minDays : Bounded.LE 0 6 := Bounded.LE.mk 4 (by decide)) : Year.Offset := + date.date.weekYear firstDay minDays /-- Returns the aligned week of the month for a `PlainDateTime`. Weeks are fixed 7-day slots diff --git a/src/Std/Time/Format.lean b/src/Std/Time/Format.lean index be6eeab82cc2..dbdda5c74f1d 100644 --- a/src/Std/Time/Format.lean +++ b/src/Std/Time/Format.lean @@ -189,15 +189,14 @@ def format (date : PlainDate) (format : String) (locale : DateFormat := .enUS) : | .G _ => some date.era | .y _ => some date.year | .u _ => some date.year - | .Y _ => some (date.weekYear locale.firstDayOfWeek) + | .Y _ => some (date.weekYear locale.firstDayOfWeek locale.minimalDaysInFirstWeek) | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear) - | .Qorq _ => some date.quarter - | .w _ => some (date.weekOfYear locale.firstDayOfWeek) + | .Q _ | .q _ => some date.quarter + | .w _ => some (date.weekOfYear locale.firstDayOfWeek locale.minimalDaysInFirstWeek) | .W _ => some (date.weekOfMonth locale.firstDayOfWeek) - | .MorL _ => some date.month + | .M _ | .L _ => some date.month | .d _ => some date.day - | .E _ => some date.weekday - | .eorc _ => some date.weekday + | .E _ | .e _ | .c _ => some date.weekday | .F _ => some date.alignedWeekOfMonth | _ => none match res with @@ -272,6 +271,8 @@ def format (time : PlainTime) (format : String) : String := | .n _ => some time.nanosecond | .s _ => some time.second | .a _ => some (HourMarker.ofOrdinal time.hour) + | .b _ => some (classifyDayPeriod time.hour time.minute time.second) + | .B _ => some (classifyExtendedDayPeriod time.hour time.minute time.second) | .h _ => some time.hour.toRelative | .K _ => some (time.hour.emod 12 (by decide)) | .S _ => some time.nanosecond @@ -454,15 +455,14 @@ def format (date : PlainDateTime) (format : String) (locale : DateFormat := .enU | .G _ => some date.era | .y _ => some date.year | .u _ => some date.year - | .Y _ => some (date.weekYear locale.firstDayOfWeek) + | .Y _ => some (date.weekYear locale.firstDayOfWeek locale.minimalDaysInFirstWeek) | .D _ => some (Sigma.mk date.year.isLeap date.dayOfYear) - | .Qorq _ => some date.quarter - | .w _ => some (date.weekOfYear locale.firstDayOfWeek) + | .Q _ | .q _ => some date.quarter + | .w _ => some (date.weekOfYear locale.firstDayOfWeek locale.minimalDaysInFirstWeek) | .W _ => some (date.weekOfMonth locale.firstDayOfWeek) - | .MorL _ => some date.month + | .M _ | .L _ => some date.month | .d _ => some date.day - | .E _ => some date.weekday - | .eorc _ => some date.weekday + | .E _ | .e _ | .c _ => some date.weekday | .F _ => some date.alignedWeekOfMonth | .H _ => some date.hour | .k _ => some date.hour.shiftTo1BasedHour @@ -470,6 +470,8 @@ def format (date : PlainDateTime) (format : String) (locale : DateFormat := .enU | .n _ => some date.nanosecond | .s _ => some date.time.second | .a _ => some (HourMarker.ofOrdinal date.hour) + | .b _ => some (classifyDayPeriod date.hour date.minute date.time.second) + | .B _ => some (classifyExtendedDayPeriod date.hour date.minute date.time.second) | .h _ => some date.hour.toRelative | .K _ => some (date.hour.emod 12 (by decide)) | .S _ => some date.nanosecond diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean index 6a8720e06820..ba11ba3bfd2a 100644 --- a/src/Std/Time/Format/Basic.lean +++ b/src/Std/Time/Format/Basic.lean @@ -7,6 +7,7 @@ module prelude public import Std.Time.Zoned +public import Std.Time.Format.Modifier public import Std.Time.Format.DateFormat import Init.Data.String.TakeDrop import Init.Data.String.Search @@ -25,502 +26,6 @@ open Std.Internal.Parsec Lean PlainTime PlainDate TimeZone DateTime set_option linter.all true -/-- -`Text` represents different text formatting styles. --/ -inductive Text - /-- Short form (e.g., "Tue") -/ - | short - /-- Full form (e.g., "Tuesday") -/ - | full - /-- Narrow form (e.g., "T") -/ - | narrow - deriving Repr, Inhabited - -namespace Text - -/-- -`classify` classifies the number of pattern letters into a `Text` type. --/ -def classify (num : Nat) : Option Text := - if num < 4 then - some (.short) - else if num = 4 then - some (.full) - else if num = 5 then - some (.narrow) - else - none - -end Text - -/-- -`Number` represents different number formatting styles. --/ -structure Number where - /-- - The number of digits to pad, based on the count of pattern letters. - -/ - padding : Nat - deriving Repr, Inhabited - -/-- -`classifyNumberText` classifies the number of pattern letters into either a `Number` or `Text`. --/ -def classifyNumberText : Nat → Option (Number ⊕ Text) - | n => if n < 3 then some (.inl ⟨n⟩) else .inr <$> (Text.classify n) - -/-- -`Fraction` represents the fraction of a second, which can either be full nanoseconds -or a truncated form with fewer digits. --/ -inductive Fraction - /-- Nanosecond precision (up to 9 digits) -/ - | nano - /-- Fewer digits (truncated precision) -/ - | truncated (digits : Nat) - deriving Repr, Inhabited - -namespace Fraction - -/-- -`classify` classifies the number of pattern letters into either a `Fraction`. It's used for `nano`. --/ -def classify (nat : Nat) : Option Fraction := - if nat < 9 then - some (.truncated nat) - else if nat = 9 then - some (.nano) - else - none - -end Fraction - -/-- -`Year` represents different year formatting styles based on the number of pattern letters. --/ -inductive Year - /-- Any size (e.g., "19000000000000") -/ - | any - /-- Two-digit year format (e.g., "23" for 2023) -/ - | twoDigit - /-- Four-digit year format (e.g., "2023") -/ - | fourDigit - /-- Extended year format for more than 4 digits (e.g., "002023") -/ - | extended (num : Nat) - deriving Repr, Inhabited - -namespace Year - -/-- -`classify` classifies the number of pattern letters into a `Year` format. --/ -def classify (num : Nat) : Option Year := - if num = 1 then - some .any - else if num = 2 then - some .twoDigit - else if num = 4 then - some .fourDigit - else if num > 4 ∨ num = 3 then - some (.extended num) - else - none - -end Year - -/-- -`ZoneId` represents different time zone ID formats based on the number of pattern letters. --/ -inductive ZoneId - /-- Short form of time zone (e.g., "PST") -/ - | short - /-- Full form of time zone (e.g., "Pacific Standard Time") -/ - | full - deriving Repr, Inhabited - -namespace ZoneId - -/-- -`classify` classifies the number of pattern letters into a `ZoneId` format. -- If 2 letters, it returns the short form. -- If 4 letters, it returns the full form. -- Otherwise, it returns none. --/ -def classify (num : Nat) : Option ZoneId := - if num = 2 then - some (.short) - else if num = 4 then - some (.full) - else - none - -end ZoneId - -/-- -`ZoneName` represents different zone name formats based on the number of pattern letters and -whether daylight saving time is considered. --/ -inductive ZoneName - /-- Short form of zone name (e.g., "PST") -/ - | short - /-- Full form of zone name (e.g., "Pacific Standard Time") -/ - | full - deriving Repr, Inhabited - -namespace ZoneName - -/-- -`classify` classifies the number of pattern letters and the letter type ('z' or 'v') -into a `ZoneName` format. -- For 'z', if less than 4 letters, it returns the short form; if 4 letters, it returns the full form. -- For 'v', if 1 letter, it returns the short form; if 4 letters, it returns the full form. -- Otherwise, it returns none. --/ -def classify (letter : Char) (num : Nat) : Option ZoneName := - if letter = 'z' then - if num < 4 then - some (.short) - else if num = 4 then - some (.full) - else - none - else if letter = 'v' then - if num = 1 then - some (.short) - else if num = 4 then - some (.full) - else - none - else - none - -end ZoneName - -/-- -`OffsetX` represents different offset formats based on the number of pattern letters. -The output will vary between the number of pattern letters, whether it's the hour, minute, second, -and whether colons are used. --/ -inductive OffsetX - /-- Only the hour is output (e.g., "+01") -/ - | hour - /-- Hour and minute without colon (e.g., "+0130") -/ - | hourMinute - /-- Hour and minute with colon (e.g., "+01:30") -/ - | hourMinuteColon - /-- Hour, minute, and second without colon (e.g., "+013015") -/ - | hourMinuteSecond - /-- Hour, minute, and second with colon (e.g., "+01:30:15") -/ - | hourMinuteSecondColon - deriving Repr, Inhabited - -namespace OffsetX - -/-- -`classify` classifies the number of pattern letters into an `OffsetX` format. --/ -def classify (num : Nat) : Option OffsetX := - if num = 1 then - some (.hour) - else if num = 2 then - some (.hourMinute) - else if num = 3 then - some (.hourMinuteColon) - else if num = 4 then - some (.hourMinuteSecond) - else if num = 5 then - some (.hourMinuteSecondColon) - else - none - -end OffsetX - -/-- -`OffsetO` represents localized offset text formats based on the number of pattern letters. --/ -inductive OffsetO - /-- Short form of the localized offset (e.g., "GMT+8") -/ - | short - /-- Full form of the localized offset (e.g., "GMT+08:00") -/ - | full - deriving Repr, Inhabited - -namespace OffsetO - -/-- -`classify` classifies the number of pattern letters into an `OffsetO` format. --/ -def classify (num : Nat) : Option OffsetO := - match num with - | 1 => some (.short) - | 4 => some (.full) - | _ => none - -end OffsetO - -/-- -`OffsetZ` represents different offset formats based on the number of pattern letters (capital 'Z'). --/ -inductive OffsetZ - /-- Hour and minute without colon (e.g., "+0130") -/ - | hourMinute - /-- Localized offset text in full form (e.g., "GMT+08:00") -/ - | full - /-- Hour, minute, and second with colon (e.g., "+01:30:15") -/ - | hourMinuteSecondColon - deriving Repr, Inhabited - -namespace OffsetZ - -/-- -`classify` classifies the number of pattern letters into an `OffsetZ` format. --/ -def classify (num : Nat) : Option OffsetZ := - match num with - | 1 | 2 | 3 => some (.hourMinute) - | 4 => some (.full) - | 5 => some (.hourMinuteSecondColon) - | _ => none - -end OffsetZ - -/-- -The `Modifier` inductive type represents various formatting options for date and time components, -matching the format symbols used in date and time strings. -These modifiers can be applied in formatting functions to generate custom date and time outputs. --/ -inductive Modifier - /-- - `G`: Era (e.g., AD, Anno Domini, A). - -/ - | G (presentation : Text) - - /-- - `y`: Year of era (e.g., 2004, 04, 0002, 2). - -/ - | y (presentation : Year) - - /-- - `u`: Year (e.g., 2004, 04, -0001, -1). - -/ - | u (presentation : Year) - - /-- - `Y`: Week-based year (e.g., 2004, 04, -0001, -1). - The week-based year may differ from the calendar year at the start or end of the year. - -/ - | Y (presentation : Year) - - /-- - `D`: Day of year (e.g., 189). - -/ - | D (presentation : Number) - - /-- - `M`: Month of year as number or text (e.g., 7, 07, Jul, July, J). - -/ - | MorL (presentation : Number ⊕ Text) - - /-- - `d`: Day of month (e.g., 10). - -/ - | d (presentation : Number) - - /-- - `Q`: Quarter of year as number or text (e.g., 3, 03, Q3, 3rd quarter). - -/ - | Qorq (presentation : Number ⊕ Text) - - /-- - `w`: Week of week-based year (e.g., 27). - -/ - | w (presentation : Number) - - /-- - `W`: Week of month (e.g., 4). - -/ - | W (presentation : Number) - - /-- - `E`: Day of week as text (e.g., Tue, Tuesday, T). - -/ - | E (presentation : Text) - - /-- - `e`: Localized day of week as number or text (e.g., 2, 02, Tue, Tuesday, T). - -/ - | eorc (presentation : Number ⊕ Text) - - /-- - `F`: Aligned week of month (e.g., 3). - -/ - | F (presentation : Number) - - /-- - `a`: AM/PM of day (e.g., PM). - -/ - | a (presentation : Text) - - /-- - `h`: Clock hour of AM/PM (1-12) (e.g., 12). - -/ - | h (presentation : Number) - - /-- - `K`: Hour of AM/PM (0-11) (e.g., 0). - -/ - | K (presentation : Number) - - /-- - `k`: Clock hour of day (1-24) (e.g., 24). - -/ - | k (presentation : Number) - - /-- - `H`: Hour of day (0-23) (e.g., 0). - -/ - | H (presentation : Number) - - /-- - `m`: Minute of hour (e.g., 30). - -/ - | m (presentation : Number) - - /-- - `s`: Second of minute (e.g., 55). - -/ - | s (presentation : Number) - - /-- - `S`: Fraction of second (e.g., 978). - -/ - | S (presentation : Fraction) - - /-- - `A`: Millisecond of day (e.g., 1234). - -/ - | A (presentation : Number) - - /-- - `n`: Nanosecond of second (e.g., 987654321). - -/ - | n (presentation : Number) - - /-- - `N`: Nanosecond of day (e.g., 1234000000). - -/ - | N (presentation : Number) - - /-- - `V`: Time zone ID (e.g., America/Los_Angeles, Z, -08:30). - -/ - | V - - /-- - `z`: Time zone name (e.g., Pacific Standard Time, PST). - -/ - | z (presentation : ZoneName) - - /-- - `O`: Localized zone offset (e.g., GMT+8, GMT+08:00, UTC-08:00). - -/ - | O (presentation : OffsetO) - - /-- - `X`: Zone offset with 'Z' for zero (e.g., Z, -08, -0830, -08:30). - -/ - | X (presentation : OffsetX) - - /-- - `x`: Zone offset without 'Z' (e.g., +0000, -08, -0830, -08:30). - -/ - | x (presentation : OffsetX) - - /-- - `Z`: Zone offset with 'Z' for UTC (e.g., +0000, -0800, -08:00). - -/ - | Z (presentation : OffsetZ) - deriving Repr, Inhabited - -/-- -`abstractParse` abstracts the parsing logic for any type that has a classify function. -It takes a constructor function to build the `Modifier` and a classify function that maps the pattern length to a specific type. --/ -private def parseMod (constructor : α → Modifier) (classify : Nat → Option α) (p : String) : Parser Modifier := - let len := p.positions.length - match classify len with - | some res => pure (constructor res) - | none => fail s!"invalid quantity of characters for '{p.front}'" - -private def parseText (constructor : Text → Modifier) (p : String) : Parser Modifier := - parseMod constructor Text.classify p - -private def parseFraction (constructor : Fraction → Modifier) (p : String) : Parser Modifier := - parseMod constructor Fraction.classify p - -private def parseNumber (constructor : Number → Modifier) (p : String) : Parser Modifier := - pure (constructor ⟨p.positions.length⟩) - -private def parseYear (constructor : Year → Modifier) (p : String) : Parser Modifier := - parseMod constructor Year.classify p - -private def parseOffsetX (constructor : OffsetX → Modifier) (p : String) : Parser Modifier := - parseMod constructor OffsetX.classify p - -private def parseOffsetZ (constructor : OffsetZ → Modifier) (p : String) : Parser Modifier := - parseMod constructor OffsetZ.classify p - -private def parseOffsetO (constructor : OffsetO → Modifier) (p : String) : Parser Modifier := - parseMod constructor OffsetO.classify p - -private def parseZoneId (p : String) : Parser Modifier := - if p.length = 2 then pure .V else fail s!"invalid quantity of characters for '{p.front}'" - -private def parseNumberText (constructor : (Number ⊕ Text) → Modifier) (p : String) : Parser Modifier := - parseMod constructor classifyNumberText p - -private def parseZoneName (constructor : ZoneName → Modifier) (p : String) : Parser Modifier := - let len := p.length - match ZoneName.classify (p.front) len with - | some res => pure (constructor res) - | none => fail s!"invalid quantity of characters for '{p.front}'" - -private def parseModifier : Parser Modifier - := (parseText Modifier.G =<< many1Chars (pchar 'G')) - <|> parseYear Modifier.y =<< many1Chars (pchar 'y') - <|> parseYear Modifier.u =<< many1Chars (pchar 'u') - <|> parseYear Modifier.Y =<< many1Chars (pchar 'Y') - <|> parseNumber Modifier.D =<< many1Chars (pchar 'D') - <|> parseNumberText Modifier.MorL =<< many1Chars (pchar 'M') - <|> parseNumberText Modifier.MorL =<< many1Chars (pchar 'L') - <|> parseNumber Modifier.d =<< many1Chars (pchar 'd') - <|> parseNumberText Modifier.Qorq =<< many1Chars (pchar 'Q') - <|> parseNumberText Modifier.Qorq =<< many1Chars (pchar 'q') - <|> parseNumber Modifier.w =<< many1Chars (pchar 'w') - <|> parseNumber Modifier.W =<< many1Chars (pchar 'W') - <|> parseText Modifier.E =<< many1Chars (pchar 'E') - <|> parseNumberText Modifier.eorc =<< many1Chars (pchar 'e') - <|> parseNumberText Modifier.eorc =<< many1Chars (pchar 'c') - <|> parseNumber Modifier.F =<< many1Chars (pchar 'F') - <|> parseText Modifier.a =<< many1Chars (pchar 'a') - <|> parseNumber Modifier.h =<< many1Chars (pchar 'h') - <|> parseNumber Modifier.K =<< many1Chars (pchar 'K') - <|> parseNumber Modifier.k =<< many1Chars (pchar 'k') - <|> parseNumber Modifier.H =<< many1Chars (pchar 'H') - <|> parseNumber Modifier.m =<< many1Chars (pchar 'm') - <|> parseNumber Modifier.s =<< many1Chars (pchar 's') - <|> parseFraction Modifier.S =<< many1Chars (pchar 'S') - <|> parseNumber Modifier.A =<< many1Chars (pchar 'A') - <|> parseNumber Modifier.n =<< many1Chars (pchar 'n') - <|> parseNumber Modifier.N =<< many1Chars (pchar 'N') - <|> parseZoneId =<< many1Chars (pchar 'V') - <|> parseZoneName Modifier.z =<< many1Chars (pchar 'z') - <|> parseOffsetO Modifier.O =<< many1Chars (pchar 'O') - <|> parseOffsetX Modifier.X =<< many1Chars (pchar 'X') - <|> parseOffsetX Modifier.x =<< many1Chars (pchar 'x') - <|> parseOffsetZ Modifier.Z =<< many1Chars (pchar 'Z') - /-- The part of a formatting string. A string is just a text and a modifier is in the format described in the `Modifier` type. @@ -663,6 +168,9 @@ private def formatWeekdayShort (symbols : DateFormatSymbols) (wd : Weekday) : St private def formatWeekdayNarrow (symbols : DateFormatSymbols) (wd : Weekday) : String := symbols.weekdayNarrow.get (wd.toOrdinal.sub 1 |>.toFin (by decide)) +private def formatWeekdayTwoLetter (symbols : DateFormatSymbols) (wd : Weekday) : String := + symbols.weekdayTwoLetter.get (wd.toOrdinal.sub 1 |>.toFin (by decide)) + private def formatEraShort (symbols : DateFormatSymbols) (era : Year.Era) : String := symbols.eraShort.get (eraIndex era) @@ -684,6 +192,9 @@ private def formatQuarterShort (symbols : DateFormatSymbols) (q : Month.Quarter) private def formatQuarterLong (symbols : DateFormatSymbols) (q : Month.Quarter) : String := symbols.quarterLong.get (q.sub 1 |>.toFin (by decide)) +private def formatQuarterNarrow (symbols : DateFormatSymbols) (q : Month.Quarter) : String := + symbols.quarterNarrow.get (q.sub 1 |>.toFin (by decide)) + private def formatMarkerShort (symbols : DateFormatSymbols) (marker : HourMarker) : String := match marker with | .am => symbols.amShort @@ -699,72 +210,115 @@ private def formatMarkerNarrow (symbols : DateFormatSymbols) (marker : HourMarke | .am => symbols.amNarrow | .pm => symbols.pmNarrow +private def formatDayPeriod (dp : DayPeriodSymbols) (period : DayPeriod) : String := + match period with + | .am => dp.am + | .pm => dp.pm + | .noon => dp.noon + | .midnight => dp.midnight + +private def extendedDayPeriodIndex : ExtendedDayPeriod → Fin 6 + | .midnight => 0 + | .night => 1 + | .morning => 2 + | .noon => 3 + | .afternoon => 4 + | .evening => 5 + +private def formatExtendedDayPeriod (arr : Vector String 6) (period : ExtendedDayPeriod) : String := + arr.get (extendedDayPeriodIndex period) + private def toSigned (data : Int) : String := if data < 0 then toString data else "+" ++ toString data -private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bool) (colon : Bool) : String := +private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bool) (colon : Bool) (padHour : Bool := true) : String := let (sign, time) := if offset.second.val ≥ 0 then ("+", offset.second) else ("-", -offset.second) let time := PlainTime.ofSeconds time let pad := leftPadAscii 2 '0' ∘ toString - let data := s!"{sign}{pad time.hour.val}" + let hourStr := if padHour then pad time.hour.val else toString time.hour.val + let data := s!"{sign}{hourStr}" let data := if withMinutes then s!"{data}{if colon then ":" else ""}{pad time.minute.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 +/-- Classify a `PlainTime` into a `DayPeriod` for the `b` pattern. -/ +def classifyDayPeriod (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) : DayPeriod := + if hour.val = 0 ∧ minute.val = 0 ∧ second.val = 0 then .midnight + else if hour.val = 12 ∧ minute.val = 0 ∧ second.val = 0 then .noon + else if hour.val < 12 then .am + else .pm + +/-- Classify a `PlainTime` into an `ExtendedDayPeriod` for the `B` pattern (CLDR flexible periods). -/ +def classifyExtendedDayPeriod (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal true) : ExtendedDayPeriod := + if hour.val = 0 ∧ minute.val = 0 ∧ second.val = 0 then .midnight + else if hour.val = 12 ∧ minute.val = 0 ∧ second.val = 0 then .noon + else if hour.val < 6 then .night + else if hour.val < 12 then .morning + else if hour.val < 18 then .afternoon + else if hour.val < 21 then .evening + else .night + set_option linter.missingDocs false in -- TODO @[expose /- for codegen -/] def TypeFormat : Modifier → Type - | .G _ => Year.Era - | .y _ => Year.Offset - | .u _ => Year.Offset - | .Y _ => Year.Offset - | .D _ => Sigma Day.Ordinal.OfYear - | .MorL _ => Month.Ordinal - | .d _ => Day.Ordinal - | .Qorq _ => Month.Quarter - | .w _ => Week.OfYear.Ordinal - | .W _ => Week.Ordinal - | .E _ => Weekday - | .eorc _ => Weekday - | .F _ => Week.Aligned.Ordinal - | .a _ => HourMarker - | .h _ => Bounded.LE 1 12 - | .K _ => Bounded.LE 0 11 - | .k _ => Bounded.LE 1 24 - | .H _ => Hour.Ordinal - | .m _ => Minute.Ordinal - | .s _ => Second.Ordinal true - | .S _ => Nanosecond.Ordinal - | .A _ => Millisecond.Offset - | .n _ => Nanosecond.Ordinal - | .N _ => Nanosecond.Offset - | .V => String - | .z _ => String - | .O _ => Offset - | .X _ => Offset - | .x _ => Offset - | .Z _ => Offset + | .G _ => Year.Era + | .y _ => Year.Offset + | .u _ => Year.Offset + | .Y _ => Year.Offset + | .D _ => Sigma Day.Ordinal.OfYear + | .M _ => Month.Ordinal + | .L _ => Month.Ordinal + | .d _ => Day.Ordinal + | .Q _ => Month.Quarter + | .q _ => Month.Quarter + | .w _ => Week.OfYear.Ordinal + | .W _ => Week.Ordinal + | .E _ => Weekday + | .e _ => Weekday + | .c _ => Weekday + | .F _ => Week.Aligned.Ordinal + | .a _ => HourMarker + | .b _ => DayPeriod + | .B _ => ExtendedDayPeriod + | .h _ => Bounded.LE 1 12 + | .K _ => Bounded.LE 0 11 + | .k _ => Bounded.LE 1 24 + | .H _ => Hour.Ordinal + | .m _ => Minute.Ordinal + | .s _ => Second.Ordinal true + | .S _ => Nanosecond.Ordinal + | .A _ => Millisecond.Offset + | .n _ => Nanosecond.Ordinal + | .N _ => Nanosecond.Offset + | .V _ => String + | .z _ => String + | .v _ => String + | .O _ => Offset + | .X _ => Offset + | .x _ => Offset + | .Z _ => Offset private def formatWith (dateformat : DateFormat) (modifier : Modifier) (data : TypeFormat modifier) : String := match modifier with | .G format => match format with | .short => formatEraShort dateformat.symbols data - | .full => formatEraLong dateformat.symbols data + | .full => formatEraLong dateformat.symbols data | .narrow => formatEraNarrow dateformat.symbols data + | .twoLetterShort => formatEraShort dateformat.symbols data | .y format => let info := data.toInt let info := if info ≤ 0 then -info + 1 else info match format with - | .any => pad 0 info + | .any => pad 0 info | .twoDigit => pad 2 (info % 100) | .fourDigit => pad 4 info | .extended n => pad n info | .u format => match format with - | .any => pad 0 (data.toInt) + | .any => pad 0 (data.toInt) | .twoDigit => pad 2 (data.toInt % 100) | .fourDigit => pad 4 data.toInt | .extended n => pad n data.toInt @@ -772,85 +326,121 @@ private def formatWith (dateformat : DateFormat) (modifier : Modifier) (data : T let info := data.toInt let info := if info ≤ 0 then -info + 1 else info match format with - | .any => pad 0 info + | .any => pad 0 info | .twoDigit => pad 2 (info % 100) | .fourDigit => pad 4 info | .extended n => pad n info | .D format => pad format.padding data.snd.val - | .MorL format => + | .M format | .L format => match format with - | .inl format => pad format.padding data.val + | .inl fmt => pad fmt.padding data.val | .inr .short => formatMonthShort dateformat.symbols data - | .inr .full => formatMonthLong dateformat.symbols data + | .inr .full => formatMonthLong dateformat.symbols data | .inr .narrow => formatMonthNarrow dateformat.symbols data + | .inr .twoLetterShort => formatMonthShort dateformat.symbols data | .d format => pad format.padding data.val - | .Qorq format => + | .Q format | .q format => match format with - | .inl format => pad format.padding data.val - | .inr .short => formatQuarterShort dateformat.symbols data - | .inr .full => formatQuarterLong dateformat.symbols data - | .inr .narrow => formatQuarterNumber data + | .inl fmt => pad fmt.padding data.val + | .inr .short => formatQuarterShort dateformat.symbols data + | .inr .full => formatQuarterLong dateformat.symbols data + | .inr .narrow => formatQuarterNarrow dateformat.symbols data + | .inr .twoLetterShort => formatQuarterNumber data | .w format => pad format.padding data.val | .W format => pad format.padding data.val | .E format => match format with - | .short => formatWeekdayShort dateformat.symbols data - | .full => formatWeekdayLong dateformat.symbols data + | .short => formatWeekdayShort dateformat.symbols data + | .full => formatWeekdayLong dateformat.symbols data | .narrow => formatWeekdayNarrow dateformat.symbols data - | .eorc format => + | .twoLetterShort => formatWeekdayTwoLetter dateformat.symbols data + | .e format | .c format => match format with - | .inl format => + | .inl fmt => let firstOrd : Int := dateformat.firstDayOfWeek.toOrdinal.val let dayOrd : Int := data.toOrdinal.val - pad format.padding ((dayOrd - firstOrd + 7) % 7 + 1) - | .inr .short => formatWeekdayShort dateformat.symbols data - | .inr .full => formatWeekdayLong dateformat.symbols data + pad fmt.padding ((dayOrd - firstOrd + 7) % 7 + 1) + | .inr .short => formatWeekdayShort dateformat.symbols data + | .inr .full => formatWeekdayLong dateformat.symbols data | .inr .narrow => formatWeekdayNarrow dateformat.symbols data + | .inr .twoLetterShort => formatWeekdayTwoLetter dateformat.symbols data | .F format => pad format.padding data.val | .a format => match format with - | .short => formatMarkerShort dateformat.symbols data - | .full => formatMarkerLong dateformat.symbols data + | .short => formatMarkerShort dateformat.symbols data + | .full => formatMarkerLong dateformat.symbols data | .narrow => formatMarkerNarrow dateformat.symbols data - | .h format => pad format.padding (data.val % 12) - | .K format => pad format.padding (data.val % 12) + | .twoLetterShort => formatMarkerShort dateformat.symbols data + | .b format => + match format with + | .short => formatDayPeriod dateformat.symbols.dayPeriodShort data + | .full => formatDayPeriod dateformat.symbols.dayPeriodLong data + | .narrow => formatDayPeriod dateformat.symbols.dayPeriodNarrow data + | .twoLetterShort => formatDayPeriod dateformat.symbols.dayPeriodShort data + | .B format => + match format with + | .short => formatExtendedDayPeriod dateformat.symbols.extendedDayPeriodShort data + | .full => formatExtendedDayPeriod dateformat.symbols.extendedDayPeriodLong data + | .narrow => formatExtendedDayPeriod dateformat.symbols.extendedDayPeriodNarrow data + | .twoLetterShort => formatExtendedDayPeriod dateformat.symbols.extendedDayPeriodShort data + | .h format => pad format.padding data.val + | .K format => pad format.padding data.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 - | .truncated n => rightTruncate n data.val (cut := true) + | .nano => pad 9 data.val + | .truncated n => + -- Pad to 9 digits first so truncation is from the left of the full nanosecond string + let s := leftPadAscii 9 '0' (toString data.val) + (s.take n).toString | .A format => pad format.padding data.val | .n format => pad format.padding data.val | .N format => pad format.padding data.val - | .V => data + | .V format => + match format with + | .unknown => "unk" + | .short => data + | .full => data | .z format => match format with | .short => data - | .full => data + | .full => data + | .v format => + match format with + | .short => data + | .full => data | .O format => match format with - | .short => s!"GMT{toSigned data.second.toHours.toInt}" - | .full => s!"GMT{toIsoString data true false true}" + | .short => + if data.second == 0 then "GMT" + else + let (sign, time) := if data.second.val ≥ 0 then ("+", data.second) else ("-", -data.second) + let t := PlainTime.ofSeconds time + let pad := leftPadAscii 2 '0' ∘ toString + if t.minute.val == 0 + then s!"GMT{sign}{t.hour.val}" + else s!"GMT{sign}{t.hour.val}:{pad t.minute.val}" + | .full => if data.second == 0 then "GMT" else s!"GMT{toIsoString data true false true}" | .X format => if data.second == 0 then "Z" else match format with - | .hour => toIsoString data false false false - | .hourMinute => toIsoString data true false false - | .hourMinuteColon => toIsoString data true false true - | .hourMinuteSecond => toIsoString data true true false + | .hour => toIsoString data false false false + | .hourMinute => toIsoString data true false false + | .hourMinuteColon => toIsoString data true false true + | .hourMinuteSecond => toIsoString data true true false | .hourMinuteSecondColon => toIsoString data true true true | .x format => match format with @@ -875,25 +465,28 @@ private def formatWith (dateformat : DateFormat) (modifier : Modifier) (data : T | .hourMinuteSecondColon => if data.second == 0 then "Z" - else toIsoString data true (data.second.val % 60 ≠ 0) true + else toIsoString data true (data.second.val % 60 ≠ 0) true -private def dateFromModifier (firstDay : Weekday) (date : DateTime) : TypeFormat modifier := +private def dateFromModifier (dateformat : DateFormat) (date : DateTime) : TypeFormat modifier := + let firstDay := dateformat.firstDayOfWeek + let minDays := dateformat.minimalDaysInFirstWeek let tz := date.timezone match modifier with | .G _ => date.era | .y _ => date.year | .u _ => date.year - | .Y _ => date.weekYear firstDay + | .Y _ => date.weekYear firstDay minDays | .D _ => Sigma.mk _ date.dayOfYear - | .MorL _ => date.month + | .M _ | .L _ => date.month | .d _ => date.day - | .Qorq _ => date.quarter - | .w _ => date.weekOfYear firstDay + | .Q _ | .q _ => date.quarter + | .w _ => date.weekOfYear firstDay minDays | .W _ => date.weekOfMonth firstDay - | .E _ => date.weekday - | .eorc _ => date.weekday + | .E _ | .e _ | .c _ => date.weekday | .F _ => date.alignedWeekOfMonth | .a _ => HourMarker.ofOrdinal date.hour + | .b _ => classifyDayPeriod date.hour date.minute date.date.get.time.second + | .B _ => classifyExtendedDayPeriod date.hour date.minute date.date.get.time.second | .h _ => HourMarker.toRelative date.hour |>.fst | .K _ => date.hour.emod 12 (by decide) | .k _ => date.hour.shiftTo1BasedHour @@ -904,9 +497,25 @@ private def dateFromModifier (firstDay : Weekday) (date : DateTime) : TypeFormat | .A _ => date.date.get.time.toMilliseconds | .n _ => date.nanosecond | .N _ => date.date.get.time.toNanoseconds - | .V => tz.name - | .z .short => tz.abbreviation - | .z .full => tz.name + | .V .unknown => "unk" + | .V .short => if tz.name.startsWith "+" || tz.name.startsWith "-" + then s!"GMT{toIsoString tz.offset true false true}" + else tz.name + | .V .full => if tz.name.startsWith "+" || tz.name.startsWith "-" + then s!"GMT{toIsoString tz.offset true false true}" + else tz.name + | .z .short => if tz.abbreviation.startsWith "+" || tz.abbreviation.startsWith "-" + then s!"GMT{toIsoString tz.offset true false true}" + else tz.abbreviation + | .z .full => if tz.name.startsWith "+" || tz.name.startsWith "-" + then s!"GMT{toIsoString tz.offset true false true}" + else tz.name + | .v .short => if tz.abbreviation.startsWith "+" || tz.abbreviation.startsWith "-" + then s!"GMT{toIsoString tz.offset true false true}" + else tz.abbreviation + | .v .full => if tz.name.startsWith "+" || tz.name.startsWith "-" + then s!"GMT{toIsoString tz.offset true false true}" + else tz.name | .O _ => tz.offset | .X _ => tz.offset | .x _ => tz.offset @@ -961,6 +570,9 @@ private def parseWeekdayShort (symbols : DateFormatSymbols) : Parser Weekday := private def parseWeekdayNarrow (symbols : DateFormatSymbols) : Parser Weekday := parseFromSymbols (weekdayPairs symbols.weekdayNarrow) +private def parseWeekdayTwoLetter (symbols : DateFormatSymbols) : Parser Weekday := + parseFromSymbols (weekdayPairs symbols.weekdayTwoLetter) + private def parseEraShort (symbols : DateFormatSymbols) : Parser Year.Era := parseFromSymbols (eraPairs symbols.eraShort) @@ -982,6 +594,9 @@ private def parseQuarterLong (symbols : DateFormatSymbols) : Parser Month.Quarte private def parseQuarterShort (symbols : DateFormatSymbols) : Parser Month.Quarter := parseFromSymbols (quarterPairs symbols.quarterShort) +private def parseQuarterNarrow (symbols : DateFormatSymbols) : Parser Month.Quarter := + parseFromSymbols (quarterPairs symbols.quarterNarrow) + private def parseMarkerShort (symbols : DateFormatSymbols) : Parser HourMarker := (pstring symbols.amShort *> pure .am) <|> (pstring symbols.pmShort *> pure .pm) @@ -991,6 +606,19 @@ private def parseMarkerLong (symbols : DateFormatSymbols) : Parser HourMarker := private def parseMarkerNarrow (symbols : DateFormatSymbols) : Parser HourMarker := (pstring symbols.amNarrow *> pure .am) <|> (pstring symbols.pmNarrow *> pure .pm) +private def parseDayPeriodFrom (dp : DayPeriodSymbols) : Parser DayPeriod := + pstring dp.midnight *> pure .midnight + <|> pstring dp.noon *> pure .noon + <|> pstring dp.am *> pure .am + <|> pstring dp.pm *> pure .pm + +private def parseExtendedDayPeriodFrom (arr : Vector String 6) : Parser ExtendedDayPeriod := + let pairs : Array (String × ExtendedDayPeriod) := #[ + (arr.get 0, .midnight), (arr.get 1, .night), (arr.get 2, .morning), + (arr.get 3, .noon), (arr.get 4, .afternoon), (arr.get 5, .evening) + ] + parseFromSymbols pairs + private def exactly (parse : Parser α) (size : Nat) : Parser (Array α) := let rec go (acc : Array α) (count : Nat) : Parser (Array α) := if count ≥ size then @@ -1082,65 +710,76 @@ private def parseOffset (withMinutes : Reason) (withSeconds : Reason) (withColon private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (TypeFormat mod) | .G format => match format with - | .short => parseEraShort config.dateformat.symbols - | .full => parseEraLong config.dateformat.symbols + | .short | .twoLetterShort => parseEraShort config.dateformat.symbols + | .full => parseEraLong config.dateformat.symbols | .narrow => parseEraNarrow config.dateformat.symbols | .y format => match format with - | .any => Int.ofNat <$> parseAtLeastNum 1 + | .any => Int.ofNat <$> parseAtLeastNum 1 | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2 | .fourDigit => Int.ofNat <$> parseNum 4 | .extended n => Int.ofNat <$> parseNum n | .u format => match format with - | .any => parseSigned <| parseAtLeastNum 1 + | .any => parseSigned <| parseAtLeastNum 1 | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2 | .fourDigit => parseSigned <| parseNum 4 | .extended n => parseSigned <| parseNum n | .Y format => match format with - | .any => parseSigned <| parseAtLeastNum 1 + | .any => parseSigned <| parseAtLeastNum 1 | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2 | .fourDigit => parseSigned <| parseNum 4 | .extended n => parseSigned <| parseNum n | .D format => Sigma.mk true <$> parseNatToBounded (parseFlexibleNum format.padding) - | .MorL format => + | .M format | .L format => match format with - | .inl format => parseNatToBounded (parseFlexibleNum format.padding) - | .inr .short => parseMonthShort config.dateformat.symbols - | .inr .full => parseMonthLong config.dateformat.symbols + | .inl fmt => parseNatToBounded (parseFlexibleNum fmt.padding) + | .inr .short | .inr .twoLetterShort => parseMonthShort config.dateformat.symbols + | .inr .full => parseMonthLong config.dateformat.symbols | .inr .narrow => parseMonthNarrow config.dateformat.symbols | .d format => parseNatToBounded (parseFlexibleNum format.padding) - | .Qorq format => + | .Q format | .q format => match format with - | .inl format => parseNatToBounded (parseFlexibleNum format.padding) + | .inl fmt => parseNatToBounded (parseFlexibleNum fmt.padding) | .inr .short => parseQuarterShort config.dateformat.symbols - | .inr .full => parseQuarterLong config.dateformat.symbols - | .inr .narrow => parseQuarterNumber + | .inr .full => parseQuarterLong config.dateformat.symbols + | .inr .narrow | .inr .twoLetterShort => parseQuarterNarrow config.dateformat.symbols | .w format => parseNatToBounded (parseFlexibleNum format.padding) | .W format => parseNatToBounded (parseFlexibleNum format.padding) | .E format => match format with - | .short => parseWeekdayShort config.dateformat.symbols - | .full => parseWeekdayLong config.dateformat.symbols + | .short | .twoLetterShort => parseWeekdayShort config.dateformat.symbols + | .full => parseWeekdayLong config.dateformat.symbols | .narrow => parseWeekdayNarrow config.dateformat.symbols - | .eorc format => + | .e format | .c format => match format with - | .inl format => do - let n ← parseFlexibleNum format.padding + | .inl fmt => do + let n ← parseFlexibleNum fmt.padding if ¬ (1 ≤ n ∧ n ≤ 7) then fail "need a natural number in the interval of 1 to 7" let firstOrd : Int := config.dateformat.firstDayOfWeek.toOrdinal.val let absOrd : Int := ((n : Int) - 1 + firstOrd - 1) % 7 + 1 return Weekday.ofOrdinal (Bounded.LE.ofNatWrapping absOrd (by decide)) | .inr .short => parseWeekdayShort config.dateformat.symbols - | .inr .full => parseWeekdayLong config.dateformat.symbols + | .inr .full => parseWeekdayLong config.dateformat.symbols | .inr .narrow => parseWeekdayNarrow config.dateformat.symbols + | .inr .twoLetterShort => parseWeekdayTwoLetter config.dateformat.symbols | .F format => parseNatToBounded (parseFlexibleNum format.padding) | .a format => match format with - | .short => parseMarkerShort config.dateformat.symbols - | .full => parseMarkerLong config.dateformat.symbols + | .short | .twoLetterShort => parseMarkerShort config.dateformat.symbols + | .full => parseMarkerLong config.dateformat.symbols | .narrow => parseMarkerNarrow config.dateformat.symbols + | .b format => + match format with + | .short | .twoLetterShort => parseDayPeriodFrom config.dateformat.symbols.dayPeriodShort + | .full => parseDayPeriodFrom config.dateformat.symbols.dayPeriodLong + | .narrow => parseDayPeriodFrom config.dateformat.symbols.dayPeriodNarrow + | .B format => + match format with + | .short | .twoLetterShort => parseExtendedDayPeriodFrom config.dateformat.symbols.extendedDayPeriodShort + | .full => parseExtendedDayPeriodFrom config.dateformat.symbols.extendedDayPeriodLong + | .narrow => parseExtendedDayPeriodFrom config.dateformat.symbols.extendedDayPeriodNarrow | .h format => parseNatToBounded (parseFlexibleNum format.padding) | .K format => parseNatToBounded (parseFlexibleNum format.padding) | .k format => parseNatToBounded (parseFlexibleNum format.padding) @@ -1154,27 +793,32 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ return res.expandTop (by decide) | .S format => match format with - | .nano => parseNatToBounded (parseFlexibleNum 9) + | .nano => parseNatToBounded (parseFlexibleNum 9) | .truncated n => parseNatToBounded (parseFractionNum n 9) | .A format => Millisecond.Offset.ofNat <$> (parseFlexibleNum format.padding) | .n format => parseNatToBounded (parseFlexibleNum format.padding) | .N format => Nanosecond.Offset.ofNat <$> (parseFlexibleNum format.padding) - | .V => parseIdentifier + | .V format => + match format with + | .unknown => pstring "unk" *> pure "unk" + | .short | .full => parseIdentifier | .z format => match format with - | .short => parseIdentifier - | .full => parseIdentifier + | .short | .full => parseIdentifier + | .v format => + match format with + | .short | .full => parseIdentifier | .O format => match format with | .short => pstring "GMT" *> parseOffset .no .no false - | .full => pstring "GMT" *> parseOffset .yes .optional false + | .full => pstring "GMT" *> parseOffset .yes .optional false | .X format => let p : Parser Offset := match format with - | .hour => parseOffset .no .no false - | .hourMinute => parseOffset .yes .no false - | .hourMinuteColon => parseOffset .yes .no true - | .hourMinuteSecond => parseOffset .yes .yes false + | .hour => parseOffset .no .no false + | .hourMinute => parseOffset .yes .no false + | .hourMinuteColon => parseOffset .yes .no true + | .hourMinuteSecond => parseOffset .yes .yes false | .hourMinuteSecondColon => parseOffset .yes .yes true p <|> (pstring "Z" *> pure (Offset.ofSeconds 0)) | .x format => @@ -1203,7 +847,7 @@ private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (Typ private def formatPartWithDate (dateformat : DateFormat) (date : DateTime) (part : FormatPart) : String := match part with - | .modifier mod => formatWith dateformat mod (dateFromModifier dateformat.firstDayOfWeek date) + | .modifier mod => formatWith dateformat mod (dateFromModifier dateformat date) | .string s => s set_option linter.missingDocs false in -- TODO @@ -1216,89 +860,114 @@ def FormatType (result : Type) : FormatString → Type namespace GenericFormat private structure DateBuilder where - G : Option Year.Era := none - y : Option Year.Offset := none - u : Option Year.Offset := none - Y : Option Year.Offset := none - D : Option (Sigma Day.Ordinal.OfYear) := none - MorL : Option Month.Ordinal := none - d : Option Day.Ordinal := none - Qorq : Option Month.Quarter := none - w : Option Week.OfYear.Ordinal := none - W : Option Week.Ordinal := none - E : Option Weekday := none - eorc : Option Weekday := none - F : Option (Bounded.LE 1 5) := none - a : Option HourMarker := none - h : Option (Bounded.LE 1 12) := none - K : Option (Bounded.LE 0 11) := none - k : Option (Bounded.LE 1 24) := none - H : Option Hour.Ordinal := none - m : Option Minute.Ordinal := none - s : Option (Second.Ordinal true) := none - S : Option Nanosecond.Ordinal := none - A : Option Millisecond.Offset := none - n : Option Nanosecond.Ordinal := none - N : Option Nanosecond.Offset := none - V : Option String := none - z : Option String := none + G : Option Year.Era := none + y : Option Year.Offset := none + u : Option Year.Offset := none + Y : Option Year.Offset := none + D : Option (Sigma Day.Ordinal.OfYear) := none + M : Option Month.Ordinal := none + L : Option Month.Ordinal := none + d : Option Day.Ordinal := none + Q : Option Month.Quarter := none + q : Option Month.Quarter := none + w : Option Week.OfYear.Ordinal := none + W : Option Week.Ordinal := none + E : Option Weekday := none + e : Option Weekday := none + c : Option Weekday := none + F : Option (Bounded.LE 1 5) := none + a : Option HourMarker := none + b : Option DayPeriod := none + B : Option ExtendedDayPeriod := none + h : Option (Bounded.LE 1 12) := none + K : Option (Bounded.LE 0 11) := none + k : Option (Bounded.LE 1 24) := none + H : Option Hour.Ordinal := none + m : Option Minute.Ordinal := none + s : Option (Second.Ordinal true) := none + S : Option Nanosecond.Ordinal := none + A : Option Millisecond.Offset := none + n : Option Nanosecond.Ordinal := none + N : Option Nanosecond.Offset := none + V : Option String := none + z : Option String := none zabbrev : Option String := none - O : Option Offset := none - X : Option Offset := none - x : Option Offset := none - Z : Option Offset := none + v : Option String := none + O : Option Offset := none + X : Option Offset := none + x : Option Offset := none + Z : Option Offset := none namespace DateBuilder private def insert (date : DateBuilder) (modifier : Modifier) (data : TypeFormat modifier) : DateBuilder := match modifier with - | .G _ => { date with G := some data } - | .y _ => { date with y := some data } - | .u _ => { date with u := some data } - | .Y _ => { date with Y := some data } - | .D _ => { date with D := some data } - | .MorL _ => { date with MorL := some data } - | .d _ => { date with d := some data } - | .Qorq _ => { date with Qorq := some data } - | .w _ => { date with w := some data } - | .W _ => { date with W := some data } - | .E _ => { date with E := some data } - | .eorc _ => { date with eorc := some data } - | .F _ => { date with F := some data } - | .a _ => { date with a := some data } - | .h _ => { date with h := some data } - | .K _ => { date with K := some data } - | .k _ => { date with k := some data } - | .H _ => { date with H := some data } - | .m _ => { date with m := some data } - | .s _ => { date with s := some data } - | .S _ => { date with S := some data } - | .A _ => { date with A := some data } - | .n _ => { date with n := some data } - | .N _ => { date with N := some data } - | .V => { date with V := some data } - | .z .full => { date with z := some data } - | .z .short => { date with zabbrev := some data } - | .O _ => { date with O := some data } - | .X _ => { date with X := some data } - | .x _ => { date with x := some data } - | .Z _ => { date with Z := some data } + | .G _ => { date with G := some data } + | .y _ => { date with y := some data } + | .u _ => { date with u := some data } + | .Y _ => { date with Y := some data } + | .D _ => { date with D := some data } + | .M _ => { date with M := some data } + | .L _ => { date with L := some data } + | .d _ => { date with d := some data } + | .Q _ => { date with Q := some data } + | .q _ => { date with q := some data } + | .w _ => { date with w := some data } + | .W _ => { date with W := some data } + | .E _ => { date with E := some data } + | .e _ => { date with e := some data } + | .c _ => { date with c := some data } + | .F _ => { date with F := some data } + | .a _ => { date with a := some data } + | .b _ => { date with b := some data } + | .B _ => { date with B := some data } + | .h _ => { date with h := some data } + | .K _ => { date with K := some data } + | .k _ => { date with k := some data } + | .H _ => { date with H := some data } + | .m _ => { date with m := some data } + | .s _ => { date with s := some data } + | .S _ => { date with S := some data } + | .A _ => { date with A := some data } + | .n _ => { date with n := some data } + | .N _ => { date with N := some data } + | .V .full => { date with V := some data } + | .V .short => { date with V := some data } + | .V .unknown => { date with V := some data } + | .z .full => { date with z := some data } + | .z .short => { date with zabbrev := some data } + | .v .full => { date with v := some data } + | .v .short => { date with v := some data } + | .O _ => { date with O := some data } + | .X _ => { date with X := some data } + | .x _ => { date with x := some data } + | .Z _ => { date with Z := some data } private def convertYearAndEra (year : Year.Offset) : Year.Era → Year.Offset | .ce => year | .bce => -(year + 1) +/-- Infer an `HourMarker` from a `DayPeriod` parsed by `b`. -/ +private def markerOfDayPeriod : DayPeriod → HourMarker + | .am | .midnight => .am + | .pm | .noon => .pm + +/-- Infer an `HourMarker` from an `ExtendedDayPeriod` parsed by `B`. -/ +private def markerOfExtendedDayPeriod : ExtendedDayPeriod → HourMarker + | .midnight | .night | .morning => .am + | .noon | .afternoon | .evening => .pm + private def build (builder : DateBuilder) (aw : Awareness) : Option DateTime := let offset := builder.O <|> builder.X <|> builder.x <|> builder.Z |>.getD Offset.zero let tz : TimeZone := { offset, - name := builder.V <|> builder.z |>.getD (offset.toIsoString true), + name := builder.V <|> builder.v <|> builder.z |>.getD (offset.toIsoString true), abbreviation := builder.zabbrev |>.getD (offset.toIsoString true), isDST := false, } - let month := builder.MorL |>.getD 0 + let month := builder.M <|> builder.L |>.getD 0 let day := builder.d |>.getD 0 let era := (builder.G.getD .ce) @@ -1308,8 +977,14 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option DateTime := <|> builder.Y |>.getD 0 + -- Derive hour marker from `a`, then fall back to `b` and `B`. + let markerOpt : Option HourMarker := + builder.a + <|> (markerOfDayPeriod <$> builder.b) + <|> (markerOfExtendedDayPeriod <$> builder.B) + let hour : Option (Bounded.LE 0 23) := - if let some marker := builder.a then + if let some marker := markerOpt then marker.toAbsolute <$> builder.h <|> marker.toAbsolute <$> ((Bounded.LE.add · 1) <$> builder.K) else diff --git a/src/Std/Time/Format/DateFormat.lean b/src/Std/Time/Format/DateFormat.lean index 56ab5cd63edc..d349b0c7d975 100644 --- a/src/Std/Time/Format/DateFormat.lean +++ b/src/Std/Time/Format/DateFormat.lean @@ -14,8 +14,24 @@ public section namespace Std namespace Time +open Internal + set_option linter.all true +/-- +`DayPeriodSymbols` holds the four locale strings used by the `b` pattern: AM, PM, noon, midnight. +-/ +structure DayPeriodSymbols where + /-- AM string (e.g., "AM"). -/ + am : String + /-- PM string (e.g., "PM"). -/ + pm : String + /-- Noon string (e.g., "noon"). -/ + noon : String + /-- Midnight string (e.g., "midnight"). -/ + midnight : String + deriving Repr, Inhabited + /-- `DateFormatSymbols` contains locale-specific strings needed for date/time formatting and parsing. -/ @@ -51,6 +67,12 @@ structure DateFormatSymbols where -/ weekdayNarrow : Vector String 7 + /-- + Two-letter abbreviated weekday names (7 elements, index 0 = Mo). + Used by `EEEEEE`, `eeeeee`, `cccccc`. + -/ + weekdayTwoLetter : Vector String 7 + /-- Short era names (2 elements: index 0 = BCE, index 1 = CE). -/ @@ -82,59 +104,102 @@ structure DateFormatSymbols where quarterNarrow : Vector String 4 /-- - Short AM marker. + Short AM marker (used by `a`/`aa`/`aaa`). -/ amShort : String /-- - Short PM marker. + Short PM marker (used by `a`/`aa`/`aaa`). -/ pmShort : String /-- - Full AM marker. + Full AM marker (used by `aaaa`). Typically lowercase per CLDR ("ante meridiem"). -/ amLong : String /-- - Full PM marker. + Full PM marker (used by `aaaa`). Typically lowercase per CLDR ("post meridiem"). -/ pmLong : String /-- - Narrow AM marker. + Narrow AM marker (used by `aaaaa`). -/ amNarrow : String /-- - Narrow PM marker. + Narrow PM marker (used by `aaaaa`). -/ pmNarrow : String + /-- + Short day-period strings for the `b` pattern (AM, PM, noon, midnight). + Used by `b`/`bb`/`bbb`. + -/ + dayPeriodShort : DayPeriodSymbols + + /-- + Full day-period strings for the `b` pattern (AM, PM, noon, midnight). + Used by `bbbb`. Per TR35, AM/PM here are lowercase ("ante meridiem" / "post meridiem"). + -/ + dayPeriodLong : DayPeriodSymbols + + /-- + Narrow day-period strings for the `b` pattern (AM, PM, noon, midnight). + Used by `bbbbb`. + -/ + dayPeriodNarrow : DayPeriodSymbols + + /-- + Short extended-day-period strings for the `B` pattern (CLDR flexible day periods). + Order: midnight, night, morning, noon, afternoon, evening. + -/ + extendedDayPeriodShort : Vector String 6 + + /-- + Full extended-day-period strings for the `B` pattern. + Order: midnight, night, morning, noon, afternoon, evening. + -/ + extendedDayPeriodLong : Vector String 6 + + /-- + Narrow extended-day-period strings for the `B` pattern. + Order: midnight, night, morning, noon, afternoon, evening. + -/ + extendedDayPeriodNarrow : Vector String 6 + namespace DateFormatSymbols /-- English (US) locale symbols. -/ def enUS : DateFormatSymbols where - monthLong := Vector.mk #["January", "February", "March", "April", "May", "June", "July", "August", "September", "October", "November", "December"] (by decide) - monthShort := Vector.mk #["Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"] (by decide) - monthNarrow := Vector.mk #["J", "F", "M", "A", "M", "J", "J", "A", "S", "O", "N", "D"] (by decide) - weekdayLong := Vector.mk #["Monday", "Tuesday", "Wednesday", "Thursday", "Friday", "Saturday", "Sunday"] (by decide) - weekdayShort := Vector.mk #["Mon", "Tue", "Wed", "Thu", "Fri", "Sat", "Sun"] (by decide) - weekdayNarrow := Vector.mk #["M", "T", "W", "T", "F", "S", "S"] (by decide) - eraShort := Vector.mk #["BCE", "CE"] (by decide) - eraLong := Vector.mk #["Before Common Era", "Common Era"] (by decide) - eraNarrow := Vector.mk #["B", "C"] (by decide) - quarterShort := Vector.mk #["Q1", "Q2", "Q3", "Q4"] (by decide) - quarterLong := Vector.mk #["1st quarter", "2nd quarter", "3rd quarter", "4th quarter"] (by decide) - quarterNarrow := Vector.mk #["1", "2", "3", "4"] (by decide) - amShort := "AM" - pmShort := "PM" - amLong := "Ante Meridiem" - pmLong := "Post Meridiem" - amNarrow := "A" - pmNarrow := "P" + monthLong := Vector.mk #["January", "February", "March", "April", "May", "June", "July", "August", "September", "October", "November", "December"] (by decide) + monthShort := Vector.mk #["Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"] (by decide) + monthNarrow := Vector.mk #["J", "F", "M", "A", "M", "J", "J", "A", "S", "O", "N", "D"] (by decide) + weekdayLong := Vector.mk #["Monday", "Tuesday", "Wednesday", "Thursday", "Friday", "Saturday", "Sunday"] (by decide) + weekdayShort := Vector.mk #["Mon", "Tue", "Wed", "Thu", "Fri", "Sat", "Sun"] (by decide) + weekdayNarrow := Vector.mk #["M", "T", "W", "T", "F", "S", "S"] (by decide) + weekdayTwoLetter := Vector.mk #["Mo", "Tu", "We", "Th", "Fr", "Sa", "Su"] (by decide) + eraShort := Vector.mk #["BC", "AD"] (by decide) + eraLong := Vector.mk #["Before Christ", "Anno Domini"] (by decide) + eraNarrow := Vector.mk #["B", "A"] (by decide) + quarterShort := Vector.mk #["Q1", "Q2", "Q3", "Q4"] (by decide) + quarterLong := Vector.mk #["1st quarter", "2nd quarter", "3rd quarter", "4th quarter"] (by decide) + quarterNarrow := Vector.mk #["1", "2", "3", "4"] (by decide) + amShort := "AM" + pmShort := "PM" + amLong := "ante meridiem" + pmLong := "post meridiem" + amNarrow := "a" + pmNarrow := "p" + dayPeriodShort := { am := "AM", pm := "PM", noon := "noon", midnight := "midnight" } + dayPeriodLong := { am := "ante meridiem", pm := "post meridiem", noon := "noon", midnight := "midnight" } + dayPeriodNarrow := { am := "a", pm := "p", noon := "n", midnight := "mi" } + extendedDayPeriodShort := Vector.mk #["midnight", "at night", "in the morning", "noon", "in the afternoon", "in the evening"] (by decide) + extendedDayPeriodLong := Vector.mk #["midnight", "at night", "in the morning", "noon", "in the afternoon", "in the evening"] (by decide) + extendedDayPeriodNarrow := Vector.mk #["mi", "night", "morning", "n", "afternoon", "evening"] (by decide) end DateFormatSymbols @@ -149,6 +214,13 @@ structure DateFormat where -/ firstDayOfWeek : Weekday + /-- + The minimum number of days that a week must have in the new year to count as week 1. + ISO 8601 uses 4 (week 1 must contain the first Thursday); US locale uses 1 (any week + containing Jan 1 is week 1). + -/ + minimalDaysInFirstWeek : Bounded.LE 0 6 + /-- Locale-specific symbols used for formatting and parsing text fields. -/ @@ -161,6 +233,7 @@ English (US) locale. -/ def enUS : DateFormat where firstDayOfWeek := .sunday + minimalDaysInFirstWeek := Bounded.LE.mk 1 (by decide) symbols := DateFormatSymbols.enUS end DateFormat diff --git a/src/Std/Time/Format/Modifier.lean b/src/Std/Time/Format/Modifier.lean new file mode 100644 index 000000000000..b21e9230d355 --- /dev/null +++ b/src/Std/Time/Format/Modifier.lean @@ -0,0 +1,809 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sofia Rodrigues +-/ +module + +prelude +public import Std.Time.Zoned +import Init.Data.String.Search + +public section + +/-! +This module defines the `Modifier` type and its sub-types, representing format pattern letters. +-/ + +namespace Std +namespace Time +open Internal +open Std.Internal.Parsec.String +open Std.Internal.Parsec Lean PlainTime PlainDate TimeZone DateTime + +set_option linter.all true + +/-- +`Text` represents different text formatting styles. +-/ +inductive Text + + /-- + Short form (e.g., "Tue") + -/ + | short + + /-- + Full form (e.g., "Tuesday") + -/ + | full + + /-- + Narrow form (e.g., "T") + -/ + | narrow + + /-- + Two-letter short form (e.g., "Tu"). Produced only by 6-letter weekday patterns (`EEEEEE`, `eeeeee`, `cccccc`). + -/ + | twoLetterShort + deriving Repr, Inhabited + +namespace Text + +/-- +`classify` classifies the number of pattern letters into a `Text` type. +-/ +def classify (num : Nat) : Option Text := + if num < 4 then + some (.short) + else if num = 4 then + some (.full) + else if num = 5 then + some (.narrow) + else + none + +end Text + +/-- +`Number` represents different number formatting styles. +-/ +structure Number where + + /-- + Minimum number of digits; output is zero-padded on the left to reach this width. Determined by the count of pattern letters. + -/ + padding : Nat + deriving Repr, Inhabited + +/-- +`classifyNumberText` classifies the number of pattern letters into either a `Number` or `Text`. +-/ +def classifyNumberText : Nat → Option (Number ⊕ Text) + | n => if n < 3 then some (.inl ⟨n⟩) else .inr <$> (Text.classify n) + +/-- +`Fraction` represents the fraction of a second, which can either be full nanoseconds +or a truncated form with fewer digits. +-/ +inductive Fraction + + /-- + Nanosecond precision (up to 9 digits) + -/ + | nano + + /-- + Truncated to `digits` digits (truncated, not rounded) + -/ + | truncated (digits : Nat) + deriving Repr, Inhabited + +namespace Fraction + +/-- +`classify` classifies the number of pattern letters into either a `Fraction`. It's used for `nano`. +-/ +def classify (nat : Nat) : Option Fraction := + if nat < 9 then + some (.truncated nat) + else if nat = 9 then + some (.nano) + else + none + +end Fraction + +/-- +`Year` represents different year formatting styles based on the number of pattern letters. +-/ +inductive Year + + /-- + Any size (e.g., "19000000000000") + -/ + | any + + /-- + Two-digit year format (e.g., "23" for 2023) + -/ + | twoDigit + + /-- + Four-digit year format (e.g., "2023") + -/ + | fourDigit + + /-- + Extended year format for more than 4 digits (e.g., "002023") + -/ + | extended (num : Nat) + deriving Repr, Inhabited + +namespace Year + +/-- +`classify` classifies the number of pattern letters into a `Year` format. +-/ +def classify (num : Nat) : Option Year := + if num = 1 then + some .any + else if num = 2 then + some .twoDigit + else if num = 4 then + some .fourDigit + else if num > 4 ∨ num = 3 then + some (.extended num) + else + none + +end Year + +/-- +`ZoneId` represents different time zone ID formats based on the number of pattern letters. +-/ +inductive ZoneId + + /-- + Unknown zone placeholder (1 letter, `V`): always formats as "unk". + -/ + | unknown + + /-- + IANA time zone ID (2 letters, `VV`, e.g., "America/Los_Angeles"). + -/ + | short + + /-- + Reserved for a future generic location format (`VVVV`). Currently formatted identically to `short`. + -/ + | full + deriving Repr, Inhabited + +namespace ZoneId + +/-- +`classify` classifies the number of pattern letters into a `ZoneId` format. +- If 1 letter, it returns the unknown form. +- If 2 letters, it returns the short form. +- If 4 letters, it returns the full form. +- Otherwise, it returns none. +-/ +def classify (num : Nat) : Option ZoneId := + if num = 1 then + some (.unknown) + else if num = 2 then + some (.short) + else if num = 4 then + some (.full) + else + none + +end ZoneId + +/-- +`ZoneName` represents different zone name formats based on the number of pattern letters and +whether daylight saving time is considered. +-/ +inductive ZoneName + /-- + Short form of zone name (e.g., "PST") + -/ + | short + /-- + Full form of zone name (e.g., "Pacific Standard Time") + -/ + | full + deriving Repr, Inhabited + +namespace ZoneName + +/-- +`classify` classifies the number of pattern letters and the letter type ('z' or 'v') +into a `ZoneName` format. +- For 'z', if less than 4 letters, it returns the short form; if 4 letters, it returns the full form. +- For 'v', if 1 letter, it returns the short form; if 4 letters, it returns the full form. +- Otherwise, it returns none. +-/ +def classify (letter : Char) (num : Nat) : Option ZoneName := + if letter = 'z' then + if num < 4 then + some (.short) + else if num = 4 then + some (.full) + else + none + else if letter = 'v' then + if num = 1 then + some (.short) + else if num = 4 then + some (.full) + else + none + else + none + +end ZoneName + +/-- +`OffsetX` represents different offset formats based on the number of pattern letters. +The output will vary between the number of pattern letters, whether it's the hour, minute, second, +and whether colons are used. +-/ +inductive OffsetX + + /-- + Only the hour is output (e.g., "+01") + -/ + | hour + + /-- + Hour and minute without colon (e.g., "+0130") + -/ + | hourMinute + + /-- + Hour and minute with colon (e.g., "+01:30") + -/ + | hourMinuteColon + + /-- + Hour, minute, and second without colon (e.g., "+013015") + -/ + | hourMinuteSecond + + /-- + Hour, minute, and second with colon (e.g., "+01:30:15") + -/ + | hourMinuteSecondColon + deriving Repr, Inhabited + +namespace OffsetX + +/-- +`classify` classifies the number of pattern letters into an `OffsetX` format. +-/ +def classify (num : Nat) : Option OffsetX := + if num = 1 then + some (.hour) + else if num = 2 then + some (.hourMinute) + else if num = 3 then + some (.hourMinuteColon) + else if num = 4 then + some (.hourMinuteSecond) + else if num = 5 then + some (.hourMinuteSecondColon) + else + none + +end OffsetX + +/-- +`OffsetO` represents localized offset text formats based on the number of pattern letters. +-/ +inductive OffsetO + + /-- + Short form of the localized offset (e.g., "GMT+8") + -/ + | short + + /-- + Full form of the localized offset (e.g., "GMT+08:00") + -/ + | full + deriving Repr, Inhabited + +namespace OffsetO + +/-- +`classify` classifies the number of pattern letters into an `OffsetO` format. +-/ +def classify (num : Nat) : Option OffsetO := + match num with + | 1 => some (.short) + | 4 => some (.full) + | _ => none + +end OffsetO + +/-- +`OffsetZ` represents different offset formats based on the number of pattern letters (capital 'Z'). +-/ +inductive OffsetZ + + /-- + Hour and minute without colon, with optional seconds (e.g., "+0130", "+013015") + -/ + | hourMinute + + /-- + Localized offset text in full form (e.g., "GMT+08:00") + -/ + | full + + /-- + Hour and minute with colon, with optional seconds, and "Z" for zero offset (e.g., "+01:30", "+01:30:15", "Z") + -/ + | hourMinuteSecondColon + deriving Repr, Inhabited + +namespace OffsetZ + +/-- +`classify` classifies the number of pattern letters into an `OffsetZ` format. +-/ +def classify (num : Nat) : Option OffsetZ := + match num with + | 1 | 2 | 3 => some (.hourMinute) + | 4 => some (.full) + | 5 => some (.hourMinuteSecondColon) + | _ => none + +end OffsetZ + +/-- +`DayPeriod` extends `HourMarker` with exact noon and midnight values, used by the `b` pattern. +-/ +inductive DayPeriod + + /-- + Ante meridiem (before noon) + -/ + | am + + /-- + Post meridiem (after noon) + -/ + | pm + + /-- + Exactly noon (12:00:00) + -/ + | noon + + /-- + Exactly midnight (00:00:00) + -/ + | midnight + deriving Repr, Inhabited + +/-- +`ExtendedDayPeriod` is a more granular day-period classification used by the `B` pattern, +subdividing the day into named English CLDR segments. +-/ +inductive ExtendedDayPeriod + + /-- + Exactly 00:00:00 + -/ + | midnight + + /-- + 21:00–06:00 (exclusive of midnight) + -/ + | night + + /-- + 06:00–12:00 + -/ + | morning + + /-- + Exactly 12:00:00 + -/ + | noon + + /-- + 12:00–18:00 + -/ + | afternoon + + /-- + 18:00–21:00 + -/ + | evening + deriving Repr, Inhabited + +/-- +`Modifier` represents a single format pattern letter with its presentation style. + +The table below lists every symbol, its `presentation` type, the `TypeFormat` value type produced +when parsing or consumed when formatting, and representative output examples. + +``` +Symbol Meaning Presentation TypeFormat Examples +────────────────────────────────────────────────────────────────────────────────────────────────── +G era Text Year.Era AD; Anno Domini; A +u year (proleptic/astronomical) Year Year.Offset 2004; 04; -0001; -1 +y year-of-era Year Year.Offset 2004; 04; 0002; 2 +D day-of-year Number Σ Day.Ordinal.OfYear 189 +M/L month-of-year Number ⊕ Text Month.Ordinal 7; 07; Jul; July; J +d day-of-month Number Day.Ordinal 10 +────────────────────────────────────────────────────────────────────────────────────────────────── +Q/q quarter-of-year Number ⊕ Text Month.Quarter 3; 03; Q3; 3rd quarter +Y week-based-year Year Year.Offset 1996; 96 +w week-of-week-based-year Number Week.Ordinal 27 +W week-of-month Number Week.Ordinal.OfMonth 4 +E day-of-week (text only) Text Weekday Tue; Tuesday; T +e/c localized day-of-week Number ⊕ Text Weekday 2; 02; Tue; Tuesday; T +F day-of-week-in-month Number Bounded.LE 1 5 3 +────────────────────────────────────────────────────────────────────────────────────────────────── +a am-pm-of-day Text HourMarker AM; PM +b day-period (noon/midnight) Text DayPeriod AM; noon; midnight +B extended day period Text ExtendedDayPeriod in the morning; at night +h clock-hour-of-am-pm (1-12) Number Bounded.LE 1 12 12 +K hour-of-am-pm (0-11) Number Bounded.LE 0 11 0 +k clock-hour-of-day (1-24) Number Bounded.LE 1 24 24 +────────────────────────────────────────────────────────────────────────────────────────────────── +H hour-of-day (0-23) Number Hour.Ordinal 0 +m minute-of-hour Number Minute.Ordinal 30 +s second-of-minute Number Second.Ordinal true 55 +S fraction-of-second Fraction Nanosecond.Ordinal 978 +A milli-of-day Number Millisecond.Offset 1234 +n nano-of-second Number Nanosecond.Ordinal 987654321 +N nano-of-day Number Nanosecond.Offset 1234000000 +────────────────────────────────────────────────────────────────────────────────────────────────── +V time-zone ID ZoneId String America/Los_Angeles; Z +z time-zone name ZoneName String Pacific Standard Time; PST +v generic zone name ZoneName String Pacific Time; PT +O localized zone-offset OffsetO Offset GMT+8; GMT+08:00 +X zone-offset ('Z' for zero) OffsetX Offset Z; -08; -0830; -08:30 +x zone-offset OffsetX Offset +0000; -08; -0830; -08:30 +Z zone-offset OffsetZ Offset +0000; -0800; -08:00 +``` +-/ +inductive Modifier + /-- + `G`: Era (e.g., AD, Anno Domini, A). + -/ + | G (presentation : Text) + + /-- + `u`: Proleptic/astronomical year (e.g., 2004, 04, -0001, -1). Can be negative: year 0 exists and -0001 = 2 BC. + Use `y` + `G` instead when you want the era-based (always-positive) representation. + -/ + | u (presentation : Year) + + /-- + `y`: Year of era (e.g., 2004, 04, 0002, 2). Never negative: year 1 BC is formatted as `1` paired with a BC era + designator. Use `u` instead when you need the proleptic/astronomical year (which can be negative). + -/ + | y (presentation : Year) + + /-- + `D`: Day of year (e.g., 189). + -/ + | D (presentation : Number) + + /-- + `M`: Month of year as number or text (e.g., 7, 07, Jul, July, J). + -/ + | M (presentation : Number ⊕ Text) + + /-- + `L`: Stand-alone month of year as number or text (e.g., 7, 07, Jul, July, J). + Stand-alone means the month is used independently (e.g., a calendar header "July") rather than as part of a full date. + In practice the output is the same as `M`; the distinction is meaningful only in locale-aware contexts. + -/ + | L (presentation : Number ⊕ Text) + + /-- + `d`: Day of month (e.g., 10). + -/ + | d (presentation : Number) + + /-- + `Q`: Quarter of year as number or text (e.g., 3, 03, Q3, 3rd quarter). + -/ + | Q (presentation : Number ⊕ Text) + + /-- + `q`: Stand-alone quarter of year as number or text (e.g., 3, 03, Q3, 3rd quarter). + Stand-alone means the value is used independently (e.g., a calendar header) rather than as part of a full date phrase. + In practice the output is the same as `Q`; the distinction is meaningful only in locale-aware contexts. + -/ + | q (presentation : Number ⊕ Text) + + /-- + `Y`: ISO week-based year (e.g., 2004, 04, 0002, 2). This is the year that contains the ISO week (`w`), which can + differ from the calendar year near year boundaries: e.g., Dec 31 may belong to week 1 of the following year. + -/ + | Y (presentation : Year) + + /-- + `w`: Week of week-based year (e.g., 27). + -/ + | w (presentation : Number) + + /-- + `W`: Week of month (e.g., 4). + -/ + | W (presentation : Number) + + /-- + `E`: Day of week as text (e.g., Tue, Tuesday, T). + -/ + | E (presentation : Text) + + /-- + `e`: Day of week as number or text (e.g., 1, 01, Mon, Monday, M). + The numeric value uses Monday=1 through Sunday=7 (ISO 8601 convention). + Text output is the same as `E`. + -/ + | e (presentation : Number ⊕ Text) + + /-- + `c`: Stand-alone day of week as number or text (e.g., 2, Tue, Tuesday, T). + Stand-alone means the day is used independently (e.g., a calendar column header) rather than as part of a full date. + Unlike `e`, `cc` (count of 2) is not valid; the minimum is `c` (1 letter) or `ccc` (3 letters). + -/ + | c (presentation : Number ⊕ Text) + + /-- + `F`: Day-of-week-in-month / occurrence of the weekday within the month (e.g., 2nd Sunday -> 2). + -/ + | F (presentation : Number) + + /-- + `a`: AM/PM of day (e.g., PM). + -/ + | a (presentation : Text) + + /-- + `b`: Day period with noon/midnight distinction (e.g., AM, noon, midnight). + -/ + | b (presentation : Text) + + /-- + `B`: Extended day period with named segments (e.g., "in the morning", "at night"). + -/ + | B (presentation : Text) + + /-- + `h`: Clock hour of AM/PM (1-12) (e.g., 12). + -/ + | h (presentation : Number) + + /-- + `K`: Hour of AM/PM (0-11) (e.g., 0). + -/ + | K (presentation : Number) + + /-- + `k`: Clock hour of day (1-24) (e.g., 24). + -/ + | k (presentation : Number) + + /-- + `H`: Hour of day (0-23) (e.g., 0). + -/ + | H (presentation : Number) + + /-- + `m`: Minute of hour (e.g., 30). + -/ + | m (presentation : Number) + + /-- + `s`: Second of minute (e.g., 55). + -/ + | s (presentation : Number) + + /-- + `S`: Fraction of second (e.g., 978). + -/ + | S (presentation : Fraction) + + /-- + `A`: Millisecond of day (e.g., 1234). + -/ + | A (presentation : Number) + + /-- + `n`: Nanosecond of second (e.g., 987654321). + -/ + | n (presentation : Number) + + /-- + `N`: Nanosecond of day (e.g., 1234000000). + -/ + | N (presentation : Number) + + /-- + `V`: Time zone ID. + - `V` (1 letter): outputs `"unk"` (unknown zone placeholder per Unicode CLDR). + - `VV` (2 letters): outputs the IANA zone ID (e.g., `"America/Los_Angeles"`), or `"Z"` for UTC. + -/ + | V (presentation : ZoneId) + + /-- + `z`: Time zone name (e.g., Pacific Standard Time, PST). + -/ + | z (presentation : ZoneName) + + /-- + `v`: Generic time zone name, without DST distinction (e.g., Pacific Time, PT). + -/ + | v (presentation : ZoneName) + + /-- + `O`: Localized zone offset using the `GMT` prefix (e.g., `GMT+8`, `GMT+08:00`). + -/ + | O (presentation : OffsetO) + + /-- + `X`: Zone offset with 'Z' for zero (e.g., Z, -08, -0830, -08:30). + -/ + | X (presentation : OffsetX) + + /-- + `x`: Zone offset without 'Z' (e.g., +0000, -08, -0830, -08:30). + -/ + | x (presentation : OffsetX) + + /-- + `Z`: Zone offset. + - `Z`, `ZZ`, `ZZZ`: output `±HHMMss` (no colon); parse `±HHMM[ss]`. Does **not** accept the literal `Z` character for UTC — use `ZZZZZ` or `XXX` for that. + - `ZZZZ`: outputs/parses localized GMT form (e.g., `GMT+08:00`). + - `ZZZZZ`: outputs `±HH:mm[:ss]` and uses `Z` for UTC (e.g., `Z`, `+01:30`). + -/ + | Z (presentation : OffsetZ) + deriving Repr, Inhabited + +/-- +`abstractParse` abstracts the parsing logic for any type that has a classify function. +It takes a constructor function to build the `Modifier` and a classify function that maps the pattern length to a specific type. +-/ +private def parseMod (constructor : α → Modifier) (classify : Nat → Option α) (p : String) : Parser Modifier := + let len := p.length + match classify len with + | some res => pure (constructor res) + | none => fail s!"invalid quantity of characters for '{p.front}'" + +private def parseText (constructor : Text → Modifier) (p : String) : Parser Modifier := + parseMod constructor Text.classify p + +private def classifyNumberMax (max : Nat) : Nat → Option Number + | n => if n ≤ max then some ⟨n⟩ else none + +private def classifySingleNumber : Nat → Option Number + | 1 => some ⟨1⟩ + | _ => none + +private def classifyWeekdayText : Nat → Option Text + | 6 => some .twoLetterShort + | n => Text.classify n + +private def parseWeekdayText (constructor : Text → Modifier) (p : String) : Parser Modifier := + parseMod constructor classifyWeekdayText p + +private def parseFraction (constructor : Fraction → Modifier) (p : String) : Parser Modifier := + parseMod constructor Fraction.classify p + +private def parseNumber (constructor : Number → Modifier) (p : String) : Parser Modifier := + pure (constructor ⟨p.length⟩) + +private def parseYear (constructor : Year → Modifier) (p : String) : Parser Modifier := + parseMod constructor Year.classify p + +private def parseOffsetX (constructor : OffsetX → Modifier) (p : String) : Parser Modifier := + parseMod constructor OffsetX.classify p + +private def parseOffsetZ (constructor : OffsetZ → Modifier) (p : String) : Parser Modifier := + parseMod constructor OffsetZ.classify p + +private def parseOffsetO (constructor : OffsetO → Modifier) (p : String) : Parser Modifier := + parseMod constructor OffsetO.classify p + +private def parseZoneId (p : String) : Parser Modifier := + match p.length with + | 1 => pure (.V .unknown) + | 2 => pure (.V .short) + | _ => fail s!"invalid quantity of characters for '{p.front}': must be 1 or 2" + +private def parseNumberText (constructor : (Number ⊕ Text) → Modifier) (p : String) : Parser Modifier := + parseMod constructor classifyNumberText p + +private def classifyWeekdayNumberText : Nat → Option (Number ⊕ Text) + | n => + if n < 3 then + some (.inl ⟨n⟩) + else if n = 6 then + some (.inr .twoLetterShort) + else + .inr <$> Text.classify n + +private def parseWeekdayNumberText (constructor : (Number ⊕ Text) → Modifier) (p : String) : Parser Modifier := + parseMod constructor classifyWeekdayNumberText p + +private def classifyStandaloneWeekdayNumberText : Nat → Option (Number ⊕ Text) + | 1 => some (.inl ⟨1⟩) + | 6 => some (.inr .twoLetterShort) + | n => + if n ≥ 3 then + .inr <$> Text.classify n + else + none + +private def parseStandaloneWeekdayNumberText (constructor : (Number ⊕ Text) → Modifier) (p : String) : Parser Modifier := + parseMod constructor classifyStandaloneWeekdayNumberText p + +private def parseAMPM (p : String) : Parser Modifier := + parseText Modifier.a p + +private def parseDayPeriod (p : String) : Parser Modifier := + parseText Modifier.b p + +private def parseBPeriod (p : String) : Parser Modifier := + parseText Modifier.B p + +private def parseZoneName (constructor : ZoneName → Modifier) (p : String) : Parser Modifier := + let len := p.length + match ZoneName.classify (p.front) len with + | some res => pure (constructor res) + | none => fail s!"invalid quantity of characters for '{p.front}'" + +/-- Parses a single format `Modifier` from the input string. -/ +def parseModifier : Parser Modifier + := (parseText Modifier.G =<< many1Chars (pchar 'G')) + <|> parseYear Modifier.y =<< many1Chars (pchar 'y') + <|> parseYear Modifier.Y =<< many1Chars (pchar 'Y') + <|> parseYear Modifier.u =<< many1Chars (pchar 'u') + <|> parseMod Modifier.D (classifyNumberMax 3) =<< many1Chars (pchar 'D') + <|> parseNumberText Modifier.M =<< many1Chars (pchar 'M') + <|> parseNumberText Modifier.L =<< many1Chars (pchar 'L') + <|> parseMod Modifier.d (classifyNumberMax 2) =<< many1Chars (pchar 'd') + <|> parseNumberText Modifier.Q =<< many1Chars (pchar 'Q') + <|> parseNumberText Modifier.q =<< many1Chars (pchar 'q') + <|> parseMod Modifier.w (classifyNumberMax 2) =<< many1Chars (pchar 'w') + <|> parseMod Modifier.W classifySingleNumber =<< many1Chars (pchar 'W') + <|> parseWeekdayText Modifier.E =<< many1Chars (pchar 'E') + <|> parseWeekdayNumberText Modifier.e =<< many1Chars (pchar 'e') + <|> parseStandaloneWeekdayNumberText Modifier.c =<< many1Chars (pchar 'c') + <|> parseMod Modifier.F classifySingleNumber =<< many1Chars (pchar 'F') + <|> parseAMPM =<< many1Chars (pchar 'a') + <|> parseDayPeriod =<< many1Chars (pchar 'b') + <|> parseBPeriod =<< many1Chars (pchar 'B') + <|> parseMod Modifier.h (classifyNumberMax 2) =<< many1Chars (pchar 'h') + <|> parseMod Modifier.K (classifyNumberMax 2) =<< many1Chars (pchar 'K') + <|> parseMod Modifier.k (classifyNumberMax 2) =<< many1Chars (pchar 'k') + <|> parseMod Modifier.H (classifyNumberMax 2) =<< many1Chars (pchar 'H') + <|> parseMod Modifier.m (classifyNumberMax 2) =<< many1Chars (pchar 'm') + <|> parseMod Modifier.s (classifyNumberMax 2) =<< many1Chars (pchar 's') + <|> parseFraction Modifier.S =<< many1Chars (pchar 'S') + <|> parseNumber Modifier.A =<< many1Chars (pchar 'A') + <|> parseNumber Modifier.n =<< many1Chars (pchar 'n') + <|> parseNumber Modifier.N =<< many1Chars (pchar 'N') + <|> parseZoneId =<< many1Chars (pchar 'V') + <|> parseZoneName Modifier.z =<< many1Chars (pchar 'z') + <|> parseZoneName Modifier.v =<< many1Chars (pchar 'v') + <|> parseOffsetO Modifier.O =<< many1Chars (pchar 'O') + <|> parseOffsetX Modifier.X =<< many1Chars (pchar 'X') + <|> parseOffsetX Modifier.x =<< many1Chars (pchar 'x') + <|> parseOffsetZ Modifier.Z =<< many1Chars (pchar 'Z') + +end Time +end Std diff --git a/src/Std/Time/Notation.lean b/src/Std/Time/Notation.lean index 2f460e13fa8e..2ba75fb8de01 100644 --- a/src/Std/Time/Notation.lean +++ b/src/Std/Time/Notation.lean @@ -18,9 +18,10 @@ open Lean Parser Command Std set_option linter.all true private meta def convertText : Text → MacroM (TSyntax `term) - | .short => `(Std.Time.Text.short) - | .full => `(Std.Time.Text.full) - | .narrow => `(Std.Time.Text.narrow) + | .short => `(Std.Time.Text.short) + | .full => `(Std.Time.Text.full) + | .narrow => `(Std.Time.Text.narrow) + | .twoLetterShort => `(Std.Time.Text.twoLetterShort) private meta def convertNumber : Number → MacroM (TSyntax `term) | ⟨padding⟩ => `(Std.Time.Number.mk $(quote padding)) @@ -35,9 +36,14 @@ private meta def convertYear : Year → MacroM (TSyntax `term) | .fourDigit => `(Std.Time.Year.fourDigit) | .extended n => `(Std.Time.Year.extended $(quote n)) +private meta def convertZoneId : ZoneId → MacroM (TSyntax `term) + | .unknown => `(Std.Time.ZoneId.unknown) + | .short => `(Std.Time.ZoneId.short) + | .full => `(Std.Time.ZoneId.full) + private meta def convertZoneName : ZoneName → MacroM (TSyntax `term) | .short => `(Std.Time.ZoneName.short) - | .full => `(Std.Time.ZoneName.full) + | .full => `(Std.Time.ZoneName.full) private meta def convertOffsetX : OffsetX → MacroM (TSyntax `term) | .hour => `(Std.Time.OffsetX.hour) @@ -61,24 +67,26 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term) | .u p => do `(Std.Time.Modifier.u $(← convertYear p)) | .Y p => do `(Std.Time.Modifier.Y $(← convertYear p)) | .D p => do `(Std.Time.Modifier.D $(← convertNumber p)) - | .MorL p => - match p with - | .inl num => do `(Std.Time.Modifier.MorL (.inl $(← convertNumber num))) - | .inr txt => do `(Std.Time.Modifier.MorL (.inr $(← convertText txt))) + | .M (.inl num) => do `(Std.Time.Modifier.M (.inl $(← convertNumber num))) + | .M (.inr txt) => do `(Std.Time.Modifier.M (.inr $(← convertText txt))) + | .L (.inl num) => do `(Std.Time.Modifier.L (.inl $(← convertNumber num))) + | .L (.inr txt) => do `(Std.Time.Modifier.L (.inr $(← convertText txt))) | .d p => do `(Std.Time.Modifier.d $(← convertNumber p)) - | .Qorq p => - match p with - | .inl num => do `(Std.Time.Modifier.Qorq (.inl $(← convertNumber num))) - | .inr txt => do `(Std.Time.Modifier.Qorq (.inr $(← convertText txt))) + | .Q (.inl num) => do `(Std.Time.Modifier.Q (.inl $(← convertNumber num))) + | .Q (.inr txt) => do `(Std.Time.Modifier.Q (.inr $(← convertText txt))) + | .q (.inl num) => do `(Std.Time.Modifier.q (.inl $(← convertNumber num))) + | .q (.inr txt) => do `(Std.Time.Modifier.q (.inr $(← convertText txt))) | .w p => do `(Std.Time.Modifier.w $(← convertNumber p)) | .W p => do `(Std.Time.Modifier.W $(← convertNumber p)) | .E p => do `(Std.Time.Modifier.E $(← convertText p)) - | .eorc p => - match p with - | .inl num => do `(Std.Time.Modifier.eorc (.inl $(← convertNumber num))) - | .inr txt => do `(Std.Time.Modifier.eorc (.inr $(← convertText txt))) + | .e (.inl num) => do `(Std.Time.Modifier.e (.inl $(← convertNumber num))) + | .e (.inr txt) => do `(Std.Time.Modifier.e (.inr $(← convertText txt))) + | .c (.inl num) => do `(Std.Time.Modifier.c (.inl $(← convertNumber num))) + | .c (.inr txt) => do `(Std.Time.Modifier.c (.inr $(← convertText txt))) | .F p => do `(Std.Time.Modifier.F $(← convertNumber p)) | .a p => do `(Std.Time.Modifier.a $(← convertText p)) + | .b p => do `(Std.Time.Modifier.b $(← convertText p)) + | .B p => do `(Std.Time.Modifier.B $(← convertText p)) | .h p => do `(Std.Time.Modifier.h $(← convertNumber p)) | .K p => do `(Std.Time.Modifier.K $(← convertNumber p)) | .k p => do `(Std.Time.Modifier.k $(← convertNumber p)) @@ -89,8 +97,9 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term) | .A p => do `(Std.Time.Modifier.A $(← convertNumber p)) | .n p => do `(Std.Time.Modifier.n $(← convertNumber p)) | .N p => do `(Std.Time.Modifier.N $(← convertNumber p)) - | .V => `(Std.Time.Modifier.V) + | .V p => do `(Std.Time.Modifier.V $(← convertZoneId p)) | .z p => do `(Std.Time.Modifier.z $(← convertZoneName p)) + | .v p => do `(Std.Time.Modifier.v $(← convertZoneName p)) | .O p => do `(Std.Time.Modifier.O $(← convertOffsetO p)) | .X p => do `(Std.Time.Modifier.X $(← convertOffsetX p)) | .x p => do `(Std.Time.Modifier.x $(← convertOffsetX p)) diff --git a/src/Std/Time/Notation/Spec.lean b/src/Std/Time/Notation/Spec.lean index 014093bdd604..017168b3fe7e 100644 --- a/src/Std/Time/Notation/Spec.lean +++ b/src/Std/Time/Notation/Spec.lean @@ -16,9 +16,10 @@ namespace Time open Lean Parser Command Std private meta def convertText : Text → MacroM (TSyntax `term) - | .short => `(Std.Time.Text.short) - | .full => `(Std.Time.Text.full) - | .narrow => `(Std.Time.Text.narrow) + | .short => `(Std.Time.Text.short) + | .full => `(Std.Time.Text.full) + | .narrow => `(Std.Time.Text.narrow) + | .twoLetterShort => `(Std.Time.Text.twoLetterShort) private meta def convertNumber : Number → MacroM (TSyntax `term) | ⟨padding⟩ => `(Std.Time.Number.mk $(quote padding)) @@ -28,20 +29,25 @@ private meta def convertFraction : Fraction → MacroM (TSyntax `term) | .truncated digits => `(Std.Time.Fraction.truncated $(quote digits)) private meta def convertYear : Year → MacroM (TSyntax `term) - | .any => `(Std.Time.Year.any) + | .any => `(Std.Time.Year.any) | .twoDigit => `(Std.Time.Year.twoDigit) | .fourDigit => `(Std.Time.Year.fourDigit) | .extended n => `(Std.Time.Year.extended $(quote n)) +private meta def convertZoneId : ZoneId → MacroM (TSyntax `term) + | .unknown => `(Std.Time.ZoneId.unknown) + | .short => `(Std.Time.ZoneId.short) + | .full => `(Std.Time.ZoneId.full) + private meta def convertZoneName : ZoneName → MacroM (TSyntax `term) | .short => `(Std.Time.ZoneName.short) - | .full => `(Std.Time.ZoneName.full) + | .full => `(Std.Time.ZoneName.full) private meta def convertOffsetX : OffsetX → MacroM (TSyntax `term) - | .hour => `(Std.Time.OffsetX.hour) - | .hourMinute => `(Std.Time.OffsetX.hourMinute) - | .hourMinuteColon => `(Std.Time.OffsetX.hourMinuteColon) - | .hourMinuteSecond => `(Std.Time.OffsetX.hourMinuteSecond) + | .hour => `(Std.Time.OffsetX.hour) + | .hourMinute => `(Std.Time.OffsetX.hourMinute) + | .hourMinuteColon => `(Std.Time.OffsetX.hourMinuteColon) + | .hourMinuteSecond => `(Std.Time.OffsetX.hourMinuteSecond) | .hourMinuteSecondColon => `(Std.Time.OffsetX.hourMinuteSecondColon) private meta def convertOffsetO : OffsetO → MacroM (TSyntax `term) @@ -49,8 +55,8 @@ private meta def convertOffsetO : OffsetO → MacroM (TSyntax `term) | .full => `(Std.Time.OffsetO.full) private meta def convertOffsetZ : OffsetZ → MacroM (TSyntax `term) - | .hourMinute => `(Std.Time.OffsetZ.hourMinute) - | .full => `(Std.Time.OffsetZ.full) + | .hourMinute => `(Std.Time.OffsetZ.hourMinute) + | .full => `(Std.Time.OffsetZ.full) | .hourMinuteSecondColon => `(Std.Time.OffsetZ.hourMinuteSecondColon) private meta def convertModifier : Modifier → MacroM (TSyntax `term) @@ -59,24 +65,26 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term) | .u p => do `(Std.Time.Modifier.u $(← convertYear p)) | .Y p => do `(Std.Time.Modifier.Y $(← convertYear p)) | .D p => do `(Std.Time.Modifier.D $(← convertNumber p)) - | .MorL p => - match p with - | .inl num => do `(Std.Time.Modifier.MorL (.inl $(← convertNumber num))) - | .inr txt => do `(Std.Time.Modifier.MorL (.inr $(← convertText txt))) + | .M (.inl num) => do `(Std.Time.Modifier.M (.inl $(← convertNumber num))) + | .M (.inr txt) => do `(Std.Time.Modifier.M (.inr $(← convertText txt))) + | .L (.inl num) => do `(Std.Time.Modifier.L (.inl $(← convertNumber num))) + | .L (.inr txt) => do `(Std.Time.Modifier.L (.inr $(← convertText txt))) | .d p => do `(Std.Time.Modifier.d $(← convertNumber p)) - | .Qorq p => - match p with - | .inl num => do `(Std.Time.Modifier.Qorq (.inl $(← convertNumber num))) - | .inr txt => do `(Std.Time.Modifier.Qorq (.inr $(← convertText txt))) + | .Q (.inl num) => do `(Std.Time.Modifier.Q (.inl $(← convertNumber num))) + | .Q (.inr txt) => do `(Std.Time.Modifier.Q (.inr $(← convertText txt))) + | .q (.inl num) => do `(Std.Time.Modifier.q (.inl $(← convertNumber num))) + | .q (.inr txt) => do `(Std.Time.Modifier.q (.inr $(← convertText txt))) | .w p => do `(Std.Time.Modifier.w $(← convertNumber p)) | .W p => do `(Std.Time.Modifier.W $(← convertNumber p)) | .E p => do `(Std.Time.Modifier.E $(← convertText p)) - | .eorc p => - match p with - | .inl num => do `(Std.Time.Modifier.eorc (.inl $(← convertNumber num))) - | .inr txt => do `(Std.Time.Modifier.eorc (.inr $(← convertText txt))) + | .e (.inl num) => do `(Std.Time.Modifier.e (.inl $(← convertNumber num))) + | .e (.inr txt) => do `(Std.Time.Modifier.e (.inr $(← convertText txt))) + | .c (.inl num) => do `(Std.Time.Modifier.c (.inl $(← convertNumber num))) + | .c (.inr txt) => do `(Std.Time.Modifier.c (.inr $(← convertText txt))) | .F p => do `(Std.Time.Modifier.F $(← convertNumber p)) | .a p => do `(Std.Time.Modifier.a $(← convertText p)) + | .b p => do `(Std.Time.Modifier.b $(← convertText p)) + | .B p => do `(Std.Time.Modifier.B $(← convertText p)) | .h p => do `(Std.Time.Modifier.h $(← convertNumber p)) | .K p => do `(Std.Time.Modifier.K $(← convertNumber p)) | .k p => do `(Std.Time.Modifier.k $(← convertNumber p)) @@ -87,8 +95,9 @@ private meta def convertModifier : Modifier → MacroM (TSyntax `term) | .A p => do `(Std.Time.Modifier.A $(← convertNumber p)) | .n p => do `(Std.Time.Modifier.n $(← convertNumber p)) | .N p => do `(Std.Time.Modifier.N $(← convertNumber p)) - | .V => `(Std.Time.Modifier.V) + | .V p => do `(Std.Time.Modifier.V $(← convertZoneId p)) | .z p => do `(Std.Time.Modifier.z $(← convertZoneName p)) + | .v p => do `(Std.Time.Modifier.v $(← convertZoneName p)) | .O p => do `(Std.Time.Modifier.O $(← convertOffsetO p)) | .X p => do `(Std.Time.Modifier.X $(← convertOffsetX p)) | .x p => do `(Std.Time.Modifier.x $(← convertOffsetX p)) diff --git a/tests/elab/timeFormats.lean b/tests/elab/timeFormats.lean index e9524d192f29..855e6956741d 100644 --- a/tests/elab/timeFormats.lean +++ b/tests/elab/timeFormats.lean @@ -1,827 +1,688 @@ import Std.Time open Std.Time -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 D, uuuu h: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 EraDate : GenericFormat .any := datespec("MM D, uuuu G") -def DateSmall : GenericFormat .any := datespec("uu-MM-dd") - --- 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: "Monday, June 16, 2014 03:03:03 -0300" +/-! +Format specifier compatibility tests, cross-checked against Java `DateTimeFormatter` (Java 17+) +and Unicode CLDR TR35. All expected values match what Java and CLDR produce for English (US) locale. -/ -#guard_msgs in -#eval FullDayTimeZone.format date₁ -def tm := date₁.toTimestamp -def date₂ := DateTime.ofTimestampWithZone tm brTZ +-- ────────────────────────────────────────────────────────────────────────────── +-- Reference inputs +-- ────────────────────────────────────────────────────────────────────────────── -/-- -info: "Monday, June 16, 2014 03:03:03 -0300" --/ -#guard_msgs in -#eval FullDayTimeZone.format date₂ +-- 2002-07-14T23:13:12.324354679+09:00, Sunday, day-of-year=195, Q3, week=29 +def zoned₄ := zoned("2002-07-14T23:13:12.324354679+09:00") +-- Same instant at UTC offset +00:00 +def zoned₅ := zoned("2002-07-14T23:13:12.324354679+00:00") +-- PlainDateTime (no zone) — same date/time fields +def datetime₄ := datetime("2002-07-14T23:13:12.324354679") +-- PlainDate only +def date₄ := date("2002-07-14") +-- PlainTime only +def time₄ := time("23:13:12.324354679") +-- BCE year: proleptic year = -2000 → year-of-era = 2001, era = BCE +def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (PlainTime.mk 12 23 12 0) -def tm₃ := date₁.toTimestamp -def date₃ := DateTime.ofTimestampWithZone tm₃ brTZ +-- Named time zones for round-trip / conversion tests +def brTZ : TimeZone := timezone("America/Sao_Paulo -03:00") +def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00") -/-- -info: "Monday, June 16, 2014 03:03:03 -0300" --/ +-- ────────────────────────────────────────────────────────────────────────────── +-- G Era +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "AD AD AD Anno Domini A" -/ +#guard_msgs in #eval zoned₄.format "G GG GGG GGGG GGGGG" +/-- info: "AD AD AD Anno Domini A" -/ +#guard_msgs in #eval datetime₄.format "G GG GGG GGGG GGGGG" +/-- info: "AD AD AD Anno Domini A" -/ +#guard_msgs in #eval date₄.format "G GG GGG GGGG GGGGG" +/-- info: "BC Before Christ B" -/ +#guard_msgs in #eval datetime₅.format "GGG GGGG GGGGG" + +-- ────────────────────────────────────────────────────────────────────────────── +-- y Year-of-era (always positive; BCE year 1 BC → y=1, era=BCE) +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "02 2002 000002002" -/ +#guard_msgs in #eval zoned₄.format "yy yyyy yyyyyyyyy" +/-- info: "02 2002 000002002" -/ +#guard_msgs in #eval datetime₄.format "yy yyyy yyyyyyyyy" +/-- info: "02 2002 000002002" -/ +#guard_msgs in #eval date₄.format "yy yyyy yyyyyyyyy" +-- proleptic -2000 → year-of-era 2001 (1 BC = year-of-era 1, 2 BC = year-of-era 2, ...) +/-- info: "01 2001 000002001" -/ +#guard_msgs in #eval datetime₅.format "yy yyyy yyyyyyyyy" + +-- ────────────────────────────────────────────────────────────────────────────── +-- u Proleptic/astronomical year (can be negative) +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "02 2002 000002002" -/ +#guard_msgs in #eval zoned₄.format "uu uuuu uuuuuuuuu" +/-- info: "02 2002 000002002" -/ +#guard_msgs in #eval datetime₄.format "uu uuuu uuuuuuuuu" +/-- info: "02 2002 000002002" -/ +#guard_msgs in #eval date₄.format "uu uuuu uuuuuuuuu" +/-- info: "-2000 -2000" -/ +#guard_msgs in #eval datetime₅.format "uuuu u" + +-- Combined year + era sanity check (matches Java) +/-- info: "2002 2002 AD" -/ +#guard_msgs in #eval datetime₄.format "uuuu yyyy G" + +/-- info: "-2000 2001 BC" -/ +#guard_msgs in #eval datetime₅.format "uuuu yyyy G" + +-- ────────────────────────────────────────────────────────────────────────────── +-- D Day-of-year +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "195 195 195" -/ +#guard_msgs in #eval zoned₄.format "D DD DDD" +/-- info: "195 195 195" -/ +#guard_msgs in #eval datetime₄.format "D DD DDD" +/-- info: "195 195 195" -/ +#guard_msgs in #eval date₄.format "D DD DDD" + +-- ────────────────────────────────────────────────────────────────────────────── +-- M Month-of-year (contextual) / L Month-of-year (standalone) +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "7 07 Jul July J" -/ +#guard_msgs in #eval zoned₄.format "M MM MMM MMMM MMMMM" +/-- info: "7 07 Jul July J" -/ +#guard_msgs in #eval datetime₄.format "M MM MMM MMMM MMMMM" +/-- info: "7 07 Jul July J" -/ +#guard_msgs in #eval date₄.format "M MM MMM MMMM MMMMM" + +-- L standalone — same values as M in English +/-- info: "7 07 Jul July J" -/ +#guard_msgs in #eval zoned₄.format "L LL LLL LLLL LLLLL" +/-- info: "7 07 Jul July J" -/ +#guard_msgs in #eval date₄.format "L LL LLL LLLL LLLLL" + +-- ────────────────────────────────────────────────────────────────────────────── +-- d Day-of-month +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "14 14" -/ +#guard_msgs in #eval zoned₄.format "d dd" +/-- info: "14 14" -/ +#guard_msgs in #eval datetime₄.format "d dd" +/-- info: "14 14" -/ +#guard_msgs in #eval date₄.format "d dd" + +-- ────────────────────────────────────────────────────────────────────────────── +-- Q Quarter-of-year (contextual) / q Quarter-of-year (standalone) +-- ────────────────────────────────────────────────────────────────────────────── + +-- Q: numeric 1-digit, 2-digit; text short (QQQ), full (QQQQ), narrow (QQQQQ) +/-- info: "3 03 Q3 3rd quarter 3" -/ +#guard_msgs in #eval zoned₄.format "Q QQ QQQ QQQQ QQQQQ" +/-- info: "3 03 Q3 3rd quarter 3" -/ +#guard_msgs in #eval datetime₄.format "Q QQ QQQ QQQQ QQQQQ" +/-- info: "3 03 Q3 3rd quarter 3" -/ +#guard_msgs in #eval date₄.format "Q QQ QQQ QQQQ QQQQQ" + +-- q standalone — same values in English +/-- info: "3 03 Q3 3rd quarter 3" -/ +#guard_msgs in #eval zoned₄.format "q qq qqq qqqq qqqqq" +/-- info: "3 03 Q3 3rd quarter 3" -/ +#guard_msgs in #eval date₄.format "q qq qqq qqqq qqqqq" + +-- ────────────────────────────────────────────────────────────────────────────── +-- w Week-of-week-based-year / W Week-of-month +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "29 29" -/ +#guard_msgs in #eval zoned₄.format "w ww" +/-- info: "29 29" -/ +#guard_msgs in #eval datetime₄.format "w ww" +/-- info: "29 29" -/ +#guard_msgs in #eval date₄.format "w ww" + +/-- info: "3" -/ +#guard_msgs in #eval zoned₄.format "W" +/-- info: "3" -/ +#guard_msgs in #eval datetime₄.format "W" +/-- info: "3" -/ +#guard_msgs in #eval date₄.format "W" + +-- ISO week boundary: 2018-12-31 belongs to ISO week 1 of 2019 +/-- info: 1 -/ #guard_msgs in -#eval FullDayTimeZone.format date₃ - --- Section for testing timezone conversion. +#eval + let t : DateTime := .ofPlainDateTime datetime("2018-12-31T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC) + IO.println s!"{t.format "w"}" --- the timestamp is always related to UTC. +-- ISO week-year boundaries, cross-checked with Python datetime.isocalendar(). +#guard date("2015-12-28").weekOfYear.val == 53 +#guard date("2015-12-31").weekOfYear.val == 53 +#guard date("2016-01-01").weekOfYear.val == 53 +#guard date("2016-01-04").weekOfYear.val == 1 +#guard date("2018-12-31").weekOfYear.val == 1 +#guard date("2019-01-01").weekOfYear.val == 1 +#guard date("2020-12-28").weekOfYear.val == 53 +#guard date("2020-12-31").weekOfYear.val == 53 +#guard date("2021-01-01").weekOfYear.val == 53 +#guard date("2021-01-03").weekOfYear.val == 53 +#guard date("2021-12-28").weekOfYear.val == 52 +#guard date("2022-01-01").weekOfYear.val == 52 +#guard date("2022-12-31").weekOfYear.val == 52 +#guard date("2023-01-01").weekOfYear.val == 52 +#guard date("2000-01-01").weekOfYear.val == 52 +#guard date("2000-01-02").weekOfYear.val == 52 +#guard date("2000-01-03").weekOfYear.val == 1 +#guard date("2004-01-01").weekOfYear.val == 1 +#guard date("2005-01-01").weekOfYear.val == 53 +#guard date("2005-01-02").weekOfYear.val == 53 +#guard date("2024-12-30").weekOfYear.val == 1 +#guard date("2024-12-31").weekOfYear.val == 1 +#guard date("2025-01-01").weekOfYear.val == 1 +#guard date("2026-05-25").weekOfYear.val == 22 +#guard date("2026-01-01").weekOfYear.val == 1 +#guard date("2026-12-28").weekOfYear.val == 53 +#guard date("2026-12-31").weekOfYear.val == 53 +#guard date("2027-01-01").weekOfYear.val == 53 + +#guard date("2015-12-28").weekYear == 2015 +#guard date("2015-12-31").weekYear == 2015 +#guard date("2016-01-01").weekYear == 2015 +#guard date("2016-01-04").weekYear == 2016 +#guard date("2018-12-31").weekYear == 2019 +#guard date("2019-01-01").weekYear == 2019 +#guard date("2020-12-28").weekYear == 2020 +#guard date("2020-12-31").weekYear == 2020 +#guard date("2021-01-01").weekYear == 2020 +#guard date("2021-01-03").weekYear == 2020 +#guard date("2021-12-28").weekYear == 2021 +#guard date("2022-01-01").weekYear == 2021 +#guard date("2022-12-31").weekYear == 2022 +#guard date("2023-01-01").weekYear == 2022 +#guard date("2000-01-01").weekYear == 1999 +#guard date("2000-01-02").weekYear == 1999 +#guard date("2000-01-03").weekYear == 2000 +#guard date("2004-01-01").weekYear == 2004 +#guard date("2005-01-01").weekYear == 2004 +#guard date("2005-01-02").weekYear == 2004 +#guard date("2024-12-30").weekYear == 2025 +#guard date("2024-12-31").weekYear == 2025 +#guard date("2025-01-01").weekYear == 2025 +#guard date("2026-05-25").weekYear == 2026 +#guard date("2026-01-01").weekYear == 2026 +#guard date("2026-12-28").weekYear == 2026 +#guard date("2026-12-31").weekYear == 2026 +#guard date("2027-01-01").weekYear == 2026 + +-- ────────────────────────────────────────────────────────────────────────────── +-- E Day-of-week (text only) +-- ────────────────────────────────────────────────────────────────────────────── + +-- 2002-07-14 = Sunday +-- E/EE/EEE = short, EEEE = full, EEEEE = narrow, EEEEEE = two-letter +/-- info: "Sun Sun Sun Sunday S Su" -/ +#guard_msgs in #eval zoned₄.format "E EE EEE EEEE EEEEE EEEEEE" +/-- info: "Sun Sun Sun Sunday S Su" -/ +#guard_msgs in #eval datetime₄.format "E EE EEE EEEE EEEEE EEEEEE" +/-- info: "Sun Sun Sun Sunday S Su" -/ +#guard_msgs in #eval date₄.format "E EE EEE EEEE EEEEE EEEEEE" + +-- ────────────────────────────────────────────────────────────────────────────── +-- e Localized day-of-week (number or text) +-- ────────────────────────────────────────────────────────────────────────────── + +-- US locale: firstDayOfWeek=Sunday → Sunday=1, Monday=2, ..., Saturday=7 +-- 2002-07-14 = Sunday → e=1 +/-- info: "1 01 Sun Sunday S Su" -/ +#guard_msgs in #eval zoned₄.format "e ee eee eeee eeeee eeeeee" +/-- info: "1 01 Sun Sunday S Su" -/ +#guard_msgs in #eval datetime₄.format "e ee eee eeee eeeee eeeeee" +/-- info: "1 01 Sun Sunday S Su" -/ +#guard_msgs in #eval date₄.format "e ee eee eeee eeeee eeeeee" + +-- ────────────────────────────────────────────────────────────────────────────── +-- c Stand-alone day-of-week +-- ────────────────────────────────────────────────────────────────────────────── + +-- c = numeric (1 letter only; cc is invalid); ccc/cccc/ccccc/cccccc = text +/-- info: "1 Sun Sunday S Su" -/ +#guard_msgs in #eval zoned₄.format "c ccc cccc ccccc cccccc" +/-- info: "1 Sun Sunday S Su" -/ +#guard_msgs in #eval datetime₄.format "c ccc cccc ccccc cccccc" +/-- info: "1 Sun Sunday S Su" -/ +#guard_msgs in #eval date₄.format "c ccc cccc ccccc cccccc" + +-- ────────────────────────────────────────────────────────────────────────────── +-- F Day-of-week-in-month (occurrence of the weekday within the month) +-- ────────────────────────────────────────────────────────────────────────────── + +-- July 14, 2002 is the 2nd Sunday of July → F=2 +/-- info: "2" -/ +#guard_msgs in #eval zoned₄.format "F" +/-- info: "2" -/ +#guard_msgs in #eval datetime₄.format "F" +/-- info: "2" -/ +#guard_msgs in #eval date₄.format "F" + +-- ────────────────────────────────────────────────────────────────────────────── +-- a AM/PM marker +-- ────────────────────────────────────────────────────────────────────────────── + +-- 23:13:12 → PM +/-- info: "PM PM PM post meridiem p" -/ +#guard_msgs in #eval zoned₄.format "a aa aaa aaaa aaaaa" +/-- info: "PM PM PM post meridiem p" -/ +#guard_msgs in #eval datetime₄.format "a aa aaa aaaa aaaaa" +/-- info: "PM PM PM post meridiem p" -/ +#guard_msgs in #eval time₄.format "a aa aaa aaaa aaaaa" + +-- ────────────────────────────────────────────────────────────────────────────── +-- b Day period with noon/midnight distinction (Java 16+ / TR35 §4) +-- ────────────────────────────────────────────────────────────────────────────── + +-- 23:13:12 → PM (not noon or midnight) +/-- info: "PM PM PM post meridiem p" -/ +#guard_msgs in #eval zoned₄.format "b bb bbb bbbb bbbbb" +/-- info: "PM PM PM post meridiem p" -/ +#guard_msgs in #eval datetime₄.format "b bb bbb bbbb bbbbb" +/-- info: "PM PM PM post meridiem p" -/ +#guard_msgs in #eval time₄.format "b bb bbb bbbb bbbbb" + +-- noon: 12:00:00 +def timeNoon := time("12:00:00") +/-- info: "noon noon noon noon n" -/ +#guard_msgs in #eval timeNoon.format "b bb bbb bbbb bbbbb" + +-- midnight: 00:00:00 +def timeMidnight := time("00:00:00") +/-- info: "midnight midnight midnight midnight mi" -/ +#guard_msgs in #eval timeMidnight.format "b bb bbb bbbb bbbbb" + +-- ────────────────────────────────────────────────────────────────────────────── +-- B Flexible day period / extended day period (Java 16+ / CLDR §4) +-- ────────────────────────────────────────────────────────────────────────────── + +-- 23:13:12 → hour 23 ≥ 21 → "at night" +/-- info: "at night at night at night at night night" -/ +#guard_msgs in #eval zoned₄.format "B BB BBB BBBB BBBBB" +/-- info: "at night at night at night at night night" -/ +#guard_msgs in #eval datetime₄.format "B BB BBB BBBB BBBBB" +/-- info: "at night at night at night at night night" -/ +#guard_msgs in #eval time₄.format "B BB BBB BBBB BBBBB" + +-- morning: 06:00–11:59 +def timeMorning := time("09:00:00") + +/-- info: "in the morning in the morning in the morning in the morning morning" -/ +#guard_msgs in #eval timeMorning.format "B BB BBB BBBB BBBBB" + +-- noon +/-- info: "noon noon noon noon n" -/ +#guard_msgs in #eval timeNoon.format "B BB BBB BBBB BBBBB" + +-- afternoon: 12:01–17:59 +def timeAfternoon := time("15:30:00") + +/-- info: "in the afternoon in the afternoon in the afternoon in the afternoon afternoon" -/ +#guard_msgs in #eval timeAfternoon.format "B BB BBB BBBB BBBBB" + +-- evening: 18:00–20:59 +def timeEvening := time("19:00:00") + +/-- info: "in the evening in the evening in the evening in the evening evening" -/ +#guard_msgs in #eval timeEvening.format "B BB BBB BBBB BBBBB" + +-- midnight +/-- info: "midnight midnight midnight midnight mi" -/ +#guard_msgs in #eval timeMidnight.format "B BB BBB BBBB BBBBB" + +-- early morning / night: 01:00 (hour 1, < 6) +def timeNight := time("01:00:00") + +/-- info: "at night at night at night at night night" -/ +#guard_msgs in #eval timeNight.format "B BB BBB BBBB BBBBB" + +-- ────────────────────────────────────────────────────────────────────────────── +-- h Clock-hour-of-AM/PM (1–12) +-- K Hour-of-AM/PM (0–11) +-- k Clock-hour-of-day (1–24) +-- H Hour-of-day (0–23) +-- ────────────────────────────────────────────────────────────────────────────── + +-- hour=23: h=11 (23%12), K=11 (23%12), k=23, H=23 +/-- info: "11 11" -/ +#guard_msgs in #eval zoned₄.format "h hh" +/-- info: "11 11" -/ +#guard_msgs in #eval datetime₄.format "h hh" +/-- info: "11 11" -/ +#guard_msgs in #eval time₄.format "h hh" + +/-- info: "11 11" -/ +#guard_msgs in #eval zoned₄.format "K KK" +/-- info: "11 11" -/ +#guard_msgs in #eval datetime₄.format "K KK" +/-- info: "11 11" -/ +#guard_msgs in #eval time₄.format "K KK" + +/-- info: "23 23" -/ +#guard_msgs in #eval zoned₄.format "k kk" +/-- info: "23 23" -/ +#guard_msgs in #eval datetime₄.format "k kk" +/-- info: "23 23" -/ +#guard_msgs in #eval time₄.format "k kk" + +/-- info: "23 23" -/ +#guard_msgs in #eval zoned₄.format "H HH" +/-- info: "23 23" -/ +#guard_msgs in #eval datetime₄.format "H HH" +/-- info: "23 23" -/ +#guard_msgs in #eval time₄.format "H HH" + +/-- info: "12 12 0 00 24 24 0 00" -/ +#guard_msgs in #eval timeMidnight.format "h hh K KK k kk H HH" + +/-- info: "12 12 0 00 12 12 12 12" -/ +#guard_msgs in #eval timeNoon.format "h hh K KK k kk H HH" + +-- ────────────────────────────────────────────────────────────────────────────── +-- m Minute / s Second +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "13 13" -/ +#guard_msgs in #eval zoned₄.format "m mm" +/-- info: "13 13" -/ +#guard_msgs in #eval datetime₄.format "m mm" +/-- info: "13 13" -/ +#guard_msgs in #eval time₄.format "m mm" + +/-- info: "12 12" -/ +#guard_msgs in #eval zoned₄.format "s ss" +/-- info: "12 12" -/ +#guard_msgs in #eval datetime₄.format "s ss" +/-- info: "12 12" -/ +#guard_msgs in #eval time₄.format "s ss" + +-- ────────────────────────────────────────────────────────────────────────────── +-- S Fraction-of-second (truncates, does not round) +-- ────────────────────────────────────────────────────────────────────────────── + +-- nanosecond = 324354679; S truncates left-to-right +/-- info: "3 32 324 3243 32435 324354679" -/ +#guard_msgs in #eval zoned₄.format "S SS SSS SSSS SSSSS SSSSSSSSS" +/-- info: "3 32 324 3243 32435 324354679" -/ +#guard_msgs in #eval datetime₄.format "S SS SSS SSSS SSSSS SSSSSSSSS" +/-- info: "3 32 324 3243 32435 324354679" -/ +#guard_msgs in #eval time₄.format "S SS SSS SSSS SSSSS SSSSSSSSS" + +-- ────────────────────────────────────────────────────────────────────────────── +-- A Millisecond-of-day / n Nanosecond-of-second / N Nanosecond-of-day +-- ────────────────────────────────────────────────────────────────────────────── + +-- milli-of-day = (23*3600 + 13*60 + 12)*1000 + 324 = 83592324 +/-- info: "83592324 083592324" -/ +#guard_msgs in #eval zoned₄.format "A AAAAAAAAA" +/-- info: "83592324 083592324" -/ +#guard_msgs in #eval datetime₄.format "A AAAAAAAAA" +/-- info: "83592324 083592324" -/ +#guard_msgs in #eval time₄.format "A AAAAAAAAA" + +-- nano-of-second = 324354679 +/-- info: "324354679 324354679" -/ +#guard_msgs in #eval zoned₄.format "n nnnnnnnnn" +/-- info: "324354679 324354679" -/ +#guard_msgs in #eval datetime₄.format "n nnnnnnnnn" +/-- info: "324354679 324354679" -/ +#guard_msgs in #eval time₄.format "n nnnnnnnnn" + +-- nano-of-day = 83592324*1000000 + 354679 = 83592324354679 +/-- info: "83592324354679 83592324354679" -/ +#guard_msgs in #eval zoned₄.format "N NNNNNNNNN" +/-- info: "83592324354679 83592324354679" -/ +#guard_msgs in #eval datetime₄.format "N NNNNNNNNN" +/-- info: "83592324354679 83592324354679" -/ +#guard_msgs in #eval time₄.format "N NNNNNNNNN" + +-- ────────────────────────────────────────────────────────────────────────────── +-- V Time-zone ID +-- ────────────────────────────────────────────────────────────────────────────── + +-- VV = IANA zone ID (or offset string for offset-only zones) +/-- info: "GMT+09:00" -/ +#guard_msgs in #eval zoned₄.format "VV" +/-- info: "GMT+00:00" -/ +#guard_msgs in #eval zoned₅.format "VV" + +-- ────────────────────────────────────────────────────────────────────────────── +-- z Time-zone name / v Generic time-zone name +-- ────────────────────────────────────────────────────────────────────────────── + +-- offset-only zone: short name = abbreviation = "+09:00"; full = name = "+09:00" +/-- info: "GMT+09:00 GMT+09:00 GMT+09:00 GMT+09:00" -/ +#guard_msgs in #eval zoned₄.format "z zz zzz zzzz" + +/-- info: "GMT+00:00 GMT+00:00 GMT+00:00 GMT+00:00" -/ +#guard_msgs in #eval zoned₅.format "z zz zzz zzzz" + +-- named zone (brTZ stored with abbreviation "BRT") +def tz : TimeZone := { offset := { second := -3600 }, name := "America/Sao_Paulo", abbreviation := "BRT", isDST := false} +def zoned₆ := DateTime.ofPlainDateTime (zoned₄.toPlainDateTime) (TimeZone.ZoneRules.ofTimeZone tz) +/-- info: "BRT BRT BRT America/Sao_Paulo America/Sao_Paulo" -/ +#guard_msgs in #eval zoned₆.format "z zz zzz zzzz zzzz" + +-- v: generic (no DST distinction) — same abbreviation/name as z for these zones +/-- info: "GMT+09:00 GMT+09:00" -/ +#guard_msgs in #eval zoned₄.format "v vvvv" + +/-- info: "GMT+00:00 GMT+00:00" -/ +#guard_msgs in #eval zoned₅.format "v vvvv" + +-- ────────────────────────────────────────────────────────────────────────────── +-- O Localized GMT offset +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "GMT+9 GMT+09:00" -/ +#guard_msgs in #eval zoned₄.format "O OOOO" +-- +00:00 → short "GMT" (UTC), full "GMT" +/-- info: "GMT GMT" -/ +#guard_msgs in #eval zoned₅.format "O OOOO" + +-- ────────────────────────────────────────────────────────────────────────────── +-- X Zone offset (uses 'Z' for UTC) +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "+09 +0900 +09:00 +0900 +09:00" -/ +#guard_msgs in #eval zoned₄.format "X XX XXX XXXX XXXXX" +-- +00:00 → 'Z' for all widths +/-- info: "Z Z Z Z Z" -/ +#guard_msgs in #eval zoned₅.format "X XX XXX XXXX XXXXX" + +-- ────────────────────────────────────────────────────────────────────────────── +-- x Zone offset (never 'Z') +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "+09 +0900 +09:00 +0900 +09:00" -/ +#guard_msgs in #eval zoned₄.format "x xx xxx xxxx xxxxx" +/-- info: "+00 +0000 +00:00 +0000 +00:00" -/ +#guard_msgs in #eval zoned₅.format "x xx xxx xxxx xxxxx" + +-- ────────────────────────────────────────────────────────────────────────────── +-- Z Zone offset (RFC / CLDR Z forms) +-- ────────────────────────────────────────────────────────────────────────────── + +/-- info: "+0900 +0900 +0900 GMT+09:00 +09:00" -/ +#guard_msgs in #eval zoned₄.format "Z ZZ ZZZ ZZZZ ZZZZZ" +-- +00:00: Z/ZZ/ZZZ=+0000, ZZZZ=GMT, ZZZZZ=Z +/-- info: "+0000 +0000 +0000 GMT Z" -/ +#guard_msgs in #eval zoned₅.format "Z ZZ ZZZ ZZZZ ZZZZZ" + +-- ────────────────────────────────────────────────────────────────────────────── +-- Common real-world format strings +-- ────────────────────────────────────────────────────────────────────────────── -/-- -Timestamp: 1723739292 -GMT: Thursday, 15 August 2024 16:28:12 -BR: 15 August 2024 13:28:12 GMT-03:00 --/ +def date₁ := zoned("2014-06-16T03:03:03-03:00") def tm₄ : Second.Offset := 1723739292 - def dateBR := DateTime.ofTimestampWithZone (Timestamp.ofSecondsSinceUnixEpoch tm₄) brTZ def dateJP := DateTime.ofTimestampWithZone (Timestamp.ofSecondsSinceUnixEpoch tm₄) jpTZ def dateUTC := DateTime.ofTimestampWithZone (Timestamp.ofSecondsSinceUnixEpoch tm₄) .UTC -/-- -info: "Thursday, August 15, 2024 13:28:12 -0300" --/ -#guard_msgs in -#eval FullDayTimeZone.format dateBR - -/-- -info: "Friday, August 16, 2024 01:28:12 +0900" --/ -#guard_msgs in -#eval FullDayTimeZone.format dateJP - -/-- -info: "Thursday, August 15, 2024 13:28:12 -0300" --/ -#guard_msgs in -#eval FullDayTimeZone.format (dateUTC.convertZoneRules (TimeZone.ZoneRules.ofTimeZone brTZ)) - -/-- -info: "Thursday, August 15, 2024 13:28:12 -0300" --/ -#guard_msgs in -#eval FullDayTimeZone.format (dateJP.convertZoneRules (TimeZone.ZoneRules.ofTimeZone brTZ)) - -/-- -info: "Thursday, August 15, 2024 16:28:12 +0000" --/ -#guard_msgs in -#eval FullDayTimeZone.format dateUTC - -/-- -info: "Thursday, August 15, 2024 16:28:12 +0000" --/ -#guard_msgs in -#eval FullDayTimeZone.format (dateBR.convertZoneRules (TimeZone.ZoneRules.ofTimeZone .UTC)) - -/-- -info: "Thursday, August 15, 2024 16:28:12 +0000" --/ -#guard_msgs in -#eval FullDayTimeZone.format (dateJP.convertZoneRules (TimeZone.ZoneRules.ofTimeZone .UTC)) - -/-- -info: "Friday, August 16, 2024 01:28:12 +0900" --/ -#guard_msgs in -#eval FullDayTimeZone.format dateJP - -/-- -info: "Friday, August 16, 2024 01:28:12 +0900" --/ -#guard_msgs in -#eval FullDayTimeZone.format (dateBR.convertZoneRules (TimeZone.ZoneRules.ofTimeZone jpTZ)) - -/-- -info: "Friday, August 16, 2024 01:28:12 +0900" --/ -#guard_msgs in -#eval FullDayTimeZone.format (dateUTC.convertZoneRules (TimeZone.ZoneRules.ofTimeZone 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.ofPlainDateTimeWithZone PlainDate brTZ -def dateJP₁ := DateTime.ofPlainDateTimeWithZone PlainDate jpTZ -def dateUTC₁ := DateTime.ofPlainDateTimeWithZone PlainDate .UTC - -/-- -info: "Thursday, August 15, 2024 14:03:47 -0300" --/ -#guard_msgs in -#eval FullDayTimeZone.format dateBR₁ - -/-- -info: "Thursday, August 15, 2024 14:03:47 +0900" --/ -#guard_msgs in -#eval FullDayTimeZone.format dateJP₁ - -/-- -info: "Thursday, August 15, 2024 23:03:47 +0900" --/ -#guard_msgs in -#eval FullDayTimeZone.format (dateUTC₁.convertZoneRules (TimeZone.ZoneRules.ofTimeZone jpTZ)) - -/-- -info: "Friday, August 16, 2024 02:03:47 +0900" --/ -#guard_msgs in -#eval FullDayTimeZone.format (dateBR₁.convertZoneRules (TimeZone.ZoneRules.ofTimeZone jpTZ)) - -/-- -info: "Thursday, August 15, 2024 14:03:47 +0900" --/ -#guard_msgs in -#eval FullDayTimeZone.format (dateJP₁.convertZoneRules (TimeZone.ZoneRules.ofTimeZone jpTZ)) - -/-- -info: "Monday, June 16, 2014 03:03:03 -0300" --/ -#guard_msgs in -#eval FullDayTimeZone.format date₂ - -/-- -info: "14:11:01" --/ -#guard_msgs in -#eval Time24Hour.formatBuilder time₁.hour time₁.minute time₁.second - -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" --/ -#guard_msgs in -#eval l -/-- -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) - -/-- -info: "2024-08-15T14:03:47-03:00" --/ -#guard_msgs in -#eval dateBR₁.toISO8601String - -/-- -info: "2024-08-15T14:03:47Z" --/ -#guard_msgs in -#eval dateUTC₁.toISO8601String - -/-- -info: "06/16/2014" --/ -#guard_msgs in -#eval ShortDate.formatBuilder date₁.month date₁.day date₁.year - -/-- -info: "0053-06-19" --/ -#guard_msgs in -#eval Formats.sqlDate.format (DateTime.ofLocalDateWithZone (PlainDate.ofEpochDay ⟨-700000⟩) .UTC) - -/-- -info: "-0002-09-16" --/ -#guard_msgs in -#eval Formats.sqlDate.format (DateTime.ofLocalDateWithZone (PlainDate.ofEpochDay ⟨-720000⟩) .UTC) - -/-- -info: "-0084-07-28" --/ -#guard_msgs in -#eval Formats.sqlDate.format (DateTime.ofLocalDateWithZone (PlainDate.ofEpochDay ⟨-750000⟩) .UTC) - -/-- -info: "-0221-09-04" --/ -#guard_msgs in -#eval Formats.sqlDate.format (DateTime.ofLocalDateWithZone (PlainDate.ofEpochDay ⟨-800000⟩) .UTC) - -/-- -info: date("-0221-09-04") --/ -#guard_msgs in -#eval PlainDate.ofEpochDay ⟨-800000⟩ - -/-- -info: date("-0221-09-04") --/ -#guard_msgs in -#eval PlainDate.ofEpochDay ⟨-800000⟩ - -/-- -info: date("2002-07-14") --/ -#guard_msgs in -#eval date("2002-07-14") - -/-- -info: time("14:13:12.000000000") --/ -#guard_msgs in -#eval time("14:13:12") - -/-- -info: zoned("2002-07-14T14:13:12.000000000Z") --/ -#guard_msgs in -#eval zoned("2002-07-14T14:13:12Z") - -/-- -info: zoned("2002-07-14T14:13:12.000000000+09:00") --/ -#guard_msgs in -#eval zoned("2002-07-14T14:13:12+09:00") - -/-- -info: "2002-07-14" --/ -#guard_msgs in -#eval zoned("2002-07-14T14:13:12+09:00").format "uuuu-MM-dd" - -/-- -info: "14-13-12" --/ -#guard_msgs in -#eval zoned("2002-07-14T14:13:12+09:00").format "HH-mm-ss" - -/- -Format --/ - -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") -def zoned₄ := zoned("2002-07-14T23:13:12.324354679+09:00") -def zoned₅ := zoned("2002-07-14T23:13:12.324354679+00:00") -def tz : TimeZone := { offset := { second := -3600 }, name := "America/Sao_Paulo", abbreviation := "BRT", isDST := false} -def zoned₆ := DateTime.ofPlainDateTime (zoned₄.toPlainDateTime) (TimeZone.ZoneRules.ofTimeZone tz) - -/-- -info: "CE CE CE Common Era C" --/ -#guard_msgs in -#eval zoned₄.format "G GG GGG GGGG GGGGG" - -/-- -info: "02 2002 000002002" --/ -#guard_msgs in -#eval zoned₄.format "yy yyyy yyyyyyyyy" - -/-- -info: "02 2002 000002002" --/ -#guard_msgs in -#eval zoned₄.format "uu uuuu uuuuuuuuu" - -/-- -info: "195 195 195" --/ -#guard_msgs in -#eval zoned₄.format "D DD DDD" - -/-- -info: "14 14 014 0014 00014" --/ -#guard_msgs in -#eval zoned₄.format "d dd ddd dddd ddddd" - -/-- -info: "7 07 Jul July J" --/ -#guard_msgs in -#eval zoned₄.format "M MM MMM MMMM MMMMM" - -/-- -info: "3 03 3rd quarter 3" --/ -#guard_msgs in -#eval zoned₄.format "Q QQ QQQQ QQQQQ" - -/-- -info: "29 29 029 0029" --/ -#guard_msgs in -#eval zoned₄.format "w ww www wwww" - -/-- -info: "3 03 003 0003" --/ -#guard_msgs in -#eval zoned₄.format "W WW WWW WWWW" - -/-- -info: "Sun Sun Sun Sunday S" --/ -#guard_msgs in -#eval zoned₄.format "E EE EEE EEEE EEEEE" - -/-- -info: "1 01 Sun Sunday S" --/ -#guard_msgs in -#eval zoned₄.format "e ee eee eeee eeeee" - -/-- -info: "2 02 002 0002" --/ -#guard_msgs in -#eval zoned₄.format "F FF FFF FFFF" - -/-- -info: "11 11 011 0011 0011" --/ -#guard_msgs in -#eval zoned₄.format "h hh hhh hhhh hhhh" - -/-- -info: "11 11 011 0011 000011" --/ -#guard_msgs in -#eval zoned₄.format "K KK KKK KKKK KKKKKK" - -/-- -info: "23 23 023 0023 000023" --/ -#guard_msgs in -#eval zoned₄.format "k kk kkk kkkk kkkkkk" - -/-- -info: "23 23 023 0023 00023" --/ -#guard_msgs in -#eval zoned₄.format "H HH HHH HHHH HHHHH" - -/-- -info: "13 13 013 0013 00013" --/ -#guard_msgs in -#eval zoned₄.format "m mm mmm mmmm mmmmm" - -/-- -info: "12 12 012 0012 00012" --/ -#guard_msgs in -#eval zoned₄.format "s ss sss ssss sssss" - +def RFC1123 : GenericFormat .any := datespec("eee, dd MMM uuuu HH:mm:ss ZZZ") +def ShortDate : GenericFormat .any := datespec("MM/dd/uuuu") +def ShortDateTime : GenericFormat .any := datespec("MM/dd/uuuu HH:mm:ss") +def FullDayTimeZone: GenericFormat .any := datespec("EEEE, MMMM dd, uuuu HH:mm:ss ZZZ") +def ISO8601Extended: GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ssXXXXX") +def LongDate : GenericFormat .any := datespec("MMMM d, uuuu") -/-- -info: "3 32 324 3243 32435" --/#guard_msgs in -#eval zoned₄.format "S SS SSS SSSS SSSSS" +/-- info: "Monday, June 16, 2014 03:03:03 -0300" -/ +#guard_msgs in #eval FullDayTimeZone.format date₁ -/-- -info: "83592324 83592324 83592324 83592324 083592324" --/ -#guard_msgs in -#eval zoned₄.format "A AA AAA AAAA AAAAAAAAA" +/-- info: "Thursday, August 15, 2024 13:28:12 -0300" -/ +#guard_msgs in #eval FullDayTimeZone.format dateBR -/-- -info: "324354679 324354679 324354679 324354679 324354679" --/ -#guard_msgs in -#eval zoned₄.format "n nn nnn nnnn nnnnnnnnn" +/-- info: "Friday, August 16, 2024 01:28:12 +0900" -/ +#guard_msgs in #eval FullDayTimeZone.format dateJP -/-- -info: "83592324354679 83592324354679 83592324354679 83592324354679 83592324354679" --/ -#guard_msgs in -#eval zoned₄.format "N NN NNN NNNN NNNNNNNNN" +/-- info: "Thursday, August 15, 2024 16:28:12 +0000" -/ +#guard_msgs in #eval FullDayTimeZone.format dateUTC -/-- -info: "+09:00" --/ -#guard_msgs in -#eval zoned₄.format "VV" +-- ISO 8601 extended format (matches Java's DateTimeFormatter.ISO_OFFSET_DATE_TIME) +/-- info: "2002-07-14T23:13:12+09:00" -/ +#guard_msgs in #eval ISO8601Extended.format zoned₄ +/-- info: "2002-07-14T23:13:12Z" -/ +#guard_msgs in #eval ISO8601Extended.format zoned₅ -/-- -info: "+09:00 +09:00 +09:00 +09:00" --/ -#guard_msgs in -#eval zoned₄.format "z zz zzzz zzzz" +-- Short date +/-- info: "06/16/2014" -/ +#guard_msgs in #eval ShortDate.formatBuilder date₁.month date₁.day date₁.year -/-- -info: "+00:00 +00:00 +00:00 +00:00" --/ -#guard_msgs in -#eval zoned₅.format "z zz zzzz zzzz" +-- Long date +/-- info: "July 14, 2002" -/ +#guard_msgs in #eval LongDate.format zoned₄ -/-- -info: "GMT+9 GMT+09:00" --/ -#guard_msgs in -#eval zoned₄.format "O OOOO" +-- RFC 1123 (HTTP date format) +/-- info: "Sun, 14 Jul 2002 23:13:12 +0900" -/ +#guard_msgs in #eval RFC1123.format zoned₄ -/-- -info: "+09 +0900 +09:00 +0900 +09:00" --/ -#guard_msgs in -#eval zoned₄.format "X XX XXX XXXX XXXXX" +-- ────────────────────────────────────────────────────────────────────────────── +-- Timezone conversion round-trips +-- ────────────────────────────────────────────────────────────────────────────── -/-- -info: "+09 +0900 +09:00 +0900 +09:00" --/ -#guard_msgs in -#eval zoned₄.format "x xx xxx xxxx xxxxx" +/-- info: "Thursday, August 15, 2024 13:28:12 -0300" -/ +#guard_msgs in #eval FullDayTimeZone.format (dateUTC.convertZoneRules (TimeZone.ZoneRules.ofTimeZone brTZ)) -/-- -info: "Z Z Z Z Z" --/ -#guard_msgs in -#eval zoned₅.format "X XX XXX XXXX XXXXX" +/-- info: "Thursday, August 15, 2024 13:28:12 -0300" -/ +#guard_msgs in #eval FullDayTimeZone.format (dateJP.convertZoneRules (TimeZone.ZoneRules.ofTimeZone brTZ)) -/-- -info: "+00 +0000 +00:00 +0000 +00:00" --/ -#guard_msgs in -#eval zoned₅.format "x xx xxx xxxx xxxxx" +/-- info: "Thursday, August 15, 2024 16:28:12 +0000" -/ +#guard_msgs in #eval FullDayTimeZone.format (dateBR.convertZoneRules (TimeZone.ZoneRules.ofTimeZone .UTC)) -/-- -info: "+0900 +0900 +0900 GMT+09:00 +09:00" --/ -#guard_msgs in -#eval zoned₄.format "Z ZZ ZZZ ZZZZ ZZZZZ" +/-- info: "Friday, August 16, 2024 01:28:12 +0900" -/ +#guard_msgs in #eval FullDayTimeZone.format (dateBR.convertZoneRules (TimeZone.ZoneRules.ofTimeZone jpTZ)) -/-- -info: "CE CE CE Common Era C" --/ -#guard_msgs in -#eval datetime₄.format "G GG GGG GGGG GGGGG" +/-- info: "Friday, August 16, 2024 01:28:12 +0900" -/ +#guard_msgs in #eval FullDayTimeZone.format (dateUTC.convertZoneRules (TimeZone.ZoneRules.ofTimeZone jpTZ)) -/-- -info: "02 2002 000002002" --/ -#guard_msgs in -#eval datetime₄.format "yy yyyy yyyyyyyyy" - -/-- -info: "02 2002 000002002" --/ -#guard_msgs in -#eval datetime₄.format "uu uuuu uuuuuuuuu" - -/-- -info: "195 195 195" --/ -#guard_msgs in -#eval datetime₄.format "D DD DDD" - -/-- -info: "7 07 Jul J" --/ -#guard_msgs in -#eval datetime₄.format "M MM MMM MMMMM" - -/-- -info: "14 14 014 0014 00014" --/ -#guard_msgs in -#eval datetime₄.format "d dd ddd dddd ddddd" - -/-- -info: "7 07 Jul July J" --/ -#guard_msgs in -#eval datetime₄.format "M MM MMM MMMM MMMMM" - -/-- -info: "14 14 0014 0014" --/#guard_msgs in -#eval datetime₄.format "d dd dddd dddd" - -/-- -info: "3 03 3rd quarter 3" --/ -#guard_msgs in -#eval datetime₄.format "Q QQ QQQQ QQQQQ" - -/-- -info: "29 29 029 0029" --/ -#guard_msgs in -#eval datetime₄.format "w ww www wwww" - -/-- -info: "3 03 003 0003" --/ -#guard_msgs in -#eval datetime₄.format "W WW WWW WWWW" +-- ────────────────────────────────────────────────────────────────────────────── +-- PlainTime formatting +-- ────────────────────────────────────────────────────────────────────────────── -/-- -info: "Sun Sun Sun Sunday S" --/ -#guard_msgs in -#eval datetime₄.format "E EE EEE EEEE EEEEE" - -/-- -info: "1 01 Sun Sunday S" --/ -#guard_msgs in -#eval datetime₄.format "e ee eee eeee eeeee" - -/-- -info: "2 02 002 0002" --/ -#guard_msgs in -#eval datetime₄.format "F FF FFF FFFF" - -/-- -info: "11 11 011 0011 0011" --/ -#guard_msgs in -#eval datetime₄.format "h hh hhh hhhh hhhh" - -/-- -info: "11 11 011 0011 000011" --/ -#guard_msgs in -#eval datetime₄.format "K KK KKK KKKK KKKKKK" - -/-- -info: "23 23 023 0023 000023" --/ -#guard_msgs in -#eval datetime₄.format "k kk kkk kkkk kkkkkk" - -/-- -info: "23 23 023 0023 00023" --/ -#guard_msgs in -#eval datetime₄.format "H HH HHH HHHH HHHHH" - -/-- -info: "13 13 013 0013 00013" --/ -#guard_msgs in -#eval datetime₄.format "m mm mmm mmmm mmmmm" - -/-- -info: "12 12 012 0012 00012" --/ -#guard_msgs in -#eval datetime₄.format "s ss sss ssss sssss" - - -/-- -info: "3 32 324 3243 32435" --/#guard_msgs in -#eval datetime₄.format "S SS SSS SSSS SSSSS" - -/-- -info: "3 32 324 3243 324354679" --/ -#guard_msgs in -#eval datetime₄.format "S SS SSS SSSS SSSSSSSSS" - -/-- -info: "83592324 83592324 83592324 83592324 083592324" --/ -#guard_msgs in -#eval datetime₄.format "A AA AAA AAAA AAAAAAAAA" - -/-- -info: "324354679 324354679 324354679 324354679 324354679" --/ -#guard_msgs in -#eval datetime₄.format "n nn nnn nnnn nnnnnnnnn" - -/-- -info: "83592324354679 83592324354679 83592324354679 83592324354679 83592324354679" --/ -#guard_msgs in -#eval datetime₄.format "N NN NNN NNNN NNNNNNNNN" - -/-- -info: "11 11 011 0011 0011" --/ -#guard_msgs in -#eval time₄.format "h hh hhh hhhh hhhh" - -/-- -info: "11 11 011 0011 000011" --/ -#guard_msgs in -#eval time₄.format "K KK KKK KKKK KKKKKK" - -/-- -info: "23 23 023 0023 000023" - --/ -#guard_msgs in -#eval time₄.format "k kk kkk kkkk kkkkkk" - -/-- -info: "23 23 023 0023 00023" --/ -#guard_msgs in -#eval time₄.format "H HH HHH HHHH HHHHH" +def time₁ := time("14:11:01") +def time₂ := time("03:11:01") +def Time24Hour : GenericFormat .any := datespec("HH:mm:ss") +def Time12Hour : GenericFormat .any := datespec("hh:mm:ss a") -/-- -info: "13 13 013 0013 00013" --/ -#guard_msgs in -#eval time₄.format "m mm mmm mmmm mmmmm" - -/-- -info: "12 12 012 0012 00012" --/ -#guard_msgs in -#eval time₄.format "s ss sss ssss sssss" +/-- info: "14:11:01" -/ +#guard_msgs in #eval Time24Hour.formatBuilder time₁.hour time₁.minute time₁.second +/-- info: "02:11:01 PM" -/ +#guard_msgs in #eval Time12Hour.formatBuilder time₁.hour.toRelative time₁.minute time₁.second (HourMarker.ofOrdinal time₁.hour) -/-- -info: "3 32 324 3243 32435" --/#guard_msgs in -#eval time₄.format "S SS SSS SSSS SSSSS" +/-- info: "03:11:01 AM" -/ +#guard_msgs in #eval Time12Hour.formatBuilder time₂.hour.toRelative time₂.minute time₂.second (HourMarker.ofOrdinal time₂.hour) -/-- -info: "3 32 324 3243 324354679" --/ -#guard_msgs in -#eval time₄.format "S SS SSS SSSS SSSSSSSSS" +-- ────────────────────────────────────────────────────────────────────────────── +-- ISO 8601 strings +-- ────────────────────────────────────────────────────────────────────────────── -/-- -info: "83592324 83592324 83592324 83592324 083592324" --/ -#guard_msgs in -#eval time₄.format "A AA AAA AAAA AAAAAAAAA" +def localTm : Second.Offset := 1723730627 +def PlainDate : PlainDateTime := PlainDateTime.ofWallTime (WallTime.ofSeconds localTm) +def dateBR₁ := DateTime.ofPlainDateTimeWithZone PlainDate brTZ +def dateUTC₁ := DateTime.ofPlainDateTimeWithZone PlainDate .UTC -/-- -info: "324354679 324354679 324354679 324354679 324354679" --/ -#guard_msgs in -#eval time₄.format "n nn nnn nnnn nnnnnnnnn" +/-- info: "2024-08-15T14:03:47-03:00" -/ +#guard_msgs in #eval dateBR₁.toISO8601String +/-- info: "2024-08-15T14:03:47Z" -/ +#guard_msgs in #eval dateUTC₁.toISO8601String -/-- -info: "83592324354679 83592324354679 83592324354679 83592324354679 83592324354679" --/ -#guard_msgs in -#eval time₄.format "N NN NNN NNNN NNNNNNNNN" +-- ────────────────────────────────────────────────────────────────────────────── +-- Historical / BC dates (SQL format) +-- ────────────────────────────────────────────────────────────────────────────── -/-- -info: "CE CE CE Common Era C" --/ -#guard_msgs in -#eval date₄.format "G GG GGG GGGG GGGGG" +/-- info: "0053-06-19" -/ +#guard_msgs in #eval Formats.sqlDate.format (DateTime.ofLocalDateWithZone (PlainDate.ofEpochDay ⟨-700000⟩) .UTC) -/-- -info: "02 2002 000002002" --/ -#guard_msgs in -#eval date₄.format "yy yyyy yyyyyyyyy" +/-- info: "-0002-09-16" -/ +#guard_msgs in #eval Formats.sqlDate.format (DateTime.ofLocalDateWithZone (PlainDate.ofEpochDay ⟨-720000⟩) .UTC) -/-- -info: "02 2002 000002002" --/ -#guard_msgs in -#eval date₄.format "uu uuuu uuuuuuuuu" +/-- info: "-0084-07-28" -/ +#guard_msgs in #eval Formats.sqlDate.format (DateTime.ofLocalDateWithZone (PlainDate.ofEpochDay ⟨-750000⟩) .UTC) -/-- -info: "195 195 195" --/ -#guard_msgs in -#eval date₄.format "D DD DDD" +/-- info: "-0221-09-04" -/ +#guard_msgs in #eval Formats.sqlDate.format (DateTime.ofLocalDateWithZone (PlainDate.ofEpochDay ⟨-800000⟩) .UTC) -/-- -info: "7 07 Jul J" --/ -#guard_msgs in -#eval date₄.format "M MM MMM MMMMM" +/-- info: date("-0221-09-04") -/ +#guard_msgs in #eval PlainDate.ofEpochDay ⟨-800000⟩ -/-- -info: "14 14 014 0014 00014" --/ -#guard_msgs in -#eval date₄.format "d dd ddd dddd ddddd" +-- ────────────────────────────────────────────────────────────────────────────── +-- Macro literals +-- ────────────────────────────────────────────────────────────────────────────── -/-- -info: "7 07 Jul July J" --/ -#guard_msgs in -#eval date₄.format "M MM MMM MMMM MMMMM" +/-- info: date("2002-07-14") -/ +#guard_msgs in #eval date("2002-07-14") -/-- -info: "14 14 0014 0014" --/#guard_msgs in -#eval date₄.format "d dd dddd dddd" +/-- info: time("14:13:12.000000000") -/ +#guard_msgs in #eval time("14:13:12") -/-- -info: "3 03 3rd quarter 3" --/ -#guard_msgs in -#eval date₄.format "Q QQ QQQQ QQQQQ" +/-- info: zoned("2002-07-14T14:13:12.000000000Z") -/ +#guard_msgs in #eval zoned("2002-07-14T14:13:12Z") -/-- -info: "29 29 029 0029" --/ -#guard_msgs in -#eval date₄.format "w ww www wwww" +/-- info: zoned("2002-07-14T14:13:12.000000000+09:00") -/ +#guard_msgs in #eval zoned("2002-07-14T14:13:12+09:00") -/-- -info: "3 03 003 0003" --/ -#guard_msgs in -#eval date₄.format "W WW WWW WWWW" +/-- info: "2002-07-14" -/ +#guard_msgs in #eval zoned("2002-07-14T14:13:12+09:00").format "uuuu-MM-dd" -/-- -info: "Sun Sun Sun Sunday S" --/ -#guard_msgs in -#eval date₄.format "E EE EEE EEEE EEEEE" +/-- info: "14-13-12" -/ +#guard_msgs in #eval zoned("2002-07-14T14:13:12+09:00").format "HH-mm-ss" -/-- -info: "1 01 Sun Sunday S" --/ -#guard_msgs in -#eval date₄.format "e ee eee eeee eeeee" +-- ────────────────────────────────────────────────────────────────────────────── +-- Error / boundary cases +-- ────────────────────────────────────────────────────────────────────────────── -/-- -info: "2 02 002 0002" --/ -#guard_msgs in -#eval date₄.format "F FF FFF FFFF" +def DateSmall : GenericFormat .any := datespec("uu-MM-dd") -/-- -info: "-2000 2001 BCE" --/ -#guard_msgs in -#eval datetime₅.format "uuuu yyyy G" +/-- info: Except.error "offset 0: condition not satisfied" -/ +#guard_msgs in #eval DateSmall.parse "-23-12-12" -/-- -info: "2002 2002 CE" --/ -#guard_msgs in -#eval datetime₄.format "uuuu yyyy G" +/-- info: zoned("2002-07-14T14:13:12.000000000+23:59") -/ +#guard_msgs in #eval zoned("2002-07-14T14:13:12+23:59") -/-- -info: "BRT BRT BRT America/Sao_Paulo America/Sao_Paulo" --/ -#guard_msgs in -#eval zoned₆.format "z zz zzz zzzz zzzz" +/-- info: Except.error "offset 22: invalid hour offset: 24. Must be between 0 and 23." -/ +#guard_msgs in #eval DateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+24:59" -/-- -info: 1 --/ -#guard_msgs in -#eval - let t : DateTime := .ofPlainDateTime datetime("2018-12-31T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC) - IO.println s!"{t.format "w"}" +/-- info: Except.error "offset 25: invalid minute offset: 60. Must be between 0 and 59." -/ +#guard_msgs in #eval DateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+23:60" -/-- -info: Except.error "offset 0: condition not satisfied" --/ -#guard_msgs in -#eval DateSmall.parse "-23-12-12" +/-- info: Except.ok (zoned("2002-07-14T14:13:12.000000000Z")) -/ +#guard_msgs in #eval DateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+00:00" -/- -Truncation Test --/ +-- ────────────────────────────────────────────────────────────────────────────── +-- Large / truncated year round-trip +-- ────────────────────────────────────────────────────────────────────────────── -/-- -info: ("19343232432-01-04T01:04:03.000000000", +/-- info: ("19343232432-01-04T01:04:03.000000000", Except.error "offset 4: expected: -", - datetime("1932-01-02T05:04:03.000000000")) --/ + datetime("1932-01-02T05:04:03.000000000")) -/ #guard_msgs in #eval let r := PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (PlainTime.mk 25 64 3 0) @@ -829,136 +690,85 @@ info: ("19343232432-01-04T01:04:03.000000000", let r := PlainDateTime.parse s (s, r, datetime("1932-01-02T05:04:03.000000000")) +-- ────────────────────────────────────────────────────────────────────────────── +-- Parse width tests +-- ────────────────────────────────────────────────────────────────────────────── + def tuple2Mk (a : f) (b : g) := some (a, b) def tuple3Mk (a : f) (b : g) (c : h) := some (a, b, c) def tuple4Mk (a : f) (b : g) (c : h) (d : i) := some (a, b, c, d) def tuple5Mk (a : f) (b : g) (c : h) (d : i) (e : j) := some (a, b, c, d, e) -def tuple6Mk (a : f) (b : g) (c : h) (d : i) (e : j) (k : z) := some (a, b, c, d, e, k) - - -/- -Parsing Length Tests --/ +-- u (proleptic year: any / 2-digit / 4-digit / 5-digit) def uFormat : GenericFormat .any := datespec("u uu uuuu uuuuu") - #eval do assert! (uFormat.parseBuilder tuple4Mk "1 11 1211 12311" |>.isOk) #eval do assert! (uFormat.parseBuilder tuple4Mk "12 11 1211 12311" |>.isOk) #eval do assert! (uFormat.parseBuilder tuple4Mk "123443 11 1211 12311" |>.isOk) #eval do assert! (uFormat.parseBuilder tuple4Mk "-1 11 1211 12311" |>.isOk) #eval do assert! (uFormat.parseBuilder tuple4Mk "1 11 -1211 12311" |>.isOk) #eval do assert! (uFormat.parseBuilder tuple4Mk "1 11 1211 -12311" |>.isOk) - #eval do assert! (not <| uFormat.parseBuilder tuple4Mk "1 -11 1211 12311" |>.isOk) #eval do assert! (not <| uFormat.parseBuilder tuple4Mk "11 1211 12134" |>.isOk) #eval do assert! (not <| uFormat.parseBuilder tuple4Mk "1 1 12 1234" |>.isOk) #eval do assert! (not <| uFormat.parseBuilder tuple4Mk "1 11 1213 111123" |>.isOk) -#eval do assert! (not <| uFormat.parseBuilder tuple4Mk "1 367 1211 12311" |>.isOk) +-- y (year-of-era: always positive) def yFormat : GenericFormat .any := datespec("y yy yyyy yyyyy") - #eval do assert! (yFormat.parseBuilder tuple4Mk "1 11 1211 12311" |>.isOk) #eval do assert! (yFormat.parseBuilder tuple4Mk "12 11 1211 12311" |>.isOk) #eval do assert! (yFormat.parseBuilder tuple4Mk "123443 11 1211 12311" |>.isOk) - #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "-1 11 1211 12311" |>.isOk) #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 -11 1211 12311" |>.isOk) #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 11 -1211 12311" |>.isOk) -#eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 11 1211 -12311" |>.isOk) #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "11 1211 12134" |>.isOk) #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 1 12 1234" |>.isOk) #eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 11 1213 111123" |>.isOk) -#eval do assert! (not <| yFormat.parseBuilder tuple4Mk "1 367 1211 12311" |>.isOk) - -def dFormat : GenericFormat .any := datespec("D DD DDD") - -#eval do assert! (dFormat.parseBuilder tuple3Mk "1 12 123" |>.isOk) -#eval do assert! (dFormat.parseBuilder tuple3Mk "323 12 123" |>.isOk) - -#eval do assert! (not <| dFormat.parseBuilder tuple3Mk "1 12 1234" |>.isOk) -#eval do assert! (not <| dFormat.parseBuilder tuple3Mk "1 123 123" |>.isOk) -#eval do assert! (not <| dFormat.parseBuilder tuple3Mk "367 12 123" |>.isOk) - -def dddFormat : GenericFormat .any := datespec("d dd ddd dddd ddddd") - -#eval do assert! (dddFormat.parseBuilder tuple5Mk "1 12 031 0031 00031" |>.isOk) -#eval do assert! (dddFormat.parseBuilder tuple5Mk "000031 12 031 0031 00031" |>.isOk) - -#eval do assert! (not <| dddFormat.parseBuilder tuple5Mk "1 12 0031 00031" |>.isOk) -#eval do assert! (not <| dddFormat.parseBuilder tuple5Mk "1 031 0031 000031" |>.isOk) - -def wFormat : GenericFormat .any := datespec("w ww www wwww") - -#eval do assert! (wFormat.parseBuilder tuple4Mk "1 01 031 0031" |>.isOk) -#eval do assert! (wFormat.parseBuilder tuple4Mk "2 01 031 0031" |>.isOk) - -#eval do assert! (not <| wFormat.parseBuilder tuple4Mk "2 01 031 00310" |>.isOk) -#eval do assert! (not <| wFormat.parseBuilder tuple4Mk "2 01 031 031" |>.isOk) +-- D (day-of-year: 1–3 letters) +def doyFormat : GenericFormat .any := datespec("D DD DDD") +#eval do assert! (doyFormat.parseBuilder tuple3Mk "1 12 123" |>.isOk) +#eval do assert! (doyFormat.parseBuilder tuple3Mk "323 12 123" |>.isOk) +#eval do assert! (not <| doyFormat.parseBuilder tuple3Mk "1 12 1234" |>.isOk) +#eval do assert! (not <| doyFormat.parseBuilder tuple3Mk "1 123 123" |>.isOk) + +-- d (day-of-month: 1–2 letters) +def domFormat : GenericFormat .any := datespec("d dd") +#eval do assert! (domFormat.parseBuilder tuple2Mk "1 12" |>.isOk) +#eval do assert! (domFormat.parseBuilder tuple2Mk "31 12" |>.isOk) +#eval do assert! (not <| domFormat.parseBuilder tuple2Mk "1 123" |>.isOk) + +-- w (week-of-year: 1–2 letters) +def wFormat : GenericFormat .any := datespec("w ww") +#eval do assert! (wFormat.parseBuilder tuple2Mk "1 01" |>.isOk) +#eval do assert! (wFormat.parseBuilder tuple2Mk "2 01" |>.isOk) +#eval do assert! (not <| wFormat.parseBuilder tuple2Mk "2 001" |>.isOk) + +-- q (quarter: 1–2 numeric letters) def qFormat : GenericFormat .any := datespec("q qq") - #eval do assert! (qFormat.parseBuilder tuple2Mk "1 02" |>.isOk) #eval do assert! (qFormat.parseBuilder tuple2Mk "3 03" |>.isOk) - #eval do assert! (not <| qFormat.parseBuilder tuple2Mk "12 32" |>.isOk) -#eval do assert! (not <| qFormat.parseBuilder tuple2Mk "000001 003" |>.isOk) -def WFormat : GenericFormat .any := datespec("W WW") - -#eval do assert! (WFormat.parseBuilder tuple2Mk "1 06" |>.isOk) -#eval do assert! (WFormat.parseBuilder tuple2Mk "3 03" |>.isOk) - -#eval do assert! (not <| WFormat.parseBuilder tuple2Mk "12 32" |>.isOk) -#eval do assert! (not <| WFormat.parseBuilder tuple2Mk "000001 003" |>.isOk) +-- W (week-of-month: 1 letter only) +def WFormat : GenericFormat .any := datespec("W") +#eval do assert! (WFormat.parseBuilder (fun x => some x) "1" |>.isOk) +#eval do assert! (WFormat.parseBuilder (fun x => some x) "5" |>.isOk) +#eval do assert! (not <| WFormat.parseBuilder (fun x => some x) "12" |>.isOk) +-- e (localized weekday: 1–2 numeric letters) def eFormat : GenericFormat .any := datespec("e ee") - #eval do assert! (eFormat.parseBuilder tuple2Mk "1 07" |>.isOk) #eval do assert! (eFormat.parseBuilder tuple2Mk "3 03" |>.isOk) - #eval do assert! (not <| eFormat.parseBuilder tuple2Mk "12 32" |>.isOk) -#eval do assert! (not <| eFormat.parseBuilder tuple2Mk "000001 003" |>.isOk) - -def FFormat : GenericFormat .any := datespec("F FF") - -#eval do assert! (FFormat.parseBuilder tuple2Mk "1 04" |>.isOk) -#eval do assert! (FFormat.parseBuilder tuple2Mk "3 03" |>.isOk) -#eval do assert! (not <| FFormat.parseBuilder tuple2Mk "12 32" |>.isOk) -#eval do assert! (not <| FFormat.parseBuilder tuple2Mk "000001 003" |>.isOk) +-- F (day-of-week-in-month: 1 letter only) +def FFormat : GenericFormat .any := datespec("F") +#eval do assert! (FFormat.parseBuilder (fun x => some x) "1" |>.isOk) +#eval do assert! (FFormat.parseBuilder (fun x => some x) "5" |>.isOk) +#eval do assert! (not <| FFormat.parseBuilder (fun x => some x) "12" |>.isOk) +-- h (clock-hour 1–12: 1–2 letters) def hFormat : GenericFormat .any := datespec("h hh") - #eval do assert! (hFormat.parseBuilder tuple2Mk "1 09" |>.isOk) #eval do assert! (hFormat.parseBuilder tuple2Mk "12 12" |>.isOk) - #eval do assert! (not <| hFormat.parseBuilder tuple2Mk "12 32" |>.isOk) -#eval do assert! (not <| hFormat.parseBuilder tuple2Mk "000001 003" |>.isOk) - -/- -Error tests with some formats. --/ - -/-- -info: zoned("2002-07-14T14:13:12.000000000+23:59") --/ -#guard_msgs in -#eval zoned("2002-07-14T14:13:12+23:59") - -/-- -info: Except.error "offset 22: invalid hour offset: 24. Must be between 0 and 23." --/ -#guard_msgs in -#eval DateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+24:59" - -/-- -info: Except.error "offset 25: invalid minute offset: 60. Must be between 0 and 59." --/ -#guard_msgs in -#eval DateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+23:60" - -/-- -info: Except.ok (zoned("2002-07-14T14:13:12.000000000Z")) --/ -#guard_msgs in -#eval DateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+00:00" diff --git a/tests/elab/versoDocs.lean b/tests/elab/versoDocs.lean index f83e5e3c62f7..921fe9c64651 100644 --- a/tests/elab/versoDocs.lean +++ b/tests/elab/versoDocs.lean @@ -242,6 +242,7 @@ error: Unknown constant `b` Hint: Insert a fully-qualified name: • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲A̲.̲b̲)̲}`b` • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲M̲e̲t̲a̲.̲G̲r̲i̲n̲d̲.̲A̲r̲i̲t̲h̲.̲C̲u̲t̲s̲a̲t̲.̲D̲v̲d̲S̲o̲l̲u̲t̲i̲o̲n̲.̲b̲)̲}`b` + • {name ̲(̲f̲u̲l̲l̲ ̲:̲=̲ ̲S̲t̲d̲.̲T̲i̲m̲e̲.̲M̲o̲d̲i̲f̲i̲e̲r̲.̲b̲)̲}`b` -/ #guard_msgs in /-- diff --git a/tests/elab/versoDocs.lean.out.expected b/tests/elab/versoDocs.lean.out.expected index c1b6876370d6..1b12dc5bbede 100644 --- a/tests/elab/versoDocs.lean.out.expected +++ b/tests/elab/versoDocs.lean.out.expected @@ -5,7 +5,7 @@ Nat.gcd.induction' {P : Nat → Nat → Prop} (m n : Nat) (H0 : ∀ (n : Nat), P (H1 : ∀ (m n : Nat), 0 < m → P (n % m) m → P m n) : P m n something : Unit yetMore' : Unit -versoDocs.lean:631:43-631:53: warning: Code element could be more specific. +versoDocs.lean:632:43-632:53: warning: Code element could be more specific. Hint: Insert a role to document it: • {̲l̲e̲a̲n̲}̲`-checked`