module Data.SBV.BitVectors.PrettyNum (
PrettyNum(..), readBin, shex, shexI, sbin, sbinI
, showCFloat, showCDouble, showHFloat, showHDouble
, showSMTFloat, showSMTDouble, smtRoundingMode
) where
import Data.Char (ord)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.List (isPrefixOf)
import Data.Maybe (fromJust)
import Data.Ratio (numerator, denominator)
import Data.Word (Word8, Word16, Word32, Word64)
import Numeric (showIntAtBase, showHex, readInt)
import Data.SBV.BitVectors.Data
import Data.SBV.BitVectors.Model ()
class PrettyNum a where
hexS :: a -> String
binS :: a -> String
hex :: a -> String
bin :: a -> String
instance PrettyNum Bool where
{hexS = show; binS = show; hex = show; bin = show}
instance PrettyNum Word8 where
{hexS = shex True True (False,8) ; binS = sbin True True (False,8) ; hex = shex False False (False,8) ; bin = sbin False False (False,8) ;}
instance PrettyNum Int8 where
{hexS = shex True True (True,8) ; binS = sbin True True (True,8) ; hex = shex False False (True,8) ; bin = sbin False False (True,8) ;}
instance PrettyNum Word16 where
{hexS = shex True True (False,16); binS = sbin True True (False,16); hex = shex False False (False,16); bin = sbin False False (False,16);}
instance PrettyNum Int16 where
{hexS = shex True True (True,16); binS = sbin True True (True,16) ; hex = shex False False (True,16); bin = sbin False False (True,16) ;}
instance PrettyNum Word32 where
{hexS = shex True True (False,32); binS = sbin True True (False,32); hex = shex False False (False,32); bin = sbin False False (False,32);}
instance PrettyNum Int32 where
{hexS = shex True True (True,32); binS = sbin True True (True,32) ; hex = shex False False (True,32); bin = sbin False False (True,32) ;}
instance PrettyNum Word64 where
{hexS = shex True True (False,64); binS = sbin True True (False,64); hex = shex False False (False,64); bin = sbin False False (False,64);}
instance PrettyNum Int64 where
{hexS = shex True True (True,64); binS = sbin True True (True,64) ; hex = shex False False (True,64); bin = sbin False False (True,64) ;}
instance PrettyNum Integer where
{hexS = shexI True True; binS = sbinI True True; hex = shexI False False; bin = sbinI False False;}
instance PrettyNum CW where
hexS cw | cwIsBit cw = hexS (cwToBool cw)
| isReal cw = let CWAlgReal w = cwVal cw in show w
| not (isBounded cw) = let CWInteger w = cwVal cw in shexI True True w
| isUninterpreted cw = show cw
| True = let CWInteger w = cwVal cw in shex True True (hasSign cw, intSizeOf cw) w
binS cw | cwIsBit cw = binS (cwToBool cw)
| isReal cw = let CWAlgReal w = cwVal cw in show w
| not (isBounded cw) = let CWInteger w = cwVal cw in sbinI True True w
| isUninterpreted cw = show cw
| True = let CWInteger w = cwVal cw in sbin True True (hasSign cw, intSizeOf cw) w
hex cw | cwIsBit cw = hexS (cwToBool cw)
| isReal cw = let CWAlgReal w = cwVal cw in show w
| not (isBounded cw) = let CWInteger w = cwVal cw in shexI False False w
| isUninterpreted cw = show cw
| True = let CWInteger w = cwVal cw in shex False False (hasSign cw, intSizeOf cw) w
bin cw | cwIsBit cw = binS (cwToBool cw)
| isReal cw = let CWAlgReal w = cwVal cw in show w
| not (isBounded cw) = let CWInteger w = cwVal cw in sbinI False False w
| isUninterpreted cw = show cw
| True = let CWInteger w = cwVal cw in sbin False False (hasSign cw, intSizeOf cw) w
instance (SymWord a, PrettyNum a) => PrettyNum (SBV a) where
hexS s = maybe (show s) (hexS :: a -> String) $ unliteral s
binS s = maybe (show s) (binS :: a -> String) $ unliteral s
hex s = maybe (show s) (hex :: a -> String) $ unliteral s
bin s = maybe (show s) (bin :: a -> String) $ unliteral s
shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
shex shType shPre (signed, size) a
| a < 0
= "-" ++ pre ++ pad l (s16 (abs (fromIntegral a :: Integer))) ++ t
| True
= pre ++ pad l (s16 a) ++ t
where t | shType = " :: " ++ (if signed then "Int" else "Word") ++ show size
| True = ""
pre | shPre = "0x"
| True = ""
l = (size + 3) `div` 4
shexI :: Bool -> Bool -> Integer -> String
shexI shType shPre a
| a < 0
= "-" ++ pre ++ s16 (abs a) ++ t
| True
= pre ++ s16 a ++ t
where t | shType = " :: Integer"
| True = ""
pre | shPre = "0x"
| True = ""
sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
sbin shType shPre (signed,size) a
| a < 0
= "-" ++ pre ++ pad size (s2 (abs (fromIntegral a :: Integer))) ++ t
| True
= pre ++ pad size (s2 a) ++ t
where t | shType = " :: " ++ (if signed then "Int" else "Word") ++ show size
| True = ""
pre | shPre = "0b"
| True = ""
sbinI :: Bool -> Bool -> Integer -> String
sbinI shType shPre a
| a < 0
= "-" ++ pre ++ s2 (abs a) ++ t
| True
= pre ++ s2 a ++ t
where t | shType = " :: Integer"
| True = ""
pre | shPre = "0b"
| True = ""
pad :: Int -> String -> String
pad l s = replicate (l length s) '0' ++ s
s2 :: (Show a, Integral a) => a -> String
s2 v = showIntAtBase 2 dig v "" where dig = fromJust . flip lookup [(0, '0'), (1, '1')]
s16 :: (Show a, Integral a) => a -> String
s16 v = showHex v ""
readBin :: Num a => String -> a
readBin ('-':s) = (readBin s)
readBin s = case readInt 2 isDigit cvt s' of
[(a, "")] -> a
_ -> error $ "SBV.readBin: Cannot read a binary number from: " ++ show s
where cvt c = ord c ord '0'
isDigit = (`elem` "01")
s' | "0b" `isPrefixOf` s = drop 2 s
| True = s
showCFloat :: Float -> String
showCFloat f
| isNaN f = "((float) NAN)"
| isInfinite f, f < 0 = "((float) (-INFINITY))"
| isInfinite f = "((float) INFINITY)"
| True = show f ++ "F"
showCDouble :: Double -> String
showCDouble f
| isNaN f = "((double) NAN)"
| isInfinite f, f < 0 = "((double) (-INFINITY))"
| isInfinite f = "((double) INFINITY)"
| True = show f
showHFloat :: Float -> String
showHFloat f
| isNaN f = "((0/0) :: Float)"
| isInfinite f, f < 0 = "((-1/0) :: Float)"
| isInfinite f = "((1/0) :: Float)"
| True = show f
showHDouble :: Double -> String
showHDouble d
| isNaN d = "((0/0) :: Double)"
| isInfinite d, d < 0 = "((-1/0) :: Double)"
| isInfinite d = "((1/0) :: Double)"
| True = show d
showSMTFloat :: RoundingMode -> Float -> String
showSMTFloat rm f
| isNaN f = as "NaN"
| isInfinite f, f < 0 = as "minusInfinity"
| isInfinite f = as "plusInfinity"
| isNegativeZero f = "(- ((_ asFloat 8 24) " ++ smtRoundingMode rm ++ " (/ 0 1)))"
| True = "((_ asFloat 8 24) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational f) ++ ")"
where as s = "(as " ++ s ++ " (_ FP 8 24))"
showSMTDouble :: RoundingMode -> Double -> String
showSMTDouble rm d
| isNaN d = as "NaN"
| isInfinite d, d < 0 = as "minusInfinity"
| isInfinite d = as "plusInfinity"
| isNegativeZero d = "(- ((_ asFloat 11 53) " ++ smtRoundingMode rm ++ " (/ 0 1)))"
| True = "((_ asFloat 11 53) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational d) ++ ")"
where as s = "(as " ++ s ++ " (_ FP 11 53))"
toSMTLibRational :: Rational -> String
toSMTLibRational r
| n < 0
= "(- (/ " ++ show (abs n) ++ " " ++ show d ++ "))"
| True
= "(/ " ++ show n ++ " " ++ show d ++ ")"
where n = numerator r
d = denominator r
smtRoundingMode :: RoundingMode -> String
smtRoundingMode RoundNearestTiesToEven = "roundNearestTiesToEven"
smtRoundingMode RoundNearestTiesToAway = "roundNearestTiesToAway"
smtRoundingMode RoundTowardPositive = "roundTowardPositive"
smtRoundingMode RoundTowardNegative = "roundTowardNegative"
smtRoundingMode RoundTowardZero = "roundTowardZero"