Dumping bounds

DumpBounds.hs

{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

import Data.SBV
import Data.Proxy
import Numeric
import Data.List

findBounds :: forall a b. (IEEEFloating a, Integral b, SymVal a, SymVal b, Metric (SBV b))
    => SRoundingMode -> Proxy a -> Proxy b -> IO (a, a)
findBounds rm pa pb = (,) <$> opt minimize <*> opt maximize
  where opt minmax = do o <- optimize Lexicographic $ do
                                x :: SBV a <- free "x"
                                z :: SBV b <- free "z"

                                minmax "z" z

                                constrain $ sFromIntegral z .== fpRoundToIntegral rm x

                        case o of
                          LexicographicResult m -> case getModelValue "x" m of
                                                     Just x  -> return x
                                                     Nothing -> error "Can't find x"
                          _ -> error "Didn't expect this!"

getBounds :: forall b. (Integral b, SymVal b, Metric (SBV b)) => Proxy b -> RoundingMode -> IO String
getBounds b m = do (lf, uf) <- findBounds (literal m) (Proxy @Float)  b
                   (ld, ud) <- findBounds (literal m) (Proxy @Double) b
                   let s =    "("  ++ sh (kindOf b)
                           ++ ", " ++ pad 22 (show m)
                           ++ ", " ++ "(" ++ pad l1 (showHFloat lf "") ++ ", " ++ pad l2 (showHFloat uf "") ++ ")"
                           ++ ", " ++ "(" ++ pad l3 (showHFloat ld "") ++ ", " ++ pad l4 (showHFloat ud "") ++ ")"
                           ++ ")"
                   return s
  where sh (KBounded b sz) = "KBounded " ++ shB b ++ " " ++ shSz sz
        sh _               = error "needs bounded kind"
        shB True  = "True "
        shB False = "False"
        shSz 8    = "8 "
        shSz i    = show i
        pad n s   = s ++ replicate (n - length s) ' '
        l1 = 15
        l2 = 13
        l3 = 23
        l4 = 21

getAllModes :: forall b. (Integral b, SymVal b, Metric (SBV b)) => Proxy b -> IO [String]
getAllModes b = mapM (getBounds b) [minBound .. maxBound]

main :: IO ()
main = do l1 <- getAllModes $ Proxy @Word8
          l2 <- getAllModes $ Proxy @Word16
          l3 <- getAllModes $ Proxy @Word32
          l4 <- getAllModes $ Proxy @Word64
          l5 <- getAllModes $ Proxy @Int8
          l6 <- getAllModes $ Proxy @Int16
          l7 <- getAllModes $ Proxy @Int32
          l8 <- getAllModes $ Proxy @Int64
          let ls = concat [l1, l2, l3, l4, l5, l6, l7, l8]
          putStrLn $ "[ " ++ intercalate ("\n, ") ls ++ "\n]"