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

-- | The simplest Heyting algebra that is not already a Boolean algebra is the
-- totally ordered set \(\{ 0, \frac{1}{2}, 1 \}\).
--
data ZeroHalfOne = Zero | Half | One
  deriving (ZeroHalfOne -> ZeroHalfOne -> Bool
(ZeroHalfOne -> ZeroHalfOne -> Bool)
-> (ZeroHalfOne -> ZeroHalfOne -> Bool) -> Eq ZeroHalfOne
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ZeroHalfOne -> ZeroHalfOne -> Bool
$c/= :: ZeroHalfOne -> ZeroHalfOne -> Bool
== :: ZeroHalfOne -> ZeroHalfOne -> Bool
$c== :: ZeroHalfOne -> ZeroHalfOne -> Bool
Eq, Eq ZeroHalfOne
Eq ZeroHalfOne
-> (ZeroHalfOne -> ZeroHalfOne -> Ordering)
-> (ZeroHalfOne -> ZeroHalfOne -> Bool)
-> (ZeroHalfOne -> ZeroHalfOne -> Bool)
-> (ZeroHalfOne -> ZeroHalfOne -> Bool)
-> (ZeroHalfOne -> ZeroHalfOne -> Bool)
-> (ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne)
-> (ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne)
-> Ord ZeroHalfOne
ZeroHalfOne -> ZeroHalfOne -> Bool
ZeroHalfOne -> ZeroHalfOne -> Ordering
ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
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 :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
$cmin :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
max :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
$cmax :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
>= :: ZeroHalfOne -> ZeroHalfOne -> Bool
$c>= :: ZeroHalfOne -> ZeroHalfOne -> Bool
> :: ZeroHalfOne -> ZeroHalfOne -> Bool
$c> :: ZeroHalfOne -> ZeroHalfOne -> Bool
<= :: ZeroHalfOne -> ZeroHalfOne -> Bool
$c<= :: ZeroHalfOne -> ZeroHalfOne -> Bool
< :: ZeroHalfOne -> ZeroHalfOne -> Bool
$c< :: ZeroHalfOne -> ZeroHalfOne -> Bool
compare :: ZeroHalfOne -> ZeroHalfOne -> Ordering
$ccompare :: ZeroHalfOne -> ZeroHalfOne -> Ordering
$cp1Ord :: Eq ZeroHalfOne
Ord, ReadPrec [ZeroHalfOne]
ReadPrec ZeroHalfOne
Int -> ReadS ZeroHalfOne
ReadS [ZeroHalfOne]
(Int -> ReadS ZeroHalfOne)
-> ReadS [ZeroHalfOne]
-> ReadPrec ZeroHalfOne
-> ReadPrec [ZeroHalfOne]
-> Read ZeroHalfOne
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [ZeroHalfOne]
$creadListPrec :: ReadPrec [ZeroHalfOne]
readPrec :: ReadPrec ZeroHalfOne
$creadPrec :: ReadPrec ZeroHalfOne
readList :: ReadS [ZeroHalfOne]
$creadList :: ReadS [ZeroHalfOne]
readsPrec :: Int -> ReadS ZeroHalfOne
$creadsPrec :: Int -> ReadS ZeroHalfOne
Read, Int -> ZeroHalfOne -> ShowS
[ZeroHalfOne] -> ShowS
ZeroHalfOne -> String
(Int -> ZeroHalfOne -> ShowS)
-> (ZeroHalfOne -> String)
-> ([ZeroHalfOne] -> ShowS)
-> Show ZeroHalfOne
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ZeroHalfOne] -> ShowS
$cshowList :: [ZeroHalfOne] -> ShowS
show :: ZeroHalfOne -> String
$cshow :: ZeroHalfOne -> String
showsPrec :: Int -> ZeroHalfOne -> ShowS
$cshowsPrec :: Int -> ZeroHalfOne -> ShowS
Show, Int -> ZeroHalfOne
ZeroHalfOne -> Int
ZeroHalfOne -> [ZeroHalfOne]
ZeroHalfOne -> ZeroHalfOne
ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne]
ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne]
(ZeroHalfOne -> ZeroHalfOne)
-> (ZeroHalfOne -> ZeroHalfOne)
-> (Int -> ZeroHalfOne)
-> (ZeroHalfOne -> Int)
-> (ZeroHalfOne -> [ZeroHalfOne])
-> (ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne])
-> (ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne])
-> (ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne])
-> Enum ZeroHalfOne
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 :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne]
$cenumFromThenTo :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne]
enumFromTo :: ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne]
$cenumFromTo :: ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne]
enumFromThen :: ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne]
$cenumFromThen :: ZeroHalfOne -> ZeroHalfOne -> [ZeroHalfOne]
enumFrom :: ZeroHalfOne -> [ZeroHalfOne]
$cenumFrom :: ZeroHalfOne -> [ZeroHalfOne]
fromEnum :: ZeroHalfOne -> Int
$cfromEnum :: ZeroHalfOne -> Int
toEnum :: Int -> ZeroHalfOne
$ctoEnum :: Int -> ZeroHalfOne
pred :: ZeroHalfOne -> ZeroHalfOne
$cpred :: ZeroHalfOne -> ZeroHalfOne
succ :: ZeroHalfOne -> ZeroHalfOne
$csucc :: ZeroHalfOne -> ZeroHalfOne
Enum, ZeroHalfOne
ZeroHalfOne -> ZeroHalfOne -> Bounded ZeroHalfOne
forall a. a -> a -> Bounded a
maxBound :: ZeroHalfOne
$cmaxBound :: ZeroHalfOne
minBound :: ZeroHalfOne
$cminBound :: ZeroHalfOne
Bounded, Typeable, Typeable ZeroHalfOne
DataType
Constr
Typeable ZeroHalfOne
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> ZeroHalfOne -> c ZeroHalfOne)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c ZeroHalfOne)
-> (ZeroHalfOne -> Constr)
-> (ZeroHalfOne -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c ZeroHalfOne))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c ZeroHalfOne))
-> ((forall b. Data b => b -> b) -> ZeroHalfOne -> ZeroHalfOne)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ZeroHalfOne -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ZeroHalfOne -> r)
-> (forall u. (forall d. Data d => d -> u) -> ZeroHalfOne -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ZeroHalfOne -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne)
-> Data ZeroHalfOne
ZeroHalfOne -> DataType
ZeroHalfOne -> Constr
(forall b. Data b => b -> b) -> ZeroHalfOne -> ZeroHalfOne
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ZeroHalfOne -> c ZeroHalfOne
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ZeroHalfOne
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) -> ZeroHalfOne -> u
forall u. (forall d. Data d => d -> u) -> ZeroHalfOne -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ZeroHalfOne -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ZeroHalfOne -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ZeroHalfOne
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ZeroHalfOne -> c ZeroHalfOne
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ZeroHalfOne)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ZeroHalfOne)
$cOne :: Constr
$cHalf :: Constr
$cZero :: Constr
$tZeroHalfOne :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne
gmapMp :: (forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne
gmapM :: (forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> ZeroHalfOne -> m ZeroHalfOne
gmapQi :: Int -> (forall d. Data d => d -> u) -> ZeroHalfOne -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ZeroHalfOne -> u
gmapQ :: (forall d. Data d => d -> u) -> ZeroHalfOne -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ZeroHalfOne -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ZeroHalfOne -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ZeroHalfOne -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ZeroHalfOne -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ZeroHalfOne -> r
gmapT :: (forall b. Data b => b -> b) -> ZeroHalfOne -> ZeroHalfOne
$cgmapT :: (forall b. Data b => b -> b) -> ZeroHalfOne -> ZeroHalfOne
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ZeroHalfOne)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c ZeroHalfOne)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c ZeroHalfOne)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c ZeroHalfOne)
dataTypeOf :: ZeroHalfOne -> DataType
$cdataTypeOf :: ZeroHalfOne -> DataType
toConstr :: ZeroHalfOne -> Constr
$ctoConstr :: ZeroHalfOne -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ZeroHalfOne
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c ZeroHalfOne
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ZeroHalfOne -> c ZeroHalfOne
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> ZeroHalfOne -> c ZeroHalfOne
$cp1Data :: Typeable ZeroHalfOne
Data, (forall x. ZeroHalfOne -> Rep ZeroHalfOne x)
-> (forall x. Rep ZeroHalfOne x -> ZeroHalfOne)
-> Generic ZeroHalfOne
forall x. Rep ZeroHalfOne x -> ZeroHalfOne
forall x. ZeroHalfOne -> Rep ZeroHalfOne x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ZeroHalfOne x -> ZeroHalfOne
$cfrom :: forall x. ZeroHalfOne -> Rep ZeroHalfOne x
Generic)

