    -----------------------------------------------------------------------------
    -- |
    -- 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 -Wno-incomplete-uni-patterns #-}

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

    import Control.Monad (unless)

    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 Data.SBV.Provers.Prover(defaultSMTCfg)

    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 [([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 :: forall a. Outputtable a => Int -> Symbolic a -> IO TestVectors
    genTest Int
    n Symbolic a
    m = Int -> [([CV], [CV])] -> IO TestVectors
    gen Int
    0 []
      where gen :: Int -> [([CV], [CV])] -> IO TestVectors
    gen Int
    i [([CV], [CV])]
    sofar
             | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    n = TestVectors -> IO TestVectors
    forall a. a -> IO a
    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
    +Int
    1) (([CV], [CV])
    t([CV], [CV]) -> [([CV], [CV])] -> [([CV], [CV])]
    forall a. a -> [a] -> [a]
    :[([CV], [CV])]
    sofar)
            tc :: IO ([CV], [CV])
    tc = do (a
    _, Result {resTraces :: Result -> [(String, CV)]
    resTraces=[(String, CV)]
    tvals, resConsts :: Result -> (CnstMap, [(SV, CV)])
    resConsts=(CnstMap
    _, [(SV, CV)]
    cs), resDefinitions :: Result -> [SMTDef]
    resDefinitions=[SMTDef]
    definitions, resConstraints :: Result -> Seq (Bool, [(String, String)], SV)
    resConstraints=Seq (Bool, [(String, String)], SV)
    cstrs, resOutputs :: Result -> [SV]
    resOutputs=[SV]
    os}) <- SMTConfig -> SBVRunMode -> Symbolic a -> IO (a, Result)
    forall (m :: * -> *) a.
    MonadIO m =>
    SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
    runSymbolic SMTConfig
    defaultSMTCfg (Maybe (Bool, [(NamedSymVar, CV)]) -> SBVRunMode
    Concrete Maybe (Bool, [(NamedSymVar, CV)])
    forall a. Maybe a
    Nothing) (Symbolic a
    m Symbolic a -> (a -> Symbolic a) -> Symbolic a
    forall a b.
    SymbolicT IO a -> (a -> SymbolicT IO b) -> SymbolicT IO b
    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
    forall (m :: * -> *). 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 String
    "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) | (Bool
    False, [(String, String)]
    _, SV
    v) <- Seq (Bool, [(String, String)], SV)
    -> [(Bool, [(String, String)], SV)]
    forall a. Seq a -> [a]
    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
                    Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([SMTDef] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [SMTDef]
    definitions) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    forall a. HasCallStack => String -> a
    error String
    "Cannot generate tests in the presence of 'smtFunction' calls!"
                    if Bool
    cond
                       then ([CV], [CV]) -> IO ([CV], [CV])
    forall a. a -> IO a
    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 String
    n)    (TV [([CV], [CV])]
    vs) = String -> [([CV], [CV])] -> String
    haskell String
    n [([CV], [CV])]
    vs
    renderTest (C String
    n)          (TV [([CV], [CV])]
    vs) = String -> [([CV], [CV])] -> String
    c       String
    n [([CV], [CV])]
    vs
    renderTest (Forte String
    n Bool
    b ([Int], [Int])
    ss) (TV [([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 String
    vname [([CV], [CV])]
    vs = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [ String
    "-- Automatically generated by SBV. Do not edit!"
                                          , String
    ""
                                          , String
    "module " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    modName String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ") where"
                                          , String
    ""
                                          ]
                                       [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 -> 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 -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate (String
    "\n" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    pad String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++  String
    ", ") ((([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]
    ++ String
    "]"
                                          ]
      where n :: String
    n | String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    vname                 = String
    "testVectors"
              | Bool -> Bool
    not (Char -> Bool
    isAlpha (String -> Char
    forall a. HasCallStack => [a] -> a
    head String
    vname)) = String
    "tv" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    vname
              | Bool
    True                       = String
    vname
            imports :: [String]
    imports
              | [([CV], [CV])] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([CV], [CV])]
    vs               = []
              | Bool
    needsInt Bool -> Bool -> Bool
    && Bool
    needsWord = [String
    "import Data.Int", String
    "import Data.Word", String
    ""]
              | Bool
    needsInt              = [String
    "import Data.Int", String
    ""]
              | Bool
    needsWord             = [String
    "import Data.Word", String
    ""]
              | Bool
    needsRatio            = [String
    "import Data.Ratio"]
              | Bool
    True                  = []
              where (([CV]
    is, [CV]
    os):[([CV], [CV])]
    _) = [([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 a
    cv       = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                                     Kind
    KReal -> Bool
    True
                                     Kind
    _     -> Bool
    False
                    isSW :: a -> Bool
    isSW a
    cv      = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                                     KBounded Bool
    True Int
    _ -> Bool
    True
                                     Kind
    _               -> Bool
    False
                    isUW :: a -> Bool
    isUW a
    cv      = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                                     KBounded Bool
    False Int
    sz -> Int
    sz Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    1
                                     Kind
    _                 -> Bool
    False
            modName :: String
    modName = let (Char
    f: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 a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    3) Char
    ' '
            getType :: [([a], [a])] -> String
    getType []         = String
    "[a]"
            getType (([a]
    i, [a]
    o):[([a], [a])]
    _) = String
    "[(" 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 -> 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]
    ++ String
    ")]"
            mkLine :: ([CV], [CV]) -> String
    mkLine  ([CV]
    i, [CV]
    o)     = String
    "("  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 -> 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]
    ++ String
    ")"
            mapType :: ([a] -> String) -> [a] -> String
    mapType [a] -> String
    f [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 [String
    x] = String
    x
            mkTuple [String]
    xs  = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String]
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            typeOf :: [a] -> String
    typeOf []    = String
    "()"
            typeOf [a
    x]   = a -> String
    forall {a}. (HasKind a, Show a) => a -> String
    t a
    x
            typeOf (a
    x:[a]
    _) = String
    "[" 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]
    ++ String
    "]"
            valOf :: [CV] -> String
    valOf  []    = String
    "()"
            valOf  [CV
    x]   = CV -> String
    s CV
    x
            valOf  [CV]
    xs    = String
    "[" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((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]
    ++ String
    "]"

            t :: a -> String
    t a
    cv = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                     Kind
    KBool             -> String
    "Bool"
                     KBounded Bool
    False Int
    8  -> String
    "Word8"
                     KBounded Bool
    False Int
    16 -> String
    "Word16"
                     KBounded Bool
    False Int
    32 -> String
    "Word32"
                     KBounded Bool
    False Int
    64 -> String
    "Word64"
                     KBounded Bool
    True  Int
    8  -> String
    "Int8"
                     KBounded Bool
    True  Int
    16 -> String
    "Int16"
                     KBounded Bool
    True  Int
    32 -> String
    "Int32"
                     KBounded Bool
    True  Int
    64 -> String
    "Int64"
                     Kind
    KUnbounded        -> String
    "Integer"
                     Kind
    KFloat            -> String
    "Float"
                     Kind
    KDouble           -> String
    "Double"
                     Kind
    KChar             -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported char"
                     Kind
    KString           -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported string"
                     Kind
    KReal             -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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 Kind
    es          -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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]
    ++ String
    "]"
                     KSet  Kind
    es          -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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]
    ++ String
    "}"
                     KUserSort String
    us Maybe [String]
    _    -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.renderTest: Unsupported uninterpreted sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    us
                     Kind
    _                 -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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 = case CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    cv of
                      Kind
    KBool             -> Int -> String -> String
    forall a. Int -> [a] -> [a]
    take Int
    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 Char
    ' ')
                      KBounded Bool
    sgn   Int
    sz -> let CInteger 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
                      Kind
    KUnbounded        -> let CInteger Integer
    w = CV -> CVal
    cvVal CV
    cv in Bool -> Bool -> Integer -> String
    shexI Bool
    False Bool
    True           Integer
    w
                      Kind
    KFloat            -> let CFloat   Float
    w = CV -> CVal
    cvVal CV
    cv in Float -> String
    showHFloat Float
    w
                      Kind
    KDouble           -> let CDouble  Double
    w = CV -> CVal
    cvVal CV
    cv in Double -> String
    showHDouble Double
    w
                      Kind
    KRational         -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported rational number"
                      KFP{}             -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported arbitrary float"
                      Kind
    KChar             -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported char"
                      Kind
    KString           -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported string"
                      Kind
    KReal             -> let CAlgReal AlgReal
    w = CV -> CVal
    cvVal CV
    cv in AlgReal -> String
    algRealToHaskell AlgReal
    w
                      KList Kind
    es          -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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]
    ++ String
    "]"
                      KSet  Kind
    es          -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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]
    ++ String
    "}"
                      KUserSort String
    us Maybe [String]
    _    -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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
    $ String
    "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
    $ String
    "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
    $ String
    "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 String
    n [([CV], [CV])]
    vs = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $
                  [ String
    "/* Automatically generated by SBV. Do not edit! */"
                  , String
    ""
                  , String
    "#include <stdio.h>"
                  , String
    "#include <inttypes.h>"
                  , String
    "#include <stdint.h>"
                  , String
    "#include <stdbool.h>"
                  , String
    "#include <string.h>"
                  , String
    "#include <math.h>"
                  , String
    ""
                  , String
    "/* The boolean type */"
                  , String
    "typedef bool SBool;"
                  , String
    ""
                  , String
    "/* The float type */"
                  , String
    "typedef float SFloat;"
                  , String
    ""
                  , String
    "/* The double type */"
                  , String
    "typedef double SDouble;"
                  , String
    ""
                  , String
    "/* Unsigned bit-vectors */"
                  , String
    "typedef uint8_t  SWord8;"
                  , String
    "typedef uint16_t SWord16;"
                  , String
    "typedef uint32_t SWord32;"
                  , String
    "typedef uint64_t SWord64;"
                  , String
    ""
                  , String
    "/* Signed bit-vectors */"
                  , String
    "typedef int8_t  SInt8;"
                  , String
    "typedef int16_t SInt16;"
                  , String
    "typedef int32_t SInt32;"
                  , String
    "typedef int64_t SInt64;"
                  , String
    ""
                  , String
    "typedef struct {"
                  , String
    "  struct {"
                  ]
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (if [([CV], [CV])] -> Bool
    forall a. [a] -> 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} {p}. (Show a, HasKind p) => String -> p -> a -> String
    mkField String
    "i") (([CV], [CV]) -> [CV]
    forall a b. (a, b) -> a
    fst ([([CV], [CV])] -> ([CV], [CV])
    forall a. HasCallStack => [a] -> a
    head [([CV], [CV])]
    vs)) [(Int
    0::Int)..])
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "  } input;"
                  , String
    "  struct {"
                  ]
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ (if [([CV], [CV])] -> Bool
    forall a. [a] -> 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} {p}. (Show a, HasKind p) => String -> p -> a -> String
    mkField String
    "o") (([CV], [CV]) -> [CV]
    forall a b. (a, b) -> b
    snd ([([CV], [CV])] -> ([CV], [CV])
    forall a. HasCallStack => [a] -> a
    head [([CV], [CV])]
    vs)) [(Int
    0::Int)..])
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [ String
    "  } output;"
                  , String
    "} " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "TestVector;"
                  , String
    ""
                  , String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "TestVector " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "[] = {"
                  ]
               [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++ [String
    "      " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\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]
    ++ [ String
    "};"
                  , String
    ""
                  , String
    "int " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "Length = " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show ([([CV], [CV])] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [([CV], [CV])]
    vs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ";"
                  , String
    ""
                  , String
    "/* Stub driver showing the test values, replace with code that uses the test vectors. */"
                  , String
    "int main(void)"
                  , String
    "{"
                  , String
    "  int i;"
                  , String
    "  for(i = 0; i < " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "Length; ++i)"
                  , String
    "  {"
                  , String
    "    " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    outLine
                  , String
    "  }"
                  , String
    ""
                  , String
    "  return 0;"
                  , String
    "}"
                  ]
      where mkField :: String -> p -> a -> String
    mkField String
    p p
    cv a
    i = String
    "    " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    t String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " " 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]
    ++ String
    ";"
                where t :: String
    t = case p -> Kind
    forall a. HasKind a => a -> Kind
    kindOf p
    cv of
                            Kind
    KBool             -> String
    "SBool"
                            KBounded Bool
    False Int
    8  -> String
    "SWord8"
                            KBounded Bool
    False Int
    16 -> String
    "SWord16"
                            KBounded Bool
    False Int
    32 -> String
    "SWord32"
                            KBounded Bool
    False Int
    64 -> String
    "SWord64"
                            KBounded Bool
    True  Int
    8  -> String
    "SInt8"
                            KBounded Bool
    True  Int
    16 -> String
    "SInt16"
                            KBounded Bool
    True  Int
    32 -> String
    "SInt32"
                            KBounded Bool
    True  Int
    64 -> String
    "SInt64"
                            k :: Kind
    k@KBounded{}      -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.renderTest: Unsupported kind: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                            Kind
    KFloat            -> String
    "SFloat"
                            Kind
    KDouble           -> String
    "SDouble"
                            Kind
    KRational         -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported rational number"
                            KFP{}             -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported arbitrary float"
                            Kind
    KChar             -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported char"
                            Kind
    KString           -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported string"
                            Kind
    KUnbounded        -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unbounded integers are not supported when generating C test-cases."
                            Kind
    KReal             -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Real values are not supported when generating C test-cases."
                            KUserSort String
    us Maybe [String]
    _    -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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
    $ String
    "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
    $ String
    "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
    $ String
    "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
    $ String
    "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
    $ String
    "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 ([CV]
    is, [CV]
    os) = String
    "{{" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((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 -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " ((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]
    ++ String
    "}}"

            v :: CV -> String
    v CV
    cv = case CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    cv of
                      Kind
    KBool            -> if CV -> Bool
    cvToBool CV
    cv then String
    "true " else String
    "false"
                      KBounded Bool
    sgn Int
    sz  -> let CInteger 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
                      Kind
    KUnbounded       -> let CInteger Integer
    w = CV -> CVal
    cvVal CV
    cv in Bool -> Bool -> Integer -> String
    shexI Bool
    False Bool
    True           Integer
    w
                      Kind
    KFloat           -> let CFloat Float
    w   = CV -> CVal
    cvVal CV
    cv in Float -> String
    showCFloat Float
    w
                      Kind
    KDouble          -> let CDouble Double
    w  = CV -> CVal
    cvVal CV
    cv in Double -> String
    showCDouble Double
    w
                      Kind
    KRational        -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported rational number"
                      KFP{}            -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported arbitrary float"
                      Kind
    KChar            -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported char"
                      Kind
    KString          -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "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
    $ String
    "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
    $ String
    "SBV.renderTest: Unsupported set sort!" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    k
                      KUserSort String
    us Maybe [String]
    _   -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.renderTest: Unsupported uninterpreted sort: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    us
                      Kind
    KReal            -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "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
    $ String
    "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
    $ String
    "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
    $ String
    "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 a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [([CV], [CV])]
    vs = String
    "printf(\"\");"
              | Bool
    True    = String
    "printf(\"%*d. " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    fmtString String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    "\\n\", " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show (String -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Int -> String
    forall a. Show a => a -> String
    show ([([CV], [CV])] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [([CV], [CV])]
    vs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1))) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ", 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 (String
    "\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 [(Int
    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 [(Int
    0::Int)..])
                        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ");"
              where ([CV]
    is, [CV]
    os) = [([CV], [CV])] -> ([CV], [CV])
    forall a. HasCallStack => [a] -> a
    head [([CV], [CV])]
    vs
                    inp :: a -> a -> String
    inp a
    cv 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]
    ++ String
    "[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 a
    cv 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]
    ++ String
    "[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 a
    cv String
    s = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                                    Kind
    KBool -> String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " == true) ? \"true \" : \"false\""
                                    Kind
    _     -> 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 -> 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 a
    cv = case a -> Kind
    forall a. HasKind a => a -> Kind
    kindOf a
    cv of
                        Kind
    KBool             -> String
    "%s"
                        KBounded Bool
    False  Int
    8 -> String
    "0x%02\"PRIx8\""
                        KBounded Bool
    False Int
    16 -> String
    "0x%04\"PRIx16\"U"
                        KBounded Bool
    False Int
    32 -> String
    "0x%08\"PRIx32\"UL"
                        KBounded Bool
    False Int
    64 -> String
    "0x%016\"PRIx64\"ULL"
                        KBounded Bool
    True   Int
    8 -> String
    "%\"PRId8\""
                        KBounded Bool
    True  Int
    16 -> String
    "%\"PRId16\""
                        KBounded Bool
    True  Int
    32 -> String
    "%\"PRId32\"L"
                        KBounded Bool
    True  Int
    64 -> String
    "%\"PRId64\"LL"
                        Kind
    KFloat            -> String
    "%f"
                        Kind
    KDouble           -> String
    "%f"
                        Kind
    KChar             -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported char"
                        Kind
    KString           -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported string"
                        Kind
    KUnbounded        -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported unbounded integers for C generation."
                        Kind
    KReal             -> String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: Unsupported real valued values for C generation."
                        Kind
    _                 -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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 String
    vname Bool
    bigEndian ([Int], [Int])
    ss [([CV], [CV])]
    vs = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\n" ([String] -> String) -> [String] -> String
    forall a b. (a -> b) -> a -> b
    $ [ String
    "// Automatically generated by SBV. Do not edit!"
                                                 , String
    "let " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    n String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " ="
                                                 , String
    "   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]
    ++ [ String
    "   in [ " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "\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)
                                                 , String
    "      ];"
                                                 ]
      where n :: String
    n | String -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    vname                 = String
    "testVectors"
              | Bool -> Bool
    not (Char -> Bool
    isAlpha (String -> Char
    forall a. HasCallStack => [a] -> a
    head String
    vname)) = String
    "tv" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    vname
              | Bool
    True                       = String
    vname
            blaster :: String
    blaster
             | Bool
    bigEndian = String
    "map (\\s. s == \"1\") (explode (string_tl r))"
             | Bool
    True      = String
    "rev (map (\\s. s == \"1\") (explode (string_tl r)))"
            toF :: Bool -> Char
    toF Bool
    True  = Char
    '1'
            toF Bool
    False = Char
    '0'
            blast :: CV -> String
    blast CV
    cv = let noForte :: String -> String
    noForte String
    w = String -> String
    forall a. HasCallStack => String -> a
    error String
    "SBV.renderTest: " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    w String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " values are not supported when generating Forte test-cases."
                       in case CV -> Kind
    forall a. HasKind a => a -> Kind
    kindOf CV
    cv of
                            Kind
    KBool             -> [Bool -> Char
    toF (CV -> Bool
    cvToBool CV
    cv)]
                            KBounded Bool
    False Int
    8  -> Int -> CVal -> String
    xlt  Int
    8 (CV -> CVal
    cvVal CV
    cv)
                            KBounded Bool
    False Int
    16 -> Int -> CVal -> String
    xlt Int
    16 (CV -> CVal
    cvVal CV
    cv)
                            KBounded Bool
    False Int
    32 -> Int -> CVal -> String
    xlt Int
    32 (CV -> CVal
    cvVal CV
    cv)
                            KBounded Bool
    False Int
    64 -> Int -> CVal -> String
    xlt Int
    64 (CV -> CVal
    cvVal CV
    cv)
                            KBounded Bool
    True Int
    8   -> Int -> CVal -> String
    xlt  Int
    8 (CV -> CVal
    cvVal CV
    cv)
                            KBounded Bool
    True Int
    16  -> Int -> CVal -> String
    xlt Int
    16 (CV -> CVal
    cvVal CV
    cv)
                            KBounded Bool
    True Int
    32  -> Int -> CVal -> String
    xlt Int
    32 (CV -> CVal
    cvVal CV
    cv)
                            KBounded Bool
    True Int
    64  -> Int -> CVal -> String
    xlt Int
    64 (CV -> CVal
    cvVal CV
    cv)
                            Kind
    KFloat            -> String -> String
    noForte String
    "Float"
                            Kind
    KDouble           -> String -> String
    noForte String
    "Double"
                            Kind
    KChar             -> String -> String
    noForte String
    "Char"
                            Kind
    KString           -> String -> String
    noForte String
    "String"
                            Kind
    KReal             -> String -> String
    noForte String
    "Real"
                            KList Kind
    ek          -> String -> String
    noForte (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "List of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek
                            KSet  Kind
    ek          -> String -> String
    noForte (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "Set of " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Kind -> String
    forall a. Show a => a -> String
    show Kind
    ek
                            Kind
    KUnbounded        -> String -> String
    noForte String
    "Unbounded integers"
                            KUserSort String
    s Maybe [String]
    _     -> String -> String
    noForte (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "Uninterpreted kind " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> String
    forall a. Show a => a -> String
    show String
    s
                            Kind
    _                 -> String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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 Int
    s (CInteger  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
    -Int
    1, Int
    sInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    2 .. Int
    0]]
            xlt Int
    _ (CFloat    Float
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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 Int
    _ (CDouble   Double
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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 Int
    _ (CFP       FP
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.renderTest.Forte: Unexpected arbitrary float value: "  String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ FP -> String
    forall a. Show a => a -> String
    show FP
    r
            xlt Int
    _ (CRational Rational
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "SBV.renderTest.Forte: Unexpected rational  value: "        String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ Rational -> String
    forall a. Show a => a -> String
    show Rational
    r
            xlt Int
    _ (CChar     Char
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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 Int
    _ (CString   String
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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 Int
    _ (CAlgReal  AlgReal
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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 Int
    _ CList{}        = String -> String
    forall a. HasCallStack => String -> a
    error   String
    "SBV.renderTest.Forte: Unexpected list value!"
            xlt Int
    _ CSet{}         = String -> String
    forall a. HasCallStack => String -> a
    error   String
    "SBV.renderTest.Forte: Unexpected set value!"
            xlt Int
    _ CTuple{}       = String -> String
    forall a. HasCallStack => String -> a
    error   String
    "SBV.renderTest.Forte: Unexpected list value!"
            xlt Int
    _ CMaybe{}       = String -> String
    forall a. HasCallStack => String -> a
    error   String
    "SBV.renderTest.Forte: Unexpected maybe value!"
            xlt Int
    _ CEither{}      = String -> String
    forall a. HasCallStack => String -> a
    error   String
    "SBV.renderTest.Forte: Unexpected sum value!"
            xlt Int
    _ (CUserSort (Maybe Int, String)
    r)  = String -> String
    forall a. HasCallStack => String -> a
    error (String -> String) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ String
    "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  (t CV
    i, t CV
    o) = String
    "("  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 -> 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]
    ++ String
    ")"
            mkTuple :: [String] -> String
    mkTuple []  = String
    "()"
            mkTuple [String
    x] = String
    x
            mkTuple [String]
    xs  = String
    "(" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    ", " [String]
    xs String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ")"
            form :: [Int] -> String -> [String]
    form []     [] = []
            form []     String
    bs = String -> [String]
    forall a. HasCallStack => String -> a
    error (String -> [String]) -> String -> [String]
    forall a b. (a -> b) -> a -> b
    $ String
    "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 a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    bs) String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " bit(s) remain."
            form (Int
    i:[Int]
    is) String
    bs
              | String -> Int
    forall a. [a] -> 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
    $ String
    "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]
    ++ String
    " 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]
    ++ String
    " remains."
              | Int
    i Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    1        = let Char
    b:String
    r = String
    bs
                                    v :: String
    v   = if Char
    b Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '1' then String
    "T" else String
    "F"
                                in String
    v String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [Int] -> String -> [String]
    form [Int]
    is String
    r
              | Bool
    True          = let (String
    f, String
    r) = Int -> String -> (String, String)
    forall a. Int -> [a] -> ([a], [a])
    splitAt Int
    i String
    bs
                                    v :: String
    v      = String
    "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]
    ++ String
    "'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