{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveFoldable      #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DeriveTraversable   #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE Safe                #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators       #-}
----------------------------------------------------------------------------
-- |
-- Module      :  Algebra.Lattice.Ordered
-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015-2019 Oleg Grenrus
-- License     :  BSD-3-Clause (see the file LICENSE)
--
-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>
--
----------------------------------------------------------------------------
module Algebra.Lattice.Ordered (
    Ordered(..)
  ) where

import Prelude ()
import Prelude.Compat

import Algebra.Heyting
import Algebra.Lattice
import Algebra.PartialOrd

import Control.DeepSeq       (NFData (..))
import Control.Monad         (ap)
import Data.Data             (Data, Typeable)
import Data.Hashable         (Hashable (..))
import Data.Universe.Class   (Finite (..), Universe (..))
import Data.Universe.Helpers (Natural, Tagged, retag)
import GHC.Generics          (Generic, Generic1)

import qualified Test.QuickCheck as QC

--
-- Ordered
--

-- | A total order gives rise to a lattice. Join is
-- 'max', meet is 'min'.
newtype Ordered a = Ordered { forall a. Ordered a -> a
getOrdered :: a }
  deriving ( Ordered a -> Ordered a -> Bool
forall a. Eq a => Ordered a -> Ordered a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Ordered a -> Ordered a -> Bool
$c/= :: forall a. Eq a => Ordered a -> Ordered a -> Bool
== :: Ordered a -> Ordered a -> Bool
$c== :: forall a. Eq a => Ordered a -> Ordered a -> Bool
Eq, Ordered a -> Ordered a -> Bool
Ordered a -> Ordered a -> Ordering
Ordered a -> Ordered a -> Ordered a
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
forall {a}. Ord a => Eq (Ordered a)
forall a. Ord a => Ordered a -> Ordered a -> Bool
forall a. Ord a => Ordered a -> Ordered a -> Ordering
forall a. Ord a => Ordered a -> Ordered a -> Ordered a
min :: Ordered a -> Ordered a -> Ordered a
$cmin :: forall a. Ord a => Ordered a -> Ordered a -> Ordered a
max :: Ordered a -> Ordered a -> Ordered a
$cmax :: forall a. Ord a => Ordered a -> Ordered a -> Ordered a
>= :: Ordered a -> Ordered a -> Bool
$c>= :: forall a. Ord a => Ordered a -> Ordered a -> Bool
> :: Ordered a -> Ordered a -> Bool
$c> :: forall a. Ord a => Ordered a -> Ordered a -> Bool
<= :: Ordered a -> Ordered a -> Bool
$c<= :: forall a. Ord a => Ordered a -> Ordered a -> Bool
< :: Ordered a -> Ordered a -> Bool
$c< :: forall a. Ord a => Ordered a -> Ordered a -> Bool
compare :: Ordered a -> Ordered a -> Ordering
$ccompare :: forall a. Ord a => Ordered a -> Ordered a -> Ordering
Ord, Int -> Ordered a -> ShowS
forall a. Show a => Int -> Ordered a -> ShowS
forall a. Show a => [Ordered a] -> ShowS
forall a. Show a => Ordered a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Ordered a] -> ShowS
$cshowList :: forall a. Show a => [Ordered a] -> ShowS
show :: Ordered a -> String
$cshow :: forall a. Show a => Ordered a -> String
showsPrec :: Int -> Ordered a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Ordered a -> ShowS
Show, ReadPrec [Ordered a]
ReadPrec (Ordered a)
ReadS [Ordered a]
forall a. Read a => ReadPrec [Ordered a]
forall a. Read a => ReadPrec (Ordered a)
forall a. Read a => Int -> ReadS (Ordered a)
forall a. Read a => ReadS [Ordered a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Ordered a]
$creadListPrec :: forall a. Read a => ReadPrec [Ordered a]
readPrec :: ReadPrec (Ordered a)
$creadPrec :: forall a. Read a => ReadPrec (Ordered a)
readList :: ReadS [Ordered a]
$creadList :: forall a. Read a => ReadS [Ordered a]
readsPrec :: Int -> ReadS (Ordered a)
$creadsPrec :: forall a. Read a => Int -> ReadS (Ordered a)
Read, Ordered a -> DataType
Ordered a -> Constr
forall {a}. Data a => Typeable (Ordered a)
forall a. Data a => Ordered a -> DataType
forall a. Data a => Ordered a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Ordered a -> Ordered a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Ordered a -> u
forall a u.
Data a =>
(forall d. Data d => d -> u) -> Ordered a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ordered a -> r
forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ordered a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Ordered a -> m (Ordered a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ordered a -> m (Ordered a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ordered a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ordered a -> c (Ordered a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ordered a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ordered a))
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 (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ordered a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ordered a -> c (Ordered a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ordered a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ordered a -> m (Ordered a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ordered a -> m (Ordered a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ordered a -> m (Ordered a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ordered a -> m (Ordered a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ordered a -> m (Ordered a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Ordered a -> m (Ordered a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ordered a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Ordered a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Ordered a -> [u]
$cgmapQ :: forall a u.
Data a =>
(forall d. Data d => d -> u) -> Ordered a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ordered a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Ordered a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ordered a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Ordered a -> r
gmapT :: (forall b. Data b => b -> b) -> Ordered a -> Ordered a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Ordered a -> Ordered a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ordered a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Ordered a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ordered a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ordered a))
dataTypeOf :: Ordered a -> DataType
$cdataTypeOf :: forall a. Data a => Ordered a -> DataType
toConstr :: Ordered a -> Constr
$ctoConstr :: forall a. Data a => Ordered a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ordered a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ordered a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ordered a -> c (Ordered a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ordered a -> c (Ordered a)
Data, Typeable, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Ordered a) x -> Ordered a
forall a x. Ordered a -> Rep (Ordered a) x
$cto :: forall a x. Rep (Ordered a) x -> Ordered a
$cfrom :: forall a x. Ordered a -> Rep (Ordered a) x
Generic, forall a b. a -> Ordered b -> Ordered a
forall a b. (a -> b) -> Ordered a -> Ordered b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> Ordered b -> Ordered a
$c<$ :: forall a b. a -> Ordered b -> Ordered a
fmap :: forall a b. (a -> b) -> Ordered a -> Ordered b
$cfmap :: forall a b. (a -> b) -> Ordered a -> Ordered b
Functor, forall a. Eq a => a -> Ordered a -> Bool
forall a. Num a => Ordered a -> a
forall a. Ord a => Ordered a -> a
forall m. Monoid m => Ordered m -> m
forall a. Ordered a -> Bool
forall a. Ordered a -> Int
forall a. Ordered a -> [a]
forall a. (a -> a -> a) -> Ordered a -> a
forall m a. Monoid m => (a -> m) -> Ordered a -> m
forall b a. (b -> a -> b) -> b -> Ordered a -> b
forall a b. (a -> b -> b) -> b -> Ordered a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: forall a. Num a => Ordered a -> a
$cproduct :: forall a. Num a => Ordered a -> a
sum :: forall a. Num a => Ordered a -> a
$csum :: forall a. Num a => Ordered a -> a
minimum :: forall a. Ord a => Ordered a -> a
$cminimum :: forall a. Ord a => Ordered a -> a
maximum :: forall a. Ord a => Ordered a -> a
$cmaximum :: forall a. Ord a => Ordered a -> a
elem :: forall a. Eq a => a -> Ordered a -> Bool
$celem :: forall a. Eq a => a -> Ordered a -> Bool
length :: forall a. Ordered a -> Int
$clength :: forall a. Ordered a -> Int
null :: forall a. Ordered a -> Bool
$cnull :: forall a. Ordered a -> Bool
toList :: forall a. Ordered a -> [a]
$ctoList :: forall a. Ordered a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Ordered a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Ordered a -> a
foldr1 :: forall a. (a -> a -> a) -> Ordered a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Ordered a -> a
foldl' :: forall b a. (b -> a -> b) -> b -> Ordered a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Ordered a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Ordered a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Ordered a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Ordered a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Ordered a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Ordered a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Ordered a -> b
foldMap' :: forall m a. Monoid m => (a -> m) -> Ordered a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Ordered a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Ordered a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Ordered a -> m
fold :: forall m. Monoid m => Ordered m -> m
$cfold :: forall m. Monoid m => Ordered m -> m
Foldable, Functor Ordered
Foldable Ordered
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Ordered (m a) -> m (Ordered a)
forall (f :: * -> *) a.
Applicative f =>
Ordered (f a) -> f (Ordered a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ordered a -> m (Ordered b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ordered a -> f (Ordered b)
sequence :: forall (m :: * -> *) a. Monad m => Ordered (m a) -> m (Ordered a)
$csequence :: forall (m :: * -> *) a. Monad m => Ordered (m a) -> m (Ordered a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ordered a -> m (Ordered b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Ordered a -> m (Ordered b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Ordered (f a) -> f (Ordered a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Ordered (f a) -> f (Ordered a)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ordered a -> f (Ordered b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ordered a -> f (Ordered b)
Traversable
           , forall a. Rep1 Ordered a -> Ordered a
forall a. Ordered a -> Rep1 Ordered a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cto1 :: forall a. Rep1 Ordered a -> Ordered a
$cfrom1 :: forall a. Ordered a -> Rep1 Ordered a
Generic1
           )

instance Applicative Ordered where
  pure :: forall a. a -> Ordered a
pure = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. Ordered (a -> b) -> Ordered a -> Ordered b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad Ordered where
  return :: forall a. a -> Ordered a
return           = forall a. a -> Ordered a
Ordered
  Ordered a
x >>= :: forall a b. Ordered a -> (a -> Ordered b) -> Ordered b
>>= a -> Ordered b
f  = a -> Ordered b
f a
x

instance NFData a => NFData (Ordered a) where
  rnf :: Ordered a -> ()
rnf (Ordered a
a) = forall a. NFData a => a -> ()
rnf a
a

instance Hashable a => Hashable (Ordered a)

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

instance (Ord a, Bounded a) => BoundedJoinSemiLattice (Ordered a) where
  bottom :: Ordered a
bottom = forall a. a -> Ordered a
Ordered forall a. Bounded a => a
minBound

instance (Ord a, Bounded a) => BoundedMeetSemiLattice (Ordered a) where
  top :: Ordered a
top = forall a. a -> Ordered a
Ordered forall a. Bounded a => a
maxBound

-- | This is interesting logic, as it satisfies both de Morgan laws;
-- but isn't Boolean: i.e. law of exluded middle doesn't hold.
--
-- Negation "smashes" value into 'minBound' or 'maxBound'.
instance (Ord a, Bounded a) => Heyting (Ordered a) where
    Ordered a
x ==> :: Ordered a -> Ordered a -> Ordered a
==> Ordered a
y | Ordered a
x forall a. Ord a => a -> a -> Bool
> Ordered a
y     = Ordered a
y
            | Bool
otherwise = forall a. BoundedMeetSemiLattice a => a
top

instance Ord a => PartialOrd (Ordered a) where
    leq :: Ordered a -> Ordered a -> Bool
leq = forall a. Ord a => a -> a -> Bool
(<=)
    comparable :: Ordered a -> Ordered a -> Bool
comparable Ordered a
_ Ordered a
_ = Bool
True

instance Universe a => Universe (Ordered a) where
    universe :: [Ordered a]
universe = forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Ordered a
Ordered forall a. Universe a => [a]
universe
instance Finite a => Finite (Ordered a) where
    universeF :: [Ordered a]
universeF = forall a b. (a -> b) -> [a] -> [b]
map forall a. a -> Ordered a
Ordered forall a. Finite a => [a]
universeF
    cardinality :: Tagged (Ordered a) Natural
cardinality = forall {k1} {k2} (s :: k1) b (t :: k2). Tagged s b -> Tagged t b
retag (forall a. Finite a => Tagged a Natural
cardinality :: Tagged a Natural)

instance QC.Arbitrary a => QC.Arbitrary (Ordered a) where
    arbitrary :: Gen (Ordered a)
arbitrary = forall a. a -> Ordered a
Ordered forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
QC.arbitrary
    shrink :: Ordered a -> [Ordered a]
shrink    = forall a b. Arbitrary a => (a -> b) -> (b -> a) -> b -> [b]
QC.shrinkMap forall a. a -> Ordered a
Ordered forall a. Ordered a -> a
getOrdered

instance QC.CoArbitrary a => QC.CoArbitrary (Ordered a) where
    coarbitrary :: forall b. Ordered a -> Gen b -> Gen b
coarbitrary = forall a b. CoArbitrary a => a -> Gen b -> Gen b
QC.coarbitrary forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ordered a -> a
getOrdered

instance QC.Function a => QC.Function (Ordered a) where
    function :: forall b. (Ordered a -> b) -> Ordered a :-> b
function = forall b a c.
Function b =>
(a -> b) -> (b -> a) -> (a -> c) -> a :-> c
QC.functionMap forall a. Ordered a -> a
getOrdered forall a. a -> Ordered a
Ordered