{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# HLINT ignore "Eta reduce" #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

-- |
-- Module      :   Grisette.Unified.Internal.Class.UnifiedSafeDivision
-- 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.Unified.Internal.Class.UnifiedSafeDivision
  ( safeDiv,
    safeMod,
    safeDivMod,
    safeQuot,
    safeRem,
    safeQuotRem,
    UnifiedSafeDivision (..),
  )
where

import Control.Monad.Error.Class (MonadError)
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.Core.Data.Class.SafeDivision
  ( ArithException,
    SafeDivision,
  )
import qualified Grisette.Internal.Core.Data.Class.SafeDivision
import Grisette.Internal.SymPrim.BV (BitwidthMismatch, IntN, WordN)
import Grisette.Internal.SymPrim.SomeBV
  ( SomeIntN,
    SomeSymIntN,
    SomeSymWordN,
    SomeWordN,
  )
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Unified.Internal.Class.UnifiedSimpleMergeable
  ( UnifiedBranching (withBaseBranching),
  )
import Grisette.Unified.Internal.EvalModeTag
  ( EvalModeTag (Sym),
  )
import Grisette.Unified.Internal.Util (withMode)

-- | Unified `Grisette.Internal.Core.Data.Class.SafeDivision.safeDiv` operation.
--
-- This function isn't able to infer the mode, so you need to provide the mode
-- explicitly. For example:
--
-- > safeDiv @mode a b
safeDiv ::
  forall mode e a m.
  (MonadError e m, UnifiedSafeDivision mode e a m) =>
  a ->
  a ->
  m a
safeDiv :: forall (mode :: EvalModeTag) e a (m :: * -> *).
(MonadError e m, UnifiedSafeDivision mode e a m) =>
a -> a -> m a
safeDiv a
a a
b =
  forall (mode :: EvalModeTag) e a (m :: * -> *) r.
UnifiedSafeDivision mode e a m =>
(SafeDivision e a m => r) -> r
withBaseSafeDivision @mode @e @a @m ((SafeDivision e a m => m a) -> m a)
-> (SafeDivision e a m => m a) -> m a
forall a b. (a -> b) -> a -> b
$
    a -> a -> m a
forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
Grisette.Internal.Core.Data.Class.SafeDivision.safeDiv a
a a
b
{-# INLINE safeDiv #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SafeDivision.safeMod` operation.
--
-- This function isn't able to infer the mode, so you need to provide the mode
-- explicitly. For example:
--
-- > safeMod @mode a b
safeMod ::
  forall mode e a m.
  (MonadError e m, UnifiedSafeDivision mode e a m) =>
  a ->
  a ->
  m a
safeMod :: forall (mode :: EvalModeTag) e a (m :: * -> *).
(MonadError e m, UnifiedSafeDivision mode e a m) =>
a -> a -> m a
safeMod a
a a
b =
  forall (mode :: EvalModeTag) e a (m :: * -> *) r.
UnifiedSafeDivision mode e a m =>
(SafeDivision e a m => r) -> r
withBaseSafeDivision @mode @e @a @m ((SafeDivision e a m => m a) -> m a)
-> (SafeDivision e a m => m a) -> m a
forall a b. (a -> b) -> a -> b
$
    a -> a -> m a
forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
Grisette.Internal.Core.Data.Class.SafeDivision.safeMod a
a a
b
{-# INLINE safeMod #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SafeDivision.safeDivMod`
-- operation.
--
-- This function isn't able to infer the mode, so you need to provide the mode
-- explicitly. For example:
--
-- > safeDivMod @mode a b
safeDivMod ::
  forall mode e a m.
  (MonadError e m, UnifiedSafeDivision mode e a m) =>
  a ->
  a ->
  m (a, a)
safeDivMod :: forall (mode :: EvalModeTag) e a (m :: * -> *).
(MonadError e m, UnifiedSafeDivision mode e a m) =>
a -> a -> m (a, a)
safeDivMod a
a a
b =
  forall (mode :: EvalModeTag) e a (m :: * -> *) r.
UnifiedSafeDivision mode e a m =>
(SafeDivision e a m => r) -> r
withBaseSafeDivision @mode @e @a @m ((SafeDivision e a m => m (a, a)) -> m (a, a))
-> (SafeDivision e a m => m (a, a)) -> m (a, a)
forall a b. (a -> b) -> a -> b
$
    a -> a -> m (a, a)
forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m (a, a)
Grisette.Internal.Core.Data.Class.SafeDivision.safeDivMod a
a a
b
{-# INLINE safeDivMod #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SafeDivision.safeQuot`
-- operation.
--
-- This function isn't able to infer the mode, so you need to provide the mode
-- explicitly. For example:
--
-- > safeQuot @mode a b
safeQuot ::
  forall mode e a m.
  (MonadError e m, UnifiedSafeDivision mode e a m) =>
  a ->
  a ->
  m a
safeQuot :: forall (mode :: EvalModeTag) e a (m :: * -> *).
(MonadError e m, UnifiedSafeDivision mode e a m) =>
a -> a -> m a
safeQuot a
a a
b =
  forall (mode :: EvalModeTag) e a (m :: * -> *) r.
UnifiedSafeDivision mode e a m =>
(SafeDivision e a m => r) -> r
withBaseSafeDivision @mode @e @a @m ((SafeDivision e a m => m a) -> m a)
-> (SafeDivision e a m => m a) -> m a
forall a b. (a -> b) -> a -> b
$
    a -> a -> m a
forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
Grisette.Internal.Core.Data.Class.SafeDivision.safeQuot a
a a
b
{-# INLINE safeQuot #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SafeDivision.safeRem` operation.
--
-- This function isn't able to infer the mode, so you need to provide the mode
-- explicitly. For example:
--
-- > safeRem @mode a b
safeRem ::
  forall mode e a m.
  (MonadError e m, UnifiedSafeDivision mode e a m) =>
  a ->
  a ->
  m a
safeRem :: forall (mode :: EvalModeTag) e a (m :: * -> *).
(MonadError e m, UnifiedSafeDivision mode e a m) =>
a -> a -> m a
safeRem a
a a
b =
  forall (mode :: EvalModeTag) e a (m :: * -> *) r.
UnifiedSafeDivision mode e a m =>
(SafeDivision e a m => r) -> r
withBaseSafeDivision @mode @e @a @m ((SafeDivision e a m => m a) -> m a)
-> (SafeDivision e a m => m a) -> m a
forall a b. (a -> b) -> a -> b
$
    a -> a -> m a
forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
Grisette.Internal.Core.Data.Class.SafeDivision.safeRem a
a a
b
{-# INLINE safeRem #-}

-- | Unified `Grisette.Internal.Core.Data.Class.SafeDivision.safeQuotRem`
-- operation.
--
-- This function isn't able to infer the mode, so you need to provide the mode
-- explicitly. For example:
--
-- > safeQuotRem @mode a b
safeQuotRem ::
  forall mode e a m.
  (MonadError e m, UnifiedSafeDivision mode e a m) =>
  a ->
  a ->
  m (a, a)
safeQuotRem :: forall (mode :: EvalModeTag) e a (m :: * -> *).
(MonadError e m, UnifiedSafeDivision mode e a m) =>
a -> a -> m (a, a)
safeQuotRem a
a a
b =
  forall (mode :: EvalModeTag) e a (m :: * -> *) r.
UnifiedSafeDivision mode e a m =>
(SafeDivision e a m => r) -> r
withBaseSafeDivision @mode @e @a @m ((SafeDivision e a m => m (a, a)) -> m (a, a))
-> (SafeDivision e a m => m (a, a)) -> m (a, a)
forall a b. (a -> b) -> a -> b
$
    a -> a -> m (a, a)
forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m (a, a)
Grisette.Internal.Core.Data.Class.SafeDivision.safeQuotRem a
a a
b
{-# INLINE safeQuotRem #-}

-- | A class that provides unified division operations.
--
-- We use this type class to help resolve the constraints for `SafeDivision`.
class UnifiedSafeDivision (mode :: EvalModeTag) e a m where
  withBaseSafeDivision :: ((SafeDivision e a m) => r) -> r

instance
  {-# INCOHERENT #-}
  (UnifiedBranching mode m, SafeDivision e a m) =>
  UnifiedSafeDivision mode e a m
  where
  withBaseSafeDivision :: forall r. (SafeDivision e a m => r) -> r
withBaseSafeDivision SafeDivision e a m => r
r = r
SafeDivision e a m => r
r

instance
  (MonadError ArithException m, UnifiedBranching mode m) =>
  UnifiedSafeDivision mode ArithException Integer m
  where
  withBaseSafeDivision :: forall r. (SafeDivision ArithException Integer m => r) -> r
withBaseSafeDivision SafeDivision ArithException Integer m => r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode (forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m r
If (IsConMode mode) (TryMerge m) (SymBranching m) => r
SafeDivision ArithException Integer m => r
r) (forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m r
If (IsConMode mode) (TryMerge m) (SymBranching m) => r
SafeDivision ArithException Integer m => r
r)

instance
  (MonadError ArithException m, UnifiedBranching 'Sym m) =>
  UnifiedSafeDivision 'Sym ArithException SymInteger m
  where
  withBaseSafeDivision :: forall r. (SafeDivision ArithException SymInteger m => r) -> r
withBaseSafeDivision SafeDivision ArithException SymInteger m => r
r = forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @'Sym @m r
If (IsConMode 'Sym) (TryMerge m) (SymBranching m) => r
SafeDivision ArithException SymInteger m => r
r

instance
  (MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) =>
  UnifiedSafeDivision mode ArithException (IntN n) m
  where
  withBaseSafeDivision :: forall r. (SafeDivision ArithException (IntN n) m => r) -> r
withBaseSafeDivision SafeDivision ArithException (IntN n) m => r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode (forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m r
If (IsConMode mode) (TryMerge m) (SymBranching m) => r
SafeDivision ArithException (IntN n) m => r
r) (forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m r
If (IsConMode mode) (TryMerge m) (SymBranching m) => r
SafeDivision ArithException (IntN n) m => r
r)

instance
  (MonadError ArithException m, UnifiedBranching 'Sym m, KnownNat n, 1 <= n) =>
  UnifiedSafeDivision 'Sym ArithException (SymIntN n) m
  where
  withBaseSafeDivision :: forall r. (SafeDivision ArithException (SymIntN n) m => r) -> r
withBaseSafeDivision SafeDivision ArithException (SymIntN n) m => r
r = forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @'Sym @m r
If (IsConMode 'Sym) (TryMerge m) (SymBranching m) => r
SafeDivision ArithException (SymIntN n) m => r
r

instance
  (MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) =>
  UnifiedSafeDivision mode ArithException (WordN n) m
  where
  withBaseSafeDivision :: forall r. (SafeDivision ArithException (WordN n) m => r) -> r
withBaseSafeDivision SafeDivision ArithException (WordN n) m => r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode (forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m r
If (IsConMode mode) (TryMerge m) (SymBranching m) => r
SafeDivision ArithException (WordN n) m => r
r) (forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m r
If (IsConMode mode) (TryMerge m) (SymBranching m) => r
SafeDivision ArithException (WordN n) m => r
r)

instance
  (MonadError ArithException m, UnifiedBranching 'Sym m, KnownNat n, 1 <= n) =>
  UnifiedSafeDivision 'Sym ArithException (SymWordN n) m
  where
  withBaseSafeDivision :: forall r. (SafeDivision ArithException (SymWordN n) m => r) -> r
withBaseSafeDivision SafeDivision ArithException (SymWordN n) m => r
r = forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @'Sym @m r
If (IsConMode 'Sym) (TryMerge m) (SymBranching m) => r
SafeDivision ArithException (SymWordN n) m => r
r

instance
  ( MonadError (Either BitwidthMismatch ArithException) m,
    UnifiedBranching mode m
  ) =>
  UnifiedSafeDivision
    mode
    (Either BitwidthMismatch ArithException)
    SomeIntN
    m
  where
  withBaseSafeDivision :: forall r.
(SafeDivision
   (Either BitwidthMismatch ArithException) SomeIntN m =>
 r)
-> r
withBaseSafeDivision SafeDivision (Either BitwidthMismatch ArithException) SomeIntN m =>
r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode (forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m r
If (IsConMode mode) (TryMerge m) (SymBranching m) => r
SafeDivision (Either BitwidthMismatch ArithException) SomeIntN m =>
r
r) (forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m r
If (IsConMode mode) (TryMerge m) (SymBranching m) => r
SafeDivision (Either BitwidthMismatch ArithException) SomeIntN m =>
r
r)

instance
  ( MonadError (Either BitwidthMismatch ArithException) m,
    UnifiedBranching 'Sym m
  ) =>
  UnifiedSafeDivision
    'Sym
    (Either BitwidthMismatch ArithException)
    SomeSymIntN
    m
  where
  withBaseSafeDivision :: forall r.
(SafeDivision
   (Either BitwidthMismatch ArithException) SomeSymIntN m =>
 r)
-> r
withBaseSafeDivision SafeDivision
  (Either BitwidthMismatch ArithException) SomeSymIntN m =>
r
r = forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @'Sym @m r
If (IsConMode 'Sym) (TryMerge m) (SymBranching m) => r
SafeDivision
  (Either BitwidthMismatch ArithException) SomeSymIntN m =>
r
r

instance
  ( MonadError (Either BitwidthMismatch ArithException) m,
    UnifiedBranching mode m
  ) =>
  UnifiedSafeDivision
    mode
    (Either BitwidthMismatch ArithException)
    SomeWordN
    m
  where
  withBaseSafeDivision :: forall r.
(SafeDivision
   (Either BitwidthMismatch ArithException) SomeWordN m =>
 r)
-> r
withBaseSafeDivision SafeDivision
  (Either BitwidthMismatch ArithException) SomeWordN m =>
r
r =
    forall (mode :: EvalModeTag) r.
Typeable mode =>
((mode ~ 'Con) => r) -> ((mode ~ 'Sym) => r) -> r
withMode @mode (forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m r
If (IsConMode mode) (TryMerge m) (SymBranching m) => r
SafeDivision
  (Either BitwidthMismatch ArithException) SomeWordN m =>
r
r) (forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @mode @m r
If (IsConMode mode) (TryMerge m) (SymBranching m) => r
SafeDivision
  (Either BitwidthMismatch ArithException) SomeWordN m =>
r
r)

instance
  ( MonadError (Either BitwidthMismatch ArithException) m,
    UnifiedBranching 'Sym m
  ) =>
  UnifiedSafeDivision
    'Sym
    (Either BitwidthMismatch ArithException)
    SomeSymWordN
    m
  where
  withBaseSafeDivision :: forall r.
(SafeDivision
   (Either BitwidthMismatch ArithException) SomeSymWordN m =>
 r)
-> r
withBaseSafeDivision SafeDivision
  (Either BitwidthMismatch ArithException) SomeSymWordN m =>
r
r = forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @'Sym @m r
If (IsConMode 'Sym) (TryMerge m) (SymBranching m) => r
SafeDivision
  (Either BitwidthMismatch ArithException) SomeSymWordN m =>
r
r