{-# LANGUAGE CPP #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# 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 Generics.Deriving
import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM
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
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  U1 a
_ <=~~ :: forall a. U1 a -> U1 a -> SymBool
<=~~ U1 a
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  U1 a
_ >~~ :: forall a. U1 a -> U1 a -> SymBool
>~~ U1 a
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  U1 a
_ >=~~ :: forall a. U1 a -> U1 a -> SymBool
>=~~ U1 a
_ = Bool -> SymBool
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
_ = Ordering -> UnionM Ordering
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
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  V1 a
_ <=~~ :: forall a. V1 a -> V1 a -> SymBool
<=~~ V1 a
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  V1 a
_ >~~ :: forall a. V1 a -> V1 a -> SymBool
>~~ V1 a
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  V1 a
_ >=~~ :: forall a. V1 a -> V1 a -> SymBool
>=~~ V1 a
_ = Bool -> SymBool
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
_ = Ordering -> UnionM Ordering
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 c -> c -> SymBool
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 c -> c -> SymBool
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 c -> c -> SymBool
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 c -> c -> SymBool
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) = c -> c -> UnionM Ordering
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 a a -> a a -> SymBool
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 a a -> a a -> SymBool
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 a a -> a a -> SymBool
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 a a -> a a -> SymBool
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) = a a -> a a -> UnionM Ordering
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
_) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  (L1 a a
a) <~~ (L1 a a
b) = a a
a a a -> a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ a a
b
  (R1 b a
_) <~~ (L1 a a
_) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  (R1 b a
a) <~~ (R1 b a
b) = b a
a b a -> b a -> SymBool
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
_) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  (L1 a a
a) <=~~ (L1 a a
b) = a a
a a a -> a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<=~~ a a
b
  (R1 b a
_) <=~~ (L1 a a
_) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  (R1 b a
a) <=~~ (R1 b a
b) = b a
a b a -> b a -> SymBool
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
_) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  (L1 a a
a) >~~ (L1 a a
b) = a a
a a a -> a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ a a
b
  (R1 b a
_) >~~ (L1 a a
_) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  (R1 b a
a) >~~ (R1 b a
b) = b a
a b a -> b a -> SymBool
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
_) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  (L1 a a
a) >=~~ (L1 a a
b) = a a
a a a -> a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>=~~ a a
b
  (R1 b a
_) >=~~ (L1 a a
_) = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  (R1 b a
a) >=~~ (R1 b a
b) = b a
a b a -> b a -> SymBool
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) = a a -> a a -> UnionM Ordering
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
_) = Ordering -> UnionM Ordering
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
LT
  symCompare' (R1 b a
