{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitwiseTerm
-- 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.PEvalBitwiseTerm () where

import Data.Bits (Bits (complement, xor, zeroBits, (.&.), (.|.)))
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim ()
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( PEvalBitwiseTerm
      ( pevalAndBitsTerm,
        pevalComplementBitsTerm,
        pevalOrBitsTerm,
        pevalXorBitsTerm,
        withSbvBitwiseTermConstraint
      ),
    SupportedPrim (withPrim),
    Term,
    andBitsTerm,
    complementBitsTerm,
    conTerm,
    orBitsTerm,
    xorBitsTerm,
    pattern ComplementBitsTerm,
    pattern ConTerm,
  )
import Grisette.Internal.SymPrim.Prim.Internal.Unfold
  ( binaryUnfoldOnce,
    unaryUnfoldOnce,
  )

pevalDefaultAndBitsTerm ::
  (Bits a, SupportedPrim a, PEvalBitwiseTerm a) => Term a -> Term a -> Term a
pevalDefaultAndBitsTerm :: forall a.
(Bits a, SupportedPrim a, PEvalBitwiseTerm a) =>
Term a -> Term a -> Term a
pevalDefaultAndBitsTerm = PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall {t}.
(SupportedPrim t, Bits t) =>
Term t -> Term t -> Maybe (Term t)
doPevalAndBitsTerm TotalRuleBinary a a a
forall a. PEvalBitwiseTerm a => Term a -> Term a -> Term a
andBitsTerm
  where
    doPevalAndBitsTerm :: Term t -> Term t -> Maybe (Term t)
doPevalAndBitsTerm (ConTerm t
a) (ConTerm t
b) =
      Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t
a t -> t -> t
forall a. Bits a => a -> a -> a
.&. t
b)
    doPevalAndBitsTerm (ConTerm t
a) Term t
b
      | t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm t
forall a. Bits a => a
zeroBits
      | t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t -> t
forall a. Bits a => a -> a
complement t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just Term t
b
    doPevalAndBitsTerm Term t
a (ConTerm t
b)
      | t
b t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm t
forall a. Bits a => a
zeroBits
      | t
b t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t -> t
forall a. Bits a => a -> a
complement t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just Term t
a
    doPevalAndBitsTerm Term t
a Term t
b | Term t
a Term t -> Term t -> Bool
forall a. Eq a => a -> a -> Bool
== Term t
b = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just Term t
a
    doPevalAndBitsTerm Term t
_ Term t
_ = Maybe (Term t)
forall a. Maybe a
Nothing

pevalDefaultOrBitsTerm ::
  (Bits a, SupportedPrim a, PEvalBitwiseTerm a) => Term a -> Term a -> Term a
pevalDefaultOrBitsTerm :: forall a.
(Bits a, SupportedPrim a, PEvalBitwiseTerm a) =>
Term a -> Term a -> Term a
pevalDefaultOrBitsTerm = PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall {t}.
(SupportedPrim t, Bits t) =>
Term t -> Term t -> Maybe (Term t)
doPevalOrBitsTerm TotalRuleBinary a a a
forall a. PEvalBitwiseTerm a => Term a -> Term a -> Term a
orBitsTerm
  where
    doPevalOrBitsTerm :: Term t -> Term t -> Maybe (Term t)
doPevalOrBitsTerm (ConTerm t
a) (ConTerm t
b) = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t
a t -> t -> t
forall a. Bits a => a -> a -> a
.|. t
b)
    doPevalOrBitsTerm (ConTerm t
a) Term t
b
      | t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just Term t
b
      | t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t -> t
forall a. Bits a => a -> a
complement t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ t -> t
forall a. Bits a => a -> a
complement t
forall a. Bits a => a
zeroBits
    doPevalOrBitsTerm Term t
a (ConTerm t
b)
      | t
b t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just Term t
a
      | t
b t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t -> t
forall a. Bits a => a -> a
complement t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ t -> t
forall a. Bits a => a -> a
complement t
forall a. Bits a => a
zeroBits
    doPevalOrBitsTerm Term t
a Term t
b | Term t
a Term t -> Term t -> Bool
forall a. Eq a => a -> a -> Bool
== Term t
b = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just Term t
a
    doPevalOrBitsTerm Term t
