Copyright | (c) Sirui Lu 2021-2024 |
---|---|
License | BSD-3-Clause (see the LICENSE file) |
Maintainer | siruilu@cs.washington.edu |
Stability | Experimental |
Portability | GHC only |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- class SymEq a => SymOrd a where
- class (SymEq1 f, forall a. SymOrd a => SymOrd (f a)) => SymOrd1 f where
- liftSymCompare :: (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
- symCompare1 :: (SymOrd1 f, SymOrd a) => f a -> f a -> Union Ordering
- class (SymEq2 f, forall a. SymOrd a => SymOrd1 (f a)) => SymOrd2 f where
- symCompare2 :: (SymOrd2 f, SymOrd a, SymOrd b) => f a b -> f a b -> Union Ordering
- symMax :: (SymOrd a, ITEOp a) => a -> a -> a
- symMin :: (SymOrd a, ITEOp a) => a -> a -> a
- mrgMax :: (SymOrd a, Mergeable a, SymBranching m, Applicative m) => a -> a -> m a
- mrgMin :: (SymOrd a, Mergeable a, SymBranching m, Applicative m) => a -> a -> m a
- data family SymOrdArgs arity a b :: Type
- class GSymOrd arity f where
- gsymCompare :: SymOrdArgs arity a b -> f a -> f b -> Union Ordering
- genericSymCompare :: (Generic a, GSymOrd Arity0 (Rep a)) => a -> a -> Union Ordering
- genericLiftSymCompare :: (Generic1 f, GSymOrd Arity1 (Rep1 f)) => (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering
Symbolic total order relation
class SymEq a => SymOrd a where Source #
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
Union
and 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)
(.<) :: a -> a -> SymBool infix 4 Source #
(.<=) :: a -> a -> SymBool infix 4 Source #
(.>) :: a -> a -> SymBool infix 4 Source #
(.>=) :: a -> a -> SymBool infix 4 Source #
symCompare :: a -> a -> Union Ordering Source #
Instances
SymOrd All Source # | |
SymOrd Any Source # | |
SymOrd Int16 Source # | |
SymOrd Int32 Source # | |
SymOrd Int64 Source # | |
SymOrd Int8 Source # | |
SymOrd Word16 Source # | |
SymOrd Word32 Source # | |
SymOrd Word64 Source # | |
SymOrd Word8 Source # | |
SymOrd ByteString Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: ByteString -> ByteString -> SymBool Source # (.<=) :: ByteString -> ByteString -> SymBool Source # (.>) :: ByteString -> ByteString -> SymBool Source # (.>=) :: ByteString -> ByteString -> SymBool Source # symCompare :: ByteString -> ByteString -> Union Ordering Source # | |
SymOrd Ordering Source # | |
SymOrd AssertionError Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: AssertionError -> AssertionError -> SymBool Source # (.<=) :: AssertionError -> AssertionError -> SymBool Source # (.>) :: AssertionError -> AssertionError -> SymBool Source # (.>=) :: AssertionError -> AssertionError -> SymBool Source # symCompare :: AssertionError -> AssertionError -> Union Ordering Source # | |
SymOrd VerificationConditions Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: VerificationConditions -> VerificationConditions -> SymBool Source # (.<=) :: VerificationConditions -> VerificationConditions -> SymBool Source # (.>) :: VerificationConditions -> VerificationConditions -> SymBool Source # (.>=) :: VerificationConditions -> VerificationConditions -> SymBool Source # symCompare :: VerificationConditions -> VerificationConditions -> Union Ordering Source # | |
SymOrd AlgReal Source # | |
SymOrd FPRoundingMode Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # (.<=) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # (.>) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # (.>=) :: FPRoundingMode -> FPRoundingMode -> SymBool Source # symCompare :: FPRoundingMode -> FPRoundingMode -> Union Ordering Source # | |
SymOrd NotRepresentableFPError Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # (.<=) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # (.>) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # (.>=) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source # symCompare :: NotRepresentableFPError -> NotRepresentableFPError -> Union Ordering Source # | |
SymOrd SomeBVException Source # | |
Defined in Grisette.Internal.SymPrim.SomeBV (.<) :: SomeBVException -> SomeBVException -> SymBool Source # (.<=) :: SomeBVException -> SomeBVException -> SymBool Source # (.>) :: SomeBVException -> SomeBVException -> SymBool Source # (.>=) :: SomeBVException -> SomeBVException -> SymBool Source # symCompare :: SomeBVException -> SomeBVException -> Union Ordering Source # | |
SymOrd SymAlgReal Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: SymAlgReal -> SymAlgReal -> SymBool Source # (.<=) :: SymAlgReal -> SymAlgReal -> SymBool Source # (.>) :: SymAlgReal -> SymAlgReal -> SymBool Source # (.>=) :: SymAlgReal -> SymAlgReal -> SymBool Source # symCompare :: SymAlgReal -> SymAlgReal -> Union Ordering Source # | |
SymOrd SymBool Source # | |
SymOrd SymFPRoundingMode Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source # (.<=) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source # (.>) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source # (.>=) :: SymFPRoundingMode -> SymFPRoundingMode -> SymBool Source # symCompare :: SymFPRoundingMode -> SymFPRoundingMode -> Union Ordering Source # | |
SymOrd SymInteger Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: SymInteger -> SymInteger -> SymBool Source # (.<=) :: SymInteger -> SymInteger -> SymBool Source # (.>) :: SymInteger -> SymInteger -> SymBool Source # (.>=) :: SymInteger -> SymInteger -> SymBool Source # symCompare :: SymInteger -> SymInteger -> Union Ordering Source # | |
SymOrd Text Source # | |
SymOrd Integer Source # | |
SymOrd () Source # | |
SymOrd Bool Source # | |
SymOrd Char Source # | |
SymOrd Double Source # | |
SymOrd Float Source # | |
SymOrd Int Source # | |
SymOrd Word Source # | |
SymOrd a => SymOrd (Identity a) Source # | |
SymOrd a => SymOrd (First a) Source # | |
SymOrd a => SymOrd (Last a) Source # | |
SymOrd a => SymOrd (Down a) Source # | |
SymOrd a => SymOrd (Dual a) Source # | |
SymOrd a => SymOrd (Product a) Source # | |
SymOrd a => SymOrd (Sum a) Source # | |
SymOrd p => SymOrd (Par1 p) Source # | |
(SymOrd a, Integral a) => SymOrd (Ratio a) Source # | |
(Generic a, GSymOrd Arity0 (Rep a), GSymEq Arity0 (Rep a)) => SymOrd (Default a) Source # | |
SymOrd a => SymOrd (Union a) Source # | |
(KnownNat n, 1 <= n) => SymOrd (IntN n) Source # | |
(KnownNat n, 1 <= n) => SymOrd (WordN n) Source # | |
(forall (n :: Nat). (KnownNat n, 1 <= n) => SymOrd (bv n), forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n), MaySomeBV bv) => SymOrd (SomeBV bv) Source # | |
Defined in Grisette.Internal.SymPrim.SomeBV | |
(KnownNat n, 1 <= n) => SymOrd (SymIntN n) Source # | |
(KnownNat n, 1 <= n) => SymOrd (SymWordN n) Source # | |
SymOrd a => SymOrd (Maybe a) Source # | |
SymOrd a => SymOrd [a] Source # | |
(SymOrd a1, SymOrd a2) => SymOrd (Either a1 a2) Source # | |
SymOrd (Proxy a) Source # | |
SymOrd (U1 p) Source # | |
SymOrd (V1 p) Source # | |
(Generic1 f, GSymOrd Arity1 (Rep1 f), GSymEq Arity1 (Rep1 f), SymOrd a) => SymOrd (Default1 f a) Source # | |
(SymOrd a, SymOrd b) => SymOrd (CBMCEither a b) Source # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept (.<) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # (.<=) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # (.>) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # (.>=) :: CBMCEither a b -> CBMCEither a b -> SymBool Source # symCompare :: CBMCEither a b -> CBMCEither a b -> Union Ordering Source # | |
ValidFP eb sb => SymOrd (FP eb sb) Source # | |
ValidFP eb sb => SymOrd (SymFP eb sb) Source # | |
(SymOrd1 a1, SymOrd a2) => SymOrd (MaybeT a1 a2) Source # | |
(SymOrd a1, SymOrd a2) => SymOrd (a1, a2) Source # | |
SymOrd a => SymOrd (Const a b) Source # | |
SymOrd (f a) => SymOrd (Ap f a) Source # | |
SymOrd (f a) => SymOrd (Alt f a) Source # | |
SymOrd (f p) => SymOrd (Rec1 f p) Source # | |
SymOrd (m (CBMCEither e a)) => SymOrd (CBMCExceptT e m a) Source # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept (.<) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # (.<=) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # (.>) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # (.>=) :: CBMCExceptT e m a -> CBMCExceptT e m a -> SymBool Source # symCompare :: CBMCExceptT e m a -> CBMCExceptT e m a -> Union Ordering Source # | |
(SymOrd a1, SymOrd1 a2, SymOrd a3) => SymOrd (ExceptT a1 a2 a3) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: ExceptT a1 a2 a3 -> ExceptT a1 a2 a3 -> SymBool Source # (.<=) :: ExceptT a1 a2 a3 -> ExceptT a1 a2 a3 -> SymBool Source # (.>) :: ExceptT a1 a2 a3 -> ExceptT a1 a2 a3 -> SymBool Source # (.>=) :: ExceptT a1 a2 a3 -> ExceptT a1 a2 a3 -> SymBool Source # symCompare :: ExceptT a1 a2 a3 -> ExceptT a1 a2 a3 -> Union Ordering Source # | |
(SymOrd1 m, SymOrd a) => SymOrd (IdentityT m a) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: IdentityT m a -> IdentityT m a -> SymBool Source # (.<=) :: IdentityT m a -> IdentityT m a -> SymBool Source # (.>) :: IdentityT m a -> IdentityT m a -> SymBool Source # (.>=) :: IdentityT m a -> IdentityT m a -> SymBool Source # symCompare :: IdentityT m a -> IdentityT m a -> Union Ordering Source # | |
(SymOrd a1, SymOrd1 a2, SymOrd a3) => SymOrd (WriterT a1 a2 a3) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # (.<=) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # (.>) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # (.>=) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # symCompare :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> Union Ordering Source # | |
(SymOrd a1, SymOrd1 a2, SymOrd a3) => SymOrd (WriterT a1 a2 a3) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # (.<=) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # (.>) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # (.>=) :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> SymBool Source # symCompare :: WriterT a1 a2 a3 -> WriterT a1 a2 a3 -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3) => SymOrd (a1, a2, a3) Source # | |
(SymOrd (l a), SymOrd (r a)) => SymOrd (Product l r a) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: Product l r a -> Product l r a -> SymBool Source # (.<=) :: Product l r a -> Product l r a -> SymBool Source # (.>) :: Product l r a -> Product l r a -> SymBool Source # (.>=) :: Product l r a -> Product l r a -> SymBool Source # symCompare :: Product l r a -> Product l r a -> Union Ordering Source # | |
(SymOrd (l a), SymOrd (r a)) => SymOrd (Sum l r a) Source # | |
(SymOrd (f p), SymOrd (g p)) => SymOrd ((f :*: g) p) Source # | |
(SymOrd (f p), SymOrd (g p)) => SymOrd ((f :+: g) p) Source # | |
SymOrd c => SymOrd (K1 i c p) Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4) => SymOrd (a1, a2, a3, a4) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4) -> (a1, a2, a3, a4) -> SymBool Source # (.<=) :: (a1, a2, a3, a4) -> (a1, a2, a3, a4) -> SymBool Source # (.>) :: (a1, a2, a3, a4) -> (a1, a2, a3, a4) -> SymBool Source # (.>=) :: (a1, a2, a3, a4) -> (a1, a2, a3, a4) -> SymBool Source # symCompare :: (a1, a2, a3, a4) -> (a1, a2, a3, a4) -> Union Ordering Source # | |
SymOrd (f (g a)) => SymOrd (Compose f g a) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: Compose f g a -> Compose f g a -> SymBool Source # (.<=) :: Compose f g a -> Compose f g a -> SymBool Source # (.>) :: Compose f g a -> Compose f g a -> SymBool Source # (.>=) :: Compose f g a -> Compose f g a -> SymBool Source # symCompare :: Compose f g a -> Compose f g a -> Union Ordering Source # | |
SymOrd (f (g p)) => SymOrd ((f :.: g) p) Source # | |
SymOrd (f p) => SymOrd (M1 i c f p) Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5) => SymOrd (a1, a2, a3, a4, a5) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5) -> (a1, a2, a3, a4, a5) -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5, SymOrd a6) => SymOrd (a1, a2, a3, a4, a5, a6) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5, a6) -> (a1, a2, a3, a4, a5, a6) -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5, SymOrd a6, SymOrd a7) => SymOrd (a1, a2, a3, a4, a5, a6, a7) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5, a6, a7) -> (a1, a2, a3, a4, a5, a6, a7) -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5, SymOrd a6, SymOrd a7, SymOrd a8) => SymOrd (a1, a2, a3, a4, a5, a6, a7, a8) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5, a6, a7, a8) -> (a1, a2, a3, a4, a5, a6, a7, a8) -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5, SymOrd a6, SymOrd a7, SymOrd a8, SymOrd a9) => SymOrd (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5, SymOrd a6, SymOrd a7, SymOrd a8, SymOrd a9, SymOrd a10) => SymOrd (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5, SymOrd a6, SymOrd a7, SymOrd a8, SymOrd a9, SymOrd a10, SymOrd a11) => SymOrd (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5, SymOrd a6, SymOrd a7, SymOrd a8, SymOrd a9, SymOrd a10, SymOrd a11, SymOrd a12) => SymOrd (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5, SymOrd a6, SymOrd a7, SymOrd a8, SymOrd a9, SymOrd a10, SymOrd a11, SymOrd a12, SymOrd a13) => SymOrd (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5, SymOrd a6, SymOrd a7, SymOrd a8, SymOrd a9, SymOrd a10, SymOrd a11, SymOrd a12, SymOrd a13, SymOrd a14) => SymOrd (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> Union Ordering Source # | |
(SymOrd a1, SymOrd a2, SymOrd a3, SymOrd a4, SymOrd a5, SymOrd a6, SymOrd a7, SymOrd a8, SymOrd a9, SymOrd a10, SymOrd a11, SymOrd a12, SymOrd a13, SymOrd a14, SymOrd a15) => SymOrd (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source # | |
Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd (.<) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> SymBool Source # (.<=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> SymBool Source # (.>) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> SymBool Source # (.>=) :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> SymBool Source # symCompare :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> Union Ordering Source # |
class (SymEq1 f, forall a. SymOrd a => SymOrd (f a)) => SymOrd1 f where Source #
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.
liftSymCompare :: (a -> b -> Union Ordering) -> f a -> f b -> Union Ordering Source #
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.
Instances
symCompare1 :: (SymOrd1 f, SymOrd a) => f a -> f a -> Union Ordering Source #
Lift the standard symCompare
function to binary type constructors.
class (SymEq2 f, forall a. SymOrd a => SymOrd1 (f a)) => SymOrd2 f where Source #
Lifting of the SymOrd
class to binary type constructors.
liftSymCompare2 :: (a -> b -> Union Ordering) -> (c -> d -> Union Ordering) -> f a c -> f b d -> Union Ordering Source #
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.
Instances
symCompare2 :: (SymOrd2 f, SymOrd a, SymOrd b) => f a b -> f a b -> Union Ordering Source #
Lift the standard symCompare
function through the type constructors.
Min and max
mrgMax :: (SymOrd a, Mergeable a, SymBranching m, Applicative m) => a -> a -> m a Source #
Symbolic maximum, with a union-like monad.
mrgMin :: (SymOrd a, Mergeable a, SymBranching m, Applicative m) => a -> a -> m a Source #
Symbolic minimum, with a union-like monad.
Generic SymOrd
data family SymOrdArgs arity a b :: Type Source #
The arguments to the generic comparison function.
Instances
data SymOrdArgs Arity0 _ _1 Source # | |
newtype SymOrdArgs Arity1 a b Source # | |
class GSymOrd arity f where Source #
The class of types that can be generically symbolically compared.
gsymCompare :: SymOrdArgs arity a b -> f a -> f b -> Union Ordering Source #
Instances
genericSymCompare :: (Generic a, GSymOrd Arity0 (Rep a)) => a -> a -> Union Ordering Source #
Generic symCompare
function.