String and number conversions

The module CONVERSION consolidates all the conversion functions between the three major built-in data types: Nat/Int/Rat, Float, and String.

  fmod CONVERSION is
    protecting RAT .
    protecting FLOAT .
    protecting STRING .

    *** number type conversions
    op float : Rat -> Float [special (...)] .
    op rat : FiniteFloat -> Rat [special (...)] .

The operation float computes the floating-point number nearest to a given rational number. If the value of the rational number falls outside the range representable by IEEE-754 double precision finite floating-point numbers, Infinity or -Infinity is returned as appropriate. This is in accord with the convention that Infinity and -Infinity are used to handle out-of-range situations in the floating-point world.

The operator rat converts finite floating-point numbers to rational numbers exactly (since every IEEE-754 finite floating-point number is a rational number). Of course, if the result happens to be a natural number or an integer, that is what you get. rat(Infinity) and rat(-Infinity) do not reduce, since they have no reasonable representation in the world of rational numbers. It is intended that the equation

  float(rat(F:FiniteFloat)) = F:FiniteFloat

is satisfied, although this holds only if the third party library (GNU GMP) being used in the implementation meets its related requirements.

    *** string <-> number conversions
    op string : Rat NzNat ~> String [special (...)] .
    op rat : String NzNat ~> Rat [special (...)] .
    op string : Float -> String [special (...)] .
    op float : String ~> Float [special (...)] .

The operator string converts a rational number to a string using a given base, which must lie in the range 2..36. Rational numbers that are really natural numbers or integers are converted to string representations of natural numbers or integers, so we have for example

  Maude> red in CONVERSION : string(-1, 10) .
  result String: "-1"

The operator rat converts a string to a rational number using a given base, which must lie in the range 2..36. Of course, if the result happens to be a natural number or an integer, that is what you get. Currently the function is very strict about which strings are converted: the string must be something that the Maude parser would recognize as a natural number, an integer or a rational number. This could be changed to a more generous interpretation in the future.

The operators string and float for conversion between floating-point numbers and strings satisfy the equation

  float(string(F:Float)) = F:Float

A new sort, DecFloat, is introduced to provide the means for arbitrary formatting of floating-point numbers.

    sort DecFloat .
    op <_,_,_> : Int String Int -> DecFloat [ctor] .
    op decFloat : Float Nat -> DecFloat [special (...)] .
  endfm

A DecFloat consists of a sign (1, 0 or $-1$), a string of digits, and a decimal point position (0 is just in front of first digit, $-n$ is $n$ positions to the left, and $+n$ is $n$ positions to the right). Thus, < -1, "123", 11 > represents -1.23e10. decFloat(F, N) converts F to a DecFloat, rounding to N significant digits using the IEEE-754 ``round to nearest'' rule with trailing zeros if needed. If N is 0, an exact DecFloat representation of F is produced--this may require hundreds of digits. For any natural number N, decFloat(Infinity, N) reduces to < 1, "Infinity", 0 >. Here are some examples.

  Maude> red in CONVERSION : decFloat(Infinity, 9) .
  result DecFloat: < 1,"Infinity",0 >

  Maude> red decFloat(-Infinity, 9) .
  result DecFloat: < -1,"Infinity",0 >

  Maude> red decFloat(123.0, 5) .
  result DecFloat: < 1,"12300",3 >

  Maude> red decFloat(-123.0, 5) .
  result DecFloat: < -1,"12300",3 >

  Maude> red decFloat(.123, 5) .
  result DecFloat: < 1,"12300",0 >

  Maude> red decFloat(.00123, 5) .
  result DecFloat: < 1,"12300",-2 >

  Maude> red decFloat(0.0, 5) .
  result DecFloat: < 0,"00000",0 >

Advisory. Counterintuitive results are possible when converting from the approximate world of floating-point numbers to the exact world of rational numbers. For example,

  Maude> red in CONVERSION : rat(1.1) .
  result PosRat: 2476979795053773/2251799813685248

This is because, as mentioned above, 1.1 cannot be represented exactly as a floating-point number, and the nearest floating-point number is

  1.100000000000000088817841970012523233890533447265625

which is the above rational number. (Note that Maude prints the number 1.1 as 1.1000000000000001, using 17 significant digits. The above representation is obtained by reducing decFloat(1.1, 52).)