{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Core.Data.Class.SOrd
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Core.Data.Class.SOrd
  ( -- * Symbolic total order relation
    SOrd (..),
    SOrd' (..),
  )
where

import Control.Monad.Except
import Control.Monad.Identity
import Control.Monad.Trans.Maybe
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.Sum
import Data.Int
import Data.Word
import GHC.TypeLits
import Generics.Deriving
import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM
import Grisette.Core.Data.BV
import Grisette.Core.Data.Class.Bool
import Grisette.Core.Data.Class.SimpleMergeable
import Grisette.Core.Data.Class.Solvable
import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.IR.SymPrim
-- >>> :set -XDataKinds
-- >>> :set -XBinaryLiterals
-- >>> :set -XFlexibleContexts
-- >>> :set -XFlexibleInstances
-- >>> :set -XFunctionalDependencies

-- | Auxiliary class for 'SOrd' instance derivation
class (SEq' f) => SOrd' f where
  -- | Auxiliary function for '(<~~) derivation
  (<~~) :: f a -> f a -> SymBool

  infix 4 <~~

  -- | Auxiliary function for '(<=~~) derivation
  (<=~~) :: f a -> f a -> SymBool

  infix 4 <=~~

  -- | Auxiliary function for '(>~~) derivation
  (>~~) :: f a -> f a -> SymBool

  infix 4 >~~

  -- | Auxiliary function for '(>=~~) derivation
  (>=~~) :: f a -> f a -> SymBool

  infix 4 >=~~

  -- | Auxiliary function for 'symCompare' derivation
  symCompare' :: f a -> f a -> UnionM Ordering

instance SOrd' U1 where
  U1 a
_ <~~ :: forall a. U1 a -> U1 a -> SymBool
<~~ U1 a
_ = forall c t. Solvable c t => c -> t
con Bool
False
  U1 a
_ <=~~ :: forall a. U1 a -> U1 a -> SymBool
<=~~ U1 a
_ = forall c t. Solvable c t => c -> t
con Bool
True
  U1 a
_ >~~ :: forall a. U1 a -> U1 a -> SymBool
>~~ U1 a
_ = forall c t. Solvable c t => c -> t
con Bool
False
  U1 a
_ >=~~ :: forall a. U1 a -> U1 a -> SymBool
>=~~ U1 a
_ = forall c t. Solvable c t => c -> t
con Bool
True
  symCompare' :: forall a. U1 a -> U1 a -> UnionM Ordering
symCompare' U1 a
_ U1 a
_ = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
EQ

instance SOrd' V1 where
  V1 a
_ <~~ :: forall a. V1 a -> V1 a -> SymBool
<~~ V1 a
_ = forall c t. Solvable c t => c -> t
con Bool
False
  V1 a
_ <=~~ :: forall a. V1 a -> V1 a -> SymBool
<=~~ V1 a
_ = forall c t. Solvable c t => c -> t
con Bool
True
  V1 a
_ >~~ :: forall a. V1 a -> V1 a -> SymBool
>~~ V1 a
_ = forall c t. Solvable c t => c -> t
con Bool
False
  V1 a
_ >=~~ :: forall a. V1 a -> V1 a -> SymBool
>=~~ V1 a
_ = forall c t. Solvable c t => c -> t
con Bool
True
  symCompare' :: forall a. V1 a -> V1 a -> UnionM Ordering
symCompare' V1 a
_ V1 a
_ = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
EQ

instance (SOrd c) => SOrd' (K1 i c) where
  (K1 c
a) <~~ :: forall a. K1 i c a -> K1 i c a -> SymBool
<~~ (K1 c
b) = c
a forall a. SOrd a => a -> a -> SymBool
<~ c
b
  (K1 c
a) <=~~ :: forall a. K1 i c a -> K1 i c a -> SymBool
<=~~ (K1 c
b) = c
a forall a. SOrd a => a -> a -> SymBool
<=~ c
b
  (K1 c
a) >~~ :: forall a. K1 i c a -> K1 i c a -> SymBool
>~~ (K1 c
b) = c
a forall a. SOrd a => a -> a -> SymBool
>~ c
b
  (K1 c
a) >=~~ :: forall a. K1 i c a -> K1 i c a -> SymBool
>=~~ (K1 c
b) = c
a forall a. SOrd a => a -> a -> SymBool
>=~ c
b
  symCompare' :: forall a. K1 i c a -> K1 i c a -> UnionM Ordering
symCompare' (K1 c
a) (K1 c
b) = forall a. SOrd a => a -> a -> UnionM Ordering
symCompare c
a c
b

instance (SOrd' a) => SOrd' (M1 i c a) where
  (M1 a a
a) <~~ :: forall a. M1 i c a a -> M1 i c a a -> SymBool
<~~ (M1 a a
b) = a a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ a a
b
  (M1 a a
a) <=~~ :: forall a. M1 i c a a -> M1 i c a a -> SymBool
<=~~ (M1 a a
b) = a a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<=~~ a a
b
  (M1 a a
a) >~~ :: forall a. M1 i c a a -> M1 i c a a -> SymBool
>~~ (M1 a a
b) = a a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ a a
b
  (M1 a a
a) >=~~ :: forall a. M1 i c a a -> M1 i c a a -> SymBool
>=~~ (M1 a a
b) = a a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>=~~ a a
b
  symCompare' :: forall a. M1 i c a a -> M1 i c a a -> UnionM Ordering
symCompare' (M1 a a
a) (M1 a a
b) = forall (f :: * -> *) a. SOrd' f => f a -> f a -> UnionM Ordering
symCompare' a a
a a a
b

instance (SOrd' a, SOrd' b) => SOrd' (a :+: b) where
  (L1 a a
_) <~~ :: forall a. (:+:) a b a -> (:+:) a b a -> SymBool
<~~ (R1 b a
_) = forall c t. Solvable c t => c -> t
con Bool
True
  (L1 a a
a) <~~ (L1 a a
b) = a a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ a a
b
  (R1 b a
_) <~~ (L1 a a
_) = forall c t. Solvable c t => c -> t
con Bool
False
  (R1 b a
a) <~~ (R1 b a
b) = b a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ b a
b
  (L1 a a
_) <=~~ :: forall a. (:+:) a b a -> (:+:) a b a -> SymBool
<=~~ (R1 b a
_) = forall c t. Solvable c t => c -> t
con Bool
True
  (L1 a a
a) <=~~ (L1 a a
b) = a a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<=~~ a a
b
  (R1 b a
_) <=~~ (L1 a a
_) = forall c t. Solvable c t => c -> t
con Bool
False
  (R1 b a
a) <=~~ (R1 b a
b) = b a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<=~~ b a
b

  (L1 a a
_) >~~ :: forall a. (:+:) a b a -> (:+:) a b a -> SymBool
>~~ (R1 b a
_) = forall c t. Solvable c t => c -> t
con Bool
False
  (L1 a a
a) >~~ (L1 a a
b) = a a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ a a
b
  (R1 b a
_) >~~ (L1 a a
_) = forall c t. Solvable c t => c -> t
con Bool
True
  (R1 b a
a) >~~ (R1 b a
b) = b a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ b a
b
  (L1 a a
_) >=~~ :: forall a. (:+:) a b a -> (:+:) a b a -> SymBool
>=~~ (R1 b a
_) = forall c t. Solvable c t => c -> t
con Bool
False
  (L1 a a
a) >=~~ (L1 a a
b) = a a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>=~~ a a
b
  (R1 b a
_) >=~~ (L1 a a
_) = forall c t. Solvable c t => c -> t
con Bool
True
  (R1 b a
a) >=~~ (R1 b a
b) = b a
a forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>=~~ b a
b

  symCompare' :: forall a. (:+:) a b a -> (:+:) a b a -> UnionM Ordering
symCompare' (L1 a a
a) (L1 a a
b) = forall (f :: * -> *) a. SOrd' f => f a -> f a -> UnionM Ordering
symCompare' a a
a a a
b
  symCompare' (L1 a a