instance PartialOrd ZeroHalfOne where
    leq :: ZeroHalfOne -> ZeroHalfOne -> Bool
leq = ZeroHalfOne -> ZeroHalfOne -> Bool
forall a. Ord a => a -> a -> Bool
(<=)

instance Lattice ZeroHalfOne where
    \/ :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
(\/) = ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
forall a. Ord a => a -> a -> a
max
    /\ :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
(/\) = ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
forall a. Ord a => a -> a -> a
min

instance BoundedJoinSemiLattice ZeroHalfOne where
    bottom :: ZeroHalfOne
bottom = ZeroHalfOne
Zero

instance BoundedMeetSemiLattice ZeroHalfOne where
    top :: ZeroHalfOne
top = ZeroHalfOne
One

-- | Not boolean: @'neg' 'Half' '\/' 'Half' = 'Half' /= 'One'@
instance Heyting ZeroHalfOne where
    ZeroHalfOne
Zero ==> :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
==> ZeroHalfOne
_    = ZeroHalfOne
One
    ZeroHalfOne
One  ==> ZeroHalfOne
x    = ZeroHalfOne
x
    ZeroHalfOne
Half ==> ZeroHalfOne
Zero = ZeroHalfOne
Zero
    ZeroHalfOne
Half ==> ZeroHalfOne
_    = ZeroHalfOne
One

    neg :: ZeroHalfOne -> ZeroHalfOne
neg ZeroHalfOne
Zero = ZeroHalfOne
One
    neg ZeroHalfOne
One  = ZeroHalfOne
Zero
    neg ZeroHalfOne
Half = ZeroHalfOne
Zero

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

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

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

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

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

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