AlphaGitHub
Source/Reference

Float32Model

reference/numeric/Float32Model.alpha

304 lines61 declarations17.2 KiBSHA-256 421f33839d13
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 136–148

modelF32FusedMultiplyAdd

Full file
136def modelF32FusedMultiplyAdd =
137  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat . (lambda unrestricted c : Nat .
138    (specSelect (modelOr (modelIsNaN a) (modelOr (modelIsNaN b) (modelIsNaN c)))
139      (specSelect (modelIsNaN a) (modelQuiet a) (specSelect (modelIsNaN b) (modelQuiet b) (modelQuiet c)))
140      (specSelect (modelOr (modelAnd (modelIsInfinite a) (modelIsZero b)) (modelAnd (modelIsZero a) (modelIsInfinite b)))
141        modelDefaultNaN
142        (specSelect (modelOr (modelIsInfinite a) (modelIsInfinite b))
143          (specSelect (modelAnd (modelIsInfinite c) (specNot (specEqual (modelXor (modelSign a) (modelSign b)) (modelSign c))))
144            modelDefaultNaN
145            (modelInfinityOf (modelXor (modelSign a) (modelSign b))))
146          (specSelect (modelIsInfinite c)
147            c
148            (modelFusedFinite a b c))))))))

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.