{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.SymBV
-- 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.Internal.SymPrim.SymBV
  ( SymWordN (SymWordN),
    SymWordN8,
    SymWordN16,
    SymWordN32,
    SymWordN64,
    SymIntN (SymIntN),
    SymIntN8,
    SymIntN16,
    SymIntN32,
    SymIntN64,
  )
where

import Control.DeepSeq (NFData)
import Data.Bits
  ( Bits
      ( bit,
        bitSize,
        bitSizeMaybe,
        complement,
        isSigned,
        popCount,
        rotate,
        shift,
        testBit,
        xor,
        (.&.),
        (.|.)
      ),
    FiniteBits (finiteBitSize),
  )
import Data.Hashable (Hashable (hashWithSalt))
import Data.Proxy (Proxy (Proxy))
import Data.String (IsString (fromString))
import GHC.Generics (Generic)
import GHC.TypeNats
  ( KnownNat,
    Nat,
    natVal,
    type (+),
    type (<=),
  )
import Grisette.Internal.Core.Data.Class.BitVector
  ( SizedBV
      ( sizedBVConcat,
        sizedBVExt,
        sizedBVSelect,
        sizedBVSext,
        sizedBVZext
      ),
  )
import Grisette.Internal.Core.Data.Class.Function
  ( Apply (FunType, apply),
  )
import Grisette.Internal.Core.Data.Class.SignConversion
  ( SignConversion (toSigned, toUnsigned),
  )
import Grisette.Internal.Core.Data.Class.Solvable
  ( Solvable (con, conView, ssym, sym),
    pattern Con,
  )
import Grisette.Internal.Core.Data.Class.SymRotate
  ( SymRotate (symRotate, symRotateNegated),
  )
import Grisette.Internal.Core.Data.Class.SymShift (SymShift (symShift, symShiftNegated))
import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSymsS), SomeSym (SomeSym))
import Grisette.Internal.SymPrim.BV
  ( IntN,
    WordN,
  )
import Grisette.Internal.SymPrim.Prim.Term
  ( ConRep (ConType),
    LinkedRep (underlyingTerm, wrapTerm),
    PEvalBVSignConversionTerm (pevalBVToSignedTerm, pevalBVToUnsignedTerm),
    PEvalBVTerm (pevalBVConcatTerm, pevalBVExtendTerm, pevalBVSelectTerm),
    PEvalBitwiseTerm
      ( pevalAndBitsTerm,
        pevalComplementBitsTerm,
        pevalOrBitsTerm,
        pevalXorBitsTerm
      ),
    PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm
      ),
    PEvalOrdTerm (pevalLeOrdTerm),
    PEvalRotateTerm
      ( pevalRotateLeftTerm,
        pevalRotateRightTerm
      ),
    PEvalShiftTerm (pevalShiftLeftTerm, pevalShiftRightTerm),
    SupportedPrim (pevalITETerm),
    SymRep (SymType),
    Term (ConTerm),
    conTerm,
    pevalEqTerm,
    pevalGeOrdTerm,
    pevalModIntegralTerm,
    pevalOrTerm,
    pevalSubNumTerm,
    pformat,
    symTerm,
  )
import Grisette.Internal.Utils.Parameterized
  ( KnownProof (KnownProof),
    LeqProof (LeqProof),
    knownAdd,
    leqAddPos,
    leqTrans,
  )
import Language.Haskell.TH.Syntax (Lift)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Grisette.Backend
-- >>> import Data.Proxy

