Additions for JSON

[robin-aws]

Care of @ajewellamz, some suggestions for useful utilities when working with the JSON library:

  function DecimalToNat(num: Decimal) : Result<nat, string>
  {
    :- Need(num.n >= 0, "Number must be > 0");
    if num.n == 0 then
      Success(0)
    else
      :- Need(num.e10 >= 0, "Number must be a whole number");
      :- Need(num.e10 < 100, "Number must be less than a googol");
      Success(GetPower(num.n, num.e10))
  }

  function DecimalToInt(num: Decimal) : Result<int, string>
  {
    if num.n == 0 then
      Success(0)
    else
      :- Need(num.e10 >= 0, "Number must be a whole number");
      :- Need(num.e10 < 100, "Number must be less than a googol");
      Success(GetPower(num.n, num.e10))
  }

  function DecimalToStr(num: Decimal) : Result<string, string>
  {
    if num.n == 0 then
      Success("0")
    else
      :- Need(-1000 < num.e10 < 1000, "Exponent must be between -1000 and 1000");
      var str := String.Base10Int2String(num.n);
      if num.e10 >= 0 then
        Success(str + Zeros(num.e10))
      else if -num.e10 < |str| then
        var pos := |str| + num.e10;
        Success(str[..pos] + "." + str[pos..])
      else
        Success("0." + Zeros(|str| - num.e10) + str)
  }

  // Return a string of this many zeros
  function Zeros(n : nat) : (ret : string)
  {
    seq(n, i => '0')
  }

  // return n x 10^pow
  function GetPower(n : nat, pow : nat) : nat
  {
    if pow == 0 then
      n
    else
      10 * GetPower(n, pow-1)
  }