Skip to content

Instantly share code, notes, and snippets.

@LeventErkok
Last active February 28, 2019 07:21
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save LeventErkok/fdc8880fe8b726362c0feba15018be36 to your computer and use it in GitHub Desktop.
Save LeventErkok/fdc8880fe8b726362c0feba15018be36 to your computer and use it in GitHub Desktop.
Dumping bounds
{-# 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]"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment