Skip to content

Commit

Permalink
Add denotationFor
Browse files Browse the repository at this point in the history
  • Loading branch information
isovector committed Mar 6, 2020
1 parent b17996d commit c1166d7
Showing 1 changed file with 18 additions and 2 deletions.
20 changes: 18 additions & 2 deletions src/Test/QuickCheck/Checkers.hs
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ module Test.QuickCheck.Checkers
-- * Model-based (semantics-based) testing
, Model(..)
, meq, meq1, meq2, meq3, meq4, meq5
, eqModels
, eqModels, denotationFor
, Model1(..)
-- * Some handy testing types
-- , Positive, NonZero(..), NonNegative(..)
Expand Down Expand Up @@ -230,6 +230,19 @@ instance (Show a, Arbitrary a, EqProp b) => EqProp (a -> b) where
eqModels :: (Model a b, EqProp b) => a -> a -> Property
eqModels = (=-=) `on` model


-- | @f `'denotationFor'` g@ proves that @f@ is a model for @g@, ie that
-- @'model' . g '=-=' f@.
denotationFor
:: (Model b b', Arbitrary a, EqProp b', Show a)
=> (a -> b')
-> (a -> b)
-> TestBatch
denotationFor f g =
( "denotation"
, [("eq", model . g =-= f)]
)

-- Other types
-- instance EqProp a => EqProp (S.Stream a) where (=-=) = eqModels

Expand Down Expand Up @@ -404,10 +417,13 @@ instance Model Float Float where model = id
instance Model Double Double where model = id
instance Model String String where model = id

-- This next one requires UndecidableInstances
-- These next two require UndecidableInstances
instance (Model a b, Model a' b') => Model (a,a') (b,b') where
model = model *** model

instance Model b b' => Model (a -> b) (a -> b') where
model f = model . f

-- instance Model (S.Stream a) (NonNegative Int -> a) where
-- model s (NonNegative i) = s S.!! i

Expand Down

0 comments on commit c1166d7

Please sign in to comment.