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

{-# OPTIONS_GHC -Wall -Werror -Wno-incomplete-uni-patterns #-}

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

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

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

import Data.SBV.Utils.PrettyNum

import qualified Data.Foldable as F (toList)

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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