2.5. Canonical String Representation🔗

Duration.toString converts a duration back to a canonical string, maximizing units and printing all five components largest-to-smallest (including zero-valued ones), with a leading '-' for negative values:

public def Duration.toString (d : Duration) : String :=
  let neg := d.val < 0
  let totalMs := d.val.toInt.natAbs
  let days := totalMs / MILLISECONDS_PER_DAY.toNat
  let rem := totalMs % MILLISECONDS_PER_DAY.toNat
  let hours := rem / MILLISECONDS_PER_HOUR.toNat
  let rem := rem % MILLISECONDS_PER_HOUR.toNat
  let minutes := rem / MILLISECONDS_PER_MINUTE.toNat
  let rem := rem % MILLISECONDS_PER_MINUTE.toNat
  let seconds := rem / MILLISECONDS_PER_SECOND.toNat
  let ms := rem % MILLISECONDS_PER_SECOND.toNat
  let body := durationComponent days "d" ++ durationComponent hours "h" ++
    durationComponent minutes "m" ++ durationComponent seconds "s" ++
    durationComponent ms "ms"
  if neg then "-" ++ body else body

For example, the canonical string representation of a duration with internal value 93784005 (one day, two hours, three minutes, four seconds, five milliseconds) is 1d2h3m4s5ms:

"1d2h3m4s5ms"#eval Duration.toString (⟨93784005⟩ : Duration)

"1d2h3m4s5ms"

normalize composes parsing and serialization — it accepts any valid string and returns its canonical form:

def

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

Canonical-form normalizer: parse the string and re-serialize. Returns none for malformed or out-of-range inputs.

theorem

Cedar.Thm.Duration.toString_injective
  (d d' : Cedar.Spec.Ext.Datetime.Duration)
  (h : d.toString = d'.toString) : d = d'
Cedar.Thm.Duration.toString_injective
  (d d' :
    Cedar.Spec.Ext.Datetime.Duration)
  (h : d.toString = d'.toString) : d = d'

toString is injective: distinct durations produce distinct strings.

theorem

Cedar.Thm.Duration.normalize_eq_iff_parse_eq (s s' : String) :
  normalize s = normalize s' ↔
    Cedar.Spec.Ext.Datetime.Duration.parse s =
      Cedar.Spec.Ext.Datetime.Duration.parse s'
Cedar.Thm.Duration.normalize_eq_iff_parse_eq
  (s s' : String) :
  normalize s = normalize s' ↔
    Cedar.Spec.Ext.Datetime.Duration.parse
        s =
      Cedar.Spec.Ext.Datetime.Duration.parse
        s'

Equal normal form iff equal value: normalization decides duration equality.