Float32Model

fused multiply-add a x b + c with ONE rounding, as SM86's FFMA performs it: the exact product (scale 2^300) and the exact addend (scale 2^150, raised to 2^300) are summed as signed exact magnitudes and rounded once. Special values: any NaN operand quiets; inf x 0 is invalid; an infinite product or addend with a finite partner gives that infinity; opposite infinities are invalid. A zero exact sum carries the sign the sum rule gives (+0 unless both are negative zero).

123def modelFusedFinite =
124  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat .
125    (specSelect (modelAnd (modelOr (modelIsZero a) (modelIsZero b)) (modelIsZero c))
126      (modelZeroOf (modelAnd (modelXor (modelSign a) (modelSign b)) (modelSign c)))
127      (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . Nat)
128        (modelSumSignedValues
129          (constructor ModelSigned ModelSignedOf (modelXor (modelSign a) (modelSign b))
130            (nat-multiply (modelScaledMagnitude a) (modelScaledMagnitude b)))
131          (modelSignedScale
132            (constructor ModelSigned ModelSignedOf (modelSign c) (modelScaledMagnitude c))
133            modelPow2Hundred50))
134        (branch ModelSignedOf sign magnitude . (modelRoundBits sign magnitude modelPow2Three00)))))))