{-# LANGUAGE MultiParamTypeClasses #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Data.Boolean
-- Copyright   :  (c) Masahiro Sakai 2012-2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Type classes for lattices and boolean algebras.
--
-----------------------------------------------------------------------------
module ToySolver.Data.Boolean
  (
  -- * Boolean algebra
    MonotoneBoolean (..)
  , Complement (..)
  , IfThenElse (..)
  , iteBoolean
  , Boolean (..)
  ) where

import Control.Arrow

infixr 3 .&&.
infixr 2 .||.
infixr 1 .=>.
infix 1 .<=>.

class MonotoneBoolean a where
  true, false :: a
  (.&&.) :: a -> a -> a
  (.||.) :: a -> a -> a
  andB :: [a] -> a
  orB :: [a] -> a

  true = [a] -> a
forall a. MonotoneBoolean a => [a] -> a
andB []
  false = [a] -> a
forall a. MonotoneBoolean a => [a] -> a
orB []
  a
a .&&. a
b = [a] -> a
forall a. MonotoneBoolean a => [a] -> a
andB [a
a,a
b]
  a
a .||. a
b = [a] -> a
forall a. MonotoneBoolean a => [a] -> a
orB [a
a,a
b]

  andB [] = a
forall a. MonotoneBoolean a => a
true
  andB [a
a] = a
a
  andB [a]
xs = (a -> a -> a) -> [a] -> a
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
(.&&.) [a]
xs

  orB [] = a
forall a. MonotoneBoolean a => a
false
  orB [a
a] = a
a
  orB [a]
xs = (a -> a -> a) -> [a] -> a
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
(.||.) [a]
xs

  {-# MINIMAL ((true, (.&&.)) | andB), ((false, (.||.)) | orB) #-}

-- | types that can be negated.
class Complement a where
  notB :: a -> a

class IfThenElse b a where
  ite :: b -> a -> a -> a

iteBoolean :: Boolean a => a -> a -> a -> a
iteBoolean :: forall a. Boolean a => a -> a -> a -> a
iteBoolean a
c a
t a
e = (a
c a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
.&&. a
t) a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
.||. (a -> a
forall a. Complement a => a -> a
notB a
c a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
.&&. a
e)

-- | types that can be combined with boolean operations.
class (MonotoneBoolean a, Complement a, IfThenElse a a) => Boolean a where
  (.=>.), (.<=>.) :: a -> a -> a

  a
x .=>. a
y = a -> a
forall a. Complement a => a -> a
notB a
x a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
.||. a
y
  a
x .<=>. a
y = (a
x a -> a -> a
forall a. Boolean a => a -> a -> a
.=>. a
y) a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
.&&. (a
y a -> a -> a
forall a. Boolean a => a -> a -> a
.=>. a
x)


instance (Complement a, Complement b) => Complement (a, b) where
  notB :: (a, b) -> (a, b)
notB (a
a,b
b) = (a -> a
forall a. Complement a => a -> a
notB a
a, b -> b
forall a. Complement a => a -> a
notB b
b)

instance (MonotoneBoolean a, MonotoneBoolean b) => MonotoneBoolean (a, b) where
  true :: (a, b)
true = (a
forall a. MonotoneBoolean a => a
true, b
forall a. MonotoneBoolean a => a
true)
  false :: (a, b)
false = (a
forall a. MonotoneBoolean a => a
false, b
forall a. MonotoneBoolean a => a
false)
  (a
xs1,b
ys1) .&&. :: (a, b) -> (a, b) -> (a, b)
.&&. (a
xs2,b
ys2) = (a
xs1 a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
.&&. a
xs2, b
ys1 b -> b -> b
forall a. MonotoneBoolean a => a -> a -> a
.&&. b
ys2)
  (a
xs1,b
ys1) .||. :: (a, b) -> (a, b) -> (a, b)
.||. (a
xs2,b
ys2) = (a
xs1 a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
.||. a
xs2, b
ys1 b -> b -> b
forall a. MonotoneBoolean a => a -> a -> a
.||. b
ys2)
  andB :: [(a, b)] -> (a, b)
andB = ([a] -> a
forall a. MonotoneBoolean a => [a] -> a
andB ([a] -> a) -> ([b] -> b) -> ([a], [b]) -> (a, b)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [b] -> b
forall a. MonotoneBoolean a => [a] -> a
andB) (([a], [b]) -> (a, b))
-> ([(a, b)] -> ([a], [b])) -> [(a, b)] -> (a, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, b)] -> ([a], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip
  orB :: [(a, b)] -> (a, b)
orB  = ([a] -> a
forall a. MonotoneBoolean a => [a] -> a
orB ([a] -> a) -> ([b] -> b) -> ([a], [b]) -> (a, b)
forall b c b' c'. (b -> c) -> (b' -> c') -> (b, b') -> (c, c')
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [b] -> b
forall a. MonotoneBoolean a => [a] -> a
orB) (([a], [b]) -> (a, b))
-> ([(a, b)] -> ([a], [b])) -> [(a, b)] -> (a, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(a, b)] -> ([a], [b])
forall a b. [(a, b)] -> ([a], [b])
unzip

instance (Boolean a, Boolean b) => IfThenElse (a, b) (a, b) where
  ite :: (a, b) -> (a, b) -> (a, b) -> (a, b)
ite (a
c1,b
c2) (a
t1,b
t2) (a
e1,b
e2) = (a -> a -> a -> a
forall b a. IfThenElse b a => b -> a -> a -> a
ite a
c1 a
t1 a
e1, b -> b -> b -> b
forall b a. IfThenElse b a => b -> a -> a -> a
ite b
c2 b
t2 b
e2)

instance (Boolean a, Boolean b) => Boolean (a, b) where
  (a
xs1,b
ys1) .=>. :: (a, b) -> (a, b) -> (a, b)
.=>. (a
xs2,b
ys2) = (a
xs1 a -> a -> a
forall a. Boolean a => a -> a -> a
.=>. a
xs2, b
ys1 b -> b -> b
forall a. Boolean a => a -> a -> a
.=>. b
ys2)
  (a
xs1,b
ys1) .<=>. :: (a, b) -> (a, b) -> (a, b)
.<=>. (a
xs2,b
ys2) = (a
xs1 a -> a -> a
forall a. Boolean a => a -> a -> a
.<=>. a
xs2, b
ys1 b -> b -> b
forall a. Boolean a => a -> a -> a
.<=>. b
ys2)

instance Complement a => Complement (b -> a) where
  notB :: (b -> a) -> b -> a
notB b -> a
f = \b
x -> a -> a
forall a. Complement a => a -> a
notB (b -> a
f b
x)

instance MonotoneBoolean a => MonotoneBoolean (b -> a) where
  true :: b -> a
true = a -> b -> a
forall a b. a -> b -> a
const a
forall a. MonotoneBoolean a => a
true
  false :: b -> a
false = a -> b -> a
forall a b. a -> b -> a
const a
forall a. MonotoneBoolean a => a
false
  b -> a
f .&&. :: (b -> a) -> (b -> a) -> b -> a
.&&. b -> a
g = \b
x -> b -> a
f b
x a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
.&&. b -> a
g b
x
  b -> a
f .||. :: (b -> a) -> (b -> a) -> b -> a
.||. b -> a
g = \b
x -> b -> a
f b
x a -> a -> a
forall a. MonotoneBoolean a => a -> a -> a
.||. b -> a
g b
x
  andB :: [b -> a] -> b -> a
andB [b -> a]
fs = \b
x -> [a] -> a
forall a. MonotoneBoolean a => [a] -> a
andB [b -> a
f b
x | b -> a
f <- [b -> a]
fs]
  orB :: [b -> a] -> b -> a
orB [b -> a]
fs = \b
x -> [a] -> a
forall a. MonotoneBoolean a => [a] -> a
orB [b -> a
f b
x | b -> a
f <- [b -> a]
fs]

instance (Boolean a) => IfThenElse (b -> a) (b -> a) where
  ite :: (b -> a) -> (b -> a) -> (b -> a) -> b -> a
ite b -> a
c b -> a
t b -> a
e = \b
x -> a -> a -> a -> a
forall b a. IfThenElse b a => b -> a -> a -> a
ite (b -> a
c b
x) (b -> a
t b
x) (b -> a
e b
x)

instance (Boolean a) => Boolean (b -> a) where
  b -> a
f .=>. :: (b -> a) -> (b -> a) -> b -> a
.=>. b -> a
g = \b
x -> b -> a
f b
x a -> a -> a
forall a. Boolean a => a -> a -> a
.=>. b -> a
g b
x
  b -> a
f .<=>. :: (b -> a) -> (b -> a) -> b -> a
.<=>. b -> a
g = \b
x -> b -> a
f b
x a -> a -> a
forall a. Boolean a => a -> a -> a
.<=>. b -> a
g b
x


instance Complement Bool where
  notB :: Bool -> Bool
notB = Bool -> Bool
not

instance MonotoneBoolean Bool where
  true :: Bool
true  = Bool
True
  false :: Bool
false = Bool
False
  .&&. :: Bool -> Bool -> Bool
(.&&.) = Bool -> Bool -> Bool
(&&)
  .||. :: Bool -> Bool -> Bool
(.||.) = Bool -> Bool -> Bool
(||)

instance IfThenElse Bool Bool where
  ite :: Bool -> Bool -> Bool -> Bool
ite Bool
c Bool
t Bool
e = if Bool
c then Bool
t else Bool
e

instance Boolean Bool where
  .<=>. :: Bool -> Bool -> Bool
(.<=>.) = Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==)