{-# 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.Functor.Identity   (Identity (..))
import Data.Hashable           (Hashable (..))
import Data.Proxy              (Proxy (..))
import Data.Semigroup          (All (..), Any (..), Endo (..), Semigroup (..))
import Data.Semigroup.Foldable (Foldable1 (..))
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,16,0)
import Data.Tuple (Solo (..))
#elif MIN_VERSION_base(4,15,0)
import GHC.Tuple (Solo (..))
#else
import Data.Tuple.Solo (Solo (..))
#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 :: a -> a -> Bool
joinLeq a
x a
y = (a
x a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
y) a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y

meetLeq :: (Eq a, Lattice a) => a -> a -> Bool
meetLeq :: a -> a -> Bool
meetLeq a
x a
y = (a
x a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
y) a -> a -> Bool
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 :: f a -> a
joins = Join a -> a
forall a. Join a -> a
getJoin (Join a -> a) -> (f a -> Join a) -> f a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Join a) -> f a -> Join a
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> Join a
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 :: f a -> a
joins1 =  Join a -> a
forall a. Join a -> a
getJoin (Join a -> a) -> (f a -> Join a) -> f a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Join a) -> f a -> Join a
forall (t :: * -> *) m a.
(Foldable1 t, Semigroup m) =>
(a -> m) -> t a -> m
foldMap1 a -> Join a
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 :: f a -> a
meets = Meet a -> a
forall a. Meet a -> a
getMeet (Meet a -> a) -> (f a -> Meet a) -> f a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Meet a) -> f a -> Meet a
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> Meet a
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 :: f a -> a
meets1 = Meet a -> a
forall a. Meet a -> a
getMeet (Meet a -> a) -> (f a -> Meet a) -> f a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Meet a) -> f a -> Meet a
forall (t :: * -> *) m a.
(Foldable1 t, Semigroup m) =>
(a -> m) -> t a -> m
foldMap1 a -> Meet a
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 :: Bool -> a
fromBool Bool
True  = a
forall a. BoundedMeetSemiLattice a => a
top
fromBool Bool
False = a
forall a. BoundedJoinSemiLattice a => a
bottom

--
-- Sets
--

instance Ord a => Lattice (Set.Set a) where
    \/ :: Set a -> Set a -> Set a
(\/) = Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
Set.union
    /\ :: Set a -> Set a -> Set a
(/\) = 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 = Set a
forall a. Set a
Set.empty

instance (Ord a, Finite a) => BoundedMeetSemiLattice (Set.Set a) where
    top :: Set a
top = [a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a]
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
(\/) = 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
(/\) = 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 = HashSet a
forall a. HashSet a
HS.empty

instance (Eq a, Hashable a, Finite a) => BoundedMeetSemiLattice (HS.HashSet a) where
    top :: HashSet a
top = [a] -> HashSet a
forall a. (Eq a, Hashable a) => [a] -> HashSet a
HS.fromList [a]
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
(\/) = (v -> v -> v) -> 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 v -> v -> v
forall a. Lattice a => a -> a -> a
(\/)
    /\ :: Map k v -> Map k v -> Map k v
(/\) = (v -> v -> v) -> 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 v -> v -> v
forall a. Lattice a => a -> a -> a
(/\)

instance (Ord k, Lattice v) => BoundedJoinSemiLattice (Map.Map k v) where
    bottom :: Map k v
