fact: Definition exp (prec : F.precision) xi := let aux x := let k0 := (x * InvLog2_64 + 0x1.8p52)%float in let kf := (k0 - 0x1.8p52)%float in let tf := (x - kf * Log2div64h - kf * Log2div64l)%float in let ki := PrimInt63.sub (normfr_mantissa (fst (frshiftexp k0))) 6755399440921280%int63 in let C := consts.[PrimInt63.land ki 63] in let kq := PrimInt63.asr ki 6 in let y := (C * Papprox tf)%float in (C, y, kq) in match xi with | Ibnd xl xu => Ibnd (if F.real xl then if PrimFloat.ltb xl (-0x1.74385446d71c4p9)%float then 0%float else if PrimFloat.ltb 0x1.62e42fefa39efp9%float xl then 0x1.fffffffffff2ap1023%float else let '(C, y, kq) := aux xl in next_down (ldshiftexp (C + (y + -0x1.8p-57))%float kq) else 0%float) (if F.real xu then if PrimFloat.ltb xu (-0x1.74385446d71c4p9)%float then 0x1p-1074%float else if PrimFloat.ltb 0x1.62e42fefa39efp9%float xu then infinity else let '(C, y, kq) := aux xu in next_up (ldshiftexp (C + (y + 0x1.8p-57))%float kq) else nan) | Inan => Inan end.
imports: Coq(Reals Psatz PrimInt63 Uint63 Sint63 PArray Floats) Flocq(Core PrimFloat BinarySingleNaN) Missing.Flocq Xreal Basic Sig Interval Float Float_full Specific_bigint Specific_ops Primitive_ops Lang_expr Lang_tac Interval_helper