generating Haskell/C test vectors from SBV

testGenerator.hs

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV

-- you can have arbitrary number of constrain/pConstrain's.. Of course, if they
-- are *hard to satisfy*, then generating tests can take a loong time. The algorithm
-- simply makes up random cases and runs the code to see if constraints are satisfied;
-- if not it tries again. So, with hard constraints, this process can take long. In
-- particular, consider "constrain false", :-)
code = do t <- free_
          x :: SWord32 <- free_
          y :: SWord32 <- free_
          -- guarantee that y is at least 5
          constrain (y .>= 5)
          -- make sure x is larger than y 75% of the time
          pConstrain 0.75 (x .> y)
          -- do some arbitrary computation..
          return (ite t (x+y) (x-y), x*y)

main :: IO ()
main = do ts <- genTest 10 code
          writeFile "sbvTest.hs" $ renderTest (Haskell "tvs") ts
          writeFile "sbvTest.c"  $ renderTest (C "tvs")       ts