packages feed

ClassLaws (empty) → 0.3.0.0

raw patch · 16 files changed

+1517/−0 lines, 16 filesdep +ChasingBottomsdep +QuickCheckdep +basesetup-changed

Dependencies added: ChasingBottoms, QuickCheck, base, mtl

Files

+ ClassLaws.cabal view
@@ -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+
+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/Control/Monad/Laws.hs view
@@ -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
+ src/Control/Monad/Laws/Instances.hs view
@@ -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. +
+ src/Control/Monad/State/Class/Laws.hs view
@@ -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))
+ src/Control/Monad/State/Class/Laws/Instances.hs view
@@ -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+
+ src/Data/Monoid/Laws.hs view
@@ -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
+ src/Data/Monoid/Laws/Instances.hs view
@@ -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
+ src/Test/ClassLaws.hs view
@@ -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
+ src/Test/ClassLaws/Core.hs view
@@ -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+
+ src/Test/ClassLaws/Partial.hs view
@@ -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
+ src/Test/ClassLaws/TestingDatatypes.hs view
@@ -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
+ src/Test/ClassLaws/TestingEquality.hs view
@@ -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+-}
+ src/Test/ClassLaws/TestingFinFuns.hs view
@@ -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+
+ src/Test/ClassLaws/TestingState.hs view
@@ -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