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

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

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

import Control.Monad (unless)

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

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

import Data.SBV.Utils.PrettyNum
import Data.SBV.Provers.Prover(defaultSMTCfg)

import qualified Data.Foldable as F (toList)

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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