{-# LANGUAGE Safe                       #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DerivingVia                #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE TypeFamilies               #-}

module Data.Prd (
    type PartialOrd
  -- * Preorders
  , Prd(..)
  , pcompareEq
  , pcompareOrd
  , pcompareRat
  -- * Re-exports
  , Ord((<=), (>=), max, min, compare)
  , Down(..)
) where

import safe Control.Applicative
import safe Data.Bool hiding (not)
import safe Data.Either
import safe Data.Functor.Apply
import safe Data.Functor.Identity
import safe Data.Int
import safe Data.List.NonEmpty
import safe Data.Maybe
import safe Data.Ord hiding ((<),(>))
import safe Data.Semigroup
import safe Data.Universe.Class (Finite(..))
import safe Data.Word
import safe GHC.Real
import safe Numeric.Natural
import safe Prelude hiding (Ord(..),Bounded)
import safe qualified Data.IntMap as IntMap
import safe qualified Data.IntSet as IntSet
import safe qualified Data.Map as Map
import safe qualified Data.Set as Set

-- | A <https://en.wikipedia.org/wiki/Partially_ordered_set partial order> on /a/.
--
type PartialOrd a = (Prd a, Eq a)

-- | A < https://en.wikipedia.org/wiki/Preorder preorder > on /a/.
--
-- A preorder relation '<~' must satisfy the following two axioms:
--
-- \( \forall x: x \leq x \) (reflexivity)
-- 
-- \( \forall a, b, c: ((a \leq b) \wedge (b \leq c)) \Rightarrow (a \leq c) \) (transitivity)
--
-- If additionally we have:
--
-- \( \forall a, b: (a \leq b) \Leftrightarrow \neg (b \leq a) \) (anti-symmetry)
--
-- then /a/ is a partial order and we may define an 'Eq' instance such that the following holds:
--
-- @
-- x '~~' y = x '==' y
-- x '<~' y = x '<' y '||' x '==' y
-- @
--
class Prd a where
    {-# MINIMAL (<~) | pcompare #-}

    infix 4 <~, >~, <, >, ?~, ~~, /~, `pcompare`, `pmax`, `pmin`

    -- | Non-strict partial order relation on /a/.
    --
    -- '<~' is reflexive, anti-symmetric, and transitive.
    --
    -- > x <~ y = x < y || x ~~ y
    -- > x <~ y = maybe False (<~ EQ) (pcompare x y)
    --
    -- for all /x/, /y/ in /a/.
    --
    (<~) :: a -> a -> Bool
    x <~ y = maybe False (<~ EQ) (pcompare x y)

    -- | Converse non-strict partial order relation on /a/.
    --
    -- '>~' is reflexive, anti-symmetric, and transitive.
    --
    -- > x >~ y = x > y || x ~~ y
    -- > x >~ y = maybe False (>~ EQ) (pcompare x y)
    --
    -- for all /x/, /y/ in /a/.
    --
    (>~) :: a -> a -> Bool
    (>~) = flip (<~)

    -- | Strict partial order relation on /a/.
    --
    -- '<' is irreflexive, asymmetric, and transitive.
    --
    -- > x < y = x <~ y && not (y <~ x)
    -- > x < y = maybe False (< EQ) (pcompare x y)
    --
    -- When '<~' is antisymmetric then /a/ is a partial 
    -- order and we have:
    -- 
    -- > x > y = x >~ y && x /~ y
    --
    -- for all /x/, /y/ in /a/.
    --
    (<) :: a -> a -> Bool
    x < y = x <~ y && not (y <~ x)

    -- | Converse strict partial order relation on /a/.
    --
    -- '>' is irreflexive, asymmetric, and transitive.
    --
    -- > x > y = x >~ y && not (y >~ x)
    -- > x > y = maybe False (> EQ) (pcompare x y)
    -- 
    -- When '<~' is antisymmetric then /a/ is a partial 
    -- order and we have:
    -- 
    -- > x > y = x >~ y && x /~ y
    --
    -- for all /x/, /y/ in /a/.
    --
    (>) :: a -> a -> Bool
    x > y = x >~ y && not (y >~ x)

    -- | Comparability relation on /a/. 
    --
    -- '?~' is reflexive, symmetric, and transitive.
    --
    -- If /a/ implements 'Ord' then we should have @x ?~ y = True@.
    --
    (?~) :: a -> a -> Bool
    x ?~ y = x <~ y || x >~ y

    -- | Equivalence relation on /a/.
    --
    -- '~~' is reflexive, symmetric, and transitive.
    --
    -- > x ~~ y = x <~ y && y <~ x
    -- > x ~~ y = maybe False (~~ EQ) (pcompare x y)
    --
    -- Use this as a lawful substitute for '==' when comparing
    -- floats, doubles, or rationals.
    --
    -- If /a/ implements 'Eq' then we should have @('~~') = ('==')@.
    --
    (~~) :: a -> a -> Bool
    (~~) x y = x <~ y && y <~ x

    -- | Negation of '~~'.
    --
    (/~) :: a -> a -> Bool
    x /~ y = not $ x ~~ y

    -- | A partial version of 'Data.Ord.max'. 
    --
    -- Returns the left-hand argument in the case of equality.
    --
    pmax :: a -> a -> Maybe a
    pmax x y = do
      o <- pcompare x y
      case o of
        GT -> Just x
        EQ -> Just x
        LT -> Just y

    -- | A partial version of 'Data.Ord.min'. 
    --
    -- Returns the left-hand argument in the case of equality.
    --
    pmin :: a -> a -> Maybe a
    pmin x y = do
      o <- pcompare x y
      case o of
        GT -> Just y
        EQ -> Just x
        LT -> Just x

    -- | Similarity relation on /a/. 
    --
    -- 'similar' is reflexive and symmetric, but not necessarily transitive.
    --
    -- Note this is only equivalent to '==' in a total (i.e. linear) order:
    --
    -- > similar (0/0 :: Float) 5 = True
    --
    -- If /a/ implements 'Ord' then we should have @('~~') = 'similar' = ('==')@.
    --
    similar :: a -> a -> Bool
    similar x y = not (x < y) && not (x > y)

    -- | A partial version of 'Data.Ord.compare'.
    --
    -- > x <  y = maybe False (<  EQ) (pcompare x y)
    -- > x >  y = maybe False (>  EQ) (pcompare x y)
    -- > x <~ y = maybe False (<~ EQ) (pcompare x y)
    -- > x >~ y = maybe False (>~ EQ) (pcompare x y)
    -- > x ~~ y = maybe False (~~ EQ) (pcompare x y)
    -- > x ?~ y = maybe False (const True) (pcompare x y)
    -- 
    -- If /a/ implements 'Ord' then we should have @'pcompare' x y = 'Just' '$' 'compare' x y@.
    --
    pcompare :: a -> a -> Maybe Ordering
    pcompare x y
      | x <~ y    = Just $ if y <~ x then EQ else LT
      | y <~ x    = Just GT
      | otherwise = Nothing

-- | Version of 'pcompare' that uses a semiorder relation and '=='.
--
-- See <https://en.wikipedia.org/wiki/Semiorder>.
--
pcompareEq :: Eq a => (a -> a -> Bool) -> a -> a -> Maybe Ordering
pcompareEq lt x y
  | lt x y = Just LT
  | x == y = Just EQ
  | 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

---------------------------------------------------------------------
-- DerivingVia
---------------------------------------------------------------------

newtype Total a = Total { getTotal :: a } deriving stock (Eq, Ord, Show, Functor)
  deriving Applicative via Identity

instance Ord a => Prd (Total a) where
  x <~ y = getTotal $ liftA2 (<=) x y
  x >~ y = getTotal $ liftA2 (>=) x y
  pcompare x y = Just . getTotal $ liftA2 compare x y

deriving via (Total ()) instance Prd ()
deriving via (Total Bool) instance Prd Bool
deriving via (Total Ordering) instance Prd Ordering
deriving via (Total Char) instance Prd Char
deriving via (Total Word) instance Prd Word
deriving via (Total Word8) instance Prd Word8
deriving via (Total Word16) instance Prd Word16
deriving via (Total Word32) instance Prd Word32
deriving via (Total Word64) instance Prd Word64
deriving via (Total Natural) instance Prd Natural
deriving via (Total Int) instance Prd Int
deriving via (Total Int8) instance Prd Int8
deriving via (Total Int16) instance Prd Int16
deriving via (Total Int32) instance Prd Int32
deriving via (Total Int64) instance Prd Int64
deriving via (Total Integer) instance Prd Integer

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

{-




instance Prd Float where
    x <= y | x /= x && y /= y = True
           | x /= x || y /= y = False
           | otherwise        = x P.<= y

    x =~ y | x /= x && y /= y = True
           | x /= x || y /= y = False
           | otherwise        = x == y
    
    x ?~ y | x /= x && y /= y = True
           | x /= x || y /= y = False
           | otherwise        = True

    pcompare x y | x /= x && y /= y = Just EQ 
                 | x /= x || y /= y = Nothing
                 | otherwise        = pcompareOrd x y

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

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

    x ?~ y | x /= x && y /= y = True
           | x /= x || y /= y = False
           | otherwise        = True

    pcompare x y | x /= x && y /= y = Just EQ 
                 | x /= x || y /= y = Nothing
                 | otherwise        = pcompareOrd x y


-}

-- N5 lattice ordering: NInf <= NaN <= PInf
n5 :: (Ord a, Fractional a) => a -> a -> Bool
n5 x y | x /= x && y /= y = True
       | x /= x = y == 1/0
       | y /= y = x == -1/0
       | otherwise = x <= y

instance Prd Float where
  (<~) = n5

instance Prd Double where
  (<~) = n5

-- N5 lattice comparison
{-
pinf = 1 :% 0
ninf = (-1) :% 0
anan = 0 :% 0

λ> pcompareRat anan pinf
Just LT
λ> pcompareRat pinf anan
Just GT
λ> pcompareRat anan anan
Just EQ
λ> pcompareRat anan (3 :% 5)
Nothing
-}
pcompareRat :: Ratio Integer -> Ratio Integer -> Maybe Ordering
pcompareRat (0:%0) (x:%0) = Just $ compare 0 x
pcompareRat (x:%0) (0:%0) = Just $ compare x 0
pcompareRat (x:%0) (y:%0) = Just $ compare (signum x) (signum y)
pcompareRat (0:%0) _ = Nothing
pcompareRat _ (0:%0) = Nothing
pcompareRat _ (x:%0) = Just $ compare 0 x -- guard against div-by-zero exceptions
pcompareRat (x:%0) _ = Just $ compare x 0
pcompareRat x y = Just $ compare x y

-- N5 lattice comparison
pcomparePos :: Ratio Natural -> Ratio Natural -> Maybe Ordering
pcomparePos (0:%0) (x:%0) = Just $ compare 0 x
pcomparePos (x:%0) (0:%0) = Just $ compare x 0
pcomparePos (_:%0) (_:%0) = Just EQ -- all non-nan infs are equal
pcomparePos (0:%0) (0:%_) = Just $ GT
pcomparePos (0:%_) (0:%0) = Just $ LT
pcomparePos (0:%0) _ = Nothing
pcomparePos _ (0:%0) = Nothing
pcomparePos (x:%y) (x':%y') = Just $ compare (x*y') (x'*y)

{-
-- N5 lattice comparison
pcomparePos (0:%0) (x:%0) = Just $ compare 0 x
pcomparePos (x:%0) (0:%0) = Just $ compare x 0
pcomparePos (_:%0) (_:%0) = Just EQ
pcomparePos (0:%0) _ = Nothing
pcomparePos _ (0:%0) = Nothing
pcomparePos (x:%y) (x':%y') = Just $ compare (x*y') (x'*y)
-}

instance Prd (Ratio Integer) where
  pcompare = pcompareRat

instance Prd (Ratio Natural) where
  pcompare = pcomparePos

{-
instance Prd (Ratio Integer) where
    pcompare (x:%y) (x':%y') | (x == 0 && y == 0) && (x' == 0 && y' == 0) = Just EQ
                             | (x == 0 && y == 0) || (x' == 0 && y' == 0) = Nothing
                             | y == 0 && y' == 0 = Just $ compare (signum x) (signum x')
                             | y == 0 = pcompareOrd x 0
                             | y' == 0 = pcompareOrd 0 x'
                             | otherwise = pcompareOrd (x%y) (x'%y')

instance Prd (Ratio Natural) where
    pcompare (x:%y) (x':%y') | (x == 0 && y == 0) && (x' == 0 && y' == 0) = Just EQ
                             | (x == 0 && y == 0) || (x' == 0 && y' == 0) = Nothing
                             | y == 0 && y' == 0 = Just EQ
                             | y == 0 = Just GT
                             | y' == 0 = Just LT
                             | otherwise = pcompareOrd (x*y') (x'*y)
-}

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

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

instance Prd a => Prd (Max a) where
  Max a <~ Max b = a <~ b

instance Prd a => Prd (Min a) where
  Min a <~ Min b = a <~ b

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

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

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

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

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

  Left a <~ Left b   = a <~ b
  Left _ <~ _        = 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

-- check semimodules paper
instance (Finite a, Prd b) => Prd (a -> b) where
  pcompare f g = mconcat [f x `pcompare` g x | x <- universeF]

instance (Finite a, Prd a) => Prd (Endo a) where
  pcompare (Endo f) (Endo g) = pcompare f g