-----------------------------------------------------------------------------
-- |
-- 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 = Bool -> String
forall a. Show a => a -> String
show
  binS :: Bool -> String
binS = Bool -> String
forall a. Show a => a -> String
show
  hexP :: Bool -> String
hexP = Bool -> String
forall a. Show a => a -> String
show
  binP :: Bool -> String
binP = Bool -> String
forall a. Show a => a -> String
show
  hex :: Bool -> String
hex  = Bool -> String
forall a. Show a => a -> String
show
  bin :: Bool -> String
bin  = Bool -> String
forall a. Show a => a -> String
show

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

instance PrettyNum Word8 where
  hexS :: Word8 -> String
hexS = Bool -> Bool -> (Bool, Int) -> Word8 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word8 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word8 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word8 -> String
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  = Bool -> Bool -> (Bool, Int) -> Word8 -> String
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  = Bool -> Bool -> (Bool, Int) -> Word8 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int8 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int8 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int8 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int8 -> String
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  = Bool -> Bool -> (Bool, Int) -> Int8 -> String
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  = Bool -> Bool -> (Bool, Int) -> Int8 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word16 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word16 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word16 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word16 -> String
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  = Bool -> Bool -> (Bool, Int) -> Word16 -> String
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  = Bool -> Bool -> (Bool, Int) -> Word16 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int16 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int16 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int16 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int16 -> String
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  = Bool -> Bool -> (Bool, Int) -> Int16 -> String
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  = Bool -> Bool -> (Bool, Int) -> Int16 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word32 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word32 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word32 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word32 -> String
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  = Bool -> Bool -> (Bool, Int) -> Word32 -> String
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  = Bool -> Bool -> (Bool, Int) -> Word32 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int32 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int32 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int32 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int32 -> String
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  = Bool -> Bool -> (Bool, Int) -> Int32 -> String
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  = Bool -> Bool -> (Bool, Int) -> Int32 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word64 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word64 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word64 -> String
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 = Bool -> Bool -> (Bool, Int) -> Word64 -> String
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  = Bool -> Bool -> (Bool, Int) -> Word64 -> String
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  = Bool -> Bool -> (Bool, Int) -> Word64 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int64 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int64 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int64 -> String
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 = Bool -> Bool -> (Bool, Int) -> Int64 -> String
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  = Bool -> Bool -> (Bool, Int) -> Int64 -> String
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  = Bool -> Bool -> (Bool, Int) -> Int64 -> String
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 :: a -> String
shBKind a
a = String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
showBaseKind (a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
a)

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

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

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

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

  hex :: CV -> String
hex CV
cv  | CV -> Bool
forall a. HasKind a => a -> Bool
isUserSort      CV
cv = CV -> String
forall a. Show a => a -> String
show CV
cv
          | CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean       CV
cv = Bool -> String
forall a. PrettyNum a => a -> String
hexS (CV -> Bool
cvToBool CV
cv)
          | CV -> Bool
forall a. HasKind a => a -> Bool
isFloat         CV
cv = let CFloat   Float
f = CV -> CVal
cvVal CV
cv in Float -> String
forall a. Show a => a -> String
show Float
f
          | CV -> Bool
forall a. HasKind a => a -> Bool
isDouble        CV
cv = let CDouble  Double
d = CV -> CVal
cvVal CV
cv in Double -> String
forall a. Show a => a -> String
show Double
d
          | CV -> Bool
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
          | CV -> Bool
forall a. HasKind a => a -> Bool
isReal          CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
          | CV -> Bool
forall a. HasKind a => a -> Bool
isString        CV
cv = let CString  String
s = CV -> CVal
cvVal CV
cv in String -> String
forall a. Show a => a -> String
show String
s
          | Bool -> Bool
