{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}
module Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
( pattern BitsConTerm,
pevalAndBitsTerm,
pevalOrBitsTerm,
pevalXorBitsTerm,
pevalComplementBitsTerm,
pevalShiftLeftTerm,
pevalShiftRightTerm,
pevalRotateLeftTerm,
pevalRotateRightTerm,
)
where
import Data.Bits
( Bits
( complement,
isSigned,
rotateR,
shiftR,
xor,
zeroBits,
(.&.),
(.|.)
),
FiniteBits (finiteBitSize),
)
import Data.Typeable (Typeable, cast)
import Grisette.Core.Data.Class.SymRotate (SymRotate (symRotate))
import Grisette.Core.Data.Class.SymShift (SymShift (symShift))
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
( andBitsTerm,
complementBitsTerm,
conTerm,
orBitsTerm,
rotateLeftTerm,
rotateRightTerm,
shiftLeftTerm,
shiftRightTerm,
xorBitsTerm,
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( SupportedPrim,
Term
( ComplementBitsTerm,
ConTerm
),
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold
( binaryUnfoldOnce,
unaryUnfoldOnce,
)
bitsConTermView :: (Bits b, Typeable b) => Term a -> Maybe b
bitsConTermView :: forall b a. (Bits b, Typeable b) => Term a -> Maybe b
bitsConTermView (ConTerm Id
_ a
b) = a -> Maybe b
forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
b
bitsConTermView Term a
_ = Maybe b
forall a. Maybe a
Nothing
pattern BitsConTerm :: forall b a. (Bits b, Typeable b) => b -> Term a
pattern $mBitsConTerm :: forall {r} {b} {a}.
(Bits b, Typeable b) =>
Term a -> (b -> r) -> ((# #) -> r) -> r
BitsConTerm b <- (bitsConTermView -> Just b)
pevalAndBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAndBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAndBitsTerm = PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
(Bits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalAndBitsTerm TotalRuleBinary a a a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
andBitsTerm
doPevalAndBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalAndBitsTerm :: forall a.
(Bits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalAndBitsTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a
a a -> a -> a
forall a. Bits a => a -> a -> a
.&. a
b)
doPevalAndBitsTerm (ConTerm Id
_ a
a) Term a
b
| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
forall a. Bits a => a
zeroBits
| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Bits a => a -> a
complement a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
b
doPevalAndBitsTerm Term a
a (ConTerm Id
_ a
b)
| a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
forall a. Bits a => a
zeroBits
| a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Bits a => a -> a
complement a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalAndBitsTerm Term a
a Term a
b | Term a
a Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
b = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalAndBitsTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing
pevalOrBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalOrBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalOrBitsTerm = PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
(Bits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalOrBitsTerm TotalRuleBinary a a a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
orBitsTerm
doPevalOrBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalOrBitsTerm :: forall a.
(Bits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalOrBitsTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a
a a -> a -> a
forall a. Bits a => a -> a -> a
.|. a
b)
doPevalOrBitsTerm (ConTerm Id
_ a
a) Term a
b
| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
b
| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Bits a => a -> a
complement a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Bits a => a -> a
complement a
forall a. Bits a => a
zeroBits
doPevalOrBitsTerm Term a
a (ConTerm Id
_ a
b)
| a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
| a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Bits a => a -> a
complement a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Bits a => a -> a
complement a
forall a. Bits a => a
zeroBits
doPevalOrBitsTerm Term a
a Term a
b | Term a
a Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
b = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalOrBitsTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing
pevalXorBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm = PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall a.
(Bits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalXorBitsTerm TotalRuleBinary a a a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a -> Term a
xorBitsTerm
doPevalXorBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalXorBitsTerm :: forall a.
(Bits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalXorBitsTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
b) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a
a a -> a -> a
forall a. Bits a => a -> a -> a
`xor` a
b)
doPevalXorBitsTerm (ConTerm Id
_ a
a) Term a
b
| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
b
| a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Bits a => a -> a
complement a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm Term a
b
doPevalXorBitsTerm Term a
a (ConTerm Id
_ a
b)
| a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
| a
b a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a -> a
forall a. Bits a => a -> a
complement a
forall a. Bits a => a
zeroBits = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm Term a
a
doPevalXorBitsTerm Term a
a Term a
b | Term a
a Term a -> Term a -> Bool
forall a. Eq a => a -> a -> Bool
== Term a
b = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
forall a. Bits a => a
zeroBits
doPevalXorBitsTerm (ComplementBitsTerm Id
_ Term a
i) (ComplementBitsTerm Id
_ Term a
j) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm Term a
i Term a
j
doPevalXorBitsTerm (ComplementBitsTerm Id
_ Term a
i) Term a
j = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm Term a
i Term a
j
doPevalXorBitsTerm Term a
i (ComplementBitsTerm Id
_ Term a
j) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm (Term a -> Term a) -> Term a -> Term a
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm Term a
i Term a
j
doPevalXorBitsTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing
pevalComplementBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm = PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary a a
forall a. (Bits a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalComplementBitsTerm TotalRuleUnary a a
forall a. (SupportedPrim a, Bits a) => Term a -> Term a
complementBitsTerm
doPevalComplementBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalComplementBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalComplementBitsTerm (ConTerm Id
_ a
a) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Bits a => a -> a
complement a
a
doPevalComplementBitsTerm (ComplementBitsTerm Id
_ Term a
a) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
a
doPevalComplementBitsTerm Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing
pevalShiftLeftTerm :: forall a. (Integral a, SymShift a, FiniteBits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalShiftLeftTerm :: forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftLeftTerm Term a
t Term a
n = PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (Term a -> PartialRuleUnary a a
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
`doPevalShiftLeftTerm` Term a
n) (Term a -> TotalRuleUnary a a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymShift a) =>
Term a -> Term a -> Term a
`shiftLeftTerm` Term a
n) Term a
t
doPevalShiftLeftTerm :: forall a. (Integral a, SymShift a, FiniteBits a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalShiftLeftTerm :: forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalShiftLeftTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
n)
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 =
if (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Id -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a -> Id
forall b. FiniteBits b => b -> Id
finiteBitSize a
n)
then Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
forall a. Bits a => a
zeroBits
else Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. SymShift a => a -> a -> a
symShift a
a a
n
doPevalShiftLeftTerm Term a
x (ConTerm Id
_ a
0) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
doPevalShiftLeftTerm Term a
_ (ConTerm Id
_ a
n)
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Id -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a -> Id
forall b. FiniteBits b => b -> Id
finiteBitSize a
n) =
Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
forall a. Bits a => a
zeroBits
doPevalShiftLeftTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing
pevalShiftRightTerm :: forall a. (Integral a, SymShift a, FiniteBits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalShiftRightTerm :: forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalShiftRightTerm Term a
t Term a
n = PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (Term a -> PartialRuleUnary a a
forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
`doPevalShiftRightTerm` Term a
n) (Term a -> TotalRuleUnary a a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymShift a) =>
Term a -> Term a -> Term a
`shiftRightTerm` Term a
n) Term a
t
doPevalShiftRightTerm :: forall a. (Integral a, SymShift a, FiniteBits a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalShiftRightTerm :: forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalShiftRightTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
n)
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> Bool
forall a. Bits a => a -> Bool
isSigned a
a) =
if (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Id -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a -> Id
forall b. FiniteBits b => b -> Id
finiteBitSize a
n)
then Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
forall a. Bits a => a
zeroBits
else Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> Id -> a
forall a. Bits a => a -> Id -> a
shiftR a
a (a -> Id
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n)
doPevalShiftRightTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
n)
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. SymShift a => a -> a -> a
symShift a
a (-a
n)
doPevalShiftRightTerm Term a
x (ConTerm Id
_ a
0) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
doPevalShiftRightTerm Term a
_ (ConTerm Id
_ a
n)
| Bool -> Bool
not (a -> Bool
forall a. Bits a => a -> Bool
isSigned a
n)
Bool -> Bool -> Bool
&& (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Id -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a -> Id
forall b. FiniteBits b => b -> Id
finiteBitSize a
n) =
Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
forall a. Bits a => a
zeroBits
doPevalShiftRightTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing
pevalRotateLeftTerm :: forall a. (Integral a, SymRotate a, FiniteBits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalRotateLeftTerm :: forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateLeftTerm Term a
t Term a
n = PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (Term a -> PartialRuleUnary a a
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
`doPevalRotateLeftTerm` Term a
n) (Term a -> TotalRuleUnary a a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymRotate a) =>
Term a -> Term a -> Term a
`rotateLeftTerm` Term a
n) Term a
t
doPevalRotateLeftTerm :: forall a. (Integral a, SymRotate a, FiniteBits a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalRotateLeftTerm :: forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalRotateLeftTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
n)
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> a -> a
forall a. SymRotate a => a -> a -> a
symRotate a
a a
n
doPevalRotateLeftTerm Term a
x (ConTerm Id
_ a
0) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
doPevalRotateLeftTerm Term a
x (ConTerm Id
_ a
n)
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Id -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
bs =
Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateLeftTerm Term a
x (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
n a -> a -> a
forall a. Integral a => a -> a -> a
`mod` Id -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
bs)
where
bs :: Id
bs = a -> Id
forall b. FiniteBits b => b -> Id
finiteBitSize a
n
doPevalRotateLeftTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing
pevalRotateRightTerm :: forall a. (Integral a, SymRotate a, FiniteBits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalRotateRightTerm :: forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateRightTerm Term a
t Term a
n = PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (Term a -> PartialRuleUnary a a
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
`doPevalRotateRightTerm` Term a
n) (Term a -> TotalRuleUnary a a
forall a.
(SupportedPrim a, Integral a, FiniteBits a, SymRotate a) =>
Term a -> Term a -> Term a
`rotateRightTerm` Term a
n) Term a
t
doPevalRotateRightTerm :: forall a. (Integral a, SymRotate a, FiniteBits a, SupportedPrim a) => Term a -> Term a -> Maybe (Term a)
doPevalRotateRightTerm :: forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalRotateRightTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
n)
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 =
Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> (a -> Term a) -> a -> Maybe (Term a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Maybe (Term a)) -> a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$
a -> Id -> a
forall a. Bits a => a -> Id -> a
rotateR
a
a
( Integer -> Id
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Id) -> Integer -> Id
forall a b. (a -> b) -> a -> b
$
(a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n :: Integer)
Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Id -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a -> Id
forall b. FiniteBits b => b -> Id
finiteBitSize a
n)
)
doPevalRotateRightTerm Term a
x (ConTerm Id
_ a
0) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
doPevalRotateRightTerm Term a
x (ConTerm Id
_ a
n)
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
0 Bool -> Bool -> Bool
&& (a -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
n :: Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Id -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
bs =
Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just (Term a -> Maybe (Term a)) -> Term a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term a
forall a.
(Integral a, SymRotate a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Term a
pevalRotateRightTerm Term a
x (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a
n a -> a -> a
forall a. Integral a => a -> a -> a
`mod` Id -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Id
bs)
where
bs :: Id
bs = a -> Id
forall b. FiniteBits b => b -> Id
finiteBitSize a
n
doPevalRotateRightTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing