3.3. Parser🔗

Datetime.parse delegates the five accepted forms to Std.Time.GenericFormat.parse, one fixed format string per form, tried in order:

public def parse (str: String) : Option Datetime := do
  if dateContainsLeapSeconds str then failure
  if !checkOffsetLen str then failure
  if !tzOffsetMinsLt60 str then failure
  let val :=
    DateOnly.parse str <|>
    DateUTC.parse str <|>
    DateUTCWithMillis.parse str <|>
    DateWithOffset.parse str <|>
    DateWithOffsetAndMillis.parse str

  let zonedTime ← val.toOption
  if zonedTime.timezone.offset.second.val.natAbs < MAX_OFFSET_SECONDS
  then datetime? zonedTime.toTimestamp.toMillisecondsSinceUnixEpoch.toInt
  else none

Three Boolean guards precede the alternation, restricting Std.Time's formats to the Cedar grammar: leap seconds (ss = 60) are rejected, timezone offsets must contain exactly four digits after the sign, and the offset minutes must be below 60. The explicit offset-width guard is needed because Lean 4.33's Std.Time parser accepts one or two digits for each offset field. A final range check bounds the timezone offset, and datetime? narrows the epoch-millisecond value to Int64.

Each of the five grammar forms parses to its epoch-millisecond value; grammar or constraint violations are rejected:

some { val := { toUInt64 := 1705276800000 } }#eval Datetime.parse "2024-01-15"                     -- date-only

some { val := { toUInt64 := 1705276800000 } }

some { val := { toUInt64 := 1705314645123 } }#eval Datetime.parse "2024-01-15T10:30:45.123Z"       -- UTC with milliseconds

some { val := { toUInt64 := 1705314645123 } }

some { val := { toUInt64 := 1705294845000 } }#eval Datetime.parse "2024-01-15T10:30:45+0530"       -- explicit offset

some { val := { toUInt64 := 1705294845000 } }

none#eval Datetime.parse "2024-02-30T00:00:00Z"           -- rejected: no Feb 30

none

none#eval Datetime.parse "2024-01-15T10:30:60Z"           -- rejected: leap second

none

none#eval Datetime.parse "10000-01-01"
-- rejected: format maximum is year 9999

none