{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Algebra.Boolean
( BooleanAlgebra
, (==>)
, not
, iff
, iff'
, Boolean
, runBoolean
, boolean
, prop_not
, prop_BooleanAlgebra
) where
import Prelude hiding (not)
import Control.Applicative (Const (..))
import Data.Data (Data, Typeable)
import Data.Functor.Identity (Identity (..))
import Data.Proxy (Proxy (..))
import Data.Semigroup (All (..), Any (..), Endo (..))
import Data.Tagged (Tagged (..))
import Data.Universe.Class (Finite)
import qualified Data.Set as S
import GHC.Generics (Generic)
#ifdef EXPORT_PROPERTIES
import Test.QuickCheck hiding ((==>))
#endif
import Algebra.Lattice ( Lattice
, BoundedLattice
, JoinSemiLattice (..)
, BoundedJoinSemiLattice
, MeetSemiLattice (..)
, BoundedMeetSemiLattice
, bottom
, top
)
import Algebra.Heyting ( HeytingAlgebra (..)
, iff
, iff'
, not
, toBoolean
, prop_HeytingAlgebra
)
class HeytingAlgebra a => BooleanAlgebra a
newtype Boolean a = Boolean
{ runBoolean :: a
}
deriving
( JoinSemiLattice, BoundedJoinSemiLattice, MeetSemiLattice
, BoundedMeetSemiLattice, Lattice, BoundedLattice, HeytingAlgebra
, Eq, Ord, Read, Show, Bounded, Typeable, Data, Generic
)
instance HeytingAlgebra a => BooleanAlgebra (Boolean a)
instance (Arbitrary a, HeytingAlgebra a) => Arbitrary (Boolean a) where
arbitrary = boolean <$> arbitrary
shrink (Boolean a) = [ boolean a' | a' <- shrink a ]
boolean :: HeytingAlgebra a => a -> Boolean a
boolean = Boolean . toBoolean
instance BooleanAlgebra Bool
instance BooleanAlgebra All
instance BooleanAlgebra Any
instance BooleanAlgebra ()
instance BooleanAlgebra (Proxy a)
instance BooleanAlgebra a => BooleanAlgebra (Tagged t a)
instance BooleanAlgebra b => BooleanAlgebra (a -> b)
instance BooleanAlgebra a => BooleanAlgebra (Identity a)
instance BooleanAlgebra a => BooleanAlgebra (Const a b)
instance BooleanAlgebra a => BooleanAlgebra (Endo a)
instance (BooleanAlgebra a, BooleanAlgebra b) => BooleanAlgebra (a, b)
instance (Ord a, Finite a) => BooleanAlgebra (S.Set a)
#ifdef EXPORT_PROPERTIES
prop_not :: (HeytingAlgebra a, Eq a, Show a) => a -> Property
prop_not a =
counterexample "not (not a) /= a" (not (not a) === a)
.&&. counterexample "not a ∧ a /= bottom" (not a /\ a === bottom)
.&&. counterexample "not a ∨ a /= top" (not a \/ a === top)
prop_BooleanAlgebra :: (BooleanAlgebra a, Eq a, Show a)
=> a -> a -> a -> Property
prop_BooleanAlgebra a b c =
prop_HeytingAlgebra a b c
.&&. prop_not a
#endif