-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Utils.PrettyNum
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Number representations in hex/bin
-----------------------------------------------------------------------------

{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns #-}

module Data.SBV.Utils.PrettyNum (
        PrettyNum(..), readBin, shex, chex, shexI, sbin, sbinI
      , showCFloat, showCDouble, showHFloat, showHDouble, showBFloat, showFloatAtBase
      , showSMTFloat, showSMTDouble, smtRoundingMode, cvToSMTLib, mkSkolemZero
      , showNegativeNumber
      ) where

import Data.Bits  ((.&.), countTrailingZeros)
import Data.Char  (intToDigit, ord, chr, toUpper)
import Data.Int   (Int8, Int16, Int32, Int64)
import Data.List  (isPrefixOf)
import Data.Maybe (fromJust, fromMaybe, listToMaybe)
import Data.Ratio (numerator, denominator)
import Data.Word  (Word8, Word16, Word32, Word64)

import qualified Data.Set as Set

import Numeric (showIntAtBase, showHex, readInt, floatToDigits)
import qualified Numeric as N (showHFloat)

import Data.SBV.Core.Data
import Data.SBV.Core.Kind (smtType, smtRoundingMode, showBaseKind)

import Data.SBV.Core.AlgReals    (algRealToSMTLib2)
import Data.SBV.Core.SizedFloats (fprToSMTLib2, bfToString)

import Data.SBV.Utils.Lib (stringToQFS)

-- | PrettyNum class captures printing of numbers in hex and binary formats; also supporting negative numbers.
class PrettyNum a where
  -- | Show a number in hexadecimal, starting with @0x@ and type.
  hexS :: a -> String
  -- | Show a number in binary, starting with @0b@ and type.
  binS :: a -> String
  -- | Show a number in hexadecimal, starting with @0x@ but no type.
  hexP :: a -> String
  -- | Show a number in binary, starting with @0b@ but no type.
  binP :: a -> String
  -- | Show a number in hex, without prefix, or types.
  hex :: a -> String
  -- | Show a number in bin, without prefix, or types.
  bin :: a -> String

-- Why not default methods? Because defaults need "Integral a" but Bool is not..
instance PrettyNum Bool where
  hexS :: Bool -> String
hexS = forall a. Show a => a -> String
show
  binS :: Bool -> String
binS = forall a. Show a => a -> String
show
  hexP :: Bool -> String
hexP = forall a. Show a => a -> String
show
  binP :: Bool -> String
binP = forall a. Show a => a -> String
show
  hex :: Bool -> String
hex  = forall a. Show a => a -> String
show
  bin :: Bool -> String
bin  = forall a. Show a => a -> String
show

instance PrettyNum String where
  hexS :: String -> String
hexS = forall a. Show a => a -> String
show
  binS :: String -> String
binS = forall a. Show a => a -> String
show
  hexP :: String -> String
hexP = forall a. Show a => a -> String
show
  binP :: String -> String
binP = forall a. Show a => a -> String
show
  hex :: String -> String
hex  = forall a. Show a => a -> String
show
  bin :: String -> String
bin  = forall a. Show a => a -> String
show

instance PrettyNum Word8 where
  hexS :: Word8 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True  Bool
True  (Bool
False, Int
8)
  binS :: Word8 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True  Bool
True  (Bool
False, Int
8)

  hexP :: Word8 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True  (Bool
False, Int
8)
  binP :: Word8 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True  (Bool
False, Int
8)

  hex :: Word8 -> String
hex  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, Int
8)
  bin :: Word8 -> String
bin  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, Int
8)

instance PrettyNum Int8 where
  hexS :: Int8 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True  Bool
True  (Bool
True, Int
8)
  binS :: Int8 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True  Bool
True  (Bool
True, Int
8)

  hexP :: Int8 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True  (Bool
True, Int
8)
  binP :: Int8 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True  (Bool
True, Int
8)

  hex :: Int8 -> String
hex  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, Int
8)
  bin :: Int8 -> String
bin  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, Int
8)

instance PrettyNum Word16 where
  hexS :: Word16 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True  Bool
True  (Bool
False, Int
16)
  binS :: Word16 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True  Bool
True  (Bool
False, Int
16)

  hexP :: Word16 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True  (Bool
False, Int
16)
  binP :: Word16 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True  (Bool
False, Int
16)

  hex :: Word16 -> String
hex  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, Int
16)
  bin :: Word16 -> String
bin  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, Int
16)

instance PrettyNum Int16 where
  hexS :: Int16 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True  Bool
True  (Bool
True, Int
16)
  binS :: Int16 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True  Bool
True  (Bool
True, Int
16)

  hexP :: Int16 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True  (Bool
True, Int
16)
  binP :: Int16 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True  (Bool
True, Int
16)

  hex :: Int16 -> String
hex  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, Int
16)
  bin :: Int16 -> String
bin  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, Int
16)

instance PrettyNum Word32 where
  hexS :: Word32 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True  Bool
True  (Bool
False, Int
32)
  binS :: Word32 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True  Bool
True  (Bool
False, Int
32)

  hexP :: Word32 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True  (Bool
False, Int
32)
  binP :: Word32 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True  (Bool
False, Int
32)

  hex :: Word32 -> String
hex  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, Int
32)
  bin :: Word32 -> String
bin  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, Int
32)

instance PrettyNum Int32 where
  hexS :: Int32 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True  Bool
True  (Bool
True, Int
32)
  binS :: Int32 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True  Bool
True  (Bool
True, Int
32)

  hexP :: Int32 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True  (Bool
True, Int
32)
  binP :: Int32 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True  (Bool
True, Int
32)

  hex :: Int32 -> String
hex  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, Int
32)
  bin :: Int32 -> String
bin  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, Int
32)

instance PrettyNum Word64 where
  hexS :: Word64 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True  Bool
True  (Bool
False, Int
64)
  binS :: Word64 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True  Bool
True  (Bool
False, Int
64)

  hexP :: Word64 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True  (Bool
False, Int
64)
  binP :: Word64 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True  (Bool
False, Int
64)

  hex :: Word64 -> String
