{-# 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
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
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
Ord, ReadPrec [N5]
ReadPrec N5
Int -> ReadS N5
ReadS [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
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]
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
forall a. a -> a -> Bounded a
maxBound :: N5
$cmaxBound :: N5
minBound :: N5
$cminBound :: N5
Bounded, Typeable, Typeable N5
N5 -> DataType
N5 -> Constr
(forall b. Data b => b -> b) -> N5 -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> N5 -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> N5 -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> N5 -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> N5 -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, 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 = forall a. (Bounded a, Enum a) => Gen a
QC.arbitraryBoundedEnum
    shrink :: N5 -> [N5]
shrink N5
x | N5
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 N5
x]

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

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

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

instance Hashable N5 where
    hashWithSalt :: Int -> N5 -> 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