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