_) (R1 b a
_) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
LT
  symCompare' (R1 b a
a) (R1 b a
b) = forall (f :: * -> *) a. SOrd' f => f a -> f a -> UnionM Ordering
symCompare' b a
a b a
b
  symCompare' (R1 b a
_) (L1 a a
_) = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
GT

instance (SOrd' a, SOrd' b) => SOrd' (a :*: b) where
  (a a
a1 :*: b a
b1) <~~ :: forall a. (:*:) a b a -> (:*:) a b a -> SymBool
<~~ (a a
a2 :*: b a
b2) = (a a
a1 forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ a a
a2) forall b. LogicalOp b => b -> b -> b
||~ ((a a
a1 forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
a2) forall b. LogicalOp b => b -> b -> b
&&~ (b a
b1 forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ b a
b2))
  (a a
a1 :*: b a
b1) <=~~ :: forall a. (:*:) a b a -> (:*:) a b a -> SymBool
<=~~ (a a
a2 :*: b a
b2) = (a a
a1 forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ a a
a2) forall b. LogicalOp b => b -> b -> b
||~ ((a a
a1 forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
a2) forall b. LogicalOp b => b -> b -> b
&&~ (b a
b1 forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<=~~ b a
b2))
  (a a
a1 :*: b a
b1) >~~ :: forall a. (:*:) a b a -> (:*:) a b a -> SymBool
>~~ (a a
a2 :*: b a
b2) = (a a
a1 forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ a a
a2) forall b. LogicalOp b => b -> b -> b
||~ ((a a
a1 forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
a2) forall b. LogicalOp b => b -> b -> b
&&~ (b a
b1 forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ b a
b2))
  (a a
a1 :*: b a
b1) >=~~ :: forall a. (:*:) a b a -> (:*:) a b a -> SymBool
>=~~ (a a
a2 :*: b a
b2) = (a a
a1 forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ a a
a2) forall b. LogicalOp b => b -> b -> b
||~ ((a a
a1 forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
a2) forall b. LogicalOp b => b -> b -> b
&&~ (b a
b1 forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>=~~ b a
b2))
  symCompare' :: forall a. (:*:) a b a -> (:*:) a b a -> UnionM Ordering