hex  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
False, Int
64)
  bin :: Word64 -> String
bin  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
False, Int
64)

instance PrettyNum Int64 where
  hexS :: Int64 -> String
hexS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
True  Bool
True  (Bool
True, Int
64)
  binS :: Int64 -> String
binS = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
True  Bool
True  (Bool
True, Int
64)

  hexP :: Int64 -> String
hexP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
True  (Bool
True, Int
64)
  binP :: Int64 -> String
binP = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
True  (Bool
True, Int
64)

  hex :: Int64 -> String
hex  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
False Bool
False (Bool
True, Int
64)
  bin :: Int64 -> String
bin  = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
False Bool
False (Bool
True, Int
64)

instance PrettyNum Integer where
  hexS :: Integer -> String
hexS = Bool -> Bool -> Integer -> String
shexI Bool
True  Bool
True
  binS :: Integer -> String
binS = Bool -> Bool -> Integer -> String
sbinI Bool
True  Bool
True

  hexP :: Integer -> String
hexP = Bool -> Bool -> Integer -> String
shexI Bool
False Bool
True
  binP :: Integer -> String
binP = Bool -> Bool -> Integer -> String
sbinI Bool
False Bool
True

  hex :: Integer -> String
hex  = Bool -> Bool -> Integer -> String
shexI Bool
False Bool
False
  bin :: Integer -> String
bin  = Bool -> Bool -> Integer -> String
sbinI Bool
False Bool
False

shBKind :: HasKind a => a -> String
shBKind :: forall a. HasKind a => a -> String
shBKind a
a = String
" :: " forall a. [a] -> [a] -> [a]
++ Kind -> String
showBaseKind (forall a. HasKind a => a -> Kind
kindOf a
a)

instance PrettyNum CV where
  hexS :: CV -> String
hexS CV
cv | forall a. HasKind a => a -> Bool
isUserSort      CV
cv = forall a. Show a => a -> String -> String
shows CV
cv                                               forall a b. (a -> b) -> a -> b
$  forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isBoolean       CV
cv = forall a. PrettyNum a => a -> String
hexS (CV -> Bool
cvToBool CV
cv)                                     forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isFloat         CV
cv = let CFloat   Float
f = CV -> CVal
cvVal CV
cv in forall a. RealFloat a => a -> String -> String
N.showHFloat Float
f            forall a b. (a -> b) -> a -> b
$  forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isDouble        CV
cv = let CDouble  Double
d = CV -> CVal
cvVal CV
cv in forall a. RealFloat a => a -> String -> String
N.showHFloat Double
d            forall a b. (a -> b) -> a -> b
$  forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isFP            CV
cv = let CFP      FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
16 Bool
True Bool
True FP
f forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isReal          CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show AlgReal
r                    forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isString        CV
cv = let CString  String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show String
s                    forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
          | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
shexI Bool
True Bool
True Integer
i
          | Bool
