{-# 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.Internal.Unified.Class.UnifiedSafeSymShift
-- 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.Unified.Class.UnifiedSafeSymShift
  ( safeSymShiftL,
    safeSymShiftR,
    safeSymStrictShiftL,
    safeSymStrictShiftR,
    UnifiedSafeSymShift (..),
  )
where

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

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

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

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

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

-- | A class that provides unified safe symbolic rotation operations.
--
-- We use this type class to help resolve the constraints for `SafeSymShift`.
class UnifiedSafeSymShift (mode :: EvalModeTag) e a m where
  withBaseSafeSymShift :: ((SafeSymShift e a m) => r) -> r

instance
  {-# INCOHERENT #-}
  (UnifiedBranching mode m, SafeSymShift e a m) =>
  UnifiedSafeSymShift mode e a m
  where
  withBaseSafeSymShift :: forall r. (SafeSymShift e a m => r) -> r
withBaseSafeSymShift SafeSymShift e a m => r
r = r
SafeSymShift e a m => r
r

instance
  (MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) =>
  UnifiedSafeSymShift mode ArithException (IntN n) m
  where
  withBaseSafeSymShift :: forall r. (SafeSymShift ArithException (IntN n) m => r) -> r
withBaseSafeSymShift SafeSymShift ArithException (IntN n) m => r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => 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
SafeSymShift 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
SafeSymShift ArithException (IntN n) m => r
r)

instance
  (MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) =>
  UnifiedSafeSymShift 'S ArithException (SymIntN n) m
  where
  withBaseSafeSymShift :: forall r. (SafeSymShift ArithException (SymIntN n) m => r) -> r
withBaseSafeSymShift SafeSymShift ArithException (SymIntN n) m => r
r = forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @'S @m r
If (IsConMode 'S) (TryMerge m) (SymBranching m) => r
SafeSymShift ArithException (SymIntN n) m => r
r

instance
  (MonadError ArithException m, UnifiedBranching mode m, KnownNat n, 1 <= n) =>
  UnifiedSafeSymShift mode ArithException (WordN n) m
  where
  withBaseSafeSymShift :: forall r. (SafeSymShift ArithException (WordN n) m => r) -> r
withBaseSafeSymShift SafeSymShift ArithException (WordN n) m => r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => 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
SafeSymShift 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
SafeSymShift ArithException (WordN n) m => r
r)

instance
  (MonadError ArithException m, UnifiedBranching 'S m, KnownNat n, 1 <= n) =>
  UnifiedSafeSymShift 'S ArithException (SymWordN n) m
  where
  withBaseSafeSymShift :: forall r. (SafeSymShift ArithException (SymWordN n) m => r) -> r
withBaseSafeSymShift SafeSymShift ArithException (SymWordN n) m => r
r = forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @'S @m r
If (IsConMode 'S) (TryMerge m) (SymBranching m) => r
SafeSymShift ArithException (SymWordN n) m => r
r

instance
  ( MonadError (Either SomeBVException ArithException) m,
    UnifiedBranching mode m
  ) =>
  UnifiedSafeSymShift
    mode
    (Either SomeBVException ArithException)
    SomeIntN
    m
  where
  withBaseSafeSymShift :: forall r.
(SafeSymShift (Either SomeBVException ArithException) SomeIntN m =>
 r)
-> r
withBaseSafeSymShift SafeSymShift (Either SomeBVException ArithException) SomeIntN m =>
r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => 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
SafeSymShift (Either SomeBVException 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
SafeSymShift (Either SomeBVException ArithException) SomeIntN m =>
r
r)

instance
  ( MonadError (Either SomeBVException ArithException) m,
    UnifiedBranching 'S m
  ) =>
  UnifiedSafeSymShift
    'S
    (Either SomeBVException ArithException)
    SomeSymIntN
    m
  where
  withBaseSafeSymShift :: forall r.
(SafeSymShift
   (Either SomeBVException ArithException) SomeSymIntN m =>
 r)
-> r
withBaseSafeSymShift SafeSymShift
  (Either SomeBVException ArithException) SomeSymIntN m =>
r
r = forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @'S @m r
If (IsConMode 'S) (TryMerge m) (SymBranching m) => r
SafeSymShift
  (Either SomeBVException ArithException) SomeSymIntN m =>
r
r

instance
  ( MonadError (Either SomeBVException ArithException) m,
    UnifiedBranching mode m
  ) =>
  UnifiedSafeSymShift
    mode
    (Either SomeBVException ArithException)
    SomeWordN
    m
  where
  withBaseSafeSymShift :: forall r.
(SafeSymShift
   (Either SomeBVException ArithException) SomeWordN m =>
 r)
-> r
withBaseSafeSymShift SafeSymShift (Either SomeBVException ArithException) SomeWordN m =>
r
r =
    forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => 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
SafeSymShift (Either SomeBVException 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
SafeSymShift (Either SomeBVException ArithException) SomeWordN m =>
r
r)

instance
  ( MonadError (Either SomeBVException ArithException) m,
    UnifiedBranching 'S m
  ) =>
  UnifiedSafeSymShift
    'S
    (Either SomeBVException ArithException)
    SomeSymWordN
    m
  where
  withBaseSafeSymShift :: forall r.
(SafeSymShift
   (Either SomeBVException ArithException) SomeSymWordN m =>
 r)
-> r
withBaseSafeSymShift SafeSymShift
  (Either SomeBVException ArithException) SomeSymWordN m =>
r
r = forall (mode :: EvalModeTag) (m :: * -> *) r.
UnifiedBranching mode m =>
(If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
withBaseBranching @'S @m r
If (IsConMode 'S) (TryMerge m) (SymBranching m) => r
SafeSymShift
  (Either SomeBVException ArithException) SomeSymWordN m =>
r
r