bottom = Map k v
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 = [(k, v)] -> Map k v
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([k]
forall a. Finite a => [a]
universeF [k] -> [v] -> [(k, v)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` v -> [v]
forall a. a -> [a]
repeat v
forall a. BoundedMeetSemiLattice a => a
top)

--
-- IntMaps
--

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

instance Lattice v => BoundedJoinSemiLattice (IM.IntMap v) where
    bottom :: IntMap v
bottom = IntMap v
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 = HashMap k v
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
(\/) = (v -> v -> v) -> 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 v -> v -> v
forall a. Lattice a => a -> a -> a
(\/)
    /\ :: HashMap k v -> HashMap k v -> HashMap k v
(/\) = (v -> v -> v) -> 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 v -> v -> v
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 = [(k, v)] -> HashMap k v
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
HM.fromList ([k]
forall a. Finite a => [a]
universeF [k] -> [v] -> [(k, v)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` v -> [v]
forall a. a -> [a]
repeat v
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 v -> v -> v
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 v -> v -> v
forall a. Lattice a => a -> a -> a
/\ k -> v
g k
x

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

instance BoundedMeetSemiLattice v => BoundedMeetSemiLattice (k -> v) where
    top :: k -> v
top = v -> k -> v
forall a b. a -> b -> a
const v
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 a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
x2, b
y1 b -> b -> b
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 a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
x2, b
y1 b -> b -> b
forall a. Lattice a => a -> a -> a
/\ b
y2)

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

instance (BoundedMeetSemiLattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (a, b) where
    top :: (a, b)
top = (a
forall a. BoundedMeetSemiLattice a => a
top, b
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     = b -> Either a b
forall a b. b -> Either a b
Right (b
x b -> b -> b
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      = a -> Either a b
forall a b. a -> Either a b
Left (a
x a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
y)

    Left a
x      /\ :: Either a b -> Either a b -> Either a b
/\ Left a
y     = a -> Either a b
forall a b. a -> Either a b
Left (a
x a -> a -> a
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    = b -> Either a b
forall a b. b -> Either a b
Right (b
x b -> b -> b
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 = a -> Either a b
forall a b. a -> Either a b
Left a
forall a. BoundedJoinSemiLattice a => a
bottom

-- | @since 2.1
instance (Lattice a, BoundedMeetSemiLattice b) => BoundedMeetSemiLattice (Either a b) where
    top :: Either a b
top = b -> Either a b
forall a b. b -> Either a b
Right b
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 { Join a -> a
getJoin :: a }
  deriving (Join a -> Join a -> Bool
(Join a -> Join a -> Bool)
-> (Join a -> Join a -> Bool) -> Eq (Join a)
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, Eq (Join a)
Eq (Join a)
-> (Join a -> Join a -> Ordering)
-> (Join a -> Join a -> Bool)
-> (Join a -> Join a -> Bool)
-> (Join a -> Join a -> Bool)
-> (Join a -> Join a -> Bool)
-> (Join a -> Join a -> Join a)
-> (Join a -> Join a -> Join a)
-> Ord (Join a)
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
$cp1Ord :: forall a. Ord a => Eq (Join a)
Ord, ReadPrec [Join a]
ReadPrec (Join a)
Int -> ReadS (Join a)
ReadS [Join a]
(Int -> ReadS (Join a))
-> ReadS [Join a]
-> ReadPrec (Join a)
-> ReadPrec [Join a]
-> Read (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
[Join a] -> ShowS
Join a -> String
(Int -> Join a -> ShowS)
-> (Join a -> String) -> ([Join a] -> ShowS) -> Show (Join a)
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
Join a -> Join a -> Bounded (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, Typeable (Join a)
DataType
Constr
Typeable (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 (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Join a))
-> (Join a -> Constr)
-> (Join a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Join a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Join a)))
-> ((forall b. Data b => b -> b) -> Join a -> Join a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Join a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Join a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Join a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Join a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Join a -> m (Join a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Join a -> m (Join a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Join a -> m (Join a))
-> Data (Join a)
Join a -> DataType
Join a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Join a))
(forall b. Data b => b -> b) -> Join a -> Join a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Join a -> c (Join a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Join a)
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 u. Int -> (forall d. Data d => d -> u) -> Join a -> u
forall u. (forall d. Data d => d -> u) -> Join a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Join a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Join a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Join a -> m (Join a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Join a -> m (Join 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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Join a))
$cJoin :: Constr
$tJoin :: DataType
gmapMo :: (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 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 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 :: 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 d. Data d => d -> u) -> Join a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Join a -> [u]
gmapQr :: (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 :: (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 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 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 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 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)
$cp1Data :: forall a. Data a => Typeable (Join a)
Data, (forall x. Join a -> Rep (Join a) x)
-> (forall x. Rep (Join a) x -> Join a) -> Generic (Join a)
forall x. Rep (Join a) x -> Join a
forall x. Join a -> Rep (Join a) x
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 = a -> Join a
forall a. a -> Join a
Join (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
b)

instance BoundedJoinSemiLattice a => Monoid (Join a) where
  mempty :: Join a
mempty = a -> Join a
forall a. a -> Join a
Join a
forall a. BoundedJoinSemiLattice a => a
bottom
  Join a
a mappend :: Join a -> Join a -> Join a
`mappend` Join a
b = a -> Join a
forall a. a -> Join a
Join (a
a a -> 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) = a -> a -> Bool
forall a. (Eq a, Lattice a) => a -> a -> Bool
joinLeq a
a a
b

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

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

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

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

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

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

-- | Monoid wrapper for meet-'Lattice'
newtype Meet a = Meet { Meet a -> a
getMeet :: a }
  deriving (Meet a -> Meet a -> Bool
(Meet a -> Meet a -> Bool)
-> (Meet a -> Meet a -> Bool) -> Eq (Meet a)
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, Eq (Meet a)
Eq (Meet a)
-> (Meet a -> Meet a -> Ordering)
-> (Meet a -> Meet a -> Bool)
-> (Meet a -> Meet a -> Bool)
-> (Meet a -> Meet a -> Bool)
-> (Meet a -> Meet a -> Bool)
-> (Meet a -> Meet a -> Meet a)
-> (Meet a -> Meet a -> Meet a)
-> Ord (Meet a)
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
$cp1Ord :: forall a. Ord a => Eq (Meet a)
Ord, ReadPrec [Meet a]
ReadPrec (Meet a)
Int -> ReadS (Meet a)
ReadS [Meet a]
(Int -> ReadS (Meet a))
-> ReadS [Meet a]
-> ReadPrec (Meet a)
-> ReadPrec [Meet a]
-> Read (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
[Meet a] -> ShowS
Meet a -> String
(Int -> Meet a -> ShowS)
-> (Meet a -> String) -> ([Meet a] -> ShowS) -> Show (Meet a)
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
Meet a -> Meet a -> Bounded (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, Typeable (Meet a)
DataType
Constr
Typeable (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 (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Meet a))
-> (Meet a -> Constr)
-> (Meet a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Meet a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Meet a)))
-> ((forall b. Data b => b -> b) -> Meet a -> Meet a)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Meet a -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Meet a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Meet a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Meet a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Meet a -> m (Meet a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Meet a -> m (Meet a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Meet a -> m (Meet a))
-> Data (Meet a)
Meet a -> DataType
Meet a -> Constr
(forall d. Data d => c (t d)) -> Maybe (c (Meet a))
(forall b. Data b => b -> b) -> Meet a -> Meet a
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Meet a -> c (Meet a)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Meet a)
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 u. Int -> (forall d. Data d => d -> u) -> Meet a -> u
forall u. (forall d. Data d => d -> u) -> Meet a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Meet a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Meet a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Meet a -> m (Meet a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Meet a -> m (Meet 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))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Meet a))
$cMeet :: Constr
$tMeet :: DataType
gmapMo :: (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 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 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 :: 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 d. Data d => d -> u) -> Meet a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Meet a -> [u]
gmapQr :: (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 :: (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 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 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 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 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)
$cp1Data :: forall a. Data a => Typeable (Meet a)
Data, (forall x. Meet a -> Rep (Meet a) x)
-> (forall x. Rep (Meet a) x -> Meet a) -> Generic (Meet a)
forall x. Rep (Meet a) x -> Meet a
forall x. Meet a -> Rep (Meet a) x
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 = a -> Meet a
forall a. a -> Meet a
Meet (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
b)

instance BoundedMeetSemiLattice a => Monoid (Meet a) where
  mempty :: Meet a
mempty = a -> Meet a
forall a. a -> Meet a
Meet a
forall a. BoundedMeetSemiLattice a => a
top
  Meet a
a mappend :: Meet a -> Meet a -> Meet a
`mappend` Meet a
b = a -> Meet a
forall a. a -> Meet a
Meet (a
a a -> 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) = a -> a -> Bool
forall a. (Eq a, Lattice a) => a -> a -> Bool
meetLeq a
a a
b

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

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

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

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

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

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

-- All

instance Lattice All where
  All Bool
a \/ :: All -> All -> All
\/ All Bool
b = Bool -> All
All (Bool -> All) -> Bool -> All
forall a b. (a -> b) -> a -> b
$ Bool
a Bool -> Bool -> Bool
forall a. Lattice a => a -> a -> a
\/ Bool
b
  All Bool
a /\ :: All -> All -> All
/\ All Bool
b = Bool -> All
All (Bool -> All) -> Bool -> All
forall a b. (a -> b) -> a -> b
$ Bool
a Bool -> Bool -> Bool
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 (Bool -> Any) -> Bool -> Any
forall a b. (a -> b) -> a -> b
$ Bool
a Bool -> Bool -> Bool
forall a. Lattice a => a -> a -> a
\/ Bool
b
  Any Bool
a /\ :: Any -> Any -> Any
/\ Any Bool
b = Bool -> Any
Any (Bool -> Any) -> Bool -> Any
forall a b. (a -> b) -> a -> b
$ Bool
a Bool -> Bool -> Bool
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 = (a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo ((a -> a) -> Endo a) -> (a -> a) -> Endo a
forall a b. (a -> b) -> a -> b
$ a -> a
a (a -> a) -> (a -> 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 = (a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo ((a -> a) -> Endo a) -> (a -> a) -> Endo a
forall a b. (a -> b) -> a -> b
$ a -> a
a (a -> a) -> (a -> a) -> a -> a
forall a. Lattice a => a -> a -> a
/\ a -> a
b

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

instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Endo a) where
  top :: Endo a
top = (a -> a) -> Endo a
forall a. (a -> a) -> Endo a
Endo a -> a
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 = a -> Tagged t a
forall k (s :: k) b. b -> Tagged s b
Tagged (a -> Tagged t a) -> a -> Tagged t a
forall a b. (a -> b) -> a -> b
$ a
a a -> 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 = a -> Tagged t a
forall k (s :: k) b. b -> Tagged s b
Tagged (a -> Tagged t a) -> a -> Tagged t a
forall a b. (a -> b) -> a -> b
$ a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
b

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

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

-- Proxy
instance Lattice (Proxy a) where
  Proxy a
_ \/ :: 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
_ = Proxy a
forall k (t :: k). Proxy t
Proxy

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

instance BoundedMeetSemiLattice (Proxy a) where
  top :: Proxy a
top = Proxy a
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 = a -> Identity a
forall a. a -> Identity a
Identity (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
\/ a
b)
  Identity a
a /\ :: Identity a -> Identity a -> Identity a
/\ Identity a
b = a -> Identity a
forall a. a -> Identity a
Identity (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
b)

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

instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Identity a) where
  bottom :: Identity a
bottom = a -> Identity a
forall a. a -> Identity a
Identity a
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 = a -> Const a b
forall k a (b :: k). a -> Const a b
Const (a
a a -> 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 = a -> Const a b
forall k a (b :: k). a -> Const a b
Const (a
a a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
b)

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

instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Const a b) where
  top :: Const a b
top = a -> Const a b
forall k a (b :: k). a -> Const a b
Const a
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
(\/) = Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
(QC..||.)
  /\ :: Property -> Property -> Property
(/\) = Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
(QC..&&.)

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

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

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

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

-- | @since 2.0.3
instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Solo a) where
  bottom :: Solo a
bottom = a -> Solo a
forall a. a -> Solo a
Solo a
forall a. BoundedJoinSemiLattice a => a
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 :: (a -> a) -> a
unsafeLfp = a -> (a -> a) -> a
forall a. Eq a => a -> (a -> a) -> a
PO.unsafeLfpFrom a
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 :: (a -> a) -> a
lfp = a -> (a -> a) -> a
forall a. (Eq a, BoundedJoinSemiLattice a) => a -> (a -> a) -> a
lfpFrom a
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 :: a -> (a -> a) -> a
lfpFrom a
init_x a -> a
f = a -> (a -> a) -> a
forall a. Eq a => a -> (a -> a) -> a
PO.unsafeLfpFrom a
init_x (\a
x -> a -> a
f a
x a -> a -> a
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 :: (a -> a) -> a
unsafeGfp = a -> (a -> a) -> a
forall a. Eq a => a -> (a -> a) -> a
PO.unsafeGfpFrom a
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 :: (a -> a) -> a
gfp = a -> (a -> a) -> a
forall a. (Eq a, BoundedMeetSemiLattice a) => a -> (a -> a) -> a
gfpFrom a
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 :: a -> (a -> a) -> a
gfpFrom a
init_x a -> a
f = a -> (a -> a) -> a
forall a. Eq a => a -> (a -> a) -> a
PO.unsafeGfpFrom a
init_x (\a
x -> a -> a
f a
x a -> a -> a
forall a. Lattice a => a -> a -> a
/\ a
x)