-- {-# LANGUAGE ConstrainedClassMethods #-}
{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE DeriveDataTypeable  #-}
{-# LANGUAGE DeriveFoldable      #-}
{-# LANGUAGE DeriveFunctor       #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DeriveTraversable   #-}
{-# LANGUAGE FlexibleContexts    #-}
module Data.Prd (
module Data.Prd
, Down(..)
) where

import Control.Applicative
import Data.Data (Data, Typeable)
import Data.Function
import Data.Int as Int (Int, Int8, Int16, Int32, Int64)
import Data.List.NonEmpty (NonEmpty(..))
import Data.Maybe
import Data.Monoid hiding (First, Last)
import Data.Ord (Down(..))
import Data.Ratio
import Data.Word (Word, Word8, Word16, Word32, Word64)
import GHC.Generics (Generic, Generic1)
import GHC.Real
import Numeric.Natural

import qualified Data.Semigroup as S
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import qualified Data.IntSet as IntSet
import qualified Data.Sequence as Seq

infix 4 <~, >~, /~, ~~, =~, ?~, pgt, pge, peq, pne, ple, plt

infix 4 lt, gt, le, ge, eq, ne, pmax, pmin

-- | A partial order on the set /a/.
--
-- A poset relation '<~' must satisfy the following three partial order axioms:
--
-- $$\forall x: x \leq x$$ (reflexivity)
--
-- $$\forall a, b: (a \leq b) \Leftrightarrow \neg (b \leq a)$$ (anti-symmetry)
--
-- $$\forall a, b, c: ((a \leq b) \wedge (b \leq c)) \Rightarrow (a \leq c)$$ (transitivity)
--
-- If a prior equality relation is available, then a valid @Prd a@ instance may be derived from a semiorder relation 'lt' as:
--
-- @
-- x '<~' y = 'lt' x y '||' x '==' y
-- @
--
-- If /a/ is derived from a semiorder then the definition of 'lt' must satisfy
-- the three semiorder axioms:
--
-- $$\forall x, y: x \lt y \Rightarrow \neg y \lt x$$ (asymmetry)
--
-- $$\forall x, y, z, w: x \lt y \wedge y \sim z \wedge z \lt w \Rightarrow x \lt w$$ (2-2 chain)
--
-- $$\forall x, y, z, w: x \lt y \wedge y \lt z \wedge y \sim w \Rightarrow \neg (x \sim w \wedge z \sim w)$$ (3-1 chain)
--
-- The poset axioms on '<~' then follow from the first & second axioms on 'lt',
-- however the converse is not true. While the first semiorder axiom on 'lt' follows, the second
-- and third semiorder axioms forbid partial orders of four items forming two disjoint chains:
--
-- * the second axiom forbids two chains of two items each (the (2+2) free poset)
-- * the third axiom forbids a three-item chain with one unrelated item
--
-- and <https://en.wikipedia.org/wiki/Semiorder semiorder>.
--
class Prd a where
{-# MINIMAL (<~) | (>~) #-}

-- | Non-strict partial order relation on /a/.
--
-- '<~' is reflexive, anti-symmetric, and transitive.
--
(<~) :: a -> a -> Bool
(<~) = flip (>~)

-- | Converse non-strict partial order relation on /a/.
--
-- '>~' is reflexive, anti-symmetric, and transitive.
--
(>~) :: a -> a -> Bool
(>~) = flip (<~)

-- | Equivalence relation on /a/.
--
-- '=~' is reflexive, symmetric, and transitive.
--
-- @ x =~ y = maybe False (== EQ) (pcomparePrd x y)
--
-- If /a/ implements 'Eq' then (ideally) @x =~ y = x == y@.
--
(=~) :: Prd a => a -> a -> Bool
x =~ y = x <~ y && x >~ y

-- | Comparability relation on /a/.
--
-- '?~' is reflexive, symmetric, and transitive.
--
-- @ x ?~ y = maybe False (const True) (pcomparePrd x y) @
--
-- If /a/ implements 'Ord' then (ideally) @x ?~ y = True@.
--
(?~) :: Prd a => a -> a -> Bool
x ?~ y = x <~ y || x >~ y

-- | Partial version of 'Data.Ord.compare'.
--
pcompare :: Eq a => a -> a -> Maybe Ordering
pcompare x y
| x lt y  = Just LT
| x  ==  y  = Just EQ
| x gt y  = Just GT
| otherwise = Nothing

-- | Similarity relation on /a/.
--
-- '~~' is reflexive and symmetric, but not necessarily transitive.
--
-- Note this is only equivalent to '==' in a total (i.e. linear) order.
--
(~~) :: Eq a => Prd a => a -> a -> Bool
x ~~ y = not (x lt y) && not (x gt y)

-- | Negation of '~~'.
--
(/~) :: Eq a => Prd a => a -> a -> Bool
x /~ y = not $x ~~ y -- | Version of 'pcompare' that uses the derived equivalence relation. -- -- This can be useful if there is no 'Eq' instance or if it is -- compromised, for example when /a/ is a floating point number. -- pcomparePrd :: Prd a => a -> a -> Maybe Ordering pcomparePrd x y | x <~ y = Just$ if y <~ x then EQ else LT
| y <~ x = Just GT
| otherwise = Nothing

-- | Version of 'pcompare' that uses 'compare'.
--
pcompareOrd :: Ord a => a -> a -> Maybe Ordering
pcompareOrd x y = Just $x compare y -- | Prefix version of '=~'. -- -- @ eq x y = maybe False (== EQ) (pcomparePrd x y) -- eq :: Prd a => a -> a -> Bool x eq y = x <~ y && x >~ y -- | Negation of 'eq'. -- -- @ ne x y = maybe False (/= EQ) (pcomparePrd x y) -- ne :: Prd a => a -> a -> Bool x ne y = not$ x eq y

-- | Prefix version of '<~'.
--
-- @ le x y = maybe False (<= EQ) (pcomparePrd x y)
--
le :: Prd a => a -> a -> Bool
x le y = x <~ y

-- | Prefix version of '>~'.
--
-- @ ge x y = maybe False (>= EQ) (pcomparePrd x y)
--
ge :: Prd a => a -> a -> Bool
x ge y = x >~ y

-- | Strict partial order relation on /a/.
--
-- 'lt' is irreflexive, asymmetric, and transitive.
--
-- @ lt x y = maybe False (< EQ) (pcompare x y) @
--
-- If /a/ implements 'Ord' then (ideally) @x lt y = x < y@.
--
lt :: Eq a => Prd a => a -> a -> Bool
x lt y | x /= x || y /= y = False -- guard on lawless 0/0 cases
| otherwise        = x <~ y && x /= y

-- | Converse strict partial order relation on /a/.
--
-- 'gt' is irreflexive, asymmetric, and transitive.
--
-- @ gt x y = maybe False (> EQ) (pcompare x y) @
--
-- If /a/ implements 'Ord' then (ideally) @x gt y = x > y@.
--
gt :: Eq a => Prd a => a -> a -> Bool
x gt y | x /= x || y /= y = False
| otherwise        = x >~ y && x /= y

-- | A partial version of ('=~')
--
-- Returns 'Nothing' instead of 'False' when the two values are not comparable.
--
peq  :: Eq a => Prd a => a -> a -> Maybe Bool
peq x y = case x pcompare y of
Just EQ -> Just True
Just _  -> Just False
Nothing -> Nothing

-- | A partial version of ('/~')
--
-- Returns 'Nothing' instead of 'False' when the two values are not comparable.
--
pne :: Eq a => Prd a => a -> a -> Maybe Bool
pne x y = case x pcompare y of
Just EQ -> Just False
Just _  -> Just True
Nothing -> Nothing

-- | A partial version of ('<~')
--
-- Returns 'Nothing' instead of 'False' when the two values are not comparable.
--
ple :: Eq a => Prd a => a -> a -> Maybe Bool
ple x y = case x pcompare y of
Just GT -> Just False
Just _  -> Just True
Nothing -> Nothing

-- | A partial version of ('>~')
--
-- Returns 'Nothing' instead of 'False' when the two values are not comparable.
--
pge :: Eq a => Prd a => a -> a -> Maybe Bool
pge x y = case x pcompare y of
Just LT -> Just False
Just _  -> Just True
Nothing -> Nothing

-- | A partial version of ('<')
--
-- Returns 'Nothing' instead of 'False' when the two values are not comparable.
--
-- @lt x y == maybe False id $plt x y@ -- plt :: Eq a => Prd a => a -> a -> Maybe Bool plt x y = case x pcompare y of Just LT -> Just True Just _ -> Just False Nothing -> Nothing -- | A partial version of ('>') -- -- Returns 'Nothing' instead of 'False' when the two values are not comparable. -- -- @gt x y == maybe False id$ pgt x y@
--
pgt :: Eq a => Prd a => a -> a -> Maybe Bool
pgt x y = case x pcompare y of
Just GT -> Just True
Just _  -> Just False
Nothing -> Nothing

-- | A partial version of 'Data.Ord.max'.
--
-- Default instance returns the connr argument in the case of equality.
--
pmax :: Eq a => Prd a => a -> a -> Maybe a
pmax x y = do
o <- pcompare x y
case o of
GT -> Just x
EQ -> Just y
LT -> Just y

pjoin :: Eq a => Min a => Foldable f => f a -> Maybe a
pjoin = foldM pmax minimal

-- | A partial version of 'Data.Ord.min'.
--
-- Default instance returns the connr argument in the case of equality.
--
pmin :: Eq a => Prd a => a -> a -> Maybe a
pmin x y = do
o <- pcompare x y
case o of
GT -> Just y
EQ -> Just x
LT -> Just x

pmeet :: Eq a => Max a => Foldable f => f a -> Maybe a
pmeet = foldM pmin maximal

sign :: Eq a => Num a => Prd a => a -> Maybe Ordering
sign x = pcompare x 0

zero :: Eq a => Num a => Prd a => a -> Bool
zero x = sign x == Just EQ

positive :: Eq a => Num a => Prd a => a -> Bool
positive x = sign x == Just GT

negative :: Eq a => Num a => Prd a => a -> Bool
negative x = sign x == Just LT

indeterminate :: Eq a => Num a => Prd a => a -> Bool
indeterminate x = sign x == Nothing

---------------------------------------------------------------------
--  Instances
---------------------------------------------------------------------

instance Prd Bool where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Char where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Integer where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Int where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Int8 where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Int16 where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Int32 where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Int64 where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Natural where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Word where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Word8 where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Word16 where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Word32 where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Word64 where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd Ordering where
(<~) = (<=)
pcompare = pcompareOrd

instance Prd a => Prd [a] where
{-# SPECIALISE instance Prd [Char] #-}
[] <~ _     = True
(_:_) <~ [] = False
(x:xs) <~ (y:ys) = x <~ y && xs <~ ys

{-
pcompare []     []     = Just EQ
pcompare []     (_:_)  = Just LT
pcompare (_:_)  []     = Just GT
pcompare (x:xs) (y:ys) = case pcompare x y of
Just EQ -> pcompare xs ys
other   -> other
-}

instance Prd a => Prd (NonEmpty a) where
(x :| xs) <~ (y :| ys) = x <~ y && xs <~ ys

instance Prd a => Prd (Down a) where
x <~ y = y <~ x

-- Canonically ordered.
instance Prd a => Prd (Dual a) where
x <~ y = y <~ x

instance Prd Any where
Any x <~ Any y = x <~ y

instance Prd All where
All x <~ All y = y <~ x

{-

-- | 'First a' forms a pre-dioid for any semigroup @a@.
instance (Eq a, Semigroup a) => Prd (S.First a) where
(<~) = (==)

instance Ord a => Prd (S.Max a) where
pcompare (S.Max x) (S.Max y) = Just $compare x y instance Ord a => Prd (S.Min a) where pcompare (S.Min x) (S.Min y) = Just$ compare y x

-}

instance Prd Float where
x <~ y | x /= x && y /= y = True
| x /= x || y /= y = False
| otherwise        = x <= y
{-
pcompare x y | x /= x && y /= y = Just EQ
| x /= x || y /= y = Nothing
| otherwise        = pcompareOrd x y

x eq y | x /= x && y /= y = True
| x /= x || y /= y = False
| otherwise = x == y

x lt y | x /= x || y /= y = False
| otherwise = shift 2 x P.< y
-}

instance Prd Double where
x <~ y | x /= x && y /= y = True
| x /= x || y /= y = False
| otherwise        = x <= y

instance  (Prd a, Integral a)  => Prd (Ratio a)  where
{-# SPECIALIZE instance Prd Rational #-}
(x:%y) <~ (x':%y') | (x eq 0 && y eq 0) || (x' eq 0 && y' eq 0) = False
| otherwise = x * y' <~ x' * y

-- Canonical semigroup ordering
instance Prd a => Prd (Maybe a) where
Just a <~ Just b = a <~ b
x@Just{} <~ Nothing = False
Nothing <~ _ = True

-- Canonical semigroup ordering
instance (Prd a, Prd b) => Prd (Either a b) where
Right a <~ Right b  = a <~ b
Right _ <~ _        = False

Left e <~ Left f   = e <~ f
Left _ <~ _        = True

instance Prd () where
pcompare _ _ = Just EQ
_ <~ _ = True

-- Canonical semigroup ordering
instance (Prd a, Prd b) => Prd (a, b) where
(a,b) <~ (i,j) = a <~ i && b <~ j

instance (Prd a, Prd b, Prd c) => Prd (a, b, c) where
(a,b,c) <~ (i,j,k) = a <~ i && b <~ j && c <~ k

instance (Prd a, Prd b, Prd c, Prd d) => Prd (a, b, c, d) where
(a,b,c,d) <~ (i,j,k,l) = a <~ i && b <~ j && c <~ k && d <~ l

instance (Prd a, Prd b, Prd c, Prd d, Prd e) => Prd (a, b, c, d, e) where
(a,b,c,d,e) <~ (i,j,k,l,m) = a <~ i && b <~ j && c <~ k && d <~ l && e <~ m

instance Ord a => Prd (Set.Set a) where
(<~) = Set.isSubsetOf

instance (Ord k, Prd a) => Prd (Map.Map k a) where
(<~) = Map.isSubmapOfBy (<~)

instance Prd a => Prd (IntMap.IntMap a) where
(<~) = IntMap.isSubmapOfBy (<~)

instance Prd IntSet.IntSet where
(<~) = IntSet.isSubsetOf

-- Helper type for 'DerivingVia'
newtype Ordered a = Ordered { getOrdered :: a }
deriving ( Eq, Ord, Show, Data, Typeable, Generic, Generic1, Functor, Foldable, Traversable)

instance Ord a => Prd (Ordered a) where
(<~) = (<=)

type Bound a = (Min a, Max a)

-- | Min element of a partially ordered set.
--
-- $$\forall x: x \ge minimal$$
--
-- This means that 'minimal' must be comparable to all values in /a/.
--
class Prd a => Min a where
minimal :: a

instance Min () where minimal = ()

instance Min Natural where minimal = 0

instance Min Bool where minimal = minBound

instance Min Ordering where minimal = minBound

instance Min Int where minimal = minBound

instance Min Int8 where minimal = minBound

instance Min Int16 where minimal = minBound

instance Min Int32 where minimal = minBound

instance Min Int64 where minimal = minBound

instance Min Word where minimal = minBound

instance Min Word8 where minimal = minBound

instance Min Word16 where minimal = minBound

instance Min Word32 where minimal = minBound

instance Min Word64 where minimal = minBound

instance Prd a => Min (IntMap.IntMap a) where
minimal = IntMap.empty

instance Ord a => Min (Set.Set a) where
minimal = Set.empty

instance (Ord k, Prd a) => Min (Map.Map k a) where
minimal = Map.empty

instance (Min a, Min b) => Min (a, b) where
minimal = (minimal, minimal)

instance (Min a, Prd b) => Min (Either a b) where
minimal = Left minimal

instance Prd a => Min (Maybe a) where
minimal = Nothing

instance Max a => Min (Down a) where
minimal = Down maximal

-- | Max element of a partially ordered set.
--
-- $$\forall x: x \le maximal$$
--
-- This means that 'maximal' must be comparable to all values in /a/.
--
class Prd a => Max a where
maximal :: a

instance Max () where maximal = ()

instance Max Bool where maximal = maxBound

instance Max Ordering where maximal = maxBound

instance Max Int where maximal = maxBound

instance Max Int8 where maximal = maxBound

instance Max Int16 where maximal = maxBound

instance Max Int32 where maximal = maxBound

instance Max Int64 where maximal = maxBound

instance Max Word where maximal = maxBound

instance Max Word8 where maximal = maxBound

instance Max Word16 where maximal = maxBound

instance Max Word32 where maximal = maxBound

instance Max Word64 where maximal = maxBound

instance (Max a, Max b) => Max (a, b) where
maximal = (maximal, maximal)

instance (Prd a, Max b) => Max (Either a b) where
maximal = Right maximal

instance Max a => Max (Maybe a) where
maximal = Just maximal

instance Min a => Max (Down a) where
maximal = Down minimal

{-
instance (Universe a, Prd a) => Prd (k -> a) where

instance Min a => Min (k -> a) where
minimal = const minimal

instance Max a => Max (k -> a) where
maximal = const maximal
-}

{-# INLINE until #-}
until :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a
until pred rel f seed = go seed
where go x | x' rel x = x
| pred x = x
| otherwise = go x'
where x' = f x

{-# INLINE while #-}
while :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a
while pred rel f seed = go seed
where go x | x' rel x = x
| not (pred x') = x
| otherwise = go x'
where x' = f x

{-
while' :: (a -> Bool) -> (a -> a -> Bool) -> (a -> a) -> a -> a
while' pred rel f seed = go seed f
where go x | x' rel x = id
| not (pred x') = id
| otherwise = go x' . f
where x' = f x
-}

-- | Greatest (resp. least) fixed point of a monitone (resp. antitone) function.
--
-- Does not check that the function is monitone (resp. antitone).
--