Conversion rounds the exact source rational once. Its scan bound comes from
the SOURCE width: using the destination's binary32 bound for a binary64
numerator silently loses large exponents. NaN payload mapping is a reference
policy; finite device conversion must be qualified separately on silicon.
441def binaryFloatConvert =
442 (lambda unrestricted source : (family BinaryFloatFormat) .
443 (lambda unrestricted destination : (family BinaryFloatFormat) .
444 (lambda unrestricted bits : Nat .
445 (let unrestricted sign =
446 (binaryFloatSign source bits)
447 in
448 (specSelect
449 (binaryFloatIsNaN source bits)
450 (binaryFloatQuiet
451 destination
452 (nat-add
453 (binaryFloatInfinityOf destination sign)
454 (nat-divide
455 (nat-multiply
456 (binaryFloatFraction source bits)
457 (binaryFloatFractionBase destination))
458 (binaryFloatFractionBase source))))
459 (specSelect
460 (binaryFloatIsInfinite source bits)
461 (binaryFloatInfinityOf destination sign)
462 (binaryFloatRoundBitsWithLimit
463 (binaryFloatRoundingChunks source)
464 destination
465 sign
466 (binaryFloatScaledMagnitude source bits)
467 (binaryFloatDenominator source))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.