Encode Invariant properties in the type system for quickcheck properties #4
Description
Currently we have quickcheck/smallcheck properties like this:
plainBecomesUnit :: TestTree
plainBecomesUnit = QC.testProperty
"For all plain formulas the found variational core is Unit"
$ \p -> isPlain p QC.==> QCM.monadicIO $
do (core, _) <- liftIO $ solveForCore p Nothing
QCM.assert $ isUnit core
which generates random plain propositions and makes sure that any plain proposition is reduced to a Unit variational core. This works but has the following problem:
...
[GOOD] (assert false)
[Debug] Proposition: : LitB False @(vsmt-0.0.1-inplace:Data.Solve ./Data/Solve.hs:56:9)
[Debug] Core: : VarCore Unit @(vsmt-0.0.1-inplace:Data.Solve ./Data/Solve.hs:56:9)
[Debug] Is Core Unit: : True @(vsmt-0.0.1-inplace:Data.Solve ./Data/Solve.hs:56:9)
*** Solver : Z3
*** Exit code: ExitSuccess
OK (0.49s)
+++ OK, passed 100 tests; 213 discarded.
All 7 tests passed (0.54s)
Test suite VSMTTest: PASS
Test suite logged to: /store/Research/VSmt/haskell/vsmt/dist-newstyle/build/x86_64-linux/ghc-8.8.4/vsmt-0.0.1/t/VSMTTest/test/vsmt-0.0.1-VSMTTest.log
(END)
namely, that quickcheck discards 213 generated propositions because these propositions failed the isPlain check in the antecedent of QC.==>. A better way is to newtype the property of Plain, i.e.:
-- | Proof that a is Plain
newtype Plain a = Plain a
and then write a generate just for Plain. This avoids the generate -> test loop and will allow the property to be tested on much more than 100 test cases.