{-# 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
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
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
Ord, ReadPrec [ZeroHalfOne]
ReadPrec ZeroHalfOne
Int -> ReadS ZeroHalfOne
ReadS [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
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]
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
forall a. a -> a -> Bounded a
maxBound :: ZeroHalfOne
$cmaxBound :: ZeroHalfOne
minBound :: ZeroHalfOne
$cminBound :: ZeroHalfOne
Bounded, Typeable, Typeable ZeroHalfOne
ZeroHalfOne -> DataType
ZeroHalfOne -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> ZeroHalfOne -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> ZeroHalfOne -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> ZeroHalfOne -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> ZeroHalfOne -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, 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 = forall a. Ord a => a -> a -> Bool
(<=)

instance Lattice ZeroHalfOne where
    \/ :: ZeroHalfOne -> ZeroHalfOne -> ZeroHalfOne
(\/) = forall a. Ord a => a -> a -> a
max
    /\ :: 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 = forall a. (Bounded a, Enum a) => Gen a
QC.arbitraryBoundedEnum
    shrink :: ZeroHalfOne -> [ZeroHalfOne]
shrink ZeroHalfOne
x | ZeroHalfOne
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 ZeroHalfOne
x]

instance QC.CoArbitrary ZeroHalfOne where
    coarbitrary :: forall b. ZeroHalfOne -> Gen b -> Gen b
coarbitrary = 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 = forall a b. (Eq a, Bounded a, Enum a) => (a -> b) -> a :-> b
QC.functionBoundedEnum

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

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