{-# LANGUAGE CPP                   #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE Safe                  #-}
{-# LANGUAGE TypeOperators         #-}
#if __GLASGOW_HASKELL__ >= 810
{-# LANGUAGE StandaloneKindSignatures #-}
#endif
module Data.OrdP (
    OrdP (..),
) where

import Control.Applicative  (Const (..))
import Data.Kind            (Type)
import Data.Proxy           (Proxy (..))
import Data.Semigroup       ((<>))
import Data.Type.Equality   ((:~:) (..), (:~~:) (..))
import GHC.Generics         ((:*:) (..), (:+:) (..))

#if MIN_VERSION_base(4,18,0)
import Data.Functor.Product (Product (..))
import Data.Functor.Sum (Sum (..))
import qualified GHC.TypeLits as TL
import qualified GHC.TypeNats as TN
#endif

#if !MIN_VERSION_base(4,19,0)
import Data.Orphans ()
#endif

import qualified Type.Reflection as TR

#if __GLASGOW_HASKELL__ >= 810
import Data.Kind (Constraint)
#endif

import Data.EqP

-- | Heterogenous lifted total order.
--
-- This class is stronger version of 'Ord1' from @base@
--
-- @
-- class (forall a. Ord a => Ord (f a)) => Ord1 f where
--     liftCompare :: (a -> b -> Ordering) -> f a -> f b -> Ordering
-- @
--
-- @since 1.0.5
#if __GLASGOW_HASKELL__ >= 810
type OrdP :: (k -> Type) -> Constraint
#endif
class (EqP f, forall a. Ord (f a)) => OrdP (f :: k -> Type) where
    comparep :: f a -> f b -> Ordering

instance OrdP ((:~:) a) where
    comparep :: forall (a :: k) (b :: k). (a :~: a) -> (a :~: b) -> Ordering
comparep a :~: a
_ a :~: b
_ = Ordering
EQ

instance OrdP ((:~~:) a) where
    comparep :: forall (a :: k) (b :: k). (a :~~: a) -> (a :~~: b) -> Ordering
comparep a :~~: a
_ a :~~: b
_ = Ordering
EQ

#if MIN_VERSION_base(4,18,0)
instance (OrdP a, OrdP b) => OrdP (Sum a b) where
    comparep :: forall (a :: k) (b :: k). Sum a b a -> Sum a b b -> Ordering
comparep (InL a a
x) (InL a b
y) = a a -> a b -> Ordering
forall (a :: k) (b :: k). a a -> a b -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
OrdP f =>
f a -> f b -> Ordering
comparep a a
x a b
y
    comparep (InL a a
_) (InR b b
_) = Ordering
LT
    comparep (InR b a
x) (InR b b
y) = b a -> b b -> Ordering
forall (a :: k) (b :: k). b a -> b b -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
OrdP f =>
f a -> f b -> Ordering
comparep b a
x b b
y
    comparep (InR b a
_) (InL a b
_) = Ordering
GT

instance (OrdP a, OrdP b) => OrdP (Product a b) where
    comparep :: forall (a :: k) (b :: k).
Product a b a -> Product a b b -> Ordering
comparep (Pair a a
x b a
y) (Pair a b
x' b b
y') = a a -> a b -> Ordering
forall (a :: k) (b :: k). a a -> a b -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
OrdP f =>
f a -> f b -> Ordering
comparep a a
x a b
x' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> b a -> b b -> Ordering
forall (a :: k) (b :: k). b a -> b b -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
OrdP f =>
f a -> f b -> Ordering
comparep b a
y b b
y'
#endif

instance (OrdP f, OrdP g) => OrdP (f :+: g) where
    comparep :: forall (a :: k) (b :: k). (:+:) f g a -> (:+:) f g b -> Ordering
comparep (L1 f a
x) (L1 f b
y) = f a -> f b -> Ordering
forall (a :: k) (b :: k). f a -> f b -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
OrdP f =>
f a -> f b -> Ordering
comparep f a
x f b
y
    comparep (L1 f a
_) (R1 g b
_) = Ordering
LT
    comparep (R1 g a
x) (R1 g b
y) = g a -> g b -> Ordering
forall (a :: k) (b :: k). g a -> g b -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
OrdP f =>
f a -> f b -> Ordering
comparep g a
x g b
y
    comparep (R1 g a
_) (L1 f b
_) = Ordering
GT

instance (OrdP a, OrdP b) => OrdP (a :*: b) where
    comparep :: forall (a :: k) (b :: k). (:*:) a b a -> (:*:) a b b -> Ordering
comparep (a a
x :*: b a
y) (a b
x' :*: b b
y') = a a -> a b -> Ordering
forall (a :: k) (b :: k). a a -> a b -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
OrdP f =>
f a -> f b -> Ordering
comparep a a
x a b
x' Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> b a -> b b -> Ordering
forall (a :: k) (b :: k). b a -> b b -> Ordering
forall k (f :: k -> *) (a :: k) (b :: k).
OrdP f =>
f a -> f b -> Ordering
comparep b a
y b b
y'

instance OrdP TR.TypeRep where
    comparep :: forall (a :: k) (b :: k). TypeRep a -> TypeRep b -> Ordering
comparep TypeRep a
x TypeRep b
y = SomeTypeRep -> SomeTypeRep -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (TypeRep a -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
TR.SomeTypeRep TypeRep a
x) (TypeRep b -> SomeTypeRep
forall k (a :: k). TypeRep a -> SomeTypeRep
TR.SomeTypeRep TypeRep b
y)

#if MIN_VERSION_base(4,18,0)
instance OrdP TL.SChar where
    comparep :: forall (a :: Char) (b :: Char). SChar a -> SChar b -> Ordering
comparep SChar a
x SChar b
y = Char -> Char -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SChar a -> Char
forall (c :: Char). SChar c -> Char
TL.fromSChar SChar a
x) (SChar b -> Char
forall (c :: Char). SChar c -> Char
TL.fromSChar SChar b
y)

instance OrdP TL.SSymbol where
    comparep :: forall (a :: Symbol) (b :: Symbol).
SSymbol a -> SSymbol b -> Ordering
comparep SSymbol a
x SSymbol b
y = String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SSymbol a -> String
forall (s :: Symbol). SSymbol s -> String
TL.fromSSymbol SSymbol a
x) (SSymbol b -> String
forall (s :: Symbol). SSymbol s -> String
TL.fromSSymbol SSymbol b
y)

instance OrdP TN.SNat where
    comparep :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Ordering
comparep SNat a
x SNat b
y = Nat -> Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (SNat a -> Nat
forall (n :: Nat). SNat n -> Nat
TN.fromSNat SNat a
x) (SNat b -> Nat
forall (n :: Nat). SNat n -> Nat
TN.fromSNat SNat b
y)
#endif

instance OrdP Proxy where
    comparep :: forall (a :: k) (b :: k). Proxy a -> Proxy b -> Ordering
comparep Proxy a
_ Proxy b
_ = Ordering
EQ

instance Ord a => OrdP (Const a) where
    comparep :: forall (a :: k) (b :: k). Const a a -> Const a b -> Ordering
comparep (Const a
x) (Const a
y) = a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare a
x a
y