{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd () where

import Control.Monad.Except (ExceptT)
import Control.Monad.Identity
  ( Identity,
    IdentityT (IdentityT),
  )
import Control.Monad.Trans.Maybe (MaybeT)
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import qualified Data.ByteString as B
import Data.Functor.Compose (Compose (Compose))
import Data.Functor.Const (Const)
import Data.Functor.Product (Product)
import Data.Functor.Sum (Sum)
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Monoid (Alt, Ap)
import qualified Data.Monoid as Monoid
import Data.Ord (Down (Down))
import Data.Proxy (Proxy)
import Data.Ratio (Ratio, denominator, numerator)
import qualified Data.Text as T
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeLits (KnownNat, type (<=))
import Generics.Deriving
  ( Default (Default),
    Default1 (Default1),
    K1 (K1),
    M1 (M1),
    Par1 (Par1),
    Rec1 (Rec1),
    U1,
    V1,
    (:.:) (Comp1),
    type (:*:),
    type (:+:),
  )
import Grisette.Internal.Core.Control.Exception
  ( AssertionError,
    VerificationConditions,
  )
import Grisette.Internal.Core.Control.Monad.Union (Union)
import Grisette.Internal.Core.Data.Class.LogicalOp
  ( LogicalOp (symNot, (.&&), (.||)),
  )
import Grisette.Internal.Core.Data.Class.PlainUnion
  ( simpleMerge,
  )
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( mrgIf,
  )
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Core.Data.Class.SymEq
  ( SymEq ((.==)),
  )
import Grisette.Internal.Core.Data.Class.TryMerge
  ( mrgSingle,
    tryMerge,
  )
import Grisette.Internal.Internal.Decl.Core.Data.Class.SymOrd
  ( SymOrd (symCompare, (.<), (.<=), (.>), (.>=)),
    SymOrd1 (liftSymCompare),
    SymOrd2,
    symCompare1,
  )
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, NotRepresentableFPError, ValidFP)
import Grisette.Internal.SymPrim.Prim.Term
  ( PEvalOrdTerm
      ( pevalLeOrdTerm,
        pevalLtOrdTerm
      ),
    pevalGeOrdTerm,
    pevalGtOrdTerm,
  )
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN (SymIntN),
    SymWordN (SymWordN),
  )
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymFP
  ( SymFP (SymFP),
    SymFPRoundingMode (SymFPRoundingMode),
  )
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
import Grisette.Internal.TH.Derivation.Derive (derive)

