feat: add FormatConfig for GenericFormat with leap second validation

src/Std/Time/Format/Basic.lean

@@ -571,13 +571,29 @@ private def getD (x : Awareness) (default : TimeZone) : TimeZone :=
 
 end Awareness
 
+/--
+Configuration options for formatting and parsing date/time strings.
+-/
+structure FormatConfig where
+  /--
+  Whether to allow leap seconds, such as `2016-12-31T23:59:60Z`.
+  Default is `false`.
+  -/
+  allowLeapSeconds : Bool := false
+
+deriving Inhabited, Repr
+
 /--
 A specification on how to format a data or parse some string.
 -/
 structure GenericFormat (awareness : Awareness) where
+  /--
+  Configuration options for formatting behavior.
+  -/
+  config : FormatConfig
 
   /--
-  The format that is not aware of the timezone.
+  The format string used for parsing and formatting.
   -/
   string : FormatString
   deriving Inhabited, Repr
@@ -1107,6 +1123,9 @@ private def parseOffset (withMinutes : Reason) (withSeconds : Reason) (withColon
   let sign ← (pchar '+' *> pure 1) <|> (pchar '-' *> pure (-1))
   let hours : Hour.Offset ← UnitVal.ofInt <$> parseNum 2
 
+  if hours.val < 0 ∨ hours.val > 23 then
+    fail s!"invalid hour offset: {hours.val}. Must be between 0 and 23."
+
   let colon := if withColon then pchar ':' else pure ':'
 
   let parseUnit {n} (reason : Reason) : Parser (Option (UnitVal n)) :=
@@ -1116,13 +1135,22 @@ private def parseOffset (withMinutes : Reason) (withSeconds : Reason) (withColon
     | .optional => optional (colon *> UnitVal.ofInt <$> parseNum 2)
 
   let minutes : Option Minute.Offset ← parseUnit withMinutes
+
+  if let some m := minutes then
+    if m.val > 59 then
+      fail s!"invalid minute offset: {m.val}. Must be between 0 and 59."
+
   let seconds : Option Second.Offset ← parseUnit withSeconds
 
+  if let some s := seconds then
+    if s.val > 59 then
+      fail s!"invalid second offset: {s.val}. Must be between 0 and 59."
+
   let hours := hours.toSeconds + (minutes.getD 0).toSeconds + (seconds.getD 0)
 
   return Offset.ofSeconds ⟨hours.val * sign⟩
 
-private def parseWith : (mod : Modifier) → Parser (TypeFormat mod)
+private def parseWith (config : FormatConfig) : (mod : Modifier) → Parser (TypeFormat mod)
   | .G format =>
     match format with
     | .short => parseEraShort
@@ -1178,7 +1206,12 @@ private def parseWith : (mod : Modifier) → Parser (TypeFormat mod)
   | .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 =>
+    if config.allowLeapSeconds then
+      parseNatToBounded (parseFlexibleNum format.padding)
+    else do
+      let res : Bounded.LE 0 59 ← parseNatToBounded (parseFlexibleNum format.padding)
+      return res.expandTop (by decide)
   | .S format =>
     match format with
     | .nano => parseNatToBounded (parseFlexibleNum 9)
@@ -1367,27 +1400,27 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type :=
 
 end DateBuilder
 
-private def parseWithDate (date : DateBuilder) (mod : FormatPart) : Parser DateBuilder := do
+private def parseWithDate (date : DateBuilder) (config : FormatConfig) (mod : FormatPart) : Parser DateBuilder := do
   match mod with
   | .modifier s => do
-    let res ← parseWith s
+    let res ← parseWith config s
     return date.insert s res
   | .string s => pstring s *> pure date
 
 /--
 Constructs a new `GenericFormat` specification for a date-time string. Modifiers can be combined to create
 custom formats, such as "YYYY, MMMM, D".
 -/
-def spec (input : String) : Except String (GenericFormat tz) := do
+def spec (input : String) (config : FormatConfig := {}) : Except String (GenericFormat tz) := do
   let string ← specParser.run input
-  return ⟨string⟩
+  return ⟨config, string⟩
 
 /--
 Builds a `GenericFormat` from the input string. If parsing fails, it will panic
 -/
-def spec! (input : String) : GenericFormat tz :=
+def spec! (input : String) (config : FormatConfig := {}) : GenericFormat tz :=
   match specParser.run input with
-  | .ok res => ⟨res⟩
+  | .ok res => ⟨config, res⟩
   | .error res => panic! res
 
 /--
@@ -1402,10 +1435,10 @@ def format (format : GenericFormat aw) (date : DateTime tz) : String :=
   format.string.map mapper
   |> String.join
 
-private def parser (format : FormatString) (aw : Awareness) : Parser (aw.type) :=
+private def parser (format : FormatString) (config : FormatConfig) (aw : Awareness) : Parser (aw.type) :=
   let rec go (builder : DateBuilder) (x : FormatString) : Parser aw.type :=
     match x with
-    | x :: xs => parseWithDate builder x >>= (go · xs)
+    | x :: xs => parseWithDate builder config x >>= (go · xs)
     | [] =>
       match builder.build aw with
       | some res => pure res
@@ -1415,11 +1448,11 @@ private def parser (format : FormatString) (aw : Awareness) : Parser (aw.type) :
 /--
 Parser for a format with a builder.
 -/
-def builderParser (format: FormatString) (func: FormatType (Option α) format) : Parser α :=
+def builderParser (format: FormatString) (config : FormatConfig) (func: FormatType (Option α) format) : Parser α :=
   let rec go (format : FormatString) (func: FormatType (Option α) format) : Parser α :=
     match format with
     | .modifier x :: xs => do
-      let res ← parseWith x
+      let res ← parseWith config x
       go xs (func res)
     | .string s :: xs => skipString s *> (go xs func)
     | [] =>
@@ -1432,7 +1465,7 @@ def builderParser (format: FormatString) (func: FormatType (Option α) format) :
 Parses the input string into a `ZoneDateTime`.
 -/
 def parse (format : GenericFormat aw) (input : String) : Except String aw.type :=
-  (parser format.string aw <* eof).run input
+  (parser format.string format.config aw <* eof).run input
 
 /--
 Parses the input string into a `ZoneDateTime` and panics if its wrong.
@@ -1446,7 +1479,7 @@ def parse! (format : GenericFormat aw) (input : String) : aw.type :=
 Parses an input string using a builder function to produce a value.
 -/
 def parseBuilder (format : GenericFormat aw)  (builder : FormatType (Option α) format.string) (input : String) : Except String α :=
-  (builderParser format.string builder).run input
+  (builderParser format.string format.config builder).run input
 
 /--
 Parses an input string using a builder function, panicking on errors.

src/Std/Time/Notation/Spec.lean

@@ -101,14 +101,23 @@ Syntax for defining a date spec at compile time.
 -/
 syntax "datespec(" str ")" : term
 
+/--
+Syntax for defining a date spec and configuration of this date spec at compile time.
+-/
+syntax "datespec(" str "," term ")" : term
+
+def formatStringToFormat (fmt : TSyntax `str) (config : Option (TSyntax `term)) : MacroM (TSyntax `term) := do
+  let input := fmt.getString
+  let format : Except String (GenericFormat .any) := GenericFormat.spec input
+  match format with
+  | .ok res =>
+    let alts ← res.string.mapM convertFormatPart
+    let alts := alts.foldl Syntax.TSepArray.push (Syntax.TSepArray.mk #[] (sep := ","))
+    let config := config.getD (← `({}))
+    `(⟨$config, [$alts,*]⟩)
+  | .error err =>
+    Macro.throwErrorAt fmt s!"cannot compile spec: {err}"
+
 macro_rules
-  | `(datespec( $format_string:str )) => do
-    let input := format_string.getString
-    let format : Except String (GenericFormat .any) := GenericFormat.spec input
-    match format with
-    | .ok res =>
-      let alts ← res.string.mapM convertFormatPart
-      let alts := alts.foldl Syntax.TSepArray.push (Syntax.TSepArray.mk #[] (sep := ","))
-      `(⟨[$alts,*]⟩)
-    | .error err =>
-      Macro.throwErrorAt format_string s!"cannot compile spec: {err}"
+  | `(datespec( $fmt:str )) => formatStringToFormat fmt none
+  | `(datespec( $fmt:str, $config:term )) => formatStringToFormat fmt config

tests/lean/run/timeFormats.lean

@@ -924,3 +924,31 @@ def hFormat : GenericFormat .any := datespec("h hh")
 
 #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 ZonedDateTime.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 ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+23:60"
+
+/--
+info: Except.ok (zoned("2002-07-14T14:13:12.000000000Z"))
+-/
+#guard_msgs in
+#eval ZonedDateTime.fromLeanDateTimeWithZoneString "2002-07-14T14:13:12+00:00"

tests/lean/run/timeLimits.lean

@@ -0,0 +1,77 @@
+import Std.Time
+open Std.Time
+
+
+def ISO8601UTCAllow : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := true })
+def ISO8601UTCNot : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ", { allowLeapSeconds := false })
+def ISO8601UTCDef : GenericFormat .any := datespec("uuuu-MM-dd'T'HH:mm:ss.SSSSSSSSSZ")
+
+/--
+info: Except.ok (zoned("2002-07-14T23:14:00.324354679-23:59"))
+-/
+#guard_msgs in
+#eval ISO8601UTCAllow.parse "2002-07-14T23:13:60.324354679-2359"
+
+/--
+info: Except.error "offset 19: need a natural number in the interval of 0 to 59"
+-/
+#guard_msgs in
+#eval ISO8601UTCNot.parse "2002-07-14T23:13:60.324354679-2359"
+
+/--
+info: Except.error "offset 19: need a natural number in the interval of 0 to 59"
+-/
+#guard_msgs in
+#eval ISO8601UTCDef.parse "2002-07-14T23:13:60.324354679-2359"
+
+/-
+Offset
+-/
+
+/--
+info: Except.error "offset 32: invalid hour offset: 24. Must be between 0 and 23."
+-/
+#guard_msgs in
+#eval ISO8601UTCAllow.parse "2002-07-14T23:14:00.324354679+2400"
+
+/--
+info: Except.error "offset 32: invalid hour offset: 99. Must be between 0 and 23."
+-/
+#guard_msgs in
+#eval ISO8601UTCAllow.parse "2002-07-14T23:14:00.324354679+9900"
+
+/--
+info: Except.error "offset 34: invalid minute offset: 99. Must be between 0 and 59."
+-/
+#guard_msgs in
+#eval ISO8601UTCAllow.parse "2002-07-14T23:14:00.324354679+0099"
+
+/--
+info: Except.ok (zoned("2002-07-14T23:14:00.324354679-23:59"))
+-/
+#guard_msgs in
+#eval ISO8601UTCAllow.parse "2002-07-14T23:14:00.324354679-2359"
+
+/--
+info: Except.ok (zoned("2002-07-14T23:14:00.324354679+23:59"))
+-/
+#guard_msgs in
+#eval ISO8601UTCAllow.parse "2002-07-14T23:14:00.324354679+2359"
+
+/--
+info: Except.error "offset 32: invalid hour offset: 24. Must be between 0 and 23."
+-/
+#guard_msgs in
+#eval ISO8601UTCAllow.parse "2002-07-14T23:14:00.324354679-2400"
+
+/--
+info: Except.error "offset 32: invalid hour offset: 99. Must be between 0 and 23."
+-/
+#guard_msgs in
+#eval ISO8601UTCAllow.parse "2002-07-14T23:14:00.324354679-9900"
+
+/--
+info: Except.error "offset 34: invalid minute offset: 99. Must be between 0 and 59."
+-/
+#guard_msgs in
+#eval ISO8601UTCAllow.parse "2002-07-14T23:14:00.324354679-0099"