diff --git a/src/Std/Time.lean b/src/Std/Time.lean index 14d3b57cc9..159a273e67 100644 --- a/src/Std/Time.lean +++ b/src/Std/Time.lean @@ -129,16 +129,22 @@ Format strings are used to convert between `String` representations and date/tim 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 `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 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"). - `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. - `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! diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean index 7b14a3cc7c..e8b3527b9f 100644 --- a/src/Std/Time/Format/Basic.lean +++ b/src/Std/Time/Format/Basic.lean @@ -98,6 +98,8 @@ 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") -/ @@ -112,10 +114,12 @@ namespace Year `classify` classifies the number of pattern letters into a `Year` format. -/ def classify (num : Nat) : Option Year := - if num = 2 then - some (.twoDigit) + if num = 1 then + some .any + else if num = 2 then + some .twoDigit else if num = 4 then - some (.fourDigit) + some .fourDigit else if num > 4 ∨ num = 3 then some (.extended num) else @@ -787,11 +791,13 @@ private def formatWith (modifier : Modifier) (data: TypeFormat modifier) : Strin let info := data.toInt let info := if info ≤ 0 then -info + 1 else info match format with + | .any => pad 0 (data.toInt) | .twoDigit => pad 2 (info % 100) | .fourDigit => pad 4 info | .extended n => pad n info | .u format => match format with + | .any => pad 0 (data.toInt) | .twoDigit => pad 2 (data.toInt % 100) | .fourDigit => pad 4 data.toInt | .extended n => pad n data.toInt @@ -1076,6 +1082,9 @@ private def parseAtLeastNum (size : Nat) : Parser Nat := let end_ ← manyChars (satisfy Char.isDigit) pure (start ++ end_) +private def parseFlexibleNum (size : Nat) : Parser Nat := + if size = 1 then parseAtLeastNum 1 else parseNum size + private def parseFractionNum (size : Nat) (pad : Nat) : Parser Nat := String.toNat! <$> rightPad pad '0' <$> exactlyChars (satisfy Char.isDigit) size @@ -1121,30 +1130,32 @@ private def parseWith : (mod : Modifier) → Parser (TypeFormat mod) | .narrow => parseEraNarrow | .y format => match format with - | .twoDigit => (2000 + ·) <$> (Int.ofNat <$> parseNum 2) + | .any => Int.ofNat <$> parseAtLeastNum 1 + | .twoDigit => (2000 + ·) <$> Int.ofNat <$> parseNum 2 | .fourDigit => Int.ofNat <$> parseNum 4 - | .extended n => Int.ofNat <$> parseAtLeastNum n + | .extended n => Int.ofNat <$> parseNum n | .u format => match format with - | .twoDigit => (2000 + ·) <$> (parseSigned <| parseNum 2) - | .fourDigit => parseSigned <| parseAtLeastNum 4 - | .extended n => parseSigned <| parseAtLeastNum n - | .D format => Sigma.mk true <$> parseNatToBounded (parseAtLeastNum format.padding) + | .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 => match format with - | .inl format => parseNatToBounded (parseAtLeastNum format.padding) + | .inl format => parseNatToBounded (parseFlexibleNum format.padding) | .inr .short => parseMonthShort | .inr .full => parseMonthLong | .inr .narrow => parseMonthNarrow - | .d format => parseNatToBounded (parseAtLeastNum format.padding) + | .d format => parseNatToBounded (parseFlexibleNum format.padding) | .Qorq format => match format with - | .inl format => parseNatToBounded (parseAtLeastNum format.padding) + | .inl format => parseNatToBounded (parseFlexibleNum format.padding) | .inr .short => parseQuarterShort | .inr .full => parseQuarterLong | .inr .narrow => parseQuarterNumber - | .w format => parseNatToBounded (parseAtLeastNum format.padding) - | .W format => parseNatToBounded (parseAtLeastNum format.padding) + | .w format => parseNatToBounded (parseFlexibleNum format.padding) + | .W format => parseNatToBounded (parseFlexibleNum format.padding) | .E format => match format with | .short => parseWeekdayShort @@ -1152,29 +1163,29 @@ private def parseWith : (mod : Modifier) → Parser (TypeFormat mod) | .narrow => parseWeekdayNarrow | .eorc format => match format with - | .inl format => Weekday.ofOrdinal <$> parseNatToBounded (parseAtLeastNum format.padding) + | .inl format => Weekday.ofOrdinal <$> parseNatToBounded (parseFlexibleNum format.padding) | .inr .short => parseWeekdayShort | .inr .full => parseWeekdayLong | .inr .narrow => parseWeekdayNarrow - | .F format => parseNatToBounded (parseAtLeastNum format.padding) + | .F format => parseNatToBounded (parseFlexibleNum format.padding) | .a format => match format with | .short => parseMarkerShort | .full => parseMarkerLong | .narrow => parseMarkerNarrow - | .h format => parseNatToBounded (parseAtLeastNum format.padding) - | .K format => parseNatToBounded (parseAtLeastNum format.padding) - | .k format => parseNatToBounded (parseAtLeastNum format.padding) - | .H format => parseNatToBounded (parseAtLeastNum format.padding) - | .m format => parseNatToBounded (parseAtLeastNum format.padding) - | .s format => parseNatToBounded (parseAtLeastNum format.padding) + | .h format => parseNatToBounded (parseFlexibleNum format.padding) + | .K format => parseNatToBounded (parseFlexibleNum format.padding) + | .k format => parseNatToBounded (parseFlexibleNum format.padding) + | .H format => parseNatToBounded (parseFlexibleNum format.padding) + | .m format => parseNatToBounded (parseFlexibleNum format.padding) + | .s format => parseNatToBounded (parseFlexibleNum format.padding) | .S format => match format with - | .nano => parseNatToBounded (parseAtLeastNum 9) + | .nano => parseNatToBounded (parseFlexibleNum 9) | .truncated n => parseNatToBounded (parseFractionNum n 9) - | .A format => Millisecond.Offset.ofNat <$> (parseAtLeastNum format.padding) - | .n format => parseNatToBounded (parseAtLeastNum format.padding) - | .N format => Nanosecond.Offset.ofNat <$> (parseAtLeastNum format.padding) + | .A format => Millisecond.Offset.ofNat <$> (parseFlexibleNum format.padding) + | .n format => parseNatToBounded (parseFlexibleNum format.padding) + | .N format => Nanosecond.Offset.ofNat <$> (parseFlexibleNum format.padding) | .V => parseIdentifier | .z format => match format with diff --git a/src/Std/Time/Notation.lean b/src/Std/Time/Notation.lean index d59f9588db..013b79a047 100644 --- a/src/Std/Time/Notation.lean +++ b/src/Std/Time/Notation.lean @@ -29,6 +29,7 @@ private def convertFraction : Fraction → MacroM (TSyntax `term) | .truncated digits => `(Std.Time.Fraction.truncated $(quote digits)) private def convertYear : Year → MacroM (TSyntax `term) + | .any => `(Std.Time.Year.any) | .twoDigit => `(Std.Time.Year.twoDigit) | .fourDigit => `(Std.Time.Year.fourDigit) | .extended n => `(Std.Time.Year.extended $(quote n)) diff --git a/src/Std/Time/Notation/Spec.lean b/src/Std/Time/Notation/Spec.lean index cd77dd4948..64d7f7fea5 100644 --- a/src/Std/Time/Notation/Spec.lean +++ b/src/Std/Time/Notation/Spec.lean @@ -27,6 +27,7 @@ private def convertFraction : Fraction → MacroM (TSyntax `term) | .truncated digits => `(Std.Time.Fraction.truncated $(quote digits)) private def convertYear : Year → MacroM (TSyntax `term) + | .any => `(Std.Time.Year.any) | .twoDigit => `(Std.Time.Year.twoDigit) | .fourDigit => `(Std.Time.Year.fourDigit) | .extended n => `(Std.Time.Year.extended $(quote n)) diff --git a/tests/lean/run/timeFormats.lean b/tests/lean/run/timeFormats.lean index 8c36f2c284..824a666962 100644 --- a/tests/lean/run/timeFormats.lean +++ b/tests/lean/run/timeFormats.lean @@ -12,6 +12,7 @@ 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 @@ -795,13 +796,20 @@ info: 1 let t : ZonedDateTime := .ofPlainDateTime datetime("2018-12-31T12:00:00") (TimeZone.ZoneRules.ofTimeZone TimeZone.UTC) IO.println s!"{t.format "w"}" + +/-- +info: Except.error "offset 0: condition not satisfied" +-/ +#guard_msgs in +#eval DateSmall.parse "-23-12-12" + /- Truncation Test -/ /-- info: ("19343232432-01-04T01:04:03.000000000", - Except.ok (datetime("19343232432-01-04T01:04:03.000000000")), + Except.error "offset 4: expected: -", datetime("1932-01-02T05:04:03.000000000")) -/ #guard_msgs in @@ -810,3 +818,109 @@ info: ("19343232432-01-04T01:04:03.000000000", let s := r.toLeanDateTimeString let r := PlainDateTime.parse s (s, r, datetime("1932-01-02T05:04:03.000000000")) + +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 +-/ + +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) + +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) + +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) + +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) + +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)