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

-- |
-- Module      :   Grisette.Internal.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.Core.Data.Class.SymOrd
  ( -- * Symbolic total order relation
    SymOrd (..),
    SymOrd1 (..),
    symCompare1,
    SymOrd2 (..),
    symCompare2,

    -- * Min and max
    symMax,
    symMin,
    mrgMax,
    mrgMin,

    -- * Generic 'SymOrd'
    SymOrdArgs (..),
    GSymOrd (..),
    genericSymCompare,
    genericLiftSymCompare,
  )
where

import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
  ( Identity (Identity),
    IdentityT (IdentityT),
  )
import Control.Monad.Trans.Maybe (MaybeT (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.Kind (Type)
import Data.Monoid (Alt, Ap)
import qualified Data.Monoid as Monoid
import Data.Ord (Down (Down))
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),
    Generic (Rep, from),
    Generic1 (Rep1, from1),
    K1 (K1),
    M1 (M1),
    Par1 (Par1),
    Rec1 (Rec1),
    U1,
    V1,
    (:.:) (Comp1),
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Grisette.Internal.Core.Control.Exception
  ( AssertionError,
    VerificationConditions,
  )
import Grisette.Internal.Core.Control.Monad.Union (Union)
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp, symIte)
import Grisette.Internal.Core.Data.Class.LogicalOp
  ( LogicalOp (symNot, (.&&), (.||)),
  )
import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Internal.Core.Data.Class.PlainUnion
  ( simpleMerge,
  )
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( SymBranching,
    mrgIf,
  )
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Core.Data.Class.SymEq
  ( GSymEq,
    SymEq ((.==)),
    SymEq1,
    SymEq2,
  )
import Grisette.Internal.Core.Data.Class.TryMerge
  ( mrgSingle,
    tryMerge,
  )
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.DeriveBuiltin (deriveBuiltins)
import Grisette.Internal.TH.DeriveInstanceProvider
  ( Strategy (ViaDefault, ViaDefault1),
  )
import Grisette.Internal.Utils.Derive (Arity0, Arity1)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim

