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

module Data.SBV.BitVectors.GenTest (genTest) where

import Data.Maybe (fromMaybe)

import Data.SBV.BitVectors.Data

-- | Generate a set of concrete test values from a symbolic program. The output
-- can be rendered as test vectors in different languages as necessary.
genTest :: Outputtable a => Int -> Symbolic a -> IO [([CW], [CW])]
genTest n m = sequence [tc | _ <- [1 .. n]]
  where tc = do (_, Result _ tvals _ _ cs _ _ _ _ _ os) <- runSymbolic' QuickCheck (m >>= output)
                let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)
                return (map snd tvals, map cval os)

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

module Data.SBV.BitVectors.GenTest (genTest) where

import Data.Maybe (fromMaybe)

import Data.SBV.BitVectors.Data

-- | 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.
genTest :: Int -> Symbolic () -> IO [([CW], [CW])]
genTest n m = sequence [tc | _ <- [1 .. n]]
  where tc = do (_, Result _ tvals _ _ cs _ _ _ _ _ os) <- runSymbolic' Concrete m
                let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs)
                return (map snd tvals, map cval os)

Make genTest use () return value, it's more usable that way.
Make genTest use () return value, it's more usable that way.