{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Tools.GenTest (
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)
newtype TestVectors = TV [([CV], [CV])]
getTestValues :: TestVectors -> [([CV], [CV])]
getTestValues :: TestVectors -> [([CV], [CV])]
getTestValues (TV vs :: [([CV], [CV])]
vs) = [([CV], [CV])]
vs
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]
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
data TestStyle = Haskell String
| C String
| Forte String Bool ([Int], [Int])
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