-----------------------------------------------------------------------------
-- |
-- 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 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 [([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 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 (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), 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 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 (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 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 (t :: * -> *) a. Foldable t => t a -> Bool
null String
vname                 = String
"testVectors"
          | Bool -> Bool
not (Char -> Bool
isAlpha (String -> Char
forall a. [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 (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 (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 (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 String
"i") (([CV], [CV]) -> [CV]
forall a b. (a, b) -> a
fst ([([CV], [CV])] -> ([CV], [CV])
forall a. [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 (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 String
"o") (([CV], [CV]) -> [CV]
forall a b. (a, b) -> b
snd ([([CV], [CV])] -> ([CV], [CV])
forall a. [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 (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 -> a -> a -> String
mkField String
p a
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 a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
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 (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 (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
- 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. [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 (t :: * -> *) a. Foldable t => t a -> Bool
null String
vname                 = String
"testVectors"
          | Bool -> Bool
not (Char -> Bool
isAlpha (String -> Char
forall a. [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 (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 (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