{-# LANGUAGE CPP                #-}
{-# LANGUAGE ConstraintKinds    #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric      #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE Safe               #-}
----------------------------------------------------------------------------
-- |
-- Module      :  Algebra.Lattice
-- 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>
--
-- In mathematics, a lattice is a partially ordered set in which every
-- two elements have a unique supremum (also called a least upper bound
-- or @join@) and a unique infimum (also called a greatest lower bound or
-- @meet@).
--
-- In this module lattices are defined using 'meet' and 'join' operators,
-- as it's constructive one.
--
----------------------------------------------------------------------------
module Algebra.Lattice (
    -- * Unbounded lattices
    Lattice (..),
    joinLeq, joins1, meetLeq, meets1,

    -- * Bounded lattices
    BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..),
    joins, meets,
    fromBool,
    BoundedLattice,

    -- * Monoid wrappers
    Meet(..), Join(..),

    -- * Fixed points of chains in lattices
    lfp, lfpFrom, unsafeLfp,
    gfp, gfpFrom, unsafeGfp,
  ) where

import Prelude ()
import Prelude.Compat

import qualified Algebra.PartialOrd as PO

import Control.Applicative   (Const (..))
import Control.Monad.Zip     (MonadZip (..))
import Data.Data             (Data, Typeable)
import Data.Foldable1        (Foldable1 (..))
import Data.Functor.Identity (Identity (..))
import Data.Hashable         (Hashable (..))
import Data.Proxy            (Proxy (..))
import Data.Semigroup        (All (..), Any (..), Endo (..), Semigroup (..))
import Data.Tagged           (Tagged (..))
import Data.Universe.Class   (Finite (..), Universe (..))
import Data.Void             (Void)
import GHC.Generics          (Generic)

import qualified Data.HashMap.Lazy as HM
import qualified Data.HashSet      as HS
import qualified Data.IntMap       as IM
import qualified Data.IntSet       as IS
import qualified Data.Map          as Map
import qualified Data.Set          as Set
import qualified Test.QuickCheck   as QC

#if MIN_VERSION_base(4,18,0)
import Data.Tuple (Solo (MkSolo))
#elif MIN_VERSION_base(4,16,0)
import Data.Tuple (Solo (Solo))
#define MkSolo Solo
#elif MIN_VERSION_base(4,15,0)
import GHC.Tuple (Solo (Solo))
#define MkSolo Solo
#else
import Data.Tuple.Solo (Solo (MkSolo))
#endif

infixr 6 /\ -- This comment needed because of CPP
infixr 5 \/

-- | An algebraic structure with joins and meets.
--
-- See <http://en.wikipedia.org/wiki/Lattice_(order)> and <http://en.wikipedia.org/wiki/Absorption_law>.
--
-- 'Lattice' is very symmetric, which is seen from the laws:
--
-- /Associativity/
--
-- @
-- x '\/' (y '\/' z) ≡ (x '\/' y) '\/' z
-- x '/\' (y '/\' z) ≡ (x '/\' y) '/\' z
-- @
--
-- /Commutativity/
--
-- @
-- x '\/' y ≡ y '\/' x
-- x '/\' y ≡ y '/\' x
-- @
--
-- /Idempotency/
--
-- @
-- x '\/' x ≡ x
-- x '/\' x ≡ x
-- @
--
-- /Absorption/
--
-- @
-- a '\/' (a '/\' b) ≡ a
-- a '/\' (a '\/' b) ≡ a
-- @
class Lattice a where
    -- | join
    (\/) :: a -> a -> a

    -- | meet
    (/\) :: a -> a -> a

-- | The partial ordering induced by the join-semilattice structure
joinLeq :: (Eq a, Lattice a) => a -> a -> Bool
joinLeq :: forall a. (Eq a, Lattice a) => a -> a -> Bool
joinLeq a
x a
y = (a
x forall a. Lattice a => a -> a -> a
\/ a
y) forall a. Eq a => a -> a -> Bool
== a
y

meetLeq :: (Eq a, Lattice a) => a -> a -> Bool
meetLeq :: forall a. (Eq a, Lattice a) => a -> a -> Bool
meetLeq a
x a
y = (a
x forall a. Lattice a => a -> a -> a
/\ a
y) forall a. Eq a => a -> a -> Bool
== a
x

-- | A join-semilattice with an identity element 'bottom' for '\/'.
--
-- /Laws/
--
-- @
-- x '\/' 'bottom' ≡ x
-- @
--
-- /Corollary/
--
-- @
-- x '/\' 'bottom'
--   ≡⟨ identity ⟩
-- (x '/\' 'bottom') '\/' 'bottom'
--   ≡⟨ absorption ⟩
-- 'bottom'
-- @
class Lattice a => BoundedJoinSemiLattice a where
    bottom :: a

-- | The join of a list of join-semilattice elements
joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a
joins :: forall a (f :: * -> *).
(BoundedJoinSemiLattice a, Foldable f) =>
f a -> a
joins = forall a. Join a -> a
getJoin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. a -> Join a
Join

-- | The join of at a list of join-semilattice elements (of length at least one)
joins1 :: (Lattice a, Foldable1 f) => f a -> a
joins1 :: forall a (f :: * -> *). (Lattice a, Foldable1 f) => f a -> a
joins1 =  forall a. Join a -> a
getJoin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable1 t, Semigroup m) =>
(a -> m) -> t a -> m
foldMap1 forall a. a -> Join a
Join

-- | A meet-semilattice with an identity element 'top' for '/\'.
--
-- /Laws/
--
-- @
-- x '/\' 'top' ≡ x
-- @
--
-- /Corollary/
--
-- @
-- x '\/' 'top'
--   ≡⟨ identity ⟩
-- (x '\/' 'top') '/\' 'top'
--   ≡⟨ absorption ⟩
-- 'top'
-- @
--
class Lattice a => BoundedMeetSemiLattice a where
    top :: a

-- | The meet of a list of meet-semilattice elements
meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a
meets :: forall a (f :: * -> *).
(BoundedMeetSemiLattice a, Foldable f) =>
f a -> a
meets = forall a. Meet a -> a
getMeet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. a -> Meet a
Meet
--
-- | The meet of at a list of meet-semilattice elements (of length at least one)
meets1 :: (Lattice a, Foldable1 f) => f a -> a
meets1 :: forall a (f :: * -> *). (Lattice a, Foldable1 f) => f a -> a
meets1 = forall a. Meet a -> a
getMeet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) m a.
(Foldable1 t, Semigroup m) =>
(a -> m) -> t a -> m
foldMap1 forall a. a -> Meet a
Meet

type BoundedLattice a = (BoundedMeetSemiLattice a, BoundedJoinSemiLattice a)

-- | 'True' to 'top' and 'False' to 'bottom'
fromBool :: BoundedLattice a => Bool -> a
fromBool :: forall a. BoundedLattice a => Bool -> a
fromBool Bool
True  = forall a. BoundedMeetSemiLattice a => a
top
fromBool Bool
False = forall a. BoundedJoinSemiLattice a => a
bottom

--
-- Sets
--

instance Ord a => Lattice (Set.Set a) where
    \/ :: Set a -> Set a -> Set a
(\/) = forall a. Ord a => Set a -> Set a -> Set a
Set.union
    /\ :: Set a -> Set a -> Set a
(/\) = forall a. Ord a => Set a -> Set a -> Set a
Set.intersection

instance Ord a => BoundedJoinSemiLattice (Set.Set a) where
    bottom :: Set a
bottom = forall a. Set a
Set.empty

instance (Ord a, Finite a) => BoundedMeetSemiLattice (Set.Set a) where
    top :: Set a
top = forall a. Ord a => [a] -> Set a
Set.fromList forall a. Finite a => [a]
universeF

--
-- IntSets
--

instance Lattice IS.IntSet where
    \/ :: IntSet -> IntSet -> IntSet
(\/) = IntSet -> IntSet -> IntSet
IS.union
    /\ :: IntSet -> IntSet -> IntSet
(/\) = IntSet -> IntSet -> IntSet
IS.intersection

instance BoundedJoinSemiLattice IS.IntSet where
    bottom :: IntSet
bottom = IntSet
IS.empty

--
-- HashSet
--


instance (Eq a, Hashable a) => Lattice (HS.HashSet a) where
    \/ :: HashSet a -> HashSet a -> HashSet a
(\/) = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HS.union
    /\ :: HashSet a -> HashSet a -> HashSet a
(/\) = forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HS.intersection

instance (Eq a, Hashable a) => BoundedJoinSemiLattice (HS.HashSet a) where
    bottom :: HashSet a
bottom = forall a. HashSet a
HS.empty

instance (Eq a, Hashable a, Finite a) => BoundedMeetSemiLattice (HS.HashSet a) where
    top :: HashSet a
top = forall a. (Eq a, Hashable a) => [a] -> HashSet a
HS.fromList forall a. Finite a => [a]
universeF

--
-- Maps
--

instance (Ord k, Lattice v) => Lattice (Map.Map k v) where
    \/ :: Map k v -> Map k v -> Map k v
(\/) = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Lattice a => a -> a -> a
(\/)
    /\ :: Map k v -> Map k v -> Map k v
(/\) = forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith forall a. Lattice a => a -> a -> a
(/\)

instance (Ord k, Lattice v) => BoundedJoinSemiLattice (Map.Map k v) where
    bottom :: Map k v
bottom = forall k a. Map k a
Map.empty

instance (Ord k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (Map.Map k v) where
    top :: Map k v
top = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (forall a. Finite a => [a]
universeF forall a b. [a] -> [b] -> [(a, b)]
`zip` forall a. a -> [a]
repeat forall a. BoundedMeetSemiLattice a => a
top)

--
-- IntMaps
--

instance Lattice v => Lattice (IM.IntMap v) where
    \/ :: IntMap v -> IntMap v -> IntMap v
(\/) = forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IM.unionWith forall a. Lattice a => a -> a -> a
(\/)
    /\ :: IntMap v -> IntMap v -> IntMap v
(/\) = forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IM.intersectionWith forall a. Lattice a => a -> a -> a
(/\)

instance Lattice v => BoundedJoinSemiLattice (IM.IntMap v) where
    bottom :: IntMap v
bottom = forall a. IntMap a
IM.empty

--
-- HashMaps
--

instance (Eq k, Hashable k, Lattice v) => BoundedJoinSemiLattice (HM.HashMap k v) where
    bottom :: HashMap k v
bottom = forall k v. HashMap k v
HM.empty

instance (Eq k, Hashable k, Lattice v) => Lattice (HM.HashMap k v) where
    \/ :: HashMap k v -> HashMap k v -> HashMap k v
(\/) = forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HM.unionWith forall a. Lattice a => a -> a -> a
(\/)
    /\ :: HashMap k v -> HashMap k v -> HashMap k v
(/\) = forall k v1 v2 v3.
(Eq k, Hashable k) =>
(v1 -> v2 -> v3) -> HashMap k v1 -> HashMap k v2 -> HashMap k v3
HM.intersectionWith forall a. Lattice a => a -> a -> a
(/\)

instance (Eq k, Hashable k, Finite k, BoundedMeetSemiLattice v) => BoundedMeetSemiLattice (HM.HashMap k v) where
    top :: HashMap k v
top = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HM.fromList (forall a. Finite a => [a]
universeF forall a b. [a] -> [b] -> [(a, b)]
`zip` forall a. a -> [a]
repeat forall a. BoundedMeetSemiLattice a => a
top)

--
-- Functions
--

instance Lattice v => Lattice (k -> v) where
    k -> v
f \/ :: (k -> v) -> (k -> v) -> k -> v
\/ k -> v
g = \k
x -> k -> v
f k
x forall a. Lattice a => a -> a -> a
\/ k -> v
g k
x
    k -> v
f /\ :: (k -> v) -> (k -> v) -> k -> v
/\ k -> v
g = \k
x -> k -> v
f k
x forall a. Lattice a => a -> a -> a
/\ k -> v
g k
x

instance BoundedJoinSemiLattice v => BoundedJoinSemiLattice (k -> v) where
    bottom :: k -> v
bottom = forall a b. a -> b -> a
const forall a. BoundedJoinSemiLattice a => a
bottom

instance BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v) where
    top :: k -> v
top = forall a b. a -> b -> a
const forall a. BoundedMeetSemiLattice a => a
top

--
-- Unit
--


instance Lattice () where
    ()
_ \/ :: () -> () -> ()
\/ ()
_ = ()
    ()
_ /\ :: () -> () -> ()
/\ ()
_ = ()

instance BoundedJoinSemiLattice () where
  bottom :: ()
bottom = ()

instance BoundedMeetSemiLattice () where
  top :: ()
top = ()

--
-- Tuples
--

instance (Lattice a, Lattice b) => Lattice (a, b) where
    (a
x1, b
y1) \/ :: (a, b) -> (a, b) -> (a, b)
\/ (a
x2, b
y2) = (a
x1 forall a. Lattice a => a -> a -> a
\/ a
x2, b
y1 forall a. Lattice a => a -> a -> a
\/ b
y2)
    (a
x1, b
y1) /\ :: (a, b) -> (a, b) -> (a, b)
/\ (a
x2, b
y2) = (a
x1 forall a. Lattice a => a -> a -> a
/\ a
x2, b
y1 forall a. Lattice a => a -> a -> a
/\ b
y2)

instance (BoundedJoinSemiLattice a, BoundedJoinSemiLattice b) => BoundedJoinSemiLattice (a, b) where
    bottom :: (a, b)
bottom = (forall a. BoundedJoinSemiLattice a => a
bottom, forall a. BoundedJoinSemiLattice a => a
bottom)

instance (BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b) where
    top :: (a, b)
top = (forall a. BoundedMeetSemiLattice a => a
top, forall a. BoundedMeetSemiLattice a => a
top)

--
-- Either
--

-- | Ordinal sum.
--
-- @since 2.1
instance (Lattice a, Lattice b) => Lattice (Either a b) where
    Right b
x     \/ :: Either a b -> Either a b -> Either a b
\/ Right b
y     = forall a b. b -> Either a b
Right (b
x forall a. Lattice a => a -> a -> a
\/ b
y)
    u :: Either a b
u@(Right b
_) \/ Either a b
_           = Either a b
u
    Either a b
_           \/ u :: Either a b
u@(Right b
_) = Either a b
u
    Left a
x      \/ Left a
y      = forall a b. a -> Either a b
Left (a
x forall a. Lattice a => a -> a -> a
\/ a
y)

    Left a
x      /\ :: Either a b -> Either a b -> Either a b
/\ Left a
y     = forall a b. a -> Either a b
Left (a
x forall a. Lattice a => a -> a -> a
/\ a
y)
    l :: Either a b
l@(Left a
_)  /\ Either a b
_          = Either a b
l
    Either a b
_           /\ l :: Either a b
l@(Left a
_) = Either a b
l
    Right b
x     /\ Right b
y    = forall a b. b -> Either a b
Right (b
x forall a. Lattice a => a -> a -> a
/\ b
y)

-- | @since 2.1
instance (BoundedJoinSemiLattice a, Lattice b) => BoundedJoinSemiLattice (Either a b) where
    bottom :: Either a b
bottom = forall a b. a -> Either a b
Left forall a. BoundedJoinSemiLattice a => a
bottom

-- | @since 2.1
instance (Lattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (Either a b) where
    top :: Either a b
top = forall a b. b -> Either a b
Right forall a. BoundedMeetSemiLattice a => a
top

--
-- Bools
--

instance Lattice Bool where
    \/ :: Bool -> Bool -> Bool
(\/) = Bool -> Bool -> Bool
(||)
    /\ :: Bool -> Bool -> Bool
(/\) = Bool -> Bool -> Bool
(&&)

instance BoundedJoinSemiLattice Bool where
    bottom :: Bool
bottom = Bool
False

instance BoundedMeetSemiLattice Bool where
    top :: Bool
top = Bool
True

--- Monoids

-- | Monoid wrapper for join-'Lattice'
newtype Join a = Join { forall a. Join a -> a
getJoin :: a }
  deriving (Join a -> Join a -> Bool
forall a. Eq a => Join a -> Join a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Join a -> Join a -> Bool
$c/= :: forall a. Eq a => Join a -> Join a -> Bool
== :: Join a -> Join a -> Bool
$c== :: forall a. Eq a => Join a -> Join a -> Bool
Eq, Join a -> Join a -> Bool
Join a -> Join a -> Ordering
Join a -> Join a -> Join 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 (Join a)
forall a. Ord a => Join a -> Join a -> Bool
forall a. Ord a => Join a -> Join a -> Ordering
forall a. Ord a => Join a -> Join a -> Join a
min :: Join a -> Join a -> Join a
$cmin :: forall a. Ord a => Join a -> Join a -> Join a
max :: Join a -> Join a -> Join a
$cmax :: forall a. Ord a => Join a -> Join a -> Join a
>= :: Join a -> Join a -> Bool
$c>= :: forall a. Ord a => Join a -> Join a -> Bool
> :: Join a -> Join a -> Bool
$c> :: forall a. Ord a => Join a -> Join a -> Bool
<= :: Join a -> Join a -> Bool
$c<= :: forall a. Ord a => Join a -> Join a -> Bool
< :: Join a -> Join a -> Bool
$c< :: forall a. Ord a => Join a -> Join a -> Bool
compare :: Join a -> Join a -> Ordering
$ccompare :: forall a. Ord a => Join a -> Join a -> Ordering
Ord, ReadPrec [Join a]
ReadPrec (Join a)
ReadS [Join a]
forall a. Read a => ReadPrec [Join a]
forall a. Read a => ReadPrec (Join a)
forall a. Read a => Int -> ReadS (Join a)
forall a. Read a => ReadS [Join a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Join a]
$creadListPrec :: forall a. Read a => ReadPrec [Join a]
readPrec :: ReadPrec (Join a)
$creadPrec :: forall a. Read a => ReadPrec (Join a)
readList :: ReadS [Join a]
$creadList :: forall a. Read a => ReadS [Join a]
readsPrec :: Int -> ReadS (Join a)
$creadsPrec :: forall a. Read a => Int -> ReadS (Join a)
Read, Int -> Join a -> ShowS
forall a. Show a => Int -> Join a -> ShowS
forall a. Show a => [Join a] -> ShowS
forall a. Show a => Join a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Join a] -> ShowS
$cshowList :: forall a. Show a => [Join a] -> ShowS
show :: Join a -> String
$cshow :: forall a. Show a => Join a -> String
showsPrec :: Int -> Join a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Join a -> ShowS
Show, Join a
forall a. a -> a -> Bounded a
forall a. Bounded a => Join a
maxBound :: Join a
$cmaxBound :: forall a. Bounded a => Join a
minBound :: Join a
$cminBound :: forall a. Bounded a => Join a
Bounded, Typeable, Join a -> DataType
Join a -> Constr
forall {a}. Data a => Typeable (Join a)
forall a. Data a => Join a -> DataType
forall a. Data a => Join a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Join a -> Join a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Join a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Join a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Join a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Join a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Join a -> m (Join a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Join a -> m (Join a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Join a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Join a -> c (Join a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Join a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Join 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 (Join a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Join a -> c (Join a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Join a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Join a -> m (Join a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Join a -> m (Join a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Join a -> m (Join a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Join a -> m (Join a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Join a -> m (Join a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Join a -> m (Join a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Join a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Join a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Join a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Join a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Join a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Join a -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Join a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Join a -> r
gmapT :: (forall b. Data b => b -> b) -> Join a -> Join a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Join a -> Join a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Join a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Join a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Join a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Join a))
dataTypeOf :: Join a -> DataType
$cdataTypeOf :: forall a. Data a => Join a -> DataType
toConstr :: Join a -> Constr
$ctoConstr :: forall a. Data a => Join a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Join a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Join a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Join a -> c (Join a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Join a -> c (Join a)
Data, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Join a) x -> Join a
forall a x. Join a -> Rep (Join a) x
$cto :: forall a x. Rep (Join a) x -> Join a
$cfrom :: forall a x. Join a -> Rep (Join a) x
Generic)

instance Lattice a => Semigroup (Join a) where
  Join a
a <> :: Join a -> Join a -> Join a
<> Join a
b = forall a. a -> Join a
Join (a
a forall a. Lattice a => a -> a -> a
\/ a
b)

instance BoundedJoinSemiLattice a => Monoid (Join a) where
  mempty :: Join a
mempty = forall a. a -> Join a
Join forall a. BoundedJoinSemiLattice a => a
bottom
  Join a
a mappend :: Join a -> Join a -> Join a
`mappend` Join a
b = forall a. a -> Join a
Join (a
a forall a. Lattice a => a -> a -> a
\/ a
b)

instance (Eq a, Lattice a) => PO.PartialOrd (Join a) where
  leq :: Join a -> Join a -> Bool
leq (Join a
a) (Join a
b) = forall a. (Eq a, Lattice a) => a -> a -> Bool
joinLeq a
a a
b

instance Functor Join where
  fmap :: forall a b. (a -> b) -> Join a -> Join b
fmap a -> b
f (Join a
x) = forall a. a -> Join a
Join (a -> b
f a
x)

instance Applicative Join where
  pure :: forall a. a -> Join a
pure = forall a. a -> Join a
Join
  Join a -> b
f <*> :: forall a b. Join (a -> b) -> Join a -> Join b
<*> Join a
x = forall a. a -> Join a
Join (a -> b
f a
x)
  Join a
_ *> :: forall a b. Join a -> Join b -> Join b
*> Join b
x = Join b
x

instance Monad Join where
  return :: forall a. a -> Join a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Join a
m >>= :: forall a b. Join a -> (a -> Join b) -> Join b
>>= a -> Join b
f = a -> Join b
f a
m
  >> :: forall a b. Join a -> Join b -> Join b
(>>) = forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
(*>)

instance MonadZip Join where
  mzip :: forall a b. Join a -> Join b -> Join (a, b)
mzip (Join a
x) (Join b
y) = forall a. a -> Join a
Join (a
x, b
y)

instance Universe a => Universe (Join a) where
  universe :: [Join a]
universe = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Join a
Join forall a. Universe a => [a]
universe

instance Finite a => Finite (Join a) where
  universeF :: [Join a]
universeF = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Join a
Join forall a. Finite a => [a]
universeF

-- | Monoid wrapper for meet-'Lattice'
newtype Meet a = Meet { forall a. Meet a -> a
getMeet :: a }
  deriving (Meet a -> Meet a -> Bool
forall a. Eq a => Meet a -> Meet a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Meet a -> Meet a -> Bool
$c/= :: forall a. Eq a => Meet a -> Meet a -> Bool
== :: Meet a -> Meet a -> Bool
$c== :: forall a. Eq a => Meet a -> Meet a -> Bool
Eq, Meet a -> Meet a -> Bool
Meet a -> Meet a -> Ordering
Meet a -> Meet a -> Meet 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 (Meet a)
forall a. Ord a => Meet a -> Meet a -> Bool
forall a. Ord a => Meet a -> Meet a -> Ordering
forall a. Ord a => Meet a -> Meet a -> Meet a
min :: Meet a -> Meet a -> Meet a
$cmin :: forall a. Ord a => Meet a -> Meet a -> Meet a
max :: Meet a -> Meet a -> Meet a
$cmax :: forall a. Ord a => Meet a -> Meet a -> Meet a
>= :: Meet a -> Meet a -> Bool
$c>= :: forall a. Ord a => Meet a -> Meet a -> Bool
> :: Meet a -> Meet a -> Bool
$c> :: forall a. Ord a => Meet a -> Meet a -> Bool
<= :: Meet a -> Meet a -> Bool
$c<= :: forall a. Ord a => Meet a -> Meet a -> Bool
< :: Meet a -> Meet a -> Bool
$c< :: forall a. Ord a => Meet a -> Meet a -> Bool
compare :: Meet a -> Meet a -> Ordering
$ccompare :: forall a. Ord a => Meet a -> Meet a -> Ordering
Ord, ReadPrec [Meet a]
ReadPrec (Meet a)
ReadS [Meet a]
forall a. Read a => ReadPrec [Meet a]
forall a. Read a => ReadPrec (Meet a)
forall a. Read a => Int -> ReadS (Meet a)
forall a. Read a => ReadS [Meet a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Meet a]
$creadListPrec :: forall a. Read a => ReadPrec [Meet a]
readPrec :: ReadPrec (Meet a)
$creadPrec :: forall a. Read a => ReadPrec (Meet a)
readList :: ReadS [Meet a]
$creadList :: forall a. Read a => ReadS [Meet a]
readsPrec :: Int -> ReadS (Meet a)
$creadsPrec :: forall a. Read a => Int -> ReadS (Meet a)
Read, Int -> Meet a -> ShowS
forall a. Show a => Int -> Meet a -> ShowS
forall a. Show a => [Meet a] -> ShowS
forall a. Show a => Meet a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Meet a] -> ShowS
$cshowList :: forall a. Show a => [Meet a] -> ShowS
show :: Meet a -> String
$cshow :: forall a. Show a => Meet a -> String
showsPrec :: Int -> Meet a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Meet a -> ShowS
Show, Meet a
forall a. a -> a -> Bounded a
forall a. Bounded a => Meet a
maxBound :: Meet a
$cmaxBound :: forall a. Bounded a => Meet a
minBound :: Meet a
$cminBound :: forall a. Bounded a => Meet a
Bounded, Typeable, Meet a -> DataType
Meet a -> Constr
forall {a}. Data a => Typeable (Meet a)
forall a. Data a => Meet a -> DataType
forall a. Data a => Meet a -> Constr
forall a.
Data a =>
(forall b. Data b => b -> b) -> Meet a -> Meet a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Meet a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Meet a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Meet a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Meet a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Meet a -> m (Meet a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Meet a -> m (Meet a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Meet a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Meet a -> c (Meet a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Meet a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Meet 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 (Meet a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Meet a -> c (Meet a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Meet a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Meet a -> m (Meet a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Meet a -> m (Meet a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Meet a -> m (Meet a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Meet a -> m (Meet a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Meet a -> m (Meet a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Meet a -> m (Meet a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Meet a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Meet a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Meet a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Meet a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Meet a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Meet a -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Meet a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Meet a -> r
gmapT :: (forall b. Data b => b -> b) -> Meet a -> Meet a
$cgmapT :: forall a.
Data a =>
(forall b. Data b => b -> b) -> Meet a -> Meet a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Meet a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Meet a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Meet a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Meet a))
dataTypeOf :: Meet a -> DataType
$cdataTypeOf :: forall a. Data a => Meet a -> DataType
toConstr :: Meet a -> Constr
$ctoConstr :: forall a. Data a => Meet a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Meet a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Meet a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Meet a -> c (Meet a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Meet a -> c (Meet a)
Data, forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Meet a) x -> Meet a
forall a x. Meet a -> Rep (Meet a) x
$cto :: forall a x. Rep (Meet a) x -> Meet a
$cfrom :: forall a x. Meet a -> Rep (Meet a) x
Generic)

instance Lattice a => Semigroup (Meet a) where
  Meet a
a <> :: Meet a -> Meet a -> Meet a
<> Meet a
b = forall a. a -> Meet a
Meet (a
a forall a. Lattice a => a -> a -> a
/\ a
b)

instance BoundedMeetSemiLattice a => Monoid (Meet a) where
  mempty :: Meet a
mempty = forall a. a -> Meet a
Meet forall a. BoundedMeetSemiLattice a => a
top
  Meet a
a mappend :: Meet a -> Meet a -> Meet a
`mappend` Meet a
b = forall a. a -> Meet a
Meet (a
a forall a. Lattice a => a -> a -> a
/\ a
b)

instance (Eq a, Lattice a) => PO.PartialOrd (Meet a) where
  leq :: Meet a -> Meet a -> Bool
leq (Meet a
a) (Meet a
b) = forall a. (Eq a, Lattice a) => a -> a -> Bool
meetLeq a
a a
b

instance Functor Meet where
  fmap :: forall a b. (a -> b) -> Meet a -> Meet b
fmap a -> b
f (Meet a
x) = forall a. a -> Meet a
Meet (a -> b
f a
x)

instance Applicative Meet where
  pure :: forall a. a -> Meet a
pure = forall a. a -> Meet a
Meet
  Meet a -> b
f <*> :: forall a b. Meet (a -> b) -> Meet a -> Meet b
<*> Meet a
x = forall a. a -> Meet a
Meet (a -> b
f a
x)
  Meet a
_ *> :: forall a b. Meet a -> Meet b -> Meet b
*> Meet b
x = Meet b
x

instance Monad Meet where
  return :: forall a. a -> Meet a
return = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Meet a
m >>= :: forall a b. Meet a -> (a -> Meet b) -> Meet b
>>= a -> Meet b
f = a -> Meet b
f a
m
  >> :: forall a b. Meet a -> Meet b -> Meet b
(>>) = forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
(*>)

instance MonadZip Meet where
  mzip :: forall a b. Meet a -> Meet b -> Meet (a, b)
mzip (Meet a
x) (Meet b
y) = forall a. a -> Meet a
Meet (a
x, b
y)

instance Universe a => Universe (Meet a) where
  universe :: [Meet a]
universe = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Meet a
Meet forall a. Universe a => [a]
universe

instance Finite a => Finite (Meet a) where
  universeF :: [Meet a]
universeF = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Meet a
Meet forall a. Finite a => [a]
universeF

-- All

instance Lattice All where
  All Bool
a \/ :: All -> All -> All
\/ All Bool
b = Bool -> All
All forall a b. (a -> b) -> a -> b
$ Bool
a forall a. Lattice a => a -> a -> a
\/ Bool
b
  All Bool
a /\ :: All -> All -> All
/\ All Bool
b = Bool -> All
All forall a b. (a -> b) -> a -> b
$ Bool
a forall a. Lattice a => a -> a -> a
/\ Bool
b

instance BoundedJoinSemiLattice All where
  bottom :: All
bottom = Bool -> All
All Bool
False

instance BoundedMeetSemiLattice All where
  top :: All
top = Bool -> All
All Bool
True

-- Any
instance Lattice Any where
  Any Bool
a \/ :: Any -> Any -> Any
\/ Any Bool
b = Bool -> Any
Any forall a b. (a -> b) -> a -> b
$ Bool
a forall a. Lattice a => a -> a -> a
\/ Bool
b
  Any Bool
a /\ :: Any -> Any -> Any
/\ Any Bool
b = Bool -> Any
Any forall a b. (a -> b) -> a -> b
$ Bool
a forall a. Lattice a => a -> a -> a
/\ Bool
b

instance BoundedJoinSemiLattice Any where
  bottom :: Any
bottom = Bool -> Any
Any Bool
False

instance BoundedMeetSemiLattice Any where
  top :: Any
top = Bool -> Any
Any Bool
True

-- Endo
instance Lattice a => Lattice (Endo a) where
  Endo a -> a
a \/ :: Endo a -> Endo a -> Endo a
\/ Endo a -> a
b = forall a. (a -> a) -> Endo a
Endo forall a b. (a -> b) -> a -> b
$ a -> a
a forall a. Lattice a => a -> a -> a
\/ a -> a
b
  Endo a -> a
a /\ :: Endo a -> Endo a -> Endo a
/\ Endo a -> a
b = forall a. (a -> a) -> Endo a
Endo forall a b. (a -> b) -> a -> b
$ a -> a
a forall a. Lattice a => a -> a -> a
/\ a -> a
b

instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Endo a) where
  bottom :: Endo a
bottom = forall a. (a -> a) -> Endo a
Endo forall a. BoundedJoinSemiLattice a => a
bottom

instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a) where
  top :: Endo a
top = forall a. (a -> a) -> Endo a
Endo forall a. BoundedMeetSemiLattice a => a
top

-- Tagged

instance Lattice a => Lattice (Tagged t a) where
  Tagged a
a \/ :: Tagged t a -> Tagged t a -> Tagged t a
\/ Tagged a
b = forall {k} (s :: k) b. b -> Tagged s b
Tagged forall a b. (a -> b) -> a -> b
$ a
a forall a. Lattice a => a -> a -> a
\/ a
b
  Tagged a
a /\ :: Tagged t a -> Tagged t a -> Tagged t a
/\ Tagged a
b = forall {k} (s :: k) b. b -> Tagged s b
Tagged forall a b. (a -> b) -> a -> b
$ a
a forall a. Lattice a => a -> a -> a
/\ a
b

instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Tagged t a) where
  bottom :: Tagged t a
bottom = forall {k} (s :: k) b. b -> Tagged s b
Tagged forall a. BoundedJoinSemiLattice a => a
bottom

instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Tagged t a) where
  top :: Tagged t a
top = forall {k} (s :: k) b. b -> Tagged s b
Tagged forall a. BoundedMeetSemiLattice a => a
top

-- Proxy
instance Lattice (Proxy a) where
  Proxy a
_ \/ :: Proxy a -> Proxy a -> Proxy a
\/ Proxy a
_ = forall {k} (t :: k). Proxy t
Proxy
  Proxy a
_ /\ :: Proxy a -> Proxy a -> Proxy a
/\ Proxy a
_ = forall {k} (t :: k). Proxy t
Proxy

instance BoundedJoinSemiLattice (Proxy a) where
  bottom :: Proxy a
bottom = forall {k} (t :: k). Proxy t
Proxy

instance BoundedMeetSemiLattice (Proxy a) where
  top :: Proxy a
top = forall {k} (t :: k). Proxy t
Proxy

-- Identity

instance Lattice a => Lattice (Identity a) where
  Identity a
a \/ :: Identity a -> Identity a -> Identity a
\/ Identity a
b = forall a. a -> Identity a
Identity (a
a forall a. Lattice a => a -> a -> a
\/ a
b)
  Identity a
a /\ :: Identity a -> Identity a -> Identity a
/\ Identity a
b = forall a. a -> Identity a
Identity (a
a forall a. Lattice a => a -> a -> a
/\ a
b)

instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Identity a) where
  top :: Identity a
top = forall a. a -> Identity a
Identity forall a. BoundedMeetSemiLattice a => a
top

instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where
  bottom :: Identity a
bottom = forall a. a -> Identity a
Identity forall a. BoundedJoinSemiLattice a => a
bottom

-- Const
instance Lattice a => Lattice (Const a b) where
  Const a
a \/ :: Const a b -> Const a b -> Const a b
\/ Const a
b = forall {k} a (b :: k). a -> Const a b
Const (a
a forall a. Lattice a => a -> a -> a
\/ a
b)
  Const a
a /\ :: Const a b -> Const a b -> Const a b
/\ Const a
b = forall {k} a (b :: k). a -> Const a b
Const (a
a forall a. Lattice a => a -> a -> a
/\ a
b)

instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Const a b) where
  bottom :: Const a b
bottom = forall {k} a (b :: k). a -> Const a b
Const forall a. BoundedJoinSemiLattice a => a
bottom

instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Const a b) where
  top :: Const a b
top = forall {k} a (b :: k). a -> Const a b
Const forall a. BoundedMeetSemiLattice a => a
top

-------------------------------------------------------------------------------
-- Void
-------------------------------------------------------------------------------

instance Lattice Void where
  Void
a \/ :: Void -> Void -> Void
\/ Void
_ = Void
a
  Void
a /\ :: Void -> Void -> Void
/\ Void
_ = Void
a

-------------------------------------------------------------------------------
-- QuickCheck
-------------------------------------------------------------------------------

instance Lattice QC.Property where
  \/ :: Property -> Property -> Property
(\/) = forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
(QC..||.)
  /\ :: Property -> Property -> Property
(/\) = forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
(QC..&&.)

instance BoundedJoinSemiLattice QC.Property where bottom :: Property
bottom = forall prop. Testable prop => prop -> Property
QC.property Bool
False
instance BoundedMeetSemiLattice QC.Property where top :: Property
top = forall prop. Testable prop => prop -> Property
QC.property Bool
True

-------------------------------------------------------------------------------
-- OneTuple
-------------------------------------------------------------------------------

-- | @since 2.0.3
instance Lattice a => Lattice (Solo a) where
  Solo a
MkSolo a \/ MkSolo b = MkSolo (a \/ b)
  Solo a
MkSolo a /\ MkSolo b = MkSolo (a /\ b)

-- | @since 2.0.3
instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Solo a) where
  top :: Solo a
top = MkSolo top

-- | @since 2.0.3
instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Solo a) where
  bottom :: Solo a
bottom = MkSolo bottom

-------------------------------------------------------------------------------
-- Theorems
-------------------------------------------------------------------------------

-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
-- Assumes that the function is monotone and does not check if that is correct.
{-# INLINE unsafeLfp #-}
unsafeLfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a
unsafeLfp :: forall a. (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a
unsafeLfp = forall a. Eq a => a -> (a -> a) -> a
PO.unsafeLfpFrom forall a. BoundedJoinSemiLattice a => a
bottom

-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
-- Forces the function to be monotone.
{-# INLINE lfp #-}
lfp :: (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a
lfp :: forall a. (Eq a, BoundedJoinSemiLattice a) => (a -> a) -> a
lfp = forall a. (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a
lfpFrom forall a. BoundedJoinSemiLattice a => a
bottom

-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
-- Forces the function to be monotone.
{-# INLINE lfpFrom #-}
lfpFrom :: (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a
lfpFrom :: forall a. (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a
lfpFrom a
init_x a -> a
f = forall a. Eq a => a -> (a -> a) -> a
PO.unsafeLfpFrom a
init_x (\a
x -> a -> a
f a
x forall a. Lattice a => a -> a -> a
\/ a
x)


-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
-- Assumes that the function is antinone and does not check if that is correct.
{-# INLINE unsafeGfp #-}
unsafeGfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a
unsafeGfp :: forall a. (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a
unsafeGfp = forall a. Eq a => a -> (a -> a) -> a
PO.unsafeGfpFrom forall a. BoundedMeetSemiLattice a => a
top

-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
-- Forces the function to be antinone.
{-# INLINE gfp #-}
gfp :: (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a
gfp :: forall a. (Eq a, BoundedMeetSemiLattice a) => (a -> a) -> a
gfp = forall a. (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a
gfpFrom forall a. BoundedMeetSemiLattice a => a
top

-- | Implementation of Kleene fixed-point theorem <http://en.wikipedia.org/wiki/Kleene_fixed-point_theorem>.
-- Forces the function to be antinone.
{-# INLINE gfpFrom #-}
gfpFrom :: (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a
gfpFrom :: forall a. (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a
gfpFrom a
init_x a -> a
f = forall a. Eq a => a -> (a -> a) -> a
PO.unsafeGfpFrom a
init_x (\a
x -> a -> a
f a
x forall a. Lattice a => a -> a -> a
/\ a
x)