Std.Float

F64 construction / projection NUM-005 integer <-> binary32 conversions. Every conversion is a named function; rounding is to nearest, ties to even (IEEE-754 roundTiesToEven); a float that is NaN or infinite, or whose rounded value does not fit, has no integer (StdNone). The arithmetic is on naturals, over the existing bit owners (the F32's Word32 and the I32's Word32), so there is no second representation of either. A natural's low 32 bits as a Word32, by compile-time division (nat-divide / nat-modulo fold on closed naturals in one step). Model.Word32's modelWord32FromNaturalTruncated is the runtime owner and counts through the value, which a 2^30-sized float bit pattern cannot afford; these conversions are compile-time arithmetic throughout, so they take this form.

173def stdFloatWord32OfNatural =
174  (lambda unrestricted value : Nat .
175    (constructor
176      ModelWord32
177      ModelWord32Value
178      (nat-to-byte (nat-modulo value 256))
179      (nat-to-byte (nat-modulo (nat-divide value 256) 256))
180      (nat-to-byte (nat-modulo (nat-divide value 65536) 256))
181      (nat-to-byte (nat-modulo (nat-divide value 16777216) 256))))