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	Trustworthy
Language	Haskell2010

Grisette.Internal.Core.Data.Class.SafeDivision

Description

Synopsis

data ArithException
- = Overflow
- | Underflow
- | DivideByZero
class (MonadError e m, TryMerge m, Mergeable a) => SafeDivision e a m where
- safeDiv :: a -> a -> m a
- safeMod :: a -> a -> m a
- safeDivMod :: a -> a -> m (a, a)
- safeQuot :: a -> a -> m a
- safeRem :: a -> a -> m a
- safeQuotRem :: a -> a -> m (a, a)

Documentation

data ArithException #

Arithmetic exceptions.

Constructors

Overflow
Underflow
DivideByZero

Instances

Instances details

Exception ArithException	Since: base-4.0.0.0
Instance details Defined in GHC.Exception.Type Methods toException :: ArithException -> SomeException # fromException :: SomeException -> Maybe ArithException # displayException :: ArithException -> String #
Show ArithException	Since: base-4.0.0.0
Instance details Defined in GHC.Exception.Type Methods showsPrec :: Int -> ArithException -> ShowS # show :: ArithException -> String # showList :: [ArithException] -> ShowS #
Eq ArithException	Since: base-3.0
Instance details Defined in GHC.Exception.Type Methods (==) :: ArithException -> ArithException -> Bool # (/=) :: ArithException -> ArithException -> Bool #
Ord ArithException	Since: base-3.0
Instance details Defined in GHC.Exception.Type Methods compare :: ArithException -> ArithException -> Ordering # (<) :: ArithException -> ArithException -> Bool # (<=) :: ArithException -> ArithException -> Bool # (>) :: ArithException -> ArithException -> Bool # (>=) :: ArithException -> ArithException -> Bool # max :: ArithException -> ArithException -> ArithException # min :: ArithException -> ArithException -> ArithException #
Mergeable ArithException Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Mergeable Methods rootStrategy :: MergingStrategy ArithException Source #
TransformError ArithException AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.Error Methods transformError :: ArithException -> AssertionError Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Int16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Int16 -> Int16 -> m Int16 Source # safeMod :: Int16 -> Int16 -> m Int16 Source # safeDivMod :: Int16 -> Int16 -> m (Int16, Int16) Source # safeQuot :: Int16 -> Int16 -> m Int16 Source # safeRem :: Int16 -> Int16 -> m Int16 Source # safeQuotRem :: Int16 -> Int16 -> m (Int16, Int16) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Int32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Int32 -> Int32 -> m Int32 Source # safeMod :: Int32 -> Int32 -> m Int32 Source # safeDivMod :: Int32 -> Int32 -> m (Int32, Int32) Source # safeQuot :: Int32 -> Int32 -> m Int32 Source # safeRem :: Int32 -> Int32 -> m Int32 Source # safeQuotRem :: Int32 -> Int32 -> m (Int32, Int32) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Int64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Int64 -> Int64 -> m Int64 Source # safeMod :: Int64 -> Int64 -> m Int64 Source # safeDivMod :: Int64 -> Int64 -> m (Int64, Int64) Source # safeQuot :: Int64 -> Int64 -> m Int64 Source # safeRem :: Int64 -> Int64 -> m Int64 Source # safeQuotRem :: Int64 -> Int64 -> m (Int64, Int64) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Int8 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Int8 -> Int8 -> m Int8 Source # safeMod :: Int8 -> Int8 -> m Int8 Source # safeDivMod :: Int8 -> Int8 -> m (Int8, Int8) Source # safeQuot :: Int8 -> Int8 -> m Int8 Source # safeRem :: Int8 -> Int8 -> m Int8 Source # safeQuotRem :: Int8 -> Int8 -> m (Int8, Int8) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Word16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Word16 -> Word16 -> m Word16 Source # safeMod :: Word16 -> Word16 -> m Word16 Source # safeDivMod :: Word16 -> Word16 -> m (Word16, Word16) Source # safeQuot :: Word16 -> Word16 -> m Word16 Source # safeRem :: Word16 -> Word16 -> m Word16 Source # safeQuotRem :: Word16 -> Word16 -> m (Word16, Word16) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Word32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Word32 -> Word32 -> m Word32 Source # safeMod :: Word32 -> Word32 -> m Word32 Source # safeDivMod :: Word32 -> Word32 -> m (Word32, Word32) Source # safeQuot :: Word32 -> Word32 -> m Word32 Source # safeRem :: Word32 -> Word32 -> m Word32 Source # safeQuotRem :: Word32 -> Word32 -> m (Word32, Word32) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Word64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Word64 -> Word64 -> m Word64 Source # safeMod :: Word64 -> Word64 -> m Word64 Source # safeDivMod :: Word64 -> Word64 -> m (Word64, Word64) Source # safeQuot :: Word64 -> Word64 -> m Word64 Source # safeRem :: Word64 -> Word64 -> m Word64 Source # safeQuotRem :: Word64 -> Word64 -> m (Word64, Word64) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Word8 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Word8 -> Word8 -> m Word8 Source # safeMod :: Word8 -> Word8 -> m Word8 Source # safeDivMod :: Word8 -> Word8 -> m (Word8, Word8) Source # safeQuot :: Word8 -> Word8 -> m Word8 Source # safeRem :: Word8 -> Word8 -> m Word8 Source # safeQuotRem :: Word8 -> Word8 -> m (Word8, Word8) Source #
(MonadUnion m, MonadError ArithException m) => SafeDivision ArithException SymInteger m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: SymInteger -> SymInteger -> m SymInteger Source # safeMod :: SymInteger -> SymInteger -> m SymInteger Source # safeDivMod :: SymInteger -> SymInteger -> m (SymInteger, SymInteger) Source # safeQuot :: SymInteger -> SymInteger -> m SymInteger Source # safeRem :: SymInteger -> SymInteger -> m SymInteger Source # safeQuotRem :: SymInteger -> SymInteger -> m (SymInteger, SymInteger) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Integer m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Integer -> Integer -> m Integer Source # safeMod :: Integer -> Integer -> m Integer Source # safeDivMod :: Integer -> Integer -> m (Integer, Integer) Source # safeQuot :: Integer -> Integer -> m Integer Source # safeRem :: Integer -> Integer -> m Integer Source # safeQuotRem :: Integer -> Integer -> m (Integer, Integer) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Int m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Int -> Int -> m Int Source # safeMod :: Int -> Int -> m Int Source # safeDivMod :: Int -> Int -> m (Int, Int) Source # safeQuot :: Int -> Int -> m Int Source # safeRem :: Int -> Int -> m Int Source # safeQuotRem :: Int -> Int -> m (Int, Int) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Word m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Word -> Word -> m Word Source # safeMod :: Word -> Word -> m Word Source # safeDivMod :: Word -> Word -> m (Word, Word) Source # safeQuot :: Word -> Word -> m Word Source # safeRem :: Word -> Word -> m Word Source # safeQuotRem :: Word -> Word -> m (Word, Word) Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Int16 -> Int16 -> m Int16 Source # safeNeg :: Int16 -> m Int16 Source # safeSub :: Int16 -> Int16 -> m Int16 Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Int32 -> Int32 -> m Int32 Source # safeNeg :: Int32 -> m Int32 Source # safeSub :: Int32 -> Int32 -> m Int32 Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Int64 -> Int64 -> m Int64 Source # safeNeg :: Int64 -> m Int64 Source # safeSub :: Int64 -> Int64 -> m Int64 Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int8 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Int8 -> Int8 -> m Int8 Source # safeNeg :: Int8 -> m Int8 Source # safeSub :: Int8 -> Int8 -> m Int8 Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Word16 -> Word16 -> m Word16 Source # safeNeg :: Word16 -> m Word16 Source # safeSub :: Word16 -> Word16 -> m Word16 Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Word32 -> Word32 -> m Word32 Source # safeNeg :: Word32 -> m Word32 Source # safeSub :: Word32 -> Word32 -> m Word32 Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Word64 -> Word64 -> m Word64 Source # safeNeg :: Word64 -> m Word64 Source # safeSub :: Word64 -> Word64 -> m Word64 Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word8 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Word8 -> Word8 -> m Word8 Source # safeNeg :: Word8 -> m Word8 Source # safeSub :: Word8 -> Word8 -> m Word8 Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException SymInteger m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: SymInteger -> SymInteger -> m SymInteger Source # safeNeg :: SymInteger -> m SymInteger Source # safeSub :: SymInteger -> SymInteger -> m SymInteger Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Integer m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Integer -> Integer -> m Integer Source # safeNeg :: Integer -> m Integer Source # safeSub :: Integer -> Integer -> m Integer Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Int m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Int -> Int -> m Int Source # safeNeg :: Int -> m Int Source # safeSub :: Int -> Int -> m Int Source #
(MonadError ArithException m, TryMerge m) => SafeLinearArith ArithException Word m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: Word -> Word -> m Word Source # safeNeg :: Word -> m Word Source # safeSub :: Word -> Word -> m Word Source #
(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Int16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: Int16 -> Int16 -> m Int16 Source # safeSymRotateR :: Int16 -> Int16 -> m Int16 Source #
(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Int32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: Int32 -> Int32 -> m Int32 Source # safeSymRotateR :: Int32 -> Int32 -> m Int32 Source #
(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Int64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: Int64 -> Int64 -> m Int64 Source # safeSymRotateR :: Int64 -> Int64 -> m Int64 Source #
(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Int8 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: Int8 -> Int8 -> m Int8 Source # safeSymRotateR :: Int8 -> Int8 -> m Int8 Source #
(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Word16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: Word16 -> Word16 -> m Word16 Source # safeSymRotateR :: Word16 -> Word16 -> m Word16 Source #
(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Word32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: Word32 -> Word32 -> m Word32 Source # safeSymRotateR :: Word32 -> Word32 -> m Word32 Source #
(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Word64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: Word64 -> Word64 -> m Word64 Source # safeSymRotateR :: Word64 -> Word64 -> m Word64 Source #
(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Word8 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: Word8 -> Word8 -> m Word8 Source # safeSymRotateR :: Word8 -> Word8 -> m Word8 Source #
(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Int m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: Int -> Int -> m Int Source # safeSymRotateR :: Int -> Int -> m Int Source #
(MonadError ArithException m, TryMerge m) => SafeSymRotate ArithException Word m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: Word -> Word -> m Word Source # safeSymRotateR :: Word -> Word -> m Word Source #
(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Int16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: Int16 -> Int16 -> m Int16 Source # safeSymShiftR :: Int16 -> Int16 -> m Int16 Source # safeSymStrictShiftL :: Int16 -> Int16 -> m Int16 Source # safeSymStrictShiftR :: Int16 -> Int16 -> m Int16 Source #
(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Int32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: Int32 -> Int32 -> m Int32 Source # safeSymShiftR :: Int32 -> Int32 -> m Int32 Source # safeSymStrictShiftL :: Int32 -> Int32 -> m Int32 Source # safeSymStrictShiftR :: Int32 -> Int32 -> m Int32 Source #
(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Int64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: Int64 -> Int64 -> m Int64 Source # safeSymShiftR :: Int64 -> Int64 -> m Int64 Source # safeSymStrictShiftL :: Int64 -> Int64 -> m Int64 Source # safeSymStrictShiftR :: Int64 -> Int64 -> m Int64 Source #
(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Int8 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: Int8 -> Int8 -> m Int8 Source # safeSymShiftR :: Int8 -> Int8 -> m Int8 Source # safeSymStrictShiftL :: Int8 -> Int8 -> m Int8 Source # safeSymStrictShiftR :: Int8 -> Int8 -> m Int8 Source #
(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Word16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: Word16 -> Word16 -> m Word16 Source # safeSymShiftR :: Word16 -> Word16 -> m Word16 Source # safeSymStrictShiftL :: Word16 -> Word16 -> m Word16 Source # safeSymStrictShiftR :: Word16 -> Word16 -> m Word16 Source #
(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Word32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: Word32 -> Word32 -> m Word32 Source # safeSymShiftR :: Word32 -> Word32 -> m Word32 Source # safeSymStrictShiftL :: Word32 -> Word32 -> m Word32 Source # safeSymStrictShiftR :: Word32 -> Word32 -> m Word32 Source #
(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Word64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: Word64 -> Word64 -> m Word64 Source # safeSymShiftR :: Word64 -> Word64 -> m Word64 Source # safeSymStrictShiftL :: Word64 -> Word64 -> m Word64 Source # safeSymStrictShiftR :: Word64 -> Word64 -> m Word64 Source #
(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Word8 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: Word8 -> Word8 -> m Word8 Source # safeSymShiftR :: Word8 -> Word8 -> m Word8 Source # safeSymStrictShiftL :: Word8 -> Word8 -> m Word8 Source # safeSymStrictShiftR :: Word8 -> Word8 -> m Word8 Source #
(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Int m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: Int -> Int -> m Int Source # safeSymShiftR :: Int -> Int -> m Int Source # safeSymStrictShiftL :: Int -> Int -> m Int Source # safeSymStrictShiftR :: Int -> Int -> m Int Source #
(MonadError ArithException m, TryMerge m) => SafeSymShift ArithException Word m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: Word -> Word -> m Word Source # safeSymShiftR :: Word -> Word -> m Word Source # safeSymStrictShiftL :: Word -> Word -> m Word Source # safeSymStrictShiftR :: Word -> Word -> m Word Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDivision ArithException (IntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: IntN n -> IntN n -> m (IntN n) Source # safeMod :: IntN n -> IntN n -> m (IntN n) Source # safeDivMod :: IntN n -> IntN n -> m (IntN n, IntN n) Source # safeQuot :: IntN n -> IntN n -> m (IntN n) Source # safeRem :: IntN n -> IntN n -> m (IntN n) Source # safeQuotRem :: IntN n -> IntN n -> m (IntN n, IntN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDivision ArithException (WordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: WordN n -> WordN n -> m (WordN n) Source # safeMod :: WordN n -> WordN n -> m (WordN n) Source # safeDivMod :: WordN n -> WordN n -> m (WordN n, WordN n) Source # safeQuot :: WordN n -> WordN n -> m (WordN n) Source # safeRem :: WordN n -> WordN n -> m (WordN n) Source # safeQuotRem :: WordN n -> WordN n -> m (WordN n, WordN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDivision ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeMod :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeDivMod :: SymIntN n -> SymIntN n -> m (SymIntN n, SymIntN n) Source # safeQuot :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeRem :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeQuotRem :: SymIntN n -> SymIntN n -> m (SymIntN n, SymIntN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDivision ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeMod :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeDivMod :: SymWordN n -> SymWordN n -> m (SymWordN n, SymWordN n) Source # safeQuot :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeRem :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeQuotRem :: SymWordN n -> SymWordN n -> m (SymWordN n, SymWordN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (IntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: IntN n -> IntN n -> m (IntN n) Source # safeNeg :: IntN n -> m (IntN n) Source # safeSub :: IntN n -> IntN n -> m (IntN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (WordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: WordN n -> WordN n -> m (WordN n) Source # safeNeg :: WordN n -> m (WordN n) Source # safeSub :: WordN n -> WordN n -> m (WordN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeNeg :: SymIntN n -> m (SymIntN n) Source # safeSub :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeLinearArith Methods safeAdd :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeNeg :: SymWordN n -> m (SymWordN n) Source # safeSub :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (IntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: IntN n -> IntN n -> m (IntN n) Source # safeSymRotateR :: IntN n -> IntN n -> m (IntN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (WordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: WordN n -> WordN n -> m (WordN n) Source # safeSymRotateR :: WordN n -> WordN n -> m (WordN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymRotateR :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymRotate ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymRotate Methods safeSymRotateL :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymRotateR :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (IntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: IntN n -> IntN n -> m (IntN n) Source # safeSymShiftR :: IntN n -> IntN n -> m (IntN n) Source # safeSymStrictShiftL :: IntN n -> IntN n -> m (IntN n) Source # safeSymStrictShiftR :: IntN n -> IntN n -> m (IntN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeSymShift ArithException (WordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: WordN n -> WordN n -> m (WordN n) Source # safeSymShiftR :: WordN n -> WordN n -> m (WordN n) Source # safeSymStrictShiftL :: WordN n -> WordN n -> m (WordN n) Source # safeSymStrictShiftR :: WordN n -> WordN n -> m (WordN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymShift ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymShiftR :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymStrictShiftL :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeSymStrictShiftR :: SymIntN n -> SymIntN n -> m (SymIntN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeSymShift ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeSymShift Methods safeSymShiftL :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymShiftR :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymStrictShiftL :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeSymStrictShiftR :: SymWordN n -> SymWordN n -> m (SymWordN n) Source #

class (MonadError e m, TryMerge m, Mergeable a) => SafeDivision e a m where Source #

Safe division with monadic error handling in multi-path execution. These procedures throw an exception when the divisor is zero. The result should be able to handle errors with MonadError.

Minimal complete definition

(safeDiv, safeMod | safeDivMod), (safeQuot, safeRem | safeQuotRem)

Methods

safeDiv :: a -> a -> m a Source #

Safe signed div with monadic error handling in multi-path execution.

>>> safeDiv (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger
ExceptT {If (= b 0) (Left divide by zero) (Right (div a b))}

safeMod :: a -> a -> m a Source #

Safe signed mod with monadic error handling in multi-path execution.

>>> safeMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger
ExceptT {If (= b 0) (Left divide by zero) (Right (mod a b))}

safeDivMod :: a -> a -> m (a, a) Source #

Safe signed divMod with monadic error handling in multi-path execution.

>>> safeDivMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymInteger, SymInteger)
ExceptT {If (= b 0) (Left divide by zero) (Right ((div a b),(mod a b)))}

safeQuot :: a -> a -> m a Source #

Safe signed quot with monadic error handling in multi-path execution.

safeRem :: a -> a -> m a Source #

Safe signed rem with monadic error handling in multi-path execution.

safeQuotRem :: a -> a -> m (a, a) Source #

Safe signed quotRem with monadic error handling in multi-path execution.

Instances

Instances details

(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Int16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Int16 -> Int16 -> m Int16 Source # safeMod :: Int16 -> Int16 -> m Int16 Source # safeDivMod :: Int16 -> Int16 -> m (Int16, Int16) Source # safeQuot :: Int16 -> Int16 -> m Int16 Source # safeRem :: Int16 -> Int16 -> m Int16 Source # safeQuotRem :: Int16 -> Int16 -> m (Int16, Int16) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Int32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Int32 -> Int32 -> m Int32 Source # safeMod :: Int32 -> Int32 -> m Int32 Source # safeDivMod :: Int32 -> Int32 -> m (Int32, Int32) Source # safeQuot :: Int32 -> Int32 -> m Int32 Source # safeRem :: Int32 -> Int32 -> m Int32 Source # safeQuotRem :: Int32 -> Int32 -> m (Int32, Int32) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Int64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Int64 -> Int64 -> m Int64 Source # safeMod :: Int64 -> Int64 -> m Int64 Source # safeDivMod :: Int64 -> Int64 -> m (Int64, Int64) Source # safeQuot :: Int64 -> Int64 -> m Int64 Source # safeRem :: Int64 -> Int64 -> m Int64 Source # safeQuotRem :: Int64 -> Int64 -> m (Int64, Int64) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Int8 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Int8 -> Int8 -> m Int8 Source # safeMod :: Int8 -> Int8 -> m Int8 Source # safeDivMod :: Int8 -> Int8 -> m (Int8, Int8) Source # safeQuot :: Int8 -> Int8 -> m Int8 Source # safeRem :: Int8 -> Int8 -> m Int8 Source # safeQuotRem :: Int8 -> Int8 -> m (Int8, Int8) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Word16 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Word16 -> Word16 -> m Word16 Source # safeMod :: Word16 -> Word16 -> m Word16 Source # safeDivMod :: Word16 -> Word16 -> m (Word16, Word16) Source # safeQuot :: Word16 -> Word16 -> m Word16 Source # safeRem :: Word16 -> Word16 -> m Word16 Source # safeQuotRem :: Word16 -> Word16 -> m (Word16, Word16) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Word32 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Word32 -> Word32 -> m Word32 Source # safeMod :: Word32 -> Word32 -> m Word32 Source # safeDivMod :: Word32 -> Word32 -> m (Word32, Word32) Source # safeQuot :: Word32 -> Word32 -> m Word32 Source # safeRem :: Word32 -> Word32 -> m Word32 Source # safeQuotRem :: Word32 -> Word32 -> m (Word32, Word32) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Word64 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Word64 -> Word64 -> m Word64 Source # safeMod :: Word64 -> Word64 -> m Word64 Source # safeDivMod :: Word64 -> Word64 -> m (Word64, Word64) Source # safeQuot :: Word64 -> Word64 -> m Word64 Source # safeRem :: Word64 -> Word64 -> m Word64 Source # safeQuotRem :: Word64 -> Word64 -> m (Word64, Word64) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Word8 m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Word8 -> Word8 -> m Word8 Source # safeMod :: Word8 -> Word8 -> m Word8 Source # safeDivMod :: Word8 -> Word8 -> m (Word8, Word8) Source # safeQuot :: Word8 -> Word8 -> m Word8 Source # safeRem :: Word8 -> Word8 -> m Word8 Source # safeQuotRem :: Word8 -> Word8 -> m (Word8, Word8) Source #
(MonadUnion m, MonadError ArithException m) => SafeDivision ArithException SymInteger m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: SymInteger -> SymInteger -> m SymInteger Source # safeMod :: SymInteger -> SymInteger -> m SymInteger Source # safeDivMod :: SymInteger -> SymInteger -> m (SymInteger, SymInteger) Source # safeQuot :: SymInteger -> SymInteger -> m SymInteger Source # safeRem :: SymInteger -> SymInteger -> m SymInteger Source # safeQuotRem :: SymInteger -> SymInteger -> m (SymInteger, SymInteger) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Integer m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Integer -> Integer -> m Integer Source # safeMod :: Integer -> Integer -> m Integer Source # safeDivMod :: Integer -> Integer -> m (Integer, Integer) Source # safeQuot :: Integer -> Integer -> m Integer Source # safeRem :: Integer -> Integer -> m Integer Source # safeQuotRem :: Integer -> Integer -> m (Integer, Integer) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Int m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Int -> Int -> m Int Source # safeMod :: Int -> Int -> m Int Source # safeDivMod :: Int -> Int -> m (Int, Int) Source # safeQuot :: Int -> Int -> m Int Source # safeRem :: Int -> Int -> m Int Source # safeQuotRem :: Int -> Int -> m (Int, Int) Source #
(MonadError ArithException m, TryMerge m) => SafeDivision ArithException Word m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: Word -> Word -> m Word Source # safeMod :: Word -> Word -> m Word Source # safeDivMod :: Word -> Word -> m (Word, Word) Source # safeQuot :: Word -> Word -> m Word Source # safeRem :: Word -> Word -> m Word Source # safeQuotRem :: Word -> Word -> m (Word, Word) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDivision ArithException (IntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: IntN n -> IntN n -> m (IntN n) Source # safeMod :: IntN n -> IntN n -> m (IntN n) Source # safeDivMod :: IntN n -> IntN n -> m (IntN n, IntN n) Source # safeQuot :: IntN n -> IntN n -> m (IntN n) Source # safeRem :: IntN n -> IntN n -> m (IntN n) Source # safeQuotRem :: IntN n -> IntN n -> m (IntN n, IntN n) Source #
(MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) => SafeDivision ArithException (WordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: WordN n -> WordN n -> m (WordN n) Source # safeMod :: WordN n -> WordN n -> m (WordN n) Source # safeDivMod :: WordN n -> WordN n -> m (WordN n, WordN n) Source # safeQuot :: WordN n -> WordN n -> m (WordN n) Source # safeRem :: WordN n -> WordN n -> m (WordN n) Source # safeQuotRem :: WordN n -> WordN n -> m (WordN n, WordN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDivision ArithException (SymIntN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeMod :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeDivMod :: SymIntN n -> SymIntN n -> m (SymIntN n, SymIntN n) Source # safeQuot :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeRem :: SymIntN n -> SymIntN n -> m (SymIntN n) Source # safeQuotRem :: SymIntN n -> SymIntN n -> m (SymIntN n, SymIntN n) Source #
(MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) => SafeDivision ArithException (SymWordN n) m Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SafeDivision Methods safeDiv :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeMod :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeDivMod :: SymWordN n -> SymWordN n -> m (SymWordN n, SymWordN n) Source # safeQuot :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeRem :: SymWordN n -> SymWordN n -> m (SymWordN n) Source # safeQuotRem :: SymWordN n -> SymWordN n -> m (SymWordN n, SymWordN n) Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SafeDivision e (bv n) (ExceptT e m), MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e) => SafeDivision (Either BitwidthMismatch e) (SomeBV bv) m Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods safeDiv :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeDivMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv) Source # safeQuot :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv) Source # safeQuotRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv) Source #