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

-- |
-- Module      :   Grisette.Internal.Unified.Class.UnifiedFiniteBits
-- 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.Unified.Class.UnifiedFiniteBits
  ( UnifiedFiniteBits (..),
    symTestBit,
    symSetBitTo,
    symFromBits,
    symBitBlast,
    symLsb,
    symMsb,
    symPopCount,
    symCountLeadingZeros,
    symCountTrailingZeros,
  )
where

import Data.Bits
  ( Bits (popCount, testBit),
    FiniteBits (countLeadingZeros, countTrailingZeros),
  )
import Data.Type.Bool (If)
import GHC.TypeLits (KnownNat, type (<=))
import Grisette.Internal.Core.Data.Class.SymFiniteBits
  ( FromBits,
    SymFiniteBits,
    setBitTo,
  )
import qualified Grisette.Internal.Core.Data.Class.SymFiniteBits as SymFiniteBits
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.SomeBV
  ( SomeIntN,
    SomeSymIntN,
    SomeSymWordN,
    SomeWordN,
  )
import Grisette.Internal.SymPrim.SymBV (SymIntN, SymWordN)
import Grisette.Internal.Unified.Class.UnifiedITEOp
  ( UnifiedITEOp (withBaseITEOp),
  )
import Grisette.Internal.Unified.EvalModeTag (EvalModeTag (C, S), IsConMode)
import Grisette.Internal.Unified.UnifiedBool (UnifiedBool (GetBool))
import Grisette.Internal.Unified.Util (DecideEvalMode, withMode)

-- | Unified `Grisette.Internal.Core.Data.Class.SymFiniteBits.symTestBit`.
symTestBit ::
  forall mode a.
  (DecideEvalMode mode, UnifiedFiniteBits mode a) =>
  a ->
  Int ->
  GetBool mode
symTestBit :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedFiniteBits mode a) =>
a -> Int -> GetBool mode
symTestBit a
a Int
i =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (a -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit a
a Int
i))
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (a -> Int -> SymBool
forall a. SymFiniteBits a => a -> Int -> SymBool
SymFiniteBits.symTestBit a
a Int
i))

-- | Unified `Grisette.Internal.Core.Data.Class.SymFiniteBits.symSetBitTo`.
symSetBitTo ::
  forall mode a.
  (DecideEvalMode mode, UnifiedFiniteBits mode a) =>
  a ->
  Int ->
  GetBool mode ->
  a
symSetBitTo :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedFiniteBits mode a) =>
a -> Int -> GetBool mode -> a
symSetBitTo a
a Int
i GetBool mode
b =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (a -> Int -> Bool -> a
forall a. Bits a => a -> Int -> Bool -> a
setBitTo a
a Int
i Bool
GetBool mode
b))
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (a -> Int -> SymBool -> a
forall a. SymFiniteBits a => a -> Int -> SymBool -> a
SymFiniteBits.symSetBitTo a
a Int
i SymBool
GetBool mode
b))

-- | Unified `Grisette.Internal.Core.Data.Class.SymFiniteBits.symFromBits`.
symFromBits ::
  forall mode a.
  (DecideEvalMode mode, UnifiedFiniteBits mode a) =>
  [GetBool mode] ->
  a
symFromBits :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedFiniteBits mode a) =>
[GetBool mode] -> a
symFromBits [GetBool mode]
bits =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a ([Bool] -> a
forall a. FromBits a => [Bool] -> a
SymFiniteBits.fromBits [Bool]
[GetBool mode]
bits))
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a ([SymBool] -> a
forall a. SymFiniteBits a => [SymBool] -> a
SymFiniteBits.symFromBits [SymBool]
[GetBool mode]
bits))

-- | Unified `Grisette.Internal.Core.Data.Class.SymFiniteBits.symBitBlast`.
symBitBlast ::
  forall mode a.
  (DecideEvalMode mode, UnifiedFiniteBits mode a) =>
  a ->
  [GetBool mode]
symBitBlast :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedFiniteBits mode a) =>
a -> [GetBool mode]
symBitBlast a
a =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (a -> [Bool]
forall a. FiniteBits a => a -> [Bool]
SymFiniteBits.bitBlast a
a))
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (a -> [SymBool]
forall a. SymFiniteBits a => a -> [SymBool]
SymFiniteBits.symBitBlast a
a))

-- | Unified `Grisette.Internal.Core.Data.Class.SymFiniteBits.symLsb`.
symLsb ::
  forall mode a.
  (DecideEvalMode mode, UnifiedFiniteBits mode a) =>
  a ->
  GetBool mode