True               = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex  Bool
True Bool
True (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i

  binS :: CV -> String
binS CV
cv | forall a. HasKind a => a -> Bool
isUserSort      CV
cv = forall a. Show a => a -> String -> String
shows CV
cv                                              forall a b. (a -> b) -> a -> b
$  forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isBoolean       CV
cv = forall a. PrettyNum a => a -> String
binS (CV -> Bool
cvToBool CV
cv)                                    forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isFloat         CV
cv = let CFloat   Float
f = CV -> CVal
cvVal CV
cv in forall a. (Show a, RealFloat a) => a -> String -> String
showBFloat Float
f             forall a b. (a -> b) -> a -> b
$  forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isDouble        CV
cv = let CDouble  Double
d = CV -> CVal
cvVal CV
cv in forall a. (Show a, RealFloat a) => a -> String -> String
showBFloat Double
d             forall a b. (a -> b) -> a -> b
$  forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isFP            CV
cv = let CFP      FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
2 Bool
True Bool
True FP
f forall a. [a] -> [a] -> [a]
++ forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isReal          CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String -> String
shows AlgReal
r                  forall a b. (a -> b) -> a -> b
$  forall a. HasKind a => a -> String
shBKind CV
cv
          | forall a. HasKind a => a -> Bool
isString        CV
cv = let CString  String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String -> String
shows String
s                  forall a b. (a -> b) -> a -> b
$  forall a. HasKind a => a -> String
shBKind CV
cv
          | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
sbinI Bool
True Bool
True Integer
i
          | Bool
True               = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin  Bool
True Bool
True (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i

  hexP :: CV -> String
hexP CV
cv | forall a. HasKind a => a -> Bool
isUserSort      CV
cv = forall a. Show a => a -> String
show CV
cv
          | forall a. HasKind a => a -> Bool
isBoolean       CV
cv = forall a. PrettyNum a => a -> String
hexS (CV -> Bool
cvToBool CV
cv)
          | forall a. HasKind a => a -> Bool
isFloat         CV
cv = let CFloat   Float
f = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Float
f
          | forall a. HasKind a => a -> Bool
isDouble        CV
cv = let CDouble  Double
d = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Double
d
          | forall a. HasKind a => a -> Bool
isFP            CV
cv = let CFP      FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
16 Bool
True Bool
True FP
f
          | forall a. HasKind a => a -> Bool
isReal          CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show AlgReal
r
          | forall a. HasKind a => a -> Bool
isString        CV
cv = let CString  String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show String
s
          | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
shexI Bool
False Bool
True Integer
i
          | Bool
True               = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex  Bool
False Bool
True (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i

  binP :: CV -> String
binP CV
cv | forall a. HasKind a => a -> Bool
isUserSort      CV
cv = forall a. Show a => a -> String
show CV
cv
          | forall a. HasKind a => a -> Bool
isBoolean       CV
cv = forall a. PrettyNum a => a -> String
binS (CV -> Bool
cvToBool CV
cv)
          | forall a. HasKind a => a -> Bool
isFloat         CV
cv = let CFloat   Float
f = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Float
f
          | forall a. HasKind a => a -> Bool
isDouble        CV
cv = let CDouble  Double
d = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Double
d
          | forall a. HasKind a => a -> Bool
isFP            CV
cv = let CFP      FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
2 Bool
True Bool
True FP
f
          | forall a. HasKind a => a -> Bool
isReal          CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show AlgReal
r
          | forall a. HasKind a => a -> Bool
isString        CV
cv = let CString  String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show String
s
          | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
sbinI Bool
False Bool
True Integer
i
          | Bool
True               = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin  Bool
False Bool
True (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i

  hex :: CV -> String
hex CV
cv  | forall a. HasKind a => a -> Bool
isUserSort      CV
cv = forall a. Show a => a -> String
show CV
cv
          | forall a. HasKind a => a -> Bool
isBoolean       CV
cv = forall a. PrettyNum a => a -> String
hexS (CV -> Bool
cvToBool CV
cv)
          | forall a. HasKind a => a -> Bool
isFloat         CV
cv = let CFloat   Float
f = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Float
f
          | forall a. HasKind a => a -> Bool
isDouble        CV
cv = let CDouble  Double
d = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Double
d
          | forall a. HasKind a => a -> Bool
isFP            CV
cv = let CFP      FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
16 Bool
False Bool
True FP
f
          | forall a. HasKind a => a -> Bool
isReal          CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show AlgReal
r
          | forall a. HasKind a => a -> Bool
isString        CV
cv = let CString  String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show String
s
          | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
shexI Bool
False Bool
False Integer
i
          | Bool
True               = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex  Bool
False Bool
False (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i

  bin :: CV -> String
bin CV
cv  | forall a. HasKind a => a -> Bool
isUserSort      CV
cv = forall a. Show a => a -> String
show CV
cv
          | forall a. HasKind a => a -> Bool
isBoolean       CV
cv = forall a. PrettyNum a => a -> String
binS (CV -> Bool
cvToBool CV
cv)
          | forall a. HasKind a => a -> Bool
isFloat         CV
cv = let CFloat   Float
f = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Float
f
          | forall a. HasKind a => a -> Bool
isDouble        CV
cv = let CDouble  Double
d = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show Double
d
          | forall a. HasKind a => a -> Bool
isFP            CV
cv = let CFP      FP
f = CV -> CVal
cvVal CV
cv in Int -> Bool -> Bool -> FP -> String
bfToString Int
2 Bool
False Bool
True FP
f
          | forall a. HasKind a => a -> Bool
isReal          CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show AlgReal
r
          | forall a. HasKind a => a -> Bool
isString        CV
cv = let CString  String
s = CV -> CVal
cvVal CV
cv in forall a. Show a => a -> String
show String
s
          | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
cv) = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in Bool -> Bool -> Integer -> String
sbinI Bool
False Bool
False Integer
i
          | Bool
True               = let CInteger Integer
i = CV -> CVal
cvVal CV
cv in forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin  Bool
False Bool
False (forall a. HasKind a => a -> Bool
hasSign CV
cv, forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i

instance (SymVal a, PrettyNum a) => PrettyNum (SBV a) where
  hexS :: SBV a -> String
hexS SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
hexS :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
  binS :: SBV a -> String
binS SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
binS :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s

  hexP :: SBV a -> String
hexP SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
hexP :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
  binP :: SBV a -> String
binP SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
binP :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s

  hex :: SBV a -> String
hex  SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
hex  :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
  bin :: SBV a -> String
bin  SBV a
s = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show SBV a
s) (forall a. PrettyNum a => a -> String
bin  :: a -> String) forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s

-- | Show as a hexadecimal value. First bool controls whether type info is printed
-- while the second boolean controls whether 0x prefix is printed. The tuple is
-- the signedness and the bit-length of the input. The length of the string
-- will /not/ depend on the value, but rather the bit-length.
shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
shex :: forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
shType Bool
shPre (Bool
signed, Int
size) a
a
 | a
a forall a. Ord a => a -> a -> Bool
< a
0
 = String
"-" forall a. [a] -> [a] -> [a]
++ String
pre forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
l (forall a. (Show a, Integral a) => a -> String
s16 (forall a. Num a => a -> a
abs (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a :: Integer)))  forall a. [a] -> [a] -> [a]
++ String
t
 | Bool
True
 = String
pre forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
l (forall a. (Show a, Integral a) => a -> String
s16 a
a) forall a. [a] -> [a] -> [a]
++ String
t
 where t :: String
t | Bool
shType = String
" :: " forall a. [a] -> [a] -> [a]
++ (if Bool
signed then String
"Int" else String
"Word") forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
size
         | Bool
True   = String
""
       pre :: String
pre | Bool
shPre = String
"0x"
           | Bool
True  = String
""
       l :: Int
l = (Int
size forall a. Num a => a -> a -> a
+ Int
3) forall a. Integral a => a -> a -> a
`div` Int
4

-- | Show as hexadecimal, but for C programs. We have to be careful about
-- printing min-bounds, since C does some funky casting, possibly losing
-- the sign bit. In those cases, we use the defined constants in <stdint.h>.
-- We also properly append the necessary suffixes as needed.
chex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
chex :: forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
chex Bool
shType Bool
shPre (Bool
signed, Int
size) a
a
   | Just String
s <- (Bool
signed, Int
size, forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [((Bool, Int, Integer), String)]
specials
   = String
s
   | Bool
True
   = forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
shType Bool
shPre (Bool
signed, Int
size) a
a forall a. [a] -> [a] -> [a]
++ String
suffix
  where specials :: [((Bool, Int, Integer), String)]
        specials :: [((Bool, Int, Integer), String)]
specials = [ ((Bool
True,  Int
8, forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
minBound :: Int8)),  String
"INT8_MIN" )
                   , ((Bool
True, Int
16, forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
minBound :: Int16)), String
"INT16_MIN")
                   , ((Bool
True, Int
32, forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
minBound :: Int32)), String
"INT32_MIN")
                   , ((Bool
True, Int
64, forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
minBound :: Int64)), String
"INT64_MIN")
                   ]
        suffix :: String
suffix = case (Bool
signed, Int
size) of
                   (Bool
False, Int
16) -> String
"U"

                   (Bool
False, Int
32) -> String
"UL"
                   (Bool
True,  Int
32) -> String
"L"

                   (Bool
False, Int
64) -> String
"ULL"
                   (Bool
True,  Int
64) -> String
"LL"

                   (Bool, Int)
_           -> String
""

-- | Show as a hexadecimal value, integer version. Almost the same as shex above
-- except we don't have a bit-length so the length of the string will depend
-- on the actual value.
shexI :: Bool -> Bool -> Integer -> String
shexI :: Bool -> Bool -> Integer -> String
shexI Bool
shType Bool
shPre Integer
a
 | Integer
a forall a. Ord a => a -> a -> Bool
< Integer
0
 = String
"-" forall a. [a] -> [a] -> [a]
++ String
pre forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Integral a) => a -> String
s16 (forall a. Num a => a -> a
abs Integer
a)  forall a. [a] -> [a] -> [a]
++ String
t
 | Bool