not (CV -> Bool
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 Bool -> Bool -> (Bool, Int) -> Integer -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex  Bool
False Bool
False (CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
cv, CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
cv) Integer
i

  bin :: CV -> String
bin CV
cv  | CV -> Bool
forall a. HasKind a => a -> Bool
isUserSort      CV
cv = CV -> String
forall a. Show a => a -> String
show CV
cv
          | CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean       CV
cv = Bool -> String
forall a. PrettyNum a => a -> String
binS (CV -> Bool
cvToBool CV
cv)
          | CV -> Bool
forall a. HasKind a => a -> Bool
isFloat         CV
cv = let CFloat   Float
f = CV -> CVal
cvVal CV
cv in Float -> String
forall a. Show a => a -> String
show Float
f
          | CV -> Bool
forall a. HasKind a => a -> Bool
isDouble        CV
cv = let CDouble  Double
d = CV -> CVal
cvVal CV
cv in Double -> String
forall a. Show a => a -> String
show Double
d
          | CV -> Bool
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
          | CV -> Bool
forall a. HasKind a => a -> Bool
isReal          CV
cv = let CAlgReal AlgReal
r = CV -> CVal
cvVal CV
cv in AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r
          | CV -> Bool
forall a. HasKind a => a -> Bool
isString        CV
cv = let CString  String
s = CV -> CVal
cvVal CV
cv in String -> String
forall a. Show a => a -> String
show String
s
          | Bool -> Bool
not (CV -> Bool
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 Bool -> Bool -> (Bool, Int) -> Integer -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
sbin  Bool
False Bool
False (CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
cv, CV -> Int
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 = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SBV a -> String
forall a. Show a => a -> String
show SBV a
s) (a -> String
forall a. PrettyNum a => a -> String
hexS :: a -> String) (Maybe a -> String) -> Maybe a -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
  binS :: SBV a -> String
binS SBV a
s = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SBV a -> String
forall a. Show a => a -> String
show SBV a
s) (a -> String
forall a. PrettyNum a => a -> String
binS :: a -> String) (Maybe a -> String) -> Maybe a -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s

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

  hex :: SBV a -> String
hex  SBV a
s = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SBV a -> String
forall a. Show a => a -> String
show SBV a
s) (a -> String
forall a. PrettyNum a => a -> String
hex  :: a -> String) (Maybe a -> String) -> Maybe a -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
s
  bin :: SBV a -> String
bin  SBV a
s = String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (SBV a -> String
forall a. Show a => a -> String
show SBV a
s) (a -> String
forall a. PrettyNum a => a -> String
bin  :: a -> String) (Maybe a -> String) -> Maybe a -> String
forall a b. (a -> b) -> a -> b
$ SBV a -> Maybe a
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 :: Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
shType Bool
shPre (Bool
signed, Int
size) a
a
 | a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0
 = String
"-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
l (Integer -> String
forall a. (Show a, Integral a) => a -> String
s16 (Integer -> Integer
forall a. Num a => a -> a
abs (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a :: Integer)))  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
 | Bool
True
 = String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
l (a -> String
forall a. (Show a, Integral a) => a -> String
s16 a
a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
 where t :: String
t | Bool
shType = String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
signed then String
"Int" else String
"Word") String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
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 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
3) Int -> Int -> Int
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 :: Bool -> Bool -> (Bool, Int) -> a -> String
chex Bool
shType Bool
shPre (Bool
signed, Int
size) a
a
   | Just String
s <- (Bool
signed, Int
size, a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a) (Bool, Int, Integer)
-> [((Bool, Int, Integer), String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [((Bool, Int, Integer), String)]
specials
   = String
s
   | Bool
True
   = Bool -> Bool -> (Bool, Int) -> a -> String
forall a.
(Show a, Integral a) =>
Bool -> Bool -> (Bool, Int) -> a -> String
shex Bool
shType Bool
shPre (Bool
signed, Int
size) a
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
suffix
  where specials :: [((Bool, Int, Integer), String)]
        specials :: [((Bool, Int, Integer), String)]
specials = [ ((Bool
True,  Int
8, Int8 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int8
forall a. Bounded a => a
minBound :: Int8)),  String
"INT8_MIN" )
                   , ((Bool
True, Int
16, Int16 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int16
forall a. Bounded a => a
minBound :: Int16)), String
"INT16_MIN")
                   , ((Bool
True, Int
32, Int32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32
forall a. Bounded a => a
minBound :: Int32)), String
"INT32_MIN")
                   , ((Bool
True, Int
64, Int64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int64
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
 = String
"-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. (Show a, Integral a) => a -> String
s16 (Integer -> Integer
forall a. Num a => a -> a
abs Integer
a)  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
 | Bool
True
 = String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. (Show a, Integral a) => a -> String
s16 Integer
a String -> String -> String
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 :: Bool -> Bool -> (Bool, Int) -> a -> String
sbin Bool
shType Bool
shPre (Bool
signed,Int
size) a
a
 | a
a a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0
 = String
"-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
size (Integer -> String
forall a. (Show a, Integral a) => a -> String
s2 (Integer -> Integer
forall a. Num a => a -> a
abs (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
a :: Integer)))  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
 | Bool
True
 = String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
size (a -> String
forall a. (Show a, Integral a) => a -> String
s2 a
a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
 where t :: String
t | Bool
shType = String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
signed then String
"Int" else String
"Word") String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
 = String
"-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. (Show a, Integral a) => a -> String
s2 (Integer -> Integer
forall a. Num a => a -> a
abs Integer
a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
 | Bool
True
 =  String
pre String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. (Show a, Integral a) => a -> String
s2 Integer
a String -> String -> String
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 = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
l Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) Char
'0' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

-- | Binary printer
s2 :: (Show a, Integral a) => a -> String
s2 :: a -> String
s2  a
v = a -> (Int -> Char) -> a -> String -> String
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 = Maybe Char -> Char
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Char -> Char) -> (Int -> Maybe Char) -> Int -> Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> [(Int, Char)] -> Maybe Char)
-> [(Int, Char)] -> Int -> Maybe Char
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> [(Int, Char)] -> Maybe Char
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 :: a -> String
s16 a
v = a -> String -> String
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 :: String -> a
readBin (Char
'-':String
s) = -(String -> a
forall a. Num a => String -> a
readBin String
s)
readBin String
s = case a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
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)]
_         -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"SBV.readBin: Cannot read a binary number from: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
s
  where cvt :: Char -> Int
