A binary32 as an I32, rounded to nearest (ties to even); NaN, the infinities
and any value whose rounding lies outside [-2^31, 2^31) have none.
295def stdF32ToI32Checked :
296 (pi unrestricted value : (family InferenceFloat32) . (family StdOption (family StdI32))) =
297 (lambda unrestricted value : (family InferenceFloat32) .
298 (app
299 (lambda unrestricted bits : Nat .
300 (app
301 (lambda unrestricted biased : Nat .
302 (app
303 (lambda unrestricted negative : Nat .
304 (nat-eliminate
305 (lambda unrestricted current : Nat . (family StdOption (family StdI32)))
306 (app
307 (lambda unrestricted magnitude : Nat .
308 (nat-eliminate
309 (lambda unrestricted current : Nat . (family StdOption (family StdI32)))
310 (nat-eliminate
311 (lambda unrestricted current : Nat . (family StdOption (family StdI32)))
312 (constructor StdOption StdNone (family StdI32))
313 (lambda unrestricted fitsPredecessor : Nat .
314 (lambda unrestricted fitsInduction : (family StdOption (family StdI32)) .
315 (constructor
316 StdOption
317 StdSome
318 (family StdI32)
319 (stdI32FromWord (stdFloatWord32OfNatural magnitude)))))
320 (nat-less-than magnitude 2147483648))
321 (lambda unrestricted negativePredecessor : Nat .
322 (lambda unrestricted negativeInduction : (family StdOption (family StdI32)) .
323 (nat-eliminate
324 (lambda unrestricted current : Nat .
325 (family StdOption (family StdI32)))
326 (constructor StdOption StdNone (family StdI32))
327 (lambda unrestricted fitsPredecessor : Nat .
328 (lambda unrestricted fitsInduction : (family StdOption (family StdI32)) .
329 (constructor
330 StdOption
331 StdSome
332 (family StdI32)
333 (stdI32FromWord
334 (stdFloatWord32OfNatural (nat-subtract 4294967296 magnitude))))))
335 (nat-less-than magnitude 2147483649))))
336 negative))
337 (nat-eliminate
338 (lambda unrestricted current : Nat . Nat)
339 (stdFloatRoundedShift
340 (nat-add (nat-modulo bits 8388608) 8388608)
341 (nat-subtract 150 biased))
342 (lambda unrestricted largePredecessor : Nat .
343 (lambda unrestricted largeInduction : Nat .
344 (nat-multiply
345 (nat-add (nat-modulo bits 8388608) 8388608)
346 (naturalPowerOfTwo (nat-subtract biased 150)))))
347 (naturalIsZero (nat-less-than biased 150))))
348 (lambda unrestricted specialPredecessor : Nat .
349 (lambda unrestricted specialInduction : (family StdOption (family StdI32)) .
350 (constructor StdOption StdNone (family StdI32))))
351 (naturalEqual biased 255)))
352 (naturalIsZero (nat-less-than bits 2147483648))))
353 (nat-modulo (nat-divide bits 8388608) 256)))
354 (modelWord32ToNatural (stdF32ToWord32 value))))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.