    -----------------------------------------------------------------------------
    -- |
    -- 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
          , 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 :: forall a. HasKind a => 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 :: 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 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 :: 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, 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 :: 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 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 a. [a] -> 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 :: forall a. (Show a, Integral a) => a -> String
    s2  a
    v = a -> (Int -> Char) -> a -> String -> String
    forall a. Integral 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 :: forall a. (Show a, Integral a) => a -> String
    s16 a
    v = a -> String -> String
    forall a. Integral 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) = -(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 a. Eq a => a -> [a] -> 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 => 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 => 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 a. [a] -> 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'

    -- | Show a float as a binary
    showBFloat :: (Show a, RealFloat a) => a -> ShowS
    showBFloat :: forall a. (Show a, RealFloat a) => 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 :: forall a. (Show a, RealFloat a) => 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 :: forall a. (Show a, Num a, Ord a) => 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