{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric      #-}
{-# LANGUAGE Safe               #-}
----------------------------------------------------------------------------
-- |
-- Module      :  Algebra.Lattice.M3
-- Copyright   :  (C) 2019 Oleg Grenrus
-- License     :  BSD-3-Clause (see the file LICENSE)
--
-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>
--
----------------------------------------------------------------------------
module Algebra.Lattice.M3 (
    M3 (..),
    ) 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.Lattice
import Algebra.PartialOrd

-- | \(M_3\), is smallest non-distributive, yet modular lattice.
--
-- <<m3.png>>
--
data M3 = M3o | M3a | M3b | M3c | M3i
  deriving (M3 -> M3 -> Bool
(M3 -> M3 -> Bool) -> (M3 -> M3 -> Bool) -> Eq M3
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: M3 -> M3 -> Bool
$c/= :: M3 -> M3 -> Bool
== :: M3 -> M3 -> Bool
$c== :: M3 -> M3 -> Bool
Eq, Eq M3
Eq M3
-> (M3 -> M3 -> Ordering)
-> (M3 -> M3 -> Bool)
-> (M3 -> M3 -> Bool)
-> (M3 -> M3 -> Bool)
-> (M3 -> M3 -> Bool)
-> (M3 -> M3 -> M3)
-> (M3 -> M3 -> M3)
-> Ord M3
M3 -> M3 -> Bool
M3 -> M3 -> Ordering
M3 -> M3 -> M3
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 :: M3 -> M3 -> M3
$cmin :: M3 -> M3 -> M3
max :: M3 -> M3 -> M3
$cmax :: M3 -> M3 -> M3
>= :: M3 -> M3 -> Bool
$c>= :: M3 -> M3 -> Bool
> :: M3 -> M3 -> Bool
$c> :: M3 -> M3 -> Bool
<= :: M3 -> M3 -> Bool
$c<= :: M3 -> M3 -> Bool
< :: M3 -> M3 -> Bool
$c< :: M3 -> M3 -> Bool
compare :: M3 -> M3 -> Ordering
$ccompare :: M3 -> M3 -> Ordering
$cp1Ord :: Eq M3
Ord, ReadPrec [M3]
ReadPrec M3
Int -> ReadS M3
ReadS [M3]
(Int -> ReadS M3)
-> ReadS [M3] -> ReadPrec M3 -> ReadPrec [M3] -> Read M3
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [M3]
$creadListPrec :: ReadPrec [M3]
readPrec :: ReadPrec M3
$creadPrec :: ReadPrec M3
readList :: ReadS [M3]
$creadList :: ReadS [M3]
readsPrec :: Int -> ReadS M3
$creadsPrec :: Int -> ReadS M3
Read, Int -> M3 -> ShowS
[M3] -> ShowS
M3 -> String
(Int -> M3 -> ShowS)
-> (M3 -> String) -> ([M3] -> ShowS) -> Show M3
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [M3] -> ShowS
$cshowList :: [M3] -> ShowS
show :: M3 -> String
$cshow :: M3 -> String
showsPrec :: Int -> M3 -> ShowS
$cshowsPrec :: Int -> M3 -> ShowS
Show, Int -> M3
M3 -> Int
M3 -> [M3]
M3 -> M3
M3 -> M3 -> [M3]
M3 -> M3 -> M3 -> [M3]
(M3 -> M3)
-> (M3 -> M3)
-> (Int -> M3)
-> (M3 -> Int)
-> (M3 -> [M3])
-> (M3 -> M3 -> [M3])
-> (M3 -> M3 -> [M3])
-> (M3 -> M3 -> M3 -> [M3])
-> Enum M3
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 :: M3 -> M3 -> M3 -> [M3]
$cenumFromThenTo :: M3 -> M3 -> M3 -> [M3]
enumFromTo :: M3 -> M3 -> [M3]
$cenumFromTo :: M3 -> M3 -> [M3]
enumFromThen :: M3 -> M3 -> [M3]
$cenumFromThen :: M3 -> M3 -> [M3]
enumFrom :: M3 -> [M3]
$cenumFrom :: M3 -> [M3]
fromEnum :: M3 -> Int
$cfromEnum :: M3 -> Int
toEnum :: Int -> M3
$ctoEnum :: Int -> M3
pred :: M3 -> M3
$cpred :: M3 -> M3
succ :: M3 -> M3
$csucc :: M3 -> M3
Enum, M3
M3 -> M3 -> Bounded M3
forall a. a -> a -> Bounded a
maxBound :: M3
$cmaxBound :: M3
minBound :: M3
$cminBound :: M3
Bounded, Typeable, Typeable M3
DataType
Constr
Typeable M3
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> M3 -> c M3)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c M3)
-> (M3 -> Constr)
-> (M3 -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c M3))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M3))
-> ((forall b. Data b => b -> b) -> M3 -> M3)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M3 -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M3 -> r)
-> (forall u. (forall d. Data d => d -> u) -> M3 -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> M3 -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> M3 -> m M3)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> M3 -> m M3)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> M3 -> m M3)
-> Data M3
M3 -> DataType
M3 -> Constr
(forall b. Data b => b -> b) -> M3 -> M3
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M3 -> c M3
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M3
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) -> M3 -> u
forall u. (forall d. Data d => d -> u) -> M3 -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M3 -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M3 -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M3 -> m M3
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M3 -> m M3
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M3
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M3 -> c M3
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M3)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M3)
$cM3i :: Constr
$cM3c :: Constr
$cM3b :: Constr
$cM3a :: Constr
$cM3o :: Constr
$tM3 :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> M3 -> m M3
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M3 -> m M3
gmapMp :: (forall d. Data d => d -> m d) -> M3 -> m M3
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> M3 -> m M3
gmapM :: (forall d. Data d => d -> m d) -> M3 -> m M3
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> M3 -> m M3
gmapQi :: Int -> (forall d. Data d => d -> u) -> M3 -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> M3 -> u
gmapQ :: (forall d. Data d => d -> u) -> M3 -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> M3 -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M3 -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> M3 -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M3 -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> M3 -> r
gmapT :: (forall b. Data b => b -> b) -> M3 -> M3
$cgmapT :: (forall b. Data b => b -> b) -> M3 -> M3
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M3)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c M3)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c M3)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c M3)
dataTypeOf :: M3 -> DataType
$cdataTypeOf :: M3 -> DataType
toConstr :: M3 -> Constr
$ctoConstr :: M3 -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M3
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c M3
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M3 -> c M3
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> M3 -> c M3
$cp1Data :: Typeable M3
Data, (forall x. M3 -> Rep M3 x)
-> (forall x. Rep M3 x -> M3) -> Generic M3
forall x. Rep M3 x -> M3
forall x. M3 -> Rep M3 x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep M3 x -> M3
$cfrom :: forall x. M3 -> Rep M3 x
Generic)

