padLeftZeros

formal source

  25
  26def pow10 (d : Nat) : Nat := Nat.pow 10 d
  27
  28def padLeftZeros (s : String) (len : Nat) : String :=
  29  let deficit := if s.length ≥ len then 0 else len - s.length
  30  let rec mkZeros (n : Nat) (acc : String) : String :=
  31    match n with
  32    | 0 => acc
  33    | n+1 => mkZeros n ("0" ++ acc)
  34  mkZeros deficit s
  35
  36/-- Render a rational q = n / m to a fixed d-decimal string. -/
  37def ratToDecimal (n : Int) (m : Nat) (d : Nat) : String :=
  38  let sign := if n < 0 then "-" else ""
  39  let nAbs : Nat := Int.natAbs n
  40  if m = 0 then sign ++ "NaN" else
  41  let scale := pow10 d
  42  let scaled : Nat := (nAbs * scale) / m
  43  let ip : Nat := scaled / scale
  44  let fp : Nat := scaled % scale
  45  let fpStr := padLeftZeros (toString fp) d
  46  sign ++ toString ip ++ (if d = 0 then "" else "." ++ fpStr)
  47
  48end NumFmt
  49
  50private def boolToJson (b : Bool) : String := if b then "true" else "false"
  51
  52private def escape (s : String) : String :=
  53  -- Minimal escaping for JSON content used here
  54  s.replace "\"" "\\\""
  55
  56private def quote (s : String) : String := "\"" ++ escape s ++ "\""
  57
  58private def AuditItem.toJson (i : AuditItem) : String :=