{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm
-- 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.SymPrim.Prim.Internal.Instances.PEvalShiftTerm
  ( pevalFiniteBitsSymShiftShiftLeftTerm,
    pevalFiniteBitsSymShiftShiftRightTerm,
  )
where

import Data.Bits (Bits (isSigned, shiftR, zeroBits), FiniteBits (finiteBitSize))
import Data.Proxy (Proxy (Proxy))
import Data.Typeable ((:~:) (Refl))
import GHC.TypeLits (KnownNat, type (+), type (<=))
import Grisette.Internal.Core.Data.Class.SymShift (SymShift (symShift))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalBVTerm (pevalBVConcatTerm, pevalBVExtendTerm),
    PEvalShiftTerm
      ( pevalShiftLeftTerm,
        pevalShiftRightTerm,
        withSbvShiftTermConstraint
      ),
    SupportedNonFuncPrim (withNonFuncPrim),
    SupportedPrim,
    Term,
    bvIsNonZeroFromGEq1,
    conTerm,
    shiftLeftTerm,
    shiftRightTerm,
    unsafePevalBVSelectTerm,
    pattern ConTerm,
    pattern SupportedTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (unaryUnfoldOnce)
import Grisette.Internal.Utils.Parameterized
  ( LeqProof (LeqProof),
    NatRepr,
    SomePositiveNatRepr (SomePositiveNatRepr),
    mkPositiveNatRepr,
    natRepr,
    subNat,
    unsafeAxiom,
    unsafeLeqProof,
  )

-- | Partial evaluation of symbolic shift left term for finite bits types.
pevalFiniteBitsSymShiftShiftLeftTerm ::
  forall bv n.
  ( forall m. (KnownNat m, 1 <= m) => Integral (bv m),
    forall m. (KnownNat m, 1 <= m) => SymShift (bv m),
    forall m. (KnownNat m, 1 <= m) => SupportedPrim (bv m),
    forall m. (KnownNat m, 1 <= m) => PEvalShiftTerm (bv m),
    PEvalBVTerm bv,
    KnownNat n,
    1 <= n
  ) =>
  Term (bv n) ->
  Term (bv n) ->
  Term (bv n)
pevalFiniteBitsSymShiftShiftLeftTerm :: forall (bv :: Natural -> *) (n :: Natural).
(forall (m :: Natural). (KnownNat m, 1 <= m) => Integral (bv m),
 forall (m :: Natural). (KnownNat m, 1 <= m) => SymShift (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 SupportedPrim (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 PEvalShiftTerm (bv m),
 PEvalBVTerm bv, KnownNat n, 1 <= n) =>
Term (bv n) -> Term (bv n) -> Term (bv n)
pevalFiniteBitsSymShiftShiftLeftTerm t :: Term (bv n)
t@Term (bv n)
SupportedTerm Term (bv n)
n =
  PartialRuleUnary (bv n) (bv n)
-> TotalRuleUnary (bv n) (bv n) -> TotalRuleUnary (bv n) (bv n)
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce
    (Term (bv n) -> PartialRuleUnary (bv n) (bv n)
forall (bv :: Natural -> *) (n :: Natural).
(forall (m :: Natural). (KnownNat m, 1 <= m) => Integral (bv m),
 forall (m :: Natural). (KnownNat m, 1 <= m) => SymShift (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 SupportedPrim (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 PEvalShiftTerm (bv m),
 PEvalBVTerm bv, KnownNat n, 1 <= n) =>
Term (bv n) -> Term (bv n) -> Maybe (Term (bv n))
`doPevalFiniteBitsSymShiftShiftLeftTerm` Term (bv n)
n)
    (Term (bv n) -> TotalRuleUnary (bv n) (bv n)
forall a. PEvalShiftTerm a => Term a -> Term a -> Term a
`shiftLeftTerm` Term (bv n)
n)
    Term (bv n)
t

doPevalFiniteBitsSymShiftShiftLeftTerm ::
  forall bv n.
  ( forall m. (KnownNat m, 1 <= m) => Integral (bv m),
    forall m. (KnownNat m, 1 <= m) => SymShift (bv m),
    forall m. (KnownNat m, 1 <= m) => SupportedPrim (bv m),
    forall m. (KnownNat m, 1 <= m) => PEvalShiftTerm (bv m),
    PEvalBVTerm bv,
    KnownNat n,
    1 <= n
  ) =>
  Term (bv n) ->
  Term (bv n) ->
  Maybe (Term (bv n))
doPevalFiniteBitsSymShiftShiftLeftTerm :: forall (bv :: Natural -> *) (n :: Natural).
(forall (m :: Natural). (KnownNat m, 1 <= m) => Integral (bv m),
 forall (m :: Natural). (KnownNat m, 1 <= m) => SymShift (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 SupportedPrim (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 PEvalShiftTerm (bv m),
 PEvalBVTerm bv, KnownNat n, 1 <= n) =>
Term (bv n) -> Term (bv n) -> Maybe (Term (bv n))
doPevalFiniteBitsSymShiftShiftLeftTerm (ConTerm bv n
a) (ConTerm bv n
n)
  | bv n
n bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
>= bv n
0 =
      if (bv n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral bv n
n :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (bv n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize bv n
n)
        then Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just (Term (bv n) -> Maybe (Term (bv n)))
-> Term (bv n) -> Maybe (Term (bv n))
forall a b. (a -> b) -> a -> b
$ bv n -> Term (bv n)
forall t. SupportedPrim t => t -> Term t
conTerm bv n
forall a. Bits a => a
zeroBits
        else Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just (Term (bv n) -> Maybe (Term (bv n)))
-> Term (bv n) -> Maybe (Term (bv n))
forall a b. (a -> b) -> a -> b
$ bv n -> Term (bv n)
forall t. SupportedPrim t => t -> Term t
conTerm (bv n -> Term (bv n)) -> bv n -> Term (bv n)
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> bv n
forall a. SymShift a => a -> a -> a
symShift bv n
a bv n
n
doPevalFiniteBitsSymShiftShiftLeftTerm Term (bv n)
x (ConTerm bv n
0) = Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just Term (bv n)
x
-- TODO: Need to handle the overflow case.
-- doPevalShiftLeftTerm (ShiftLeftTerm _ x (ConTerm  n)) (ConTerm  n1)
--   | n >= 0 && n1 >= 0 = Just $ pevalShiftLeftTerm x (conTerm $ n + n1)
doPevalFiniteBitsSymShiftShiftLeftTerm Term (bv n)
_ (ConTerm bv n
n)
  | bv n
n bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
> bv n
0 Bool -> Bool -> Bool
&& (bv n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral bv n
n :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (bv n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize bv n
n) =
      Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just (Term (bv n) -> Maybe (Term (bv n)))
-> Term (bv n) -> Maybe (Term (bv n))
forall a b. (a -> b) -> a -> b
$ bv n -> Term (bv n)
forall t. SupportedPrim t => t -> Term t
conTerm bv n
forall a. Bits a => a
zeroBits
doPevalFiniteBitsSymShiftShiftLeftTerm Term (bv n)
x (ConTerm bv n
shiftAmount)
  | bv n
shiftAmount bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
> bv n
0 =
      case (SomePositiveNatRepr
namount, SomePositiveNatRepr
nremaining) of
        ( SomePositiveNatRepr (NatRepr n
_ :: NatRepr amount),
          SomePositiveNatRepr (NatRepr n
nremaining :: NatRepr remaining)
          ) ->
            case ( forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @remaining @n,
                   forall (a :: Natural) (b :: Natural). a :~: b
forall {k} (a :: k) (b :: k). a :~: b
unsafeAxiom @(remaining + amount) @n
                 ) of
              (LeqProof n n
LeqProof, (n + n) :~: n
Refl) ->
                Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just (Term (bv n) -> Maybe (Term (bv n)))
-> Term (bv n) -> Maybe (Term (bv n))
forall a b. (a -> b) -> a -> b
$
                  Term (bv n) -> Term (bv n) -> Term (bv (n + n))
forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
pevalBVConcatTerm
                    (NatRepr n -> NatRepr 0 -> NatRepr n -> Term (bv n) -> Term (bv n)
forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm NatRepr n
nn (forall (n :: Natural). KnownNat n => NatRepr n
natRepr @0) NatRepr n
nremaining Term (bv n)
x)
                    (bv n -> Term (bv n)
forall t. SupportedPrim t => t -> Term t
conTerm bv n
forall a. Bits a => a
zeroBits :: Term (bv amount))
  where
    nn :: NatRepr n
nn = forall (n :: Natural). KnownNat n => NatRepr n
natRepr @n
    namount :: SomePositiveNatRepr
namount = Natural -> SomePositiveNatRepr
mkPositiveNatRepr (Natural -> SomePositiveNatRepr) -> Natural -> SomePositiveNatRepr
forall a b. (a -> b) -> a -> b
$ bv n -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral bv n
shiftAmount
    nremaining :: SomePositiveNatRepr
nremaining =
      Natural -> SomePositiveNatRepr
mkPositiveNatRepr (Natural -> SomePositiveNatRepr) -> Natural -> SomePositiveNatRepr
forall a b. (a -> b) -> a -> b
$
        Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (bv n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize bv n
shiftAmount) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- bv n -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral bv n
shiftAmount
doPevalFiniteBitsSymShiftShiftLeftTerm Term (bv n)
_ Term (bv n)
_ = Maybe (Term (bv n))
forall a. Maybe a
Nothing

-- | Partial evaluation of symbolic shift right term for finite bits types.
pevalFiniteBitsSymShiftShiftRightTerm ::
  forall bv n.
  ( forall m. (KnownNat m, 1 <= m) => Integral (bv m),
    forall m. (KnownNat m, 1 <= m) => SymShift (bv m),
    forall m. (KnownNat m, 1 <= m) => SupportedPrim (bv m),
    forall m. (KnownNat m, 1 <= m) => PEvalShiftTerm (bv m),
    PEvalBVTerm bv,
    KnownNat n,
    1 <= n
  ) =>
  Term (bv n) ->
  Term (bv n) ->
  Term (bv n)
pevalFiniteBitsSymShiftShiftRightTerm :: forall (bv :: Natural -> *) (n :: Natural).
(forall (m :: Natural). (KnownNat m, 1 <= m) => Integral (bv m),
 forall (m :: Natural). (KnownNat m, 1 <= m) => SymShift (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 SupportedPrim (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 PEvalShiftTerm (bv m),
 PEvalBVTerm bv, KnownNat n, 1 <= n) =>
Term (bv n) -> Term (bv n) -> Term (bv n)
pevalFiniteBitsSymShiftShiftRightTerm t :: Term (bv n)
t@Term (bv n)
SupportedTerm Term (bv n)
n =
  PartialRuleUnary (bv n) (bv n)
-> TotalRuleUnary (bv n) (bv n) -> TotalRuleUnary (bv n) (bv n)
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce
    (Term (bv n) -> PartialRuleUnary (bv n) (bv n)
forall (bv :: Natural -> *) (n :: Natural).
(forall (m :: Natural). (KnownNat m, 1 <= m) => Integral (bv m),
 forall (m :: Natural). (KnownNat m, 1 <= m) => SymShift (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 SupportedPrim (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 PEvalShiftTerm (bv m),
 PEvalBVTerm bv, KnownNat n, 1 <= n) =>
Term (bv n) -> Term (bv n) -> Maybe (Term (bv n))
`doPevalFiniteBitsSymShiftShiftRightTerm` Term (bv n)
n)
    (Term (bv n) -> TotalRuleUnary (bv n) (bv n)
forall a. PEvalShiftTerm a => Term a -> Term a -> Term a
`shiftRightTerm` Term (bv n)
n)
    Term (bv n)
t

doPevalFiniteBitsSymShiftShiftRightTerm ::
  forall bv n.
  ( forall m. (KnownNat m, 1 <= m) => Integral (bv m),
    forall m. (KnownNat m, 1 <= m) => SymShift (bv m),
    forall m. (KnownNat m, 1 <= m) => SupportedPrim (bv m),
    forall m. (KnownNat m, 1 <= m) => PEvalShiftTerm (bv m),
    PEvalBVTerm bv,
    KnownNat n,
    1 <= n
  ) =>
  Term (bv n) ->
  Term (bv n) ->
  Maybe (Term (bv n))
doPevalFiniteBitsSymShiftShiftRightTerm :: forall (bv :: Natural -> *) (n :: Natural).
(forall (m :: Natural). (KnownNat m, 1 <= m) => Integral (bv m),
 forall (m :: Natural). (KnownNat m, 1 <= m) => SymShift (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 SupportedPrim (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 PEvalShiftTerm (bv m),
 PEvalBVTerm bv, KnownNat n, 1 <= n) =>
Term (bv n) -> Term (bv n) -> Maybe (Term (bv n))
doPevalFiniteBitsSymShiftShiftRightTerm (ConTerm bv n
a) (ConTerm bv n
n)
  | bv n
n bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
>= bv n
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (bv n -> Bool
forall a. Bits a => a -> Bool
isSigned bv n
a) =
      if (bv n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral bv n
n :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (bv n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize bv n
n)
        then Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just (Term (bv n) -> Maybe (Term (bv n)))
-> Term (bv n) -> Maybe (Term (bv n))
forall a b. (a -> b) -> a -> b
$ bv n -> Term (bv n)
forall t. SupportedPrim t => t -> Term t
conTerm bv n
forall a. Bits a => a
zeroBits
        else Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just (Term (bv n) -> Maybe (Term (bv n)))
-> Term (bv n) -> Maybe (Term (bv n))
forall a b. (a -> b) -> a -> b
$ bv n -> Term (bv n)
forall t. SupportedPrim t => t -> Term t
conTerm (bv n -> Term (bv n)) -> bv n -> Term (bv n)
forall a b. (a -> b) -> a -> b
$ bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
shiftR bv n
a (bv n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral bv n
n)
doPevalFiniteBitsSymShiftShiftRightTerm (ConTerm bv n
a) (ConTerm bv n
n)
  -- if n >= 0 then -n must be in the range
  | bv n
n bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
>= bv n
0 = Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just (Term (bv n) -> Maybe (Term (bv n)))
-> Term (bv n) -> Maybe (Term (bv n))
forall a b. (a -> b) -> a -> b
$ bv n -> Term (bv n)
forall t. SupportedPrim t => t -> Term t
conTerm (bv n -> Term (bv n)) -> bv n -> Term (bv n)
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> bv n
forall a. SymShift a => a -> a -> a
symShift bv n
a (-bv n
n)
doPevalFiniteBitsSymShiftShiftRightTerm Term (bv n)
x (ConTerm bv n
0) = Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just Term (bv n)
x
-- doPevalFiniteBitsSymShiftShiftRightTerm (ShiftRightTerm _ x (ConTerm  n)) (ConTerm  n1)
--   | n >= 0 && n1 >= 0 = Just $ pevalFiniteBitsSymShiftShiftRightTerm x (conTerm $ n + n1)
doPevalFiniteBitsSymShiftShiftRightTerm Term (bv n)
x (ConTerm bv n
shiftAmount)
  | Bool -> Bool
not (bv n -> Bool
forall a. Bits a => a -> Bool
isSigned bv n
shiftAmount)
      Bool -> Bool -> Bool
&& (bv n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral bv n
shiftAmount :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (bv n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize bv n
shiftAmount) =
      Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just (Term (bv n) -> Maybe (Term (bv n)))
-> Term (bv n) -> Maybe (Term (bv n))
forall a b. (a -> b) -> a -> b
$ bv n -> Term (bv n)
forall t. SupportedPrim t => t -> Term t
conTerm bv n
forall a. Bits a => a
zeroBits
  | bv n -> Bool
forall a. Bits a => a -> Bool
isSigned bv n
shiftAmount
      Bool -> Bool -> Bool
&& (bv n -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral bv n
shiftAmount :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (bv n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize bv n
shiftAmount) =
      Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just (Term (bv n) -> Maybe (Term (bv n)))
-> Term (bv n) -> Maybe (Term (bv n))
forall a b. (a -> b) -> a -> b
$ Bool -> NatRepr n -> Term (bv 1) -> Term (bv n)
forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
True NatRepr n
nn (Term (bv 1) -> Term (bv n)) -> Term (bv 1) -> Term (bv n)
forall a b. (a -> b) -> a -> b
$ NatRepr n
-> NatRepr (n - 1) -> NatRepr 1 -> Term (bv n) -> Term (bv 1)
forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm NatRepr n
nn NatRepr (n - 1)
nnp1 NatRepr 1
none Term (bv n)
x
  where
    nn :: NatRepr n
nn = forall (n :: Natural). KnownNat n => NatRepr n
natRepr @n
    none :: NatRepr 1
none = forall (n :: Natural). KnownNat n => NatRepr n
natRepr @1
    nnp1 :: NatRepr (n - 1)
nnp1 = NatRepr n -> NatRepr 1 -> NatRepr (n - 1)
forall (n :: Natural) (m :: Natural).
(n <= m) =>
NatRepr m -> NatRepr n -> NatRepr (m - n)
subNat NatRepr n
nn NatRepr 1
none
doPevalFiniteBitsSymShiftShiftRightTerm Term (bv n)
x (ConTerm bv n
shiftAmount)
  | bv n
shiftAmount bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
> bv n
0 =
      case (SomePositiveNatRepr
namount, SomePositiveNatRepr
nremaining) of
        ( SomePositiveNatRepr NatRepr n
namount,
          SomePositiveNatRepr (NatRepr n
nremaining :: NatRepr remaining)
          ) ->
            case forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @remaining @n of
              LeqProof n n
LeqProof ->
                Term (bv n) -> Maybe (Term (bv n))
forall a. a -> Maybe a
Just (Term (bv n) -> Maybe (Term (bv n)))
-> Term (bv n) -> Maybe (Term (bv n))
forall a b. (a -> b) -> a -> b
$
                  Bool -> NatRepr n -> Term (bv n) -> Term (bv n)
forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm (bv n -> Bool
forall a. Bits a => a -> Bool
isSigned bv n
shiftAmount) NatRepr n
nn (Term (bv n) -> Term (bv n)) -> Term (bv n) -> Term (bv n)
forall a b. (a -> b) -> a -> b
$
                    NatRepr n -> NatRepr n -> NatRepr n -> Term (bv n) -> Term (bv n)
forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural).
PEvalBVTerm bv =>
NatRepr n -> NatRepr ix -> NatRepr w -> Term (bv n) -> Term (bv w)
unsafePevalBVSelectTerm NatRepr n
nn NatRepr n
namount NatRepr n
nremaining Term (bv n)
x
  where
    nn :: NatRepr n
nn = forall (n :: Natural). KnownNat n => NatRepr n
natRepr @n
    namount :: SomePositiveNatRepr
namount = Natural -> SomePositiveNatRepr
mkPositiveNatRepr (Natural -> SomePositiveNatRepr) -> Natural -> SomePositiveNatRepr
forall a b. (a -> b) -> a -> b
$ bv n -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral bv n
shiftAmount
    nremaining :: SomePositiveNatRepr
nremaining =
      Natural -> SomePositiveNatRepr
mkPositiveNatRepr (Natural -> SomePositiveNatRepr) -> Natural -> SomePositiveNatRepr
forall a b. (a -> b) -> a -> b
$
        Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (bv n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize bv n
shiftAmount) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- bv n -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral bv n
shiftAmount
doPevalFiniteBitsSymShiftShiftRightTerm Term (bv n)
_ Term (bv n)
_ = Maybe (Term (bv n))
forall a. Maybe a
Nothing

instance (KnownNat n, 1 <= n) => PEvalShiftTerm (IntN n) where
  pevalShiftLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalShiftLeftTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall (bv :: Natural -> *) (n :: Natural).
(forall (m :: Natural). (KnownNat m, 1 <= m) => Integral (bv m),
 forall (m :: Natural). (KnownNat m, 1 <= m) => SymShift (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 SupportedPrim (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 PEvalShiftTerm (bv m),
 PEvalBVTerm bv, KnownNat n, 1 <= n) =>
Term (bv n) -> Term (bv n) -> Term (bv n)
pevalFiniteBitsSymShiftShiftLeftTerm
  pevalShiftRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalShiftRightTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall (bv :: Natural -> *) (n :: Natural).
(forall (m :: Natural). (KnownNat m, 1 <= m) => Integral (bv m),
 forall (m :: Natural). (KnownNat m, 1 <= m) => SymShift (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 SupportedPrim (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 PEvalShiftTerm (bv m),
 PEvalBVTerm bv, KnownNat n, 1 <= n) =>
Term (bv n) -> Term (bv n) -> Term (bv n)
pevalFiniteBitsSymShiftShiftRightTerm
  withSbvShiftTermConstraint :: forall r. (SIntegral (NonFuncSBVBaseType (IntN n)) => r) -> r
withSbvShiftTermConstraint SIntegral (NonFuncSBVBaseType (IntN n)) => r
r =
    Proxy n -> (BVIsNonZero n => r) -> r
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => r) -> r) -> (BVIsNonZero n => r) -> r
forall a b. (a -> b) -> a -> b
$
      forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @(IntN n) r
NonFuncPrimConstraint (IntN n) => r
SIntegral (NonFuncSBVBaseType (IntN n)) => r
r

instance (KnownNat n, 1 <= n) => PEvalShiftTerm (WordN n) where
  pevalShiftLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalShiftLeftTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall (bv :: Natural -> *) (n :: Natural).
(forall (m :: Natural). (KnownNat m, 1 <= m) => Integral (bv m),
 forall (m :: Natural). (KnownNat m, 1 <= m) => SymShift (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 SupportedPrim (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 PEvalShiftTerm (bv m),
 PEvalBVTerm bv, KnownNat n, 1 <= n) =>
Term (bv n) -> Term (bv n) -> Term (bv n)
pevalFiniteBitsSymShiftShiftLeftTerm
  pevalShiftRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalShiftRightTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall (bv :: Natural -> *) (n :: Natural).
(forall (m :: Natural). (KnownNat m, 1 <= m) => Integral (bv m),
 forall (m :: Natural). (KnownNat m, 1 <= m) => SymShift (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 SupportedPrim (bv m),
 forall (m :: Natural).
 (KnownNat m, 1 <= m) =>
 PEvalShiftTerm (bv m),
 PEvalBVTerm bv, KnownNat n, 1 <= n) =>
Term (bv n) -> Term (bv n) -> Term (bv n)
pevalFiniteBitsSymShiftShiftRightTerm
  withSbvShiftTermConstraint :: forall r. (SIntegral (NonFuncSBVBaseType (WordN n)) => r) -> r
withSbvShiftTermConstraint SIntegral (NonFuncSBVBaseType (WordN n)) => r
r =
    Proxy n -> (BVIsNonZero n => r) -> r
forall (w :: Natural) r (proxy :: Natural -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) ((BVIsNonZero n => r) -> r) -> (BVIsNonZero n => r) -> r
forall a b. (a -> b) -> a -> b
$
      forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @(WordN n) r
NonFuncPrimConstraint (WordN n) => r
SIntegral (NonFuncSBVBaseType (WordN n)) => r
r