True
 = String
pre forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Integral a) => a -> String
s16 Integer
a forall a. [a] -> [a] -> [a]
++ String
t
 where t :: String
t | Bool
shType = String
" :: Integer"
         | Bool
True   = String
""
       pre :: String
pre | Bool
shPre = String
"0x"
           | Bool
True  = String
""

-- | Similar to 'shex'; except in binary.
sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
sbin :: forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
shType Bool
shPre (Bool
signed,Int
size) a
a
 | a
a forall a. Ord a => a -> a -> Bool
< a
0
 = String
"-" forall a. [a] -> [a] -> [a]
++ String
pre forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
size (forall a. (Show a, Integral a) => a -> String
s2 (forall a. Num a => a -> a
abs (forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a :: Integer)))  forall a. [a] -> [a] -> [a]
++ String
t
 | Bool
True
 = String
pre forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
size (forall a. (Show a, Integral a) => a -> String
s2 a
a) forall a. [a] -> [a] -> [a]
++ String
t
 where t :: String
t | Bool
shType = String
" :: " forall a. [a] -> [a] -> [a]
++ (if Bool
signed then String
"Int" else String
"Word") forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
size
         | Bool
True   = String
""
       pre :: String
pre | Bool
shPre = String
"0b"
           | Bool
True  = String
""

-- | Similar to 'shexI'; except in binary.
sbinI :: Bool -> Bool -> Integer -> String
sbinI :: Bool -> Bool -> Integer -> String
sbinI Bool
shType Bool
shPre Integer
a
 | Integer
a forall a. Ord a => a -> a -> Bool
< Integer
0
 = String
"-" forall a. [a] -> [a] -> [a]
++ String
pre forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Integral a) => a -> String
s2 (forall a. Num a => a -> a
abs Integer
a) forall a. [a] -> [a] -> [a]
++ String
t
 | Bool
True
 =  String
pre forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Integral a) => a -> String
s2 Integer
a forall a. [a] -> [a] -> [a]
++ String
t
 where t :: String
t | Bool
shType = String
" :: Integer"
         | Bool
True   = String
""
       pre :: String
pre | Bool
shPre = String
"0b"
           | Bool
True  = String
""

-- | Pad a string to a given length. If the string is longer, then we don't drop anything.
pad :: Int -> String -> String
pad :: Int -> String -> String
pad Int
l String
s = forall a. Int -> a -> [a]
replicate (Int
l forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) Char
'0' forall a. [a] -> [a] -> [a]
++ String
s

-- | Binary printer
s2 :: (Show a, Integral a) => a -> String
s2 :: forall a. (Show a, Integral a) => a -> String
s2  a
v = forall a.
(Integral a, Show a) =>
a -> (Int -> Char) -> a -> String -> String
showIntAtBase a
2 Int -> Char
dig a
v String
"" where dig :: Int -> Char
dig = forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup [(Int
0, Char
'0'), (Int
1, Char
'1')]

-- | Hex printer
s16 :: (Show a, Integral a) => a -> String
s16 :: forall a. (Show a, Integral a) => a -> String
s16 a
v = forall a. (Integral a, Show a) => a -> String -> String
showHex a
v String
""

-- | A more convenient interface for reading binary numbers, also supports negative numbers
readBin :: Num a => String -> a
readBin :: forall a. Num a => String -> a
readBin (Char
'-':String
s) = -(forall a. Num a => String -> a
readBin String
s)
readBin String
s = case forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
readInt a
2 Char -> Bool
isDigit Char -> Int
cvt String
s' of
              [(a
a, String
"")] -> a
a
              [(a, String)]
_         -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.readBin: Cannot read a binary number from: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
s
  where cvt :: Char -> Int
cvt Char
c = Char -> Int
ord Char
c forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0'
        isDigit :: Char -> Bool
isDigit = (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"01")
        s' :: String
s' | String
"0b" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
s = forall a. Int -> [a] -> [a]
drop Int
2 String
s
           | Bool
True                = String
s

-- | A version of show for floats that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.
showCFloat :: Float -> String
showCFloat :: Float -> String
showCFloat Float
f
   | forall a. RealFloat a => a -> Bool
isNaN Float
f             = String
"((float) NAN)"
   | forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f forall a. Ord a => a -> a -> Bool
< Float
0 = String
"((float) (-INFINITY))"
   | forall a. RealFloat a => a -> Bool
isInfinite Float
f        = String
"((float) INFINITY)"
   | Bool
True                = forall a. RealFloat a => a -> String -> String
N.showHFloat Float
f forall a b. (a -> b) -> a -> b
$ String
"F /* " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Float
f forall a. [a] -> [a] -> [a]
++ String
"F */"

-- | A version of show for doubles that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included.
showCDouble :: Double -> String
showCDouble :: Double -> String
showCDouble Double
d
   | forall a. RealFloat a => a -> Bool
isNaN Double
d             = String
"((double) NAN)"
   | forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d forall a. Ord a => a -> a -> Bool
< Double
0 = String
"((double) (-INFINITY))"
   | forall a. RealFloat a => a -> Bool
isInfinite Double
d        = String
"((double) INFINITY)"
   | Bool
