    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Tools.GenTest
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Test generation from symbolic programs
    -----------------------------------------------------------------------------

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Tools.GenTest (
            -- * Test case generation
            genTest, TestVectors, getTestValues, renderTest, TestStyle(..)
            ) where

    import Data.Bits     (testBit)
    import Data.Char     (isAlpha, toUpper)
    import Data.Function (on)
    import Data.List     (intercalate, groupBy)
    import Data.Maybe    (fromMaybe)

    import Data.SBV.Core.AlgReals
    import Data.SBV.Core.Data

    import Data.SBV.Utils.PrettyNum

    import qualified Data.Foldable as F (toList)

    -- | Type of test vectors (abstract)
    newtype TestVectors = TV [([CV], [CV])]

    -- | Retrieve the test vectors for further processing. This function
    -- is useful in cases where 'renderTest' is not sufficient and custom
    -- output (or further preprocessing) is needed.
    getTestValues :: TestVectors -> [([CV], [CV])]
    getTestValues :: TestVectors -> [([CV], [CV])]
    getTestValues (TV vs :: [([CV], [CV])]
    vs) = [([CV], [CV])]
    vs

    -- | Generate a set of concrete test values from a symbolic program. The output
    -- can be rendered as test vectors in different languages as necessary. Use the
    -- function 'output' call to indicate what fields should be in the test result.
    -- (Also see 'constrain' for filtering acceptable test values.)
    genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors
    genTest :: Int -> Symbolic a -> IO TestVectors
    genTest n :: Int
    n m :: Symbolic a
    m = Int -> [([CV], [CV])] -> IO TestVectors
    gen 0 []
      where gen :: Int -> [([CV], [CV])] -> IO TestVectors
    gen i :: Int
    i sofar :: [([CV], [CV])]
    sofar
             | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n = TestVectors -> IO TestVectors
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TestVectors -> IO TestVectors) -> TestVectors -> IO TestVectors
    forall a b. (a -> b) -> a -> b
    $ [([CV], [CV])] -> TestVectors
    TV ([([CV], [CV])] -> TestVectors) -> [([CV], [CV])] -> TestVectors
    forall a b. (a -> b) -> a -> b
    $ [([CV], [CV])] -> [([CV], [CV])]
    forall a. [a] -> [a]
    reverse [([CV], [CV])]
    sofar
             | Bool
    True   = do ([CV], [CV])
    t <- IO ([CV], [CV])
    tc
                           Int -> [([CV], [CV])] -> IO TestVectors
    gen (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +1) (([CV], [CV])
    t([CV], [CV]) -> [([CV], [CV])] -> [([CV], [CV])]
    forall a. a -> [a] -> [a]
    :[([CV], [CV])]
    sofar)
            tc :: IO ([CV], [CV])
    tc = do (_, Result {resTraces :: Result -> [(String, CV)]
    resTraces=[(String, CV)]
    tvals, resConsts :: Result -> [(SV, CV)]
    resConsts=[(SV, CV)]
    cs, resConstraints :: Result -> Seq (Bool, [(String, String)], SV)
    resConstraints=Seq (Bool, [(String, String)], SV)
    cstrs, resOutputs :: Result -> [SV]
    resOutputs=[SV]
    os}) <- SBVRunMode -> Symbolic a -> IO (a, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)]) -> SBVRunMode
    Concrete Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)])
    forall a. Maybe a
    Nothing) (Symbolic a
    m Symbolic a -> (a -> Symbolic a) -> Symbolic a
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= a -> Symbolic a
    forall a (m :: * -> *).
    (Outputtable a, MonadSymbolic m) =>
    a -> m a
    output)
                    let cval :: SV -> CV
    cval = CV -> Maybe CV -> CV
    forall a. a -> Maybe a -> a
    fromMaybe (String -> CV
    forall a. HasCallStack => String -> a
    error "Cannot generate tests in the presence of uninterpeted constants!") (Maybe CV -> CV) -> (SV -> Maybe CV) -> SV -> CV
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (SV -> [(SV, CV)] -> Maybe CV
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(SV, CV)]
    cs)
                        cond :: Bool
    cond = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and [CV -> Bool
    cvToBool (SV -> CV
    cval SV
    v) | (False, _, v :: SV
    v) <- Seq (Bool, [(String, String)], SV)
    -> [(Bool, [(String, String)], SV)]
    forall (t :: * -> *) a. Foldable t => t a -> [a]
    F.toList Seq (Bool, [(String, String)], SV)
    cstrs] -- Only pick-up "hard" constraints, as indicated by False in the fist component
                    if Bool
    cond
                       then ([CV], [CV]) -> IO ([CV], [CV])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (((String, CV) -> CV) -> [(String, CV)] -> [CV]
    forall a b. (a -> b) -> [a] -> [b]
    map (String, CV) -> CV
    forall a b. (a, b) -> b
    snd [(String, CV)]
    tvals, (SV -> CV) -> [SV] -> [CV]
    forall a b. (a -> b) -> [a] -> [b]
    map SV -> CV
    cval [SV]
    os)
                       else IO ([CV], [CV])
    tc   -- try again, with the same set of constraints

    -- | Test output style
    data TestStyle = Haskell String                     -- ^ As a Haskell value with given name
                   | C       String                     -- ^ As a C array of structs with given name
                   | Forte   String Bool ([Int], [Int]) -- ^ As a Forte/Verilog value with given name.
                                                        -- If the boolean is True then vectors are blasted big-endian, otherwise little-endian
                                                        -- The indices are the split points on bit-vectors for input and output values

    -- | Render the test as a Haskell value with the given name @n@.
    renderTest :: TestStyle -> TestVectors -> String
    renderTest :: TestStyle -> TestVectors -> String
    renderTest (Haskell n :: String
    n)    (TV vs :: [([CV], [CV])]
    vs) = String -> [([CV], [CV])] -> String
    haskell String
    n [([CV], [CV])]
    vs
    renderTest (C n :: String
    n)          (TV vs :: [([CV], [CV])]
    vs) = String -> [([CV], [CV])] -> String
    c       String
    n [([CV], [CV])]
    vs
    renderTest (Forte n :: String
    n b :: Bool
    b ss :: ([Int], [Int])
    ss) (TV vs :: [([CV], [CV])]
    vs) = String -> Bool -> ([Int], [Int]) -> [([CV], [CV])] -> String
    forte   String
    n Bool
    b ([Int], [Int])
    ss [([CV], [CV])]
    vs

    haskell :: String -> [([CV], [CV])] -> String
    haskell :: String -> [([CV], [CV])] -> String
    haskell vname :: String
    vname vs :: [([CV], [CV])]
    vs = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [ "-- Automatically generated by SBV. Do not edit!"
                                          , ""
                                          , "module " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    modName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ") where"
                                          , ""
                                          ]
                                       [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String]
    imports
                                       [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " :: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [([CV], [CV])] -> String
    forall a a.
    (HasKind a, HasKind a, Show a, Show a) =>
    [([a], [a])] -> String
    getType [([CV], [CV])]
    vs
                                          , String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " = [ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ("\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    pad String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++  ", ") ((([CV], [CV]) -> String) -> [([CV], [CV])] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ([CV], [CV]) -> String
    mkLine [([CV], [CV])]
    vs), String
    pad String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "]"
                                          ]
      where n :: String
    n | String -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    vname                 = "testVectors"
              | Bool -> Bool
    not (Char -> Bool
    isAlpha (String -> Char
    forall a. [a] -> a
    head String
    vname)) = "tv" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    vname
              | Bool
    True                       = String
    vname
            imports :: [String]
    imports
              | [([CV], [CV])] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([CV], [CV])]
    vs               = []
              | Bool
    needsInt Bool -> Bool -> Bool
    && Bool
    needsWord = ["import Data.Int", "import Data.Word", ""]
              | Bool
    needsInt              = ["import Data.Int", ""]
              | Bool
    needsWord             = ["import Data.Word", ""]
              | Bool
    needsRatio            = ["import Data.Ratio"]
              | Bool
    True                  = []
              where ((is :: [CV]
    is, os :: [CV]
    os):_) = [([CV], [CV])]
    vs
                    params :: [CV]
    params       = [CV]
    is [CV] -> [CV] -> [CV]
    forall a. [a] -> [a] -> [a]
    ++ [CV]
    os
                    needsInt :: Bool
    needsInt     = (CV -> Bool) -> [CV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any CV -> Bool
    forall a. HasKind a => a -> Bool
    isSW [CV]
    params
                    needsWord :: Bool
    needsWord    = (CV -> Bool) -> [CV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any CV -> Bool
    forall a. HasKind a => a -> Bool
    isUW [CV]
    params
                    needsRatio :: Bool
    needsRatio   = (CV -> Bool) -> [CV] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any CV -> Bool
    forall a. HasKind a => a -> Bool
    isR [CV]
    params
                    isR :: a -> Bool
    isR cv :: a
    cv       = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                                     KReal -> Bool
    True
                                     _     -> Bool
    False
                    isSW :: a -> Bool
    isSW cv :: a
    cv      = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                                     KBounded True _ -> Bool
    True
                                     _               -> Bool
    False
                    isUW :: a -> Bool
    isUW cv :: a
    cv      = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                                     KBounded False sz :: Int
    sz -> Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > 1
                                     _                 -> Bool
    False
            modName :: String
    modName = let (f :: Char
    f:r :: String
    r) = String
    n in Char -> Char
    toUpper Char
    f Char -> String -> String
    forall a. a -> [a] -> [a]
    : String
    r
            pad :: String
    pad = Int -> Char -> String
    forall a. Int -> a -> [a]
    replicate (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + 3) ' '
            getType :: [([a], [a])] -> String
    getType []         = "[a]"
            getType ((i :: [a]
    i, o :: [a]
    o):_) = "[(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([a] -> String) -> [a] -> String
    forall a. HasKind a => ([a] -> String) -> [a] -> String
    mapType [a] -> String
    forall a. (HasKind a, Show a) => [a] -> String
    typeOf [a]
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ", " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([a] -> String) -> [a] -> String
    forall a. HasKind a => ([a] -> String) -> [a] -> String
    mapType [a] -> String
    forall a. (HasKind a, Show a) => [a] -> String
    typeOf [a]
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")]"
            mkLine :: ([CV], [CV]) -> String
    mkLine  (i :: [CV]
    i, o :: [CV]
    o)     = "("  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([CV] -> String) -> [CV] -> String
    forall a. HasKind a => ([a] -> String) -> [a] -> String
    mapType [CV] -> String
    valOf  [CV]
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ", " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ([CV] -> String) -> [CV] -> String
    forall a. HasKind a => ([a] -> String) -> [a] -> String
    mapType [CV] -> String
    valOf  [CV]
    o String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            mapType :: ([a] -> String) -> [a] -> String
    mapType f :: [a] -> String
    f cvs :: [a]
    cvs = [String] -> String
    mkTuple ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ ([a] -> String) -> [[a]] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map [a] -> String
    f ([[a]] -> [String]) -> [[a]] -> [String]
    forall a b. (a -> b) -> a -> b
    $ (a -> a -> Bool) -> [a] -> [[a]]
    forall a. (a -> a -> Bool) -> [a] -> [[a]]
    groupBy (Kind -> Kind -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Kind -> Kind -> Bool) -> (a -> Kind) -> a -> a -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf) [a]
    cvs
            mkTuple :: [String] -> String
    mkTuple [x :: String
    x] = String
    x
            mkTuple xs :: [String]
    xs  = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            typeOf :: [a] -> String
    typeOf []    = "()"
            typeOf [x :: a
    x]   = a -> String
    forall a. (HasKind a, Show a) => a -> String
    t a
    x
            typeOf (x :: a
    x:_) = "[" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. (HasKind a, Show a) => a -> String
    t a
    x String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "]"
            valOf :: [CV] -> String
    valOf  []    = "()"
            valOf  [x :: CV
    x]   = CV -> String
    s CV
    x
            valOf  xs :: [CV]
    xs    = "[" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " ((CV -> String) -> [CV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map CV -> String
    s [CV]
    xs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "]"

            t :: a -> String
    t cv :: a
    cv = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                     KBool               -> "Bool"
                     KBounded False 8    -> "Word8"
                     KBounded False 16   -> "Word16"
                     KBounded False 32   -> "Word32"
                     KBounded False 64   -> "Word64"
                     KBounded True  8    -> "Int8"
                     KBounded True  16   -> "Int16"
                     KBounded True  32   -> "Int32"
                     KBounded True  64   -> "Int64"
                     KUnbounded          -> "Integer"
                     KFloat              -> "Float"
                     KDouble             -> "Double"
                     KChar               -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported char"
                     KString             -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported string"
                     KReal               -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported real valued test value: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    cv
                     KList es :: Kind
    es            -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported list valued test: [" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    es String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "]"
                     KSet  es :: Kind
    es            -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported set valued test: {" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    es String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "}"
                     KUninterpreted us :: String
    us _ -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported uninterpreted sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    us
                     _                   -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unexpected CV: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    cv

            s :: CV -> String
    s cv :: CV
    cv = case CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    cv of
                      KBool               -> Int -> String -> String
    forall a. Int -> [a] -> [a]
    take 5 (Bool -> String
    forall a. Show a => a -> String
    show (CV -> Bool
    cvToBool CV
    cv) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Char -> String
    forall a. a -> [a]
    repeat ' ')
                      KBounded sgn :: Bool
    sgn   sz :: Int
    sz   -> let CInteger w :: Integer
    w = 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 (Bool
    sgn, Int
    sz) Integer
    w
                      KUnbounded          -> let CInteger w :: Integer
    w = CV -> CVal
    cvVal CV
    cv in Bool -> Bool -> Integer -> String
    shexI Bool
    False Bool
    True           Integer
    w
                      KFloat              -> let CFloat   w :: Float
    w = CV -> CVal
    cvVal CV
    cv in Float -> String
    showHFloat Float
    w
                      KDouble             -> let CDouble  w :: Double
    w = CV -> CVal
    cvVal CV
    cv in Double -> String
    showHDouble Double
    w
                      KChar               -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported char"
                      KString             -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported string"
                      KReal               -> let CAlgReal w :: AlgReal
    w = CV -> CVal
    cvVal CV
    cv in AlgReal -> String
    algRealToHaskell AlgReal
    w
                      KList es :: Kind
    es            -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported list valued sort: [" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    es String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "]"
                      KSet  es :: Kind
    es            -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported set valued sort: {" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    es String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "}"
                      KUninterpreted us :: String
    us _ -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported uninterpreted sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    us
                      k :: Kind
    k@KTuple{}          -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported tuple: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                      k :: Kind
    k@KMaybe{}          -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported maybe: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                      k :: Kind
    k@KEither{}         -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported sum: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k

    c :: String -> [([CV], [CV])] -> String
    c :: String -> [([CV], [CV])] -> String
    c n :: String
    n vs :: [([CV], [CV])]
    vs = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $
                  [ "/* Automatically generated by SBV. Do not edit! */"
                  , ""
                  , "#include <stdio.h>"
                  , "#include <inttypes.h>"
                  , "#include <stdint.h>"
                  , "#include <stdbool.h>"
                  , "#include <string.h>"
                  , "#include <math.h>"
                  , ""
                  , "/* The boolean type */"
                  , "typedef bool SBool;"
                  , ""
                  , "/* The float type */"
                  , "typedef float SFloat;"
                  , ""
                  , "/* The double type */"
                  , "typedef double SDouble;"
                  , ""
                  , "/* Unsigned bit-vectors */"
                  , "typedef uint8_t  SWord8;"
                  , "typedef uint16_t SWord16;"
                  , "typedef uint32_t SWord32;"
                  , "typedef uint64_t SWord64;"
                  , ""
                  , "/* Signed bit-vectors */"
                  , "typedef int8_t  SInt8;"
                  , "typedef int16_t SInt16;"
                  , "typedef int32_t SInt32;"
                  , "typedef int64_t SInt64;"
                  , ""
                  , "typedef struct {"
                  , "  struct {"
                  ]
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (if [([CV], [CV])] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([CV], [CV])]
    vs then [] else (CV -> Int -> String) -> [CV] -> [Int] -> [String]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (String -> CV -> Int -> String
    forall a a. (Show a, HasKind a) => String -> a -> a -> String
    mkField "i") (([CV], [CV]) -> [CV]
    forall a b. (a, b) -> a
    fst ([([CV], [CV])] -> ([CV], [CV])
    forall a. [a] -> a
    head [([CV], [CV])]
    vs)) [(0::Int)..])
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "  } input;"
                  , "  struct {"
                  ]
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (if [([CV], [CV])] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([CV], [CV])]
    vs then [] else (CV -> Int -> String) -> [CV] -> [Int] -> [String]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (String -> CV -> Int -> String
    forall a a. (Show a, HasKind a) => String -> a -> a -> String
    mkField "o") (([CV], [CV]) -> [CV]
    forall a b. (a, b) -> b
    snd ([([CV], [CV])] -> ([CV], [CV])
    forall a. [a] -> a
    head [([CV], [CV])]
    vs)) [(0::Int)..])
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "  } output;"
                  , "} " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "TestVector;"
                  , ""
                  , String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "TestVector " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "[] = {"
                  ]
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ ["      " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n    , " ((([CV], [CV]) -> String) -> [([CV], [CV])] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ([CV], [CV]) -> String
    mkLine [([CV], [CV])]
    vs)]
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "};"
                  , ""
                  , "int " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "Length = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show ([([CV], [CV])] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [([CV], [CV])]
    vs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ";"
                  , ""
                  , "/* Stub driver showing the test values, replace with code that uses the test vectors. */"
                  , "int main(void)"
                  , "{"
                  , "  int i;"
                  , "  for(i = 0; i < " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "Length; ++i)"
                  , "  {"
                  , "    " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    outLine
                  , "  }"
                  , ""
                  , "  return 0;"
                  , "}"
                  ]
      where mkField :: String -> a -> a -> String
    mkField p :: String
    p cv :: a
    cv i :: a
    i = "    " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    p 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]
    ++ ";"
                where t :: String
    t = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                            KBool               -> "SBool"
                            KBounded False 8    -> "SWord8"
                            KBounded False 16   -> "SWord16"
                            KBounded False 32   -> "SWord32"
                            KBounded False 64   -> "SWord64"
                            KBounded True  8    -> "SInt8"
                            KBounded True  16   -> "SInt16"
                            KBounded True  32   -> "SInt32"
                            KBounded True  64   -> "SInt64"
                            k :: Kind
    k@KBounded{}        -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                            KFloat              -> "SFloat"
                            KDouble             -> "SDouble"
                            KChar               -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported char"
                            KString             -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported string"
                            KUnbounded          -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unbounded integers are not supported when generating C test-cases."
                            KReal               -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Real values are not supported when generating C test-cases."
                            KUninterpreted us :: String
    us _ -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported uninterpreted sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    us
                            k :: Kind
    k@KList{}           -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported list sort: "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                            k :: Kind
    k@KSet{}            -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported set sort: "   String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                            k :: Kind
    k@KTuple{}          -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported tuple sort: "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                            k :: Kind
    k@KMaybe{}          -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported maybe sort: "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                            k :: Kind
    k@KEither{}         -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported either sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k

            mkLine :: ([CV], [CV]) -> String
    mkLine (is :: [CV]
    is, os :: [CV]
    os) = "{{" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " ((CV -> String) -> [CV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map CV -> String
    v [CV]
    is) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "}, {" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " ((CV -> String) -> [CV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map CV -> String
    v [CV]
    os) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "}}"

            v :: CV -> String
    v cv :: CV
    cv = case CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    cv of
                      KBool               -> if CV -> Bool
    cvToBool CV
    cv then "true " else "false"
                      KBounded sgn :: Bool
    sgn sz :: Int
    sz     -> let CInteger w :: Integer
    w = CV -> CVal
    cvVal CV
    cv in Bool -> Bool -> (Bool, Int) -> Integer -> String
    forall a.
    (Show a, Integral a) =>
    Bool -> Bool -> (Bool, Int) -> a -> String
    chex  Bool
    False Bool
    True (Bool
    sgn, Int
    sz) Integer
    w
                      KUnbounded          -> let CInteger w :: Integer
    w = CV -> CVal
    cvVal CV
    cv in Bool -> Bool -> Integer -> String
    shexI Bool
    False Bool
    True           Integer
    w
                      KFloat              -> let CFloat w :: Float
    w   = CV -> CVal
    cvVal CV
    cv in Float -> String
    showCFloat Float
    w
                      KDouble             -> let CDouble w :: Double
    w  = CV -> CVal
    cvVal CV
    cv in Double -> String
    showCDouble Double
    w
                      KChar               -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported char"
                      KString             -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported string"
                      k :: Kind
    k@KList{}           -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported list sort!" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                      k :: Kind
    k@KSet{}            -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported set sort!" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                      KUninterpreted us :: String
    us _ -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported uninterpreted sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    us
                      KReal               -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Real values are not supported when generating C test-cases."
                      k :: Kind
    k@KTuple{}          -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported tuple sort!" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                      k :: Kind
    k@KMaybe{}          -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported maybe sort!" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                      k :: Kind
    k@KEither{}         -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unsupported sum sort!" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k

            outLine :: String
    outLine
              | [([CV], [CV])] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([CV], [CV])]
    vs = "printf(\"\");"
              | Bool
    True    = "printf(\"%*d. " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fmtString String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "\\n\", " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Int -> String
    forall a. Show a => a -> String
    show ([([CV], [CV])] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [([CV], [CV])]
    vs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - 1))) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ", i"
                        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (String -> String) -> [String] -> String
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap ("\n           , " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ) ((CV -> Int -> String) -> [CV] -> [Int] -> [String]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith CV -> Int -> String
    forall a a. (HasKind a, Show a) => a -> a -> String
    inp [CV]
    is [(0::Int)..] [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (CV -> Int -> String) -> [CV] -> [Int] -> [String]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith CV -> Int -> String
    forall a a. (HasKind a, Show a) => a -> a -> String
    out [CV]
    os [(0::Int)..])
                        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ");"
              where (is :: [CV]
    is, os :: [CV]
    os) = [([CV], [CV])] -> ([CV], [CV])
    forall a. [a] -> a
    head [([CV], [CV])]
    vs
                    inp :: a -> a -> String
    inp cv :: a
    cv i :: a
    i = a -> String -> String
    forall a. HasKind a => a -> String -> String
    mkBool a
    cv (String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "[i].input.i"  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i)
                    out :: a -> a -> String
    out cv :: a
    cv i :: a
    i = a -> String -> String
    forall a. HasKind a => a -> String -> String
    mkBool a
    cv (String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "[i].output.o" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    i)
                    mkBool :: a -> String -> String
    mkBool cv :: a
    cv s :: String
    s = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                                    KBool -> "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " == true) ? \"true \" : \"false\""
                                    _     -> String
    s
                    fmtString :: String
    fmtString = [String] -> String
    unwords ((CV -> String) -> [CV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map CV -> String
    forall a. (HasKind a, Show a) => a -> String
    fmt [CV]
    is) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " -> " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    unwords ((CV -> String) -> [CV] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map CV -> String
    forall a. (HasKind a, Show a) => a -> String
    fmt [CV]
    os)

            fmt :: a -> String
    fmt cv :: a
    cv = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                        KBool             -> "%s"
                        KBounded False  8 -> "0x%02\"PRIx8\""
                        KBounded False 16 -> "0x%04\"PRIx16\"U"
                        KBounded False 32 -> "0x%08\"PRIx32\"UL"
                        KBounded False 64 -> "0x%016\"PRIx64\"ULL"
                        KBounded True   8 -> "%\"PRId8\""
                        KBounded True  16 -> "%\"PRId16\""
                        KBounded True  32 -> "%\"PRId32\"L"
                        KBounded True  64 -> "%\"PRId64\"LL"
                        KFloat            -> "%f"
                        KDouble           -> "%f"
                        KChar             -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported char"
                        KString           -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported string"
                        KUnbounded        -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported unbounded integers for C generation."
                        KReal             -> String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: Unsupported real valued values for C generation."
                        _                 -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unexpected CV: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show a
    cv

    forte :: String -> Bool -> ([Int], [Int]) -> [([CV], [CV])] -> String
    forte :: String -> Bool -> ([Int], [Int]) -> [([CV], [CV])] -> String
    forte vname :: String
    vname bigEndian :: Bool
    bigEndian ss :: ([Int], [Int])
    ss vs :: [([CV], [CV])]
    vs = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [ "// Automatically generated by SBV. Do not edit!"
                                                 , "let " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " ="
                                                 , "   let c s = val [_, r] = str_split s \"'\" in " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    blaster
                                                 ]
                                              [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ "   in [ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate "\n      , " ((([CV], [CV]) -> String) -> [([CV], [CV])] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map ([CV], [CV]) -> String
    forall (t :: * -> *) (t :: * -> *).
    (Foldable t, Foldable t) =>
    (t CV, t CV) -> String
    mkLine [([CV], [CV])]
    vs)
                                                 , "      ];"
                                                 ]
      where n :: String
    n | String -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    vname                 = "testVectors"
              | Bool -> Bool
    not (Char -> Bool
    isAlpha (String -> Char
    forall a. [a] -> a
    head String
    vname)) = "tv" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    vname
              | Bool
    True                       = String
    vname
            blaster :: String
    blaster
             | Bool
    bigEndian = "map (\\s. s == \"1\") (explode (string_tl r))"
             | Bool
    True      = "rev (map (\\s. s == \"1\") (explode (string_tl r)))"
            toF :: Bool -> Char
    toF True  = '1'
            toF False = '0'
            blast :: CV -> String
    blast cv :: CV
    cv = let noForte :: String -> String
    noForte w :: String
    w = String -> String
    forall a. HasCallStack => String -> a
    error "SBV.renderTest: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    w String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " values are not supported when generating Forte test-cases."
                       in case CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    cv of
                            KBool              -> [Bool -> Char
    toF (CV -> Bool
    cvToBool CV
    cv)]
                            KBounded False 8   -> Int -> CVal -> String
    xlt  8 (CV -> CVal
    cvVal CV
    cv)
                            KBounded False 16  -> Int -> CVal -> String
    xlt 16 (CV -> CVal
    cvVal CV
    cv)
                            KBounded False 32  -> Int -> CVal -> String
    xlt 32 (CV -> CVal
    cvVal CV
    cv)
                            KBounded False 64  -> Int -> CVal -> String
    xlt 64 (CV -> CVal
    cvVal CV
    cv)
                            KBounded True 8    -> Int -> CVal -> String
    xlt  8 (CV -> CVal
    cvVal CV
    cv)
                            KBounded True 16   -> Int -> CVal -> String
    xlt 16 (CV -> CVal
    cvVal CV
    cv)
                            KBounded True 32   -> Int -> CVal -> String
    xlt 32 (CV -> CVal
    cvVal CV
    cv)
                            KBounded True 64   -> Int -> CVal -> String
    xlt 64 (CV -> CVal
    cvVal CV
    cv)
                            KFloat             -> String -> String
    noForte "Float"
                            KDouble            -> String -> String
    noForte "Double"
                            KChar              -> String -> String
    noForte "Char"
                            KString            -> String -> String
    noForte "String"
                            KReal              -> String -> String
    noForte "Real"
                            KList ek :: Kind
    ek           -> String -> String
    noForte (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "List of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek
                            KSet  ek :: Kind
    ek           -> String -> String
    noForte (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "Set of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek
                            KUnbounded         -> String -> String
    noForte "Unbounded integers"
                            KUninterpreted s :: String
    s _ -> String -> String
    noForte (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "Uninterpreted kind " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    s
                            _                  -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Unexpected CV: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ CV -> String
    forall a. Show a => a -> String
    show CV
    cv

            xlt :: Int -> CVal -> String
    xlt s :: Int
    s (CInteger  v :: Integer
    v)  = [Bool -> Char
    toF (Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    testBit Integer
    v Int
    i) | Int
    i <- [Int
    sInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1, Int
    sInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -2 .. 0]]
            xlt _ (CFloat    r :: Float
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest.Forte: Unexpected float value: "         String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Float -> String
    forall a. Show a => a -> String
    show Float
    r
            xlt _ (CDouble   r :: Double
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest.Forte: Unexpected double value: "        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Double -> String
    forall a. Show a => a -> String
    show Double
    r
            xlt _ (CChar     r :: Char
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest.Forte: Unexpected char value: "          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Char -> String
    forall a. Show a => a -> String
    show Char
    r
            xlt _ (CString   r :: String
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest.Forte: Unexpected string value: "        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    r
            xlt _ (CAlgReal  r :: AlgReal
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest.Forte: Unexpected real value: "          String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ AlgReal -> String
    forall a. Show a => a -> String
    show AlgReal
    r
            xlt _ CList{}        = String -> String
    forall a. HasCallStack => String -> a
    error   "SBV.renderTest.Forte: Unexpected list value!"
            xlt _ CSet{}         = String -> String
    forall a. HasCallStack => String -> a
    error   "SBV.renderTest.Forte: Unexpected set value!"
            xlt _ CTuple{}       = String -> String
    forall a. HasCallStack => String -> a
    error   "SBV.renderTest.Forte: Unexpected list value!"
            xlt _ CMaybe{}       = String -> String
    forall a. HasCallStack => String -> a
    error   "SBV.renderTest.Forte: Unexpected maybe value!"
            xlt _ CEither{}      = String -> String
    forall a. HasCallStack => String -> a
    error   "SBV.renderTest.Forte: Unexpected sum value!"
            xlt _ (CUserSort r :: (Maybe Int, String)
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest.Forte: Unexpected uninterpreted value: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ (Maybe Int, String) -> String
    forall a. Show a => a -> String
    show (Maybe Int, String)
    r

            mkLine :: (t CV, t CV) -> String
    mkLine  (i :: t CV
    i, o :: t CV
    o) = "("  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    mkTuple ([Int] -> String -> [String]
    form (([Int], [Int]) -> [Int]
    forall a b. (a, b) -> a
    fst ([Int], [Int])
    ss) ((CV -> String) -> t CV -> String
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap CV -> String
    blast t CV
    i)) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ", " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ [String] -> String
    mkTuple ([Int] -> String -> [String]
    form (([Int], [Int]) -> [Int]
    forall a b. (a, b) -> b
    snd ([Int], [Int])
    ss) ((CV -> String) -> t CV -> String
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap CV -> String
    blast t CV
    o)) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            mkTuple :: [String] -> String
    mkTuple []  = "()"
            mkTuple [x :: String
    x] = String
    x
            mkTuple xs :: [String]
    xs  = "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate ", " [String]
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ ")"
            form :: [Int] -> String -> [String]
    form []     [] = []
            form []     bs :: String
    bs = String -> [String]
    forall a. HasCallStack => String -> a
    error (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Mismatched index in stream, extra " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    bs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " bit(s) remain."
            form (i :: Int
    i:is :: [Int]
    is) bs :: String
    bs
              | String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    bs Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    i = String -> [String]
    forall a. HasCallStack => String -> a
    error (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ "SBV.renderTest: Mismatched index in stream, was looking for " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " bit(s), but only " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    bs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ " remains."
              | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1        = let b :: Char
    b:r :: String
    r = String
    bs
                                    v :: String
    v   = if Char
    b Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '1' then "T" else "F"
                                in String
    v String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [Int] -> String -> [String]
    form [Int]
    is String
    r
              | Bool
    True          = let (f :: String
    f, r :: String
    r) = Int -> String -> (String, String)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    i String
    bs
                                    v :: String
    v      = "c \"" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    i String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ "'b" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    f String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\""
                                in String
    v String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [Int] -> String -> [String]
    form [Int]
    is String
    r