{-# LANGUAGE Safe #-}
----------------------------------------------------------------------------
-- |
-- Module      :  Algebra.PartialOrd
-- Copyright   :  (C) 2010-2015 Maximilian Bolingbroke
-- 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 qualified Data.IntMap as IM
import qualified Data.IntSet as IS
import qualified Data.Map    as M
import qualified Data.Set    as S
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 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 PartialOrd () where
    leq _ _ = True

instance PartialOrd Void where
    leq _ _ = True

instance Ord a => PartialOrd (S.Set a) where
    leq = S.isSubsetOf

instance PartialOrd IS.IntSet where
    leq = IS.isSubsetOf

instance (Ord k, PartialOrd v) => PartialOrd (M.Map k v) where
    leq = M.isSubmapOfBy leq

instance PartialOrd v => PartialOrd (IM.IntMap v) where
    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
lfpFrom = lfpFrom' 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 = lfpFrom' (\_ _ -> True)

{-# INLINE lfpFrom' #-}
lfpFrom' :: Eq a => (a -> a -> Bool) -> a -> (a -> a) -> a
lfpFrom' check init_x f = go init_x
  where go x | x' == x      = x
             | x `check` x' = go x'
             | otherwise    = error "lfpFrom: non-monotone function"
          where x' = f 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 = gfpFrom' 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 = gfpFrom' (\_ _ -> True)

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