{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE Safe #-}
module Algebra.Lattice (
Lattice (..),
joinLeq, joins1, meetLeq, meets1,
BoundedJoinSemiLattice(..), BoundedMeetSemiLattice(..),
joins, meets,
fromBool,
BoundedLattice,
Meet(..), Join(..),
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 /\
infixr 5 \/
class Lattice a where
(\/) :: a -> a -> a
(/\) :: a -> a -> a
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
class Lattice a => BoundedJoinSemiLattice a where
bottom :: a
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
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
class Lattice a => BoundedMeetSemiLattice a where
top :: a
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
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)
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
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
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
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
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)
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
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)
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
instance Lattice () where
()
_ \/ :: () -> () -> ()
\/ ()
_ = ()
()
_ /\ :: () -> () -> ()
/\ ()
_ = ()
instance BoundedJoinSemiLattice () where
bottom :: ()
bottom = ()
instance BoundedMeetSemiLattice () where
top :: ()
top = ()
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)
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)
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
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
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
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
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
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
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
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
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
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
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
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
instance Lattice Void where
Void
a \/ :: Void -> Void -> Void
\/ Void
_ = Void
a
Void
a /\ :: Void -> Void -> Void
/\ Void
_ = Void
a
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
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)
instance BoundedMeetSemiLattice a => BoundedMeetSemiLattice (Solo a) where
top :: Solo a
top = MkSolo top
instance BoundedJoinSemiLattice a => BoundedJoinSemiLattice (Solo a) where
bottom :: Solo a
bottom = MkSolo bottom
{-# 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
{-# 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
{-# 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)
{-# 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
{-# 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
{-# 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)