-- | 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.Union` and `Grisette.Core.PlainUnion` for more
-- information.
--
-- >>> a `symCompare` b :: Union Ordering
-- {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 SymOrd via (Default X)
class (SymEq a) => SymOrd 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 =
    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
$
      a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare a
x a
y Union Ordering -> (Ordering -> Union SymBool) -> Union SymBool
forall a b. Union a -> (a -> Union b) -> Union b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Ordering
LT -> Bool -> Union SymBool
forall c t. Solvable c t => c -> t
con Bool
True
        Ordering
EQ -> Bool -> Union SymBool
forall c t. Solvable c t => c -> t
con Bool
False
        Ordering
GT -> Bool -> Union SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  {-# INLINE (.<) #-}
  a
x .<= a
y = SymBool -> SymBool
forall b. LogicalOp b => b -> b
symNot (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.> a
y)
  {-# INLINE (.<=) #-}
  a
x .> a
y = a
y a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< a
x
  {-# INLINE (.>) #-}
  a
x .>= a
y = a
y a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.<= a
x
  {-# INLINE (.>=) #-}
  symCompare :: a -> a -> Union Ordering
  symCompare a
l a
r =
    SymBool -> Union Ordering -> Union Ordering -> Union Ordering
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
      (a
l a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< a
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 (a
l a -> a -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== a
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 #-}
  {-# MINIMAL (.<) | symCompare #-}

-- | Lifting of the 'SymOrd' class to unary type constructors.
--
-- Any instance should be subject to the following law that canonicity is
-- preserved:
--
-- @liftSymCompare symCompare@ should be equivalent to @symCompare@, under the
-- symbolic semantics.
--
-- This class therefore represents the generalization of 'SymOrd' by decomposing
-- its main method into a canonical lifting on a canonical inner method, so that
-- the lifting can be reused for other arguments than the canonical one.
class (SymEq1 f, forall a. (SymOrd a) => SymOrd (f a)) => SymOrd1 f where
  -- | Lift a 'symCompare' function through the type constructor.
  --
  -- The function will usually be applied to an symbolic comparison function,
  -- but the more general type ensures that the implementation uses it to
  -- compare elements of the first container with elements of the second.
  liftSymCompare :: (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering

-- | Lift the standard 'symCompare' function to binary type constructors.
symCompare1 :: (SymOrd1 f, SymOrd a) => f a -> f a -> Union Ordering
symCompare1 :: forall (f :: * -> *) a.
(SymOrd1 f, SymOrd a) =>
f a -> f a -> Union Ordering
symCompare1 = (a -> a -> Union Ordering) -> f a -> f a -> 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 -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare
{-# INLINE symCompare1 #-}

-- | Lifting of the 'SymOrd' class to binary type constructors.
class (SymEq2 f, forall a. (SymOrd a) => SymOrd1 (f a)) => SymOrd2 f where
  -- | Lift a 'symCompare' function through the type constructor.
  --
  -- The function will usually be applied to an symbolic comparison function,
  -- but the more general type ensures that the implementation uses it to
  -- compare elements of the first container with elements of the second.
  liftSymCompare2 ::
    (a -> b -> Union Ordering) ->
    (c -> d -> Union Ordering) ->
    f a c ->
    f b d ->
    Union Ordering

-- | Lift the standard 'symCompare' function through the type constructors.
symCompare2 :: (SymOrd2 f, SymOrd a, SymOrd b) => f a b -> f a b -> Union Ordering
symCompare2 :: forall (f :: * -> * -> *) a b.
(SymOrd2 f, SymOrd a, SymOrd b) =>
f a b -> f a b -> Union Ordering
symCompare2 = (a -> a -> Union Ordering)
-> (b -> b -> Union Ordering) -> f a b -> f a b -> Union Ordering
forall a b c d.
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering) -> f a c -> f b d -> Union Ordering
forall (f :: * -> * -> *) a b c d.
SymOrd2 f =>
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering) -> f a c -> f b d -> Union Ordering
liftSymCompare2 a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare b -> b -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare
{-# INLINE symCompare2 #-}

-- | Symbolic maximum.
symMax :: (SymOrd a, ITEOp a) => a -> a -> a
symMax :: forall a. (SymOrd a, ITEOp a) => a -> a -> a
symMax a
x a
y = SymBool -> a -> a -> a
forall v. ITEOp v => SymBool -> v -> v -> v
symIte (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
y) a
x a
y
{-# INLINE symMax #-}

-- | Symbolic minimum.
symMin :: (SymOrd a, ITEOp a) => a -> a -> a
symMin :: forall a. (SymOrd a, ITEOp a) => a -> a -> a
symMin a
x a
y = SymBool -> a -> a -> a
forall v. ITEOp v => SymBool -> v -> v -> v
symIte (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
y) a
y a
x
{-# INLINE symMin #-}

-- | Symbolic maximum, with a union-like monad.
mrgMax ::
  (SymOrd a, Mergeable a, SymBranching m, Applicative m) =>
  a ->
  a ->
  m a
mrgMax :: forall a (m :: * -> *).
(SymOrd a, Mergeable a, SymBranching m, Applicative m) =>
a -> a -> m a
mrgMax a
x a
y = SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
y) (a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x) (a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
y)
{-# INLINE mrgMax #-}

-- | Symbolic minimum, with a union-like monad.
mrgMin ::
  (SymOrd a, Mergeable a, SymBranching m, Applicative m) =>
  a ->
  a ->
  m a
mrgMin :: forall a (m :: * -> *).
(SymOrd a, Mergeable a, SymBranching m, Applicative m) =>
a -> a -> m a
mrgMin a
x a
y = SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
x a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
y) (a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
y) (a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
x)
{-# INLINE mrgMin #-}

-- Derivations

-- | The arguments to the generic comparison function.
data family SymOrdArgs arity a b :: Type

data instance SymOrdArgs Arity0 _ _ = SymOrdArgs0

newtype instance SymOrdArgs Arity1 a b
  = SymOrdArgs1 (a -> b -> Union Ordering)

-- | The class of types that can be generically symbolically compared.
class GSymOrd arity f where
  gsymCompare :: SymOrdArgs arity a b -> f a -> f b -> Union Ordering

instance GSymOrd arity V1 where
  gsymCompare :: forall a b. SymOrdArgs arity a b -> V1 a -> V1 b -> Union Ordering
gsymCompare SymOrdArgs arity a b
_ V1 a
_ V1 b
_ = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ
  {-# INLINE gsymCompare #-}

instance GSymOrd arity U1 where
  gsymCompare :: forall a b. SymOrdArgs arity a b -> U1 a -> U1 b -> Union Ordering
gsymCompare SymOrdArgs arity a b
_ U1 a
_ U1 b
_ = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ
  {-# INLINE gsymCompare #-}

instance
  (GSymOrd arity a, GSymOrd arity b) =>
  GSymOrd arity (a :*: b)
  where
  gsymCompare :: forall a b.
SymOrdArgs arity a b
-> (:*:) a b a -> (:*:) a b b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args (a a
a1 :*: b a
b1) (a b
a2 :*: b b
b2) = do
    Ordering
l <- SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall a b. SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args a a
a1 a b
a2
    case Ordering
l of
      Ordering
EQ -> SymOrdArgs arity a b -> b a -> b b -> Union Ordering
forall a b. SymOrdArgs arity a b -> b a -> b b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args b a
b1 b b
b2
      Ordering
_ -> Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
l
  {-# INLINE gsymCompare #-}

instance
  (GSymOrd arity a, GSymOrd arity b) =>
  GSymOrd arity (a :+: b)
  where
  gsymCompare :: forall a b.
SymOrdArgs arity a b
-> (:+:) a b a -> (:+:) a b b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args (L1 a a
a) (L1 a b
b) = SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall a b. SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args a a
a a b
b
  gsymCompare SymOrdArgs arity a b
_ (L1 a a
_) (R1 b b
_) = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT
  gsymCompare SymOrdArgs arity a b
args (R1 b a
a) (R1 b b
b) = SymOrdArgs arity a b -> b a -> b b -> Union Ordering
forall a b. SymOrdArgs arity a b -> b a -> b b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args b a
a b b
b
  gsymCompare SymOrdArgs arity a b
_ (R1 b a
_) (L1 a b
_) = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
GT
  {-# INLINE gsymCompare #-}

instance (GSymOrd arity a) => GSymOrd arity (M1 i c a) where
  gsymCompare :: forall a b.
SymOrdArgs arity a b -> M1 i c a a -> M1 i c a b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args (M1 a a
a) (M1 a b
b) = SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall a b. SymOrdArgs arity a b -> a a -> a b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs arity a b
args a a
a a b
b
  {-# INLINE gsymCompare #-}

instance (SymOrd a) => GSymOrd arity (K1 i a) where
  gsymCompare :: forall a b.
SymOrdArgs arity a b -> K1 i a a -> K1 i a b -> Union Ordering
gsymCompare SymOrdArgs arity a b
_ (K1 a
a) (K1 a
b) = a
a a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
`symCompare` a
b
  {-# INLINE gsymCompare #-}

instance GSymOrd Arity1 Par1 where
  gsymCompare :: forall a b.
SymOrdArgs Arity1 a b -> Par1 a -> Par1 b -> Union Ordering
gsymCompare (SymOrdArgs1 a -> b -> Union Ordering
c) (Par1 a
a) (Par1 b
b) = a -> b -> Union Ordering
c a
a b
b
  {-# INLINE gsymCompare #-}

instance (SymOrd1 f) => GSymOrd Arity1 (Rec1 f) where
  gsymCompare :: forall a b.
SymOrdArgs Arity1 a b -> Rec1 f a -> Rec1 f b -> Union Ordering
gsymCompare (SymOrdArgs1 a -> b -> Union Ordering
c) (Rec1 f a
a) (Rec1 f b
b) = (a -> b -> Union Ordering) -> f a -> f 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
c f a
a f b
b
  {-# INLINE gsymCompare #-}

instance (SymOrd1 f, GSymOrd Arity1 g) => GSymOrd Arity1 (f :.: g) where
  gsymCompare :: forall a b.
SymOrdArgs Arity1 a b
-> (:.:) f g a -> (:.:) f g b -> Union Ordering
gsymCompare SymOrdArgs Arity1 a b
targs (Comp1 f (g a)
a) (Comp1 f (g b)
b) = (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 (SymOrdArgs Arity1 a b -> g a -> g b -> Union Ordering
forall a b. SymOrdArgs Arity1 a b -> g a -> g b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs Arity1 a b
targs) f (g a)
a f (g b)
b
  {-# INLINE gsymCompare #-}

instance
  (Generic a, GSymOrd Arity0 (Rep a), GSymEq Arity0 (Rep a)) =>
  SymOrd (Default a)
  where
  symCompare :: Default a -> Default a -> Union Ordering
symCompare (Default a
l) (Default a
r) = a -> a -> Union Ordering
forall a.
(Generic a, GSymOrd Arity0 (Rep a)) =>
a -> a -> Union Ordering
genericSymCompare a
l a
r
  {-# INLINE symCompare #-}

-- | Generic 'symCompare' function.
genericSymCompare :: (Generic a, GSymOrd Arity0 (Rep a)) => a -> a -> Union Ordering
genericSymCompare :: forall a.
(Generic a, GSymOrd Arity0 (Rep a)) =>
a -> a -> Union Ordering
genericSymCompare a
l a
r = SymOrdArgs Arity0 Any Any
-> Rep a Any -> Rep a Any -> Union Ordering
forall a b.
SymOrdArgs Arity0 a b -> Rep a a -> Rep a b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare SymOrdArgs Arity0 Any Any
forall _ _. SymOrdArgs Arity0 _ _
SymOrdArgs0 (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
l) (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
r)
{-# INLINE genericSymCompare #-}

instance
  (Generic1 f, GSymOrd Arity1 (Rep1 f), GSymEq Arity1 (Rep1 f), SymOrd a) =>
  SymOrd (Default1 f a)
  where
  symCompare :: Default1 f a -> Default1 f a -> Union Ordering
symCompare = Default1 f a -> Default1 f a -> Union Ordering
forall (f :: * -> *) a.
(SymOrd1 f, SymOrd a) =>
f a -> f a -> Union Ordering
symCompare1
  {-# INLINE symCompare #-}

instance
  (Generic1 f, GSymOrd Arity1 (Rep1 f), GSymEq Arity1 (Rep1 f)) =>
  SymOrd1 (Default1 f)
  where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering)
-> Default1 f a -> Default1 f b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
c (Default1 f a
l) (Default1 f b
r) = (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
forall (f :: * -> *) a b.
(Generic1 f, GSymOrd Arity1 (Rep1 f)) =>
(a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
genericLiftSymCompare a -> b -> Union Ordering
c f a
l f b
r
  {-# INLINE liftSymCompare #-}

-- | Generic 'liftSymCompare' function.
genericLiftSymCompare ::
  (Generic1 f, GSymOrd Arity1 (Rep1 f)) =>
  (a -> b -> Union Ordering) ->
  f a ->
  f b ->
  Union Ordering
genericLiftSymCompare :: forall (f :: * -> *) a b.
(Generic1 f, GSymOrd Arity1 (Rep1 f)) =>
(a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
genericLiftSymCompare a -> b -> Union Ordering
c f a
l f b
r = SymOrdArgs Arity1 a b -> Rep1 f a -> Rep1 f b -> Union Ordering
forall a b.
SymOrdArgs Arity1 a b -> Rep1 f a -> Rep1 f b -> Union Ordering
forall arity (f :: * -> *) a b.
GSymOrd arity f =>
SymOrdArgs arity a b -> f a -> f b -> Union Ordering
gsymCompare ((a -> b -> Union Ordering) -> SymOrdArgs Arity1 a b
forall a b. (a -> b -> Union Ordering) -> SymOrdArgs Arity1 a b
SymOrdArgs1 a -> b -> Union Ordering
c) (f a -> Rep1 f a
forall a. f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f a
l) (f b -> Rep1 f b
forall a. f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1 f b
r)
{-# INLINE genericLiftSymCompare #-}

#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 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
    a
x1 <- Union a
x
    a
y1 <- Union a
y
    SymBool -> Union SymBool
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (SymBool -> Union SymBool) -> SymBool -> Union SymBool
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.<= a
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
    a
x1 <- Union a
x
    a
y1 <- Union a
y
    SymBool -> Union SymBool
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (SymBool -> Union SymBool) -> SymBool -> Union SymBool
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< a
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
    a
x1 <- Union a
x
    a
y1 <- Union a
y
    SymBool -> Union SymBool
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (SymBool -> Union SymBool) -> SymBool -> Union SymBool
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= a
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
    a
x1 <- Union a
x
    a
y1 <- Union a
y
    SymBool -> Union SymBool
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (SymBool -> Union SymBool) -> SymBool -> Union SymBool
forall a b. (a -> b) -> a -> b
$ a
x1 a -> a -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.> a
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
    a
x1 <- Union a
x
    a
y1 <- Union a
y
    a
x1 a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
`symCompare` a
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
    a
x1 <- Union a
x
    b
y1 <- Union b
y
    a -> b -> Union Ordering
f a
x1 b
y1

-- Instances
deriveBuiltins
  (ViaDefault ''SymOrd)
  [''SymOrd]
  [ ''Maybe,
    ''Either,
    ''(),
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''AssertionError,
    ''VerificationConditions,
    ''NotRepresentableFPError,
    ''Identity,
    ''Monoid.Dual,
    ''Monoid.Sum,
    ''Monoid.Product,
    ''Monoid.First,
    ''Monoid.Last
  ]

deriveBuiltins
  (ViaDefault1 ''SymOrd1)
  [''SymOrd, ''SymOrd1]
  [ ''Maybe,
    ''Either,
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''Identity,
    ''Monoid.Dual,
    ''Monoid.Sum,
    ''Monoid.Product,
    ''Monoid.First,
    ''Monoid.Last
  ]

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
  Ordering
oxy <- a -> b -> Union Ordering
f a
x b
y
  case Ordering
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 #-}

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

instance (SymOrd1 m, SymOrd e) => SymOrd1 (ExceptT e m) where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering)
-> ExceptT e m a -> ExceptT e m b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
f (ExceptT m (Either e a)
l) (ExceptT m (Either e b)
r) =
    (Either e a -> Either e b -> Union Ordering)
-> m (Either e a) -> m (Either e 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)
-> Either e a -> Either e b -> Union Ordering
forall a b.
(a -> b -> Union Ordering)
-> Either e a -> Either e 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 (Either e a)
l m (Either e b)
r
  {-# INLINE liftSymCompare #-}

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

instance (SymOrd1 m) => SymOrd1 (MaybeT m) where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering)
-> MaybeT m a -> MaybeT m b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
f (MaybeT m (Maybe a)
l) (MaybeT m (Maybe b)
r) = (Maybe a -> Maybe b -> Union Ordering)
-> m (Maybe a) -> m (Maybe 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) -> Maybe a -> Maybe b -> Union Ordering
forall a b.
(a -> b -> Union Ordering) -> Maybe a -> Maybe 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 (Maybe a)
l m (Maybe b)
r
  {-# INLINE liftSymCompare #-}

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

instance (SymOrd1 m, SymOrd w) => SymOrd1 (WriterLazy.WriterT w m) where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering)
-> WriterT w m a -> WriterT w m b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
f (WriterLazy.WriterT m (a, w)
l) (WriterLazy.WriterT m (b, w)
r) =
    ((a, w) -> (b, w) -> Union Ordering)
-> m (a, w) -> m (b, w) -> 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)
-> (w -> w -> Union Ordering) -> (a, w) -> (b, w) -> Union Ordering
forall a b c d.
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering) -> (a, c) -> (b, d) -> Union Ordering
forall (f :: * -> * -> *) a b c d.
SymOrd2 f =>
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering) -> f a c -> f b d -> Union Ordering
liftSymCompare2 a -> b -> Union Ordering
f w -> w -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare) m (a, w)
l m (b, w)
r
  {-# INLINE liftSymCompare #-}

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

instance (SymOrd1 m, SymOrd w) => SymOrd1 (WriterStrict.WriterT w m) where
  liftSymCompare :: forall a b.
(a -> b -> Union Ordering)
-> WriterT w m a -> WriterT w m b -> Union Ordering
liftSymCompare a -> b -> Union Ordering
f (WriterStrict.WriterT m (a, w)
l) (WriterStrict.WriterT m (b, w)
r) =
    ((a, w) -> (b, w) -> Union Ordering)
-> m (a, w) -> m (b, w) -> 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)
-> (w -> w -> Union Ordering) -> (a, w) -> (b, w) -> Union Ordering
forall a b c d.
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering) -> (a, c) -> (b, d) -> Union Ordering
forall (f :: * -> * -> *) a b c d.
SymOrd2 f =>
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering) -> f a c -> f b d -> Union Ordering
liftSymCompare2 a -> b -> Union Ordering
f w -> w -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare) m (a, w)
l m (b, w)
r
  {-# 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
    Ordering
res <- a -> b -> Union Ordering
comp a
l b
r
    case Ordering
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 #-}

instance SymOrd2 Either where
  liftSymCompare2 :: forall a b c d.
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering)
-> Either a c
-> Either b d
-> Union Ordering
liftSymCompare2 a -> b -> Union Ordering
f c -> d -> Union Ordering
_ (Left a
l) (Left b
r) = a -> b -> Union Ordering
f a
l b
r
  liftSymCompare2 a -> b -> Union Ordering
_ c -> d -> Union Ordering
g (Right c
l) (Right d
r) = c -> d -> Union Ordering
g c
l d
r
  liftSymCompare2 a -> b -> Union Ordering
_ c -> d -> Union Ordering
_ (Left a
_) (Right d
_) = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT
  liftSymCompare2 a -> b -> Union Ordering
_ c -> d -> Union Ordering
_ (Right c
_) (Left b
_) = Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
GT
  {-# INLINE liftSymCompare2 #-}

instance SymOrd2 (,) where
  liftSymCompare2 :: forall a b c d.
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering) -> (a, c) -> (b, d) -> Union Ordering
liftSymCompare2 a -> b -> Union Ordering
f c -> d -> Union Ordering
g (a
a1, c
b1) (b
a2, d
b2) = do
    Ordering
ma <- a -> b -> Union Ordering
f a
a1 b
a2
    Ordering
mb <- c -> d -> Union Ordering
g c
b1 d
b2
    Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Ordering -> Union Ordering) -> Ordering -> Union Ordering
forall a b. (a -> b) -> a -> b
$ Ordering
ma Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Ordering
mb
  {-# INLINE liftSymCompare2 #-}

instance (SymOrd a) => SymOrd2 ((,,) a) where
  liftSymCompare2 :: forall a b c d.
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering)
-> (a, a, c)
-> (a, b, d)
-> Union Ordering
liftSymCompare2 a -> b -> Union Ordering
f c -> d -> Union Ordering
g (a
a1, a
b1, c
c1) (a
a2, b
b2, d
c2) = do
    Ordering
ma <- a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare a
a1 a
a2
    Ordering
mb <- a -> b -> Union Ordering
f a
b1 b
b2
    Ordering
mc <- c -> d -> Union Ordering
g c
c1 d
c2
    Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Ordering -> Union Ordering) -> Ordering -> Union Ordering
forall a b. (a -> b) -> a -> b
$ Ordering
ma Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Ordering
mb Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Ordering
mc
  {-# INLINE liftSymCompare2 #-}

instance (SymOrd a, SymOrd b) => SymOrd2 ((,,,) a b) where
  liftSymCompare2 :: forall a b c d.
(a -> b -> Union Ordering)
-> (c -> d -> Union Ordering)
-> (a, b, a, c)
-> (a, b, b, d)
-> Union Ordering
liftSymCompare2 a -> b -> Union Ordering
f c -> d -> Union Ordering
g (a
a1, b
b1, a
c1, c
d1) (a
a2, b
b2, b
c2, d
d2) = do
    Ordering
ma <- a -> a -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare a
a1 a
a2
    Ordering
mb <- b -> b -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare b
b1 b
b2
    Ordering
mc <- a -> b -> Union Ordering
f a
c1 b
c2
    Ordering
md <- c -> d -> Union Ordering
g c
d1 d
d2
    Ordering -> Union Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Ordering -> Union Ordering) -> Ordering -> Union Ordering
forall a b. (a -> b) -> a -> b
$ Ordering
ma Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Ordering
mb Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Ordering
mc Ordering -> Ordering -> Ordering
forall a. Semigroup a => a -> a -> a
<> Ordering
md
  {-# INLINE liftSymCompare2 #-}