{-# LANGUAGE Safe #-}
----------------------------------------------------------------------------
-- |
-- Module      :  Algebra.PartialOrd
-- 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>
--
----------------------------------------------------------------------------
module Algebra.PartialOrd (
    -- * Partial orderings
    PartialOrd(..),
    partialOrdEq,

    -- * Fixed points of chains in partial orders
    lfpFrom, unsafeLfpFrom,
    gfpFrom, unsafeGfpFrom
  ) where

import           Data.Foldable     (Foldable (..))
import           Data.Hashable     (Hashable (..))
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.List.Compat  as L
import qualified Data.Map          as Map
import           Data.Monoid       (All (..), Any (..))
import qualified Data.Set          as Set
import           Data.Void         (Void)

-- | 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
--
-- @
-- 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
--
-- @
-- `comparable` a b ==> a ``leq`` b || b ``leq`` a
-- @
--
-- 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`,
--
-- @
-- 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

    -- | 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 a
x a
y = a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq a
x a
y Bool -> Bool -> Bool
|| a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq a
y a
x

-- | The equality relation induced by the partial-order structure. It satisfies
-- the laws of an equivalence relation:
-- @
-- Reflexive:  a == a
-- Symmetric:  a == b ==> b == a
-- Transitive: a == b && b == c ==> a == c
-- @
partialOrdEq :: PartialOrd a => a -> a -> Bool
partialOrdEq :: a -> a -> Bool
partialOrdEq a
x a
y = a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq a
x a
y Bool -> Bool -> Bool
&& a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq a
y a
x

instance PartialOrd () where
    leq :: () -> () -> Bool
leq ()
_ ()
_ = Bool
True

-- | @since 2
instance PartialOrd Bool where
    leq :: Bool -> Bool -> Bool
leq = Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
(<=)

instance PartialOrd Any where
    leq :: Any -> Any -> Bool
leq = Any -> Any -> Bool
forall a. Ord a => a -> a -> Bool
(<=)

instance PartialOrd All where
    leq :: All -> All -> Bool
leq = All -> All -> Bool
forall a. Ord a => a -> a -> Bool
(<=)

instance PartialOrd Void where
    leq :: Void -> Void -> Bool
leq Void
_ Void
_ = Bool
True

-- | @'leq' = 'Data.List.isSequenceOf'@.
instance Eq a => PartialOrd [a] where
    leq :: [a] -> [a] -> Bool
leq = [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
L.isSubsequenceOf

instance Ord a => PartialOrd (Set.Set a) where
    leq :: Set a -> Set a -> Bool
leq = Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf

instance PartialOrd IS.IntSet where
    leq :: IntSet -> IntSet -> Bool
leq = IntSet -> IntSet -> Bool
IS.isSubsetOf

instance (Eq k, Hashable k) => PartialOrd (HS.HashSet k) where
    leq :: HashSet k -> HashSet k -> Bool
leq HashSet k
a HashSet k
b = HashSet k -> Bool
forall a. HashSet a -> Bool
HS.null (HashSet k -> HashSet k -> HashSet k
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
HS.difference HashSet k
a HashSet k
b)

instance (Ord k, PartialOrd v) => PartialOrd (Map.Map k v) where
    leq :: Map k v -> Map k v -> Bool
leq = (v -> v -> Bool) -> Map k v -> Map k v -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy v -> v -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq

instance PartialOrd v => PartialOrd (IM.IntMap v) where
    leq :: IntMap v -> IntMap v -> Bool
leq = (v -> v -> Bool) -> IntMap v -> IntMap v -> Bool
forall a b. (a -> b -> Bool) -> IntMap a -> IntMap b -> Bool
IM.isSubmapOfBy v -> v -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq

instance (Eq k, Hashable k, PartialOrd v) => PartialOrd (HM.HashMap k v) where
    HashMap k v
x leq :: HashMap k v -> HashMap k v -> Bool
`leq` HashMap k v
y = {- wish: HM.isSubmapOfBy leq -}
        HashMap k v -> Bool
forall k v. HashMap k v -> Bool
HM.null (HashMap k v -> HashMap k v -> HashMap k v
forall k v w.
(Eq k, Hashable k) =>
HashMap k v -> HashMap k w -> HashMap k v
HM.difference HashMap k v
x HashMap k v
y) Bool -> Bool -> Bool
&& All -> Bool
getAll (HashMap k All -> All
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (HashMap k All -> All) -> HashMap k All -> All
forall a b. (a -> b) -> a -> b
$ (v -> v -> All) -> HashMap k v -> HashMap k v -> HashMap k All
forall k v1 v2 v3.
(Eq k, Hashable k) =>
(v1 -> v2 -> v3) -> HashMap k v1 -> HashMap k v2 -> HashMap k v3
HM.intersectionWith (\v
vx v
vy -> Bool -> All
All (v
vx v -> v -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` v
vy)) HashMap k v
x HashMap k v
y)

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
    (a
x1, b
y1) leq :: (a, b) -> (a, b) -> Bool
`leq` (a
x2, b
y2) = a
x1 a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` a
x2 Bool -> Bool -> Bool
&& b
y1 b -> b -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` b
y2

