{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.SafeDiv
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.SafeDiv
  ( ArithException (..),
    SafeDiv (..),
    DivOr (..),
    divOrZero,
    modOrDividend,
    quotOrZero,
    remOrDividend,
    divModOrZeroDividend,
    quotRemOrZeroDividend,
  )
where

import Control.Exception (ArithException (DivideByZero, Overflow, Underflow))
import Control.Monad.Except (MonadError (throwError))
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Core.Data.Class.LogicalOp (LogicalOp ((.&&)))
import Grisette.Internal.Core.Data.Class.Mergeable (Mergeable)
import Grisette.Internal.Core.Data.Class.SimpleMergeable
  ( mrgIf,
  )
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.Core.Data.Class.SymEq (SymEq ((.==)))
import Grisette.Internal.Core.Data.Class.TryMerge
  ( TryMerge,
    mrgSingle,
    tryMerge,
  )
import Grisette.Internal.SymPrim.BV
  ( IntN,
    WordN,
  )
import Grisette.Internal.SymPrim.Prim.Term
  ( PEvalDivModIntegralTerm
      ( pevalDivIntegralTerm,
        pevalModIntegralTerm,
        pevalQuotIntegralTerm,
        pevalRemIntegralTerm
      ),
  )
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN (SymIntN),
    SymWordN (SymWordN),
  )
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
import Grisette.Lib.Data.Functor (mrgFmap)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Control.Monad.Except
-- >>> import Control.Exception

-- | Safe division handling with default values returned on exception.
class DivOr a where
  -- | Safe 'div' with default value returned on exception.
  --
  -- >>> divOr "d" "a" "b" :: SymInteger
  -- (ite (= b 0) d (div a b))
  divOr :: a -> a -> a -> a

  -- | Safe 'mod' with default value returned on exception.
  --
  -- >>> modOr "d" "a" "b" :: SymInteger
  -- (ite (= b 0) d (mod a b))
  modOr :: a -> a -> a -> a

  -- | Safe 'divMod' with default value returned on exception.
  --
  -- >>> divModOr ("d", "m") "a" "b" :: (SymInteger, SymInteger)
  -- ((ite (= b 0) d (div a b)),(ite (= b 0) m (mod a b)))
  divModOr :: (a, a) -> a -> a -> (a, a)

  -- | Safe 'quot' with default value returned on exception.
  quotOr :: a -> a -> a -> a

  -- | Safe 'rem' with default value returned on exception.
  remOr :: a -> a -> a -> a

  -- | Safe 'quotRem' with default value returned on exception.
  quotRemOr :: (a, a) -> a -> a -> (a, a)

