{-# LANGUAGE DeriveTraversable, GeneralizedNewtypeDeriving #-}
-- | Join semilattices, related to 'Data.Semilattice.Lower.Lower' and 'Upper'.
module Data.Semilattice.Meet
( Meet(..)
, Meeting(..)
, GreaterThan(..)
) where

import Data.HashMap.Lazy as HashMap
import Data.HashSet as HashSet
import Data.IntMap as IntMap
import Data.IntSet as IntSet
import Data.Map as Map
import Data.Semigroup
import Data.Semilattice.Upper
import Data.Set as Set

-- | A meet semilattice is an idempotent commutative semigroup.
class Meet s where
  -- | The meet operation.
  --
  --   Laws:
  --
  --   Idempotence:
  --
  -- @
  -- x '/\' x = x
  -- @
  --
  --   Associativity:
  --
  -- @
  -- a '/\' (b '/\' c) = (a '/\' b) '/\' c
  -- @
  --
  --   Commutativity:
  --
  -- @
  -- a '/\' b = b '/\' a
  -- @
  --
  --   Additionally, if @s@ has an 'Upper' bound, then 'upperBound' must be its identity:
  --
  -- @
  -- 'upperBound' '/\' a = a
  -- a '/\' 'upperBound' = a
  -- @
  --
  --   If @s@ has a 'Data.Semilattice.Lower.Lower' bound, then 'Data.Semilattice.Lower.lowerBound' must be its absorbing element:
  --
  -- @
  -- 'Data.Semilattice.Lower.lowerBound' '/\' a = 'Data.Semilattice.Lower.lowerBound'
  -- a '/\' 'Data.Semilattice.Lower.lowerBound' = 'Data.Semilattice.Lower.lowerBound'
  -- @
  (/\) :: s -> s -> s

  infixr 7 /\


-- Prelude

instance Meet () where
  _ /\ _ = ()

-- | Boolean conjunction forms a semilattice.
--
--   Idempotence:
--
--   prop> x /\ x == (x :: Bool)
--
--   Associativity:
--
--   prop> a /\ (b /\ c) == (a /\ b) /\ (c :: Bool)
--
--   Commutativity:
--
--   prop> a /\ b == b /\ (a :: Bool)
--
--   Identity:
--
--   prop> upperBound /\ a == (a :: Bool)
--
--   Absorption:
--
--   prop> lowerBound /\ a == (lowerBound :: Bool)
instance Meet Bool where
  (/\) = (&&)

-- | Orderings form a semilattice.
--
--   Idempotence:
--
--   prop> x /\ x == (x :: Ordering)
--
--   Associativity:
--
--   prop> a /\ (b /\ c) == (a /\ b) /\ (c :: Ordering)
--
--   Commutativity:
--
--   prop> a /\ b == b /\ (a :: Ordering)
--
--   Identity:
--
--   prop> upperBound /\ a == (a :: Ordering)
--
--   Absorption:
--
--   prop> lowerBound /\ a == (lowerBound :: Ordering)
instance Meet Ordering where
  LT /\ _ = LT
  _ /\ LT = LT
  GT /\ b = b
  a /\ GT = a
  _ /\ _ = EQ

-- | Functions with semilattice codomains form a semilattice.
--
--   Idempotence:
--
--   prop> \ (Fn x) -> x /\ x ~= (x :: Int -> Bool)
--
--   Associativity:
--
--   prop> \ (Fn a) (Fn b) (Fn c) -> a /\ (b /\ c) ~= (a /\ b) /\ (c :: Int -> Bool)
--
--   Commutativity:
--
--   prop> \ (Fn a) (Fn b) -> a /\ b ~= b /\ (a :: Int -> Bool)
--
--   Identity:
--
--   prop> \ (Fn a) -> upperBound /\ a ~= (a :: Int -> Bool)
--
--   Absorption:
--
--   prop> \ (Fn a) -> lowerBound /\ a ~= (lowerBound :: Int -> Bool)
instance Meet b => Meet (a -> b) where
  f /\ g = (/\) <$> f <*> g


-- Data.Semigroup

-- | The greatest lowerBound bound gives rise to a meet semilattice.
--
--   Idempotence:
--
--   prop> x /\ x == (x :: Min Int)
--
--   Associativity:
--
--   prop> a /\ (b /\ c) == (a /\ b) /\ (c :: Min Int)
--
--   Commutativity:
--
--   prop> a /\ b == b /\ (a :: Min Int)
--
--   Identity:
--
--   prop> upperBound /\ a == (a :: Min Int)
--
--   Absorption:
--
--   prop> lowerBound /\ a == (lowerBound :: Min Int)
instance Ord a => Meet (Min a) where
  (/\) = (<>)


-- containers

-- | IntMap union with 'Meet'able values forms a semilattice.
--
--   Idempotence:
--
--   prop> x /\ x == (x :: IntMap (Set Char))
--
--   Associativity:
--
--   prop> a /\ (b /\ c) == (a /\ b) /\ (c :: IntMap (Set Char))
--
--   Commutativity:
--
--   prop> a /\ b == b /\ (a :: IntMap (Set Char))
--
--   Absorption:
--
--   prop> lowerBound /\ a == (lowerBound :: IntMap (Set Char))
instance Meet a => Meet (IntMap a) where
  (/\) = IntMap.intersectionWith (/\)

-- | IntSet intersection forms a semilattice.
--
--   Idempotence:
--
--   prop> x /\ x == (x :: IntSet)
--
--   Associativity:
--
--   prop> a /\ (b /\ c) == (a /\ b) /\ (c :: IntSet)
--
--   Commutativity:
--
--   prop> a /\ b == b /\ (a :: IntSet)
--
--   Absorption:
--
--   prop> lowerBound /\ a == (lowerBound :: IntSet)
instance Meet IntSet where
  (/\) = IntSet.intersection

-- | Map union with 'Meet'able values forms a semilattice.
--
--   Idempotence:
--
--   prop> x /\ x == (x :: Map Char (Set Char))
--
--   Associativity:
--
--   prop> a /\ (b /\ c) == (a /\ b) /\ (c :: Map Char (Set Char))
--
--   Commutativity:
--
--   prop> a /\ b == b /\ (a :: Map Char (Set Char))
--
--   Absorption:
--
--   prop> lowerBound /\ a == (lowerBound :: Map Char (Set Char))
instance (Ord k, Meet a) => Meet (Map k a) where
  (/\) = Map.intersectionWith (/\)

-- | Set intersection forms a semilattice.
--
--   Idempotence:
--
--   prop> x /\ x == (x :: Set Char)
--
--   Associativity:
--
--   prop> a /\ (b /\ c) == (a /\ b) /\ (c :: Set Char)
--
--   Commutativity:
--
--   prop> a /\ b == b /\ (a :: Set Char)
--
--   Absorption:
--
--   prop> lowerBound /\ a == (lowerBound :: Set Char)
instance Ord a => Meet (Set a) where
  (/\) = Set.intersection


-- unordered-containers

-- | HashMap union with 'Meet'able values forms a semilattice.
--
--   Idempotence:
--
--   prop> x /\ x == (x :: HashMap Char (Set Char))
--
--   Associativity:
--
--   prop> a /\ (b /\ c) == (a /\ b) /\ (c :: HashMap Char (Set Char))
--
--   Commutativity:
--
--   prop> a /\ b == b /\ (a :: HashMap Char (Set Char))
--
--   Absorption:
--
--   prop> lowerBound /\ a == (lowerBound :: HashMap Char (Set Char))
instance (Eq k, Meet a) => Meet (HashMap k a) where
  (/\) = HashMap.intersectionWith (/\)

-- | HashSet intersection forms a semilattice.
--
--   Idempotence:
--
--   prop> x /\ x == (x :: HashSet Char)
--
--   Associativity:
--
--   prop> a /\ (b /\ c) == (a /\ b) /\ (c :: HashSet Char)
--
--   Commutativity:
--
--   prop> a /\ b == b /\ (a :: HashSet Char)
--
--   Absorption:
--
--   prop> lowerBound /\ a == (lowerBound :: HashSet Char)
instance Eq a => Meet (HashSet a) where
  (/\) = HashSet.intersection


-- | A 'Semigroup' for any 'Meet' semilattice.
--
--   If the semilattice has an 'Upper' bound, there is additionally a 'Monoid' instance.
newtype Meeting a = Meeting { getMeeting :: a }
  deriving (Bounded, Enum, Eq, Foldable, Functor, Meet, Num, Ord, Read, Show, Traversable, Upper)

-- | 'Meeting' '<>' is associative.
--
--   prop> Meeting a <> (Meeting b <> Meeting c) == (Meeting a <> Meeting b) <> Meeting (c :: IntSet)
instance Meet a => Semigroup (Meeting a) where
  (<>) = (/\)

-- | 'Meeting' 'mempty' is the left- and right-identity.
--
--   prop> let (l, r) = (mappend mempty (Meeting x), mappend (Meeting x) mempty) in l == Meeting x && r == Meeting (x :: Bool)
instance (Upper a, Meet a) => Monoid (Meeting a) where
  mappend = (<>)
  mempty = upperBound


-- | 'Meet' semilattices give rise to a partial 'Ord'ering.
newtype GreaterThan a = GreaterThan { getGreaterThan :: a }
  deriving (Enum, Eq, Foldable, Functor, Meet, Num, Read, Show, Traversable)

-- | NB: This is not in general a total ordering.
instance (Eq a, Meet a) => Ord (GreaterThan a) where
  compare a b
    | a == b      = EQ
    | a /\ b == a = LT
    | otherwise   = GT

  a <= b = a /\ b == a


-- $setup
-- >>> import Data.Semilattice.Lower
-- >>> import Test.QuickCheck
-- >>> import Test.QuickCheck.Function
-- >>> import Test.QuickCheck.Instances.UnorderedContainers ()
-- >>> instance Arbitrary a => Arbitrary (Min a) where arbitrary = Min <$> arbitrary
-- >>> :{
-- infix 4 ~=
-- f ~= g = (==) <$> f <*> g
-- :}