diff --git a/ClassLaws.cabal b/ClassLaws.cabal new file mode 100644 --- /dev/null +++ b/ClassLaws.cabal @@ -0,0 +1,86 @@ +-- Initial ClassLaws.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +-- The name of the package. +name: ClassLaws + +-- The package version. See the Haskell package versioning policy (PVP) +-- for standards guiding when and how versions should be incremented. +-- http://www.haskell.org/haskellwiki/Package_versioning_policy +-- PVP summary: +-+------- breaking API changes +-- | | +----- non-breaking API additions +-- | | | +--- code changes with no API change +version: 0.3.0.0 + +-- A short (one-line) description of the package. +synopsis: Stating and checking laws for type class methods + +homepage: http://wiki.portal.chalmers.se/cse/pmwiki.php/FP/ClassLaws + +-- A longer description of the package. + +description: The specification of a class in Haskell often starts with + stating, in text, the laws that should be satisfied by methods + defined in instances of the class, followed by the type of the + methods of the class. The ClassLaws library is a framework that + supports testing such class laws using QuickCheck. Our framework is + a light-weight class law testing framework, which requires a limited + amount of work per class law, and per datatype for which the class + law is tested. We also show how to test class laws with + partially-defined values. Using partially-defined values, we show + that the standard lazy and strict implementations of the state monad + do not satisfy the expected laws. More information can be found at + http://wiki.portal.chalmers.se/cse/pmwiki.php/FP/ClassLaws + +-- The license under which the package is released. +license: BSD3 + +-- The file containing the license text. +license-file: LICENSE + +-- The package author(s). +author: Patrik Jansson and Johan Jeuring + +-- An email address to which users can send suggestions, bug reports, and +-- patches. +maintainer: patrikj@chalmers.se + +-- A copyright notice. +-- copyright: + +category: Testing + +build-type: Simple + +-- Constraint on the version of Cabal needed to build this package. +cabal-version: >=1.8 + + +library + -- Modules exported by the library. + exposed-modules: + Test.ClassLaws, Test.ClassLaws.Core, Test.ClassLaws.TestingEquality, Test.ClassLaws.Partial, + Test.ClassLaws.TestingFinFuns, + Test.ClassLaws.TestingDatatypes, Test.ClassLaws.TestingState, + Control.Monad.Laws, Control.Monad.Laws.Instances, + Control.Monad.State.Class.Laws, Control.Monad.State.Class.Laws.Instances, + Data.Monoid.Laws, Data.Monoid.Laws.Instances + + -- The Control.Monad and Data.Monoid laws should perhaps be split off + -- Some modules may be made internal + + -- Modules included in this library but not exported. + -- other-modules: +-- Test.ClassLaws.Tests, + + + -- Other library packages from which modules are imported. + build-depends: + base >=4.5 && < 5, + mtl >= 1 && < 3, + QuickCheck >= 2 && < 3, + ChasingBottoms >=1.3 && < 2 + + -- Directories containing source files. + hs-source-dirs: src + diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2012, Patrik Jansson and Johan Jeuring + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Patrik Jansson and Johan Jeuring nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/src/Control/Monad/Laws.hs b/src/Control/Monad/Laws.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Laws.hs @@ -0,0 +1,152 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE EmptyDataDecls #-} + +{- | This module implements the laws in Control.Monad, specified in +the Haskell 2010 report, in 6.3.5 for Functor, in 6.3.6 for Monad, and +in Chapter 13, module Control.Monad. -} +module Control.Monad.Laws (module Test.ClassLaws, module Control.Monad.Laws) where +import Control.Monad -- For MonadPlus; Functor and Monad are both in the Prelude +import Test.ClassLaws (LawTest(lawtest), LawArgs, LawBody, Law, (=.=), TestEqual, testEqual) + +data FunctorLaw1 a (f :: * -> *) +data FunctorLaw2 a b c (f :: * -> *) + +class Functor f => FunctorLaws f where + + functorLaw1 :: Law (FunctorLaw1 a f) + functorLaw2 :: Law (FunctorLaw2 a b c f) + + functorLaw1 = defaultFunctorLaw1 + functorLaw2 = defaultFunctorLaw2 + +defaultFunctorLaw1 x = fmap id x =.= id x +defaultFunctorLaw2 (f,g,x) = (fmap f . fmap g) x =.= fmap (f . g) x + +type instance LawArgs (FunctorLaw1 a f) = f a +type instance LawBody (FunctorLaw1 a f) = f a + +type instance LawArgs (FunctorLaw2 a b c f) = (b -> c, a -> b, f a) +type instance LawBody (FunctorLaw2 a b c f) = f c + +instance (FunctorLaws f, TestEqual (f a)) => LawTest (FunctorLaw1 a f) where + lawtest _ = testEqual . functorLaw1 + +instance (FunctorLaws f, TestEqual (f c)) => LawTest (FunctorLaw2 a b c f) where + lawtest _ = testEqual . functorLaw2 + + +data MonadLaw1 a b (m :: * -> *) +data MonadLaw2 b (m :: * -> *) +data MonadLaw3 b c d (m :: * -> *) + +class Monad m => MonadLaws m where + + monadLaw1 :: Law (MonadLaw1 a b m) + monadLaw2 :: Law (MonadLaw2 b m) + monadLaw3 :: Law (MonadLaw3 b c d m) + + monadLaw1 = defaultMonadLaw1 + monadLaw2 = defaultMonadLaw2 + monadLaw3 = defaultMonadLaw3 + +defaultMonadLaw1 (a,k) = return a >>= k =.= k a +defaultMonadLaw2 m = m >>= return =.= m +defaultMonadLaw3 (m,k,h) = m >>= (\x -> k x >>= h) =.= (m >>= k) >>= h + +type instance LawArgs (MonadLaw1 a b m) = (a, a -> m b) +type instance LawBody (MonadLaw1 a b m) = m b + +type instance LawArgs (MonadLaw2 b m) = m b +type instance LawBody (MonadLaw2 b m) = m b + +type instance LawArgs (MonadLaw3 b c d m) = (m b, b -> m c, c -> m d) +type instance LawBody (MonadLaw3 b c d m) = m d + +instance (MonadLaws m,TestEqual (m b)) => LawTest (MonadLaw1 a b m) where + lawtest _ = testEqual . monadLaw1 + +instance (MonadLaws m,TestEqual (m b)) => LawTest (MonadLaw2 b m) where + lawtest _ = testEqual . monadLaw2 + +instance (MonadLaws m,TestEqual (m d)) => LawTest (MonadLaw3 b c d m) where + lawtest _ = testEqual . monadLaw3 + + +data FunctorMonadLaw a b (m :: * -> *) + +class (Functor m, Monad m) => FunctorMonadLaws m where + + functorMonadLaw :: Law (FunctorMonadLaw a b m) + + functorMonadLaw = defaultFunctorMonadLaw + +defaultFunctorMonadLaw (f,xs) = fmap f xs =.= xs >>= return . f + + +type instance LawArgs (FunctorMonadLaw a b m) = (a -> b, m a) +type instance LawBody (FunctorMonadLaw a b m) = m b + +instance (FunctorMonadLaws m,TestEqual (m b)) => LawTest (FunctorMonadLaw a b m) where + lawtest _ = testEqual . functorMonadLaw + + +{- | The laws for MonadPlus are less prominently declared in the base +libraries. -} + +data MonadPlusLaw1 a (m :: * -> *) +data MonadPlusLaw2 a (m :: * -> *) +data MonadPlusLaw3 a b (m :: * -> *) +data MonadPlusLaw4 a (m :: * -> *) +data MonadPlusLaw5 a (m :: * -> *) + +class MonadPlus m => MonadPlusLaws m where + + monadPlusLaw1 :: Law (MonadPlusLaw1 a m) + monadPlusLaw2 :: Law (MonadPlusLaw2 a m) + monadPlusLaw3 :: Law (MonadPlusLaw3 a b m) + monadPlusLaw4 :: Law (MonadPlusLaw4 a m) + monadPlusLaw5 :: Law (MonadPlusLaw5 a m) + + monadPlusLaw1 = defaultMonadPlusLaw1 + monadPlusLaw2 = defaultMonadPlusLaw2 + monadPlusLaw3 = defaultMonadPlusLaw3 + monadPlusLaw4 = defaultMonadPlusLaw4 + monadPlusLaw5 = defaultMonadPlusLaw5 + +defaultMonadPlusLaw1 x = mzero `mplus` x =.= x +defaultMonadPlusLaw2 x = x `mplus` mzero =.= x +defaultMonadPlusLaw3 f = mzero >>= f =.= mzero +defaultMonadPlusLaw4 v = v >> mzero =.= mzero +defaultMonadPlusLaw5 (a,b,c) = a `mplus` (b `mplus` c) =.= (a `mplus` b) `mplus` c + +type instance LawArgs (MonadPlusLaw1 a m) = m a +type instance LawBody (MonadPlusLaw1 a m) = m a + +type instance LawArgs (MonadPlusLaw2 a m) = m a +type instance LawBody (MonadPlusLaw2 a m) = m a + +type instance LawArgs (MonadPlusLaw3 a b m) = a -> m b +type instance LawBody (MonadPlusLaw3 a b m) = m b + +type instance LawArgs (MonadPlusLaw4 a m) = m a +type instance LawBody (MonadPlusLaw4 a m) = m a + +type instance LawArgs (MonadPlusLaw5 a m) = (m a, m a, m a) +type instance LawBody (MonadPlusLaw5 a m) = m a + +instance (MonadPlusLaws m,TestEqual (m a)) => LawTest (MonadPlusLaw1 a m) where + lawtest _ = testEqual . monadPlusLaw1 + +instance (MonadPlusLaws m,TestEqual (m a)) => LawTest (MonadPlusLaw2 a m) where + lawtest _ = testEqual . monadPlusLaw2 + +instance (MonadPlusLaws m,TestEqual (m b)) => LawTest (MonadPlusLaw3 a b m) where + lawtest _ = testEqual . monadPlusLaw3 + +instance (MonadPlusLaws m,TestEqual (m a)) => LawTest (MonadPlusLaw4 a m) where + lawtest _ = testEqual . monadPlusLaw4 + +instance (MonadPlusLaws m,TestEqual (m a)) => LawTest (MonadPlusLaw5 a m) where + lawtest _ = testEqual . monadPlusLaw5 diff --git a/src/Control/Monad/Laws/Instances.hs b/src/Control/Monad/Laws/Instances.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Laws/Instances.hs @@ -0,0 +1,176 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} + +-- | Tests the Monad ClassLaws for a few example datatypes. Mainly +-- instance declarations and QuickCheck tests + a 'main' to run it. +module Control.Monad.Laws.Instances where +import Control.Monad.State +import Control.Monad.Laws +import Test.ClassLaws +import Test.ClassLaws.TestingDatatypes(MyList(..), (+++), snoc, foldrMyList) + +instance FunctorLaws [] where + functorLaw1 xs = addSteps (defaultFunctorLaw1 xs) + (case xs of + [] -> nilCase + ys@(_:_) -> conCase ys) + where + nilCase = + [ fmap id [] + , -- definition of fmap on [] + [] + ] + conCase (y:ys) = + [ fmap id (y:ys) + , -- definition of fmap on (x:xs) + id y:fmap id ys + , -- definition of id + y:fmap id ys +-- y:fmap id (ys++ys) -- gives an error (used to test error injection) + , -- induction hypothesis + y:ys + , -- definition of id + id (y:ys) + ] + +testFunctorList + = do quickLawCheck (undefined::FunctorLaw1 Char []) + quickFLawCheck (undefined::FunctorLaw2 Int Char Bool []) + +instance FunctorLaws Maybe + +testFunctorMaybe + = do quickLawCheck (undefined::FunctorLaw1 Char Maybe) + quickFLawCheck (undefined::FunctorLaw2 Int Char Bool Maybe) + + +instance FunctorLaws IO + +{- -- How do I test IO values? + +testFunctorIO + = do quickBlind (undefined::FunctorLaw1 Char IO) + quickBlind (undefined::FunctorLaw2 Int Char Bool IO) +-} + + +{- +The following instance of Functor for MyList should *not* satisfy the functor +laws. +-} + +-- Wrong instance of functor, because the order is reversed by fmap. + +instance Functor MyList where + fmap f Nil = Nil + fmap f (Cons x xs) = snoc (f x) (fmap f xs) + +instance FunctorLaws MyList + where + functorLaw1 xs = addSteps (defaultFunctorLaw1 xs) + (case xs of + Nil -> nilCase + zs@(Cons y ys) -> conCase zs) + where + nilCase = + [ fmap id Nil + , -- definition of fmap on [] + Nil + ] + conCase (Cons y ys) = + [ fmap id (Cons y ys) + , -- definition of fmap on (x:xs) + snoc (id y) (fmap id ys) + , -- definition of id + snoc y (fmap id ys) + , -- induction hypothesis + snoc y ys + , -- definition of id + id (Cons y ys) + ] + +testFunctorMyList + = do quickLawCheck (undefined::FunctorLaw1 Int MyList) + quickFLawCheck (undefined::FunctorLaw2 Char Int Int MyList) + + +instance MonadLaws [] + +testMonadList + = do quickFLawCheck (undefined::MonadLaw1 Char Int []) + quickLawCheck (undefined::MonadLaw2 Int []) + quickFLawCheck (undefined::MonadLaw3 Int Bool Char []) + + +instance MonadLaws Maybe + +testMonadMaybe + = do quickFLawCheck (undefined::MonadLaw1 Char Int Maybe) + quickLawCheck (undefined::MonadLaw2 Int Maybe) + quickFLawCheck (undefined::MonadLaw3 Int Bool Char Maybe) + + +instance FunctorMonadLaws MyList + +testFunctorMonadMyList + = do quickFLawCheck (undefined:: FunctorMonadLaw Char Int MyList) + + +instance MonadLaws IO + + +instance MonadLaws (State s) + +testMonadState + = do quickFLawCheck (undefined::MonadLaw1 Bool Int (State Bool)) + quickFLawCheck (undefined::MonadLaw2 Int (State Bool)) -- necessary because of Show State problem + quickFLawCheck (undefined::MonadLaw3 Int Bool Char (State Bool)) + + +instance Monad MyList where + m >>= k = foldrMyList ((+++) . k) Nil m + m >> k = foldrMyList ((+++) . (\ _ -> k)) Nil m + return x = Cons x (Cons x Nil) -- gives an error +-- return x = Cons x Nil -- correct + fail _ = Nil + +instance MonadLaws MyList + +testMonadMyList + = do quickFLawCheck (undefined::MonadLaw1 Char Int MyList) + quickLawCheck (undefined::MonadLaw2 Int MyList) + quickFLawCheck (undefined::MonadLaw3 Int Bool Char MyList) + + +instance FunctorMonadLaws [] + +testFunctorMonadList + = do quickFLawCheck (undefined::FunctorMonadLaw Char Int []) + + +instance FunctorMonadLaws Maybe + +testFunctorMonadMaybe + = do quickFLawCheck (undefined::FunctorMonadLaw Char Int Maybe) + + +instance FunctorMonadLaws IO + + +main = do testMonadMaybe + testMonadState + + testFunctorList + testFunctorMaybe + + testFunctorMonadList + testFunctorMonadMaybe + +expectedFailures = do + testMonadMyList + testFunctorMyList + testFunctorMonadMyList + +-- No MonadPlusLaw instances yet. + diff --git a/src/Control/Monad/State/Class/Laws.hs b/src/Control/Monad/State/Class/Laws.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/State/Class/Laws.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE EmptyDataDecls #-} + +-- | Laws for the 'MonadState' class. A submodule has a +-- 'Control.Monad.State.Class.Laws.Instances.main' which runs quite a +-- few tests for the lazy and strict state monads. +module Control.Monad.State.Class.Laws where +import Control.Monad.State.Class (MonadState(..)) +import Test.ClassLaws + +class MonadState s m => MonadStateLaws s m where + monadStatePutPut :: Law (MonadStatePutPut s m) + monadStatePutGet :: Law (MonadStatePutGet s m) + monadStateGetPut :: Law (MonadStateGetPut m) + monadStateGetGet :: Law (MonadStateGetGet s a m) + + monadStatePutPut = defaultMonadStatePutPut + monadStatePutGet = defaultMonadStatePutGet + monadStateGetPut = defaultMonadStateGetPut + monadStateGetGet = defaultMonadStateGetGet + +defaultMonadStatePutPut (s,s') = put s' >> put s =.= put s +defaultMonadStatePutGet s = put s >> get =.= put s >> return s +defaultMonadStateGetPut _ = get >>= put =.= return () +defaultMonadStateGetGet k = get >>= (\s->get >>= k s) =.= get >>= \s->k s s + +data MonadStatePutPut s (m :: * -> *) +data MonadStatePutGet s (m :: * -> *) +data MonadStateGetPut (m :: * -> *) +data MonadStateGetGet s a (m :: * -> *) + +type instance LawArgs (MonadStatePutPut s m) = (s, s) +type instance LawBody (MonadStatePutPut s m) = m () + +type instance LawArgs (MonadStatePutGet s m) = s +type instance LawBody (MonadStatePutGet s m) = m s + +type instance LawArgs (MonadStateGetPut m) = () +type instance LawBody (MonadStateGetPut m) = m () + +type instance LawArgs (MonadStateGetGet s a m) = s -> s -> m a +type instance LawBody (MonadStateGetGet s a m) = m a + + +instance (MonadStateLaws s m, TestEqual (m ())) => + LawTest (MonadStatePutPut s m) where + lawtest _ = testEqual . (monadStatePutPut :: Law (MonadStatePutPut s m)) +-- lawtest _ = testEqual . monadStatePutPut -- explicit type needed + +instance (MonadStateLaws s m, TestEqual (m s)) => + LawTest (MonadStatePutGet s m) where + lawtest _ = testEqual . (monadStatePutGet :: Law (MonadStatePutGet s m)) + +instance (MonadStateLaws s m, TestEqual (m ())) => + LawTest (MonadStateGetPut m) where + lawtest _ = testEqual . (monadStateGetPut :: Law (MonadStateGetPut m)) + +instance (MonadStateLaws s m, TestEqual (m a)) => + LawTest (MonadStateGetGet s a m) where + lawtest _ = testEqual . (monadStateGetGet :: Law (MonadStateGetGet s a m)) diff --git a/src/Control/Monad/State/Class/Laws/Instances.hs b/src/Control/Monad/State/Class/Laws/Instances.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/State/Class/Laws/Instances.hs @@ -0,0 +1,86 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +-- | Tests of the 'MonadState' laws for lazy and strict state monads. +-- The laws are one level up in the module hierarchy: +-- 'Control.Monad.State.Class.Laws.defaultMonadStatePutGet' etc. +module Control.Monad.State.Class.Laws.Instances where + +import Control.Monad.Laws + ( MonadLaws, FunctorLaws, FunctorMonadLaws + , MonadLaw1, MonadLaw2, MonadLaw3 + , FunctorLaw1, FunctorLaw2, FunctorMonadLaw + ) +import Control.Monad.State.Class.Laws + +import Test.ClassLaws +import Test.ClassLaws.TestingState + + +instance MonadStateLaws s (State s) +instance MonadLaws (State s) +instance FunctorLaws (State s) +instance FunctorMonadLaws (State s) + + +instance MonadStateLaws s (SS s) +instance MonadLaws (SS s) +instance FunctorLaws (SS s) +instance FunctorMonadLaws (SS s) +---------------------------------------------------------------------- + +testLawsStateL = do + quickLawCheck (undefined::MonadStatePutPut Bool (State Bool)) + quickLawCheck (undefined::MonadStatePutGet Bool (State Bool)) + quickLawCheck (undefined::MonadStateGetPut (State Bool)) + quickLawCheck (undefined::MonadStateGetGet Bool Ordering (State Bool)) + quickLawCheck (undefined::FunctorLaw1 () (State Bool)) + quickLawCheck (undefined::FunctorLaw2 Ordering Bool () (State Bool)) + quickLawCheck (undefined::MonadLaw1 Bool () (State Bool)) + quickLawCheck (undefined::MonadLaw2 Ordering (State Bool)) + quickLawCheck (undefined::MonadLaw3 () Ordering Bool (State Bool)) + quickLawCheck (undefined::FunctorMonadLaw () Ordering (State Bool)) + +testLawsStatePartialL = do + quickLawCheckPartial (undefined::MonadStatePutPut Bool (State Bool)) + quickLawCheckPartial (undefined::MonadStatePutGet Bool (State Bool)) + quickLawCheckPartial (undefined::MonadStateGetPut (State Bool)) + quickLawCheckPartial (undefined::MonadStateGetGet Bool Ordering (State Bool)) + quickLawCheckPartial (undefined::FunctorLaw1 () (State Bool)) + quickLawCheckPartial (undefined::FunctorLaw2 Ordering Bool () (State Bool)) + quickLawCheckPartial (undefined::MonadLaw1 Bool () (State Bool)) + quickLawCheckPartial (undefined::MonadLaw2 Ordering (State Bool)) + quickLawCheckPartial (undefined::MonadLaw3 () Ordering Bool (State Bool)) + quickLawCheckPartial (undefined::FunctorMonadLaw () Ordering (State Bool)) + +testLawsStateS = do + quickLawCheck (undefined::MonadStatePutPut Bool (SS Bool)) + quickLawCheck (undefined::MonadStatePutGet Bool (SS Bool)) + quickLawCheck (undefined::MonadStateGetPut (SS Bool)) + quickLawCheck (undefined::MonadStateGetGet Bool Ordering (SS Bool)) + quickLawCheck (undefined::FunctorLaw1 () (SS Bool)) + quickLawCheck (undefined::FunctorLaw2 Ordering Bool () (SS Bool)) + quickLawCheck (undefined::MonadLaw1 Bool () (SS Bool)) + quickLawCheck (undefined::MonadLaw2 Ordering (SS Bool)) + quickLawCheck (undefined::MonadLaw3 () Ordering Bool (SS Bool)) + quickLawCheck (undefined::FunctorMonadLaw () Ordering (SS Bool)) + +-- TODO: fix the class constraints problems (related to ChasingBottoms Data a => SemanticEq a instances) +testLawsStatePartialS = do + quickLawCheckPartial (undefined::MonadStatePutPut Bool (SS Bool)) + quickLawCheckPartial (undefined::MonadStatePutGet Bool (SS Bool)) + quickLawCheckPartial (undefined::MonadStateGetPut (SS Bool)) + -- quickLawCheckPartial (undefined::MonadStateGetGet Bool Ordering (SS Bool)) + quickLawCheckPartial (undefined::FunctorLaw1 () (SS Bool)) + quickLawCheckPartial (undefined::FunctorLaw2 Ordering Bool () (SS Bool)) + -- quickLawCheckPartial (undefined::MonadLaw1 Bool () (SS Bool)) + quickLawCheckPartial (undefined::MonadLaw2 Ordering (SS Bool)) + -- quickLawCheckPartial (undefined::MonadLaw3 () Ordering Bool (SS Bool)) + quickLawCheckPartial (undefined::FunctorMonadLaw () Ordering (SS Bool)) + +main = do + testLawsStateL + testLawsStatePartialL + testLawsStateS + testLawsStatePartialS + diff --git a/src/Data/Monoid/Laws.hs b/src/Data/Monoid/Laws.hs new file mode 100644 --- /dev/null +++ b/src/Data/Monoid/Laws.hs @@ -0,0 +1,43 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE EmptyDataDecls #-} + +-- | ClassLaws for the 'Monoid' class. Actual tests are defined in the Instances submodule and can be run from 'Data.Monoid.Laws.Instances.main'. +module Data.Monoid.Laws where +import Data.Monoid +import Test.ClassLaws + +data MonoidLaw1 m +data MonoidLaw2 m +data MonoidLaw3 m + +class Monoid m => MonoidLaws m where + + monoidLaw1 :: Law (MonoidLaw1 m) + monoidLaw2 :: Law (MonoidLaw2 m) + monoidLaw3 :: Law (MonoidLaw3 m) + + monoidLaw1 = defaultMonoidLaw1 + monoidLaw2 = defaultMonoidLaw2 + monoidLaw3 = defaultMonoidLaw3 + +defaultMonoidLaw1 m = m =.= m `mappend` mempty +defaultMonoidLaw2 m = m `mappend` mempty =.= m +defaultMonoidLaw3 (m1,m2,m3) = m1 `mappend` (m2 `mappend` m3) =.= (m1 `mappend` m2) `mappend` m3 + +type instance LawArgs (MonoidLaw1 m) = m +type instance LawBody (MonoidLaw1 m) = m + +type instance LawArgs (MonoidLaw2 m) = m +type instance LawBody (MonoidLaw2 m) = m + +type instance LawArgs (MonoidLaw3 m) = (m, m, m) +type instance LawBody (MonoidLaw3 m) = m + +instance (MonoidLaws a, TestEqual a) => LawTest (MonoidLaw1 a) where + lawtest _ = testEqual . monoidLaw1 + +instance (MonoidLaws a, TestEqual a) => LawTest (MonoidLaw2 a) where + lawtest _ = testEqual . monoidLaw2 + +instance (MonoidLaws a, TestEqual a) => LawTest (MonoidLaw3 a) where + lawtest _ = testEqual . monoidLaw3 diff --git a/src/Data/Monoid/Laws/Instances.hs b/src/Data/Monoid/Laws/Instances.hs new file mode 100644 --- /dev/null +++ b/src/Data/Monoid/Laws/Instances.hs @@ -0,0 +1,99 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverlappingInstances #-} + +-- | Conctrete tests of some instances od the 'Monoid' laws (for +-- 'Endo', mainly). The laws themselves are one level up in the module +-- hierarchy: 'Data.Monoid.Laws.defaultMonoidLaw1' etc. +module Data.Monoid.Laws.Instances where + +import Data.Monoid (Monoid(mappend, mempty), Endo(Endo), appEndo) +import Data.Monoid.Laws (MonoidLaws(..), MonoidLaw1, MonoidLaw2, MonoidLaw3) + +import Test.ClassLaws ( Equal, Law, quickLawCheck, lawtest, Property, quickCheck + , Partial(Partial), unPartial + , ArbitraryPartial(arbitraryPartial), SemanticEq((==!), semanticEq), SemanticOrd + , quickLawCheckPartial + ) + +import Test.ClassLaws.TestingDatatypes (MyList(..), (+++)) + +import Test.ClassLaws.TestingFinFuns(arbitraryPartialFun, showPartialFun, eqPartial, semEqFun) + +import Control.Monad (liftM) +import Data.List(intersperse) + +instance MonoidLaws (Endo a) + +-- | Cheating: just showing a few values (@map f [0..10]@). +instance Show (Endo Int) where + show (Endo f) = "E("++(concat $ intersperse "," $ map (show . f) [0..10])++")" + +testMonoidEndo = + do quickLawCheck (undefined::MonoidLaw1 (Endo Bool)) + quickLawCheck (undefined::MonoidLaw2 (Endo Bool)) + quickLawCheck (undefined::MonoidLaw3 (Endo Bool)) + +instance (Bounded a, Enum a, Show (Partial a)) => Show (Partial (Endo a)) where + show (Partial (Endo e)) = showPartialFun e + +instance (Bounded a, Enum a, SemanticOrd a, + ArbitraryPartial a) => ArbitraryPartial (Endo a) where + arbitraryPartial = liftM Endo (arbitraryPartialFun arbitraryPartial) + +instance (Bounded a, Enum a, Eq a) => Eq (Endo a) where + (Endo f) == (Endo g) = f == g + +{- +-- Alternative definition, needs -- {-# LANGUAGE UndecidableInstances #-} +instance SemanticEq (a->a) => SemanticEq (Endo a) where + semanticEq tweak (Endo f) (Endo g) = semanticEq tweak f g +-} +instance (Bounded a, Enum a, SemanticEq a) => SemanticEq (Endo a) where + semanticEq tweak (Endo f) (Endo g) = semEqFun semanticEq tweak f g + +testMonoidEndoPartial = do + quickLawCheckPartial (undefined::MonoidLaw1 (Endo Bool)) -- expected failure + quickLawCheckPartial (undefined::MonoidLaw2 (Endo Bool)) -- expected failure + quickLawCheckPartial (undefined::MonoidLaw3 (Endo Bool)) + +{- +The following Monoid instance for MyList does *not* satisfy the Monoid laws. +-} + +instance Monoid (MyList a) where + mempty = Nil + mappend xs ys = xs +++ ys +++ xs + +instance MonoidLaws (MyList a) + +testMonoidMyList = + do quickLawCheck (undefined :: MonoidLaw1 (MyList Int)) + quickLawCheck (undefined :: MonoidLaw2 (MyList Int)) + quickLawCheck (undefined :: MonoidLaw3 (MyList Int)) + + +main = do testMonoidEndo + testMonoidMyList -- expected failures + +-- ================================================================ +-- Just for fun: Endo Bool is also finite and bounded ... + +instance Bounded (Endo Bool) where + minBound = Endo (const False) + maxBound = Endo (const True) + +instance Enum (Endo Bool) where + fromEnum (Endo f) = 2*fromEnum (f False) + fromEnum (f True) + toEnum n = Endo (\b->if b then toEnum(n`mod`2) else toEnum (n`div`2)) + -- cheating: should really check if n is within 0..3 + +b2i :: Bool -> Int +b2i = fromEnum + +instance Show (Endo Bool) where + show (Endo f) = 'E':concatMap (show.b2i.f) [False,True] + +test_roundtrip :: Bool +test_roundtrip = (toEnum :: Int -> Endo Bool) . (fromEnum :: Endo Bool -> Int) == id diff --git a/src/Test/ClassLaws.hs b/src/Test/ClassLaws.hs new file mode 100644 --- /dev/null +++ b/src/Test/ClassLaws.hs @@ -0,0 +1,13 @@ +-- | The central part of ClassLaws is defined in the .Core, .Partial +-- and .TestingEquality. Some more helper functions and examples +-- reside in Test.ClassLaws.*. Finally, laws for the Monoid, Monad and +-- MonadState classes live under their definitions in the hierarchy: +-- Data.Monoid.Laws, Control.Monad.Laws, etc. +module Test.ClassLaws ( module Test.ClassLaws.Core + , module Test.ClassLaws.Partial + , module Test.ClassLaws.TestingEquality + , module Test.QuickCheck) where +import Test.ClassLaws.Core +import Test.ClassLaws.TestingEquality +import Test.ClassLaws.Partial +import Test.QuickCheck diff --git a/src/Test/ClassLaws/Core.hs b/src/Test/ClassLaws/Core.hs new file mode 100644 --- /dev/null +++ b/src/Test/ClassLaws/Core.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleContexts #-} + +-- | The core of ClassLaws are the type families 'LawArgs', 'LawBody' and +-- 'Param', tied together by the type class 'LawTest'. +module Test.ClassLaws.Core where +import Test.QuickCheck +import Test.ClassLaws.Partial + +-- | An equality proof is represented as a list of (at least two) equal values. +type Equal = [] +-- | A Theorem is a claim that a LHS equals a RHS - an 'Equal' of length two. +type Theorem = Equal + +infixr 0 =.= +-- | Contructing an equality theorem: @lhs =.= rhs = [lhs, rhs]@. +(=.=) :: a -> a -> Theorem a +lhs =.= rhs = [lhs, rhs] + +-- | Take a two-element "theorem" and an equality proof chain to splice in the middle. +addSteps :: Theorem a -> Equal a -> Equal a +addSteps [lhs,rhs] steps = lhs : steps ++ [rhs] +addSteps _ _ = error "addSteps should only be used on two-element lists" + + +-- | The forall quantified part on the top level of the law +type family LawArgs t +-- | The type in the body of the forall +type family LawBody t +-- | Parameters needed for 'Equal' checking of the body +type family Param b + +-- | The 'Law's we handle are of this form. +type Law t = LawArgs t -> Equal (LawBody t) + +{- | +Class LawTest defines a test method, which returns a testable property, which we +can use to test a law for a type t. This class is independent of the actual laws +to test - it can be used for Monoid, Monad, ... +-} +class LawTest t where + lawtest :: t -> LawArgs t -> Param (LawBody t) -> Property + +-- | Helper function to test laws where arguments lack a Show instance. +blindlawtest :: (LawTest t) => t -> Blind (LawArgs t) -> Param (LawBody t) -> Property +blindlawtest a (Blind f) = lawtest a f + +-- | Helper function to test laws where we should care about partial values. +partiallawtest :: (LawTest t) => t -> Partial ((LawArgs t) -> Param (LawBody t) -> Property) +partiallawtest a = Partial $ lawtest a + +-- | Top level use of ClassLaws is often @'quickLawCheck' someLaw@ +quickLawCheck :: + (Show (LawArgs t), + Arbitrary (LawArgs t), + Show (Param (LawBody t)), + Arbitrary (Param (LawBody t)), + LawTest t) => + t -> IO () +quickLawCheck = quickCheck . lawtest +-- quickLawCheck law = quickCheck (lawtest law) -- alternative version does not need expl. type sig. +-- | Variant not needing a Show instance for the 'LawArg's +quickFLawCheck law = quickCheck (blindlawtest law) + +-- | Checking laws in the precense of partial values +quickLawCheckPartial + :: ( Show (Partial (Param (LawBody t))) + , Show (Partial (LawArgs t)) + , ArbitraryPartial (Param (LawBody t)) + , ArbitraryPartial (LawArgs t) + , LawTest t) => + t -> IO () +quickLawCheckPartial = quickCheck . Partial . lawtest + diff --git a/src/Test/ClassLaws/Partial.hs b/src/Test/ClassLaws/Partial.hs new file mode 100644 --- /dev/null +++ b/src/Test/ClassLaws/Partial.hs @@ -0,0 +1,108 @@ +{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, FlexibleContexts #-} +-- | This module collects the infrastructure used to easily switch +-- between testing ClassLaws with or without partial values. Built +-- around QuickCheck and ChasingBottoms. +module Test.ClassLaws.Partial + ( module Test.ClassLaws.Partial + , module Test.ChasingBottoms + ) where +import Test.QuickCheck +import Test.ChasingBottoms hiding (Result, listOf) -- clash with QuickCheck + +import Data.List (intersperse) +import Control.Monad (liftM2, liftM3) + +-- | A modifier to indicate that partial values should be generated +-- (or tested, or both). +newtype Partial a = Partial {unPartial :: a} + +instance TestablePartial prop => Testable (Partial prop) where + property (Partial x) = propertyPartial x + +-- | Declaring a property for possibly partial values. +class TestablePartial prop where + propertyPartial :: prop -> Property + +-- | We copy the QuickCheck structure to make sure generators of +-- partial values and equality checks handling partial values are +-- used. +class ArbitraryPartial a where + arbitraryPartial :: Gen a + + shrinkPartial :: a -> [a] + shrinkPartial _ = [] + + +instance TestablePartial Bool where + propertyPartial = property + +instance TestablePartial Property where + propertyPartial = property + +instance ( ArbitraryPartial a + , Show (Partial a) + , TestablePartial prop + ) => TestablePartial (a -> prop) where + propertyPartial f = forAllShrink arb shr prop + where + arb = fmap Partial arbitraryPartial + shr (Partial x) = map Partial (shrinkPartial x) + prop (Partial x) = propertyPartial (f x) + +-------------------------------------------------------------- + +-- | Helper for showing partial values +showPartial :: String -> (a -> String) -> a -> String +showPartial t _ p | isBottom p = "_|_" ++ t ++ "_" +showPartial _ f p = f p + +instance Show (Partial ()) where + show (Partial u) = showPartial "()" show u + +instance Show (Partial Bool) where + show (Partial b) = showPartial "Bool" show b + +instance Show (Partial Char) where + show (Partial c) = showPartial "Char" show c + +instance Show (Partial Int) where + show (Partial i) = showPartial "Int" show i + +-- | Helper for generating partial values: @genPartial ib ia ga@ +-- generates 'bottom' with frequence @ib@ and @ga@ with frequency +-- @ia@. +genPartial :: Int -> Int -> Gen a -> Gen a +genPartial ib ia ga = frequency [ (ib, return bottom), (ia, ga) ] + +instance ArbitraryPartial Int where + arbitraryPartial = genPartial 1 20 $ arbitrary + +instance ArbitraryPartial Char where + arbitraryPartial = genPartial 1 20 $ arbitrary + +instance ArbitraryPartial Bool where + arbitraryPartial = genPartial 1 10 $ arbitrary + +instance ArbitraryPartial () where + arbitraryPartial = genPartial 1 5 $ arbitrary + +------------------------------------------------------------ + +instance (Show (Partial a), Show (Partial b)) => Show (Partial (a,b)) where + show = showPartial "(,)" showPair + where showPair (Partial (a,b)) = + "(" ++ show (Partial a) ++ "," + ++ show (Partial b) ++ ")" + +instance (ArbitraryPartial a, ArbitraryPartial b) => ArbitraryPartial (a,b) where + arbitraryPartial = liftM2 (,) arbitraryPartial arbitraryPartial + +instance (Show (Partial a), Show (Partial b), Show (Partial c)) => Show (Partial (a,b,c)) where + show = showPartial "(,)" showTriple + where showTriple (Partial (a,b,c)) = + "(" ++ show (Partial a) ++ "," + ++ show (Partial b) ++ "," + ++ show (Partial c) ++ ")" + +instance (ArbitraryPartial a, ArbitraryPartial b, ArbitraryPartial c) => ArbitraryPartial (a,b,c) where + arbitraryPartial = liftM3 (,,) arbitraryPartial arbitraryPartial arbitraryPartial diff --git a/src/Test/ClassLaws/TestingDatatypes.hs b/src/Test/ClassLaws/TestingDatatypes.hs new file mode 100644 --- /dev/null +++ b/src/Test/ClassLaws/TestingDatatypes.hs @@ -0,0 +1,79 @@ +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts, UndecidableInstances #-} + +-- | Some example usage of the ClassLaws framework +module Test.ClassLaws.TestingDatatypes where +import Control.Monad.State (State, runState, state, liftM) +import Data.Monoid (Endo(Endo)) +import Test.ClassLaws + +-- | To check equality of 'Endo'-functions we can generate argument values. +type instance Param (Endo a) = a + +instance (SemanticEq (Endo a), Show (Partial (Endo a))) => TestEqual (Endo a) where + testEqual l _ = testEqPartial (==!) l + +{- +instance (Eq ( a), Show (Partial a)) => TestEqual (Endo a) where + testEqual = testRunEqPartial appEndo (==) +-} + +instance (Arbitrary a, CoArbitrary a) => Arbitrary (Endo a) where + arbitrary = liftM Endo arbitrary + +-- | For lists, no 'Param'eter is needed, so we use @()@. +type instance Param [a] = () + +instance (Eq a, Show a) => TestEqual [a] where + testEqual p _ = testEq (==) p + +-- Maybe +type instance Param (Maybe a) = () + +instance (Eq a, Show a) => TestEqual (Maybe a) where + testEqual p _ = testEq (==) p + +-- State +type instance Param (State s a) = s + +instance (Eq a, Show a, Eq s, Show s) => TestEqual (State s a) where + testEqual = testRunEq runState (==) + +instance (CoArbitrary s, Arbitrary a, Arbitrary s) => Arbitrary (State s a) where + arbitrary = fmap state arbitrary + +-- | We use the MyList datatype to provide instances that do not +-- satisfy some class laws. +data MyList a = Cons a (MyList a) + | Nil + deriving (Show, Eq) + +foldrMyList :: (a -> b -> b) -> b -> MyList a -> b +foldrMyList f e Nil = e +foldrMyList f e (Cons x xs) = f x (foldrMyList f e xs) + +list2MyList :: [a] -> MyList a +list2MyList [] = Nil +list2MyList (x:xs) = Cons x (list2MyList xs) + +myList2List :: MyList a -> [a] +myList2List Nil = [] +myList2List (Cons x xs) = x:myList2List xs + +(+++) :: MyList a -> MyList a -> MyList a +Nil +++ xs = xs +(Cons y ys) +++ xs = Cons y (ys +++ xs) + +snoc :: a -> MyList a -> MyList a +snoc y Nil = Cons y Nil +snoc y (Cons x xs) = Cons x (snoc y xs) + +instance Arbitrary a => Arbitrary (MyList a) where + arbitrary = fmap list2MyList arbitrary + shrink = map list2MyList . shrink . myList2List + +type instance Param (MyList a) = () + +instance (Eq a, Show a) => TestEqual (MyList a) where + testEqual p _ = testEq (==) p diff --git a/src/Test/ClassLaws/TestingEquality.hs b/src/Test/ClassLaws/TestingEquality.hs new file mode 100644 --- /dev/null +++ b/src/Test/ClassLaws/TestingEquality.hs @@ -0,0 +1,87 @@ +{-# LANGUAGE FlexibleContexts #-} + +{- | + +The following class + helper functions implement law-agnostic testing +functionality that is used to test laws for various classes. + +-} + +module Test.ClassLaws.TestingEquality where +import Test.QuickCheck.Property + +import Test.ClassLaws.Core(Equal, Param) +import Test.ClassLaws.Partial(Partial(Partial)) + +-- | A class for types which can be checked for 'Equal'ity, possibly +-- needing some extra 'Param'eters. +class TestEqual b where + testEqual :: Equal b -> Param b -> Property + +-- | The first function, 'testRunEq', returns a property implementing +-- an equality check. It takes a function that can `run' a value and a +-- comparison operator to a predicate (which in turn takes some +-- supposedly equal values, and a parameter needed for the run +-- function, and returns a 'Property'). +testRunEq :: Show r => (t -> p -> r) -> (r -> r -> Bool) -> + (Equal t -> p -> Property) +testRunEq run (==) steps p = testEq (==) (map (`run` p) steps) + +-- | The second function, 'testEq', does the same, but now for pairs +-- that are not necessarily runnable. +testEq :: Show a => (a -> a -> Bool) -> + (Equal a -> Property) +testEq (==) steps = + whenFail (print $ failingPair (==) steps) + $ property $ liftBool $ pairwiseEq (==) steps + +---- + +-- | Variant of 'testRunEq' intended for 'Partial' values. (Only the +-- Show part differs - the user also needs to supply an equality +-- operator handling 'Partial' values.) +testRunEqPartial :: Show (Partial r) => + (t -> p -> r) -> (r -> r -> Bool) -> + (Equal t -> p -> Property) +testRunEqPartial run (==) steps p = testEqPartial (==) (map (`run` p) steps) + +-- | Similar variant of 'testEq' for 'Partial' values. +testEqPartial :: Show (Partial a) => (a -> a -> Bool) -> Equal a -> Property +testEqPartial (==) steps = + whenFail (print $ Partial (failingPair (==) steps)) + $ property $ liftBool (pairwiseEq (==) steps) + +---- + +-- | Local helper +pairwiseEq :: (r -> r -> Bool) -> [r] -> Bool +pairwiseEq (==) [] = True +pairwiseEq (==) [x] = True +pairwiseEq (==) (x:y:ys) = x==y && pairwiseEq (==) (y:ys) + +-- | Position in an equality proof +type Pos = Int + +-- | Local helper +failingPair :: (a -> a -> Bool) -> Equal a -> (Pos, a, a) +failingPair = failingPair' 1 +-- | Local helper +failingPair' pos (==) (x:y:ys) = if not (x==y) + then (pos,x,y) + else failingPair' (1+pos) (==) (y:ys) + +{- The following function generalises testEq and testRunEq +testRunEq :: Show r => + Maybe (p,r -> p -> r) -> (r -> r -> Bool) -> Equal r -> Property +testRunEq startrun (==) steps = + let run = case startrun of + Nothing -> id + Just (start,run) -> flip run start + in whenFail (print (failingPair (==) (map run steps))) + $ property + $ liftBool (pairwiseEq (==) (map run steps)) + +-- An instance of testRunEq +testEq :: Show a => (a -> a -> Bool) -> Equal a -> Property +testEq = testRunEq Nothing +-} diff --git a/src/Test/ClassLaws/TestingFinFuns.hs b/src/Test/ClassLaws/TestingFinFuns.hs new file mode 100644 --- /dev/null +++ b/src/Test/ClassLaws/TestingFinFuns.hs @@ -0,0 +1,141 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE OverlappingInstances #-} + +-- | Functions from a finite type can be shown, checked for equality, +-- and generated. We provide variants both for total and for partial +-- values. +module Test.ClassLaws.TestingFinFuns where +import Test.QuickCheck +import Test.ClassLaws.Partial + (Partial(..), ArbitraryPartial(arbitraryPartial), genPartial + , bottom, isBottom + , SemanticEq ( (==!), semanticEq ), Tweak + , SemanticOrd ( (<=!), semanticCompare, (/\!), semanticMeet, semanticJoin ) + ) +import Data.List (intersperse) +import Control.Monad (forM) + +showPartialFun :: + (Bounded a, Enum a, Show (Partial b), Show (Partial a)) => + (a -> b) -> String +showPartialFun f = + if isBottom f + then "<_bot_a->b_>" + else "<(" ++ + (concat $ intersperse "; " + [ show (Partial x) ++ "->" ++ + show (Partial (f x)) + | x <- (bottom:enumElems)]) + ++ ")>" + + +showFun :: (Enum a, Bounded a, Show a, Show b) => (a -> b) -> String +showFun f = "<(" ++ (concat $ intersperse "; " + [ show x ++ "->" ++ show (f x) + | x <- enumElems]) + ++ ")>" + +enumElems :: (Bounded a, Enum a) => [a] +enumElems = [minBound .. maxBound] + + +arbitraryPartialFun :: forall e a. + (Enum e, Bounded e, SemanticOrd a) => + Gen a -> Gen (e -> a) +arbitraryPartialFun ag = do + funtab <- forM (bottom : enumElems :: [e]) (\_ -> ag) + genPartial 1 10 (return (table2fun funtab)) + +type FunTab e a = [a] + +table2fun :: (Enum e, Bounded e, SemanticOrd a) => + FunTab e a -> (e -> a) +table2fun tab@(_:tottab) = fun + where meet = lMeet tab + fun x | isBottom x = meet + | otherwise = tail tottab !! (fromEnum x) + +lMeet :: (SemanticOrd a) => [a] -> a +lMeet [] = bottom +lMeet [x] = x +lMeet (x:xs) = x /\! lMeet xs + +------------------------------------------------------------ + +instance (Enum a, Bounded a, Show a, Show b) => + Show (a->b) where + show = showFun + +instance ( Enum e, Bounded e, Eq e + , SemanticOrd s, ArbitraryPartial s + ) => ArbitraryPartial (e -> s) where + arbitraryPartial = arbitraryPartialFun arbitraryPartial + +instance ( Enum e, Bounded e + , Show (Partial e), Show (Partial b) + ) => Show (Partial (e->b)) where + show (Partial f) = showPartialFun f +------------------------------------------------------------ + +semanticLE _ a b = case ( isBottom a, isBottom b ) of + (True, _) -> True + _ -> False +------------------------------------------------------------ + +instance (Bounded a, Enum a, Eq b) => Eq (a->b) where + f == g = all (\x -> f x == g x) enumElems + +instance (Bounded a, Enum a, SemanticEq b) => SemanticEq (a->b) where + semanticEq = semEqFun semanticEq + +type SemEq a = Tweak->a->a->Bool +semEqFun :: (Bounded a, Enum a) => SemEq b -> SemEq (a->b) +semEqFun semEqB tweak f g = eqPartial (all (\x -> semEqB tweak (f x) (g x)) + (bottom : enumElems)) + f g + +instance (Bounded a, Enum a, SemanticOrd b) => SemanticOrd (a->b) where + semanticCompare tweak f g = + case ( semanticEq tweak f g + , isBottom f + , isBottom g ) of + (True, _, _) -> Just EQ + (_, True, _) -> Just LT + (_, _, True) -> Just GT + (_, _, _) -> + if lessEqPartial (all (\x -> f x <=! g x) enumElems) f g then + Just LT + else if lessEqPartial (all (\x -> g x <=! f x) enumElems) f g then + Just GT + else + Nothing + semanticJoin tweak f g = undefined + -- semanticJoin tweak f g = case (isBottom f, isBottom g) of + -- (True, True) -> Just bottom + -- (True, False) -> Just g + -- (False, True) -> Just f + -- (False, False) -> (\x -> (\/!) (f x) (g x)) + -- propagate Nothing here how? + semanticMeet tweak f g = case (isBottom f, isBottom g) of + (False, False) -> \x -> (/\!) (f x) (g x) + (_, _) -> bottom + +------------------------------------------------------------ + + +lessEqPartial nonBotLE x y = case (isBottom x, isBottom y) of + (True, _) -> True + (False, True) -> False + (False, False) -> nonBotLE + +eqPartial nonBotEq x y = case (isBottom x, isBottom y) of + (True, True) -> True + (False, False) -> nonBotEq + _ -> False + +meetPartial q x y = case (isBottom x, isBottom y) of + (False, False) -> q + _ -> bottom + diff --git a/src/Test/ClassLaws/TestingState.hs b/src/Test/ClassLaws/TestingState.hs new file mode 100644 --- /dev/null +++ b/src/Test/ClassLaws/TestingState.hs @@ -0,0 +1,276 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverlappingInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +-- | Implementations of the infrastructure needed to test state monad +-- laws. +module Test.ClassLaws.TestingState where +import Test.ClassLaws +{- +-- More details about the imports. +import Test.QuickCheck +import Test.ChasingBottoms + ( bottom, isBottom + , SemanticEq ( (==!), semanticEq ) + , SemanticOrd ( semanticCompare, semanticMeet, semanticJoin ) + ) +import Test.ClassLaws.Partial + (Partial(..), ArbitraryPartial(arbitraryPartial), genPartial) +import Test.ClassLaws.TestingEquality + ( TestEqual(testEqual) + , testEqPartial, testEq + , testRunEqPartial, testRunEq) +-} + +import Test.ClassLaws.TestingFinFuns + +import Control.Monad.State.Class(MonadState(..)) +import Control.Monad (liftM, liftM2) + +import Data.Data + +data Pair a b = Pair a b + +fstP ~(Pair a b) = a +sndP ~(Pair a b) = b + +newtype State s a = S {runS :: s -> Pair a s} + +getState :: State s s +getState = S $ \s -> Pair s s + +putState :: s -> State s () +putState s = S $ const (Pair () s) + +returnState a = S $ \s -> Pair a s + + +bindStateL m k = S $ \s -> let (Pair a s') = runS m s + in runS (k a) s' + +fmapStateL f m = S $ \s -> let (Pair a s') = runS m s + in (Pair (f a) s') + + +bindStateS m k = S $ \s -> case runS m s of + (Pair a s') -> runS (k a) s' + +fmapStateS f m = S $ \s -> case runS m s of + (Pair a s') -> (Pair (f a) s') + +------------------------------------------------------------ + +pairFromGen :: Gen a -> Gen b -> Gen (Pair a b) +pairFromGen a b = (liftM2 Pair a b) + +pairShowPartial :: String -> Pair a b -> String +pairShowPartial _ p | isBottom p = "_|_P_" +pairShowPartial pab (Pair a b) = pab + +basicPairShow :: (a-> String) -> (b -> String) -> Pair a b -> String +basicPairShow sa sb (Pair a b) = "("++sa a++", "++sb b++")" + +instance (Arbitrary a, Arbitrary b) => Arbitrary (Pair a b) where + arbitrary = pairFromGen arbitrary arbitrary + +instance (CoArbitrary a, CoArbitrary b) => CoArbitrary (Pair a b) where + coarbitrary (Pair a b) = variant 1 . coarbitrary a . coarbitrary b + +instance (Show a, Show b) => Show (Pair a b) where + show = basicPairShow show show + +instance (ArbitraryPartial a, ArbitraryPartial b) => + ArbitraryPartial (Pair a b) where + arbitraryPartial = genPartial 1 9 $ pairFromGen arbitraryPartial arbitraryPartial + +instance (Show (Partial a), Show (Partial b)) => + Show (Partial (Pair a b)) where + show (Partial p) = pairShowPartial (basicPairShow (show.Partial) (show.Partial) p) p + +------------------------------------------------------------ + +instance ( Arbitrary a + , Arbitrary s + , CoArbitrary s + ) => Arbitrary (State s a) where + arbitrary = liftM S arbitrary + +instance (Enum s, Bounded s, Show a, Show s) => + Show (State s a) where + show (S f) = "(S " ++ show f ++ ")" + +instance ( ArbitraryPartial a, SemanticOrd a + , ArbitraryPartial s, SemanticOrd s + , Enum s, Bounded s, Eq s + ) => ArbitraryPartial (State s a) where + arbitraryPartial = genPartial 1 20 (liftM S arbitraryPartial) + +instance (Enum s, Bounded s, Show (Partial a), Show (Partial s)) => + Show (Partial (State s a)) where + show (Partial s) | isBottom s = "_|_St_" + show (Partial (S f)) = "(S " ++ show (Partial f) ++ ")" + +------------------------------------------------------------ + +instance (Eq a, Eq b) => Eq (Pair a b) where + px == py = pairRecPatt (==) (==) (&&) px py + +instance (SemanticEq a, SemanticEq b) => SemanticEq (Pair a b) where + semanticEq tweak x y = + -- case ( isBottomTimeOut (timeOutLimit tweak) x + -- , isBottomTimeOut (timeOutLimit tweak) y ) of + case ( isBottom x, isBottom y ) of + (True, True) -> True + (False, False) -> + ((semanticEq tweak) (fstP x) (fstP y)) && + ((semanticEq tweak) (sndP x) (sndP y)) + _ -> False + +instance (SemanticOrd a, SemanticOrd b) => SemanticOrd (Pair a b) where + semanticCompare tweak x y = + case ( semanticEq tweak x y + , isBottom x + , isBottom y ) of + (True, _, _) -> Just EQ + (_, True, _) -> Just LT + (_, _, True) -> Just GT + (_, _, _) -> + case (l == r) of + True -> l + _ -> Nothing + where + l = semanticCompare tweak (fstP x) (fstP y) + r = semanticCompare tweak (sndP x) (sndP y) + semanticJoin tweak x y = case (isBottom x, isBottom y) of + (True, True) -> Just bottom + (True, False) -> Just y + (False, True) -> Just x + -- (False, True) -> cast x + (False, False) -> case ( semanticJoin tweak (fstP x) (fstP y) + , semanticJoin tweak (sndP x) (sndP y)) of + (Nothing, _) -> Nothing + (_, Nothing) -> Nothing + (Just fst, Just snd) -> Just $ Pair fst snd + semanticMeet tweak x y = case (isBottom x, isBottom y) of + (True, _) -> bottom + (_, True) -> bottom + (False, False) -> Pair (semanticMeet tweak (fstP x) (fstP y)) + (semanticMeet tweak (sndP x) (sndP y)) + +-- -- semanticLE _tweak a b = case ( isBottomTimeOut (timeOutLimit tweak) a +-- -- , isBottomTimeOut (timeOutLimit tweak) b ) of +-- semanticLE _ a b = case ( isBottom a, isBottom b ) of +-- (True, _) -> True +-- _ -> False + +pairRecPatt :: (a->a->ta) -> (b->b->tb) -> (ta->tb->t) -> Pair a b -> Pair a b -> t +pairRecPatt opA opB topOp px py = topOp (opA (fstP px) (fstP py)) (opB (sndP px) (sndP py)) + +------------------------------------------------------------ + +instance (Enum a, Bounded a, Eq a, Eq b) => Eq (State a b) where + (==) x y = eqPartial q x y + where q = statePatt (==) x y + +instance (Enum a, Bounded a, SemanticEq a, SemanticEq b) => SemanticEq (State a b) where + semanticEq tweak x y = eqPartial q x y + where q = statePatt (semanticEq tweak) x y +instance (Enum a, Bounded a, SemanticOrd a, SemanticOrd b) => SemanticOrd (State a b) where + semanticCompare tweak x y = + case ( semanticEq tweak x y + , isBottom x + , isBottom y ) of + (True, _, _) -> Just EQ + (_, True, _) -> Just LT + (_, _, True) -> Just GT + (_, _, _) -> statePatt (semanticCompare tweak) x y + semanticJoin tweak x y = error "TODO: semanticJoin for State not yet implemented" + -- semanticJoin tweak f g = case (isBottom f, isBottom g) of + -- (True, True) -> Just bottom + -- (True, False) -> Just g + -- (False, True) -> Just f + -- (False, False) -> (\x -> (\/!) (f x) (g x)) + -- propagate Nothing here how? + semanticMeet tweak x y = case (isBottom x, isBottom y) of + (False, False) -> S $ statePatt (semanticMeet tweak) x y + (_, _) -> bottom + +statePatt op (S f1) (S f2) = op f1 f2 + +------------------------------------------------------------ + +instance Arbitrary Ordering where + arbitrary = enumTotArb $ zip [1,1,1] $ enumElems + +instance CoArbitrary Ordering where + coarbitrary = coarbitrary . fromEnum + +instance ArbitraryPartial Ordering where + arbitraryPartial = genPartial 1 9 $ enumTotArb $ + zip [1,1,1] $ enumElems + +instance Show (Partial Ordering) where + show = enumShowBot_auxLst ["Ord", "LT", "EQ", "GT"] . unPartial + +enumTotArb :: [(Int,a)] -> Gen a +enumTotArb as = frequency $ map (\(f,a) -> (f,return a)) as + +enumShowBot_auxLst :: (Bounded a, Enum a) => [String] -> a -> String +enumShowBot_auxLst (s:ss) x | isBottom x = "_|_"++s++"_" +enumShowBot_auxLst (s:ss) x = ss !! fromEnum x + + + + + +-- instances for the lazy state +instance Monad (State s) where + return = returnState + (>>=) = bindStateL + +instance Functor (State s) where + fmap = fmapStateL + +instance Monad (State s) => MonadState s (State s) where + get = getState + put = putState + + +instance ( SemanticEq a, Show (Partial a) + , SemanticEq s, Show (Partial s) + , Bounded s, Enum s) => TestEqual (State s a) where + testEqual eq _ = testEqPartial (==!) (map runS eq) + +type instance Param (State s a) = s + +---------------------------------------------------------------------- +newtype SS s a = SS {unSS :: State s a} + deriving( Arbitrary, Show, ArbitraryPartial, MonadState s) + +instance ( SemanticEq a, Show (Partial a) + , SemanticEq s, Show (Partial s) + , Bounded s, Enum s) => TestEqual (SS s a) where + testEqual eq _ = testEqPartial (==!) (map unSS eq) +instance (Enum s, Bounded s, Show (Partial a), Show (Partial s)) => + Show (Partial (SS s a)) where + show (Partial (SS x)) = show (Partial x) + + + +instance Monad (SS s) where + return = SS . returnState + (SS m) >>= k = bindSS + where + bindSS = SS $ S $ \s -> case runS m s of + (Pair a s') -> x s' + where + SS (S x) = k a + +instance Functor (SS s) where + fmap f (SS m) = SS $ S $ \s -> case runS m s of + (Pair a s') -> (Pair (f a) s') + +type instance Param (SS s a) = s