#define CONCRETE_SORD(type) \
instance SymOrd type where \
  l .<= r = con $ l <= r; \
  l .< r = con $ l < r; \
  l .>= r = con $ l >= r; \
  l .> r = con $ l > r; \
  symCompare l r = mrgSingle $ compare l r; \
  {-# INLINE (.<=) #-}; \
  {-# INLINE (.<) #-}; \
  {-# INLINE (.>=) #-}; \
  {-# INLINE (.>) #-}; \
  {-# INLINE symCompare #-}

#define CONCRETE_SORD_BV(type) \
instance (KnownNat n, 1 <= n) => SymOrd (type n) where \
  l .<= r = con $ l <= r; \
  l .< r = con $ l < r; \
  l .>= r = con $ l >= r; \
  l .> r = con $ l > r; \
  symCompare l r = mrgSingle $ compare l r; \
  {-# INLINE (.<=) #-}; \
  {-# INLINE (.<) #-}; \
  {-# INLINE (.>=) #-}; \
  {-# INLINE (.>) #-}; \
  {-# INLINE symCompare #-}

#if 1
CONCRETE_SORD(Bool)
CONCRETE_SORD(Integer)
CONCRETE_SORD(Char)
CONCRETE_SORD(Int)
CONCRETE_SORD(Int8)
CONCRETE_SORD(Int16)
CONCRETE_SORD(Int32)
CONCRETE_SORD(Int64)
CONCRETE_SORD(Word)
CONCRETE_SORD(Word8)
CONCRETE_SORD(Word16)
CONCRETE_SORD(Word32)
CONCRETE_SORD(Word64)
CONCRETE_SORD(Float)
CONCRETE_SORD(Double)
CONCRETE_SORD(B.ByteString)
CONCRETE_SORD(T.Text)
CONCRETE_SORD(FPRoundingMode)
CONCRETE_SORD(Monoid.All)
CONCRETE_SORD(Monoid.Any)
CONCRETE_SORD(Ordering)
CONCRETE_SORD_BV(WordN)
CONCRETE_SORD_BV(IntN)
CONCRETE_SORD(AlgReal)
#endif

instance SymOrd (Proxy a) where
  Proxy a
_ .<= :: Proxy a -> Proxy a -> SymBool
.<= Proxy a
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  {-# INLINE (.<=) #-}
  Proxy a
_ .< :: Proxy a -> Proxy a -> SymBool
.< Proxy a
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  {-# INLINE (.<) #-}
  Proxy a
_ .>= :: Proxy a -> Proxy a -> SymBool
.>= Proxy a
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  {-# INLINE (.>=) #-}
  Proxy a
_ .> :: Proxy a -> Proxy a -> SymBool
.> Proxy a
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  {-# INLINE (.>) #-}
  symCompare :: Proxy a -> Proxy a -> Union Ordering
symCompare Proxy a
_ Proxy a
_ = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ
  {-# INLINE symCompare #-}

instance SymOrd1 Proxy where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering) -> Proxy a -> Proxy b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
_ Proxy a
_ Proxy b
_ = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ
  {-# INLINE liftSymCompare #-}

instance (SymOrd a, Integral a) => SymOrd (Ratio a) where
  Ratio a
a .<= :: Ratio a -> Ratio a -> SymBool
.<= Ratio a
b = Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
a a -> a -> a
forall a. Num a => a -> a -> a
* Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
b a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.<= Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
b a -> a -> a
forall a. Num a => a -> a -> a
* Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
a
  {-# INLINE (.<=) #-}
  Ratio a
a .< :: Ratio a -> Ratio a -> SymBool
.< Ratio a
b = Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
a a -> a -> a
forall a. Num a => a -> a -> a
* Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
b a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
b a -> a -> a
forall a. Num a => a -> a -> a
* Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
a
  {-# INLINE (.<) #-}

instance (ValidFP eb sb) => SymOrd (FP eb sb) where
  FP eb sb
l .<= :: FP eb sb -> FP eb sb -> SymBool
.<= FP eb sb
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FP eb sb
l FP eb sb -> FP eb sb -> Bool
forall a. Ord a => a -> a -> Bool
<= FP eb sb
r
  {-# INLINE (.<=) #-}
  FP eb sb
l .< :: FP eb sb -> FP eb sb -> SymBool
.< FP eb sb
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FP eb sb
l FP eb sb -> FP eb sb -> Bool
forall a. Ord a => a -> a -> Bool
< FP eb sb
r
  {-# INLINE (.<) #-}
  FP eb sb
l .>= :: FP eb sb -> FP eb sb -> SymBool
.>= FP eb sb
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FP eb sb
l FP eb sb -> FP eb sb -> Bool
forall a. Ord a => a -> a -> Bool
>= FP eb sb
r
  {-# INLINE (.>=) #-}
  FP eb sb
l .> :: FP eb sb -> FP eb sb -> SymBool
.> FP eb sb
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ FP eb sb
l FP eb sb -> FP eb sb -> Bool
forall a. Ord a => a -> a -> Bool
> FP eb sb
r
  {-# INLINE (.>) #-}

-- SymOrd
#define SORD_SIMPLE(symtype) \
instance SymOrd symtype where \
  (symtype a) .<= (symtype b) = SymBool $ pevalLeOrdTerm a b; \
  (symtype a) .< (symtype b) = SymBool $ pevalLtOrdTerm a b; \
  (symtype a) .>= (symtype b) = SymBool $ pevalGeOrdTerm a b; \
  (symtype a) .> (symtype b) = SymBool $ pevalGtOrdTerm a b; \
  a `symCompare` b = mrgIf \
    (a .< b) \
    (mrgSingle LT) \
    (mrgIf (a .== b) (mrgSingle EQ) (mrgSingle GT)); \
  {-# INLINE (.<=) #-}; \
  {-# INLINE (.<) #-}; \
  {-# INLINE (.>=) #-}; \
  {-# INLINE (.>) #-}; \
  {-# INLINE symCompare #-}

#define SORD_BV(symtype) \
instance (KnownNat n, 1 <= n) => SymOrd (symtype n) where \
  (symtype a) .<= (symtype b) = SymBool $ pevalLeOrdTerm a b; \
  (symtype a) .< (symtype b) = SymBool $ pevalLtOrdTerm a b; \
  (symtype a) .>= (symtype b) = SymBool $ pevalGeOrdTerm a b; \
  (symtype a) .> (symtype b) = SymBool $ pevalGtOrdTerm a b; \
  a `symCompare` b = mrgIf \
    (a .< b) \
    (mrgSingle LT) \
    (mrgIf (a .== b) (mrgSingle EQ) (mrgSingle GT)); \
  {-# INLINE (.<=) #-}; \
  {-# INLINE (.<) #-}; \
  {-# INLINE (.>=) #-}; \
  {-# INLINE (.>) #-}; \
  {-# INLINE symCompare #-}

instance (ValidFP eb sb) => SymOrd (SymFP eb sb) where
  (SymFP Term (FP eb sb)
a) .<= :: SymFP eb sb -> SymFP eb sb -> SymBool
.<= (SymFP Term (FP eb sb)
b) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLeOrdTerm Term (FP eb sb)
a Term (FP eb sb)
b
  {-# INLINE (.<=) #-}
  (SymFP Term (FP eb sb)
a) .< :: SymFP eb sb -> SymFP eb sb -> SymBool
.< (SymFP Term (FP eb sb)
b) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLtOrdTerm Term (FP eb sb)
a Term (FP eb sb)
b
  {-# INLINE (.<) #-}
  (SymFP Term (FP eb sb)
a) .>= :: SymFP eb sb -> SymFP eb sb -> SymBool
.>= (SymFP Term (FP eb sb)
b) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalGeOrdTerm Term (FP eb sb)
a Term (FP eb sb)
b
  {-# INLINE (.>=) #-}
  (SymFP Term (FP eb sb)
a) .> :: SymFP eb sb -> SymFP eb sb -> SymBool
.> (SymFP Term (FP eb sb)
b) = Term Bool -> SymBool
SymBool (Term Bool -> SymBool) -> Term Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ Term (FP eb sb) -> Term (FP eb sb) -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalGtOrdTerm Term (FP eb sb)
a Term (FP eb sb)
b
  {-# INLINE (.>) #-}

instance SymOrd SymBool where
  SymBool
l .<= :: SymBool -> SymBool -> SymBool
.<= SymBool
r = SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
l SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| SymBool
r
  {-# INLINE (.<=) #-}
  SymBool
l .< :: SymBool -> SymBool -> SymBool
.< SymBool
r = SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
l SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
r
  {-# INLINE (.<) #-}
  SymBool
l .>= :: SymBool -> SymBool -> SymBool
.>= SymBool
r = SymBool
l SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
r
  {-# INLINE (.>=) #-}
  SymBool
l .> :: SymBool -> SymBool -> SymBool
.> SymBool
r = SymBool
l SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
r
  {-# INLINE (.>) #-}
  symCompare :: SymBool -> SymBool -> Union Ordering
symCompare SymBool
l SymBool
r =
    SymBool -> Union Ordering -> Union Ordering -> Union Ordering
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
      (SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot SymBool
l SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymBool
r)
      (Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT)
      (SymBool -> Union Ordering -> Union Ordering -> Union Ordering
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymBool
l SymBool -> SymBool -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== SymBool
r) (Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ) (Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
GT))
  {-# INLINE symCompare #-}

#if 1
SORD_SIMPLE(SymInteger)
SORD_SIMPLE(SymAlgReal)
SORD_SIMPLE(SymFPRoundingMode)
SORD_BV(SymIntN)
SORD_BV(SymWordN)
#endif

-- Union
instance (SymOrd a) => SymOrd (Union a) where
  Union a
x .<= :: Union a -> Union a -> SymBool
.<= Union a
y = Union SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union SymBool -> SymBool) -> Union SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ do
    x1 <- Union a
x
    y1 <- y
    mrgSingle $ x1 .<= y1
  Union a
x .< :: Union a -> Union a -> SymBool
.< Union a
y = Union SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union SymBool -> SymBool) -> Union SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ do
    x1 <- Union a
x
    y1 <- y
    mrgSingle $ x1 .< y1
  Union a
x .>= :: Union a -> Union a -> SymBool
.>= Union a
y = Union SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union SymBool -> SymBool) -> Union SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ do
    x1 <- Union a
x
    y1 <- y
    mrgSingle $ x1 .>= y1
  Union a
x .> :: Union a -> Union a -> SymBool
.> Union a
y = Union SymBool -> SymBool
forall (u :: * -> *) a.
(SimpleMergeable a, PlainUnion u) =>
u a -> a
simpleMerge (Union SymBool -> SymBool) -> Union SymBool -> SymBool
forall a b. (a -> b) -> a -> b
$ do
    x1 <- Union a
x
    y1 <- y
    mrgSingle $ x1 .> y1
  Union a
x symCompare :: Union a -> Union a -> Union Ordering
`symCompare` Union a
y = Union Ordering -> Union Ordering
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union Ordering -> Union Ordering)
-> Union Ordering -> Union Ordering
forall a b. (a -> b) -> a -> b
$ do
    x1 <- Union a
x
    y1 <- y
    x1 `symCompare` y1

instance SymOrd1 Union where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering) -> Union a -> Union b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
f Union a
x Union b
y = Union Ordering -> Union Ordering
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (Union Ordering -> Union Ordering)
-> Union Ordering -> Union Ordering
forall a b. (a -> b) -> a -> b
$ do
    x1 <- Union a
x
    y1 <- y
    f x1 y1

derive
  [ ''(),
    ''AssertionError,
    ''VerificationConditions,
    ''NotRepresentableFPError
  ]
  [''SymOrd]

derive
  [ ''Either,
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,)
  ]
  [''SymOrd, ''SymOrd1, ''SymOrd2]

derive
  [ ''Maybe,
    ''Identity,
    ''Monoid.Dual,
    ''Monoid.First,
    ''Monoid.Last,
    ''Monoid.Sum,
    ''Monoid.Product,
    ''ExceptT,
    ''MaybeT,
    ''WriterLazy.WriterT,
    ''WriterStrict.WriterT
  ]
  [''SymOrd, ''SymOrd1]

symCompareSingleList :: (SymOrd a) => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList :: forall a. SymOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
isLess Bool
isStrict = [a] -> [a] -> SymBool
go
  where
    go :: [a] -> [a] -> SymBool
go [] [] = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> Bool
not Bool
isStrict)
    go (a
x : [a]
xs) (a
y : [a]
ys) =
      (if Bool
isLess then a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< a
y else a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.> a
y) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| (a
x a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
y SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& [a] -> [a] -> SymBool
go [a]
xs [a]
ys)
    go [] [a]
_ = if Bool
isLess then Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True else Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
    go [a]
_ [] = if Bool
isLess then Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False else Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True

symLiftCompareList ::
  (a -> b -> Union Ordering) -> [a] -> [b] -> Union Ordering
symLiftCompareList :: forall a b.
(a -> b -> Union Ordering) -> [a] -> [b] -> Union Ordering
symLiftCompareList a -> b -> Union Ordering
_ [] [] = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ
symLiftCompareList a -> b -> Union Ordering
f (a
x : [a]
xs) (b
y : [b]
ys) = do
  oxy <- a -> b -> Union Ordering
f a
x b
y
  case oxy of
    Ordering
LT -> Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT
    Ordering
EQ -> (a -> b -> Union Ordering) -> [a] -> [b] -> Union Ordering
forall a b.
(a -> b -> Union Ordering) -> [a] -> [b] -> Union Ordering
symLiftCompareList a -> b -> Union Ordering
f [a]
xs [b]
ys
    Ordering
GT -> Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
GT
symLiftCompareList a -> b -> Union Ordering
_ [] [b]
_ = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT
symLiftCompareList a -> b -> Union Ordering
_ [a]
_ [] = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
GT

-- []
instance (SymOrd a) => SymOrd [a] where
  {-# INLINE (.<=) #-}
  {-# INLINE (.<) #-}
  {-# INLINE symCompare #-}
  {-# INLINE (.>=) #-}
  {-# INLINE (.>) #-}
  .<= :: [a] -> [a] -> SymBool
(.<=) = Bool -> Bool -> [a] -> [a] -> SymBool
forall a. SymOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
True Bool
False
  .< :: [a] -> [a] -> SymBool
(.<) = Bool -> Bool -> [a] -> [a] -> SymBool
forall a. SymOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
True Bool
True
  .>= :: [a] -> [a] -> SymBool
(.>=) = Bool -> Bool -> [a] -> [a] -> SymBool
forall a. SymOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
False Bool
False
  .> :: [a] -> [a] -> SymBool
(.>) = Bool -> Bool -> [a] -> [a] -> SymBool
forall a. SymOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
False Bool
True
  symCompare :: [a] -> [a] -> Union Ordering
symCompare = (a -> a -> Union Ordering) -> [a] -> [a] -> Union Ordering
forall a b.
(a -> b -> Union Ordering) -> [a] -> [b] -> Union Ordering
symLiftCompareList a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare

instance SymOrd1 [] where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering) -> [a] -> [b] -> Union Ordering
liftSymCompare = (a -> b -> Union Ordering) -> [a] -> [b] -> Union Ordering
forall a b.
(a -> b -> Union Ordering) -> [a] -> [b] -> Union Ordering
symLiftCompareList
  {-# INLINE liftSymCompare #-}

-- IdentityT
instance (SymOrd1 m, SymOrd a) => SymOrd (IdentityT m a) where
  symCompare :: IdentityT m a -> IdentityT m a -> Union Ordering
symCompare = IdentityT m a -> IdentityT m a -> Union Ordering
forall (f :: * -> *) a.
(SymOrd1 f, SymOrd a) =>
f a -> f a -> Union Ordering
symCompare1
  {-# INLINE symCompare #-}

instance (SymOrd1 m) => SymOrd1 (IdentityT m) where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering)
-> IdentityT m a -> IdentityT m b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
f (IdentityT m a
l) (IdentityT m b
r) = (a -> b -> Union Ordering) -> m a -> m b -> Union Ordering
forall a b.
(a -> b -> Union Ordering) -> m a -> m b -> Union Ordering
forall (f :: * -> *) a b.
SymOrd1 f =>
(a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
f m a
l m b
r
  {-# INLINE liftSymCompare #-}

-- Product
deriving via
  (Default (Product l r a))
  instance
    (SymOrd (l a), SymOrd (r a)) => SymOrd (Product l r a)

deriving via
  (Default1 (Product l r))
  instance
    (SymOrd1 l, SymOrd1 r) => SymOrd1 (Product l r)

-- Sum
deriving via
  (Default (Sum l r a))
  instance
    (SymOrd (l a), SymOrd (r a)) => SymOrd (Sum l r a)

deriving via
  (Default1 (Sum l r))
  instance
    (SymOrd1 l, SymOrd1 r) => SymOrd1 (Sum l r)

-- Compose
deriving via
  (Default (Compose f g a))
  instance
    (SymOrd (f (g a))) => SymOrd (Compose f g a)

instance (SymOrd1 f, SymOrd1 g) => SymOrd1 (Compose f g) where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering)
-> Compose f g a -> Compose f g b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
f (Compose f (g a)
l) (Compose f (g b)
r) =
    (g a -> g b -> Union Ordering)
-> f (g a) -> f (g b) -> Union Ordering
forall a b.
(a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
forall (f :: * -> *) a b.
SymOrd1 f =>
(a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
liftSymCompare ((a -> b -> Union Ordering) -> g a -> g b -> Union Ordering
forall a b.
(a -> b -> Union Ordering) -> g a -> g b -> Union Ordering
forall (f :: * -> *) a b.
SymOrd1 f =>
(a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
f) f (g a)
l f (g b)
r

-- Const
deriving via (Default (Const a b)) instance (SymOrd a) => SymOrd (Const a b)

deriving via (Default1 (Const a)) instance (SymOrd a) => SymOrd1 (Const a)

-- Alt
deriving via (Default (Alt f a)) instance (SymOrd (f a)) => SymOrd (Alt f a)

deriving via (Default1 (Alt f)) instance (SymOrd1 f) => SymOrd1 (Alt f)

-- Ap
deriving via (Default (Ap f a)) instance (SymOrd (f a)) => SymOrd (Ap f a)

deriving via (Default1 (Ap f)) instance (SymOrd1 f) => SymOrd1 (Ap f)

-- Generic
deriving via (Default (U1 p)) instance SymOrd (U1 p)

deriving via (Default (V1 p)) instance SymOrd (V1 p)

deriving via
  (Default (K1 i c p))
  instance
    (SymOrd c) => SymOrd (K1 i c p)

deriving via
  (Default (M1 i c f p))
  instance
    (SymOrd (f p)) => SymOrd (M1 i c f p)

deriving via
  (Default ((f :+: g) p))
  instance
    (SymOrd (f p), SymOrd (g p)) => SymOrd ((f :+: g) p)

deriving via
  (Default ((f :*: g) p))
  instance
    (SymOrd (f p), SymOrd (g p)) => SymOrd ((f :*: g) p)

deriving via
  (Default (Par1 p))
  instance
    (SymOrd p) => SymOrd (Par1 p)

deriving via
  (Default (Rec1 f p))
  instance
    (SymOrd (f p)) => SymOrd (Rec1 f p)

deriving via
  (Default ((f :.: g) p))
  instance
    (SymOrd (f (g p))) => SymOrd ((f :.: g) p)

-- Down
instance (SymOrd a) => SymOrd (Down a) where
  symCompare :: Down a -> Down a -> Union Ordering
symCompare = Down a -> Down a -> Union Ordering
forall (f :: * -> *) a.
(SymOrd1 f, SymOrd a) =>
f a -> f a -> Union Ordering
symCompare1
  {-# INLINE symCompare #-}

instance SymOrd1 Down where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering) -> Down a -> Down b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
comp (Down a
l) (Down b
r) = do
    res <- a -> b -> Union Ordering
comp a
l b
r
    case res of
      Ordering
LT -> Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
GT
      Ordering
EQ -> Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ
      Ordering
GT -> Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT
  {-# INLINE liftSymCompare #-}