This is a testing abstraction layer that allows the integration of test properties and functions into the What4 library without requiring a binding to a specific testing library or version thereof (e.g. QuickCheck, Hedgehog, etc.). All test properties and functions should be specified using the primary set of functions in this module, and then the actual test code will specify a binding of these abstractions to a specific test library.

In this way, the What4 can implement not only local tests but the test functionality can be exported to enable downstream modules to perform extended testing.

The actual tests should be written using only the functions exported in the testing exports section of this module. Note that only the set of functions needed for What4 is defined by this testing abstraction; if additional testing functions are needed, the GenEnv context should be extended to add an adaptation entry and the function should be defined here for use by the tests.

The overlap (common subset) between testing libraries such as QuickCheck and Hedgehog is only of moderate size: both libraries (and especially Hedgehog) provide functionality that is not present in the other library. This module does not attempt to provide full coverage for the functionality in both libraries; the intent is that test functions can be written using the proxy functions defined here and that downstream code using either of QuickCheck or Hedgehog can utilize these support functions in their own tests. As such, it is recommended that the What4 integrated tests are limited in expression to the common subset that can be described here.

A specific test configuration will need to use the functions and definitions in the concretization exports to bind these abstracted test functions to the specific library being used by that test suite.

For example, to bind to QuickCheck, specify:

import QuickCheck
import qualified Test.Verification as V

quickCheckGenerators = V.GenEnv { V.genChooseBool = elements [ True, False ]
                                , V.genChooseInteger = \r -> choose r
                                , V.genChooseInt = \r -> choose r
                                , V.genGetSize = getSize
                                }

genTest :: String -> V.Gen V.Property -> TestTree
genTest nm p = testProperty nm
               (property $ V.toNativeProperty quickCheckGenerators p)

These definitions should be used by the tests themselves. Most of these parallel a corresponding function in QuickCheck or Hedgehog, so the adaptation is minimal.

Used by test implementation functions to map from this Verification abstraction to the actual test mechanism (e.g. QuickCheck, HedgeHog, etc.)