{-# 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.Internal.Core.Data.Class.SOrd
-- 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.SOrd
  ( -- * Symbolic total order relation
    SOrd (..),
    SOrd' (..),
    symMax,
    symMin,
    mrgMax,
    mrgMin,
  )
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.Sum (Sum)
import Data.Int (Int16, Int32, Int64, Int8)
import qualified Data.Text as T
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeLits (KnownNat, type (<=))
import Generics.Deriving
  ( Default (Default),
    Generic (Rep, from),
    K1 (K1),
    M1 (M1),
    U1,
    V1,
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)
import Grisette.Internal.Core.Control.Monad.UnionM (UnionM, liftToMonadUnion)
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.SEq (SEq ((./=), (.==)), SEq' ((..==)))
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( UnionMergeable1,
    mrgIf,
  )
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Core.Data.Class.TryMerge
  ( mrgSingle,
    tryMerge,
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Term
  ( PEvalOrdTerm
      ( pevalLeOrdTerm,
        pevalLtOrdTerm
      ),
    pevalGeOrdTerm,
    pevalGtOrdTerm,
  )
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN (SymIntN),
    SymWordN (SymWordN),
  )
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))

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

-- | 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 `PlainUnion` 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.
(UnionMergeable1 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT)
      (SymBool -> UnionM Ordering -> UnionM Ordering -> UnionM Ordering
forall (u :: * -> *) a.
(UnionMergeable1 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ) (Ordering -> UnionM Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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

#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(B.ByteString)
CONCRETE_SORD(T.Text)
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 [] [] = 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
GT
symCompareList [] [a]
_ = Ordering -> UnionM Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT
symCompareList [a]
_ [] = Ordering -> UnionM Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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

-- SOrd
#define SORD_SIMPLE(symtype) \
instance SOrd 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))

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

instance SOrd 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
  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
  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
  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
  symCompare :: SymBool -> SymBool -> UnionM Ordering
symCompare SymBool
l SymBool
r =
    SymBool -> UnionM Ordering -> UnionM Ordering -> UnionM Ordering
forall (u :: * -> *) a.
(UnionMergeable1 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 -> UnionM Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT)
      (SymBool -> UnionM Ordering -> UnionM Ordering -> UnionM Ordering
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymBool
l SymBool -> SymBool -> SymBool
forall a. SEq a => a -> a -> SymBool
.== SymBool
r) (Ordering -> UnionM Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ) (Ordering -> UnionM Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
GT))

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

-- Exception
instance SOrd AssertionError where
  AssertionError
_ .<= :: AssertionError -> AssertionError -> SymBool
.<= AssertionError
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  AssertionError
_ .< :: AssertionError -> AssertionError -> SymBool
.< AssertionError
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  AssertionError
_ .>= :: AssertionError -> AssertionError -> SymBool
.>= AssertionError
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  AssertionError
_ .> :: AssertionError -> AssertionError -> SymBool
.> AssertionError
_ = Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  AssertionError
_ symCompare :: AssertionError -> AssertionError -> UnionM Ordering
`symCompare` AssertionError
_ = Ordering -> UnionM Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
EQ

instance SOrd VerificationConditions where
  VerificationConditions
l .>= :: VerificationConditions -> VerificationConditions -> SymBool
.>= VerificationConditions
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ VerificationConditions
l VerificationConditions -> VerificationConditions -> Bool
forall a. Ord a => a -> a -> Bool
>= VerificationConditions
r
  VerificationConditions
l .> :: VerificationConditions -> VerificationConditions -> SymBool
.> VerificationConditions
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ VerificationConditions
l VerificationConditions -> VerificationConditions -> Bool
forall a. Ord a => a -> a -> Bool
> VerificationConditions
r
  VerificationConditions
l .<= :: VerificationConditions -> VerificationConditions -> SymBool
.<= VerificationConditions
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ VerificationConditions
l VerificationConditions -> VerificationConditions -> Bool
forall a. Ord a => a -> a -> Bool
<= VerificationConditions
r
  VerificationConditions
l .< :: VerificationConditions -> VerificationConditions -> SymBool
.< VerificationConditions
r = Bool -> SymBool
forall c t. Solvable c t => c -> t
con (Bool -> SymBool) -> Bool -> SymBool
forall a b. (a -> b) -> a -> b
$ VerificationConditions
l VerificationConditions -> VerificationConditions -> Bool
forall a. Ord a => a -> a -> Bool
< VerificationConditions
r
  VerificationConditions
l symCompare :: VerificationConditions -> VerificationConditions -> UnionM Ordering
`symCompare` VerificationConditions
r = Ordering -> UnionM Ordering
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (Ordering -> UnionM Ordering) -> Ordering -> UnionM Ordering
forall a b. (a -> b) -> a -> b
$ VerificationConditions
l VerificationConditions -> VerificationConditions -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` VerificationConditions
r

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

-- | 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 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 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 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 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 a. 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 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 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 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 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 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 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 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 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 a. 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle Ordering
LT
  symCompare' (R1 b a
a) (R1 b a
b) = b a -> b a -> UnionM Ordering
forall a. 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 a. 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 a. 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 a. 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 a. 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 a. 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 a. 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 a. 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 a. 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 a. 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 a. 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 a. 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 a. 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 a. 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 a. 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 (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m 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 x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> SymBool
forall a. Rep a a -> Rep a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
..< a -> Rep a Any
forall x. a -> Rep a x
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 x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> SymBool
forall a. Rep a a -> Rep a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
..<= a -> Rep a Any
forall x. a -> Rep a x
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 x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> SymBool
forall a. Rep a a -> Rep a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
..> a -> Rep a Any
forall x. a -> Rep a x
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 x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x Rep a Any -> Rep a Any -> SymBool
forall a. Rep a a -> Rep a a -> SymBool
forall (f :: * -> *) a. SOrd' f => f a -> f a -> SymBool
..>= a -> Rep a Any
forall x. a -> Rep a x
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 a. Rep a a -> Rep a a -> UnionM Ordering
forall (f :: * -> *) a. SOrd' f => f a -> f a -> UnionM Ordering
symCompare' (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
x) (a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
y)

symMax :: (SOrd a, ITEOp a) => a -> a -> a
symMax :: forall a. (SOrd 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. SOrd a => a -> a -> SymBool
.>= a
y) a
x a
y

symMin :: (SOrd a, ITEOp a) => a -> a -> a
symMin :: forall a. (SOrd 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. SOrd a => a -> a -> SymBool
.>= a
y) a
y a
x

mrgMax ::
  (SOrd a, Mergeable a, UnionMergeable1 m, Applicative m) =>
  a ->
  a ->
  m a
mrgMax :: forall a (m :: * -> *).
(SOrd a, Mergeable a, UnionMergeable1 m, Applicative m) =>
a -> a -> m a
mrgMax a
x a
y = SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
x a -> a -> SymBool
forall a. SOrd 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)

mrgMin ::
  (SOrd a, Mergeable a, UnionMergeable1 m, Applicative m) =>
  a ->
  a ->
  m a
mrgMin :: forall a (m :: * -> *).
(SOrd a, Mergeable a, UnionMergeable1 m, Applicative m) =>
a -> a -> m a
mrgMin a
x a
y = SymBool -> m a -> m a -> m a
forall (u :: * -> *) a.
(UnionMergeable1 u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (a
x a -> a -> SymBool
forall a. SOrd 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)