-- | Symbolic signed bit vector type. Indexed with the bit width.
-- Signedness affects the semantics of the operations, including
-- comparison/extension, etc.
--
-- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
-- >>> "a" + 5 :: SymIntN 5
-- (+ 0b00101 a)
-- >>> sizedBVConcat (con 0b101 :: SymIntN 3) (con 0b110 :: SymIntN 3)
-- 0b101110
-- >>> sizedBVExt (Proxy @6) (con 0b101 :: SymIntN 3)
-- 0b111101
-- >>> (8 :: SymIntN 4) .< (7 :: SymIntN 4)
-- true
--
-- More operations are available. Please refer to "Grisette.Core#g:symops" for
-- more information.
newtype SymIntN (n :: Nat) = SymIntN {forall (n :: Nat). SymIntN n -> Term (IntN n)
underlyingIntNTerm :: Term (IntN n)}
  deriving ((forall (m :: * -> *). Quote m => SymIntN n -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    SymIntN n -> Code m (SymIntN n))
-> Lift (SymIntN n)
forall (n :: Nat) (m :: * -> *). Quote m => SymIntN n -> m Exp
forall (n :: Nat) (m :: * -> *).
Quote m =>
SymIntN n -> Code m (SymIntN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymIntN n -> m Exp
forall (m :: * -> *). Quote m => SymIntN n -> Code m (SymIntN n)
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => SymIntN n -> m Exp
lift :: forall (m :: * -> *). Quote m => SymIntN n -> m Exp
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
SymIntN n -> Code m (SymIntN n)
liftTyped :: forall (m :: * -> *). Quote m => SymIntN n -> Code m (SymIntN n)
Lift, SymIntN n -> ()
(SymIntN n -> ()) -> NFData (SymIntN n)
forall (n :: Nat). SymIntN n -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Nat). SymIntN n -> ()
rnf :: SymIntN n -> ()
NFData, (forall x. SymIntN n -> Rep (SymIntN n) x)
-> (forall x. Rep (SymIntN n) x -> SymIntN n)
-> Generic (SymIntN n)
forall (n :: Nat) x. Rep (SymIntN n) x -> SymIntN n
forall (n :: Nat) x. SymIntN n -> Rep (SymIntN n) x
forall x. Rep (SymIntN n) x -> SymIntN n
forall x. SymIntN n -> Rep (SymIntN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Nat) x. SymIntN n -> Rep (SymIntN n) x
from :: forall x. SymIntN n -> Rep (SymIntN n) x
$cto :: forall (n :: Nat) x. Rep (SymIntN n) x -> SymIntN n
to :: forall x. Rep (SymIntN n) x -> SymIntN n
Generic)

-- | Symbolic 8-bit signed bit-vector.
type SymIntN8 = SymIntN 8

-- | Symbolic 16-bit signed bit-vector.
type SymIntN16 = SymIntN 16

-- | Symbolic 32-bit signed bit-vector.
type SymIntN32 = SymIntN 32

-- | Symbolic 64-bit signed bit-vector.
type SymIntN64 = SymIntN 64

-- | Symbolic unsigned bit vector type. Indexed with the bit width.
-- Signedness affects the semantics of the operations, including
-- comparison/extension, etc.
--
-- >>> :set -XOverloadedStrings -XDataKinds -XBinaryLiterals
-- >>> "a" + 5 :: SymWordN 5
-- (+ 0b00101 a)
-- >>> sizedBVConcat (con 0b101 :: SymWordN 3) (con 0b110 :: SymWordN 3)
-- 0b101110
-- >>> sizedBVExt (Proxy @6) (con 0b101 :: SymWordN 3)
-- 0b000101
-- >>> (8 :: SymWordN 4) .< (7 :: SymWordN 4)
-- false
--
-- More operations are available. Please refer to "Grisette.Core#g:symops" for
-- more information.
newtype SymWordN (n :: Nat) = SymWordN {forall (n :: Nat). SymWordN n -> Term (WordN n)
underlyingWordNTerm :: Term (WordN n)}
  deriving ((forall (m :: * -> *). Quote m => SymWordN n -> m Exp)
-> (forall (m :: * -> *).
    Quote m =>
    SymWordN n -> Code m (SymWordN n))
-> Lift (SymWordN n)
forall (n :: Nat) (m :: * -> *). Quote m => SymWordN n -> m Exp
forall (n :: Nat) (m :: * -> *).
Quote m =>
SymWordN n -> Code m (SymWordN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => SymWordN n -> m Exp
forall (m :: * -> *). Quote m => SymWordN n -> Code m (SymWordN n)
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => SymWordN n -> m Exp
lift :: forall (m :: * -> *). Quote m => SymWordN n -> m Exp
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
SymWordN n -> Code m (SymWordN n)
liftTyped :: forall (m :: * -> *). Quote m => SymWordN n -> Code m (SymWordN n)
Lift, SymWordN n -> ()
(SymWordN n -> ()) -> NFData (SymWordN n)
forall (n :: Nat). SymWordN n -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Nat). SymWordN n -> ()
rnf :: SymWordN n -> ()
NFData, (forall x. SymWordN n -> Rep (SymWordN n) x)
-> (forall x. Rep (SymWordN n) x -> SymWordN n)
-> Generic (SymWordN n)
forall (n :: Nat) x. Rep (SymWordN n) x -> SymWordN n
forall (n :: Nat) x. SymWordN n -> Rep (SymWordN n) x
forall x. Rep (SymWordN n) x -> SymWordN n
forall x. SymWordN n -> Rep (SymWordN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Nat) x. SymWordN n -> Rep (SymWordN n) x
from :: forall x. SymWordN n -> Rep (SymWordN n) x
$cto :: forall (n :: Nat) x. Rep (SymWordN n) x -> SymWordN n
to :: forall x. Rep (SymWordN n) x -> SymWordN n
Generic)

-- | Symbolic 8-bit unsigned bit-vector.
type SymWordN8 = SymWordN 8

-- | Symbolic 16-bit unsigned bit-vector.
type SymWordN16 = SymWordN 16

-- | Symbolic 32-bit unsigned bit-vector.
type SymWordN32 = SymWordN 32

-- | Symbolic 64-bit unsigned bit-vector.
type SymWordN64 = SymWordN 64

instance (KnownNat n, 1 <= n) => ConRep (SymIntN n) where
  type ConType (SymIntN n) = IntN n

instance (KnownNat n, 1 <= n) => SymRep (IntN n) where
  type SymType (IntN n) = SymIntN n

instance (KnownNat n, 1 <= n) => LinkedRep (IntN n) (SymIntN n) where
  underlyingTerm :: SymIntN n -> Term (IntN n)
underlyingTerm (SymIntN Term (IntN n)
a) = Term (IntN n)
a
  wrapTerm :: Term (IntN n) -> SymIntN n
wrapTerm = Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN

instance (KnownNat n, 1 <= n) => ConRep (SymWordN n) where
  type ConType (SymWordN n) = WordN n

instance (KnownNat n, 1 <= n) => SymRep (WordN n) where
  type SymType (WordN n) = SymWordN n

instance (KnownNat n, 1 <= n) => LinkedRep (WordN n) (SymWordN n) where
  underlyingTerm :: SymWordN n -> Term (WordN n)
underlyingTerm (SymWordN Term (WordN n)
a) = Term (WordN n)
a
  wrapTerm :: Term (WordN n) -> SymWordN n
wrapTerm = Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN

-- Aggregate instances

instance (KnownNat n, 1 <= n) => Apply (SymIntN n) where
  type FunType (SymIntN n) = SymIntN n
  apply :: SymIntN n -> FunType (SymIntN n)
apply = SymIntN n -> FunType (SymIntN n)
SymIntN n -> SymIntN n
forall a. a -> a
id

instance (KnownNat n, 1 <= n) => Apply (SymWordN n) where
  type FunType (SymWordN n) = SymWordN n
  apply :: SymWordN n -> FunType (SymWordN n)
apply = SymWordN n -> FunType (SymWordN n)
SymWordN n -> SymWordN n
forall a. a -> a
id

#define SOLVABLE_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => Solvable (contype n) (symtype n) where \
  con = symtype . conTerm; \
  sym = symtype . symTerm; \
  conView (symtype (ConTerm _ t)) = Just t; \
  conView _ = Nothing

#if 1
SOLVABLE_BV(IntN, SymIntN)
SOLVABLE_BV(WordN, SymWordN)
#endif

-- Num

