a value in [lo, hi] / d less the value of `word` (a positive binary32
below 2^24, exponent field at most 150): the binary32 nearest the
difference, its sign set when the word is the larger; zero when the
interval reaches the word's value (the difference is below its width
116def float32ExactRemainder =
117 (lambda unrestricted lo : Nat .
118 (lambda unrestricted hi : Nat .
119 (lambda unrestricted d : Nat .
120 (lambda unrestricted word : Nat .
121 (let unrestricted shift = (specPow2 (nat-subtract 150 (modelExponent word))) in
122 (let unrestricted value = (nat-multiply (nat-add (modelFraction word) modelPow2Twenty3) d) in
123 (let unrestricted low = (nat-multiply lo shift) in
124 (let unrestricted high = (nat-multiply hi shift) in
125 (let unrestricted scale = (nat-multiply d shift) in
126 (specSelect (nat-less-than value low)
127 (float32ExactBetween (nat-subtract low value) scale (nat-subtract high value) scale)
128 (specSelect (nat-less-than high value)
129 (nat-add modelPow2Thirty1 (float32ExactBetween (nat-subtract value high) scale (nat-subtract value low) scale))
130 0)))))))))))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.