{-# 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
( 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,
)
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
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
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)
| 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 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