GenTest.hs

import Data.SBV
import Data.List (zip4)

import qualified Data.Map as M

data MyTestData = TD0 Bool
                | TD1 Integer
                | TD2 Word32
                deriving Show

-- Generate n distinct instances of MyTestData
gen :: Int -> IO [MyTestData]
gen n = do dict <- getModelDictionary <$> sat pick

           let grab :: Int -> MyTestData
               grab caseNo = case (lkup "c" :: Integer, lkup "b", lkup "i", lkup "w") of
                               (0, b, _, _) -> TD0 b
                               (1, _, i, _) -> TD1 i
                               (2, _, _, w) -> TD2 w
                               (t, _, _, _) -> error $ "Impossible: Got a tag: " ++ show t
                 where lkup tag = case (tag ++ show caseNo) `M.lookup` dict of
                                    Nothing -> error $ "Cannot find value of " ++ show (tag ++ show caseNo) ++ " in the dictionary!"
                                    Just v  -> fromCW v


           return $ map grab [1..n]

 where pick = do cs <- mapM (sInteger . ("c" ++) . show) [1..n] -- which constructor
                 bs <- mapM (sBool    . ("b" ++) . show) [1..n] -- values for booleans
                 is <- mapM (sInteger . ("i" ++) . show) [1..n] -- values for integers
                 ws <- mapM (sWord32  . ("w" ++) . show) [1..n] -- values for words

                 -- require cs to be one of the three constructors
                 constrain $ bAll (`inRange` (0, 2)) cs

                 -- codify what "different" means between two elements
                 let different (c0, b0, i0, w0) (c1, b1, i1, w1) =
                                 (c0 ./= c1)                   -- different constructor
                             ||| (    (c0 .== 0 ==> b0 ./= b1)  -- OR, data differs for each choice
                                  &&& (c0 .== 1 ==> i0 ./= i1)
                                  &&& (c0 .== 2 ==> w0 ./= w1)
                                 )

                 -- require that choices differ
                 let choices = zip4 cs bs is ws

                     walk []     = true
                     walk (e:es) = bAll (different e) es &&& walk es

                 constrain $ walk choices

{- We get:
*Main> main
TD2 16
TD1 4
TD0 True
TD1 8
TD1 10
TD1 12
TD2 2
TD1 16
TD0 False
TD2 0
-}
main :: IO ()
main = mapM_ print =<< gen 10