symCompare' (a a
a1 :*: b a
b1) (a a
a2 :*: b a
b2) = do
    Ordering
l <- forall (f :: * -> *) a. SOrd' f => f a -> f a -> UnionM Ordering
symCompare' a a
a1 a a
a2
    case Ordering
l of
      Ordering
EQ -> forall (f :: * -> *) a. SOrd' f => f a -> f a -> UnionM Ordering
symCompare' b a
b1 b a
b2
      Ordering
_ -> forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
l

derivedSymLt :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
derivedSymLt :: forall a. (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
derivedSymLt a
x a
y = forall a x. Generic a => a -> Rep a x
from a
x forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ forall a x. Generic a => a -> Rep a x
from a
y

derivedSymLe :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
derivedSymLe :: forall a. (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
derivedSymLe a
x a
y = forall a x. Generic a => a -> Rep a x
from a
x forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<=~~ forall a x. Generic a => a -> Rep a x
from a
y

derivedSymGt :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
derivedSymGt :: forall a. (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
derivedSymGt a
x a
y = forall a x. Generic a => a -> Rep a x
from a
x forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ forall a x. Generic a => a -> Rep a x
from a
y

derivedSymGe :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
derivedSymGe :: forall a. (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
derivedSymGe a
x a
y = forall a x. Generic a => a -> Rep a x
from a
x forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>=~~ forall a x. Generic a => a -> Rep a x
from a
y

derivedSymCompare :: (Generic a, SOrd' (Rep a)) => a -> a -> UnionM Ordering
derivedSymCompare :: forall a. (Generic a, SOrd' (Rep a)) => a -> a -> UnionM Ordering
derivedSymCompare a
x a
y = forall (f :: * -> *) a. SOrd' f => f a -> f a -> UnionM Ordering
symCompare' (forall a x. Generic a => a -> Rep a x
from a
x) (forall a x. Generic a => a -> Rep a x
from a
y)

-- | Symbolic total order. Note that we can't use Haskell's 'Ord' class since
-- symbolic comparison won't necessarily return a concrete 'Bool' or 'Ordering'
-- value.
--
-- >>> let a = 1 :: SymInteger
-- >>> let b = 2 :: SymInteger
-- >>> a <~ b
-- true
-- >>> a >~ b
-- false
--
-- >>> let a = "a" :: SymInteger
-- >>> let b = "b" :: SymInteger
-- >>> a <~ b
-- (< a b)
-- >>> a <=~ b
-- (<= a b)
-- >>> a >~ b
-- (< b a)
-- >>> a >=~ b
-- (<= b a)
--
-- For `symCompare`, `Ordering` is not a solvable type, and the result would
-- be wrapped in a union-like monad. See `Grisette.Core.Control.Monad.UnionMBase` and `UnionLike` for more
-- information.
--
-- >>> a `symCompare` b :: UnionM Ordering -- UnionM is UnionMBase specialized with SymBool
-- {If (< a b) LT (If (= a b) EQ GT)}
--
-- __Note:__ This type class can be derived for algebraic data types.
-- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.
--
-- > data X = ... deriving Generic deriving SOrd via (Default X)
class (SEq a) => SOrd a where
  (<~) :: a -> a -> SymBool
  infix 4 <~
  (<=~) :: a -> a -> SymBool
  infix 4 <=~
  (>~) :: a -> a -> SymBool
  infix 4 >~
  (>=~) :: a -> a -> SymBool
  infix 4 >=~
  a
x <~ a
y = a
x forall a. SOrd a => a -> a -> SymBool
<=~ a
y forall b. LogicalOp b => b -> b -> b
&&~ a
x forall a. SEq a => a -> a -> SymBool
/=~ a
y
  a
x >~ a
y = a
y forall a. SOrd a => a -> a -> SymBool
<~ a
x
  a
x >=~ a
y = a
y forall a. SOrd a => a -> a -> SymBool
<=~ a
x
  symCompare :: a -> a -> UnionM Ordering
  symCompare a
l a
r =
    forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
      (a
l forall a. SOrd a => a -> a -> SymBool
<~ a
r)
      (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
LT)
      (forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
l forall a. SEq a => a -> a -> SymBool
==~ a
r) (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
EQ) (forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
GT))
  {-# MINIMAL (<=~) #-}

instance (SEq a, Generic a, SOrd' (Rep a)) => SOrd (Default a) where
  (Default a
l) <=~ :: Default a -> Default a -> SymBool
<=~ (Default a
r) = a
l forall a. (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
`derivedSymLe` a
r
  (Default a
l) <~ :: Default a -> Default a -> SymBool
<~ (Default a
r) = a
l forall a. (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
`derivedSymLt` a
r
  (Default a
l) >=~ :: Default a -> Default a -> SymBool
>=~ (Default a
r) = a
l forall a. (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
`derivedSymGe` a
r
  (Default a
l) >~ :: Default a -> Default a -> SymBool
>~ (Default a
r) = a
l forall a. (Generic a, SOrd' (Rep a)) => a -> a -> SymBool
`derivedSymGt` a
r
  symCompare :: Default a -> Default a -> UnionM Ordering
symCompare (Default a
l) (Default a
r) = forall a. (Generic a, SOrd' (Rep a)) => a -> a -> UnionM Ordering
derivedSymCompare a
l a
r

#define CONCRETE_SORD(type) \
instance SOrd 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

#define CONCRETE_SORD_BV(type) \
instance (KnownNat n, 1 <= n) => SOrd (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

#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(SomeWordN)
CONCRETE_SORD(SomeIntN)
CONCRETE_SORD(B.ByteString)
CONCRETE_SORD_BV(WordN)
CONCRETE_SORD_BV(IntN)
#endif

symCompareSingleList :: (SOrd a) => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList :: forall a. SOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
isLess Bool
isStrict = [a] -> [a] -> SymBool
go
  where
    go :: [a] -> [a] -> SymBool
go [] [] = 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 forall a. SOrd a => a -> a -> SymBool
<~ a
y else a
x forall a. SOrd a => a -> a -> SymBool
>~ a
y) forall b. LogicalOp b => b -> b -> b
||~ (a
x forall a. SEq a => a -> a -> SymBool
==~ a
y forall b. LogicalOp b => b -> b -> b
&&~ [a] -> [a] -> SymBool
go [a]
xs [a]
ys)
    go [] [a]
_ = if Bool
isLess then forall c t. Solvable c t => c -> t
con Bool
True else forall c t. Solvable c t => c -> t
con Bool
False
    go [a]
_ [] = if Bool
isLess then forall c t. Solvable c t => c -> t
con Bool
False else forall c t. Solvable c t => c -> t
con Bool
True

symCompareList :: (SOrd a) => [a] -> [a] -> UnionM Ordering
symCompareList :: forall a. SOrd a => [a] -> [a] -> UnionM Ordering
symCompareList [] [] = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
EQ
symCompareList (a
x : [a]
xs) (a
y : [a]
ys) = do
  Ordering
oxy <- forall a. SOrd a => a -> a -> UnionM Ordering
symCompare a
x a
y
  case Ordering
oxy of
    Ordering
LT -> forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
LT
    Ordering
EQ -> forall a. SOrd a => [a] -> [a] -> UnionM Ordering
symCompareList [a]
xs [a]
ys
    Ordering
GT -> forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
GT
symCompareList [] [a]
_ = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
LT
symCompareList [a]
_ [] = forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
GT

instance (SOrd a) => SOrd [a] where
  <=~ :: [a] -> [a] -> SymBool
(<=~) = forall a. SOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
True Bool
False
  <~ :: [a] -> [a] -> SymBool
(<~) = forall a. SOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
True Bool
True
  >=~ :: [a] -> [a] -> SymBool
(>=~) = forall a. SOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
False Bool
False
  >~ :: [a] -> [a] -> SymBool
(>~) = forall a. SOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
False Bool
True
  symCompare :: [a] -> [a] -> UnionM Ordering
symCompare = forall a. SOrd a => [a] -> [a] -> UnionM Ordering
symCompareList

deriving via (Default (Maybe a)) instance SOrd a => SOrd (Maybe a)

deriving via (Default (Either a b)) instance (SOrd a, SOrd b) => SOrd (Either a b)

deriving via (Default ()) instance SOrd ()

deriving via (Default (a, b)) instance (SOrd a, SOrd b) => SOrd (a, b)

deriving via (Default (a, b, c)) instance (SOrd a, SOrd b, SOrd c) => SOrd (a, b, c)

deriving via
  (Default (a, b, c, d))
  instance
    (SOrd a, SOrd b, SOrd c, SOrd d) =>
    SOrd (a, b, c, d)

deriving via
  (Default (a, b, c, d, e))
  instance
    (SOrd a, SOrd b, SOrd c, SOrd d, SOrd e) =>
    SOrd (a, b, c, d, e)

deriving via
  (Default (a, b, c, d, e, f))
  instance
    (SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f) =>
    SOrd (a, b, c, d, e, f)

deriving via
  (Default (a, b, c, d, e, f, g))
  instance
    (SOrd a, SOrd b, SOrd c, SOrd d, SOrd e, SOrd f, SOrd g) =>
    SOrd (a, b, c, d, e, f, g)

deriving via
  (Default (a, b, c, d, e, f, g, h))
  instance
    ( SOrd a,
      SOrd b,
      SOrd c,
      SOrd d,
      SOrd e,
      SOrd f,
      SOrd g,
      SOrd h
    ) =>
    SOrd (a, b, c, d, e, f, g, h)

deriving via
  (Default (Sum f g a))
  instance
    (SOrd (f a), SOrd (g a)) => SOrd (Sum f g a)

instance (SOrd (m (Maybe a))) => SOrd (MaybeT m a) where
  (MaybeT m (Maybe a)
l) <=~ :: MaybeT m a -> MaybeT m a -> SymBool
<=~ (MaybeT m (Maybe a)
r) = m (Maybe a)
l forall a. SOrd a => a -> a -> SymBool
<=~ m (Maybe a)
r
  (MaybeT m (Maybe a)
l) <~ :: MaybeT m a -> MaybeT m a -> SymBool
<~ (MaybeT m (Maybe a)
r) = m (Maybe a)
l forall a. SOrd a => a -> a -> SymBool
<~ m (Maybe a)
r
  (MaybeT m (Maybe a)
l) >=~ :: MaybeT m a -> MaybeT m a -> SymBool
>=~ (MaybeT m (Maybe a)
r) = m (Maybe a)
l forall a. SOrd a => a -> a -> SymBool
>=~ m (Maybe a)
r
  (MaybeT m (Maybe a)
l) >~ :: MaybeT m a -> MaybeT m a -> SymBool
>~ (MaybeT m (Maybe a)
r) = m (Maybe a)
l forall a. SOrd a => a -> a -> SymBool
>~ m (Maybe a)
r
  symCompare :: MaybeT m a -> MaybeT m a -> UnionM Ordering
symCompare (MaybeT m (Maybe a)
l) (MaybeT m (Maybe a)
r) = forall a. SOrd a => a -> a -> UnionM Ordering
symCompare m (Maybe a)
l m (Maybe a)
r

instance (SOrd (m (Either e a))) => SOrd (ExceptT e m a) where
  (ExceptT m (Either e a)
l) <=~ :: ExceptT e m a -> ExceptT e m a -> SymBool
<=~ (ExceptT m (Either e a)
r) = m (Either e a)
l forall a. SOrd a => a -> a -> SymBool
<=~ m (Either e a)
r
  (ExceptT m (Either e a)
l) <~ :: ExceptT e m a -> ExceptT e m a -> SymBool
<~ (ExceptT m (Either e a)
r) = m (Either e a)
l forall a. SOrd a => a -> a -> SymBool
<~ m (Either e a)
r
  (ExceptT m (Either e a)
l) >=~ :: ExceptT e m a -> ExceptT e m a -> SymBool
>=~ (ExceptT m (Either e a)
r) = m (Either e a)
l forall a. SOrd a => a -> a -> SymBool
>=~ m (Either e a)
r
  (ExceptT m (Either e a)
l) >~ :: ExceptT e m a -> ExceptT e m a -> SymBool
>~ (ExceptT m (Either e a)
r) = m (Either e a)
l forall a. SOrd a => a -> a -> SymBool
>~ m (Either e a)
r
  symCompare :: ExceptT e m a -> ExceptT e m a -> UnionM Ordering
symCompare (ExceptT m (Either e a)
l) (ExceptT m (Either e a)
r) = forall a. SOrd a => a -> a -> UnionM Ordering
symCompare m (Either e a)
l m (Either e a)
r

instance (SOrd (m (a, s))) => SOrd (WriterLazy.WriterT s m a) where
  (WriterLazy.WriterT m (a, s)
l) <=~ :: WriterT s m a -> WriterT s m a -> SymBool
<=~ (WriterLazy.WriterT m (a, s)
r) = m (a, s)
l forall a. SOrd a => a -> a -> SymBool
<=~ m (a, s)
r
  (WriterLazy.WriterT m (a, s)
l) <~ :: WriterT s m a -> WriterT s m a -> SymBool
<~ (WriterLazy.WriterT m (a, s)
r) = m (a, s)
l forall a. SOrd a => a -> a -> SymBool
<~ m (a, s)
r
  (WriterLazy.WriterT m (a, s)
l) >=~ :: WriterT s m a -> WriterT s m a -> SymBool
>=~ (WriterLazy.WriterT m (a, s)
r) = m (a, s)
l forall a. SOrd a => a -> a -> SymBool
>=~ m (a, s)
r
  (WriterLazy.WriterT m (a, s)
l) >~ :: WriterT s m a -> WriterT s m a -> SymBool
>~ (WriterLazy.WriterT m (a, s)
r) = m (a, s)
l forall a. SOrd a => a -> a -> SymBool
>~ m (a, s)
r
  symCompare :: WriterT s m a -> WriterT s m a -> UnionM Ordering
symCompare (WriterLazy.WriterT m (a, s)
l) (WriterLazy.WriterT m (a, s)
r) = forall a. SOrd a => a -> a -> UnionM Ordering
symCompare m (a, s)
l m (a, s)
r

instance (SOrd (m (a, s))) => SOrd (WriterStrict.WriterT s m a) where
  (WriterStrict.WriterT m (a, s)
l) <=~ :: WriterT s m a -> WriterT s m a -> SymBool
<=~ (WriterStrict.WriterT m (a, s)
r) = m (a, s)
l forall a. SOrd a => a -> a -> SymBool
<=~ m (a, s)
r
  (WriterStrict.WriterT m (a, s)
l) <~ :: WriterT s m a -> WriterT s m a -> SymBool
<~ (WriterStrict.WriterT m (a, s)
r) = m (a, s)
l forall a. SOrd a => a -> a -> SymBool
<~ m (a, s)
r
  (WriterStrict.WriterT m (a, s)
l) >=~ :: WriterT s m a -> WriterT s m a -> SymBool
>=~ (WriterStrict.WriterT m (a, s)
r) = m (a, s)
l forall a. SOrd a => a -> a -> SymBool
>=~ m (a, s)
r
  (WriterStrict.WriterT m (a, s)
l) >~ :: WriterT s m a -> WriterT s m a -> SymBool
>~ (WriterStrict.WriterT m (a, s)
r) = m (a, s)
l forall a. SOrd a => a -> a -> SymBool
>~ m (a, s)
r
  symCompare :: WriterT s m a -> WriterT s m a -> UnionM Ordering
symCompare (WriterStrict.WriterT m (a, s)
l) (WriterStrict.WriterT m (a, s)
r) = forall a. SOrd a => a -> a -> UnionM Ordering
symCompare m (a, s)
l m (a, s)
r

instance (SOrd a) => SOrd (Identity a) where
  (Identity a
l) <=~ :: Identity a -> Identity a -> SymBool
<=~ (Identity a
r) = a
l forall a. SOrd a => a -> a -> SymBool
<=~ a
r
  (Identity a
l) <~ :: Identity a -> Identity a -> SymBool
<~ (Identity a
r) = a
l forall a. SOrd a => a -> a -> SymBool
<~ a
r
  (Identity a
l) >=~ :: Identity a -> Identity a -> SymBool
>=~ (Identity a
r) = a
l forall a. SOrd a => a -> a -> SymBool
>=~ a
r
  (Identity a
l) >~ :: Identity a -> Identity a -> SymBool
>~ (Identity a
r) = a
l forall a. SOrd a => a -> a -> SymBool
>~ a
r
  (Identity a
l) symCompare :: Identity a -> Identity a -> UnionM Ordering
`symCompare` (Identity a
r) = a
l forall a. SOrd a => a -> a -> UnionM Ordering
`symCompare` a
r

instance (SOrd (m a)) => SOrd (IdentityT m a) where
  (IdentityT m a
l) <=~ :: IdentityT m a -> IdentityT m a -> SymBool
<=~ (IdentityT m a
r) = m a
l forall a. SOrd a => a -> a -> SymBool
<=~ m a
r
  (IdentityT m a
l) <~ :: IdentityT m a -> IdentityT m a -> SymBool
<~ (IdentityT m a
r) = m a
l forall a. SOrd a => a -> a -> SymBool
<~ m a
r
  (IdentityT m a
l) >=~ :: IdentityT m a -> IdentityT m a -> SymBool
>=~ (IdentityT m a
r) = m a
l forall a. SOrd a => a -> a -> SymBool
>=~ m a
r
  (IdentityT m a
l) >~ :: IdentityT m a -> IdentityT m a -> SymBool
>~ (IdentityT m a
r) = m a
l forall a. SOrd a => a -> a -> SymBool
>~ m a
r
  (IdentityT m a
l) symCompare :: IdentityT m a -> IdentityT m a -> UnionM Ordering
`symCompare` (IdentityT m a
r) = m a
l forall a. SOrd a => a -> a -> UnionM Ordering
`symCompare` m a
r