{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.SafeSymShift
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.SafeSymShift
  ( SafeSymShift (..),
  )
where

import Control.Exception (ArithException (Overflow))
import Control.Monad.Error.Class (MonadError (throwError))
import Data.Bits (Bits (shiftL, shiftR), FiniteBits (finiteBitSize))
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.Core.Control.Monad.Class.Union (MonadUnion)
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.SymOrd
  ( SymOrd ((.<), (.>=)),
  )
import Grisette.Internal.Core.Data.Class.TryMerge
  ( TryMerge,
    mrgSingle,
    tryMerge,
  )
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Term
  ( PEvalShiftTerm
      ( pevalShiftLeftTerm,
        pevalShiftRightTerm
      ),
  )
import Grisette.Internal.SymPrim.SymBV (SymIntN (SymIntN), SymWordN (SymWordN))

-- | Safe version for `shiftL` or `shiftR`.
--
-- The `safeSymShiftL` and `safeSymShiftR` are defined for all non-negative
-- shift amounts.
--
-- * Shifting by negative shift amounts is an error.
-- * The result is defined to be 0 when shifting left by more than or equal to
-- the  bit size of the number.
-- * The result is defined to be 0 when shifting right by more than or equal to
-- the bit size of the number and the number is unsigned or signed non-negative.
-- * The result is defined to be -1 when shifting right by more than or equal to
-- the bit size of the number and the number is signed negative.
--
-- The `safeSymStrictShiftL` and `safeSymStrictShiftR` are defined for all
-- non-negative shift amounts that is less than the bit size. Shifting by more
-- than or equal to the bit size is an error, otherwise they are the same as the
-- non-strict versions.
class (MonadError e m, TryMerge m, Mergeable a) => SafeSymShift e a m where
  safeSymShiftL :: a -> a -> m a
  safeSymShiftR :: a -> a -> m a
  safeSymStrictShiftL :: a -> a -> m a
  safeSymStrictShiftR :: a -> a -> m a

-- | This function handles the case when the shift amount is out the range of
-- `Int` correctly.
safeSymShiftLConcreteNum ::
  (MonadError ArithException m, TryMerge m, Integral a, FiniteBits a, Mergeable a) =>
  Bool ->
  a ->
  a ->
  m a
safeSymShiftLConcreteNum :: forall (m :: * -> *) a.
(MonadError ArithException m, TryMerge m, Integral a, FiniteBits a,
 Mergeable a) =>
Bool -> a -> a -> m a
safeSymShiftLConcreteNum Bool
_ a
_ a
s | a
s a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ArithException -> m a
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow
safeSymShiftLConcreteNum Bool
allowLargeShiftAmount a
a a
s
  | (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
s :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
a) =
      if Bool
allowLargeShiftAmount
        then a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
0
        else m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ArithException -> m a
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow
safeSymShiftLConcreteNum Bool
_ a
a a
s = a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ a -> Int -> a
forall a. Bits a => a -> Int -> a
shiftL a
a (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
s)

-- | This function handles the case when the shift amount is out the range of
-- `Int` correctly.
safeSymShiftRConcreteNum ::
  ( MonadError ArithException m,
    TryMerge m,
    Integral a,
    FiniteBits a,
    Mergeable a
  ) =>
  Bool ->
  a ->
  a ->
  m a
safeSymShiftRConcreteNum :: forall (m :: * -> *) a.
(MonadError ArithException m, TryMerge m, Integral a, FiniteBits a,
 Mergeable a) =>
Bool -> a -> a -> m a
safeSymShiftRConcreteNum Bool
_ a
_ a
s | a
s a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ArithException -> m a
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow
safeSymShiftRConcreteNum Bool
allowLargeShiftAmount a
a a
s
  | (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
s :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
a) =
      if Bool
allowLargeShiftAmount
        then a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle a
0
        else m a -> m a
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ ArithException -> m a
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow
safeSymShiftRConcreteNum Bool
_ a
a a
s = a -> m a
forall (m :: * -> *) a.
(TryMerge m, Applicative m, Mergeable a) =>
a -> m a
mrgSingle (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ a -> Int -> a
forall a. Bits a => a -> Int -> a
shiftR a
a (a -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
s)

#define SAFE_SYM_SHIFT_CONCRETE(T) \
  instance (MonadError ArithException m, TryMerge m) => \
    SafeSymShift ArithException T m where \
    safeSymShiftL = safeSymShiftLConcreteNum True; \
    safeSymShiftR = safeSymShiftRConcreteNum True; \
    safeSymStrictShiftL = safeSymShiftLConcreteNum False; \
    safeSymStrictShiftR = safeSymShiftRConcreteNum False

#if 1
SAFE_SYM_SHIFT_CONCRETE(Word8)
SAFE_SYM_SHIFT_CONCRETE(Word16)
SAFE_SYM_SHIFT_CONCRETE(Word32)
SAFE_SYM_SHIFT_CONCRETE(Word64)
SAFE_SYM_SHIFT_CONCRETE(Word)
SAFE_SYM_SHIFT_CONCRETE(Int8)
SAFE_SYM_SHIFT_CONCRETE(Int16)
SAFE_SYM_SHIFT_CONCRETE(Int32)
SAFE_SYM_SHIFT_CONCRETE(Int64)
SAFE_SYM_SHIFT_CONCRETE(Int)
#endif

instance
  (MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) =>
  SafeSymShift ArithException (WordN n) m
  where
  safeSymShiftL :: WordN n -> WordN n -> m (WordN n)
safeSymShiftL = Bool -> WordN n -> WordN n -> m (WordN n)
forall (m :: * -> *) a.
(MonadError ArithException m, TryMerge m, Integral a, FiniteBits a,
 Mergeable a) =>
Bool -> a -> a -> m a
safeSymShiftLConcreteNum Bool
True
  safeSymShiftR :: WordN n -> WordN n -> m (WordN n)
safeSymShiftR = Bool -> WordN n -> WordN n -> m (WordN n)
forall (m :: * -> *) a.
(MonadError ArithException m, TryMerge m, Integral a, FiniteBits a,
 Mergeable a) =>
Bool -> a -> a -> m a
safeSymShiftRConcreteNum Bool
True
  safeSymStrictShiftL :: WordN n -> WordN n -> m (WordN n)
safeSymStrictShiftL = Bool -> WordN n -> WordN n -> m (WordN n)
forall (m :: * -> *) a.
(MonadError ArithException m, TryMerge m, Integral a, FiniteBits a,
 Mergeable a) =>
Bool -> a -> a -> m a
safeSymShiftLConcreteNum Bool
False
  safeSymStrictShiftR :: WordN n -> WordN n -> m (WordN n)
safeSymStrictShiftR = Bool -> WordN n -> WordN n -> m (WordN n)
forall (m :: * -> *) a.
(MonadError ArithException m, TryMerge m, Integral a, FiniteBits a,
 Mergeable a) =>
Bool -> a -> a -> m a
safeSymShiftRConcreteNum Bool
False

instance
  (MonadError ArithException m, TryMerge m, KnownNat n, 1 <= n) =>
  SafeSymShift ArithException (IntN n) m
  where
  safeSymShiftL :: IntN n -> IntN n -> m (IntN n)
safeSymShiftL = Bool -> IntN n -> IntN n -> m (IntN n)
forall (m :: * -> *) a.
(MonadError ArithException m, TryMerge m, Integral a, FiniteBits a,
 Mergeable a) =>
Bool -> a -> a -> m a
safeSymShiftLConcreteNum Bool
True
  safeSymShiftR :: IntN n -> IntN n -> m (IntN n)
safeSymShiftR = Bool -> IntN n -> IntN n -> m (IntN n)
forall (m :: * -> *) a.
(MonadError ArithException m, TryMerge m, Integral a, FiniteBits a,
 Mergeable a) =>
Bool -> a -> a -> m a
safeSymShiftRConcreteNum Bool
True
  safeSymStrictShiftL :: IntN n -> IntN n -> m (IntN n)
safeSymStrictShiftL = Bool -> IntN n -> IntN n -> m (IntN n)
forall (m :: * -> *) a.
(MonadError ArithException m, TryMerge m, Integral a, FiniteBits a,
 Mergeable a) =>
Bool -> a -> a -> m a
safeSymShiftLConcreteNum Bool
False
  safeSymStrictShiftR :: IntN n -> IntN n -> m (IntN n)
safeSymStrictShiftR = Bool -> IntN n -> IntN n -> m (IntN n)
forall (m :: * -> *) a.
(MonadError ArithException m, TryMerge m, Integral a, FiniteBits a,
 Mergeable a) =>
Bool -> a -> a -> m a
safeSymShiftRConcreteNum Bool
False

instance
  (MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) =>
  SafeSymShift ArithException (SymWordN n) m
  where
  safeSymShiftL :: SymWordN n -> SymWordN n -> m (SymWordN n)
safeSymShiftL (SymWordN Term (WordN n)
a) (SymWordN Term (WordN n)
s) =
    SymWordN n -> m (SymWordN n)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymWordN n -> m (SymWordN n)) -> SymWordN n -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term (WordN n)
a Term (WordN n)
s
  safeSymShiftR :: SymWordN n -> SymWordN n -> m (SymWordN n)
safeSymShiftR (SymWordN Term (WordN n)
a) (SymWordN Term (WordN n)
s) =
    SymWordN n -> m (SymWordN n)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymWordN n -> m (SymWordN n)) -> SymWordN n -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term (WordN n)