instance PartialOrd M3 where
    M3
M3o leq :: M3 -> M3 -> Bool
`leq` M3
_   = Bool
True
    M3
_   `leq` M3
M3i = Bool
True
    M3
M3a `leq` M3
M3a = Bool
True
    M3
M3b `leq` M3
M3b = Bool
True
    M3
M3c `leq` M3
M3c = Bool
True
    M3
_   `leq` M3
_   = Bool
False

instance Lattice M3 where
    M3
M3o \/ :: M3 -> M3 -> M3
\/ M3
y   = M3
y
    M3
M3i \/ M3
_   = M3
M3i
    M3
x   \/ M3
M3o = M3
x
    M3
_   \/ M3
M3i = M3
M3i
    M3
M3a \/ M3
M3a = M3
M3a
    M3
M3b \/ M3
M3b = M3
M3b
    M3
M3c \/ M3
M3c = M3
M3c
    M3
_   \/ M3
_   = M3
M3i

    M3
M3o /\ :: M3 -> M3 -> M3
/\ M3
_   = M3
M3o
    M3
M3i /\ M3
y   = M3
y
    M3
_   /\ M3
M3o = M3
M3o
    M3
x   /\ M3
M3i = M3
x
    M3
M3a /\ M3
M3a = M3
M3a
    M3
M3b /\ M3
M3b = M3
M3b
    M3
M3c /\ M3
M3c = M3
M3c
    M3
_   /\ M3
_   = M3
M3o

instance BoundedJoinSemiLattice M3 where
    bottom :: M3
bottom = M3
M3o

instance BoundedMeetSemiLattice M3 where
    top :: M3
top = M3
M3i

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

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

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

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

instance NFData M3 where
    rnf :: M3 -> ()
rnf M3
x = M3
x M3 -> () -> ()
`seq` ()

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