1{-# Language BlockArguments, OverloadedStrings #-} 2{-# Language BangPatterns #-} 3module Cryptol.Backend.FloatHelpers where 4 5import Data.Char (isDigit) 6import Data.Ratio(numerator,denominator) 7import LibBF 8 9import Cryptol.Utils.PP 10import Cryptol.Utils.Panic(panic) 11import Cryptol.Backend.Monad( EvalError(..) ) 12 13 14data BF = BF 15 { bfExpWidth :: !Integer 16 , bfPrecWidth :: !Integer 17 , bfValue :: !BigFloat 18 } 19 20 21-- | Make LibBF options for the given precision and rounding mode. 22fpOpts :: Integer -> Integer -> RoundMode -> BFOpts 23fpOpts e p r = 24 case ok of 25 Just opts -> opts 26 Nothing -> panic "floatOpts" [ "Invalid Float size" 27 , "exponent: " ++ show e 28 , "precision: " ++ show p 29 ] 30 where 31 ok = do eb <- rng expBits expBitsMin expBitsMax e 32 pb <- rng precBits precBitsMin precBitsMax p 33 pure (eb <> pb <> allowSubnormal <> rnd r) 34 35 rng f a b x = if toInteger a <= x && x <= toInteger b 36 then Just (f (fromInteger x)) 37 else Nothing 38 39 40 41-- | Mapping from the rounding modes defined in the `Float.cry` to 42-- the rounding modes of `LibBF`. 43fpRound :: Integer -> Either EvalError RoundMode 44fpRound n = 45 case n of 46 0 -> Right NearEven 47 1 -> Right NearAway 48 2 -> Right ToPosInf 49 3 -> Right ToNegInf 50 4 -> Right ToZero 51 _ -> Left (BadRoundingMode n) 52 53-- | Check that we didn't get an unexpected status. 54fpCheckStatus :: (BigFloat,Status) -> BigFloat 55fpCheckStatus (r,s) = 56 case s of 57 MemError -> panic "checkStatus" [ "libBF: Memory error" ] 58 _ -> r 59 60 61-- | Pretty print a float 62fpPP :: PPOpts -> BF -> Doc 63fpPP opts bf = 64 case bfSign num of 65 Nothing -> "fpNaN" 66 Just s 67 | bfIsFinite num -> text hacStr 68 | otherwise -> 69 case s of 70 Pos -> "fpPosInf" 71 Neg -> "fpNegInf" 72 where 73 num = bfValue bf 74 precW = bfPrecWidth bf 75 76 base = useFPBase opts 77 78 withExp :: PPFloatExp -> ShowFmt -> ShowFmt 79 withExp e f = case e of 80 AutoExponent -> f 81 ForceExponent -> f <> forceExp 82 83 str = bfToString base fmt num 84 fmt = addPrefix <> showRnd NearEven <> 85 case useFPFormat opts of 86 FloatFree e -> withExp e $ showFree 87 $ Just $ fromInteger precW 88 FloatFixed n e -> withExp e $ showFixed $ fromIntegral n 89 FloatFrac n -> showFrac $ fromIntegral n 90 91 -- non-base 10 literals are not overloaded so we add an explicit 92 -- .0 if one is not present. Moreover, we trim any extra zeros 93 -- that appear in a decimal representation. 94 hacStr 95 | base == 10 = trimZeros 96 | elem '.' str = str 97 | otherwise = case break (== 'p') str of 98 (xs,ys) -> xs ++ ".0" ++ ys 99 100 trimZeros = 101 case break (== '.') str of 102 (xs,'.':ys) -> 103 case break (not . isDigit) ys of 104 (frac, suffix) -> xs ++ '.' : processFraction frac ++ suffix 105 _ -> str 106 107 processFraction frac = 108 case dropWhile (== '0') (reverse frac) of 109 [] -> "0" 110 zs -> reverse zs 111 112-- | Make a literal 113fpLit :: 114 Integer {- ^ Exponent width -} -> 115 Integer {- ^ Precision width -} -> 116 Rational -> 117 BF 118fpLit e p rat = floatFromRational e p NearEven rat 119 120-- | Make a floating point number from a rational, using the given rounding mode 121floatFromRational :: Integer -> Integer -> RoundMode -> Rational -> BF 122floatFromRational e p r rat = 123 BF { bfExpWidth = e 124 , bfPrecWidth = p 125 , bfValue = fpCheckStatus 126 if den == 1 then bfRoundFloat opts num 127 else bfDiv opts num (bfFromInteger den) 128 } 129 where 130 opts = fpOpts e p r 131 132 num = bfFromInteger (numerator rat) 133 den = denominator rat 134 135 136-- | Convert a floating point number to a rational, if possible. 137floatToRational :: String -> BF -> Either EvalError Rational 138floatToRational fun bf = 139 case bfToRep (bfValue bf) of 140 BFNaN -> Left (BadValue fun) 141 BFRep s num -> 142 case num of 143 Inf -> Left (BadValue fun) 144 Zero -> Right 0 145 Num i ev -> Right case s of 146 Pos -> ab 147 Neg -> negate ab 148 where ab = fromInteger i * (2 ^^ ev) 149 150 151-- | Convert a floating point number to an integer, if possible. 152floatToInteger :: String -> RoundMode -> BF -> Either EvalError Integer 153floatToInteger fun r fp = 154 do rat <- floatToRational fun fp 155 pure case r of 156 NearEven -> round rat 157 NearAway -> if rat > 0 then ceiling rat else floor rat 158 ToPosInf -> ceiling rat 159 ToNegInf -> floor rat 160 ToZero -> truncate rat 161 _ -> panic "fpCvtToInteger" 162 ["Unexpected rounding mode", show r] 163 164 165floatFromBits :: 166 Integer {- ^ Exponent width -} -> 167 Integer {- ^ Precision widht -} -> 168 Integer {- ^ Raw bits -} -> 169 BF 170floatFromBits e p bv = BF { bfValue = bfFromBits (fpOpts e p NearEven) bv 171 , bfExpWidth = e, bfPrecWidth = p } 172 173 174-- | Turn a float into raw bits. 175-- @NaN@ is represented as a positive "quiet" @NaN@ 176-- (most significant bit in the significand is set, the rest of it is 0) 177floatToBits :: Integer -> Integer -> BigFloat -> Integer 178floatToBits e p bf = bfToBits (fpOpts e p NearEven) bf 179