packages feed

lattices 1.5.0 → 1.6.0

raw patch · 13 files changed

+682/−261 lines, 13 filesdep +base-compatdep +quickcheck-instancesdep +semigroupoidsdep ~QuickCheckdep ~basedep ~containers

Dependencies added: base-compat, quickcheck-instances, semigroupoids, universe-instances-base

Dependency ranges changed: QuickCheck, base, containers, tasty-quickcheck, transformers, unordered-containers

Files

Algebra/Lattice.hs view
@@ -1,6 +1,10 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-}+#if __GLASGOW_HASKELL__ >=710 && MIN_VERSION_unordered_containers(0,2,6)+{-# LANGUAGE Safe #-}+#else {-# LANGUAGE Trustworthy #-}+#endif {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-} #if __GLASGOW_HASKELL__ >= 707 && __GLASGOW_HASKELL__ < 709@@ -41,17 +45,13 @@     gfp, gfpFrom, unsafeGfp,   ) where +import Prelude ()+import Prelude.Compat+ import qualified Algebra.PartialOrd as PO  import           Data.Universe.Class (Universe(..), Finite(..)) -#if MIN_VERSION_base(4,8,0)-#else-import           Control.Applicative (Applicative(..))-import           Data.Foldable       (Foldable, foldMap)-import           Data.Monoid         (Monoid(..))-#endif- import           Control.Monad.Zip (MonadZip(..)) import           Data.Data         (Data, Typeable) import           Data.Hashable     (Hashable(..))@@ -70,9 +70,8 @@ import qualified Data.HashMap.Lazy as HM  import Control.Applicative (Const(..))-#if MIN_VERSION_base(4,8,0) import Data.Functor.Identity (Identity(..))-#endif+import Data.Semigroup.Foldable (Foldable1 (..))  infixr 6 /\ -- This comment needed because of CPP infixr 5 \/@@ -98,10 +97,6 @@ joinLeq :: (Eq a, JoinSemiLattice a) => a -> a -> Bool joinLeq x y = (x \/ y) == y --- | The join of at a list of join-semilattice elements (of length at least one)-joins1 :: JoinSemiLattice a => [a] -> a-joins1 = foldr1 (\/)- -- | A algebraic structure with element meets: <http://en.wikipedia.org/wiki/Semilattice> -- -- > Associativity: x /\ (y /\ z) == (x /\ y) /\ z@@ -123,10 +118,8 @@ meetLeq :: (Eq a, MeetSemiLattice a) => a -> a -> Bool meetLeq x y = (x /\ y) == x --- | The meet of at a list of meet-semilattice elements (of length at least one)-meets1 :: MeetSemiLattice a => [a] -> a-meets1 = foldr1 (/\) + -- | The combination of two semi lattices makes a lattice if the absorption law holds: -- see <http://en.wikipedia.org/wiki/Absorption_law> and <http://en.wikipedia.org/wiki/Lattice_(order)> --@@ -143,6 +136,10 @@ joins :: (BoundedJoinSemiLattice a, Foldable f) => f a -> a joins = getJoin . foldMap Join +-- | The join of at a list of join-semilattice elements (of length at least one)+joins1 :: (JoinSemiLattice a, Foldable1 f) => f a -> a+joins1 =  getJoin . foldMap1 Join+ -- | A meet-semilattice with some element |top| that /\ approaches. -- -- > Identity: x /\ top == x@@ -152,7 +149,10 @@ -- | The meet of a list of meet-semilattice elements meets :: (BoundedMeetSemiLattice a, Foldable f) => f a -> a meets = getMeet . foldMap Meet-+--+-- | The meet of at a list of meet-semilattice elements (of length at least one)+meets1 :: (MeetSemiLattice a, Foldable1 f) => f a -> a+meets1 = getMeet . foldMap1 Meet  -- | Lattices with both bounds class (Lattice a, BoundedJoinSemiLattice a, BoundedMeetSemiLattice a) => BoundedLattice a where@@ -189,6 +189,11 @@ instance JoinSemiLattice IS.IntSet where     (\/) = IS.union +instance MeetSemiLattice IS.IntSet where+    (/\) = IS.intersection++instance Lattice IS.IntSet+ instance BoundedJoinSemiLattice IS.IntSet where     bottom = IS.empty @@ -202,6 +207,8 @@ instance (Eq a, Hashable a) => MeetSemiLattice (HS.HashSet a) where     (/\) = HS.intersection +instance (Eq a, Hashable a) => Lattice (HS.HashSet a)+ instance (Eq a, Hashable a) => BoundedJoinSemiLattice (HS.HashSet a) where     bottom = HS.empty @@ -234,6 +241,12 @@  instance JoinSemiLattice v => BoundedJoinSemiLattice (IM.IntMap v) where     bottom = IM.empty++instance MeetSemiLattice v => MeetSemiLattice (IM.IntMap v) where+    (/\) = IM.intersectionWith (/\)++instance Lattice v => Lattice (IM.IntMap v)+  -- -- HashMaps
+ Algebra/Lattice/Divisibility.hs view
@@ -0,0 +1,77 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DeriveDataTypeable #-}+#if __GLASGOW_HASKELL__ < 709+{-# LANGUAGE Trustworthy #-}+#else+{-# LANGUAGE Safe #-}+#endif+----------------------------------------------------------------------------+-- |+-- Module      :  Algebra.Lattice.Divisibility+-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke, 2015 Oleg Grenrus+-- License     :  BSD-3-Clause (see the file LICENSE)+--+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------+module Algebra.Lattice.Divisibility (+    Divisibility(..)+  ) where++import Prelude ()+import Prelude.Compat++import Algebra.Lattice+import Algebra.PartialOrd++import Control.DeepSeq+import Control.Monad+import Data.Data+import Data.Hashable+import GHC.Generics++--+-- Divisibility+--++-- | A divisibility lattice. @'join' = 'lcm'@, @'meet' = 'gcd'@. +newtype Divisibility a = Divisibility { getDivisibility :: a }+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable+#if __GLASGOW_HASKELL__ >= 706+           , Generic1+#endif+           )++instance Applicative Divisibility where+  pure = return+  (<*>) = ap++instance Monad Divisibility where+  return           = Divisibility+  Divisibility x >>= f  = f x++instance NFData a => NFData (Divisibility a) where+  rnf (Divisibility a) = rnf a++instance Hashable a => Hashable (Divisibility a)++instance Integral a => JoinSemiLattice (Divisibility a) where+  Divisibility x \/ Divisibility y = Divisibility (lcm x y)++instance Integral a => MeetSemiLattice (Divisibility a) where+  Divisibility x /\ Divisibility y = Divisibility (gcd x y)++instance Integral a => Lattice (Divisibility a) where++instance Integral a => BoundedJoinSemiLattice (Divisibility a) where+  bottom = Divisibility 1++instance (Eq a, Integral a) => PartialOrd (Divisibility a) where+    leq (Divisibility a) (Divisibility b) = b `mod` a == 0
Algebra/Lattice/Dropped.hs view
@@ -1,6 +1,9 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DeriveDataTypeable #-}@@ -23,20 +26,11 @@   , retractDropped   ) where -#ifndef MIN_VERSION_base-#define MIN_VERSION_base(x,y,z) 1-#endif+import Prelude ()+import Prelude.Compat  import Algebra.Lattice -#if MIN_VERSION_base(4,8,0)-#else-import Control.Applicative-import Data.Monoid (Monoid(..))-import Data.Foldable-import Data.Traversable-#endif- import Control.DeepSeq import Control.Monad import Data.Data@@ -51,23 +45,11 @@ -- As a bonus, the top will be an absorbing element for the join. data Dropped a = Top                | Drop a-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable #if __GLASGOW_HASKELL__ >= 706            , Generic1 #endif            )--instance Functor Dropped where-  fmap _ Top      = Top-  fmap f (Drop a) = Drop (f a)--instance Foldable Dropped where-  foldMap _ Top      = mempty-  foldMap f (Drop a) = f a--instance Traversable Dropped where-  traverse _ Top      = pure Top-  traverse f (Drop a) = Drop <$> f a  instance Applicative Dropped where   pure = return
+ Algebra/Lattice/Free.hs view
@@ -0,0 +1,148 @@+{-# LANGUAGE RankNTypes #-}++----------------------------------------------------------------------------+-- |+-- Module      :  Algebra.Lattice.Free+-- License     :  BSD-3-Clause (see the file LICENSE)+--+-- Maintainer  :  Oleg Grenrus <oleg.grenrus@iki.fi>+--+----------------------------------------------------------------------------++module Algebra.Lattice.Free+  ( -- * Free join-semilattices+    FreeJoinSemiLattice+  , liftFreeJoinSemiLattice+  , lowerFreeJoinSemiLattice+  , retractFreeJoinSemiLattice++   -- * Free meet-semilattices+  , FreeMeetSemiLattice+  , liftFreeMeetSemiLattice+  , lowerFreeMeetSemiLattice+  , retractFreeMeetSemiLattice++   -- * Free lattices+  , FreeLattice+  , liftFreeLattice+  , lowerFreeLattice+  , retractFreeLattice+  ) where++import Prelude ()+import Prelude.Compat++import Algebra.Lattice+import Data.Universe.Class++--+-- Free join-semilattices+--++newtype FreeJoinSemiLattice a = FreeJoinSemiLattice+  { lowerFreeJoinSemiLattice :: forall b. JoinSemiLattice b =>+                                            (a -> b) -> b+  }++liftFreeJoinSemiLattice :: a -> FreeJoinSemiLattice a+liftFreeJoinSemiLattice a = FreeJoinSemiLattice (\inj -> inj a)++retractFreeJoinSemiLattice :: JoinSemiLattice a => FreeJoinSemiLattice a -> a+retractFreeJoinSemiLattice a = lowerFreeJoinSemiLattice a id++instance Functor FreeJoinSemiLattice where+  fmap f (FreeJoinSemiLattice g) = FreeJoinSemiLattice (\inj -> g (inj . f))+  a <$ FreeJoinSemiLattice f = FreeJoinSemiLattice (\inj -> f (const (inj a)))++instance JoinSemiLattice (FreeJoinSemiLattice a) where+  FreeJoinSemiLattice f \/ FreeJoinSemiLattice g =+    FreeJoinSemiLattice (\inj -> f inj \/ g inj)++instance BoundedJoinSemiLattice a =>+         BoundedJoinSemiLattice (FreeJoinSemiLattice a) where+  bottom = FreeJoinSemiLattice (\inj -> inj bottom)++instance Universe a => Universe (FreeJoinSemiLattice a) where+  universe = fmap liftFreeJoinSemiLattice universe++instance Finite a => Finite (FreeJoinSemiLattice a) where+  universeF = fmap liftFreeJoinSemiLattice universeF+++--+-- Free meet-semilattices+--++newtype FreeMeetSemiLattice a = FreeMeetSemiLattice+  { lowerFreeMeetSemiLattice :: forall b. MeetSemiLattice b =>+                                            (a -> b) -> b+  }++instance Functor FreeMeetSemiLattice where+  fmap f (FreeMeetSemiLattice g) = FreeMeetSemiLattice (\inj -> g (inj . f))+  a <$ FreeMeetSemiLattice f = FreeMeetSemiLattice (\inj -> f (const (inj a)))++liftFreeMeetSemiLattice :: a -> FreeMeetSemiLattice a+liftFreeMeetSemiLattice a = FreeMeetSemiLattice (\inj -> inj a)++retractFreeMeetSemiLattice :: MeetSemiLattice a => FreeMeetSemiLattice a -> a+retractFreeMeetSemiLattice a = lowerFreeMeetSemiLattice a id++instance MeetSemiLattice (FreeMeetSemiLattice a) where+  FreeMeetSemiLattice f /\ FreeMeetSemiLattice g =+    FreeMeetSemiLattice (\inj -> f inj /\ g inj)++instance BoundedMeetSemiLattice a =>+         BoundedMeetSemiLattice (FreeMeetSemiLattice a) where+  top = FreeMeetSemiLattice (\inj -> inj top)++instance Universe a => Universe (FreeMeetSemiLattice a) where+  universe = fmap liftFreeMeetSemiLattice universe++instance Finite a => Finite (FreeMeetSemiLattice a) where+  universeF = fmap liftFreeMeetSemiLattice universeF+++--+-- Free lattices+--++newtype FreeLattice a = FreeLattice+  { lowerFreeLattice :: forall b. Lattice b =>+                                    (a -> b) -> b+  }++instance Functor FreeLattice where+  fmap f (FreeLattice g) = FreeLattice (\inj -> g (inj . f))+  a <$ FreeLattice f = FreeLattice (\inj -> f (const (inj a)))++liftFreeLattice :: a -> FreeLattice a+liftFreeLattice a = FreeLattice (\inj -> inj a)++retractFreeLattice :: Lattice a => FreeLattice a -> a+retractFreeLattice a = lowerFreeLattice a id++instance JoinSemiLattice (FreeLattice a) where+  FreeLattice f \/ FreeLattice g = FreeLattice (\inj -> f inj \/ g inj)++instance MeetSemiLattice (FreeLattice a) where+  FreeLattice f /\ FreeLattice g = FreeLattice (\inj -> f inj /\ g inj)++instance Lattice (FreeLattice a)++instance BoundedJoinSemiLattice a =>+         BoundedJoinSemiLattice (FreeLattice a) where+  bottom = FreeLattice (\inj -> inj bottom)++instance BoundedMeetSemiLattice a =>+         BoundedMeetSemiLattice (FreeLattice a) where+  top = FreeLattice (\inj -> inj top)++instance BoundedLattice a =>+         BoundedLattice (FreeLattice a)++instance Universe a => Universe (FreeLattice a) where+  universe = fmap liftFreeLattice universe++instance Finite a => Finite (FreeLattice a) where+  universeF = fmap liftFreeLattice universeF
Algebra/Lattice/Levitated.hs view
@@ -1,6 +1,9 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DeriveDataTypeable #-}@@ -23,20 +26,11 @@   , retractLevitated   ) where -#ifndef MIN_VERSION_base-#define MIN_VERSION_base(x,y,z) 1-#endif+import Prelude ()+import Prelude.Compat  import Algebra.Lattice -#if MIN_VERSION_base(4,8,0)-#else-import Control.Applicative-import Data.Monoid (Monoid(..))-import Data.Foldable-import Data.Traversable-#endif- import Control.DeepSeq import Control.Monad import Data.Data@@ -53,25 +47,11 @@ data Levitated a = Top                  | Levitate a                  | Bottom-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable #if __GLASGOW_HASKELL__ >= 706            , Generic1 #endif            )-instance Functor Levitated where-  fmap _ Bottom       = Bottom-  fmap _ Top          = Top-  fmap f (Levitate a) = Levitate (f a)--instance Foldable Levitated where-  foldMap _ Bottom       = mempty-  foldMap _ Top          = mempty-  foldMap f (Levitate a) = f a--instance Traversable Levitated where-  traverse _ Bottom       = pure Bottom-  traverse _ Top          = pure Top-  traverse f (Levitate a) = Levitate <$> f a  instance Applicative Levitated where   pure = return
Algebra/Lattice/Lexicographic.hs view
@@ -1,6 +1,9 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DeriveDataTypeable #-}@@ -22,20 +25,12 @@     Lexicographic(..)   ) where -#ifndef MIN_VERSION_base-#define MIN_VERSION_base(x,y,z) 1-#endif+import Prelude ()+import Prelude.Compat  import Algebra.Lattice import Algebra.PartialOrd -#if MIN_VERSION_base(4,8,0)-#else-import Control.Applicative-import Data.Foldable-import Data.Traversable-#endif- import Control.DeepSeq import Control.Monad import Data.Data@@ -60,21 +55,12 @@ -- 'Timestamps'.  Typically this is done in an arbitary, but -- deterministic manner. data Lexicographic k v = Lexicographic !k !v-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable #if __GLASGOW_HASKELL__ >= 706            , Generic1 #endif            ) -instance Foldable (Lexicographic k) where-  foldMap f (Lexicographic _ v) = f v--instance Traversable (Lexicographic k) where-  traverse f (Lexicographic k v) = Lexicographic k <$> f v--instance Functor (Lexicographic k) where-  fmap f (Lexicographic k v) = Lexicographic k (f v)- instance BoundedJoinSemiLattice k => Applicative (Lexicographic k) where   pure = return   (<*>) = ap@@ -91,19 +77,40 @@  instance (Hashable k, Hashable v) => Hashable (Lexicographic k v) -instance (PartialOrd k, JoinSemiLattice k, JoinSemiLattice v) => JoinSemiLattice (Lexicographic k v) where+-- Why we have 'bottom', and not @v1 \\/ v2@ in the @otherwise@ clause?+--+-- For example what is the join of @(2, 1)@ and @(3, 2)@+-- in lexicographic divisibility divisibility lattice.+--+-- With @v1 \\/ v2@, we get the upper bound, but not least!+--+-- @+-- (2, 1) `leq` (6, 2)+-- (3, 2) `leq` (6, 2)+-- @+--+-- But @(6, 1) `leq` (6, 2)@, and+--+-- @+-- (2, 1) `leq` (6, 1)+-- (3, 2) `leq` (6, 1)+-- @+--+instance (PartialOrd k, JoinSemiLattice k, BoundedJoinSemiLattice v) => JoinSemiLattice (Lexicographic k v) where   l@(Lexicographic k1 v1) \/ r@(Lexicographic k2 v2)+    | k1 == k2 = Lexicographic k1 (v1 \/ v2)     | k1 `leq` k2 = r     | k2 `leq` k1 = l-    | otherwise   = Lexicographic (k1 \/ k2) (v1 \/ v2)+    | otherwise   = Lexicographic (k1 \/ k2) bottom -instance (PartialOrd k, MeetSemiLattice k, MeetSemiLattice v) => MeetSemiLattice (Lexicographic k v) where+instance (PartialOrd k, MeetSemiLattice k, BoundedMeetSemiLattice v) => MeetSemiLattice (Lexicographic k v) where   l@(Lexicographic k1 v1) /\ r@(Lexicographic k2 v2)+    | k1 == k2 = Lexicographic k1 (v1 /\ v2)     | k1 `leq` k2 = l     | k2 `leq` k1 = r-    | otherwise   = Lexicographic (k1 /\ k2) (v1 /\ v2)+    | otherwise   = Lexicographic (k1 /\ k2) top -instance (PartialOrd k, Lattice k, Lattice v) => Lattice (Lexicographic k v) where+instance (PartialOrd k, Lattice k, BoundedLattice v) => Lattice (Lexicographic k v) where  instance (PartialOrd k, BoundedJoinSemiLattice k, BoundedJoinSemiLattice v) => BoundedJoinSemiLattice (Lexicographic k v) where   bottom = Lexicographic bottom bottom@@ -115,6 +122,9 @@  instance (PartialOrd k, PartialOrd v) => PartialOrd (Lexicographic k v) where   Lexicographic k1 v1 `leq` Lexicographic k2 v2+    | k1   ==  k2 = v1 `leq` v2     | k1 `leq` k2 = True-    | k1   ==  k1 = v1 `leq` v2     | otherwise   = False -- Incomparable or k2 `leq` k1+  comparable (Lexicographic k1 v1) (Lexicographic k2 v2)+    | k1 == k2 = comparable v1 v2+    | otherwise = comparable k1 k2
Algebra/Lattice/Lifted.hs view
@@ -1,6 +1,9 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeOperators #-} #if __GLASGOW_HASKELL__ < 709@@ -22,20 +25,11 @@   , retractLifted   ) where -#ifndef MIN_VERSION_base-#define MIN_VERSION_base(x,y,z) 1-#endif+import Prelude ()+import Prelude.Compat  import Algebra.Lattice -#if MIN_VERSION_base(4,8,0)-#else-import Control.Applicative-import Data.Monoid (Monoid(..))-import Data.Foldable-import Data.Traversable-#endif- import Control.DeepSeq import Control.Monad import Data.Data@@ -50,23 +44,11 @@ -- As a bonus, the bottom will be an absorbing element for the meet. data Lifted a = Lift a               | Bottom-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable #if __GLASGOW_HASKELL__ >= 706            , Generic1 #endif            )--instance Functor Lifted where-  fmap _ Bottom   = Bottom-  fmap f (Lift a) = Lift (f a)--instance Foldable Lifted where-  foldMap _ Bottom   = mempty-  foldMap f (Lift a) = f a--instance Traversable Lifted where-  traverse _ Bottom   = pure Bottom-  traverse f (Lift a) = Lift <$> f a  instance Applicative Lifted where   pure = return
Algebra/Lattice/Op.hs view
@@ -1,6 +1,9 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DeriveDataTypeable #-}@@ -22,20 +25,12 @@     Op(..)   ) where -#ifndef MIN_VERSION_base-#define MIN_VERSION_base(x,y,z) 1-#endif+import Prelude ()+import Prelude.Compat  import Algebra.Lattice import Algebra.PartialOrd -#if MIN_VERSION_base(4,8,0)-#else-import Control.Applicative-import Data.Foldable-import Data.Traversable-#endif- import Control.DeepSeq import Control.Monad import Data.Data@@ -49,21 +44,12 @@ -- | The opposite lattice of a given lattice.  That is, switch -- meets and joins. newtype Op a = Op { getOp :: a }-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable #if __GLASGOW_HASKELL__ >= 706            , Generic1 #endif            ) -instance Foldable Op where-  foldMap f (Op a) = f a--instance Traversable Op where-  traverse f (Op a) = Op <$> f a--instance Functor Op where-  fmap f (Op a) = Op (f a)- instance Applicative Op where   pure = return   (<*>) = ap@@ -83,7 +69,7 @@ instance JoinSemiLattice a => MeetSemiLattice (Op a) where   Op x /\ Op y = Op (x \/ y) -instance (Lattice a, Ord a) => Lattice (Op a) where+instance Lattice a => Lattice (Op a) where  instance BoundedMeetSemiLattice a => BoundedJoinSemiLattice (Op a) where   bottom = Op top@@ -91,7 +77,8 @@ instance BoundedJoinSemiLattice a => BoundedMeetSemiLattice (Op a) where   top = Op bottom -instance (BoundedLattice a, Ord a, Bounded a) => BoundedLattice (Op a) where+instance BoundedLattice a => BoundedLattice (Op a) where  instance PartialOrd a => PartialOrd (Op a) where     Op a `leq` Op b = b `leq` a -- Note swap.+    comparable (Op a) (Op b) = comparable a b
Algebra/Lattice/Ordered.hs view
@@ -1,6 +1,9 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE DeriveDataTypeable #-}@@ -22,20 +25,12 @@     Ordered(..)   ) where -#ifndef MIN_VERSION_base-#define MIN_VERSION_base(x,y,z) 1-#endif+import Prelude ()+import Prelude.Compat  import Algebra.Lattice import Algebra.PartialOrd -#if MIN_VERSION_base(4,8,0)-#else-import Control.Applicative-import Data.Foldable-import Data.Traversable-#endif- import Control.DeepSeq import Control.Monad import Data.Data@@ -49,21 +44,12 @@ -- | A total order gives rise to a lattice. Join is -- max, meet is min. newtype Ordered a = Ordered { getOrdered :: a }-  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic+  deriving ( Eq, Ord, Show, Read, Data, Typeable, Generic, Functor, Foldable, Traversable #if __GLASGOW_HASKELL__ >= 706            , Generic1 #endif            ) -instance Foldable Ordered where-  foldMap f (Ordered a) = f a--instance Traversable Ordered where-  traverse f (Ordered a) = Ordered <$> f a--instance Functor Ordered where-  fmap f (Ordered a) = Ordered (f a)- instance Applicative Ordered where   pure = return   (<*>) = ap@@ -83,7 +69,7 @@ instance Ord a => MeetSemiLattice (Ordered a) where   Ordered x /\ Ordered y = Ordered (min x y) -instance (Lattice a, Ord a) => Lattice (Ordered a) where+instance Ord a => Lattice (Ordered a) where  instance (Ord a, Bounded a) => BoundedJoinSemiLattice (Ordered a) where   bottom = Ordered minBound@@ -91,7 +77,8 @@ instance (Ord a, Bounded a) => BoundedMeetSemiLattice (Ordered a) where   top = Ordered maxBound -instance (BoundedLattice a, Ord a, Bounded a) => BoundedLattice (Ordered a) where+instance (Ord a, Bounded a) => BoundedLattice (Ordered a) where  instance Ord a => PartialOrd (Ordered a) where     leq = (<=)+    comparable _ _ = True
Algebra/PartialOrd.hs view
@@ -18,37 +18,82 @@     gfpFrom, unsafeGfpFrom   ) where -import qualified Data.Set as S+import qualified Data.IntMap as IM import qualified Data.IntSet as IS import qualified Data.Map as M-import qualified Data.IntMap as IM-+import qualified Data.Set as S --- | A partial ordering on sets: <http://en.wikipedia.org/wiki/Partially_ordered_set>+-- | A partial ordering on sets+-- (<http://en.wikipedia.org/wiki/Partially_ordered_set>) is a set equipped+-- with a binary relation, `leq`, that obeys the following laws ----- This can be defined using either 'joinLeq' or 'meetLeq', or a more efficient definition--- can be derived directly.+-- @+-- Reflexive:     a ``leq`` a+-- Antisymmetric: a ``leq`` b && b ``leq`` a ==> a == b+-- Transitive:    a ``leq`` b && b ``leq`` c ==> a ``leq`` c+-- @ --+-- Two elements of the set are said to be `comparable` when they are are+-- ordered with respect to the `leq` relation. So+-- -- @--- Reflexive:     a `leq` a--- Antisymmetric: a `leq` b && b `leq` a ==> a == b--- Transitive:    a `leq` b && b `leq` c ==> a `leq` c+-- `comparable` a b ==> a ``leq`` b || b ``leq`` a -- @ ----- The superclass equality (which can be defined using 'partialOrdEq') must obey these laws:+-- If `comparable` always returns true then the relation `leq` defines a+-- total ordering (and an `Ord` instance may be defined). Any `Ord` instance is+-- trivially an instance of `PartialOrd`. 'Algebra.Lattice.Ordered' provides a+-- convenient wrapper to satisfy 'PartialOrd' given 'Ord'. --+-- As an example consider the partial ordering on sets induced by set+-- inclusion.  Then for sets `a` and `b`,+-- -- @--- Reflexive:  a == a--- Transitive: a == b && b == c ==> a == b+-- a ``leq`` b -- @+--+-- is true when `a` is a subset of `b`.  Two sets are `comparable` if one is a+-- subset of the other. Concretely+--+-- @+-- a = {1, 2, 3}+-- b = {1, 3, 4}+-- c = {1, 2}+--+-- a ``leq`` a = `True`+-- a ``leq`` b = `False`+-- a ``leq`` c = `False`+-- b ``leq`` a = `False`+-- b ``leq`` b = `True`+-- b ``leq`` c = `False`+-- c ``leq`` a = `True`+-- c ``leq`` b = `False`+-- c ``leq`` c = `True`+--+-- `comparable` a b = `False`+-- `comparable` a c = `True`+-- `comparable` b c = `False`+-- @ class Eq a => PartialOrd a where+    -- | The relation that induces the partial ordering     leq :: a -> a -> Bool --- | The equality relation induced by the partial-order structure+    -- | Whether two elements are ordered with respect to the relation. A+    -- default implementation is given by+    --+    -- > comparable x y = leq x y || leq y x+    comparable :: a -> a -> Bool+    comparable x y = leq x y || leq y x++-- | The equality relation induced by the partial-order structure. It must obey+-- the laws+-- @+-- Reflexive:  a == a+-- Transitive: a == b && b == c ==> a == c+-- @ partialOrdEq :: PartialOrd a => a -> a -> Bool partialOrdEq x y = leq x y && leq y x - instance Ord a => PartialOrd (S.Set a) where     leq = S.isSubsetOf @@ -56,16 +101,15 @@     leq = IS.isSubsetOf  instance (Ord k, PartialOrd v) => PartialOrd (M.Map k v) where-    m1 `leq` m2 = m1 `M.isSubmapOf` m2 && M.fold (\(x1, x2) b -> b && x1 `leq` x2) True (M.intersectionWith (,) m1 m2)+    leq = M.isSubmapOfBy leq  instance PartialOrd v => PartialOrd (IM.IntMap v) where-    im1 `leq` im2 = im1 `IM.isSubmapOf` im2 && IM.fold (\(x1, x2) b -> b && x1 `leq` x2) True (IM.intersectionWith (,) im1 im2)+    leq = IM.isSubmapOfBy leq  instance (PartialOrd a, PartialOrd b) => PartialOrd (a, b) where     -- NB: *not* a lexical ordering. This is because for some component partial orders, lexical     -- ordering is incompatible with the transitivity axiom we require for the derived partial order     (x1, y1) `leq` (x2, y2) = x1 `leq` x2 && y1 `leq` y2-  -- | Least point of a partially ordered monotone function. Checks that the function is monotone. lfpFrom :: PartialOrd a => a -> (a -> a) -> a
CHANGELOG.md view
@@ -1,3 +1,13 @@+# 1.6.0 (2017-06-26)++- Correct PartialOrd Map and IntMap instances+- Add Lattice instance for `containers` types.+- Change `meets1` and `joins1` to use `Foldable1`+- Add `comparable` to `PartialOrd`+- Add `Algebra.Lattice.Free` module+- Add `Divisibility` lattice.+- Fix `Lexicographic`.+ # 1.5.0 (2015-12-18)  - Move `PartialOrd (k -> v)` instance into own module
lattices.cabal view
@@ -1,5 +1,5 @@ name:               lattices-version:            1.5.0+version:            1.6.0 cabal-version:      >= 1.10 category:           Math license:            BSD3@@ -7,14 +7,19 @@ author:             Maximilian Bolingbroke <batterseapower@hotmail.com> maintainer:         Oleg Grenrus <oleg.grenrus@iki.fi> homepage:           http://github.com/phadej/lattices/-bug-reports:        http://github.com/phadej/lattices.git/issues+bug-reports:        http://github.com/phadej/lattices/issues copyright:          (C) 2010-2015 Maximilian Bolingbroke build-type:         Simple extra-source-files: README.md CHANGELOG.md-tested-with:        GHC==7.4.2, GHC==7.6.3, GHC==7.8.4, GHC==7.10.2+tested-with:        GHC==7.4.2, GHC==7.6.3, GHC==7.8.4, GHC==7.10.3, GHC==8.0.2, GHC==8.2.1 synopsis:           Fine-grained library for constructing and manipulating lattices description:-  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 mathematics, a lattice is a partially ordered set in which every two+  elements @x@ and @y@ have a unique supremum (also called a least upper bound, join, or @x /\\ y@)+  and a unique infimum (also called a greatest lower bound, meet, or @x \\/ y@).+  .+  This package provide type-classes for different lattice types, as well+  as a class for the partial order.  source-repository head   type: git@@ -23,7 +28,9 @@ library   exposed-modules:  Algebra.Enumerable,                     Algebra.Lattice,+                    Algebra.Lattice.Divisibility,                     Algebra.Lattice.Dropped,+                    Algebra.Lattice.Free,                     Algebra.Lattice.Levitated,                     Algebra.Lattice.Lexicographic,                     Algebra.Lattice.Lifted,@@ -32,19 +39,26 @@                     Algebra.PartialOrd,                     Algebra.PartialOrd.Instances -  build-depends:    base                       >= 4.5  && < 4.9,+  build-depends:    base                       >= 4.5  && < 4.11,+                    base-compat                >= 0.9.3 && < 0.10,                     containers                 >= 0.3  && < 0.6,                     deepseq                    >= 1.1  && < 1.5,                     hashable                   >= 1.2  && < 1.3,-                    semigroups                 >= 0.16 && < 0.19,                     tagged                     >= 0.7  && < 0.9,-                    void                       >= 0.7  && < 0.8,                     unordered-containers       >= 0.2  && < 0.3,+                    semigroupoids              >= 5.2  && < 5.3,                     universe-base              >= 1.0  && < 1.1,                     universe-reverse-instances >= 1.0  && < 1.1   ghc-options:      -Wall   default-language: Haskell2010 +  if !impl(ghc >= 8.0)+    build-depends:  semigroups                 >= 0.16 && < 0.19++  if !impl(ghc >= 7.10)+    build-depends:   void                       >= 0.7  && < 0.8,+                     transformers               >= 0.3  && < 0.6+   if impl(ghc >= 7.4 && < 7.5)     build-depends:  ghc-prim @@ -54,9 +68,14 @@   hs-source-dirs:      test   ghc-options:         -Wall   default-language:    Haskell2010-  build-depends:       base              >= 4.5  && < 4.9,-                       tasty             >= 0.10 && < 0.12,-                       tasty-quickcheck  >= 0.8  && < 0.9,+  build-depends:       base,+                       base-compat          >= 0.9.3 && <0.10,+                       tasty                >= 0.10  && < 0.12,+                       tasty-quickcheck     >= 0.8   && < 0.10,+                       QuickCheck           >= 2.10  && <2.11,+                       quickcheck-instances >=0.3.16 && <0.4,+                       universe-instances-base >= 1.0 && <1.1,                        lattices,+                       containers,                        transformers,-                       QuickCheck+                       unordered-containers
test/Tests.hs view
@@ -5,21 +5,20 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} module Main (main) where -#if MIN_VERSION_base(4,8,0)-#else-import Control.Applicative-import Data.Foldable-#endif+import Prelude ()+import Prelude.Compat -import Data.Functor.Compose-import Data.Functor.Identity-import Data.Monoid-import Data.Traversable-import Control.Monad (ap)+import Data.Maybe (listToMaybe, isJust)+import Data.Monoid ((<>))+import Control.Monad (ap, guard) import Test.QuickCheck.Function import Test.Tasty import Test.Tasty.QuickCheck as QC +import Algebra.Lattice+import Algebra.PartialOrd++import qualified Algebra.Lattice.Divisibility as Div import qualified Algebra.Lattice.Dropped as D import qualified Algebra.Lattice.Levitated as L import qualified Algebra.Lattice.Lexicographic as LO@@ -27,81 +26,44 @@ import qualified Algebra.Lattice.Op as Op import qualified Algebra.Lattice.Ordered as O +import Data.IntMap (IntMap)+import Data.IntSet (IntSet)+import Data.Map (Map)+import Data.Set (Set)++import Data.Universe.Instances.Base ()+import Test.QuickCheck.Instances ()+ -- For old GHC to work+data Proxy (a :: *) = Proxy data Proxy1 (a :: * -> *) = Proxy1  main :: IO () main = defaultMain tests  tests :: TestTree-tests = testGroup "Tests" [theseProps]--theseProps :: TestTree-theseProps = testGroup "These"-  [ functorLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)-  , functorLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated)-  , functorLaws "Lexicographic" (Proxy1 :: Proxy1 (LO.Lexicographic Bool))-  , functorLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)-  , functorLaws "Op" (Proxy1 :: Proxy1 Op.Op)-  , functorLaws "Ordered" (Proxy1 :: Proxy1 O.Ordered)+tests = testGroup "Tests"+  [ latticeLaws "M3" False (Proxy :: Proxy M3) -- non distributive lattice!+  , latticeLaws "M2" True (Proxy :: Proxy M2) -- M2+  , latticeLaws "Map" True (Proxy :: Proxy (Map Int (O.Ordered Int)))+  , latticeLaws "IntMap" True (Proxy :: Proxy (IntMap (O.Ordered Int)))+  , latticeLaws "Set" True (Proxy :: Proxy (Set Int))+  , latticeLaws "IntSet" True (Proxy :: Proxy IntSet)+  , latticeLaws "Ordered" True (Proxy :: Proxy (O.Ordered Int))+  , latticeLaws "Divisibility" True (Proxy :: Proxy (Div.Divisibility Int))+  , latticeLaws "LexOrdered" True (Proxy :: Proxy (LO.Lexicographic (O.Ordered Int) (O.Ordered Int)))+  , latticeLaws "Lexicographic" False (Proxy :: Proxy (LO.Lexicographic (Set Bool) (Set Bool)))+  , latticeLaws "Lexicographic" False (Proxy :: Proxy (LO.Lexicographic M2 M2)) -- non distributive!+  , testProperty "Lexicographic M2 M2 contains M3" $ QC.property $+      isJust searchM3LexM2   , monadLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)   , monadLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated)   , monadLaws "Lexicographic" (Proxy1 :: Proxy1 (LO.Lexicographic Bool))   , monadLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)   , monadLaws "Op" (Proxy1 :: Proxy1 Op.Op)   , monadLaws "Ordered" (Proxy1 :: Proxy1 O.Ordered)-  , traversableLaws "Dropped" (Proxy1 :: Proxy1 D.Dropped)-  , traversableLaws "Levitated" (Proxy1 :: Proxy1 L.Levitated)-  , traversableLaws "Lexicographic" (Proxy1 :: Proxy1 (LO.Lexicographic Bool))-  , traversableLaws "Lifted" (Proxy1 :: Proxy1 U.Lifted)-  , traversableLaws "Op" (Proxy1 :: Proxy1 Op.Op)-  , traversableLaws "Ordered" (Proxy1 :: Proxy1 O.Ordered)   ] -functorLaws :: forall (f :: * -> *). ( Functor f-                                     , Arbitrary (f Int)-                                     , Eq (f Int)-                                     , Show (f Int))-            => String-            -> Proxy1 f-            -> TestTree-functorLaws name _ = testGroup ("Functor laws: " <> name)-  [ QC.testProperty "identity" identityProp-  , QC.testProperty "composition" compositionProp-  ]-  where-    identityProp :: f Int -> Property-    identityProp x = fmap id x === x--    compositionProp :: f Int -> Fun Int Int -> Fun Int Int -> Property-    compositionProp x (Fun _ f) (Fun _ g) = fmap g (fmap f x) === fmap (g . f) x--traversableLaws :: forall (t :: * -> *). ( Traversable t-                                         , Arbitrary (t Int)-                                         , Eq (t Int)-                                         , Show (t Int))-                => String-                -> Proxy1 t-                -> TestTree-traversableLaws name _ = testGroup ("Traversable laws: " <> name)-  [ QC.testProperty "identity" identityProp-  , QC.testProperty "composition" compositionProp-  , QC.testProperty "functor" functorProp-  , QC.testProperty "foldable" foldableProp-  ]-  where-    identityProp :: t Int -> Property-    identityProp x = traverse Identity x === Identity x--    compositionProp :: t Int -> Fun Int (Maybe Int) -> Fun Int ([] Int) -> Property-    compositionProp x (Fun _ f) (Fun _ g) = traverse (Compose . fmap g . f) x === (Compose . fmap (traverse g) . traverse f $ x)--    functorProp :: t Int -> Fun Int Int -> Property-    functorProp x (Fun _ f) = fmap f x === fmapDefault f x--    foldableProp :: t Int -> Fun Int [Int] -> Property-    foldableProp x (Fun _ f) = foldMap f x === foldMapDefault f x- monadLaws :: forall (m :: * -> *). ( Monad m #if !MIN_VERSION_base(4, 8, 0)                                    , Applicative m@@ -138,9 +100,95 @@     apProp f x = (f' <*> x) === ap f' x        where f' = apply <$> f +-------------------------------------------------------------------------------+-- Lattice distributive+------------------------------------------------------------------------------- --- Orphan instances+latticeLaws+    :: forall a. (Eq a, Show a, Arbitrary a,  Lattice a, PartialOrd a)+    => String+    -> Bool -- ^ distributive+    -> Proxy a+    -> TestTree+latticeLaws name distr _ = testGroup ("Lattice laws: " <> name) $+    [ QC.testProperty "leq = joinLeq" joinLeqProp+    , QC.testProperty "leq = meetLeq" meetLeqProp+    , QC.testProperty "meet is lower bound" meetLower+    , QC.testProperty "join is upper bound" joinUpper+    , QC.testProperty "meet commutes" meetComm+    , QC.testProperty "join commute" joinComm+    , QC.testProperty "meet associative" meetAssoc+    , QC.testProperty "join associative" joinAssoc+    , QC.testProperty "absorbtion 1" meetAbsorb+    , QC.testProperty "absorbtion 2" joinAbsorb+    , QC.testProperty "meet idempontent" meetIdemp+    , QC.testProperty "join idempontent" joinIdemp+    , QC.testProperty "comparableDef" comparableDef+    ] ++ if not distr then [] else+    -- Not all lattices are distributive!+    [ QC.testProperty "x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z)" distrProp+    , QC.testProperty "x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z)" distr2Prop+    ]+  where+    joinLeqProp :: a -> a -> Property+    joinLeqProp x y = leq x y === joinLeq x y +    meetLeqProp :: a -> a -> Property+    meetLeqProp x y = leq x y === meetLeq x y++    meetLower :: a -> a -> Property+    meetLower x y = (m `leq` x) QC..&&. (m `leq` y)+      where+        m = x /\ y++    joinUpper :: a -> a -> Property+    joinUpper x y = (x `leq` j) QC..&&. (y `leq` j)+      where+        j = x \/ y++    meetComm :: a -> a -> Property+    meetComm x y = x /\ y === y /\ x++    joinComm :: a -> a -> Property+    joinComm x y = x \/ y === y \/ x++    meetAssoc :: a -> a -> a -> Property+    meetAssoc x y z = x /\ (y /\ z) === (x /\ y) /\ z++    joinAssoc :: a -> a -> a -> Property+    joinAssoc x y z = x \/ (y \/ z) === (x \/ y) \/ z++    meetAbsorb :: a -> a -> Property+    meetAbsorb x y = x /\ (x \/ y) === x++    joinAbsorb :: a -> a -> Property+    joinAbsorb x y = x \/ (x /\ y) === x++    meetIdemp :: a -> Property+    meetIdemp x = x /\ x === x++    joinIdemp :: a -> Property+    joinIdemp x = x \/ x === x++    comparableDef :: a -> a -> Property+    comparableDef x y = (leq x y || leq y x) === comparable x y++    distrProp :: a -> a -> a -> Property+    distrProp x y z = lhs === rhs+      where+        lhs = x /\ (y \/ z)+        rhs = (x /\ y) \/ (x /\ z)++    distr2Prop :: a -> a -> a -> Property+    distr2Prop x y z = lhs === rhs+      where+        lhs = x \/ (y /\ z)+        rhs = (x \/ y) /\ (x \/ z)++-------------------------------------------------------------------------------+-- Orphans+-------------------------------------------------------------------------------+ instance Arbitrary a => Arbitrary (D.Dropped a) where   arbitrary = frequency [ (1, pure D.Top)                         , (9, D.Drop <$> arbitrary)@@ -159,9 +207,143 @@  instance Arbitrary a => Arbitrary (O.Ordered a) where   arbitrary = O.Ordered <$> arbitrary+  shrink = map O.Ordered . shrink . O.getOrdered +instance (Arbitrary a, Num a, Ord a) => Arbitrary (Div.Divisibility a) where+  arbitrary = divisibility <$> arbitrary+  shrink d = filter (<d) . map divisibility . shrink . Div.getDivisibility $ d++divisibility :: (Ord a, Num a) => a -> Div.Divisibility a+divisibility x | x < (-1)  = Div.Divisibility (abs x)+               | x < 1     = Div.Divisibility 1+               | otherwise = Div.Divisibility x++ instance Arbitrary a => Arbitrary (Op.Op a) where   arbitrary = Op.Op <$> arbitrary  instance (Arbitrary k, Arbitrary v) => Arbitrary (LO.Lexicographic k v) where-  arbitrary = LO.Lexicographic <$> arbitrary <*> arbitrary+    arbitrary = uncurry LO.Lexicographic <$> arbitrary+    shrink (LO.Lexicographic k v) = uncurry LO.Lexicographic <$> shrink (k, v)++-------------------------------------------------------------------------------+-- Examples+-------------------------------------------------------------------------------++-- | Non-distributive lattice+data M3 = M3_0 | M3_a | M3_b | M3_c | M3_1+  deriving (Eq, Ord, Show, Enum, Bounded)++instance Arbitrary M3 where+    arbitrary = QC.arbitraryBoundedEnum++instance PartialOrd M3 where+    x    `leq` y    | x == y = True+    M3_0 `leq` _             = True+    _    `leq` M3_1          = True+    _    `leq` _             = False++instance JoinSemiLattice M3 where+    x    \/ M3_0          = x+    M3_0 \/ y             = y+    _    \/ M3_1          = M3_1+    M3_1 \/ _             = M3_1+    x    \/ y | x == y    = x+              | otherwise = M3_1++instance MeetSemiLattice M3 where+    x    /\ M3_1          = x+    M3_1 /\ y             = y+    _    /\ M3_0          = M3_0+    M3_0 /\ _             = M3_0+    x    /\ y | x == y    = x+              | otherwise = M3_0++instance Lattice M3 where++-- | Set Bool, M2+data M2 = M2_0 | M2_T | M2_F | M2_1+  deriving (Eq, Ord, Show, Enum, Bounded)++instance Arbitrary M2 where+    arbitrary = QC.arbitraryBoundedEnum++instance PartialOrd M2 where+    x    `leq` y   | x == y  = True+    M2_0 `leq` _             = True+    _    `leq` M2_1          = True+    _    `leq` _             = False++instance JoinSemiLattice M2 where+    x    \/ M2_0          = x+    M2_0 \/ y             = y+    _    \/ M2_1          = M2_1+    M2_1 \/ _             = M2_1+    x    \/ y | x == y    = x+              | otherwise = M2_1++instance MeetSemiLattice M2 where+    x    /\ M2_1          = x+    M2_1 /\ y             = y+    _    /\ M2_0          = M2_0+    M2_0 /\ _             = M2_0+    x    /\ y | x == y    = x+              | otherwise = M2_0++instance Lattice M2 where++instance BoundedJoinSemiLattice M2 where+    bottom = M2_0++instance BoundedMeetSemiLattice M2 where+    top = M2_1++instance BoundedLattice M2 where++-------------------------------------------------------------------------------+-- Lexicographic M2 search+-------------------------------------------------------------------------------++searchM3 :: (Eq a, PartialOrd a, Lattice a) => [a] -> Maybe (a,a,a,a,a)+searchM3 xs = listToMaybe $ do+    x0 <- xs+    xa <- xs+    guard (xa `notElem` [x0])+    guard (x0 `leq` xa)+    xb <- xs+    guard (xb `notElem` [x0,xa])+    guard (x0 `leq` xb)+    guard (not $ comparable xa xb)+    xc <- xs+    guard (xc `notElem` [x0,xa,xb])+    guard (x0 `leq` xc)+    guard (not $ comparable xa xc)+    guard (not $ comparable xb xc)+    x1 <- xs+    guard (x1 `notElem` [x0,xa,xb,xc])+    guard (x0 `leq` x1)+    guard (xa `leq` x1)+    guard (xb `leq` x1)+    guard (xc `leq` x1)++    -- homomorphism+    let f M3_0 = x1+        f M3_a = xa+        f M3_b = xb+        f M3_c = xc+        f M3_1 = x1++    ma <- [minBound .. maxBound]+    mb <- [minBound .. maxBound]+    guard (f (ma /\ mb) == f ma /\ f mb)+    guard (f (ma \/ mb) == f ma \/ f mb)++    return (x0,xa,xb,xc,x1)++type L2 = LO.Lexicographic M2 M2++searchM3LexM2 :: Maybe (L2,L2,L2,L2,L2)+searchM3LexM2 = searchM3 xs+  where+    xs = [ LO.Lexicographic x y | x <- ys, y <- ys ]+    ys = [minBound .. maxBound]