True                = forall a. RealFloat a => a -> String -> String
N.showHFloat Double
d String
" /* " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Double
d forall a. [a] -> [a] -> [a]
++ String
" */"

-- | A version of show for floats that generates correct Haskell literals for nan/infinite
showHFloat :: Float -> String
showHFloat :: Float -> String
showHFloat Float
f
   | forall a. RealFloat a => a -> Bool
isNaN Float
f             = String
"((0/0) :: Float)"
   | forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f forall a. Ord a => a -> a -> Bool
< Float
0 = String
"((-1/0) :: Float)"
   | forall a. RealFloat a => a -> Bool
isInfinite Float
f        = String
"((1/0) :: Float)"
   | Bool
True                = forall a. Show a => a -> String
show Float
f

-- | A version of show for doubles that generates correct Haskell literals for nan/infinite
showHDouble :: Double -> String
showHDouble :: Double -> String
showHDouble Double
d
   | forall a. RealFloat a => a -> Bool
isNaN Double
d             = String
"((0/0) :: Double)"
   | forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d forall a. Ord a => a -> a -> Bool
< Double
0 = String
"((-1/0) :: Double)"
   | forall a. RealFloat a => a -> Bool
isInfinite Double
d        = String
"((1/0) :: Double)"
   | Bool
True                = forall a. Show a => a -> String
show Double
d

-- | A version of show for floats that generates correct SMTLib literals using the rounding mode
showSMTFloat :: RoundingMode -> Float -> String
showSMTFloat :: RoundingMode -> Float -> String
showSMTFloat RoundingMode
rm Float
f
   | forall a. RealFloat a => a -> Bool
isNaN Float
f             = String -> String
as String
"NaN"
   | forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f forall a. Ord a => a -> a -> Bool
< Float
0 = String -> String
as String
"-oo"
   | forall a. RealFloat a => a -> Bool
isInfinite Float
f        = String -> String
as String
"+oo"
   | forall a. RealFloat a => a -> Bool
isNegativeZero Float
f    = String -> String
as String
"-zero"
   | Float
f forall a. Eq a => a -> a -> Bool
== Float
0              = String -> String
as String
"+zero"
   | Bool
True                = String
"((_ to_fp 8 24) " forall a. [a] -> [a] -> [a]
++ RoundingMode -> String
smtRoundingMode RoundingMode
rm forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Rational -> String
toSMTLibRational (forall a. Real a => a -> Rational
toRational Float
f) forall a. [a] -> [a] -> [a]
++ String
")"
   where as :: String -> String
as String
s = String
"(_ " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" 8 24)"


-- | A version of show for doubles that generates correct SMTLib literals using the rounding mode
showSMTDouble :: RoundingMode -> Double -> String
showSMTDouble :: RoundingMode -> Double -> String
showSMTDouble RoundingMode
rm Double
d
   | forall a. RealFloat a => a -> Bool
isNaN Double
d             = String -> String
as String
"NaN"
   | forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d forall a. Ord a => a -> a -> Bool
< Double
0 = String -> String
as String
"-oo"
   | forall a. RealFloat a => a -> Bool
isInfinite Double
d        = String -> String
as String
"+oo"
   | forall a. RealFloat a => a -> Bool
isNegativeZero Double
d    = String -> String
as String
"-zero"
   | Double
d forall a. Eq a => a -> a -> Bool
== Double
0              = String -> String
as String
"+zero"
   | Bool
True                = String
"((_ to_fp 11 53) " forall a. [a] -> [a] -> [a]
++ RoundingMode -> String
smtRoundingMode RoundingMode
rm forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Rational -> String
toSMTLibRational (forall a. Real a => a -> Rational
toRational Double
d) forall a. [a] -> [a] -> [a]
++ String
")"
   where as :: String -> String
as String
s = String
"(_ " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" 11 53)"

-- | Show an SBV rational as an SMTLib value. This is used for faithful rationals.
showSMTRational :: Rational -> String
showSMTRational :: Rational -> String
showSMTRational Rational
r = String
"(SBV.Rational " forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber (forall a. Ratio a -> a
numerator Rational
r) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber (forall a. Ratio a -> a
denominator Rational
r) forall a. [a] -> [a] -> [a]
++ String
")"

-- | Show a rational in SMTLib format. This is used for conversions from regular rationals.
toSMTLibRational :: Rational -> String
toSMTLibRational :: Rational -> String
toSMTLibRational Rational
r
   | Integer
n forall a. Ord a => a -> a -> Bool
< Integer
0
   = String
"(- (/ "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Num a => a -> a
abs Integer
n) forall a. [a] -> [a] -> [a]
++ String
".0 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
d forall a. [a] -> [a] -> [a]
++ String
".0))"
   | Bool
True
   = String
"(/ " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n forall a. [a] -> [a] -> [a]
++ String
".0 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
d forall a. [a] -> [a] -> [a]
++ String
".0)"
  where n :: Integer
n = forall a. Ratio a -> a
numerator Rational
r
        d :: Integer
d = forall a. Ratio a -> a
denominator Rational
r

-- | Convert a CV to an SMTLib2 compliant value
cvToSMTLib :: RoundingMode -> CV -> String
cvToSMTLib :: RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm CV
x
  | forall a. HasKind a => a -> Bool
isBoolean       CV
x, CInteger  Integer
w      <- CV -> CVal
cvVal CV
x = if Integer
w forall a. Eq a => a -> a -> Bool
== Integer
0 then String
"false" else String
"true"
  | forall a. HasKind a => a -> Bool
isUserSort      CV
x, CUserSort (Maybe Int
_, String
s) <- CV -> CVal
cvVal CV
x = String -> String
roundModeConvert String
s
  | forall a. HasKind a => a -> Bool
isReal          CV
x, CAlgReal  AlgReal
r      <- CV -> CVal
cvVal CV
x = AlgReal -> String
algRealToSMTLib2 AlgReal
r
  | forall a. HasKind a => a -> Bool
isFloat         CV
x, CFloat    Float
f      <- CV -> CVal
cvVal CV
x = RoundingMode -> Float -> String
showSMTFloat  RoundingMode
rm Float
f
  | forall a. HasKind a => a -> Bool