a Term (WordN n)
s
  safeSymStrictShiftL :: SymWordN n -> SymWordN n -> m (SymWordN n)
safeSymStrictShiftL a :: SymWordN n
a@(SymWordN Term (WordN n)
ta) s :: SymWordN n
s@(SymWordN Term (WordN n)
ts) =
    SymBool -> m (SymWordN n) -> m (SymWordN n) -> m (SymWordN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
      (SymWordN n
s SymWordN n -> SymWordN n -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= Int -> SymWordN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SymWordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymWordN n
a))
      (ArithException -> m (SymWordN n)
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow)
      (SymWordN n -> m (SymWordN n)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymWordN n -> m (SymWordN n)) -> SymWordN n -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term (WordN n)
ta Term (WordN n)
ts)
  safeSymStrictShiftR :: SymWordN n -> SymWordN n -> m (SymWordN n)
safeSymStrictShiftR a :: SymWordN n
a@(SymWordN Term (WordN n)
ta) s :: SymWordN n
s@(SymWordN Term (WordN n)
ts) =
    SymBool -> m (SymWordN n) -> m (SymWordN n) -> m (SymWordN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
      (SymWordN n
s SymWordN n -> SymWordN n -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= Int -> SymWordN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SymWordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymWordN n
a))
      (ArithException -> m (SymWordN n)
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow)
      (SymWordN n -> m (SymWordN n)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymWordN n -> m (SymWordN n)) -> SymWordN n -> m (SymWordN n)
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term (WordN n)
ta Term (WordN n)
ts)

