{-# 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.SafeDivision
( ArithException (..),
SafeDivision (..),
)
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.Prim.PartialEval.Integral
( pevalDivBoundedIntegralTerm,
pevalDivIntegralTerm,
pevalModBoundedIntegralTerm,
pevalModIntegralTerm,
pevalQuotBoundedIntegralTerm,
pevalQuotIntegralTerm,
pevalRemBoundedIntegralTerm,
pevalRemIntegralTerm,
)
import Grisette.IR.SymPrim.Data.SymPrim
( SymIntN (SymIntN),
SymInteger (SymInteger),
SymWordN (SymWordN),
)
class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeDivision e a | a -> e where
safeDiv :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
safeDiv a
l a
r = do
(a
d, a
_) <- a -> a -> uf (a, a)
forall e a (uf :: * -> *).
(SafeDivision e a, MonadError e uf, MonadUnion uf) =>
a -> a -> uf (a, a)
forall (uf :: * -> *).
(MonadError e uf, MonadUnion uf) =>
a -> a -> uf (a, a)
safeDivMod a
l a
r
a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
d
safeMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
safeMod a
l a
r = do
(a
_, a
m) <- a -> a -> uf (a, a)
forall e a (uf :: * -> *).
(SafeDivision e a, MonadError e uf, MonadUnion uf) =>
a -> a -> uf (a, a)
forall (uf :: * -> *).
(MonadError e uf, MonadUnion uf) =>
a -> a -> uf (a, a)
safeDivMod a
l a
r
a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
m
safeDivMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a)
safeDivMod a
l a
r = do
a
d <- a -> a -> uf a
forall e a (uf :: * -> *).
(SafeDivision e a, MonadError e uf, MonadUnion uf) =>
a -> a -> uf a
forall (uf :: * -> *).
(MonadError e uf, MonadUnion uf) =>
a -> a -> uf a
safeDiv a
l a
r
a
m <- a -> a -> uf a
forall e a (uf :: * -> *).
(SafeDivision e a, MonadError e uf, MonadUnion uf) =>
a -> a -> uf a
forall (uf :: * -> *).
(MonadError e uf, MonadUnion uf) =>
a -> a -> uf a
safeMod a
l a
r
(a, a) -> uf (a, a)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
d, a
m)
safeQuot :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
safeQuot a
l a
r = do
(a
d, a
m) <- a -> a -> uf (a, a)
forall e a (uf :: * -> *).
(SafeDivision e a, MonadError e uf, MonadUnion uf) =>
a -> a -> uf (a, a)
forall (uf :: * -> *).
(MonadError e uf, MonadUnion uf) =>
a -> a -> uf (a, a)
safeDivMod a
l a
r
SymBool -> uf a -> uf a -> uf a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
((a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.>= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| (a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.<= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| a
m a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
.== a
0)
(a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
d)
(a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> uf a) -> a -> uf a
forall a b. (a -> b) -> a -> b
$ a
d a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)
safeRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a
safeRem a
l a
r = do
(a
_, a
m) <- a -> a -> uf (a, a)
forall e a (uf :: * -> *).
(SafeDivision e a, MonadError e uf, MonadUnion uf) =>
a -> a -> uf (a, a)
forall (uf :: * -> *).
(MonadError e uf, MonadUnion uf) =>
a -> a -> uf (a, a)
safeDivMod a
l a
r
SymBool -> uf a -> uf a -> uf a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
((a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.>= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| (a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.<= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| a
m a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
.== a
0)
(a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
m)
(a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> uf a) -> a -> uf a
forall a b. (a -> b) -> a -> b
$ a
m a -> a -> a
forall a. Num a => a -> a -> a
- a
r)
safeQuotRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a)
safeQuotRem a
l a
r = do
(a
d, a
m) <- a -> a -> uf (a, a)
forall e a (uf :: * -> *).
(SafeDivision e a, MonadError e uf, MonadUnion uf) =>
a -> a -> uf (a, a)
forall (uf :: * -> *).
(MonadError e uf, MonadUnion uf) =>
a -> a -> uf (a, a)
safeDivMod a
l a
r
SymBool -> uf (a, a) -> uf (a, a) -> uf (a, a)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
((a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.>= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| (a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.<= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| a
m a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
.== a
0)
((a, a) -> uf (a, a)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
d, a
m))
((a, a) -> uf (a, a)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
d a -> a -> a
forall a. Num a => a -> a -> a
+ a
1, a
m a -> a -> a
forall a. Num a => a -> a -> a
- a
r))
safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
safeDiv' e -> e'
t a
l a
r = do
(a
d, a
_) <- (e -> e') -> a -> a -> uf (a, a)
forall e a e' (uf :: * -> *).
(SafeDivision e a, MonadError e' uf, MonadUnion uf,
Mergeable e') =>
(e -> e') -> a -> a -> uf (a, a)
forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(e -> e') -> a -> a -> uf (a, a)
safeDivMod' e -> e'
t a
l a
r
a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
d
safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
safeMod' e -> e'
t a
l a
r = do
(a
_, a
m) <- (e -> e') -> a -> a -> uf (a, a)
forall e a e' (uf :: * -> *).
(SafeDivision e a, MonadError e' uf, MonadUnion uf,
Mergeable e') =>
(e -> e') -> a -> a -> uf (a, a)
forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(e -> e') -> a -> a -> uf (a, a)
safeDivMod' e -> e'
t a
l a
r
a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
m
safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a)
safeDivMod' e -> e'
t a
l a
r = do
a
d <- (e -> e') -> a -> a -> uf a
forall e a e' (uf :: * -> *).
(SafeDivision e a, MonadError e' uf, MonadUnion uf,
Mergeable e') =>
(e -> e') -> a -> a -> uf a
forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(e -> e') -> a -> a -> uf a
safeDiv' e -> e'
t a
l a
r
a
m <- (e -> e') -> a -> a -> uf a
forall e a e' (uf :: * -> *).
(SafeDivision e a, MonadError e' uf, MonadUnion uf,
Mergeable e') =>
(e -> e') -> a -> a -> uf a
forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(e -> e') -> a -> a -> uf a
safeMod' e -> e'
t a
l a
r
(a, a) -> uf (a, a)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
d, a
m)
safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
safeQuot' e -> e'
t a
l a
r = do
(a
d, a
m) <- (e -> e') -> a -> a -> uf (a, a)
forall e a e' (uf :: * -> *).
(SafeDivision e a, MonadError e' uf, MonadUnion uf,
Mergeable e') =>
(e -> e') -> a -> a -> uf (a, a)
forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(e -> e') -> a -> a -> uf (a, a)
safeDivMod' e -> e'
t a
l a
r
SymBool -> uf a -> uf a -> uf a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
((a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.>= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| (a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.<= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| a
m a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
.== a
0)
(a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
d)
(a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> uf a) -> a -> uf a
forall a b. (a -> b) -> a -> b
$ a
d a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)
safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a
safeRem' e -> e'
t a
l a
r = do
(a
_, a
m) <- (e -> e') -> a -> a -> uf (a, a)
forall e a e' (uf :: * -> *).
(SafeDivision e a, MonadError e' uf, MonadUnion uf,
Mergeable e') =>
(e -> e') -> a -> a -> uf (a, a)
forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(e -> e') -> a -> a -> uf (a, a)
safeDivMod' e -> e'
t a
l a
r
SymBool -> uf a -> uf a -> uf a
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
((a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.>= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| (a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.<= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| a
m a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
.== a
0)
(a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle a
m)
(a -> uf a
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a -> uf a) -> a -> uf a
forall a b. (a -> b) -> a -> b
$ a
m a -> a -> a
forall a. Num a => a -> a -> a
- a
r)
safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a)
safeQuotRem' e -> e'
t a
l a
r = do
(a
d, a
m) <- (e -> e') -> a -> a -> uf (a, a)
forall e a e' (uf :: * -> *).
(SafeDivision e a, MonadError e' uf, MonadUnion uf,
Mergeable e') =>
(e -> e') -> a -> a -> uf (a, a)
forall e' (uf :: * -> *).
(MonadError e' uf, MonadUnion uf, Mergeable e') =>
(e -> e') -> a -> a -> uf (a, a)
safeDivMod' e -> e'
t a
l a
r
SymBool -> uf (a, a) -> uf (a, a) -> uf (a, a)
forall (u :: * -> *) a.
(UnionLike u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
((a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.>= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.> a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| (a
l a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.<= a
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& a
r a -> a -> SymBool
forall a. SOrd a => a -> a -> SymBool
.< a
0) SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| a
m a -> a -> SymBool
forall a. SEq a => a -> a -> SymBool
.== a
0)
((a, a) -> uf (a, a)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
d, a
m))
((a, a) -> uf (a, a)
forall (u :: * -> *) a. (UnionLike u, Mergeable a) => a -> u a
mrgSingle (a
d a -> a -> a
forall a. Num a => a -> a -> a
+ a
1, a
m a -> a -> a
forall a. Num a => a -> a -> a
- a
r))
{-# MINIMAL (safeDivMod | (safeDiv, safeMod)), (safeDivMod' | (safeDiv', safeMod')) #-}
#define QUOTE() '
#define QID(a) a
#define QRIGHT(a) QID(a)'
#define QRIGHTT(a) QID(a)' t'
#define QRIGHTU(a) QID(a)' _'
#define SAFE_DIVISION_CONCRETE_FUNC(name, op) \
name _ r | r == 0 = merge $ throwError DivideByZero; \
name l r = mrgSingle $ l `op` r; \
QRIGHTT(name) _ r | r == 0 = let _ = t' in merge $ throwError (t' DivideByZero); \
QRIGHTU(name) l r = mrgSingle $ l `op` r
#define SAFE_DIVISION_CONCRETE(type) \
instance SafeDivision ArithException type where \
SAFE_DIVISION_CONCRETE_FUNC(safeDiv, div); \
SAFE_DIVISION_CONCRETE_FUNC(safeMod, mod); \
SAFE_DIVISION_CONCRETE_FUNC(safeDivMod, divMod); \
SAFE_DIVISION_CONCRETE_FUNC(safeQuot, quot); \
SAFE_DIVISION_CONCRETE_FUNC(safeRem, rem); \
SAFE_DIVISION_CONCRETE_FUNC(safeQuotRem, quotRem)
#define SAFE_DIVISION_CONCRETE_BV(type) \
instance (KnownNat n, 1 <= n) => SafeDivision ArithException (type n) where \
SAFE_DIVISION_CONCRETE_FUNC(safeDiv, div); \
SAFE_DIVISION_CONCRETE_FUNC(safeMod, mod); \
SAFE_DIVISION_CONCRETE_FUNC(safeDivMod, divMod); \
SAFE_DIVISION_CONCRETE_FUNC(safeQuot, quot); \
SAFE_DIVISION_CONCRETE_FUNC(safeRem, rem); \
SAFE_DIVISION_CONCRETE_FUNC(safeQuotRem, quotRem)
#if 1
SAFE_DIVISION_CONCRETE(Integer)
SAFE_DIVISION_CONCRETE(Int8)
SAFE_DIVISION_CONCRETE(Int16)
SAFE_DIVISION_CONCRETE(Int32)
SAFE_DIVISION_CONCRETE(Int64)
SAFE_DIVISION_CONCRETE(Int)
SAFE_DIVISION_CONCRETE(Word8)
SAFE_DIVISION_CONCRETE(Word16)
SAFE_DIVISION_CONCRETE(Word32)
SAFE_DIVISION_CONCRETE(Word64)
SAFE_DIVISION_CONCRETE(Word)
#endif
#define SAFE_DIVISION_CONCRETE_FUNC_SOME(stype, type, name, op) \
name (stype (l :: type l)) (stype (r :: type r)) = \
(case sameNat (Proxy @l) (Proxy @r) of \
Just Refl -> \
if r == 0 \
then merge $ throwError $ Right DivideByZero \
else mrgSingle $ stype $ l `op` r; \
Nothing -> merge $ throwError $ Left BitwidthMismatch); \
QRIGHT(name) t (stype (l :: type l)) (stype (r :: type r)) = \
(case sameNat (Proxy @l) (Proxy @r) of \
Just Refl -> \
if r == 0 \
then merge $ throwError $ t (Right DivideByZero) \
else mrgSingle $ stype $ l `op` r; \
Nothing -> merge $ throwError $ t (Left BitwidthMismatch))
#define SAFE_DIVISION_CONCRETE_FUNC_SOME_DIVMOD(stype, type, name, op) \
name (stype (l :: type l)) (stype (r :: type r)) = \
(case sameNat (Proxy @l) (Proxy @r) of \
Just Refl -> \
if r == 0 \
then merge $ throwError $ Right DivideByZero \
else (case l `op` r of (d, m) -> mrgSingle (stype d, stype m)); \
Nothing -> merge $ throwError $ Left BitwidthMismatch); \
QRIGHT(name) t (stype (l :: type l)) (stype (r :: type r)) = \
(case sameNat (Proxy @l) (Proxy @r) of \
Just Refl -> \
if r == 0 \
then merge $ throwError $ t (Right DivideByZero) \
else (case l `op` r of (d, m) -> mrgSingle (stype d, stype m)); \
Nothing -> merge $ throwError $ t (Left BitwidthMismatch))
#if 1
SAFE_DIVISION_CONCRETE_BV(IntN)
SAFE_DIVISION_CONCRETE_BV(WordN)
instance SafeDivision (Either BitwidthMismatch ArithException) SomeIntN where
SAFE_DIVISION_CONCRETE_FUNC_SOME(SomeIntN, IntN, safeDiv, div)
SAFE_DIVISION_CONCRETE_FUNC_SOME(SomeIntN, IntN, safeMod, mod)
SAFE_DIVISION_CONCRETE_FUNC_SOME_DIVMOD(SomeIntN, IntN, safeDivMod, divMod)
SAFE_DIVISION_CONCRETE_FUNC_SOME(SomeIntN, IntN, safeQuot, quot)
SAFE_DIVISION_CONCRETE_FUNC_SOME(SomeIntN, IntN, safeRem, rem)
SAFE_DIVISION_CONCRETE_FUNC_SOME_DIVMOD(SomeIntN, IntN, safeQuotRem, quotRem)
instance SafeDivision (Either BitwidthMismatch ArithException) SomeWordN where
SAFE_DIVISION_CONCRETE_FUNC_SOME(SomeWordN, WordN, safeDiv, div)
SAFE_DIVISION_CONCRETE_FUNC_SOME(SomeWordN, WordN, safeMod, mod)
SAFE_DIVISION_CONCRETE_FUNC_SOME_DIVMOD(SomeWordN, WordN, safeDivMod, divMod)
SAFE_DIVISION_CONCRETE_FUNC_SOME(SomeWordN, WordN, safeQuot, quot)
SAFE_DIVISION_CONCRETE_FUNC_SOME(SomeWordN, WordN, safeRem, rem)
SAFE_DIVISION_CONCRETE_FUNC_SOME_DIVMOD(SomeWordN, WordN, safeQuotRem, quotRem)
#endif
#define SAFE_DIVISION_SYMBOLIC_FUNC(name, type, op) \
name (type l) rs@(type r) = \
mrgIf \
(rs .== con 0) \
(throwError DivideByZero) \
(mrgSingle $ type $ op l r); \
QRIGHT(name) t (type l) rs@(type r) = \
mrgIf \
(rs .== con 0) \
(throwError (t DivideByZero)) \
(mrgSingle $ type $ op l r)
#define SAFE_DIVISION_SYMBOLIC_FUNC2(name, type, op1, op2) \
name (type l) rs@(type r) = \
mrgIf \
(rs .== con 0) \
(throwError DivideByZero) \
(mrgSingle (type $ op1 l r, type $ op2 l r)); \
QRIGHT(name) t (type l) rs@(type r) = \
mrgIf \
(rs .== con 0) \
(throwError (t DivideByZero)) \
(mrgSingle (type $ op1 l r, type $ op2 l r))
#if 1
instance SafeDivision ArithException SymInteger where
SAFE_DIVISION_SYMBOLIC_FUNC(safeDiv, SymInteger, pevalDivIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, SymInteger, pevalModIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC(safeQuot, SymInteger, pevalQuotIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, SymInteger, pevalRemIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC2(safeDivMod, SymInteger, pevalDivIntegralTerm, pevalModIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC2(safeQuotRem, SymInteger, pevalQuotIntegralTerm, pevalRemIntegralTerm)
#endif
#define SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(name, type, op) \
name ls@(type l) rs@(type r) = \
mrgIf \
(rs .== con 0) \
(throwError DivideByZero) \
(mrgIf (rs .== con (-1) .&& ls .== con minBound) \
(throwError Overflow) \
(mrgSingle $ type $ op l r)); \
QRIGHT(name) t ls@(type l) rs@(type r) = \
mrgIf \
(rs .== con 0) \
(throwError (t DivideByZero)) \
(mrgIf (rs .== con (-1) .&& ls .== con minBound) \
(throwError (t Overflow)) \
(mrgSingle $ type $ op l r))
#define SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(name, type, op1, op2) \
name ls@(type l) rs@(type r) = \
mrgIf \
(rs .== con 0) \
(throwError DivideByZero) \
(mrgIf (rs .== con (-1) .&& ls .== con minBound) \
(throwError Overflow) \
(mrgSingle (type $ op1 l r, type $ op2 l r))); \
QRIGHT(name) t ls@(type l) rs@(type r) = \
mrgIf \
(rs .== con 0) \
(throwError (t DivideByZero)) \
(mrgIf (rs .== con (-1) .&& ls .== con minBound) \
(throwError (t Overflow)) \
(mrgSingle (type $ op1 l r, type $ op2 l r)))
#if 1
instance (KnownNat n, 1 <= n) => SafeDivision ArithException (SymIntN n) where
SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(safeDiv, SymIntN, pevalDivBoundedIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, SymIntN, pevalModBoundedIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(safeQuot, SymIntN, pevalQuotBoundedIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, SymIntN, pevalRemBoundedIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(safeDivMod, SymIntN, pevalDivBoundedIntegralTerm, pevalModBoundedIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(safeQuotRem, SymIntN, pevalQuotBoundedIntegralTerm, pevalRemBoundedIntegralTerm)
#endif
#if 1
instance (KnownNat n, 1 <= n) => SafeDivision ArithException (SymWordN n) where
SAFE_DIVISION_SYMBOLIC_FUNC(safeDiv, SymWordN, pevalDivIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, SymWordN, pevalModIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC(safeQuot, SymWordN, pevalQuotIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, SymWordN, pevalRemIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC2(safeDivMod, SymWordN, pevalDivIntegralTerm, pevalModIntegralTerm)
SAFE_DIVISION_SYMBOLIC_FUNC2(safeQuotRem, SymWordN, pevalQuotIntegralTerm, pevalRemIntegralTerm)
#endif