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

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalShiftTerm
-- 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.PEvalShiftTerm
  ( pevalFiniteBitsSymShiftShiftLeftTerm,
    pevalFiniteBitsSymShiftShiftRightTerm,
  )
where

import Data.Bits (Bits (isSigned, shiftR, zeroBits), FiniteBits (finiteBitSize))
import Data.Proxy (Proxy (Proxy))
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.Core.Data.Class.SymShift (SymShift (symShift))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim (bvIsNonZeroFromGEq1)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalShiftTerm (pevalShiftLeftTerm, pevalShiftRightTerm, withSbvShiftTermConstraint),
    SupportedNonFuncPrim (withNonFuncPrim),
    SupportedPrim,
    Term (ConTerm),
    conTerm,
    shiftLeftTerm,
    shiftRightTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold (unaryUnfoldOnce)

pevalFiniteBitsSymShiftShiftLeftTerm ::
  forall a.
  (Integral a, SymShift a, FiniteBits a, PEvalShiftTerm a) =>
  Term a ->
  Term a ->
  Term a
pevalFiniteBitsSymShiftShiftLeftTerm :: forall a.
(Integral a, SymShift a, FiniteBits a, PEvalShiftTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymShiftShiftLeftTerm Term a
t 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, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
`doPevalFiniteBitsSymShiftShiftLeftTerm` Term a
n)
    (Term a -> TotalRuleUnary a a
forall a. PEvalShiftTerm a => Term a -> Term a -> Term a
`shiftLeftTerm` Term a
n)
    Term a
t

doPevalFiniteBitsSymShiftShiftLeftTerm ::
  forall a.
  (Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
  Term a ->
  Term a ->
  Maybe (Term a)
doPevalFiniteBitsSymShiftShiftLeftTerm :: forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalFiniteBitsSymShiftShiftLeftTerm (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
doPevalFiniteBitsSymShiftShiftLeftTerm 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)
doPevalFiniteBitsSymShiftShiftLeftTerm 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
doPevalFiniteBitsSymShiftShiftLeftTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

pevalFiniteBitsSymShiftShiftRightTerm ::
  forall a.
  (Integral a, SymShift a, FiniteBits a, PEvalShiftTerm a) =>
  Term a ->
  Term a ->
  Term a
pevalFiniteBitsSymShiftShiftRightTerm :: forall a.
(Integral a, SymShift a, FiniteBits a, PEvalShiftTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymShiftShiftRightTerm Term a
t 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, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
`doPevalFiniteBitsSymShiftShiftRightTerm` Term a
n)
    (Term a -> TotalRuleUnary a a
forall a. PEvalShiftTerm a => Term a -> Term a -> Term a
`shiftRightTerm` Term a
n)
    Term a
t

doPevalFiniteBitsSymShiftShiftRightTerm ::
  forall a.
  (Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
  Term a ->
  Term a ->
  Maybe (Term a)
doPevalFiniteBitsSymShiftShiftRightTerm :: forall a.
(Integral a, SymShift a, FiniteBits a, SupportedPrim a) =>
Term a -> Term a -> Maybe (Term a)
doPevalFiniteBitsSymShiftShiftRightTerm (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)
doPevalFiniteBitsSymShiftShiftRightTerm (ConTerm Id
_ a
a) (ConTerm Id
_ a
n)
  -- if n >= 0 then -n must be in the range
  | 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)
doPevalFiniteBitsSymShiftShiftRightTerm Term a
x (ConTerm Id
_ a
0) = Term a -> Maybe (Term a)
forall a. a -> Maybe a
Just Term a
x
-- doPevalFiniteBitsSymShiftShiftRightTerm (ShiftRightTerm _ x (ConTerm _ n)) (ConTerm _ n1)
--   | n >= 0 && n1 >= 0 = Just $ pevalFiniteBitsSymShiftShiftRightTerm x (conTerm $ n + n1)
doPevalFiniteBitsSymShiftShiftRightTerm 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
doPevalFiniteBitsSymShiftShiftRightTerm Term a
_ Term a
_ = Maybe (Term a)
forall a. Maybe a
Nothing

instance (KnownNat n, 1 <= n) => PEvalShiftTerm (IntN n) where
  pevalShiftLeftTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalShiftLeftTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymShift a, FiniteBits a, PEvalShiftTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymShiftShiftLeftTerm
  pevalShiftRightTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalShiftRightTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Integral a, SymShift a, FiniteBits a, PEvalShiftTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymShiftShiftRightTerm
  withSbvShiftTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (SIntegral (NonFuncSBVBaseType n (IntN n)) => r) -> r
withSbvShiftTermConstraint proxy n
p SIntegral (NonFuncSBVBaseType n (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 (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @(IntN n) proxy n
p r
(SymVal (NonFuncSBVBaseType n (IntN n)),
 EqSymbolic (SBVType n (IntN n)), Mergeable (SBVType n (IntN n)),
 SMTDefinable (SBVType n (IntN n)), Mergeable (SBVType n (IntN n)),
 SBVType n (IntN n) ~ SBV (NonFuncSBVBaseType n (IntN n)),
 PrimConstraint n (IntN n)) =>
r
SIntegral (NonFuncSBVBaseType n (IntN n)) => r
r

instance (KnownNat n, 1 <= n) => PEvalShiftTerm (WordN n) where
  pevalShiftLeftTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalShiftLeftTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(Integral a, SymShift a, FiniteBits a, PEvalShiftTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymShiftShiftLeftTerm
  pevalShiftRightTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalShiftRightTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(Integral a, SymShift a, FiniteBits a, PEvalShiftTerm a) =>
Term a -> Term a -> Term a
pevalFiniteBitsSymShiftShiftRightTerm
  withSbvShiftTermConstraint :: forall (n :: Nat) (proxy :: Nat -> *) r.
KnownIsZero n =>
proxy n -> (SIntegral (NonFuncSBVBaseType n (WordN n)) => r) -> r
withSbvShiftTermConstraint proxy n
p SIntegral (NonFuncSBVBaseType n (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 (n :: Nat) (proxy :: Nat -> *) r.
(SupportedNonFuncPrim a, KnownIsZero n) =>
proxy n
-> ((SymVal (NonFuncSBVBaseType n a), EqSymbolic (SBVType n a),
     Mergeable (SBVType n a), SMTDefinable (SBVType n a),
     Mergeable (SBVType n a),
     SBVType n a ~ SBV (NonFuncSBVBaseType n a), PrimConstraint n a) =>
    r)
-> r
withNonFuncPrim @(WordN n) proxy n
p r
(SymVal (NonFuncSBVBaseType n (WordN n)),
 EqSymbolic (SBVType n (WordN n)), Mergeable (SBVType n (WordN n)),
 SMTDefinable (SBVType n (WordN n)),
 Mergeable (SBVType n (WordN n)),
 SBVType n (WordN n) ~ SBV (NonFuncSBVBaseType n (WordN n)),
 PrimConstraint n (WordN n)) =>
r
SIntegral (NonFuncSBVBaseType n (WordN n)) => r
r