cvt Char
c = Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0'
        isDigit :: Char -> Bool
isDigit = (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"01")
        s' :: String
s' | String
"0b" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
s = Int -> String -> String
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
   | Float -> Bool
forall a. RealFloat a => a -> Bool
isNaN Float
f             = String
"((float) NAN)"
   | Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f Float -> Float -> Bool
forall a. Ord a => a -> a -> Bool
< Float
0 = String
"((float) (-INFINITY))"
   | Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f        = String
"((float) INFINITY)"
   | Bool
True                = Float -> String -> String
forall a. RealFloat a => a -> String -> String
N.showHFloat Float
f (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"F /* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Float -> String
forall a. Show a => a -> String
show Float
f String -> String -> String
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
   | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
d             = String
"((double) NAN)"
   | Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0 = String
"((double) (-INFINITY))"
   | Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d        = String
"((double) INFINITY)"
   | Bool
True                = Double -> String -> String
forall a. RealFloat a => a -> String -> String
N.showHFloat Double
d String
" /* " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Double -> String
forall a. Show a => a -> String
show Double
d String -> String -> String
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
   | Float -> Bool
forall a. RealFloat a => a -> Bool
isNaN Float
f             = String
"((0/0) :: Float)"
   | Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f Float -> Float -> Bool
forall a. Ord a => a -> a -> Bool
< Float
0 = String
"((-1/0) :: Float)"
   | Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f        = String
"((1/0) :: Float)"
   | Bool
True                = Float -> String
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
   | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
d             = String
"((0/0) :: Double)"
   | Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0 = String
"((-1/0) :: Double)"
   | Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d        = String
"((1/0) :: Double)"
   | Bool
True                = Double -> String
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
   | Float -> Bool
forall a. RealFloat a => a -> Bool
isNaN Float
f             = String -> String
as String
"NaN"
   | Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f, Float
f Float -> Float -> Bool
forall a. Ord a => a -> a -> Bool
< Float
0 = String -> String
as String
"-oo"
   | Float -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Float
f        = String -> String
as String
"+oo"
   | Float -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero Float
f    = String -> String
as String
"-zero"
   | Float
f Float -> Float -> Bool
forall a. Eq a => a -> a -> Bool
== Float
0              = String -> String
as String
"+zero"
   | Bool
True                = String
"((_ to_fp 8 24) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RoundingMode -> String
smtRoundingMode RoundingMode
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
toSMTLibRational (Float -> Rational
forall a. Real a => a -> Rational
toRational Float
f) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
   where as :: String -> String
as String
s = String
"(_ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
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
   | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
d             = String -> String
as String
"NaN"
   | Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d, Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
0 = String -> String
as String
"-oo"
   | Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
d        = String -> String
as String
"+oo"
   | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero Double
d    = String -> String
as String
"-zero"
   | Double
d Double -> Double -> Bool
forall a. Eq a => a -> a -> Bool
== Double
0              = String -> String
as String
"+zero"
   | Bool
True                = String
"((_ to_fp 11 53) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RoundingMode -> String
smtRoundingMode RoundingMode
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Rational -> String
toSMTLibRational (Double -> Rational
forall a. Real a => a -> Rational
toRational Double
d) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
   where as :: String -> String
as String
s = String
"(_ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r) String -> String -> String
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0
   = String
"(- (/ "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Integer -> Integer
forall a. Num a => a -> a
abs Integer
n) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".0 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".0))"
   | Bool
