3.5. Canonical String Representation🔗

Datetime stores an arbitrary Int64 millisecond value, but the grammar only spells years 0000–9999, so — unlike the decimal and duration toString, which are total — datetime serialization is partial. toString? returns none for any value outside the representable interval and otherwise emits the most explicit grammar form, YYYY-MM-DDTHH:mm:ss.SSS±HHMM, always normalizing the instant to a +0000 UTC offset:

def

Cedar.Thm.Datetime.toString? (d : Datetime) : Option String
Cedar.Thm.Datetime.toString?
  (d : Datetime) : Option String

Canonical partial serializer for datetime values. Every successful result has the fixed form YYYY-MM-DDTHH:mm:ss.SSS±HHMM.

For example, every representable instant renders with an explicit millisecond field and a UTC offset; a parsed +0530 offset comes back as the equivalent UTC time:

some "2024-01-15T05:00:45.000+0000"#eval (Datetime.parse "2024-01-15T10:30:45+0530").bind toString?

some "2024-01-15T05:00:45.000+0000"

Values beyond the representable interval have no literal (the datetime.offset(duration) operator can reach them, as noted in the Grammar section), so they do not serialize:

theorem

Cedar.Thm.Datetime.toString?_eq_none_of_not_representable (d : Datetime)
  (h :
    d.val.toInt < MIN_REPRESENTABLE_MILLIS ∨
      MAX_REPRESENTABLE_MILLIS < d.val.toInt) :
  toString? d = none
Cedar.Thm.Datetime.toString?_eq_none_of_not_representable
  (d : Datetime)
  (h :
    d.val.toInt <
        MIN_REPRESENTABLE_MILLIS ∨
      MAX_REPRESENTABLE_MILLIS <
        d.val.toInt) :
  toString? d = none

Values outside the exact grammar-representable millisecond interval do not serialize: the canonical local-time selection returns none, so toString? short-circuits.

normalize composes parsing and serialization — it accepts any valid string and returns its canonical form. Because serialization is partial, the re-serialization is a bind rather than the total map used for decimal and duration:

def

Cedar.Thm.Datetime.normalize (str : String) : Option String
Cedar.Thm.Datetime.normalize
  (str : String) : Option String

Canonical-form normalizer: parse the string and re-serialize. Returns none for malformed inputs (mirror of the decimal and duration normalizers); because serialization is partial the re-serialization is a bind rather than the total map used there.

Serialization is injective on the values it covers: two datetimes with the same (defined) canonical string are equal.

theorem

Cedar.Thm.Datetime.toString?_injective {d d' : Datetime} {str : String}
  (h : toString? d = some str) (h' : toString? d' = some str) : d = d'
Cedar.Thm.Datetime.toString?_injective
  {d d' : Datetime} {str : String}
  (h : toString? d = some str)
  (h' : toString? d' = some str) : d = d'

toString? is injective on the values it serializes: datetimes with the same (defined) canonical string are equal. (Partial-serializer analogue of Decimal/Duration's toString_injective.)

Normalization therefore decides datetime equality, up to the partiality of serialization. The forward direction carries a serializability hypothesis on the parsed values: without it, two distinct parseable-but-unrepresentable instants would both normalize to none while their parses differ. A full serialization-completeness result (parse s = some d → (toString? d).isSome, needing the Std.Time civil-calendar round-trip) would discharge it and recover the unconditional decimal/duration form; the backward direction already holds unconditionally.

theorem

Cedar.Thm.Datetime.normalize_eq_iff_parse_eq (s s' : String)
  (hs :
    ∀ (d : Datetime),
      Datetime.parse s = some d → (toString? d).isSome = true)
  (hs' :
    ∀ (d : Datetime),
      Datetime.parse s' = some d → (toString? d).isSome = true) :
  normalize s = normalize s' ↔ Datetime.parse s = Datetime.parse s'
Cedar.Thm.Datetime.normalize_eq_iff_parse_eq
  (s s' : String)
  (hs :
    ∀ (d : Datetime),
      Datetime.parse s = some d →
        (toString? d).isSome = true)
  (hs' :
    ∀ (d : Datetime),
      Datetime.parse s' = some d →
        (toString? d).isSome = true) :
  normalize s = normalize s' ↔
    Datetime.parse s = Datetime.parse s'

Equal normal form iff equal parse — normalization decides datetime equality.

Datetime serialization is partial (toString?), so normalize = (parse ·).bind toString? can collapse two distinct parseable-but-unserializable values to the shared none. The forward direction therefore carries a serializability hypothesis on the parsed values; this is exactly what a full serialization-completeness result (parse s = some d → (toString? d).isSome, which needs the Std.Time civil-calendar round-trip) would discharge unconditionally, closing the gap with Decimal/Duration's total-toString versions. The backward direction is unconditional.