-- | Safe 'div' with 0 returned on exception.
divOrZero :: (DivOr a, Num a) => a -> a -> a
divOrZero :: forall a. (DivOr a, Num a) => a -> a -> a
divOrZero a
l = a -> a -> a -> a
forall a. DivOr a => a -> a -> a -> a
divOr (a
l a -> a -> a
forall a. Num a => a -> a -> a
- a
l) a
l
{-# INLINE divOrZero #-}

-- | Safe 'mod' with dividend returned on exception.
modOrDividend :: (DivOr a, Num a) => a -> a -> a
modOrDividend :: forall a. (DivOr a, Num a) => a -> a -> a
modOrDividend a
l = a -> a -> a -> a
forall a. DivOr a => a -> a -> a -> a
modOr a
l a
l
{-# INLINE modOrDividend #-}

-- | Safe 'quot' with 0 returned on exception.
quotOrZero :: (DivOr a, Num a) => a -> a -> a
quotOrZero :: forall a. (DivOr a, Num a) => a -> a -> a
quotOrZero a
l = a -> a -> a -> a
forall a. DivOr a => a -> a -> a -> a
quotOr (a
l a -> a -> a
forall a. Num a => a -> a -> a
- a
l) a
l
{-# INLINE quotOrZero #-}

-- | Safe 'rem' with dividend returned on exception.
remOrDividend :: (DivOr a, Num a) => a -> a -> a
remOrDividend :: forall a. (DivOr a, Num a) => a -> a -> a
remOrDividend a
l = a -> a -> a -> a
forall a. DivOr a => a -> a -> a -> a
remOr a
l a
l
{-# INLINE remOrDividend #-}

-- | Safe 'divMod' with 0 returned on exception.
divModOrZeroDividend :: (DivOr a, Num a) => a -> a -> (a, a)
divModOrZeroDividend :: forall a. (DivOr a, Num a) => a -> a -> (a, a)
divModOrZeroDividend a
l = (a, a) -> a -> a -> (a, a)
forall a. DivOr a => (a, a) -> a -> a -> (a, a)
divModOr (a
l a -> a -> a
forall a. Num a => a -> a -> a
- a
l, a
l) a
l
{-# INLINE divModOrZeroDividend #-}

-- | Safe 'quotRem' with 0 returned on exception.
quotRemOrZeroDividend :: (DivOr a, Num a) => a -> a -> (a, a)
quotRemOrZeroDividend :: forall a. (DivOr a, Num a) => a -> a -> (a, a)
quotRemOrZeroDividend a
l = (a, a) -> a -> a -> (a, a)
forall a. DivOr a => (a, a) -> a -> a -> (a, a)
quotRemOr (a
l a -> a -> a
forall a. Num a => a -> a -> a
- a
l, a
l) a
l
{-# INLINE quotRemOrZeroDividend #-}

-- | 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`.
class (MonadError e m, TryMerge m, Mergeable a, DivOr a) => SafeDiv e a m where
  -- | Safe 'div' with monadic error handling in multi-path execution.
  --
  -- >>> safeDiv "a" "b" :: ExceptT ArithException Union SymInteger
  -- ExceptT {If (= b 0) (Left divide by zero) (Right (div a b))}
  safeDiv :: a -> a -> m a
  safeDiv a
l a
r = ((a, a) -> a) -> m (a, a) -> m a
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (a, a) -> a
forall a b. (a, b) -> a
fst (m (a, a) -> m a) -> m (a, a) -> m a
forall a b. (a -> b) -> a -> b
$ a -> a -> m (a, a)
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m (a, a)
safeDivMod a
l a
r
  {-# INLINE safeDiv #-}

  -- | Safe 'mod' with monadic error handling in multi-path execution.
  --
  -- >>> safeMod "a" "b" :: ExceptT ArithException Union SymInteger
  -- ExceptT {If (= b 0) (Left divide by zero) (Right (mod a b))}
  safeMod :: a -> a -> m a
  safeMod a
l a
r = ((a, a) -> a) -> m (a, a) -> m a
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (a, a) -> a
forall a b. (a, b) -> b
snd (m (a, a) -> m a) -> m (a, a) -> m a
forall a b. (a -> b) -> a -> b
$ a -> a -> m (a, a)
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m (a, a)
safeDivMod a
l a
r
  {-# INLINE safeMod #-}

  -- | Safe 'divMod' with monadic error handling in multi-path execution.
  --
  -- >>> safeDivMod "a" "b" :: ExceptT ArithException Union (SymInteger, SymInteger)
  -- ExceptT {If (= b 0) (Left divide by zero) (Right ((div a b),(mod a b)))}
  safeDivMod :: a -> a -> m (a, a)
  safeDivMod a
l a
r = do
    a
d <- a -> a -> m a
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeDiv a
l a
r
    a
m <- a -> a -> m a
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeMod a
l a
r
    (a, a) -> m (a, a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a
d, a
m)
  {-# INLINE safeDivMod #-}

  -- | Safe 'quot' with monadic error handling in multi-path execution.
  safeQuot :: a -> a -> m a
  safeQuot a
l a
r = ((a, a) -> a) -> m (a, a) -> m a
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (a, a) -> a
forall a b. (a, b) -> a
fst (m (a, a) -> m a) -> m (a, a) -> m a
forall a b. (a -> b) -> a -> b
$ a -> a -> m (a, a)
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m (a, a)
safeQuotRem a
l a
r
  {-# INLINE safeQuot #-}

  -- | Safe 'rem' with monadic error handling in multi-path execution.
  safeRem :: a -> a -> m a
  safeRem a
l a
r = ((a, a) -> a) -> m (a, a) -> m a
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap (a, a) -> a
forall a b. (a, b) -> b
snd (m (a, a) -> m a) -> m (a, a) -> m a
forall a b. (a -> b) -> a -> b
$ a -> a -> m (a, a)
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m (a, a)
safeQuotRem a
l a
r
  {-# INLINE safeRem #-}

  -- | Safe 'quotRem' with monadic error handling in multi-path execution.
  safeQuotRem :: a -> a -> m (a, a)
  safeQuotRem a
l a
r = do
    a
q <- a -> a -> m a
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeQuot a
l a
r
    a
m <- a -> a -> m a
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeRem a
l a
r
    (a, a) -> m (a, a)
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a
q, a
m)
  {-# INLINE safeQuotRem #-}

  {-# MINIMAL
    ((safeDiv, safeMod) | safeDivMod),
    ((safeQuot, safeRem) | safeQuotRem)
    #-}

concreteDivOrHelper ::
  (Integral a) =>
  (a -> a -> r) ->
  r ->
  a ->
  a ->
  r
concreteDivOrHelper :: forall a r. Integral a => (a -> a -> r) -> r -> a -> a -> r
concreteDivOrHelper a -> a -> r
f r
d a
l a
r
  | a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 = r
d
  | Bool
otherwise = a -> a -> r
f a
l a
r

concreteSafeDivHelper ::
  (MonadError ArithException m, TryMerge m, Integral a, Mergeable r) =>
  (a -> a -> r) ->
  a ->
  a ->
  m r
concreteSafeDivHelper :: forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSafeDivHelper a -> a -> r
f a
l a
r
  | a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 = m r -> m r
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ ArithException -> m r
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
DivideByZero
  | Bool
otherwise = r -> m r
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (r -> m r) -> r -> m r
forall a b. (a -> b) -> a -> b
$ a -> a -> r
f a
l a
r

concreteSignedBoundedDivOrHelper ::
  ( Integral a,
    Bounded a,
    Mergeable r
  ) =>
  (a -> a -> r) ->
  r ->
  a ->
  a ->
  r
concreteSignedBoundedDivOrHelper :: forall a r.
(Integral a, Bounded a, Mergeable r) =>
(a -> a -> r) -> r -> a -> a -> r
concreteSignedBoundedDivOrHelper a -> a -> r
f r
d a
l a
r
  | a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 = r
d
  | a
l a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== -a
1 = r
d
  | Bool
otherwise = a -> a -> r
f a
l a
r

concreteSignedBoundedSafeDivHelper ::
  ( MonadError ArithException m,
    TryMerge m,
    Integral a,
    Bounded a,
    Mergeable r
  ) =>
  (a -> a -> r) ->
  a ->
  a ->
  m r
concreteSignedBoundedSafeDivHelper :: forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a, Bounded a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSignedBoundedSafeDivHelper a -> a -> r
f a
l a
r
  | a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 = m r -> m r
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ ArithException -> m r
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
DivideByZero
  | a
l a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& a
r a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== -a
1 = m r -> m r
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ ArithException -> m r
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow
  | Bool
otherwise = r -> m r
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (r -> m r) -> r -> m r
forall a b. (a -> b) -> a -> b
$ a -> a -> r
f a
l a
r

#define QUOTE() '
#define QID(a) a
#define QRIGHT(a) QID(a)'

#define QRIGHTT(a) QID(a)' t'
#define QRIGHTU(a) QID(a)' _'

#define DIVISION_OR_CONCRETE(type) \
instance DivOr type where \
  divOr = concreteDivOrHelper div; \
  modOr = concreteDivOrHelper mod; \
  divModOr = concreteDivOrHelper divMod; \
  quotOr = concreteDivOrHelper quot; \
  remOr = concreteDivOrHelper rem; \
  quotRemOr = concreteDivOrHelper quotRem

#define SAFE_DIVISION_CONCRETE(type) \
instance (MonadError ArithException m, TryMerge m) => \
  SafeDiv ArithException type m where \
  safeDiv = concreteSafeDivHelper div; \
  safeMod = concreteSafeDivHelper mod; \
  safeDivMod = concreteSafeDivHelper divMod; \
  safeQuot = concreteSafeDivHelper quot; \
  safeRem = concreteSafeDivHelper rem; \
  safeQuotRem = concreteSafeDivHelper quotRem

#define DIVISION_OR_CONCRETE_SIGNED_BOUNDED(type) \
instance DivOr type where \
  divOr = concreteSignedBoundedDivOrHelper div; \
  modOr = concreteDivOrHelper mod; \
  divModOr = concreteSignedBoundedDivOrHelper divMod; \
  quotOr = concreteSignedBoundedDivOrHelper quot; \
  remOr = concreteDivOrHelper rem; \
  quotRemOr = concreteSignedBoundedDivOrHelper quotRem

#define SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(type) \
instance (MonadError ArithException m, TryMerge m) => \
  SafeDiv ArithException type m where \
  safeDiv = concreteSignedBoundedSafeDivHelper div; \
  safeMod = concreteSafeDivHelper mod; \
  safeDivMod = concreteSignedBoundedSafeDivHelper divMod; \
  safeQuot = concreteSignedBoundedSafeDivHelper quot; \
  safeRem = concreteSafeDivHelper rem; \
  safeQuotRem = concreteSignedBoundedSafeDivHelper quotRem

#if 1
DIVISION_OR_CONCRETE(Integer)
SAFE_DIVISION_CONCRETE(Integer)
DIVISION_OR_CONCRETE_SIGNED_BOUNDED(Int8)
SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int8)
DIVISION_OR_CONCRETE_SIGNED_BOUNDED(Int16)
SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int16)
DIVISION_OR_CONCRETE_SIGNED_BOUNDED(Int32)
SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int32)
DIVISION_OR_CONCRETE_SIGNED_BOUNDED(Int64)
SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int64)
DIVISION_OR_CONCRETE_SIGNED_BOUNDED(Int)
SAFE_DIVISION_CONCRETE_SIGNED_BOUNDED(Int)
DIVISION_OR_CONCRETE(Word8)
SAFE_DIVISION_CONCRETE(Word8)
DIVISION_OR_CONCRETE(Word16)
SAFE_DIVISION_CONCRETE(Word16)
DIVISION_OR_CONCRETE(Word32)
SAFE_DIVISION_CONCRETE(Word32)
DIVISION_OR_CONCRETE(Word64)
SAFE_DIVISION_CONCRETE(Word64)
DIVISION_OR_CONCRETE(Word)
SAFE_DIVISION_CONCRETE(Word)


#endif

instance (KnownNat n, 1 <= n) => DivOr (IntN n) where
  divOr :: IntN n -> IntN n -> IntN n -> IntN n
divOr = (IntN n -> IntN n -> IntN n)
-> IntN n -> IntN n -> IntN n -> IntN n
forall a r.
(Integral a, Bounded a, Mergeable r) =>
(a -> a -> r) -> r -> a -> a -> r
concreteSignedBoundedDivOrHelper IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
div
  modOr :: IntN n -> IntN n -> IntN n -> IntN n
modOr = (IntN n -> IntN n -> IntN n)
-> IntN n -> IntN n -> IntN n -> IntN n
forall a r. Integral a => (a -> a -> r) -> r -> a -> a -> r
concreteDivOrHelper IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
mod
  divModOr :: (IntN n, IntN n) -> IntN n -> IntN n -> (IntN n, IntN n)
divModOr = (IntN n -> IntN n -> (IntN n, IntN n))
-> (IntN n, IntN n) -> IntN n -> IntN n -> (IntN n, IntN n)
forall a r.
(Integral a, Bounded a, Mergeable r) =>
(a -> a -> r) -> r -> a -> a -> r
concreteSignedBoundedDivOrHelper IntN n -> IntN n -> (IntN n, IntN n)
forall a. Integral a => a -> a -> (a, a)
divMod
  quotOr :: IntN n -> IntN n -> IntN n -> IntN n
quotOr = (IntN n -> IntN n -> IntN n)
-> IntN n -> IntN n -> IntN n -> IntN n
forall a r.
(Integral a, Bounded a, Mergeable r) =>
(a -> a -> r) -> r -> a -> a -> r
concreteSignedBoundedDivOrHelper IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
quot
  remOr :: IntN n -> IntN n -> IntN n -> IntN n
remOr = (IntN n -> IntN n -> IntN n)
-> IntN n -> IntN n -> IntN n -> IntN n
forall a r. Integral a => (a -> a -> r) -> r -> a -> a -> r
concreteDivOrHelper IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
rem
  quotRemOr :: (IntN n, IntN n) -> IntN n -> IntN n -> (IntN n, IntN n)
quotRemOr = (IntN n -> IntN n -> (IntN n, IntN n))
-> (IntN n, IntN n) -> IntN n -> IntN n -> (IntN n, IntN n)
forall a r.
(Integral a, Bounded a, Mergeable r) =>
(a -> a -> r) -> r -> a -> a -> r
concreteSignedBoundedDivOrHelper IntN n -> IntN n -> (IntN n, IntN n)
forall a. Integral a => a -> a -> (a, a)
quotRem

instance
  (MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) =>
  SafeDiv ArithException (IntN n) m
  where
  safeDiv :: IntN n -> IntN n -> m (IntN n)
safeDiv = (IntN n -> IntN n -> IntN n) -> IntN n -> IntN n -> m (IntN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a, Bounded a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSignedBoundedSafeDivHelper IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
div
  safeMod :: IntN n -> IntN n -> m (IntN n)
safeMod = (IntN n -> IntN n -> IntN n) -> IntN n -> IntN n -> m (IntN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSafeDivHelper IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
mod
  safeDivMod :: IntN n -> IntN n -> m (IntN n, IntN n)
safeDivMod = (IntN n -> IntN n -> (IntN n, IntN n))
-> IntN n -> IntN n -> m (IntN n, IntN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a, Bounded a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSignedBoundedSafeDivHelper IntN n -> IntN n -> (IntN n, IntN n)
forall a. Integral a => a -> a -> (a, a)
divMod
  safeQuot :: IntN n -> IntN n -> m (IntN n)
safeQuot = (IntN n -> IntN n -> IntN n) -> IntN n -> IntN n -> m (IntN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a, Bounded a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSignedBoundedSafeDivHelper IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
quot
  safeRem :: IntN n -> IntN n -> m (IntN n)
safeRem = (IntN n -> IntN n -> IntN n) -> IntN n -> IntN n -> m (IntN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSafeDivHelper IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
rem
  safeQuotRem :: IntN n -> IntN n -> m (IntN n, IntN n)
safeQuotRem = (IntN n -> IntN n -> (IntN n, IntN n))
-> IntN n -> IntN n -> m (IntN n, IntN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a, Bounded a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSignedBoundedSafeDivHelper IntN n -> IntN n -> (IntN n, IntN n)
forall a. Integral a => a -> a -> (a, a)
quotRem

instance (KnownNat n, 1 <= n) => DivOr (WordN n) where
  divOr :: WordN n -> WordN n -> WordN n -> WordN n
divOr = (WordN n -> WordN n -> WordN n)
-> WordN n -> WordN n -> WordN n -> WordN n
forall a r. Integral a => (a -> a -> r) -> r -> a -> a -> r
concreteDivOrHelper WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
div
  modOr :: WordN n -> WordN n -> WordN n -> WordN n
modOr = (WordN n -> WordN n -> WordN n)
-> WordN n -> WordN n -> WordN n -> WordN n
forall a r. Integral a => (a -> a -> r) -> r -> a -> a -> r
concreteDivOrHelper WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
mod
  divModOr :: (WordN n, WordN n) -> WordN n -> WordN n -> (WordN n, WordN n)
divModOr = (WordN n -> WordN n -> (WordN n, WordN n))
-> (WordN n, WordN n) -> WordN n -> WordN n -> (WordN n, WordN n)
forall a r. Integral a => (a -> a -> r) -> r -> a -> a -> r
concreteDivOrHelper WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
divMod
  quotOr :: WordN n -> WordN n -> WordN n -> WordN n
quotOr = (WordN n -> WordN n -> WordN n)
-> WordN n -> WordN n -> WordN n -> WordN n
forall a r. Integral a => (a -> a -> r) -> r -> a -> a -> r
concreteDivOrHelper WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
quot
  remOr :: WordN n -> WordN n -> WordN n -> WordN n
remOr = (WordN n -> WordN n -> WordN n)
-> WordN n -> WordN n -> WordN n -> WordN n
forall a r. Integral a => (a -> a -> r) -> r -> a -> a -> r
concreteDivOrHelper WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
rem
  quotRemOr :: (WordN n, WordN n) -> WordN n -> WordN n -> (WordN n, WordN n)
quotRemOr = (WordN n -> WordN n -> (WordN n, WordN n))
-> (WordN n, WordN n) -> WordN n -> WordN n -> (WordN n, WordN n)
forall a r. Integral a => (a -> a -> r) -> r -> a -> a -> r
concreteDivOrHelper WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
quotRem

instance
  (MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) =>
  SafeDiv ArithException (WordN n) m
  where
  safeDiv :: WordN n -> WordN n -> m (WordN n)
safeDiv = (WordN n -> WordN n -> WordN n)
-> WordN n -> WordN n -> m (WordN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSafeDivHelper WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
div
  safeMod :: WordN n -> WordN n -> m (WordN n)
safeMod = (WordN n -> WordN n -> WordN n)
-> WordN n -> WordN n -> m (WordN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSafeDivHelper WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
mod
  safeDivMod :: WordN n -> WordN n -> m (WordN n, WordN n)
safeDivMod = (WordN n -> WordN n -> (WordN n, WordN n))
-> WordN n -> WordN n -> m (WordN n, WordN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSafeDivHelper WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
divMod
  safeQuot :: WordN n -> WordN n -> m (WordN n)
safeQuot = (WordN n -> WordN n -> WordN n)
-> WordN n -> WordN n -> m (WordN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSafeDivHelper WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
quot
  safeRem :: WordN n -> WordN n -> m (WordN n)
safeRem = (WordN n -> WordN n -> WordN n)
-> WordN n -> WordN n -> m (WordN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSafeDivHelper WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
rem
  safeQuotRem :: WordN n -> WordN n -> m (WordN n, WordN n)
safeQuotRem = (WordN n -> WordN n -> (WordN n, WordN n))
-> WordN n -> WordN n -> m (WordN n, WordN n)
forall (m :: * -> *) a r.
(MonadError ArithException m, TryMerge m, Integral a,
 Mergeable r) =>
(a -> a -> r) -> a -> a -> m r
concreteSafeDivHelper WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
quotRem

#define DIVISION_OR_SYMBOLIC_FUNC(name, type, op) \
name d (type l) rs@(type r) = \
  symIte (rs .== con 0) d (type $ op l r)

#define DIVISION_OR_SYMBOLIC_FUNC2(name, type, op1, op2) \
name (dd, dm) (type l) rs@(type r) = \
  (symIte (rs .== con 0) dd (type $ op1 l r), \
   symIte (rs .== con 0) dm (type $ op2 l r))

#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); \

#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)); \

#if 1
instance DivOr SymInteger where
  DIVISION_OR_SYMBOLIC_FUNC(divOr, SymInteger, pevalDivIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC(modOr, SymInteger, pevalModIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC(quotOr, SymInteger, pevalQuotIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC(remOr, SymInteger, pevalRemIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC2(divModOr, SymInteger, pevalDivIntegralTerm, pevalModIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC2(quotRemOr, SymInteger, pevalQuotIntegralTerm, pevalRemIntegralTerm)
instance
  (MonadUnion m, MonadError ArithException m) =>
  SafeDiv ArithException SymInteger m 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 DIVISION_OR_SYMBOLIC_FUNC_BOUNDED_SIGNED(name, type, op) \
name d ls@(type l) rs@(type r) = \
  symIte \
    (rs .== con 0) \
    d \
    (symIte (rs .== con (-1) .&& ls .== con minBound) \
      d \
      (type $ op l r)) \

#define DIVISION_OR_SYMBOLIC_FUNC2_BOUNDED_SIGNED(name, type, op1, op2) \
name (dd, dr) ls@(type l) rs@(type r) = \
  (symIte \
    (rs .== con 0) \
    dd \
    (symIte (rs .== con (-1) .&& ls .== con minBound) \
      dd \
      (type $ op1 l r)), \
  symIte \
    (rs .== con 0) \
    dr \
    (symIte (rs .== con (-1) .&& ls .== con minBound) \
      dr \
      (type $ op2 l r))) \

#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)); \

#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))); \

#if 1
instance (KnownNat n, 1 <= n) => DivOr (SymIntN n) where
  DIVISION_OR_SYMBOLIC_FUNC_BOUNDED_SIGNED(divOr, SymIntN, pevalDivIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC(modOr, SymIntN, pevalModIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC_BOUNDED_SIGNED(quotOr, SymIntN, pevalQuotIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC(remOr, SymIntN, pevalRemIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC2_BOUNDED_SIGNED(divModOr, SymIntN, pevalDivIntegralTerm, pevalModIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC2_BOUNDED_SIGNED(quotRemOr, SymIntN, pevalQuotIntegralTerm, pevalRemIntegralTerm)
instance
  (MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) =>
  SafeDiv ArithException (SymIntN n) m where
  SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(safeDiv, SymIntN, pevalDivIntegralTerm)
  SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, SymIntN, pevalModIntegralTerm)
  SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(safeQuot, SymIntN, pevalQuotIntegralTerm)
  SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, SymIntN, pevalRemIntegralTerm)
  SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(safeDivMod, SymIntN, pevalDivIntegralTerm, pevalModIntegralTerm)
  SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(safeQuotRem, SymIntN, pevalQuotIntegralTerm, pevalRemIntegralTerm)
#endif

#if 1
instance (KnownNat n, 1 <= n) => DivOr (SymWordN n) where
  DIVISION_OR_SYMBOLIC_FUNC(divOr, SymWordN, pevalDivIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC(modOr, SymWordN, pevalModIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC(quotOr, SymWordN, pevalQuotIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC(remOr, SymWordN, pevalRemIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC2(divModOr, SymWordN, pevalDivIntegralTerm, pevalModIntegralTerm)
  DIVISION_OR_SYMBOLIC_FUNC2(quotRemOr, SymWordN, pevalQuotIntegralTerm, pevalRemIntegralTerm)
instance
  (MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) =>
  SafeDiv ArithException (SymWordN n) m 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