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

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

instance PartialOrd N5 where
    N5
N5o leq :: N5 -> N5 -> Bool
`leq` N5
_   = Bool
True
    N5
_   `leq` N5
N5i = Bool
True
    N5
N5a `leq` N5
N5a = Bool
True
    N5
N5b `leq` N5
N5a = Bool
True
    N5
N5b `leq` N5
N5b = Bool
True
    N5
N5c `leq` N5
N5c = Bool
True
    N5
_   `leq` N5
_   = Bool
False

instance Lattice N5 where
    N5
N5o \/ :: N5 -> N5 -> N5
\/ N5
y   = N5
y
    N5
N5i \/ N5
_   = N5
N5i
    N5
x   \/ N5
N5o = N5
x
    N5
_   \/ N5
N5i = N5
N5i
    N5
N5a \/ N5
N5a = N5
N5a
    N5
N5a \/ N5
N5b = N5
N5a
    N5
N5b \/ N5
N5a = N5
N5a
    N5
N5b \/ N5
N5b = N5
N5b
    N5
N5c \/ N5
N5c = N5
N5c
    N5
_   \/ N5
_   = N5
N5i

    N5
N5o /\ :: N5 -> N5 -> N5
/\ N5
_   = N5
N5o
    N5
N5i /\ N5
y   = N5
y
    N5
_   /\ N5
N5o = N5
N5o
    N5
x   /\ N5
N5i = N5
x
    N5
N5a /\ N5
N5a = N5
N5a
    N5
N5b /\ N5
N5b = N5
N5b
    N5
N5a /\ N5
N5b = N5
N5b
    N5
N5b /\ N5
N5a = N5
N5b
    N5
N5c /\ N5
N5c = N5
N5c
    N5
_   /\ N5
_   = N5
N5o

instance BoundedJoinSemiLattice N5 where
    bottom :: N5
bottom = N5
N5o

instance BoundedMeetSemiLattice N5 where
    top :: N5
top = N5
N5i

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

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

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

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

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

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