isDouble        CV
x, CDouble   Double
d      <- CV -> CVal
cvVal CV
x = RoundingMode -> Double -> String
showSMTDouble RoundingMode
rm Double
d
  | forall a. HasKind a => a -> Bool
isRational      CV
x, CRational Rational
r      <- CV -> CVal
cvVal CV
x = Rational -> String
showSMTRational Rational
r
  | forall a. HasKind a => a -> Bool
isFP            CV
x, CFP       FP
f      <- CV -> CVal
cvVal CV
x = FP -> String
fprToSMTLib2 FP
f
  | Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded CV
x), CInteger  Integer
w      <- CV -> CVal
cvVal CV
x = if Integer
w forall a. Ord a => a -> a -> Bool
>= Integer
0 then forall a. Show a => a -> String
show Integer
w else String
"(- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Num a => a -> a
abs Integer
w) forall a. [a] -> [a] -> [a]
++ String
")"
  | Bool -> Bool
not (forall a. HasKind a => a -> Bool
hasSign CV
x)  , CInteger  Integer
w      <- CV -> CVal
cvVal CV
x = Int -> Integer -> String
smtLibHex (forall a. HasKind a => a -> Int
intSizeOf CV
x) Integer
w
  -- signed numbers (with 2's complement representation) is problematic
  -- since there's no way to put a bvneg over a positive number to get minBound..
  -- Hence, we punt and use binary notation in that particular case
  | forall a. HasKind a => a -> Bool
hasSign CV
x        , CInteger  Integer
w      <- CV -> CVal
cvVal CV
x = if Integer
w forall a. Eq a => a -> a -> Bool
== forall a. Num a => a -> a
negate (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ forall a. HasKind a => a -> Int
intSizeOf CV
x)
                                                     then Int -> String
mkMinBound (forall a. HasKind a => a -> Int
intSizeOf CV
x)
                                                     else Bool -> String -> String
negIf (Integer
w forall a. Ord a => a -> a -> Bool
< Integer
0) forall a b. (a -> b) -> a -> b
$ Int -> Integer -> String
smtLibHex (forall a. HasKind a => a -> Int
intSizeOf CV
x) (forall a. Num a => a -> a
abs Integer
w)
  | forall a. HasKind a => a -> Bool
isChar CV
x         , CChar Char
c          <- CV -> CVal
cvVal CV
x = String
"(_ char " forall a. [a] -> [a] -> [a]
++ Int -> Integer -> String
smtLibHex Int
8 (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
ord Char
c)) forall a. [a] -> [a] -> [a]
++ String
")"
  | forall a. HasKind a => a -> Bool
isString CV
x       , CString String
s        <- CV -> CVal
cvVal CV
x = Char
'\"' forall a. a -> [a] -> [a]
: String -> String
stringToQFS String
s forall a. [a] -> [a] -> [a]
++ String
"\""
  | forall a. HasKind a => a -> Bool
isList CV
x         , CList [CVal]
xs         <- CV -> CVal
cvVal CV
x = Kind -> [CVal] -> String
smtLibSeq (forall a. HasKind a => a -> Kind
kindOf CV
x) [CVal]
xs
  | forall a. HasKind a => a -> Bool
isSet CV
x          , CSet RCSet CVal
s           <- CV -> CVal
cvVal CV
x = Kind -> RCSet CVal -> String
smtLibSet (forall a. HasKind a => a -> Kind
kindOf CV
x) RCSet CVal
s
  | forall a. HasKind a => a -> Bool
isTuple CV
x        , CTuple [CVal]
xs        <- CV -> CVal
cvVal CV
x = Kind -> [CVal] -> String
smtLibTup (forall a. HasKind a => a -> Kind
kindOf CV
x) [CVal]
xs
  | forall a. HasKind a => a -> Bool
isMaybe CV
x        , CMaybe Maybe CVal
mc        <- CV -> CVal
cvVal CV
x = Kind -> Maybe CVal -> String
smtLibMaybe  (forall a. HasKind a => a -> Kind
kindOf CV
x) Maybe CVal
mc
  | forall a. HasKind a => a -> Bool
isEither CV
x       , CEither Either CVal CVal
ec       <- CV -> CVal
cvVal CV
x = Kind -> Either CVal CVal -> String
smtLibEither (forall a. HasKind a => a -> Kind
kindOf CV
x) Either CVal CVal
ec

  | Bool
True = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.cvtCV: Impossible happened: Kind/Value disagreement on: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. HasKind a => a -> Kind
kindOf CV
x, CV
x)
  where roundModeConvert :: String -> String
roundModeConvert String
s = forall a. a -> Maybe a -> a
fromMaybe String
s (forall a. [a] -> Maybe a
listToMaybe [RoundingMode -> String
smtRoundingMode RoundingMode
m | RoundingMode
m <- [forall a. Bounded a => a
minBound .. forall a. Bounded a => a
maxBound] :: [RoundingMode], forall a. Show a => a -> String
show RoundingMode
m forall a. Eq a => a -> a -> Bool
== String
s])
        -- Carefully code hex numbers, SMTLib is picky about lengths of hex constants. For the time
        -- being, SBV only supports sizes that are multiples of 4, but the below code is more robust
        -- in case of future extensions to support arbitrary sizes.
        smtLibHex :: Int -> Integer -> String
        smtLibHex :: Int -> Integer -> String
smtLibHex Int
1  Integer
v = String
"#b" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
v
        smtLibHex Int
sz Integer
v
          | Int
sz forall a. Integral a => a -> a -> a
`mod` Int
4 forall a. Eq a => a -> a -> Bool
== Int
0 = String
"#x" forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad (Int
sz forall a. Integral a => a -> a -> a
`div` Int
4) (forall a. (Integral a, Show a) => a -> String -> String
showHex Integer
v String
"")
          | Bool
True            = String
"#b" forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
sz (Integer -> String -> String
showBin Integer
v String
"")
           where showBin :: Integer -> String -> String
