{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric      #-}
{-# LANGUAGE Safe               #-}
----------------------------------------------------------------------------
-- |
-- Module      :  Algebra.Lattice.M2
-- Copyright   :  (C) 2019 Oleg Grenrus
-- License     :  BSD-3-Clause (see the file LICENSE)
--
-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>
--
----------------------------------------------------------------------------
module Algebra.Lattice.M2 (
    M2 (..),
    toSetBool,
    fromSetBool,
    ) where

import Control.DeepSeq     (NFData (..))
import Data.Data           (Data, Typeable)
import Data.Hashable       (Hashable (..))
import Data.Universe.Class (Finite (..), Universe (..))
import GHC.Generics        (Generic)

import qualified Test.QuickCheck as QC

import Algebra.Heyting
import Algebra.Lattice
import Algebra.PartialOrd

import           Data.Set (Set)
import qualified Data.Set as Set

-- | \(M_2\) is isomorphic to \(\mathcal{P}\{\mathbb{B}\}\), i.e. powerset of 'Bool'.
--
-- <<m2.png>>
--
data M2 = M2o | M2a | M2b | M2i
  deriving (M2 -> M2 -> Bool
(M2 -> M2 -> Bool) -> (M2 -> M2 -> Bool) -> Eq M2
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: M2 -> M2 -> Bool
== :: M2 -> M2 -> Bool
$c/= :: M2 -> M2 -> Bool
/= :: M2 -> M2 -> Bool
Eq, Eq M2
Eq M2 =>
(M2 -> M2 -> Ordering)
-> (M2 -> M2 -> Bool)
-> (M2 -> M2 -> Bool)
-> (M2 -> M2 -> Bool)
-> (M2 -> M2 -> Bool)
-> (M2 -> M2 -> M2)
-> (M2 -> M2 -> M2)
-> Ord M2
M2 -> M2 -> Bool
M2 -> M2 -> Ordering
M2 -> M2 -> M2
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: M2 -> M2 -> Ordering
compare :: M2 -> M2 -> Ordering
$c< :: M2 -> M2 -> Bool
< :: M2 -> M2 -> Bool
$c<= :: M2 -> M2 -> Bool
<= :: M2 -> M2 -> Bool
$c> :: M2 -> M2 -> Bool
> :: M2 -> M2 -> Bool
$c>= :: M2 -> M2 -> Bool
>= :: M2 -> M2 -> Bool
$cmax :: M2 -> M2 -> M2
max :: M2 -> M2 -> M2
$cmin :: M2 -> M2 -> M2
min :: M2 -> M2 -> M2
Ord, ReadPrec [M2]
ReadPrec M2
Int -> ReadS M2
ReadS [M2]
(Int -> ReadS M2)
-> ReadS [M2] -> ReadPrec M2 -> ReadPrec [M2] -> Read M2
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS M2
readsPrec :: Int -> ReadS M2
$creadList :: ReadS [M2]
readList :: ReadS [M2]
$creadPrec :: ReadPrec M2
readPrec :: ReadPrec M2
$creadListPrec :: ReadPrec [M2]
readListPrec :: ReadPrec [M2]
Read, Int -> M2 -> ShowS
[M2] -> ShowS
M2 -> String
(Int -> M2 -> ShowS)
-> (M2 -> String) -> ([M2] -> ShowS) -> Show M2
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> M2 -> ShowS
showsPrec :: Int -> M2 -> ShowS
$cshow :: M2 -> String
show :: M2 -> String
$cshowList :: [M2] -> ShowS
showList :: [M2] -> ShowS
Show, Int -> M2
M2 -> Int
M2 -> [M2]
M2 -> M2
M2 -> M2 -> [M2]
M2 -> M2 -> M2 -> [M2]
(M2 -> M2)
-> (M2 -> M2)
-> (Int -> M2)
-> (M2 -> Int)
-> (M2 -> [M2])
-> (M2 -> M2 -> [M2])
-> (M2 -> M2 -> [M2])
-> (M2 -> M2 -> M2 -> [M2])
-> Enum M2
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: M2 -> M2
succ :: M2 -> M2
$cpred :: M2 -> M2
pred :: M2 -> M2
$ctoEnum :: Int -> M2
toEnum :: Int -> M2
$cfromEnum :: M2 -> Int
fromEnum :: M2 -> Int
$cenumFrom :: M2 -> [M2]
enumFrom :: M2 -> [M2]
$cenumFromThen :: M2 -> M2 -> [M2]
enumFromThen :: M2 -> M2 -> [M2]
$cenumFromTo :: M2 -> M2 -> [M2]
enumFromTo :: M2 -> M2 -> [M2]
$cenumFromThenTo :: M2 -> M2 -> M2 -> [M2]
enumFromThenTo :: M2 -> M2 -> M2 -> [M2]
Enum, M2
M2 -> M2 -> Bounded M2
forall a. a -> a -> Bounded a
$cminBound :: M2
minBound :: M2
$cmaxBound :: M2
maxBound :: M2
Bounded, Typeable, Typeable M2
Typeable M2 =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> M2 -> c M2)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c M2)
-> (M2 -> Constr)
-> (M2 -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c M2))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M2))
-> ((forall b. Data b => b -> b) -> M2 -> M2)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M2 -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M2 -> r)
-> (forall u. (forall d. Data d => d -> u) -> M2 -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> M2 -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> M2 -> m M2)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> M2 -> m M2)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> M2 -> m M2)
-> Data M2
M2 -> Constr
M2 -> DataType
(forall b. Data b => b -> b) -> M2 -> M2
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> M2 -> u
forall u. (forall d. Data d => d -> u) -> M2 -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M2 -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M2 -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M2 -> m M2
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M2 -> m M2
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M2
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M2 -> c M2
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M2)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M2)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M2 -> c M2
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M2 -> c M2
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M2
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M2
$ctoConstr :: M2 -> Constr
toConstr :: M2 -> Constr
$cdataTypeOf :: M2 -> DataType
dataTypeOf :: M2 -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M2)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M2)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M2)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M2)
$cgmapT :: (forall b. Data b => b -> b) -> M2 -> M2
gmapT :: (forall b. Data b => b -> b) -> M2 -> M2
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M2 -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M2 -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M2 -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M2 -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> M2 -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> M2 -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> M2 -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> M2 -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M2 -> m M2
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M2 -> m M2
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M2 -> m M2
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M2 -> m M2
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M2 -> m M2
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M2 -> m M2
Data, (forall x. M2 -> Rep M2 x)
-> (forall x. Rep M2 x -> M2) -> Generic M2
forall x. Rep M2 x -> M2
forall x. M2 -> Rep M2 x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. M2 -> Rep M2 x
from :: forall x. M2 -> Rep M2 x
$cto :: forall x. Rep M2 x -> M2
to :: forall x. Rep M2 x -> M2
Generic)