symLsb :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedFiniteBits mode a) =>
a -> GetBool mode
symLsb a
a =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (a -> Bool
forall a. Bits a => a -> Bool
SymFiniteBits.lsb a
a))
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (a -> SymBool
forall a. SymFiniteBits a => a -> SymBool
SymFiniteBits.symLsb a
a))

-- | Unified `Grisette.Internal.Core.Data.Class.SymFiniteBits.symMsb`.
symMsb ::
  forall mode a.
  (DecideEvalMode mode, UnifiedFiniteBits mode a) =>
  a ->
  GetBool mode
symMsb :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedFiniteBits mode a) =>
a -> GetBool mode
symMsb a
a =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (a -> Bool
forall a. FiniteBits a => a -> Bool
SymFiniteBits.msb a
a))
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (a -> SymBool
forall a. SymFiniteBits a => a -> SymBool
SymFiniteBits.symMsb a
a))

-- | Unified `Grisette.Internal.Core.Data.Class.SymFiniteBits.symPopCount`.
symPopCount ::
  forall mode a.
  (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) =>
  a ->
  a
symPopCount :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedFiniteBits mode a, Num a,
 UnifiedITEOp mode a) =>
a -> a
symPopCount a
a =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> a) -> Int -> a
forall a b. (a -> b) -> a -> b
$ a -> Int
forall a. Bits a => a -> Int
popCount a
a))
    ( forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a ((If
    (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
  a)
 -> a)
-> (If
      (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) v r.
UnifiedITEOp mode v =>
(If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
withBaseITEOp @mode @a (a -> a
forall a. (Num a, ITEOp a, SymFiniteBits a) => a -> a
SymFiniteBits.symPopCount a
a)
    )

-- | Unified
-- `Grisette.Internal.Core.Data.Class.SymFiniteBits.symCountLeadingZeros`.
symCountLeadingZeros ::
  forall mode a.
  (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) =>
  a ->
  a
symCountLeadingZeros :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedFiniteBits mode a, Num a,
 UnifiedITEOp mode a) =>
a -> a
symCountLeadingZeros a
a =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> a) -> Int -> a
forall a b. (a -> b) -> a -> b
$ a -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros a
a))
    ( forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a ((If
    (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
  a)
 -> a)
-> (If
      (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) v r.
UnifiedITEOp mode v =>
(If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
withBaseITEOp @mode @a (a -> a
forall a. (Num a, ITEOp a, SymFiniteBits a) => a -> a
SymFiniteBits.symCountLeadingZeros a
a)
    )

-- | Unified
-- `Grisette.Internal.Core.Data.Class.SymFiniteBits.symCountTrailingZeros`.
symCountTrailingZeros ::
  forall mode a.
  (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) =>
  a ->
  a
symCountTrailingZeros :: forall (mode :: EvalModeTag) a.
(DecideEvalMode mode, UnifiedFiniteBits mode a, Num a,
 UnifiedITEOp mode a) =>
a -> a
symCountTrailingZeros a
a =
  forall (mode :: EvalModeTag) r.
DecideEvalMode mode =>
((mode ~ 'C) => r) -> ((mode ~ 'S) => r) -> r
withMode @mode
    (forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a (Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> a) -> Int -> a
forall a b. (a -> b) -> a -> b
$ a -> Int
forall b. FiniteBits b => b -> Int
countTrailingZeros a
a))
    ( forall (mode :: EvalModeTag) a r.
UnifiedFiniteBits mode a =>
(If
   (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
 r)
-> r
withBaseFiniteBits @mode @a ((If
    (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
  a)
 -> a)
-> (If
      (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
        forall (mode :: EvalModeTag) v r.
UnifiedITEOp mode v =>
(If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
withBaseITEOp @mode @a (a -> a
forall a. (Num a, ITEOp a, SymFiniteBits a) => a -> a
SymFiniteBits.symCountTrailingZeros a
a)
    )

-- | A class that provides unified equality comparison.
--
-- We use this type class to help resolve the constraints for `FiniteBits`,
-- `FromBits` and `SymFiniteBits`.
class UnifiedFiniteBits mode a where
  withBaseFiniteBits ::
    ((If (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a)) => r) ->
    r

instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'C (WordN n) where
  withBaseFiniteBits :: forall r.
(If
   (IsConMode 'C)
   (FiniteBits (WordN n), FromBits (WordN n))
   (SymFiniteBits (WordN n)) =>
 r)
-> r
withBaseFiniteBits If
  (IsConMode 'C)
  (FiniteBits (WordN n), FromBits (WordN n))
  (SymFiniteBits (WordN n)) =>
r
r = r
If
  (IsConMode 'C)
  (FiniteBits (WordN n), FromBits (WordN n))
  (SymFiniteBits (WordN n)) =>
r
r

instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'C (IntN n) where
  withBaseFiniteBits :: forall r.
(If
   (IsConMode 'C)
   (FiniteBits (IntN n), FromBits (IntN n))
   (SymFiniteBits (IntN n)) =>
 r)
-> r
withBaseFiniteBits If
  (IsConMode 'C)
  (FiniteBits (IntN n), FromBits (IntN n))
  (SymFiniteBits (IntN n)) =>
r
r = r
If
  (IsConMode 'C)
  (FiniteBits (IntN n), FromBits (IntN n))
  (SymFiniteBits (IntN n)) =>
r
r

instance UnifiedFiniteBits 'C SomeWordN where
  withBaseFiniteBits :: forall r.
(If
   (IsConMode 'C)
   (FiniteBits SomeWordN, FromBits SomeWordN)
   (SymFiniteBits SomeWordN) =>
 r)
-> r
withBaseFiniteBits If
  (IsConMode 'C)
  (FiniteBits SomeWordN, FromBits SomeWordN)
  (SymFiniteBits SomeWordN) =>
r
r = r
If
  (IsConMode 'C)
  (FiniteBits SomeWordN, FromBits SomeWordN)
  (SymFiniteBits SomeWordN) =>
r
r

instance UnifiedFiniteBits 'C SomeIntN where
  withBaseFiniteBits :: forall r.
(If
   (IsConMode 'C)
   (FiniteBits SomeIntN, FromBits SomeIntN)
   (SymFiniteBits SomeIntN) =>
 r)
-> r
withBaseFiniteBits If
  (IsConMode 'C)
  (FiniteBits SomeIntN, FromBits SomeIntN)
  (SymFiniteBits SomeIntN) =>
r
r = r
If
  (IsConMode 'C)
  (FiniteBits SomeIntN, FromBits SomeIntN)
  (SymFiniteBits SomeIntN) =>
r
r

instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'S (SymWordN n) where
  withBaseFiniteBits :: forall r.
(If
   (IsConMode 'S)
   (FiniteBits (SymWordN n), FromBits (SymWordN n))
   (SymFiniteBits (SymWordN n)) =>
 r)
-> r
withBaseFiniteBits If
  (IsConMode 'S)
  (FiniteBits (SymWordN n), FromBits (SymWordN n))
  (SymFiniteBits (SymWordN n)) =>
r
r = r
If
  (IsConMode 'S)
  (FiniteBits (SymWordN n), FromBits (SymWordN n))
  (SymFiniteBits (SymWordN n)) =>
r
r

instance (KnownNat n, 1 <= n) => UnifiedFiniteBits 'S (SymIntN n) where
  withBaseFiniteBits :: forall r.
(If
   (IsConMode 'S)
   (FiniteBits (SymIntN n), FromBits (SymIntN n))
   (SymFiniteBits (SymIntN n)) =>
 r)
-> r
withBaseFiniteBits If
  (IsConMode 'S)
  (FiniteBits (SymIntN n), FromBits (SymIntN n))
  (SymFiniteBits (SymIntN n)) =>
r
r = r
If
  (IsConMode 'S)
  (FiniteBits (SymIntN n), FromBits (SymIntN n))
  (SymFiniteBits (SymIntN n)) =>
r
r

instance UnifiedFiniteBits 'S SomeSymWordN where
  withBaseFiniteBits :: forall r.
(If
   (IsConMode 'S)
   (FiniteBits SomeSymWordN, FromBits SomeSymWordN)
   (SymFiniteBits SomeSymWordN) =>
 r)
-> r
withBaseFiniteBits If
  (IsConMode 'S)
  (FiniteBits SomeSymWordN, FromBits SomeSymWordN)
  (SymFiniteBits SomeSymWordN) =>
r
r = r
If
  (IsConMode 'S)
  (FiniteBits SomeSymWordN, FromBits SomeSymWordN)
  (SymFiniteBits SomeSymWordN) =>
r
r

instance UnifiedFiniteBits 'S SomeSymIntN where
  withBaseFiniteBits :: forall r.
(If
   (IsConMode 'S)
   (FiniteBits SomeSymIntN, FromBits SomeSymIntN)
   (SymFiniteBits SomeSymIntN) =>
 r)
-> r
withBaseFiniteBits If
  (IsConMode 'S)
  (FiniteBits SomeSymIntN, FromBits SomeSymIntN)
  (SymFiniteBits SomeSymIntN) =>
r
r = r
If
  (IsConMode 'S)
  (FiniteBits SomeSymIntN, FromBits SomeSymIntN)
  (SymFiniteBits SomeSymIntN) =>
r
r