| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Grisette.Core.Data.Class.Integer
Contents
Description
Synopsis
- data ArithException
- class SignedDivMod a where
- divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- class UnsignedDivMod a where
- udivs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- umods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- class SignedQuotRem a where
- quots :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- rems :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a
- class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a
Symbolic integer operations
data ArithException #
Arithmetic exceptions.
Constructors
| Overflow | |
| Underflow | |
| LossOfPrecision | |
| DivideByZero | |
| Denormal | |
| RatioZeroDenominator | Since: base-4.6.0.0 |
Instances
class SignedDivMod a where Source #
Safe signed div and mod with monadic error handling in multi-path
execution. These procedures show throw DivideByZero exception when the
divisor is zero. The result should be able to handle errors with
MonadError, and the error type should be compatible with ArithException
(see TransformError for more details).
Methods
divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
Safe signed div with monadic error handling in multi-path execution.
>>>divs (ssym "a") (ssym "b") :: ExceptT AssertionError UnionM SymIntegerExceptT {If (= b 0) (Left AssertionError) (Right (div a b))}
mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
Safe signed mod with monadic error handling in multi-path execution.
>>>mods (ssym "a") (ssym "b") :: ExceptT AssertionError UnionM SymIntegerExceptT {If (= b 0) (Left AssertionError) (Right (mod a b))}
Instances
| SignedDivMod (Sym Integer) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim Methods divs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => Sym Integer -> Sym Integer -> uf (Sym Integer) Source # mods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => Sym Integer -> Sym Integer -> uf (Sym Integer) Source # | |
class UnsignedDivMod a where Source #
Safe unsigned div and mod with monadic error handling in multi-path
execution. These procedures show throw DivideByZero exception when the
divisor is zero. The result should be able to handle errors with
MonadError, and the error type should be compatible with ArithException
(see TransformError for more details).
Methods
udivs :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
umods :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
class SignedQuotRem a where Source #
Safe signed quot and rem with monadic error handling in multi-path
execution. These procedures show throw DivideByZero exception when the
divisor is zero. The result should be able to handle errors with
MonadError, and the error type should be compatible with ArithException
(see TransformError for more details).
Methods
quots :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
rems :: (MonadError e uf, MonadUnion uf, TransformError ArithException e) => a -> a -> uf a Source #
class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a Source #
Aggregation for the operations on symbolic integer types
Instances
| SymIntegerOp (Sym Integer) Source # | |
Defined in Grisette.IR.SymPrim.Data.SymPrim | |