a) (R1 b a
b) = b a -> b a -> UnionM Ordering
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
_) = Ordering -> UnionM Ordering
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 a a -> a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ a a
a2) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
||~ ((a a
a1 a a -> a a -> SymBool
forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
a2) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ (b a
b1 b a -> b a -> SymBool
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 a a -> a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ a a
a2) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
||~ ((a a
a1 a a -> a a -> SymBool
forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
a2) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ (b a
b1 b a -> b a -> SymBool
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 a a -> a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ a a
a2) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
||~ ((a a
a1 a a -> a a -> SymBool
forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
a2) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ (b a
b1 b a -> b a -> SymBool
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 a a -> a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ a a
a2) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
||~ ((a a
a1 a a -> a a -> SymBool
forall (f :: * -> *) a. SEq' f => f a -> f a -> SymBool
==~~ a a
a2) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ (b a
b1 b a -> b a -> SymBool
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 <- a a -> a a -> UnionM Ordering
forall (f :: * -> *) a. SOrd' f => f a -> f a -> UnionM Ordering
symCompare' a a
a1 a a
a2
    case Ordering
l of
      Ordering
EQ -> b a -> b a -> UnionM Ordering
forall (f :: * -> *) a. SOrd' f => f a -> f a -> UnionM Ordering
symCompare' b a
b1 b a
b2
      Ordering
_ -> Ordering -> UnionM 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 = a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<~~ a -> Rep a Any
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 = a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
<=~~ a -> Rep a Any
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 = a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>~~ a -> Rep a Any
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 = a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
>=~~ a -> Rep a Any
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 = Rep a Any -> Rep a Any -> UnionM Ordering
forall (f :: * -> *) a. SOrd' f => f a -> f a -> UnionM Ordering
symCompare' (a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
x) (a -> Rep a Any
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 a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
<=~ a
y SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
&&~ a
x a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
/=~ a
y
  a
x >~ a
y = a
y a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
<~ a
x
  a
x >=~ a
y = a
y a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
<=~ a
x
  symCompare :: a -> a -> UnionM Ordering
  symCompare a
l a
r =
    SymBool -> UnionM Ordering -> UnionM Ordering -> UnionM Ordering
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
      (a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
<~ a
r)
      (Ordering -> UnionM Ordering
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
LT)
      (SymBool -> UnionM Ordering -> UnionM Ordering -> UnionM Ordering
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
l a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
==~ a
r) (Ordering -> UnionM Ordering
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle Ordering
EQ) (Ordering -> UnionM Ordering
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 a -> a -> SymBool
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 a -> a -> SymBool
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 a -> a -> SymBool
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 a -> a -> SymBool
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) = a -> a -> UnionM Ordering
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

#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(B.ByteString)
#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
forall {a}. SOrd a => [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. SOrd a => a -> a -> SymBool
<~ a
y else a
x a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
>~ a
y) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
||~ (a
x a -> a -> SymBool
forall a. SEq 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

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

instance (SOrd a) => SOrd [a] where
  <=~ :: [a] -> [a] -> SymBool
(<=~) = Bool -> Bool -> [a] -> [a] -> SymBool
forall a. SOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
True Bool
False
  <~ :: [a] -> [a] -> SymBool
(<~) = Bool -> Bool -> [a] -> [a] -> SymBool
forall a. SOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
True Bool
True
  >=~ :: [a] -> [a] -> SymBool
(>=~) = Bool -> Bool -> [a] -> [a] -> SymBool
forall a. SOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
False Bool
False
  >~ :: [a] -> [a] -> SymBool
(>~) = Bool -> Bool -> [a] -> [a] -> SymBool
forall a. SOrd a => Bool -> Bool -> [a] -> [a] -> SymBool
symCompareSingleList Bool
False Bool
True
  symCompare :: [a] -> [a] -> UnionM Ordering
symCompare = [a] -> [a] -> UnionM Ordering
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 m (Maybe a) -> m (Maybe a) -> SymBool
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 m (Maybe a) -> m (Maybe a) -> SymBool
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 m (Maybe a) -> m (Maybe a) -> SymBool
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 m (Maybe a) -> m (Maybe a) -> SymBool
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) = m (Maybe a) -> m (Maybe a) -> UnionM Ordering
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 m (Either e a) -> m (Either e a) -> SymBool
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 m (Either e a) -> m (Either e a) -> SymBool
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 m (Either e a) -> m (Either e a) -> SymBool
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 m (Either e a) -> m (Either e a) -> SymBool
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) = m (Either e a) -> m (Either e a) -> UnionM Ordering
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 m (a, s) -> m (a, s) -> SymBool
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 m (a, s) -> m (a, s) -> SymBool
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 m (a, s) -> m (a, s) -> SymBool
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 m (a, s) -> m (a, s) -> SymBool
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) = m (a, s) -> m (a, s) -> UnionM Ordering
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 m (a, s) -> m (a, s) -> SymBool
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 m (a, s) -> m (a, s) -> SymBool
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 m (a, s) -> m (a, s) -> SymBool
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 m (a, s) -> m (a, s) -> SymBool
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) = m (a, s) -> m (a, s) -> UnionM Ordering
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 a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
<=~ a
r
  (Identity a
l) <~ :: Identity a -> Identity a -> SymBool
<~ (Identity a
r) = a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
<~ a
r
  (Identity a
l) >=~ :: Identity a -> Identity a -> SymBool
>=~ (Identity a
r) = a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
>=~ a
r
  (Identity a
l) >~ :: Identity a -> Identity a -> SymBool
>~ (Identity a
r) = a
l a -> a -> SymBool
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 a -> a -> UnionM Ordering
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 m a -> m a -> SymBool
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 m a -> m a -> SymBool
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 m a -> m a -> SymBool
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 m a -> m a -> SymBool
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 m a -> m a -> UnionM Ordering
forall a. SOrd a => a -> a -> UnionM Ordering
`symCompare` m a
r