{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalRotateTerm
  ( pevalFiniteBitsSymRotateRotateLeftTerm,
    pevalFiniteBitsSymRotateRotateRightTerm,
  )
where

import Data.Bits (Bits (rotateR), FiniteBits (finiteBitSize))
import Data.Proxy (Proxy (Proxy))
import qualified Data.SBV as SBV
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.Core.Data.Class.SymRotate (SymRotate (symRotate))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim (bvIsNonZeroFromGEq1)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalRotateTerm
      ( pevalRotateLeftTerm,
        pevalRotateRightTerm,
        sbvRotateLeftTerm,
        sbvRotateRightTerm,
        withSbvRotateTermConstraint
      ),
    SupportedNonFuncPrim (withNonFuncPrim),
    Term,
    conTerm,
    rotateLeftTerm,
    rotateRightTerm,
    pattern ConTerm,
    pattern SupportedTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (unaryUnfoldOnce)

-- | Partial evaluation of symbolic rotate left term for finite bits types.
pevalFiniteBitsSymRotateRotateLeftTerm ::
  forall a.
  (Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
  Term a ->
  Term a ->
  Term a
pevalFiniteBitsSymRotateRotateLeftTerm :: forall a.
(Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymRotateRotateLeftTerm t :: Term a
t@Term a
SupportedTerm Term a
n =
  PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
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, PEvalRotateTerm a) =>
Term a -> Term a -> Maybe (Term a)
`doPevalFiniteBitsSymRotateRotateLeftTerm` Term a
n)
    (Term a -> TotalRuleUnary a a
forall a. PEvalRotateTerm a => Term a -> Term a -> Term a
`rotateLeftTerm` Term a
n)
    Term a
t

doPevalFiniteBitsSymRotateRotateLeftTerm ::
  forall a.
  (Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
  Term a ->
  Term a ->
  Maybe (Term a)
doPevalFiniteBitsSymRotateRotateLeftTerm :: forall a.
(Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
Term a -> Term a -> Maybe (Term a)
doPevalFiniteBitsSymRotateRotateLeftTerm (ConTerm a
a) (ConTerm 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 => 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)
doPevalFiniteBitsSymRotateRotateLeftTerm Term a
x (ConTerm a
0) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
-- doPevalFiniteBitsSymRotateRotateLeftTerm (RotateLeftTerm _ x (ConTerm  n)) (ConTerm  n1)
--   | n >= 0 && n1 >= 0 = Just $ pevalFiniteBitsSymRotateRotateLeftTerm x (conTerm $ n + n1)
doPevalFiniteBitsSymRotateRotateLeftTerm Term a
x (ConTerm 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
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
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, PEvalRotateTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymRotateRotateLeftTerm
          Term a
x
          (a -> Term a
forall t. SupportedPrim 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` Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
bs)
  where
    bs :: Int
bs = a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
n
doPevalFiniteBitsSymRotateRotateLeftTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

-- | Partial evaluation of symbolic rotate right term for finite bits types.
pevalFiniteBitsSymRotateRotateRightTerm ::
  forall a.
  (Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
  Term a ->
  Term a ->
  Term a
pevalFiniteBitsSymRotateRotateRightTerm :: forall a.
(Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymRotateRotateRightTerm t :: Term a
t@Term a
SupportedTerm Term a
n =
  PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
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, PEvalRotateTerm a) =>
Term a -> Term a -> Maybe (Term a)
`doPevalFiniteBitsSymRotateRotateRightTerm` Term a
n)
    (Term a -> TotalRuleUnary a a
forall a. PEvalRotateTerm a => Term a -> Term a -> Term a
`rotateRightTerm` Term a
n)
    Term a
t

doPevalFiniteBitsSymRotateRotateRightTerm ::
  forall a.
  (Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
  Term a ->
  Term a ->
  Maybe (Term a)
doPevalFiniteBitsSymRotateRotateRightTerm :: forall a.
(Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
Term a -> Term a -> Maybe (Term a)
doPevalFiniteBitsSymRotateRotateRightTerm (ConTerm a
a) (ConTerm 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 => t -> Term t
conTerm (a -> Maybe (Term a)) -> a -> Maybe (Term a)
forall a b. (a -> b) -> a -> b
$
        a -> Int -> a
forall a. Bits a => a -> Int -> a
rotateR
          a
a
          ( Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Integer -> Int
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` Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
n)
          )
doPevalFiniteBitsSymRotateRotateRightTerm Term a
x (ConTerm a
0) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
-- doPevalFiniteBitsSymRotateRotateRightTerm (RotateRightTerm _ x (ConTerm  n)) (ConTerm  n1)
--   | n >= 0 && n1 >= 0 = Just $ pevalFiniteBitsSymRotateRotateRightTerm x (conTerm $ n + n1)
doPevalFiniteBitsSymRotateRotateRightTerm Term a
x (ConTerm 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
>= Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
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, PEvalRotateTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymRotateRotateRightTerm
          Term a
x
          (a -> Term a
forall t. SupportedPrim 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` Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
bs)
  where
    bs :: Int
bs = a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize a
n
doPevalFiniteBitsSymRotateRotateRightTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

instance (KnownNat n, 1 <= n) => PEvalRotateTerm (IntN n) where
  pevalRotateLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalRotateLeftTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymRotateRotateLeftTerm
  pevalRotateRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalRotateRightTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymRotateRotateRightTerm
  withSbvRotateTermConstraint :: forall r. (SIntegral (NonFuncSBVBaseType (IntN n)) => r) -> r
withSbvRotateTermConstraint SIntegral (NonFuncSBVBaseType (IntN n)) => r
r =
    Proxy n -> (BVIsNonZero n => r) -> r
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). 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

  -- SBV's rotateLeft and rotateRight are broken for signed values, so we have to
  -- do this
  -- https://github.com/LeventErkok/sbv/issues/673
  sbvRotateLeftTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n)
sbvRotateLeftTerm SBVType (IntN n)
l SBVType (IntN n)
r =
    forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @(IntN n) ((NonFuncPrimConstraint (IntN n) => SBVType (IntN n))
 -> SBVType (IntN n))
-> (NonFuncPrimConstraint (IntN n) => SBVType (IntN n))
-> SBVType (IntN n)
forall a b. (a -> b) -> a -> b
$
      forall t r.
PEvalRotateTerm t =>
(SIntegral (NonFuncSBVBaseType t) => r) -> r
withSbvRotateTermConstraint @(IntN n) ((SIntegral (NonFuncSBVBaseType (IntN n)) => SBVType (IntN n))
 -> SBVType (IntN n))
-> (SIntegral (NonFuncSBVBaseType (IntN n)) => SBVType (IntN n))
-> SBVType (IntN n)
forall a b. (a -> b) -> a -> b
$
        SBV (WordN n) -> SBV (IntN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral (SBV (WordN n) -> SBV (IntN n)) -> SBV (WordN n) -> SBV (IntN n)
forall a b. (a -> b) -> a -> b
$
          SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
forall a b. (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
SBV.sRotateLeft
            (SBV (IntN n) -> SBV (WordN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN n)
SBVType (IntN n)
l :: SBV.SWord n)
            (SBV (IntN n) -> SBV (WordN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN n)
SBVType (IntN n)
r :: SBV.SWord n)
  sbvRotateRightTerm :: SBVType (IntN n) -> SBVType (IntN n) -> SBVType (IntN n)
sbvRotateRightTerm SBVType (IntN n)
l SBVType (IntN n)
r =
    forall a r.
SupportedNonFuncPrim a =>
(NonFuncPrimConstraint a => r) -> r
withNonFuncPrim @(IntN n) ((NonFuncPrimConstraint (IntN n) => SBVType (IntN n))
 -> SBVType (IntN n))
-> (NonFuncPrimConstraint (IntN n) => SBVType (IntN n))
-> SBVType (IntN n)
forall a b. (a -> b) -> a -> b
$
      forall t r.
PEvalRotateTerm t =>
(SIntegral (NonFuncSBVBaseType t) => r) -> r
withSbvRotateTermConstraint @(IntN n) ((SIntegral (NonFuncSBVBaseType (IntN n)) => SBVType (IntN n))
 -> SBVType (IntN n))
-> (SIntegral (NonFuncSBVBaseType (IntN n)) => SBVType (IntN n))
-> SBVType (IntN n)
forall a b. (a -> b) -> a -> b
$
        SBV (WordN n) -> SBV (IntN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral (SBV (WordN n) -> SBV (IntN n)) -> SBV (WordN n) -> SBV (IntN n)
forall a b. (a -> b) -> a -> b
$
          SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
forall a b. (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
SBV.sRotateRight
            (SBV (IntN n) -> SBV (WordN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN n)
SBVType (IntN n)
l :: SBV.SWord n)
            (SBV (IntN n) -> SBV (WordN n)
forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
SBV.sFromIntegral SBV (IntN n)
SBVType (IntN n)
r :: SBV.SWord n)

instance (KnownNat n, 1 <= n) => PEvalRotateTerm (WordN n) where
  pevalRotateLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalRotateLeftTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymRotateRotateLeftTerm
  pevalRotateRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalRotateRightTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(Integral a, SymRotate a, FiniteBits a, PEvalRotateTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymRotateRotateRightTerm
  withSbvRotateTermConstraint :: forall r. (SIntegral (NonFuncSBVBaseType (WordN n)) => r) -> r
withSbvRotateTermConstraint SIntegral (NonFuncSBVBaseType (WordN n)) => r
r =
    Proxy n -> (BVIsNonZero n => r) -> r
forall (w :: Nat) r (proxy :: Nat -> *).
(1 <= w) =>
proxy w -> (BVIsNonZero w => r) -> r
bvIsNonZeroFromGEq1 (forall (t :: Nat). 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