{-# 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.Internal.Impl.Core.Data.Class.SafeDiv
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Internal.Impl.Core.Data.Class.SafeDiv () where

import Control.Exception (ArithException (DivideByZero, Overflow))
import Control.Monad.Except (MonadError (throwError))
import Data.Bifunctor (Bifunctor (bimap))
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.AsKey (AsKey (AsKey))
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.Internal.Decl.Core.Data.Class.SafeDiv
  ( DivOr (divModOr, divOr, modOr, quotOr, quotRemOr, remOr),
    SafeDiv (safeDiv, safeDivMod, safeMod, safeQuot, safeQuotRem, safeRem),
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.SymPrim.SymInteger (SymInteger)

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, op) \
name d l r = symIte (r .== con 0) d (op l r)

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

#define SAFE_DIVISION_SYMBOLIC_FUNC(name, op) \
name l r = mrgIf (r .== con 0) (throwError DivideByZero) (mrgSingle $ op l r)

#define SAFE_DIVISION_SYMBOLIC_FUNC2(name, op1, op2) \
name l r = mrgIf (r .== con 0) (throwError DivideByZero) (mrgSingle (op1 l r, op2 l r))

#if 1
instance DivOr SymInteger where
  DIVISION_OR_SYMBOLIC_FUNC(divOr, div)
  DIVISION_OR_SYMBOLIC_FUNC(modOr, mod)
  DIVISION_OR_SYMBOLIC_FUNC(quotOr, quot)
  DIVISION_OR_SYMBOLIC_FUNC(remOr, rem)
  DIVISION_OR_SYMBOLIC_FUNC2(divModOr, div, mod)
  DIVISION_OR_SYMBOLIC_FUNC2(quotRemOr, quot, rem)
instance
  (MonadUnion m, MonadError ArithException m) =>
  SafeDiv ArithException SymInteger m where
  SAFE_DIVISION_SYMBOLIC_FUNC(safeDiv, div)
  SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, mod)
  SAFE_DIVISION_SYMBOLIC_FUNC(safeQuot, quot)
  SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, rem)
  SAFE_DIVISION_SYMBOLIC_FUNC2(safeDivMod, div, mod)
  SAFE_DIVISION_SYMBOLIC_FUNC2(safeQuotRem, quot, rem)
#endif

#define DIVISION_OR_SYMBOLIC_FUNC_BOUNDED_SIGNED(name, op) \
name d l r = \
  symIte (r .== con 0) d $ \
    symIte (r .== con (-1) .&& l .== con minBound) d (op l r)

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

#define SAFE_DIVISION_SYMBOLIC_FUNC_BOUNDED_SIGNED(name, op) \
name l r = \
  mrgIf (r .== con 0) (throwError DivideByZero) $ \
    mrgIf (r .== con (-1) .&& l .== con minBound) \
      (throwError Overflow) \
      (mrgSingle $ op l r)

#define SAFE_DIVISION_SYMBOLIC_FUNC2_BOUNDED_SIGNED(name, op1, op2) \
name l r = \
  mrgIf (r .== con 0) (throwError DivideByZero) $ \
    mrgIf (r .== con (-1) .&& l .== con minBound) \
      (throwError Overflow) \
      (mrgSingle (op1 l r, op2 l r))

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

#if 1
instance (KnownNat n, 1 <= n) => DivOr (SymWordN n) where
  DIVISION_OR_SYMBOLIC_FUNC(divOr, div)
  DIVISION_OR_SYMBOLIC_FUNC(modOr, mod)
  DIVISION_OR_SYMBOLIC_FUNC(quotOr, quot)
  DIVISION_OR_SYMBOLIC_FUNC(remOr, rem)
  DIVISION_OR_SYMBOLIC_FUNC2(divModOr, div, mod)
  DIVISION_OR_SYMBOLIC_FUNC2(quotRemOr, quot, rem)
instance
  (MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) =>
  SafeDiv ArithException (SymWordN n) m where
  SAFE_DIVISION_SYMBOLIC_FUNC(safeDiv, div)
  SAFE_DIVISION_SYMBOLIC_FUNC(safeMod, mod)
  SAFE_DIVISION_SYMBOLIC_FUNC(safeQuot, quot)
  SAFE_DIVISION_SYMBOLIC_FUNC(safeRem, rem)
  SAFE_DIVISION_SYMBOLIC_FUNC2(safeDivMod, div, mod)
  SAFE_DIVISION_SYMBOLIC_FUNC2(safeQuotRem, quot, rem)
#endif

instance (DivOr a) => DivOr (AsKey a) where
  divOr :: AsKey a -> AsKey a -> AsKey a -> AsKey a
