{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
-- 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.IR.SymPrim.Data.Prim.PartialEval.Bits
  ( pattern BitsConTerm,
    pevalAndBitsTerm,
    pevalOrBitsTerm,
    pevalXorBitsTerm,
    pevalComplementBitsTerm,
    pevalShiftBitsTerm,
    pevalRotateBitsTerm,
  )
where

import Data.Bits
import Data.Typeable
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Unfold

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) -> (Void# -> r) -> r
BitsConTerm b <- (bitsConTermView -> Just b)

-- bitand
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

-- bitor
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

-- bitxor
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

-- complement
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

-- shift
pevalShiftBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
pevalShiftBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Id -> Term a
pevalShiftBitsTerm Term a
t Id
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 -> Id -> Maybe (Term a)
forall a.
(Bits a, SupportedPrim a) =>
Term a -> Id -> Maybe (Term a)
`doPevalShiftBitsTerm` Id
n) (Term a -> Id -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Id -> Term a
`shiftBitsTerm` Id
n) Term a
t

doPevalShiftBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Maybe (Term a)
doPevalShiftBitsTerm :: forall a.
(Bits a, SupportedPrim a) =>
Term a -> Id -> Maybe (Term a)
doPevalShiftBitsTerm (ConTerm Id
_ a
a) Id
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 -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> Id -> a
forall a. Bits a => a -> Id -> a
shift a
a Id
n
doPevalShiftBitsTerm Term a
x Id
0 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
doPevalShiftBitsTerm Term a
_ Id
a
  | case a -> Maybe Id
forall a. Bits a => a -> Maybe Id
bitSizeMaybe (a
forall a. Bits a => a
zeroBits :: a) of
      Just Id
b -> Id
a Id -> Id -> Bool
forall a. Ord a => a -> a -> Bool
>= Id
b
      Maybe Id
Nothing -> Bool
False =
      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
doPevalShiftBitsTerm (ShiftBitsTerm Id
_ Term a
x Id
n) Id
n1
  | (Id
n Id -> Id -> Bool
forall a. Ord a => a -> a -> Bool
>= Id
0 Bool -> Bool -> Bool
&& Id
n1 Id -> Id -> Bool
forall a. Ord a => a -> a -> Bool
>= Id
0) Bool -> Bool -> Bool
|| (Id
n Id -> Id -> Bool
forall a. Ord a => a -> a -> Bool
<= Id
0 Bool -> Bool -> Bool
&& Id
n1 Id -> Id -> Bool
forall a. Ord a => a -> a -> Bool
<= Id
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
$ Term a -> Id -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Id -> Term a
shiftBitsTerm Term a
x (Id
n Id -> Id -> Id
forall a. Num a => a -> a -> a
+ Id
n1)
doPevalShiftBitsTerm Term a
_ Id
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- rotate
pevalRotateBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
pevalRotateBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Id -> Term a
pevalRotateBitsTerm Term a
t Id
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 -> Id -> Maybe (Term a)
forall a.
(Bits a, SupportedPrim a) =>
Term a -> Id -> Maybe (Term a)
`doPevalRotateBitsTerm` Id
n) (Term a -> Id -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Id -> Term a
`rotateBitsTerm` Id
n) Term a
t

doPevalRotateBitsTerm :: forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Maybe (Term a)
doPevalRotateBitsTerm :: forall a.
(Bits a, SupportedPrim a) =>
Term a -> Id -> Maybe (Term a)
doPevalRotateBitsTerm (ConTerm Id
_ a
a) Id
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 -> Term a) -> a -> Term a
forall a b. (a -> b) -> a -> b
$ a -> Id -> a
forall a. Bits a => a -> Id -> a
rotate a
a Id
n
doPevalRotateBitsTerm Term a
x Id
0 = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
doPevalRotateBitsTerm Term a
x Id
a
  | case Maybe Id
bsize of
      Just Id
s -> Id
s Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
/= Id
0 Bool -> Bool -> Bool
&& (Id
a Id -> Id -> Bool
forall a. Ord a => a -> a -> Bool
>= Id
s Bool -> Bool -> Bool
|| Id
a Id -> Id -> Bool
forall a. Ord a => a -> a -> Bool
< Id
0)
      Maybe Id
Nothing -> Bool
False = do
      Id
cbsize <- Maybe Id
bsize
      if Id
a Id -> Id -> Bool
forall a. Ord a => a -> a -> Bool
>= Id
cbsize
        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
$ Term a -> Id -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Id -> Term a
pevalRotateBitsTerm Term a
x (Id
a Id -> Id -> Id
forall a. Num a => a -> a -> a
- Id
cbsize)
        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
$ Term a -> Id -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Id -> Term a
pevalRotateBitsTerm Term a
x (Id
a Id -> Id -> Id
forall a. Num a => a -> a -> a
+ Id
cbsize)
  where
    bsize :: Maybe Id
bsize = a -> Maybe Id
forall a. Bits a => a -> Maybe Id
bitSizeMaybe (a
forall a. Bits a => a
zeroBits :: a)
doPevalRotateBitsTerm (RotateBitsTerm Id
_ Term a
x Id
n) Id
n1 = 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 -> Id -> Term a
forall a. (SupportedPrim a, Bits a) => Term a -> Id -> Term a
rotateBitsTerm Term a
x (Id
n Id -> Id -> Id
forall a. Num a => a -> a -> a
+ Id
n1)
doPevalRotateBitsTerm Term a
_ Id
_ = Maybe (Term a)
forall a. Maybe a
Nothing