_ Term t
_ = Maybe (Term t)
forall a. Maybe a
Nothing

pevalDefaultXorBitsTerm ::
  (PEvalBitwiseTerm a, SupportedPrim a, Bits a) => Term a -> Term a -> Term a
pevalDefaultXorBitsTerm :: forall a.
(PEvalBitwiseTerm a, SupportedPrim a, Bits a) =>
Term a -> Term a -> Term a
pevalDefaultXorBitsTerm = PartialRuleBinary a a a
-> TotalRuleBinary a a a -> TotalRuleBinary a a a
forall a b c.
SupportedPrim c =>
PartialRuleBinary a b c
-> TotalRuleBinary a b c -> TotalRuleBinary a b c
binaryUnfoldOnce PartialRuleBinary a a a
forall {t}.
(SupportedPrim t, Bits t, PEvalBitwiseTerm t) =>
Term t -> Term t -> Maybe (Term t)
doPevalXorBitsTerm TotalRuleBinary a a a
forall a. PEvalBitwiseTerm a => Term a -> Term a -> Term a
xorBitsTerm
  where
    doPevalXorBitsTerm :: Term t -> Term t -> Maybe (Term t)
doPevalXorBitsTerm (ConTerm t
a) (ConTerm t
b) =
      Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t
a t -> t -> t
forall a. Bits a => a -> a -> a
`xor` t
b)
    doPevalXorBitsTerm (ConTerm t
a) Term t
b
      | t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just Term t
b
      | t
a t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t -> t
forall a. Bits a => a -> a
complement t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t
forall t. PEvalBitwiseTerm t => Term t -> Term t
pevalComplementBitsTerm Term t
b
    doPevalXorBitsTerm Term t
a (ConTerm t
b)
      | t
b t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just Term t
a
      | t
b t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t -> t
forall a. Bits a => a -> a
complement t
forall a. Bits a => a
zeroBits = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t
forall t. PEvalBitwiseTerm t => Term t -> Term t
pevalComplementBitsTerm Term t
a
    doPevalXorBitsTerm Term t
a Term t
b | Term t
a Term t -> Term t -> Bool
forall a. Eq a => a -> a -> Bool
== Term t
b = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm t
forall a. Bits a => a
zeroBits
    doPevalXorBitsTerm (ComplementBitsTerm Term t
i) (ComplementBitsTerm Term t
j) =
      Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term t
forall a. PEvalBitwiseTerm a => Term a -> Term a -> Term a
pevalXorBitsTerm Term t
i Term t
j
    doPevalXorBitsTerm (ComplementBitsTerm Term t
i) Term t
j =
      Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t
forall t. PEvalBitwiseTerm t => Term t -> Term t
pevalComplementBitsTerm (Term t -> Term t) -> Term t -> Term t
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term t
forall a. PEvalBitwiseTerm a => Term a -> Term a -> Term a
pevalXorBitsTerm Term t
i Term t
j
    doPevalXorBitsTerm Term t
i (ComplementBitsTerm Term t
j) =
      Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ Term t -> Term t
forall t. PEvalBitwiseTerm t => Term t -> Term t
pevalComplementBitsTerm (Term t -> Term t) -> Term t -> Term t
forall a b. (a -> b) -> a -> b
$ Term t -> Term t -> Term t
forall a. PEvalBitwiseTerm a => Term a -> Term a -> Term a
pevalXorBitsTerm Term t
i Term t
j
    doPevalXorBitsTerm Term t
_ Term t
_ = Maybe (Term t)
forall a. Maybe a
Nothing

pevalDefaultComplementBitsTerm ::
  (Bits a, SupportedPrim a, PEvalBitwiseTerm a) => Term a -> Term a
pevalDefaultComplementBitsTerm :: forall a.
(Bits a, SupportedPrim a, PEvalBitwiseTerm a) =>
Term a -> Term a
pevalDefaultComplementBitsTerm =
  PartialRuleUnary a a -> TotalRuleUnary a a -> TotalRuleUnary a a
forall a b.
SupportedPrim b =>
PartialRuleUnary a b -> TotalRuleUnary a b -> TotalRuleUnary a b
unaryUnfoldOnce PartialRuleUnary a a
forall {t}. Bits t => Term t -> Maybe (Term t)
doPevalComplementBitsTerm TotalRuleUnary a a
forall t. PEvalBitwiseTerm t => Term t -> Term t
complementBitsTerm
  where
    doPevalComplementBitsTerm :: Term t -> Maybe (Term t)