instance
  (MonadError ArithException m, MonadUnion m, KnownNat n, 1 <= n) =>
  SafeSymShift ArithException (SymIntN n) m
  where
  safeSymShiftL :: SymIntN n -> SymIntN n -> m (SymIntN n)
safeSymShiftL (SymIntN Term (IntN n)
a) ss :: SymIntN n
ss@(SymIntN Term (IntN n)
s) =
    SymBool -> m (SymIntN n) -> m (SymIntN n) -> m (SymIntN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
      (SymIntN n
ss SymIntN n -> SymIntN n -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< SymIntN n
0)
      (ArithException -> m (SymIntN n)
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow)
      (SymIntN n -> m (SymIntN n)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymIntN n -> m (SymIntN n)) -> SymIntN n -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term (IntN n)
a Term (IntN n)
s)
  safeSymShiftR :: SymIntN n -> SymIntN n -> m (SymIntN n)
safeSymShiftR (SymIntN Term (IntN n)
a) ss :: SymIntN n
ss@(SymIntN Term (IntN n)
s) =
    SymBool -> m (SymIntN n) -> m (SymIntN n) -> m (SymIntN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
      (SymIntN n
ss SymIntN n -> SymIntN n -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< SymIntN n
0)
      (ArithException -> m (SymIntN n)
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow)
      (SymIntN n -> m (SymIntN n)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymIntN n -> m (SymIntN n)) -> SymIntN n -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term (IntN n)
a Term (IntN n)
s)
  safeSymStrictShiftL :: SymIntN n -> SymIntN n -> m (SymIntN n)
safeSymStrictShiftL a :: SymIntN n
a@(SymIntN Term (IntN n)
ta) s :: SymIntN n
s@(SymIntN Term (IntN n)
ts) =
    SymBool -> m (SymIntN n) -> m (SymIntN n) -> m (SymIntN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
      (SymIntN n
s SymIntN n -> SymIntN n -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| (SymIntN n
bs SymIntN n -> SymIntN n -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
s SymIntN n -> SymIntN n -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= SymIntN n
bs))
      (ArithException -> m (SymIntN n)
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow)
      (SymIntN n -> m (SymIntN n)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymIntN n -> m (SymIntN n)) -> SymIntN n -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term (IntN n)
ta Term (IntN n)
ts)
    where
      bs :: SymIntN n
bs = Int -> SymIntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
a)
  safeSymStrictShiftR :: SymIntN n -> SymIntN n -> m (SymIntN n)
safeSymStrictShiftR a :: SymIntN n
a@(SymIntN Term (IntN n)
ta) s :: SymIntN n
s@(SymIntN Term (IntN n)
ts) =
    SymBool -> m (SymIntN n) -> m (SymIntN n) -> m (SymIntN n)
forall (u :: * -> *) a.
(SymBranching u, Mergeable a) =>
SymBool -> u a -> u a -> u a
mrgIf
      (SymIntN n
s SymIntN n -> SymIntN n -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.< SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.|| (SymIntN n
bs SymIntN n -> SymIntN n -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= SymIntN n
0 SymBool -> SymBool -> SymBool
forall b. LogicalOp b => b -> b -> b
.&& SymIntN n
s SymIntN n -> SymIntN n -> SymBool
forall a. SymOrd a => a -> a -> SymBool
.>= SymIntN n
bs))
      (ArithException -> m (SymIntN n)
forall a. ArithException -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArithException
Overflow)
      (SymIntN n -> m (SymIntN n)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SymIntN n -> m (SymIntN n)) -> SymIntN n -> m (SymIntN n)
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term (IntN n)
ta Term (IntN n)
ts)
    where
      bs :: SymIntN n
bs = Int -> SymIntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
a)