#define NUM_BV(symtype) \
instance (KnownNat n, 1 <= n) => Num (symtype n) where \
  (symtype l) + (symtype r) = symtype $ pevalAddNumTerm l r; \
  (symtype l) - (symtype r) = symtype $ pevalSubNumTerm l r; \
  (symtype l) * (symtype r) = symtype $ pevalMulNumTerm l r; \
  negate (symtype v) = symtype $ pevalNegNumTerm v; \
  abs (symtype v) = symtype $ pevalAbsNumTerm v; \
  signum (symtype v) = symtype $ pevalSignumNumTerm v; \
  fromInteger i = con $ fromInteger i

#if 1
NUM_BV(SymIntN)
NUM_BV(SymWordN)
#endif

-- Bits

#define BITS_BV(symtype, signed) \
instance (KnownNat n, 1 <= n) => Bits (symtype n) where \
  symtype l .&. symtype r = symtype $ pevalAndBitsTerm l r; \
  {-# INLINE (.&.) #-}; \
  symtype l .|. symtype r = symtype $ pevalOrBitsTerm l r; \
  {-# INLINE (.|.) #-}; \
  symtype l `xor` symtype r = symtype $ pevalXorBitsTerm l r; \
  {-# INLINE xor #-}; \
  complement (symtype n) = symtype $ pevalComplementBitsTerm n; \
  {-# INLINE complement #-}; \
  shift (symtype n) i | i > 0 = symtype $ pevalShiftLeftTerm n (conTerm $ fromIntegral i); \
  shift (symtype n) i | i < 0 = symtype $ pevalShiftRightTerm n (conTerm $ fromIntegral (-i)); \
  shift (symtype n) _ = symtype n; \
  {-# INLINE shift #-}; \
  rotate (symtype n) i | i > 0 = symtype $ pevalRotateLeftTerm n (conTerm $ fromIntegral i); \
  rotate (symtype n) i | i < 0 = symtype $ pevalRotateRightTerm n (conTerm $ fromIntegral (-i)); \
  rotate (symtype n) _ = symtype n; \
  {-# INLINE rotate #-}; \
  bitSize = finiteBitSize; \
  {-# INLINE bitSize #-}; \
  bitSizeMaybe = Just . finiteBitSize; \
  {-# INLINE bitSizeMaybe #-}; \
  isSigned _ = signed; \
  {-# INLINE isSigned #-}; \
  testBit (Con n) =  testBit n; \
  testBit _ = error "You cannot call testBit on symbolic variables"; \
  {-# INLINE testBit #-}; \
  bit = con . bit; \
  {-# INLINE bit #-}; \
  popCount (Con n) = popCount n; \
  popCount _ = error "You cannot call popCount on symbolic variables"; \
  {-# INLINE popCount #-}

#if 1
BITS_BV(SymIntN, True)
BITS_BV(SymWordN, False)
#endif

-- FiniteBits

#define FINITE_BITS_BV(symtype) \
instance (KnownNat n, 1 <= n) => FiniteBits (symtype n) where \
  finiteBitSize _ = fromIntegral $ natVal (Proxy @n); \
  {-# INLINE finiteBitSize #-}; \

#if 1
FINITE_BITS_BV(SymIntN)
FINITE_BITS_BV(SymWordN)
#endif

-- Show

#define SHOW_BV(symtype) \
instance (KnownNat n, 1 <= n) => Show (symtype n) where \
  show (symtype t) = pformat t

#if 1
SHOW_BV(SymIntN)
SHOW_BV(SymWordN)
#endif

-- Hashable

#define HASHABLE_BV(symtype) \
instance (KnownNat n, 1 <= n) => Hashable (symtype n) where \
  hashWithSalt s (symtype v) = s `hashWithSalt` v

#if 1
HASHABLE_BV(SymIntN)
HASHABLE_BV(SymWordN)
#endif

-- Eq

#define EQ_BV(symtype) \
instance (KnownNat n, 1 <= n) => Eq (symtype n) where \
  (symtype l) == (symtype r) = l == r

#if 1
EQ_BV(SymIntN)
EQ_BV(SymWordN)
#endif

-- IsString

#define IS_STRING_BV(symtype) \
instance (KnownNat n, 1 <= n) => IsString (symtype n) where \
  fromString = ssym . fromString

#if 1
IS_STRING_BV(SymIntN)
IS_STRING_BV(SymWordN)
#endif

-- SizedBV

#define BVCONCAT_SIZED(symtype) \
sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => symtype l -> symtype r -> symtype (l + r); \
sizedBVConcat (symtype l) (symtype r) = \
  case (leqAddPos pl pr, knownAdd (KnownProof @l) (KnownProof @r)) of \
    (LeqProof, KnownProof) -> \
      symtype (pevalBVConcatTerm l r); \
  where; \
    pl = Proxy :: Proxy l; \
    pr = Proxy :: Proxy r

#define BVZEXT_SIZED(symtype) \
sizedBVZext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> symtype l -> symtype r; \
sizedBVZext _ (symtype v) = \
  case leqTrans (LeqProof @1 @l) (LeqProof @l @r) of \
    LeqProof -> symtype $ pevalBVExtendTerm False (Proxy @r) v

#define BVSEXT_SIZED(symtype) \
sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> symtype l -> symtype r; \
sizedBVSext _ (symtype v) = \
  case leqTrans (LeqProof @1 @l) (LeqProof @l @r) of \
    LeqProof -> symtype $ pevalBVExtendTerm True (Proxy @r) v

#define BVSELECT_SIZED(symtype) \
sizedBVSelect :: forall n ix w p q. (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) => \
  p ix -> q w -> symtype n -> symtype w; \
sizedBVSelect pix pw (symtype v) = symtype $ pevalBVSelectTerm pix pw v

#if 1
instance SizedBV SymIntN where
  BVCONCAT_SIZED(SymIntN)
  BVZEXT_SIZED(SymIntN)
  BVSEXT_SIZED(SymIntN)
  sizedBVExt :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> SymIntN l -> SymIntN r
sizedBVExt = proxy r -> SymIntN l -> SymIntN r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> SymIntN l -> SymIntN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext
  BVSELECT_SIZED(SymIntN)

instance SizedBV SymWordN where
  BVCONCAT_SIZED(SymWordN)
  BVZEXT_SIZED(SymWordN)
  BVSEXT_SIZED(SymWordN)
  sizedBVExt :: forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> SymWordN l -> SymWordN r
sizedBVExt = proxy r -> SymWordN l -> SymWordN r
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> SymWordN l -> SymWordN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext
  BVSELECT_SIZED(SymWordN)
#endif

-- BV

#define BVCONCAT(somety, origty) \
bvConcat (somety (a :: origty l)) (somety (b :: origty r)) = \
  case (leqAddPos (Proxy @l) (Proxy @r), knownAdd @l @r KnownProof KnownProof) of \
    (LeqProof, KnownProof) -> \
      somety $ sizedBVConcat a b

#define BVZEXT(somety, origty) \
bvZext l (somety (a :: origty n)) \
  | l < n = error "bvZext: trying to zero extend a value to a smaller size" \
  | otherwise = res (Proxy @n) \
  where \
    n = fromIntegral $ natVal (Proxy @n); \
    res :: forall (l :: Nat). Proxy l -> somety; \
    res p = \
      case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
        (KnownProof, LeqProof, LeqProof) -> somety $ sizedBVZext p a

#define BVSEXT(somety, origty) \
bvSext l (somety (a :: origty n)) \
  | l < n = error "bvZext: trying to zero extend a value to a smaller size" \
  | otherwise = res (Proxy @n) \
  where \
    n = fromIntegral $ natVal (Proxy @n); \
    res :: forall (l :: Nat). Proxy l -> somety; \
    res p = \
      case (unsafeKnownProof @l (fromIntegral l), unsafeLeqProof @1 @l, unsafeLeqProof @n @l) of \
        (KnownProof, LeqProof, LeqProof) -> somety $ sizedBVSext p a

#define BVSELECT(somety, origty) \
bvSelect ix w (somety (a :: origty n)) \
    | ix + w > n = error "bvSelect: trying to select a bitvector outside the bounds of the input" \
    | w == 0 = error "bvSelect: trying to select a bitvector of size 0" \
    | otherwise = res (Proxy @n) (Proxy @n) \
    where \
      n = fromIntegral $ natVal (Proxy @n); \
      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> somety; \
      res _ _ = \
        case ( unsafeKnownProof @ix (fromIntegral ix), \
               unsafeKnownProof @w (fromIntegral w), \
               unsafeLeqProof @1 @w, \
               unsafeLeqProof @(ix + w) @n \
             ) of \
          (KnownProof, KnownProof, LeqProof, LeqProof) -> \
            somety $ sizedBVSelect (Proxy @ix) (Proxy @w) a

#define BVBV(somety, origty) \
  bv n i = case mkNatRepr n of \
    Some (natRepr :: NatRepr x) -> \
      case unsafeLeqProof @1 @x of \
        LeqProof -> withKnownNat natRepr $ \
          somety (fromIntegral i :: origty x)

-- BVSignConversion

instance (KnownNat n, 1 <= n) => SignConversion (SymWordN n) (SymIntN n) where
  toSigned :: SymWordN n -> SymIntN n
toSigned (SymWordN Term (WordN n)
n) = Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (IntN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (WordN n) -> Term (IntN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (u n) -> Term (s n)
pevalBVToSignedTerm Term (WordN n)
n
  toUnsigned :: SymIntN n -> SymWordN n
toUnsigned (SymIntN Term (IntN n)
n) = Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term (IntN n) -> Term (WordN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Term (IntN n) -> Term (WordN n)
forall (u :: Nat -> *) (s :: Nat -> *) (n :: Nat).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (s n) -> Term (u n)
pevalBVToUnsignedTerm Term (IntN n)
n

-- SymShift
instance (KnownNat n, 1 <= n) => SymShift (SymWordN n) where
  symShift :: SymWordN n -> SymWordN n -> SymWordN n
symShift (SymWordN Term (WordN n)
a) (SymWordN Term (WordN n)
s) = Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term (WordN n)
a Term (WordN n)
s
  symShiftNegated :: SymWordN n -> SymWordN n -> SymWordN n
symShiftNegated (SymWordN Term (WordN n)
a) (SymWordN Term (WordN n)
s) = Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> SymWordN n) -> Term (WordN n) -> SymWordN n
forall a b. (a -> b) -> a -> b
$ Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term (WordN n)
a Term (WordN n)
s

instance (KnownNat n, 1 <= n) => SymShift (SymIntN n) where
  symShift :: SymIntN n -> SymIntN n -> SymIntN n
symShift SymIntN n
a SymIntN n
_ | SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = SymIntN n
a
  symShift as :: SymIntN n
as@(SymIntN Term (IntN n)
a) (SymIntN Term (IntN n)
s)
    | SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 =
        Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
          Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
            (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeOrdTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0))
            (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term (IntN n)
a Term (IntN n)
s)
            ( Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
                (Term (IntN n) -> Term (IntN n) -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (-IntN n
2)))
                ( Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
                    (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeOrdTerm Term (IntN n)
a (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0))
                    (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0)
                    (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (-IntN n
1))
                )
                (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term (IntN n)
a (Term (IntN n) -> Term (IntN n)
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term (IntN n)
s))
            )
  symShift (SymIntN Term (IntN n)
a) (SymIntN Term (IntN n)
s) =
    Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
      Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
        (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeOrdTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0))
        (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term (IntN n)
a Term (IntN n)
s)
        ( Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
            (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (-IntN n
bs)))
            (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term (IntN n)
a (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
bs))
            (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term (IntN n)
a (Term (IntN n) -> Term (IntN n)
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term (IntN n)
s))
        )
    where
      bs :: IntN n
bs = Int -> IntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (IntN n
0 :: IntN n)) :: IntN n
  symShiftNegated :: SymIntN n -> SymIntN n -> SymIntN n
symShiftNegated (SymIntN Term (IntN n)
a) (SymIntN Term (IntN n)
s) =
    Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
      Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
        (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalGeOrdTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0))
        (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term (IntN n)
a Term (IntN n)
s)
        ( Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
            (Term (IntN n) -> Term (IntN n) -> Term Bool
forall a. PEvalOrdTerm a => Term a -> Term a -> Term Bool
pevalLeOrdTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (-IntN n
bs)))
            (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0)
            (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term (IntN n)
a (Term (IntN n) -> Term (IntN n)
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term (IntN n)
s))
        )
    where
      bs :: IntN n
bs = Int -> IntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (IntN n
0 :: IntN n)) :: IntN n

-- SymRotate
instance (KnownNat n, 1 <= n) => SymRotate (SymWordN n) where
  symRotate :: SymWordN n -> SymWordN n -> SymWordN n
symRotate (SymWordN Term (WordN n)
a) (SymWordN Term (WordN n)
s) = Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateLeftTerm Term (WordN n)
a Term (WordN n)
s)
  symRotateNegated :: SymWordN n -> SymWordN n -> SymWordN n
symRotateNegated (SymWordN Term (WordN n)
a) (SymWordN Term (WordN n)
s) =
    Term (WordN n) -> SymWordN n
forall (n :: Nat). Term (WordN n) -> SymWordN n
SymWordN (Term (WordN n) -> Term (WordN n) -> Term (WordN n)
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateRightTerm Term (WordN n)
a Term (WordN n)
s)

instance (KnownNat n, 1 <= n) => SymRotate (SymIntN n) where
  symRotate :: SymIntN n -> SymIntN n -> SymIntN n
symRotate as :: SymIntN n
as@(SymIntN Term (IntN n)
a) (SymIntN Term (IntN n)
s)
    | SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = SymIntN n
as
    | SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 =
        Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
          Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
            ( Term Bool -> Term Bool -> Term Bool
pevalOrTerm
                (Term (IntN n) -> Term (IntN n) -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0))
                (Term (IntN n) -> Term (IntN n) -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (-IntN n
2)))
            )
            Term (IntN n)
a
            (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateLeftTerm Term (IntN n)
a (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
1))
    | Bool
otherwise =
        Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
          Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateLeftTerm
            Term (IntN n)
a
            ( Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalModIntegralTerm
                Term (IntN n)
s
                (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Int -> IntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> IntN n) -> Int -> IntN n
forall a b. (a -> b) -> a -> b
$ SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
as))
            )
  symRotateNegated :: SymIntN n -> SymIntN n -> SymIntN n
symRotateNegated as :: SymIntN n
as@(SymIntN Term (IntN n)
a) (SymIntN Term (IntN n)
s)
    | SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = SymIntN n
as
    | SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 =
        Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
          Term Bool -> Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm
            ( Term Bool -> Term Bool -> Term Bool
pevalOrTerm
                (Term (IntN n) -> Term (IntN n) -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
0))
                (Term (IntN n) -> Term (IntN n) -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term (IntN n)
s (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (-IntN n
2)))
            )
            Term (IntN n)
a
            (Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateLeftTerm Term (IntN n)
a (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm IntN n
1))
    | Bool
otherwise =
        Term (IntN n) -> SymIntN n
forall (n :: Nat). Term (IntN n) -> SymIntN n
SymIntN (Term (IntN n) -> SymIntN n) -> Term (IntN n) -> SymIntN n
forall a b. (a -> b) -> a -> b
$
          Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateRightTerm
            Term (IntN n)
a
            ( Term (IntN n) -> Term (IntN n) -> Term (IntN n)
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalModIntegralTerm
                Term (IntN n)
s
                (IntN n -> Term (IntN n)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (Int -> IntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> IntN n) -> Int -> IntN n
forall a b. (a -> b) -> a -> b
$ SymIntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize SymIntN n
as))
            )

#define ALLSYMS_BV(t) \
instance (KnownNat n, 1 <= n) => AllSyms (t n) where \
  allSymsS v = (SomeSym v :)

#if 1
ALLSYMS_BV(SymIntN)
ALLSYMS_BV(SymWordN)
#endif