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