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

-- 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
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
-- TODO: Need to handle the overflow case.
-- doPevalShiftLeftTerm (ShiftLeftTerm _ x (ConTerm _ n)) (ConTerm _ n1)
--   | n >= 0 && n1 >= 0 = Just $ pevalShiftLeftTerm x (conTerm $ n + n1)
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) -- if n >= 0 then -n must be in the range
doPevalShiftRightTerm Term a
x (ConTerm Id
_ a
0) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
-- doPevalShiftRightTerm (ShiftRightTerm _ x (ConTerm _ n)) (ConTerm _ n1)
--   | n >= 0 && n1 >= 0 = Just $ pevalShiftRightTerm x (conTerm $ n + n1)
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 -- Just $ conTerm $ rotateL a (fromIntegral n)
doPevalRotateLeftTerm Term a
x (ConTerm Id
_ a
0) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
-- doPevalRotateLeftTerm (RotateLeftTerm _ x (ConTerm _ n)) (ConTerm _ n1)
--   | n >= 0 && n1 >= 0 = Just $ pevalRotateLeftTerm x (conTerm $ n + n1)
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 (RotateRightTerm _ x (ConTerm _ n)) (ConTerm _ n1)
--   | n >= 0 && n1 >= 0 = Just $ pevalRotateRightTerm x (conTerm $ n + n1)
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