module Tip
( Equality
, (:=>:)
, And
, Or
, Neg
, Forall
, Exists
, (===)
, (=/=)
, bool
, (==>)
, (.&&.)
, (.||.)
, neg
, question
, forAll
, exists
, module Test.QuickCheck
) where
import Test.QuickCheck hiding ((===), (==>), (.&&.), (.||.), forAll)
import qualified Test.QuickCheck as QC
infix 3 ===
infix 3 =/=
infixr 2 .&&.
infixr 1 .||.
infixr 0 ==>
infixr 0 :=>:
data Equality a = a :=: a
data a :=>: b = Given a b
data And a b = And a b
data Or a b = Or a b
data Neg a = Neg a
data Forall a b = Forall (a -> b)
data Exists a b = Exists (a -> b)
(===) :: a -> a -> Equality a
(===) = (:=:)
(=/=) :: a -> a -> Neg (Equality a)
u =/= v = Neg (u === v)
bool :: Bool -> Equality Bool
bool lhs = lhs === True
(==>) :: a -> b -> a :=>: b
(==>) = Given
(.&&.) :: a -> b -> And a b
(.&&.) = And
(.||.) :: a -> b -> Or a b
(.||.) = Or
neg :: a -> Neg a
neg = Neg
question :: a -> Neg a
question = Neg
forAll :: (a -> b) -> Forall a b
forAll = Forall
exists :: (a -> b) -> Exists a b
exists = Exists
instance (Eq a, Show a) => Testable (Equality a) where
property (x :=: y) = x QC.=== y
instance Testable b => Testable (Bool :=>: b) where
property (Given x p) = x QC.==> p
instance Testable b => Testable (Neg Bool :=>: b) where
property (Given (Neg x) p) = not x QC.==> p
instance Testable (Neg Bool) where
property (Neg x) = property (not x)
instance (Eq a, Show a, Testable b) => Testable (Equality a :=>: b) where
property (Given (x :=: y) p) = x == y QC.==> p
instance (Testable a, Testable b) => Testable (And a b) where
property (And p q) = p QC..&&. q
instance (Testable a, Testable b) => Testable (Or a b) where
property (Or p q) = p QC..||. q
instance (Arbitrary a, Show a, Testable b) => Testable (Forall a b) where
property (Forall p) = property p