divOr (AsKey a
def) (AsKey a
n) (AsKey a
d) = a -> AsKey a
forall a. a -> AsKey a
AsKey (a -> AsKey a) -> a -> AsKey a
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> a
forall a. DivOr a => a -> a -> a -> a
divOr a
def a
n a
d
  modOr :: AsKey a -> AsKey a -> AsKey a -> AsKey a
modOr (AsKey a
def) (AsKey a
n) (AsKey a
d) = a -> AsKey a
forall a. a -> AsKey a
AsKey (a -> AsKey a) -> a -> AsKey a
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> a
forall a. DivOr a => a -> a -> a -> a
modOr a
def a
n a
d
  divModOr :: (AsKey a, AsKey a) -> AsKey a -> AsKey a -> (AsKey a, AsKey a)
divModOr (AsKey a
defDiv, AsKey a
defMod) (AsKey a
n) (AsKey a
d) =
    (a -> AsKey a) -> (a -> AsKey a) -> (a, a) -> (AsKey a, AsKey a)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> AsKey a
forall a. a -> AsKey a
AsKey a -> AsKey a
forall a. a -> AsKey a
AsKey ((a, a) -> (AsKey a, AsKey a)) -> (a, a) -> (AsKey a, AsKey a)
forall a b. (a -> b) -> a -> b
$ (a, a) -> a -> a -> (a, a)
forall a. DivOr a => (a, a) -> a -> a -> (a, a)
divModOr (a
defDiv, a
defMod) a
n a
d
  quotOr :: AsKey a -> AsKey a -> AsKey a -> AsKey a
quotOr (AsKey a
def) (AsKey a
n) (AsKey a
d) = a -> AsKey a
forall a. a -> AsKey a
AsKey (a -> AsKey a) -> a -> AsKey a
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> a
forall a. DivOr a => a -> a -> a -> a
quotOr a
def a
n a
d
  remOr :: AsKey a -> AsKey a -> AsKey a -> AsKey a
remOr (AsKey a
def) (AsKey a
n) (AsKey a
d) = a -> AsKey a
forall a. a -> AsKey a
AsKey (a -> AsKey a) -> a -> AsKey a
forall a b. (a -> b) -> a -> b
$ a -> a -> a -> a
forall a. DivOr a => a -> a -> a -> a
remOr a
def a
n a
d
  quotRemOr :: (AsKey a, AsKey a) -> AsKey a -> AsKey a -> (AsKey a, AsKey a)
quotRemOr (AsKey a
defDiv, AsKey a
defRem) (AsKey a
n) (AsKey a
d) =
    (a -> AsKey a) -> (a -> AsKey a) -> (a, a) -> (AsKey a, AsKey a)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> AsKey a
forall a. a -> AsKey a
AsKey a -> AsKey a
forall a. a -> AsKey a
AsKey ((a, a) -> (AsKey a, AsKey a)) -> (a, a) -> (AsKey a, AsKey a)
forall a b. (a -> b) -> a -> b
$ (a, a) -> a -> a -> (a, a)
forall a. DivOr a => (a, a) -> a -> a -> (a, a)
quotRemOr (a
defDiv, a
defRem) a
n a
d

instance (SafeDiv e a m) => SafeDiv e (AsKey a) m where
  safeDiv :: AsKey a -> AsKey a -> m (AsKey a)
safeDiv (AsKey a
n) (AsKey a
d) = do
    r <- a -> a -> m a
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeDiv a
n a
d
    mrgSingle $ AsKey r
  safeMod :: AsKey a -> AsKey a -> m (AsKey a)
safeMod (AsKey a
n) (AsKey a
d) = do
    r <- a -> a -> m a
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeMod a
n a
d
    mrgSingle $ AsKey r
  safeDivMod :: AsKey a -> AsKey a -> m (AsKey a, AsKey a)
safeDivMod (AsKey a
n) (AsKey a
d) = do
    (rd, rm) <- a -> a -> m (a, a)
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m (a, a)
safeDivMod a
n a
d
    mrgSingle (AsKey rd, AsKey rm)
  safeQuot :: AsKey a -> AsKey a -> m (AsKey a)
safeQuot (AsKey a
n) (AsKey a
d) = do
    r <- a -> a -> m a
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeQuot a
n a
d
    mrgSingle $ AsKey r
  safeRem :: AsKey a -> AsKey a -> m (AsKey a)
safeRem (AsKey a
n) (AsKey a
d) = do
    r <- a -> a -> m a
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeRem a
n a
d
    mrgSingle $ AsKey r
  safeQuotRem :: AsKey a -> AsKey a -> m (AsKey a, AsKey a)
safeQuotRem (AsKey a
n) (AsKey a
d) = do
    (rq, rr) <- a -> a -> m (a, a)
forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m (a, a)
safeQuotRem a
n a
d
    mrgSingle (AsKey rq, AsKey rr)