{-# 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) = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast a
b
bitsConTermView Term a
_ = 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 = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(Bits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalAndBitsTerm 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) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a
a forall a. Bits a => a -> a -> a
.&. a
b)
doPevalAndBitsTerm (ConTerm Id
_ a
a) Term a
b
  | a
a forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a. Bits a => a
zeroBits
  | a
a forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a -> a
complement forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just Term a
b
doPevalAndBitsTerm Term a
a (ConTerm Id
_ a
b)
  | a
b forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a. Bits a => a
zeroBits
  | a
b forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a -> a
complement forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just Term a
a
doPevalAndBitsTerm Term a
a Term a
b | Term a
a forall a. Eq a => a -> a -> Bool
== Term a
b = forall a. a -> Maybe a
Just Term a
a
doPevalAndBitsTerm Term a
_ 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 = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(Bits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalOrBitsTerm 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) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a
a forall a. Bits a => a -> a -> a
.|. a
b)
doPevalOrBitsTerm (ConTerm Id
_ a
a) Term a
b
  | a
a forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just Term a
b
  | a
a forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a -> a
complement forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> a
complement forall a. Bits a => a
zeroBits
doPevalOrBitsTerm Term a
a (ConTerm Id
_ a
b)
  | a
b forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just Term a
a
  | a
b forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a -> a
complement forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> a
complement forall a. Bits a => a
zeroBits
doPevalOrBitsTerm Term a
a Term a
b | Term a
a forall a. Eq a => a -> a -> Bool
== Term a
b = forall a. a -> Maybe a
Just Term a
a
doPevalOrBitsTerm Term a
_ 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 = forall a b c.
(Typeable a, Typeable b, SupportedPrim c) =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce forall a.
(Bits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalXorBitsTerm 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) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (a
a forall a. Bits a => a -> a -> a
`xor` a
b)
doPevalXorBitsTerm (ConTerm Id
_ a
a) Term a
b
  | a
a forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just Term a
b
  | a
a forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a -> a
complement forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm Term a
b
doPevalXorBitsTerm Term a
a (ConTerm Id
_ a
b)
  | a
b forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just Term a
a
  | a
b forall a. Eq a => a -> a -> Bool
== forall a. Bits a => a -> a
complement forall a. Bits a => a
zeroBits = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm Term a
a
doPevalXorBitsTerm Term a
a Term a
b | Term a
a forall a. Eq a => a -> a -> Bool
== Term a
b = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a. Bits a => a
zeroBits
doPevalXorBitsTerm (ComplementBitsTerm Id
_ Term a
i) (ComplementBitsTerm Id
_ Term a
j) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm forall a b. (a -> b) -> a -> b
$ 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) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm Term a
i Term a
j
doPevalXorBitsTerm Term a
_ 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 = forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce forall a. (Bits a, SupportedPrim a) => Term a -> Maybe (Term a)
doPevalComplementBitsTerm 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) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> a
complement a
a
doPevalComplementBitsTerm (ComplementBitsTerm Id
_ Term a
a) = forall a. a -> Maybe a
Just Term a
a
doPevalComplementBitsTerm 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 = forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (forall a.
(Bits a, SupportedPrim a) =>
Term a -> Id -> Maybe (Term a)
`doPevalShiftBitsTerm` Id
n) (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 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Id -> a
shift a
a Id
n
doPevalShiftBitsTerm Term a
x Id
0 = forall a. a -> Maybe a
Just Term a
x
doPevalShiftBitsTerm Term a
_ Id
a
  | case forall a. Bits a => a -> Maybe Id
bitSizeMaybe (forall a. Bits a => a
zeroBits :: a) of
      Just Id
b -> Id
a forall a. Ord a => a -> a -> Bool
>= Id
b
      Maybe Id
Nothing -> Bool
False =
      forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a. Bits a => a
zeroBits
doPevalShiftBitsTerm (ShiftBitsTerm Id
_ Term a
x Id
n) Id
n1
  | (Id
n forall a. Ord a => a -> a -> Bool
>= Id
0 Bool -> Bool -> Bool
&& Id
n1 forall a. Ord a => a -> a -> Bool
>= Id
0) Bool -> Bool -> Bool
|| (Id
n forall a. Ord a => a -> a -> Bool
<= Id
0 Bool -> Bool -> Bool
&& Id
n1 forall a. Ord a => a -> a -> Bool
<= Id
0) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Bits a) => Term a -> Id -> Term a
shiftBitsTerm Term a
x (Id
n forall a. Num a => a -> a -> a
+ Id
n1)
doPevalShiftBitsTerm Term a
_ Id
_ = 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 = forall a b.
(Typeable a, SupportedPrim b) =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce (forall a.
(Bits a, SupportedPrim a) =>
Term a -> Id -> Maybe (Term a)
`doPevalRotateBitsTerm` Id
n) (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 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Id -> a
rotate a
a Id
n
doPevalRotateBitsTerm Term a
x Id
0 = 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 forall a. Eq a => a -> a -> Bool
/= Id
0 Bool -> Bool -> Bool
&& (Id
a forall a. Ord a => a -> a -> Bool
>= Id
s Bool -> Bool -> Bool
|| Id
a forall a. Ord a => a -> a -> Bool
< Id
0)
      Maybe Id
Nothing -> Bool
False = do
      Id
cbsize <- Maybe Id
bsize
      if Id
a forall a. Ord a => a -> a -> Bool
>= Id
cbsize
        then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Id -> Term a
pevalRotateBitsTerm Term a
x (Id
a forall a. Num a => a -> a -> a
- Id
cbsize)
        else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (Bits a, SupportedPrim a) => Term a -> Id -> Term a
pevalRotateBitsTerm Term a
x (Id
a forall a. Num a => a -> a -> a
+ Id
cbsize)
  where
    bsize :: Maybe Id
bsize = forall a. Bits a => a -> Maybe Id
bitSizeMaybe (forall a. Bits a => a
zeroBits :: a)
doPevalRotateBitsTerm (RotateBitsTerm Id
_ Term a
x Id
n) Id
n1 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. (SupportedPrim a, Bits a) => Term a -> Id -> Term a
rotateBitsTerm Term a
x (Id
n forall a. Num a => a -> a -> a
+ Id
n1)
doPevalRotateBitsTerm Term a
_ Id
_ = forall a. Maybe a
Nothing