Low level functions to access the SBV infrastructure, for developers who want to build further tools on top of SBV. End-users of the library should not need to use this module.
- data Result
- runSymbolic :: Symbolic a -> IO Result
- data SBV a = SBV !(Bool, Size) !(Either CW (Cached SW))
- generateGoldCheck :: FilePath -> Bool -> forall a. Show a => IO a -> FilePath -> IO ()
- showsAs :: Show a => a -> String -> Assertion
- ioShowsAs :: Show a => IO a -> String -> Assertion
- mkTestSuite :: ((forall a. Show a => IO a -> FilePath -> IO ()) -> Test) -> SBVTestSuite
- data SBVTestSuite = SBVTestSuite ((forall a. Show a => IO a -> FilePath -> IO ()) -> Test)
- module Test.HUnit
Running symbolic programs manually
The Symbolic value. Either a constant (
Left) or a symbolic
Right Cached). Note that caching is essential for making
sure sharing is preserved. The parameter
a is phantom, but is
extremely important in keeping the user interface strongly typed.
Integrating with the test framework
Functionality needed for extending SBV's internal test-suite. Only for developers of further libraries on top of SBV.
Create a gold file for the test case
Run an IO computation and check that it's result shows as
SBVTestSuite, avoids exporting the constructor
A Test-suite, parameterized by the gold-check generator/checker