{-# 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 Prelude ()
import Prelude.Compat

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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: M2 -> M2 -> Bool
$c/= :: M2 -> M2 -> Bool
== :: M2 -> M2 -> Bool
$c== :: M2 -> M2 -> Bool
Eq, Eq 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
min :: M2 -> M2 -> M2
$cmin :: M2 -> M2 -> M2
max :: M2 -> M2 -> M2
$cmax :: M2 -> M2 -> M2
>= :: M2 -> M2 -> Bool
$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
compare :: M2 -> M2 -> Ordering
$ccompare :: M2 -> M2 -> Ordering
Ord, ReadPrec [M2]
ReadPrec M2
Int -> ReadS M2
ReadS [M2]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [M2]
$creadListPrec :: ReadPrec [M2]
readPrec :: ReadPrec M2
$creadPrec :: ReadPrec M2
readList :: ReadS [M2]
$creadList :: ReadS [M2]
readsPrec :: Int -> ReadS M2
$creadsPrec :: Int -> ReadS M2
Read, Int -> M2 -> ShowS
[M2] -> ShowS
M2 -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M2] -> ShowS
$cshowList :: [M2] -> ShowS
show :: M2 -> String
$cshow :: M2 -> String
showsPrec :: Int -> M2 -> ShowS
$cshowsPrec :: Int -> M2 -> ShowS
Show, Int -> M2
M2 -> Int
M2 -> [M2]
M2 -> M2
M2 -> M2 -> [M2]
M2 -> M2 -> M2 -> [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
enumFromThenTo :: M2 -> M2 -> M2 -> [M2]
$cenumFromThenTo :: M2 -> M2 -> M2 -> [M2]
enumFromTo :: M2 -> M2 -> [M2]
$cenumFromTo :: M2 -> M2 -> [M2]
enumFromThen :: M2 -> M2 -> [M2]
$cenumFromThen :: M2 -> M2 -> [M2]
enumFrom :: M2 -> [M2]
$cenumFrom :: M2 -> [M2]
fromEnum :: M2 -> Int
$cfromEnum :: M2 -> Int
toEnum :: Int -> M2
$ctoEnum :: Int -> M2
pred :: M2 -> M2
$cpred :: M2 -> M2
succ :: M2 -> M2
$csucc :: M2 -> M2
Enum, M2
forall a. a -> a -> Bounded a
maxBound :: M2
$cmaxBound :: M2
minBound :: M2
$cminBound :: M2
Bounded, Typeable, Typeable M2
M2 -> DataType
M2 -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M2 -> m M2
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M2 -> m M2
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> M2 -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> M2 -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> M2 -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> M2 -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M2 -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M2 -> r
gmapT :: (forall b. Data b => b -> b) -> M2 -> M2
$cgmapT :: (forall b. Data b => b -> b) -> M2 -> M2
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M2)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M2)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M2)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M2)
dataTypeOf :: M2 -> DataType
$cdataTypeOf :: M2 -> DataType
toConstr :: M2 -> Constr
$ctoConstr :: M2 -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M2
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M2
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M2 -> c M2
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M2 -> c M2
Data, 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
$cto :: forall x. Rep M2 x -> M2
$cfrom :: forall x. M2 -> Rep M2 x
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 = forall a. Monoid a => a
mempty
toSetBool M2
M2a = forall a. a -> Set a
Set.singleton Bool
False
toSetBool M2
M2b = forall a. a -> Set a
Set.singleton Bool
True
toSetBool M2
M2i = 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 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 = forall a. (Bounded a, Enum a) => Gen a
QC.arbitraryBoundedEnum
    shrink :: M2 -> [M2]
shrink M2
x | M2
x forall a. Eq a => a -> a -> Bool
== forall a. Bounded a => a
minBound = []
             | Bool
otherwise     = [forall a. Bounded a => a
minBound .. forall a. Enum a => a -> a
pred M2
x]

instance QC.CoArbitrary M2 where
    coarbitrary :: forall b. M2 -> Gen b -> Gen b
coarbitrary = 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 = forall a b. (Eq a, Bounded a, Enum a) => (a -> b) -> a :-> b
QC.functionBoundedEnum

instance Universe M2 where universe :: [M2]
universe = [forall a. Bounded a => a
minBound .. 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 seq :: forall a b. a -> b -> b
`seq` ()

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