-- | Ordinal sum.
--
-- @since 2.1
instance (PartialOrd a, PartialOrd b) => PartialOrd (Either a b) where
    leq :: Either a b -> Either a b -> Bool
leq (Right b
x) (Right b
y) = b -> b -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq b
x b
y
    leq (Right b
_) Either a b
_         = Bool
False
    leq Either a b
_         (Right b
_) = Bool
True
    leq (Left a
x)  (Left a
y)  = a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq a
x a
y

    comparable :: Either a b -> Either a b -> Bool
comparable (Right b
x) (Right b
y) = b -> b -> Bool
forall a. PartialOrd a => a -> a -> Bool
comparable b
x b
y
    comparable (Right b
_) Either a b
_         = Bool
True
    comparable Either a b
_         (Right b
_) = Bool
True
    comparable (Left a
x)  (Left a
y)  = a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
comparable a
x a
y

-- | Least point of a partially ordered monotone function. Checks that the function is monotone.
lfpFrom :: PartialOrd a => a -> (a -> a) -> a
lfpFrom :: a -> (a -> a) -> a
lfpFrom = (a -> a -> Bool) -> a -> (a -> a) -> a
forall a. Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a
lfpFrom' a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq

-- | Least point of a partially ordered monotone function. Does not checks that the function is monotone.
unsafeLfpFrom :: Eq a => a -> (a -> a) -> a
unsafeLfpFrom :: a -> (a -> a) -> a
unsafeLfpFrom = (a -> a -> Bool) -> a -> (a -> a) -> a
forall a. Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a
lfpFrom' (\a
_ a
_ -> Bool
True)

{-# INLINE lfpFrom' #-}
lfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a
lfpFrom' :: (a -> a -> Bool) -> a -> (a -> a) -> a
lfpFrom' a -> a -> Bool
check a
init_x a -> a
f = a -> a
go a
init_x
  where go :: a -> a
go a
x | a
x' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x      = a
x
             | a
x a -> a -> Bool
`check` a
x' = a -> a
go a
x'
             | Bool
otherwise    = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"lfpFrom: non-monotone function"
          where x' :: a
x' = a -> a
f a
x


-- | Greatest fixed point of a partially ordered antinone function. Checks that the function is antinone.
{-# INLINE gfpFrom #-}
gfpFrom :: PartialOrd a => a -> (a -> a) -> a
gfpFrom :: a -> (a -> a) -> a
gfpFrom = (a -> a -> Bool) -> a -> (a -> a) -> a
forall a. Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a
gfpFrom' a -> a -> Bool
forall a. PartialOrd a => a -> a -> Bool
leq

-- | Greatest fixed point of a partially ordered antinone function. Does not check that the function is antinone.
{-# INLINE unsafeGfpFrom #-}
unsafeGfpFrom :: Eq a => a -> (a -> a) -> a
unsafeGfpFrom :: a -> (a -> a) -> a
unsafeGfpFrom = (a -> a -> Bool) -> a -> (a -> a) -> a
forall a. Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a
gfpFrom' (\a
_ a
_ -> Bool
True)

{-# INLINE gfpFrom' #-}
gfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a
gfpFrom' :: (a -> a -> Bool) -> a -> (a -> a) -> a
gfpFrom' a -> a -> Bool
check a
init_x a -> a
f = a -> a
go a
init_x
  where go :: a -> a
go a
x | a
x' a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x      = a
x
             | a
x' a -> a -> Bool
`check` a
x = a -> a
go a
x'
             | Bool
otherwise    = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"gfpFrom: non-antinone function"
          where x' :: a
x' = a -> a
f a
x