doPevalComplementBitsTerm (ConTerm t
a) = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just (Term t -> Maybe (Term t)) -> Term t -> Maybe (Term t)
forall a b. (a -> b) -> a -> b
$ t -> Term t
forall t. SupportedPrim t => t -> Term t
conTerm (t -> Term t) -> t -> Term t
forall a b. (a -> b) -> a -> b
$ t -> t
forall a. Bits a => a -> a
complement t
a
    doPevalComplementBitsTerm (ComplementBitsTerm Term t
a) = Term t -> Maybe (Term t)
forall a. a -> Maybe a
Just Term t
a
    doPevalComplementBitsTerm Term t
_ = Maybe (Term t)
forall a. Maybe a
Nothing

instance (KnownNat n, 1 <= n) => PEvalBitwiseTerm (WordN n) where
  pevalAndBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalAndBitsTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(Bits a, SupportedPrim a, PEvalBitwiseTerm a) =>
Term a -> Term a -> Term a
pevalDefaultAndBitsTerm
  pevalOrBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalOrBitsTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(Bits a, SupportedPrim a, PEvalBitwiseTerm a) =>
Term a -> Term a -> Term a
pevalDefaultOrBitsTerm
  pevalXorBitsTerm :: Term (WordN n) -> Term (WordN n) -> Term (WordN n)
pevalXorBitsTerm = Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall a.
(PEvalBitwiseTerm a, SupportedPrim a, Bits a) =>
Term a -> Term a -> Term a
pevalDefaultXorBitsTerm
  pevalComplementBitsTerm :: Term (WordN n) -> Term (WordN n)
pevalComplementBitsTerm = Term (WordN n) -> Term (WordN n)
forall a.
(Bits a, SupportedPrim a, PEvalBitwiseTerm a) =>
Term a -> Term a
pevalDefaultComplementBitsTerm
  withSbvBitwiseTermConstraint :: forall r. (Bits (SBVType (WordN n)) => r) -> r
withSbvBitwiseTermConstraint Bits (SBVType (WordN n)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(WordN n) r
Bits (SBVType (WordN n)) => r
(PrimConstraint (WordN n), SMTDefinable (SBVType (WordN n)),
 Mergeable (SBVType (WordN n)), Typeable (SBVType (WordN n))) =>
r
r

instance (KnownNat n, 1 <= n) => PEvalBitwiseTerm (IntN n) where
  pevalAndBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalAndBitsTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Bits a, SupportedPrim a, PEvalBitwiseTerm a) =>
Term a -> Term a -> Term a
pevalDefaultAndBitsTerm
  pevalOrBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalOrBitsTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(Bits a, SupportedPrim a, PEvalBitwiseTerm a) =>
Term a -> Term a -> Term a
pevalDefaultOrBitsTerm
  pevalXorBitsTerm :: Term (IntN n) -> Term (IntN n) -> Term (IntN n)
pevalXorBitsTerm = Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall a.
(PEvalBitwiseTerm a, SupportedPrim a, Bits a) =>
Term a -> Term a -> Term a
pevalDefaultXorBitsTerm
  pevalComplementBitsTerm :: Term (IntN n) -> Term (IntN n)
pevalComplementBitsTerm = Term (IntN n) -> Term (IntN n)
forall a.
(Bits a, SupportedPrim a, PEvalBitwiseTerm a) =>
Term a -> Term a
pevalDefaultComplementBitsTerm
  withSbvBitwiseTermConstraint :: forall r. (Bits (SBVType (IntN n)) => r) -> r
withSbvBitwiseTermConstraint Bits (SBVType (IntN n)) => r
r = forall t a.
SupportedPrim t =>
((PrimConstraint t, SMTDefinable (SBVType t),
  Mergeable (SBVType t), Typeable (SBVType t)) =>
 a)
-> a
withPrim @(IntN n) r
Bits (SBVType (IntN n)) => r
(PrimConstraint (IntN n), SMTDefinable (SBVType (IntN n)),
 Mergeable (SBVType (IntN n)), Typeable (SBVType (IntN n))) =>
r
r