showBin = forall a.
(Integral a, Show a) =>
a -> (Int -> Char) -> a -> String -> String
showIntAtBase Integer
2 Int -> Char
intToDigit
        negIf :: Bool -> String -> String
        negIf :: Bool -> String -> String
negIf Bool
True  String
a = String
"(bvneg " forall a. [a] -> [a] -> [a]
++ String
a forall a. [a] -> [a] -> [a]
++ String
")"
        negIf Bool
False String
a = String
a

        smtLibSeq :: Kind -> [CVal] -> String
        smtLibSeq :: Kind -> [CVal] -> String
smtLibSeq Kind
k          [] = String
"(as seq.empty " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k forall a. [a] -> [a] -> [a]
++ String
")"
        smtLibSeq (KList Kind
ek) [CVal]
xs = let mkSeq :: [String] -> String
mkSeq  [String
e]   = String
e
                                      mkSeq  [String]
es    = String
"(seq.++ " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
es forall a. [a] -> [a] -> [a]
++ String
")"
                                      mkUnit :: String -> String
mkUnit String
inner = String
"(seq.unit " forall a. [a] -> [a] -> [a]
++ String
inner forall a. [a] -> [a] -> [a]
++ String
")"
                                  in [String] -> String
mkSeq (String -> String
mkUnit forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
ek forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CVal]
xs)
        smtLibSeq Kind
k [CVal]
_ = forall a. HasCallStack => String -> a
error String
"SBV.cvToSMTLib: Impossible case (smtLibSeq), received kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k

        smtLibSet :: Kind -> RCSet CVal -> String
        smtLibSet :: Kind -> RCSet CVal -> String
smtLibSet Kind
k RCSet CVal
set = case RCSet CVal
set of
                            RegularSet    Set CVal
rs -> forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr' (String -> CVal -> String -> String
modify String
"true")  (String -> String
start String
"false") Set CVal
rs
                            ComplementSet Set CVal
rs -> forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr' (String -> CVal -> String -> String
modify String
"false") (String -> String
start String
"true")  Set CVal
rs
          where ke :: Kind
ke = case Kind
k of
                       KSet Kind
ek -> Kind
ek
                       Kind
_       -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibSet), received kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k

                start :: String -> String
start String
def = String
"((as const " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ String
def forall a. [a] -> [a] -> [a]
++ String
")"

                modify :: String -> CVal -> String -> String
modify String
how CVal
e String
s = String
"(store " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
ke CVal
e) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
how forall a. [a] -> [a] -> [a]
++ String
")"

        smtLibTup :: Kind -> [CVal] -> String
        smtLibTup :: Kind -> [CVal] -> String
smtLibTup (KTuple []) [CVal]
_  = String
"mkSBVTuple0"
        smtLibTup (KTuple [Kind]
ks) [CVal]
xs = String
"(mkSBVTuple" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks) forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Kind
ek CVal
e -> RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
ek CVal
e)) [Kind]
ks [CVal]
xs) forall a. [a] -> [a] -> [a]
++ String
")"
        smtLibTup Kind
k           [CVal]
_  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibTup), received kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k

        dtConstructor :: String -> [String] -> Kind -> String
dtConstructor String
fld []   Kind
res =  String
"(as " forall a. [a] -> [a] -> [a]
++ String
fld forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res forall a. [a] -> [a] -> [a]
++ String
")"
        dtConstructor String
fld [String]
args Kind
res = String
"((as " forall a. [a] -> [a] -> [a]
++ String
fld forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args forall a. [a] -> [a] -> [a]
++ String
")"

        smtLibMaybe :: Kind -> Maybe CVal -> String
        smtLibMaybe :: Kind -> Maybe CVal -> String
smtLibMaybe km :: Kind
km@KMaybe{}   Maybe CVal
Nothing   = String -> [String] -> Kind -> String
dtConstructor String
"nothing_SBVMaybe" []                       Kind
km
        smtLibMaybe km :: Kind
km@(KMaybe Kind
k) (Just  CVal
c) = String -> [String] -> Kind -> String
dtConstructor String
"just_SBVMaybe"    [RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
k CVal
c)] Kind
km
        smtLibMaybe Kind
k             Maybe CVal
_         = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibMaybe), received kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k

        smtLibEither :: Kind -> Either CVal CVal -> String
        smtLibEither :: Kind -> Either CVal CVal -> String
smtLibEither ke :: Kind
ke@(KEither  Kind
k Kind
_) (Left CVal
c)  = String -> [String] -> Kind -> String
dtConstructor String
"left_SBVEither"  [RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
k CVal
c)] Kind
ke
        smtLibEither ke :: Kind
ke@(KEither  Kind
_ Kind
k) (Right CVal
c) = String -> [String] -> Kind -> String
dtConstructor String
"right_SBVEither" [RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
k CVal
c)] Kind
ke
        smtLibEither Kind
k                 Either CVal CVal
_         = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibEither), received kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k

        -- anomaly at the 2's complement min value! Have to use binary notation here
        -- as there is no positive value we can provide to make the bvneg work.. (see above)
        mkMinBound :: Int -> String
        mkMinBound :: Int -> String
mkMinBound Int
i = String
"#b1" forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (Int
iforall a. Num a => a -> a -> a
-Int
1) Char
'0'

-- | Create a skolem 0 for the kind
mkSkolemZero :: RoundingMode -> Kind -> String
mkSkolemZero :: RoundingMode -> Kind -> String
mkSkolemZero RoundingMode
_ (KUserSort String
_ (Just (String
f:[String]
_))) = String
f
mkSkolemZero RoundingMode
_ (KUserSort String
s Maybe [String]
_)            = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.mkSkolemZero: Unexpected user sort: " forall a. [a] -> [a] -> [a]
++ String
s
mkSkolemZero RoundingMode
rm Kind
k                         = RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k (Integer
0::Integer))

-- | Show a float as a binary
showBFloat :: (Show a, RealFloat a) => a -> ShowS
showBFloat :: forall a. (Show a, RealFloat a) => a -> String -> String
showBFloat = forall a. (Show a, RealFloat a) => Int -> a -> String -> String
showFloatAtBase Int
2