instance PartialOrd M2 where
    M2
M2o leq :: M2 -> M2 -> Bool
`leq` M2
_   = Bool
True
    M2
_   `leq` M2
M2i = Bool
True
    M2
M2a `leq` M2
M2a = Bool
True
    M2
M2b `leq` M2
M2b = Bool
True
    M2
_   `leq` M2
_   = Bool
False

instance Lattice M2 where
    M2
M2o \/ :: M2 -> M2 -> M2
\/ M2
y   = M2
y
    M2
M2i \/ M2
_   = M2
M2i
    M2
x   \/ M2
M2o = M2
x
    M2
_   \/ M2
M2i = M2
M2i
    M2
M2a \/ M2
M2a = M2
M2a
    M2
M2b \/ M2
M2b = M2
M2b
    M2
_   \/ M2
_   = M2
M2i

    M2
M2o /\ :: M2 -> M2 -> M2
/\ M2
_   = M2
M2o
    M2
M2i /\ M2
y   = M2
y
    M2
_   /\ M2
M2o = M2
M2o
    M2
x   /\ M2
M2i = M2
x
    M2
M2a /\ M2
M2a = M2
M2a
    M2
M2b /\ M2
M2b = M2
M2b
    M2
_   /\ M2
_   = M2
M2o

instance BoundedJoinSemiLattice M2 where
    bottom :: M2
