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

{-# OPTIONS_GHC -Wall -Werror #-}

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

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

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

import Data.SBV.Utils.PrettyNum

import qualified Data.Foldable as F (toList)

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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