    "The string decimal representation of the given
     [[floating point number|float]]. If the given number is
     [[negative|Float.negative]], the string representation will
     begin with `-`. The [[whole part|Float.wholePart]] and
     [[fractional parts|Float.fractionalPart]] of the number are
     separated by a `.` decimal point. Digits consist of decimal
     digits `0` to `9`.

     The number of decimal places following the decimal point is
     controlled by the parameters [[minDecimalPlaces]] and
     [[maxDecimalPlaces]], which default to `1` and `9`
     respectively, so that by default the string representation
     always contains a decimal point, and never contains more
     than nine decimal places. The decimal representation is
     truncated so that the number of decimal places never
     exceeds the specified maximum.

     For example:

     - `formatFloat(1234.1234)` is `\"1234.1234\"`
     - `formatFloat(0.1234)` is `\"0.1234\"`
     - `formatFloat(1234.0)` is `\"1234.0\"`
     - `formatFloat(1234.0,0)` is `\"1234\"`
     - `formatFloat(1234.1234,6)` is `\"1234.123400\"`
     - `formatFloat(1234.1234,0,2)` is `\"1234.12\"`
     - `formatFloat(0.0001,2,2)` is `\"0.00\"`
     - `formatFloat(0.0001,0,2)` is `\"0\"`

     Finally:

     - `formatFloat(-0.0)` is `\"0.0\"`,
     - `formatFloat(0.0/0)` is `\"NaN\"`,
     - `formatFloat(1.0/0)` is `\"Infinity\"`, and
     - `formatFloat(-1.0/0)` is `\"-Infinity\".`

     This function never produces a representation involving
     scientific notation."
    tagged("Numbers")
    see (`function formatInteger`,
         `function parseFloat`)
    shared String formatFloat(
            "The floating point value to format."
            Float float,
            "The minimum number of allowed decimal places.

             If `minDecimalPlaces<=0`, the result may have no
             decimal point."
            Integer minDecimalPlaces=1,
            "The maximum number of allowed decimal places.

             If `maxDecimalPlaces<=0`, the result always has no
             decimal point."
            Integer maxDecimalPlaces=9) {
        if (float.undefined || float.infinite) {
            return float.string;
        }
        variable {Character*} digits = {};
        variable Integer i = maxDecimalPlaces;
        Float m = float.magnitude;
        while (true) {
            Float f = m * 10.0.powerOfInteger(--i); //really slow for large i
            Float d = (f.fractionalPart * 10).wholePart;
            Character c = (d.integer+zeroInt).character;
            digits = digits.follow(c);
            if (f.wholePart==0.0) {
                break;
            }
        }
        String string = String(digits);
        Integer point = string.size - maxDecimalPlaces;
        String wholePart;
        String fractionalPart;
        if (point>0) {
            wholePart = string[0:point];
            fractionalPart = string[point...];
        }
        else {
            wholePart = "0";
            fractionalPart
                    = string.padLeading(maxDecimalPlaces, '0');
        }

        String normalized =
                fractionalPart
                    .trimTrailing('0'.equals)
                    .padTrailing(minDecimalPlaces, '0');
        String signed =
                float.negative
                    then "-" + wholePart
                    else wholePart;
        return normalized.empty
                then signed
                else signed + "." + normalized;
    }