1.5. Canonical String Representation🔗

toString converts a decimal back to its canonical string form, always producing exactly 4 fractional digits:

public instance : ToString Decimal where
  toString (d : Decimal) : String :=
    let neg   := if d < 0 then "-" else ""
    let d     := d.natAbs
    let left  := d / (Nat.pow 10 DECIMAL_DIGITS)
    let right := d % (Nat.pow 10 DECIMAL_DIGITS)
    let right :=
      -- this is not generalized for arbitrary DECIMAL_DIGITS
      if right < 10 then s!".000{right}"
      else if right < 100 then s!".00{right}"
      else if right < 1000 then s!".0{right}"
      else s!".{right}"
    s!"{neg}{left}{right}"

For example, the canonical string representation of a decimal with internal value 12000 is 1.2000:

"1.2000"#eval toString (⟨12000⟩ : Decimal)

"1.2000"

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

def

Cedar.Thm.Decimal.normalize (s : String) : Option String
Cedar.Thm.Decimal.normalize (s : String) :
  Option String

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

theorem

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

toString is injective: distinct decimals produce distinct strings.

theorem

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

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