True
   = String
"(/ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".0 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".0)"
  where n :: Integer
n = Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r
        d :: Integer
d = Rational -> Integer
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
  | CV -> Bool
forall a. HasKind a => a -> Bool
isBoolean       CV
x, CInteger  Integer
w      <- CV -> CVal
cvVal CV
x = if Integer
w Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then String
"false" else String
"true"
  | CV -> Bool
forall a. HasKind a => a -> Bool
isUserSort      CV
x, CUserSort (Maybe Int
_, String
s) <- CV -> CVal
cvVal CV
x = String -> String
roundModeConvert String
s
  | CV -> Bool
forall a. HasKind a => a -> Bool
isReal          CV
x, CAlgReal  AlgReal
r      <- CV -> CVal
cvVal CV
x = AlgReal -> String
algRealToSMTLib2 AlgReal
r
  | CV -> Bool
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
  | CV -> Bool
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
  | CV -> Bool
forall a. HasKind a => a -> Bool
isRational      CV
x, CRational Rational
r      <- CV -> CVal
cvVal CV
x = Rational -> String
showSMTRational Rational
r
  | CV -> Bool
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 (CV -> Bool
forall a. HasKind a => a -> Bool
isBounded CV
x), CInteger  Integer
w      <- CV -> CVal
cvVal CV
x = if Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Integer -> String
forall a. Show a => a -> String
show Integer
w else String
"(- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Integer -> Integer
forall a. Num a => a -> a
abs Integer
w) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  | Bool -> Bool
not (CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
x)  , CInteger  Integer
w      <- CV -> CVal
cvVal CV
x = Int -> Integer -> String
smtLibHex (CV -> Int
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
  | CV -> Bool
forall a. HasKind a => a -> Bool
hasSign CV
x        , CInteger  Integer
w      <- CV -> CVal
cvVal CV
x = if Integer
w Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Integer
forall a. Num a => a -> a
negate (Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
x)
                                                     then Int -> String
mkMinBound (CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
x)
                                                     else Bool -> String -> String
negIf (Integer
w Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0) (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> String
smtLibHex (CV -> Int
forall a. HasKind a => a -> Int
intSizeOf CV
x) (Integer -> Integer
forall a. Num a => a -> a
abs Integer
w)
  | CV -> Bool
forall a. HasKind a => a -> Bool
isChar CV
x         , CChar Char
c          <- CV -> CVal
cvVal CV
x = String
"(_ char " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Integer -> String
smtLibHex Int
8 (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
ord Char
c)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  | CV -> Bool
forall a. HasKind a => a -> Bool
isString CV
x       , CString String
s        <- CV -> CVal
cvVal CV
x = Char
'\"' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> String
stringToQFS String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""
  | CV -> Bool
forall a. HasKind a => a -> Bool
isList CV
x         , CList [CVal]
xs         <- CV -> CVal
cvVal CV
x = Kind -> [CVal] -> String
smtLibSeq (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) [CVal]
xs
  | CV -> Bool
forall a. HasKind a => a -> Bool
isSet CV
x          , CSet RCSet CVal
s           <- CV -> CVal
cvVal CV
x = Kind -> RCSet CVal -> String
smtLibSet (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) RCSet CVal
s
  | CV -> Bool
forall a. HasKind a => a -> Bool
isTuple CV
x        , CTuple [CVal]
xs        <- CV -> CVal
cvVal CV
x = Kind -> [CVal] -> String
smtLibTup (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) [CVal]
xs
  | CV -> Bool
forall a. HasKind a => a -> Bool
isMaybe CV
x        , CMaybe Maybe CVal
mc        <- CV -> CVal
cvVal CV
x = Kind -> Maybe CVal -> String
smtLibMaybe  (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) Maybe CVal
mc
  | CV -> Bool
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 (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x) Either CVal CVal
ec

  | Bool
True = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.cvtCV: Impossible happened: Kind/Value disagreement on: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, CV) -> String
forall a. Show a => a -> String
show (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x, CV
x)
  where roundModeConvert :: String -> String
roundModeConvert String
s = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
s ([String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe [RoundingMode -> String
smtRoundingMode RoundingMode
m | RoundingMode
m <- [RoundingMode
forall a. Bounded a => a
minBound .. RoundingMode
forall a. Bounded a => a
maxBound] :: [RoundingMode], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
m String -> String -> Bool
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
v
        smtLibHex Int
sz Integer
v
          | Int
sz Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
4 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = String
"#x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad (Int
sz Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
4) (Integer -> String -> String
forall a. (Integral a, Show a) => a -> String -> String
showHex Integer
v String
"")
          | Bool
True            = String
"#b" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
pad Int
sz (Integer -> String -> String
showBin Integer
v String
"")
           where showBin :: Integer -> String -> String
showBin = Integer -> (Int -> Char) -> Integer -> String -> String
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k String -> String -> String
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.++ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
es String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                      mkUnit :: String -> String
mkUnit String
inner = String
"(seq.unit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
inner String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                  in [String] -> String
mkSeq (String -> String
mkUnit (String -> String) -> (CVal -> String) -> CVal -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (CV -> String) -> (CVal -> CV) -> CVal -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
ek (CVal -> String) -> [CVal] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [CVal]
xs)
        smtLibSeq Kind
k [CVal]
_ = String -> String
forall a. HasCallStack => String -> a
error String
"SBV.cvToSMTLib: Impossible case (smtLibSeq), received kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
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 -> (CVal -> String -> String) -> String -> Set CVal -> String
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 -> (CVal -> String -> String) -> String -> Set CVal -> String
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
_       -> String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibSet), received kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k

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

                modify :: String -> CVal -> String -> String
modify String
how CVal
e String
s = String
"(store " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> CVal -> CV
CV Kind
ke CVal
e) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
how String -> String -> String
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Kind -> CVal -> String) -> [Kind] -> [CVal] -> [String]
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) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        smtLibTup Kind
k           [CVal]
_  = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibTup), received kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k

        dtConstructor :: String -> [String] -> Kind -> String