bottom = M2
M2o

instance BoundedMeetSemiLattice M2 where
    top :: M2
top = M2
M2i

instance Heyting M2 where
    M2
M2o ==> :: M2 -> M2 -> M2
==> M2
_   = M2
M2i
    M2
M2i ==> M2
x   = M2
x

    M2
M2a ==> M2
M2o = M2
M2b
    M2
M2a ==> M2
M2a = M2
M2i
    M2
M2a ==> M2
M2b = M2
M2b
    M2
M2a ==> M2
M2i = M2
M2i

    M2
M2b ==> M2
M2o = M2
M2a
    M2
M2b ==> M2
M2a = M2
M2a
    M2
M2b ==> M2
M2b = M2
M2i
    M2
M2b ==> M2
M2i = M2
M2i

    neg :: M2 -> M2
neg M2
M2o = M2
M2i
    neg M2
M2a = M2
M2b
    neg M2
M2b = M2
M2a
    neg M2
M2i = M2
M2o

toSetBool :: M2 -> Set Bool
toSetBool :: M2 -> Set Bool
toSetBool M2
M2o = Set Bool
forall a. Monoid a => a
mempty
toSetBool M2
M2a = Bool -> Set Bool
forall a. a -> Set a
Set.singleton Bool
False
toSetBool M2
M2b = Bool -> Set Bool
forall a. a -> Set a
Set.singleton Bool
True
toSetBool M2
M2i = [Bool] -> Set Bool
forall a. Ord a => [a] -> Set a
Set.fromList [Bool
True, Bool
False]

fromSetBool :: Set Bool -> M2
fromSetBool :: Set Bool -> M2
fromSetBool Set Bool
x = case Set Bool -> [Bool]
forall a. Set a -> [a]
Set.toList Set Bool
x of
    [Bool
False,Bool
True] -> M2
M2i
    [Bool
False]      -> M2
M2a
    [Bool
True]       -> M2
M2b
    [Bool]
_            -> M2
M2o

instance QC.Arbitrary M2 where
    arbitrary :: Gen M2
arbitrary = Gen M2
forall a. (Bounded a, Enum a) => Gen a
QC.arbitraryBoundedEnum
    shrink :: M2 -> [M2]
shrink M2
x | M2
x M2 -> M2 -> Bool
forall a. Eq a => a -> a -> Bool
== M2
forall a. Bounded a => a
minBound = []
             | Bool
otherwise     = [M2
forall a. Bounded a => a
minBound .. M2 -> M2
forall a. Enum a => a -> a
pred M2
x]

instance QC.CoArbitrary M2 where
    coarbitrary :: forall b. M2 -> Gen b -> Gen b
coarbitrary = M2 -> Gen b -> Gen b
forall a b. Enum a => a -> Gen b -> Gen b
QC.coarbitraryEnum

instance QC.Function M2 where
    function :: forall b. (M2 -> b) -> M2 :-> b
function = (M2 -> b) -> M2 :-> b
forall a b. (Eq a, Bounded a, Enum a) => (a -> b) -> a :-> b
QC.functionBoundedEnum

instance Universe M2 where universe :: [M2]
universe = [M2
forall a. Bounded a => a
minBound .. M2
forall a. Bounded a => a
maxBound]
instance Finite M2 where cardinality :: Tagged M2 Natural
cardinality = Tagged M2 Natural
4

instance NFData M2 where
    rnf :: M2 -> ()
rnf M2
x = M2
x M2 -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance Hashable M2 where
    hashWithSalt :: Int -> M2 -> Int
hashWithSalt Int
salt = Int -> Int -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt (Int -> Int) -> (M2 -> Int) -> M2 -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M2 -> Int
forall a. Enum a => a -> Int
fromEnum