{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Core.Data.Class.SafeLinearArith
( ArithException (..),
SafeLinearArith (..),
)
where
import Control.Exception (ArithException (DivideByZero, Overflow, Underflow))
import Control.Monad.Except (MonadError (throwError))
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, sameNat, type (<=))
import Grisette.Core.Control.Monad.Union (MonadUnion)
import Grisette.Core.Data.BV
( BitwidthMismatch (BitwidthMismatch),
IntN,
SomeIntN (SomeIntN),
SomeWordN (SomeWordN),
WordN,
)
import Grisette.Core.Data.Class.LogicalOp
( LogicalOp ((.&&), (.||)),
)
import Grisette.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Core.Data.Class.SEq (SEq ((./=), (.==)))
import Grisette.Core.Data.Class.SOrd (SOrd ((.<), (.>), (.>=)))
import Grisette.Core.Data.Class.SimpleMergeable
( merge,
mrgIf,
mrgSingle,
)
import Grisette.Core.Data.Class.Solvable (Solvable (con))
import Grisette.IR.SymPrim.Data.SymPrim
( SymIntN,
SymInteger,
SymWordN,
)
class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeLinearArith e a | a -> e where
safeAdd :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
safeNeg :: (MonadError e uf, MonadUnion uf) => a -> uf a
safeMinus :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> uf a
safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
instance SafeLinearArith ArithException Integer where
safeAdd :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
Integer -> Integer -> uf Integer
safeAdd Integer
l Integer
r = Integer -> uf Integer
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
r)
safeNeg :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
Integer -> uf Integer
safeNeg Integer
l = Integer -> uf Integer
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (-Integer
l)
safeMinus :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
Integer -> Integer -> uf Integer
safeMinus Integer
l Integer
r = Integer -> uf Integer
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
r)
safeAdd' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> Integer -> Integer -> uf Integer
safeAdd' ArithException -> e'
_ Integer
l Integer
r = Integer -> uf Integer
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
r)
safeNeg' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> Integer -> uf Integer
safeNeg' ArithException -> e'
_ Integer
l = Integer -> uf Integer
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (-Integer
l)
safeMinus' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> Integer -> Integer -> uf Integer
safeMinus' ArithException -> e'
_ Integer
l Integer
r = Integer -> uf Integer
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
r)
#define SAFE_LINARITH_SIGNED_CONCRETE_BODY \
safeAdd l r = let res = l + r in \
mrgIf (con $ l > 0 && r > 0 && res < 0) \
(throwError Overflow) \
(mrgIf (con $ l < 0 && r < 0 && res >= 0) \
(throwError Underflow) \
(return res));\
safeAdd' t' l r = let res = l + r in \
mrgIf (con $ l > 0 && r > 0 && res < 0) \
(throwError (t' Overflow)) \
(mrgIf (con $ l < 0 && r < 0 && res >= 0) \
(throwError (t' Underflow)) \
(return res)); \
safeMinus l r = let res = l - r in \
mrgIf (con $ l >= 0 && r < 0 && res < 0) \
(throwError Overflow) \
(mrgIf (con $ l < 0 && r > 0 && res > 0) \
(throwError Underflow) \
(return res));\
safeMinus' t' l r = let res = l - r in \
mrgIf (con $ l >= 0 && r < 0 && res < 0) \
(throwError (t' Overflow)) \
(mrgIf (con $ l < 0 && r > 0 && res > 0) \
(throwError (t' Underflow)) \
(return res)); \
safeNeg v = mrgIf (con $ v == minBound) (throwError Overflow) (return $ -v);\
safeNeg' t' v = mrgIf (con $ v == minBound) (throwError (t' Overflow)) (return $ -v)
#define SAFE_LINARITH_SIGNED_CONCRETE(type) \
instance SafeLinearArith ArithException type where \
SAFE_LINARITH_SIGNED_CONCRETE_BODY
#define SAFE_LINARITH_SIGNED_BV_CONCRETE(type) \
instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (type n) where \
SAFE_LINARITH_SIGNED_CONCRETE_BODY
#define SAFE_LINARITH_UNSIGNED_CONCRETE_BODY \
safeAdd l r = let res = l + r in \
mrgIf (con $ l > res || r > res) \
(throwError Overflow) \
(return res);\
safeAdd' t' l r = let res = l + r in \
mrgIf (con $ l > res || r > res) \
(throwError (t' Overflow)) \
(return res); \
safeMinus l r = \
mrgIf (con $ r > l) \
(throwError Underflow) \
(return $ l - r);\
safeMinus' t' l r = \
mrgIf (con $ r > l) \
(throwError $ t' Underflow) \
(return $ l - r);\
safeNeg v = mrgIf (con $ v /= 0) (throwError Underflow) (return $ -v);\
safeNeg' t' v = mrgIf (con $ v /= 0) (throwError (t' Underflow)) (return $ -v)
#define SAFE_LINARITH_UNSIGNED_CONCRETE(type) \
instance SafeLinearArith ArithException type where \
SAFE_LINARITH_UNSIGNED_CONCRETE_BODY
#define SAFE_LINARITH_UNSIGNED_BV_CONCRETE(type) \
instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (type n) where \
SAFE_LINARITH_UNSIGNED_CONCRETE_BODY
#define SAFE_LINARITH_SOME_CONCRETE(type, ctype) \
instance SafeLinearArith (Either BitwidthMismatch ArithException) type where \
safeAdd (type (l :: ctype l)) (type (r :: ctype r)) = merge (\
case sameNat (Proxy @l) (Proxy @r) of \
Just Refl -> type <$> safeAdd' Right l r; \
_ -> throwError $ Left BitwidthMismatch); \
safeAdd' t (type (l :: ctype l)) (type (r :: ctype r)) = merge (\
case sameNat (Proxy @l) (Proxy @r) of \
Just Refl -> type <$> safeAdd' (t . Right) l r; \
_ -> let t' = t; _ = t' in throwError $ t' $ Left BitwidthMismatch); \
safeMinus (type (l :: ctype l)) (type (r :: ctype r)) = merge (\
case sameNat (Proxy @l) (Proxy @r) of \
Just Refl -> type <$> safeMinus' Right l r; \
_ -> throwError $ Left BitwidthMismatch); \
safeMinus' t (type (l :: ctype l)) (type (r :: ctype r)) = merge (\
case sameNat (Proxy @l) (Proxy @r) of \
Just Refl -> type <$> safeMinus' (t . Right) l r; \
_ -> let t' = t; _ = t' in throwError $ t' $ Left BitwidthMismatch); \
safeNeg (type l) = merge $ type <$> safeNeg' Right l; \
safeNeg' t (type l) = merge $ type <$> safeNeg' (t . Right) l
#if 1
SAFE_LINARITH_SIGNED_CONCRETE(Int8)
SAFE_LINARITH_SIGNED_CONCRETE(Int16)
SAFE_LINARITH_SIGNED_CONCRETE(Int32)
SAFE_LINARITH_SIGNED_CONCRETE(Int64)
SAFE_LINARITH_SIGNED_CONCRETE(Int)
SAFE_LINARITH_SIGNED_BV_CONCRETE(IntN)
SAFE_LINARITH_SOME_CONCRETE(SomeIntN, IntN)
SAFE_LINARITH_UNSIGNED_CONCRETE(Word8)
SAFE_LINARITH_UNSIGNED_CONCRETE(Word16)
SAFE_LINARITH_UNSIGNED_CONCRETE(Word32)
SAFE_LINARITH_UNSIGNED_CONCRETE(Word64)
SAFE_LINARITH_UNSIGNED_CONCRETE(Word)
SAFE_LINARITH_UNSIGNED_BV_CONCRETE(WordN)
SAFE_LINARITH_SOME_CONCRETE(SomeWordN, WordN)
#endif
instance SafeLinearArith ArithException SymInteger where
safeAdd :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymInteger -> SymInteger -> uf SymInteger
safeAdd SymInteger
ls SymInteger
rs = SymInteger -> uf SymInteger
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (SymInteger -> uf SymInteger) -> SymInteger -> uf SymInteger
forall a b. (a -> b) -> a -> b
$ SymInteger
ls SymInteger -> SymInteger -> SymInteger
forall a. Num a => a -> a -> a
+ SymInteger
rs
safeAdd' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger
safeAdd' ArithException -> e'
_ SymInteger
ls SymInteger
rs = SymInteger -> uf SymInteger
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (SymInteger -> uf SymInteger) -> SymInteger -> uf SymInteger
forall a b. (a -> b) -> a -> b
$ SymInteger
ls SymInteger -> SymInteger -> SymInteger
forall a. Num a => a -> a -> a
+ SymInteger
rs
safeNeg :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymInteger -> uf SymInteger
safeNeg SymInteger
v = SymInteger -> uf SymInteger
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (SymInteger -> uf SymInteger) -> SymInteger -> uf SymInteger
forall a b. (a -> b) -> a -> b
$ -SymInteger
v
safeNeg' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymInteger -> uf SymInteger
safeNeg' ArithException -> e'
_ SymInteger
v = SymInteger -> uf SymInteger
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (SymInteger -> uf SymInteger) -> SymInteger -> uf SymInteger
forall a b. (a -> b) -> a -> b
$ -SymInteger
v
safeMinus :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymInteger -> SymInteger -> uf SymInteger
safeMinus SymInteger
ls SymInteger
rs = SymInteger -> uf SymInteger
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (SymInteger -> uf SymInteger) -> SymInteger -> uf SymInteger
forall a b. (a -> b) -> a -> b
$ SymInteger
ls SymInteger -> SymInteger -> SymInteger
forall a. Num a => a -> a -> a
- SymInteger
rs
safeMinus' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymInteger -> SymInteger -> uf SymInteger
safeMinus' ArithException -> e'
_ SymInteger
ls SymInteger
rs = SymInteger -> uf SymInteger
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (SymInteger -> uf SymInteger) -> SymInteger -> uf SymInteger
forall a b. (a -> b) -> a -> b
$ SymInteger
ls SymInteger -> SymInteger -> SymInteger
forall a. Num a => a -> a -> a
- SymInteger
rs
instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymIntN n) where
safeAdd :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymIntN n -> SymIntN n -> uf (SymIntN n)
safeAdd SymIntN n
ls SymIntN n
rs =
SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymIntN n
0)
(SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
rs SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
res SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0) (ArithException -> uf (SymIntN n)
forall a. ArithException -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow) (SymIntN n -> uf (SymIntN n)
forall a. a -> uf a
forall (m :: * -> *) a. Monad m => a -> m a
return SymIntN n
res))
( SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
rs SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
res SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.>= SymIntN n
0)
(ArithException -> uf (SymIntN n)
forall a. ArithException -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Underflow)
(SymIntN n -> uf (SymIntN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle SymIntN n
res)
)
where
res :: SymIntN n
res = SymIntN n
ls SymIntN n -> SymIntN n -> SymIntN n
forall a. Num a => a -> a -> a
+ SymIntN n
rs
safeAdd' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n)
safeAdd' ArithException -> e'
f SymIntN n
ls SymIntN n
rs =
SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymIntN n
0)
(SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
rs SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
res SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0) (e' -> uf (SymIntN n)
forall a. e' -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e' -> uf (SymIntN n)) -> e' -> uf (SymIntN n)
forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Overflow) (SymIntN n -> uf (SymIntN n)
forall a. a -> uf a
forall (m :: * -> *) a. Monad m => a -> m a
return SymIntN n
res))
( SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
rs SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
res SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.>= SymIntN n
0)
(e' -> uf (SymIntN n)
forall a. e' -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e' -> uf (SymIntN n)) -> e' -> uf (SymIntN n)
forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Underflow)
(SymIntN n -> uf (SymIntN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle SymIntN n
res)
)
where
res :: SymIntN n
res = SymIntN n
ls SymIntN n -> SymIntN n -> SymIntN n
forall a. Num a => a -> a -> a
+ SymIntN n
rs
safeNeg :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymIntN n -> uf (SymIntN n)
safeNeg SymIntN n
v = SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
v SymIntN n -> SymIntN n -> SymBool
forall a. SEq a => a -> a -> SymBool
.== IntN n -> SymIntN n
forall c t. Solvable c t => c -> t
con IntN n
forall a. Bounded a => a
minBound) (ArithException -> uf (SymIntN n)
forall a. ArithException -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow) (SymIntN n -> uf (SymIntN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (SymIntN n -> uf (SymIntN n)) -> SymIntN n -> uf (SymIntN n)
forall a b. (a -> b) -> a -> b
$ -SymIntN n
v)
safeNeg' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymIntN n -> uf (SymIntN n)
safeNeg' ArithException -> e'
f SymIntN n
v = SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
v SymIntN n -> SymIntN n -> SymBool
forall a. SEq a => a -> a -> SymBool
.== IntN n -> SymIntN n
forall c t. Solvable c t => c -> t
con IntN n
forall a. Bounded a => a
minBound) (e' -> uf (SymIntN n)
forall a. e' -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e' -> uf (SymIntN n)) -> e' -> uf (SymIntN n)
forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Overflow) (SymIntN n -> uf (SymIntN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (SymIntN n -> uf (SymIntN n)) -> SymIntN n -> uf (SymIntN n)
forall a b. (a -> b) -> a -> b
$ -SymIntN n
v)
safeMinus :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymIntN n -> SymIntN n -> uf (SymIntN n)
safeMinus SymIntN n
ls SymIntN n
rs =
SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.>= SymIntN n
0)
(SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
rs SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
res SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0) (ArithException -> uf (SymIntN n)
forall a. ArithException -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow) (SymIntN n -> uf (SymIntN n)
forall a. a -> uf a
forall (m :: * -> *) a. Monad m => a -> m a
return SymIntN n
res))
( SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
rs SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
res SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymIntN n
0)
(ArithException -> uf (SymIntN n)
forall a. ArithException -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Underflow)
(SymIntN n -> uf (SymIntN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle SymIntN n
res)
)
where
res :: SymIntN n
res = SymIntN n
ls SymIntN n -> SymIntN n -> SymIntN n
forall a. Num a => a -> a -> a
- SymIntN n
rs
safeMinus' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymIntN n -> SymIntN n -> uf (SymIntN n)
safeMinus' ArithException -> e'
f SymIntN n
ls SymIntN n
rs =
SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.>= SymIntN n
0)
(SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymIntN n
rs SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
res SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0) (e' -> uf (SymIntN n)
forall a. e' -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e' -> uf (SymIntN n)) -> e' -> uf (SymIntN n)
forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Overflow) (SymIntN n -> uf (SymIntN n)
forall a. a -> uf a
forall (m :: * -> *) a. Monad m => a -> m a
return SymIntN n
res))
( SymBool -> uf (SymIntN n) -> uf (SymIntN n) -> uf (SymIntN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymIntN n
ls SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
rs SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
res SymIntN n -> SymIntN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymIntN n
0)
(e' -> uf (SymIntN n)
forall a. e' -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e' -> uf (SymIntN n)) -> e' -> uf (SymIntN n)
forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Underflow)
(SymIntN n -> uf (SymIntN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle SymIntN n
res)
)
where
res :: SymIntN n
res = SymIntN n
ls SymIntN n -> SymIntN n -> SymIntN n
forall a. Num a => a -> a -> a
- SymIntN n
rs
instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (SymWordN n) where
safeAdd :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymWordN n -> SymWordN n -> uf (SymWordN n)
safeAdd SymWordN n
ls SymWordN n
rs =
SymBool -> uf (SymWordN n) -> uf (SymWordN n) -> uf (SymWordN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymWordN n
ls SymWordN n -> SymWordN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymWordN n
res SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| SymWordN n
rs SymWordN n -> SymWordN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymWordN n
res)
(ArithException -> uf (SymWordN n)
forall a. ArithException -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow)
(SymWordN n -> uf (SymWordN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle SymWordN n
res)
where
res :: SymWordN n
res = SymWordN n
ls SymWordN n -> SymWordN n -> SymWordN n
forall a. Num a => a -> a -> a
+ SymWordN n
rs
safeAdd' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e')
-> SymWordN n -> SymWordN n -> uf (SymWordN n)
safeAdd' ArithException -> e'
f SymWordN n
ls SymWordN n
rs =
SymBool -> uf (SymWordN n) -> uf (SymWordN n) -> uf (SymWordN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymWordN n
ls SymWordN n -> SymWordN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymWordN n
res SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| SymWordN n
rs SymWordN n -> SymWordN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymWordN n
res)
(e' -> uf (SymWordN n)
forall a. e' -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e' -> uf (SymWordN n)) -> e' -> uf (SymWordN n)
forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Overflow)
(SymWordN n -> uf (SymWordN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle SymWordN n
res)
where
res :: SymWordN n
res = SymWordN n
ls SymWordN n -> SymWordN n -> SymWordN n
forall a. Num a => a -> a -> a
+ SymWordN n
rs
safeNeg :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymWordN n -> uf (SymWordN n)
safeNeg SymWordN n
v = SymBool -> uf (SymWordN n) -> uf (SymWordN n) -> uf (SymWordN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymWordN n
v SymWordN n -> SymWordN n -> SymBool
forall a. SEq a => a -> a -> SymBool
./= SymWordN n
0) (ArithException -> uf (SymWordN n)
forall a. ArithException -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Underflow) (SymWordN n -> uf (SymWordN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle SymWordN n
v)
safeNeg' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e') -> SymWordN n -> uf (SymWordN n)
safeNeg' ArithException -> e'
f SymWordN n
v = SymBool -> uf (SymWordN n) -> uf (SymWordN n) -> uf (SymWordN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf (SymWordN n
v SymWordN n -> SymWordN n -> SymBool
forall a. SEq a => a -> a -> SymBool
./= SymWordN n
0) (e' -> uf (SymWordN n)
forall a. e' -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e' -> uf (SymWordN n)) -> e' -> uf (SymWordN n)
forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Underflow) (SymWordN n -> uf (SymWordN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle SymWordN n
v)
safeMinus :: forall (uf :: * -> *).
(MonadError ArithException uf, MonadUnion uf) =>
SymWordN n -> SymWordN n -> uf (SymWordN n)
safeMinus SymWordN n
ls SymWordN n
rs =
SymBool -> uf (SymWordN n) -> uf (SymWordN n) -> uf (SymWordN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymWordN n
rs SymWordN n -> SymWordN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymWordN n
ls)
(ArithException -> uf (SymWordN n)
forall a. ArithException -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Underflow)
(SymWordN n -> uf (SymWordN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle SymWordN n
res)
where
res :: SymWordN n
res = SymWordN n
ls SymWordN n -> SymWordN n -> SymWordN n
forall a. Num a => a -> a -> a
- SymWordN n
rs
safeMinus' :: forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(ArithException -> e')
-> SymWordN n -> SymWordN n -> uf (SymWordN n)
safeMinus' ArithException -> e'
f SymWordN n
ls SymWordN n
rs =
SymBool -> uf (SymWordN n) -> uf (SymWordN n) -> uf (SymWordN n)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
(SymWordN n
rs SymWordN n -> SymWordN n -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> SymWordN n
ls)
(e' -> uf (SymWordN n)
forall a. e' -> uf a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (e' -> uf (SymWordN n)) -> e' -> uf (SymWordN n)
forall a b. (a -> b) -> a -> b
$ ArithException -> e'
f ArithException
Underflow)
(SymWordN n -> uf (SymWordN n)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle SymWordN n
res)
where
res :: SymWordN n
res = SymWordN n
ls SymWordN n -> SymWordN n -> SymWordN n
forall a. Num a => a -> a -> a
- SymWordN n
rs