dtConstructor String
fld []   Kind
res =  String
"(as " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fld String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        dtConstructor String
fld [String]
args Kind
res = String
"((as " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fld String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
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
_         = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibMaybe), received kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
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
_         = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.cvToSMTLib: Impossible case (smtLibEither), received kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
iInt -> Int -> Int
forall 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]
_)            = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.mkSkolemZero: Unexpected user sort: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
mkSkolemZero RoundingMode
rm Kind
k                         = RoundingMode -> CV -> String
cvToSMTLib RoundingMode
rm (Kind -> Integer -> CV
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 :: a -> String -> String
showBFloat = Int -> a -> String -> String
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 :: Int -> a -> String -> String
showFloatAtBase Int
base a
input
  | Int
base Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2 = String -> String -> String
forall a. HasCallStack => String -> a
error (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"showFloatAtBase: Received invalid base (must be >= 2): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
base
  | Bool
True     = String -> String -> String
showString (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. RealFloat a => a -> String
fmt a
input
  where fmt :: a -> String
fmt a
x
         | a -> Bool
forall a. RealFloat a => a -> Bool
isNaN a
x                   = String
"NaN"
         | a -> Bool
forall a. RealFloat a => a -> Bool
isInfinite a
x              = (if a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 then String
"-" else String
"") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"Infinity"
         | a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 Bool -> Bool -> Bool
|| a -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero a
x = Char
'-' Char -> String -> String
forall a. a -> [a] -> [a]
: a -> String
forall a. RealFloat a => a -> String
cvt (-a
x)
         | Bool
True                      = a -> String
forall a. RealFloat a => a -> String
cvt a
x

        basePow2 :: Bool
basePow2 = Int
base Int -> Int -> Int
forall a. Bits a => a -> a -> a
.&. (Int
baseInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
        lg2Base :: Int
lg2Base  = Int -> Int
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<" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
">"

        powChar :: Char
powChar
          | Int
base Int -> Int -> Bool
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 Integer -> a -> ([Int], Int)
forall a. RealFloat a => Integer -> a -> ([Int], Int)
floatToDigits (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
base) a
x of
                  ([],   Int
e) -> (Int
0, [], Int
e Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
                  (Int
d:[Int]
ds, Int
e) -> (Int
d, [Int]
ds, Int
e Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

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

               shSigned :: a -> String
shSigned a
v
                | a
v a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0      =       a -> String
forall a. Show a => a -> String
show a
v
                | Bool
True       = Char
'+' Char -> String -> String
forall a. a -> [a] -> [a]
: a -> String
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
         | (Int -> Bool) -> t Int -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) t Int
digits = String
""
         | Bool
True              = String
"." String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int -> String) -> t Int -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> String
toDigit t Int
digits

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