{-# 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
(
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))
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
#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
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
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
class (SEq' f) => SOrd' f where
(..<) :: f a -> f a -> SymBool
infix 4 ..<
(..<=) :: f a -> f a -> SymBool
infix 4 ..<=
(..>) :: f a -> f a -> SymBool
infix 4 ..>
(..>=) :: f a -> f a -> SymBool
infix 4 ..>=
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)