-- | Like Haskell's showHFloat, but uses arbitrary base instead.
-- Note that the exponent is always written in decimal. Let the exponent value be d:
--    If base=10, then we use @e@ to denote the exponent; meaning 10^d
--    If base is a power of 2, then we use @p@ to denote the exponent; meaning 2^d
--    Otherwise, we use @ to denote the exponent, and it means base^d
showFloatAtBase :: (Show a, RealFloat a) => Int -> a -> ShowS
showFloatAtBase :: forall a. (Show a, RealFloat a) => Int -> a -> String -> String
showFloatAtBase Int
base a
input
  | Int
base forall a. Ord a => a -> a -> Bool
< Int
2 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"showFloatAtBase: Received invalid base (must be >= 2): " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
base
  | Bool
True     = String -> String -> String
showString forall a b. (a -> b) -> a -> b
$ forall {a}. RealFloat a => a -> String
fmt a
input
  where fmt :: a -> String
fmt a
x
         | forall a. RealFloat a => a -> Bool
isNaN a
x                   = String
"NaN"
         | forall a. RealFloat a => a -> Bool
isInfinite a
x              = (if a
x forall a. Ord a => a -> a -> Bool
< a
0 then String
"-" else String
"") forall a. [a] -> [a] -> [a]
++ String
"Infinity"
         | a
x forall a. Ord a => a -> a -> Bool
< a
0 Bool -> Bool -> Bool
|| forall a. RealFloat a => a -> Bool
isNegativeZero a
x = Char
'-' forall a. a -> [a] -> [a]
: forall {a}. RealFloat a => a -> String
cvt (-a
x)
         | Bool
True                      = forall {a}. RealFloat a => a -> String
cvt a
x

        basePow2 :: Bool
basePow2 = Int
base forall a. Bits a => a -> a -> a
.&. (Int
baseforall a. Num a => a -> a -> a
-Int
1) forall a. Eq a => a -> a -> Bool
== Int
0
        lg2Base :: Int
lg2Base  = forall b. FiniteBits b => b -> Int
countTrailingZeros Int
base  -- only used when basePow2 is true

        prefix :: String
prefix = case Int
base of
                   Int
2  -> String
"0b"
                   Int
8  -> String
"0o"
                   Int
10 -> String
""
                   Int
16 -> String
"0x"
                   Int
x  -> String
"0<" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
x forall a. [a] -> [a] -> [a]
++ String
">"

        powChar :: Char
powChar
          | Int
base forall a. Eq a => a -> a -> Bool
== Int
10 = Char
'e'
          | Bool
basePow2   = Char
'p'
          | Bool
True       = Char
'@'

        -- why r-1? Because we're shifting the fraction by 1 digit; does reducing the exponent by 1
        f2d :: a -> (Int, [Int], Int)
f2d a
x = case forall a. RealFloat a => Integer -> a -> ([Int], Int)
floatToDigits (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
base) a
x of
                  ([],   Int
e) -> (Int
0, [], Int
e forall a. Num a => a -> a -> a
- Int
1)
                  (Int
d:[Int]
ds, Int
e) -> (Int
d, [Int]
ds, Int
e forall a. Num a => a -> a -> a
- Int
1)

        cvt :: a -> String
cvt a
x
         | a
x forall a. Eq a => a -> a -> Bool
== a
0 = String
prefix forall a. [a] -> [a] -> [a]
++ Char
'0' forall a. a -> [a] -> [a]
: Char
powChar forall a. a -> [a] -> [a]
: String
"+0"
         | Bool
True   = String
prefix forall a. [a] -> [a] -> [a]
++ Int -> String
toDigit Int
d forall a. [a] -> [a] -> [a]
++ forall {t :: * -> *}. Foldable t => t Int -> String
frac [Int]
ds forall a. [a] -> [a] -> [a]
++ String
pow
         where (Int
d, [Int]
ds, Int
e)  = forall {a}. RealFloat a => a -> (Int, [Int], Int)
f2d a
x
               pow :: String
pow
                | Int
base forall a. Eq a => a -> a -> Bool
== Int
10 = Char
powChar forall a. a -> [a] -> [a]
: forall {a}. (Ord a, Num a, Show a) => a -> String
shSigned Int
e
                | Bool
basePow2   = Char
powChar forall a. a -> [a] -> [a]
: forall {a}. (Ord a, Num a, Show a) => a -> String
shSigned (Int
e forall a. Num a => a -> a -> a
* Int
lg2Base)
                | Bool
True       = Char
powChar forall a. a -> [a] -> [a]
: forall {a}. (Ord a, Num a, Show a) => a -> String
shSigned Int
e

               shSigned :: a -> String
shSigned a
v
                | a
v forall a. Ord a => a -> a -> Bool
< a
0      =       forall a. Show a => a -> String
show a
v
                | Bool
True       = Char
'+' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show a
v

        -- Given digits, show them except if they're all 0 then drop
        frac :: t Int -> String
frac t Int
digits
         | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== Int
0) t Int
digits = String
""
         | Bool
True              = String
"." forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> String
toDigit t Int
digits

        toDigit :: Int -> String
toDigit Int
v = forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toUpper String
d
           where d :: String
d | Int
v forall a. Ord a => a -> a -> Bool
<= Int
15 = [Int -> Char
intToDigit Int
v]
                   | Int
v forall a. Ord a => a -> a -> Bool
<  Int
36 = [Int -> Char
chr (Char -> Int
ord Char
'a' forall a. Num a => a -> a -> a
+ Int
v forall a. Num a => a -> a -> a
- Int
10)]
                   | Bool
True    = Char
'<' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show Int
v forall a. [a] -> [a] -> [a]
++ String
">"

-- | When we show a negative number in SMTLib, we must properly parenthesize.
showNegativeNumber :: (Show a, Num a, Ord a) => a -> String
showNegativeNumber :: forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber a
i
  | a
i forall a. Ord a => a -> a -> Bool
< a
0 = String
"(- " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (-a
i) forall a. [a] -> [a] -> [a]
++ String
")"
  | Bool
True  = forall a. Show a => a -> String
show a
i