{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.SomeBV
-- 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.SomeBV
  ( SomeBV (..),

    -- * Constructing and pattern matching on SomeBV
    unsafeSomeBV,
    conBV,
    conBVView,
    pattern ConBV,
    symBV,
    ssymBV,
    isymBV,
    arbitraryBV,

    -- * Synonyms
    pattern SomeIntN,
    type SomeIntN,
    pattern SomeWordN,
    type SomeWordN,
    pattern SomeSymIntN,
    type SomeSymIntN,
    pattern SomeSymWordN,
    type SomeSymWordN,

    -- * Helpers for manipulating SomeBV
    unarySomeBV,
    unarySomeBVR1,
    binSomeBV,
    binSomeBVR1,
    binSomeBVR2,
    binSomeBVSafe,
    binSomeBVSafeR1,
    binSomeBVSafeR2,
  )
where

import Control.DeepSeq (NFData (rnf))
import Control.Exception (throw)
import Control.Monad.Except (ExceptT, MonadError)
import Data.Bifunctor (Bifunctor (bimap))
import Data.Bits
  ( Bits
      ( bit,
        bitSize,
        bitSizeMaybe,
        clearBit,
        complement,
        complementBit,
        isSigned,
        popCount,
        rotate,
        rotateL,
        rotateR,
        setBit,
        shift,
        shiftL,
        shiftR,
        testBit,
        unsafeShiftL,
        unsafeShiftR,
        xor,
        zeroBits,
        (.&.),
        (.|.)
      ),
    FiniteBits (countLeadingZeros, countTrailingZeros, finiteBitSize),
  )
import Data.Data (Proxy (Proxy))
import Data.Hashable (Hashable (hashWithSalt))
import Data.Maybe (fromJust)
import Data.Type.Equality (type (:~:) (Refl))
import GHC.TypeNats
  ( KnownNat,
    Nat,
    natVal,
    sameNat,
    type (+),
    type (<=),
  )
import Grisette.Internal.Core.Control.Monad.UnionM (UnionM)
import Grisette.Internal.Core.Data.Class.BitVector
  ( BV (bv, bvConcat, bvExt, bvSelect, bvSext, bvZext),
    SizedBV
      ( sizedBVConcat,
        sizedBVExt,
        sizedBVFromIntegral,
        sizedBVSelect,
        sizedBVSext,
        sizedBVZext
      ),
  )
import Grisette.Internal.Core.Data.Class.EvaluateSym
  ( EvaluateSym (evaluateSym),
  )
import Grisette.Internal.Core.Data.Class.ExtractSymbolics
  ( ExtractSymbolics (extractSymbolics),
  )
import Grisette.Internal.Core.Data.Class.GPretty
  ( GPretty (gpretty),
  )
import Grisette.Internal.Core.Data.Class.GenSym
  ( GenSym (fresh),
    GenSymSimple (simpleFresh),
  )
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Core.Data.Class.Mergeable
  ( Mergeable (rootStrategy),
    MergingStrategy (SortedStrategy),
    wrapStrategy,
  )
import Grisette.Internal.Core.Data.Class.SEq (SEq ((./=), (.==)))
import Grisette.Internal.Core.Data.Class.SOrd
  ( SOrd (symCompare, (.<), (.<=), (.>), (.>=)),
  )
import Grisette.Internal.Core.Data.Class.SafeDivision
  ( SafeDivision (safeDiv, safeDivMod, safeMod, safeQuot, safeQuotRem, safeRem),
  )
import Grisette.Internal.Core.Data.Class.SafeLinearArith
  ( SafeLinearArith (safeAdd, safeNeg, safeSub),
  )
import Grisette.Internal.Core.Data.Class.SafeSymRotate
  ( SafeSymRotate (safeSymRotateL, safeSymRotateR),
  )
import Grisette.Internal.Core.Data.Class.SafeSymShift
  ( SafeSymShift
      ( safeSymShiftL,
        safeSymShiftR,
        safeSymStrictShiftL,
        safeSymStrictShiftR
      ),
  )
import Grisette.Internal.Core.Data.Class.SignConversion
  ( SignConversion (toSigned, toUnsigned),
  )
import Grisette.Internal.Core.Data.Class.Solvable
  ( Solvable (con, conView, isym, ssym, sym),
  )
import Grisette.Internal.Core.Data.Class.SubstituteSym
  ( SubstituteSym (substituteSym),
  )
import Grisette.Internal.Core.Data.Class.SymRotate (SymRotate (symRotate, symRotateNegated))
import Grisette.Internal.Core.Data.Class.SymShift (SymShift (symShift, symShiftNegated))
import Grisette.Internal.Core.Data.Class.ToCon (ToCon (toCon))
import Grisette.Internal.Core.Data.Class.ToSym (ToSym (toSym))
import Grisette.Internal.Core.Data.Class.TryMerge (TryMerge)
import Grisette.Internal.Core.Data.Symbol (Identifier, Symbol)
import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSyms, allSymsS))
import Grisette.Internal.SymPrim.BV
  ( BitwidthMismatch (BitwidthMismatch),
    IntN,
    WordN,
  )
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN,
    SymWordN,
  )
import Grisette.Internal.Utils.Parameterized
  ( KnownProof (KnownProof),
    LeqProof (LeqProof),
    NatRepr,
    SomePositiveNatRepr (SomePositiveNatRepr),
    knownAdd,
    leqAddPos,
    mkPositiveNatRepr,
    unsafeKnownProof,
    unsafeLeqProof,
  )
import Grisette.Lib.Control.Monad.Except (mrgModifyError, mrgThrowError)
import Grisette.Lib.Data.Functor (mrgFmap)
import Language.Haskell.TH.Syntax (Lift (liftTyped))
import Test.QuickCheck (Arbitrary (arbitrary), Gen)
import Unsafe.Coerce (unsafeCoerce)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> :set -XDataKinds
-- >>> :set -XBinaryLiterals
-- >>> :set -XFlexibleContexts
-- >>> :set -XFlexibleInstances
-- >>> :set -XFunctionalDependencies

-- | Non-indexed bitvectors.
data SomeBV bv where
  SomeBV :: (KnownNat n, 1 <= n) => bv n -> SomeBV bv

instance
  (forall n. (KnownNat n, 1 <= n) => Hashable (bv n)) =>
  Hashable (SomeBV bv)
  where
  hashWithSalt :: Int -> SomeBV bv -> Int
hashWithSalt Int
s (SomeBV (bv n
bv :: bv n)) =
    Int
s Int -> Nat -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) Int -> bv n -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` bv n
bv
  {-# INLINE hashWithSalt #-}

instance
  (forall n. (KnownNat n, 1 <= n) => Lift (bv n)) =>
  Lift (SomeBV bv)
  where
  liftTyped :: forall (m :: * -> *). Quote m => SomeBV bv -> Code m (SomeBV bv)
liftTyped (SomeBV bv n
bv) = [||bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n
bv||]

instance
  (forall n. (KnownNat n, 1 <= n) => Show (bv n)) =>
  Show (SomeBV bv)
  where
  show :: SomeBV bv -> String
show (SomeBV bv n
bv) = bv n -> String
forall a. Show a => a -> String
show bv n
bv
  {-# INLINE show #-}

instance
  (forall n. (KnownNat n, 1 <= n) => NFData (bv n)) =>
  NFData (SomeBV bv)
  where
  rnf :: SomeBV bv -> ()
rnf (SomeBV bv n
bv) = bv n -> ()
forall a. NFData a => a -> ()
rnf bv n
bv
  {-# INLINE rnf #-}

instance (forall n. (KnownNat n, 1 <= n) => Eq (bv n)) => Eq (SomeBV bv) where
  == :: SomeBV bv -> SomeBV bv -> Bool
(==) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Eq a => a -> a -> Bool
(==)
  {-# INLINE (==) #-}
  /= :: SomeBV bv -> SomeBV bv -> Bool
(/=) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
  {-# INLINE (/=) #-}

instance (forall n. (KnownNat n, 1 <= n) => Ord (bv n)) => Ord (SomeBV bv) where
  < :: SomeBV bv -> SomeBV bv -> Bool
(<) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
(<)
  {-# INLINE (<) #-}
  <= :: SomeBV bv -> SomeBV bv -> Bool
(<=) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
  {-# INLINE (<=) #-}
  > :: SomeBV bv -> SomeBV bv -> Bool
(>) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
(>)
  {-# INLINE (>) #-}
  >= :: SomeBV bv -> SomeBV bv -> Bool
(>=) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
  {-# INLINE (>=) #-}
  max :: SomeBV bv -> SomeBV bv -> SomeBV bv
max = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Ord a => a -> a -> a
max
  {-# INLINE max #-}
  min :: SomeBV bv -> SomeBV bv -> SomeBV bv
min = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Ord a => a -> a -> a
min
  {-# INLINE min #-}
  compare :: SomeBV bv -> SomeBV bv -> Ordering
compare = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> Ordering)
-> SomeBV bv -> SomeBV bv -> Ordering
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Ordering
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
  {-# INLINE compare #-}

instance (forall n. (KnownNat n, 1 <= n) => Num (bv n)) => Num (SomeBV bv) where
  + :: SomeBV bv -> SomeBV bv -> SomeBV bv
(+) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Num a => a -> a -> a
(+)
  {-# INLINE (+) #-}
  (-) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 (-)
  {-# INLINE (-) #-}
  * :: SomeBV bv -> SomeBV bv -> SomeBV bv
(*) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Num a => a -> a -> a
(*)
  {-# INLINE (*) #-}
  negate :: SomeBV bv -> SomeBV bv
negate = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
forall a. Num a => a -> a
negate
  {-# INLINE negate #-}
  abs :: SomeBV bv -> SomeBV bv
abs = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
forall a. Num a => a -> a
abs
  {-# INLINE abs #-}
  signum :: SomeBV bv -> SomeBV bv
signum = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
forall a. Num a => a -> a
signum
  {-# INLINE signum #-}
  fromInteger :: Integer -> SomeBV bv
fromInteger =
    String -> Integer -> SomeBV bv
forall a. HasCallStack => String -> a
error (String -> Integer -> SomeBV bv) -> String -> Integer -> SomeBV bv
forall a b. (a -> b) -> a -> b
$
      String
"fromInteger is not defined for SomeBV as no bitwidth is known, use "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(bv <bitwidth> <value>) instead"
  {-# INLINE fromInteger #-}

instance
  (forall n. (KnownNat n, 1 <= n) => Bits (bv n)) =>
  Bits (SomeBV bv)
  where
  .&. :: SomeBV bv -> SomeBV bv -> SomeBV bv
(.&.) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Bits a => a -> a -> a
(.&.)
  .|. :: SomeBV bv -> SomeBV bv -> SomeBV bv
(.|.) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Bits a => a -> a -> a
(.|.)
  xor :: SomeBV bv -> SomeBV bv -> SomeBV bv
xor = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Bits a => a -> a -> a
xor
  complement :: SomeBV bv -> SomeBV bv
complement = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
forall a. Bits a => a -> a
complement
  shift :: SomeBV bv -> Int -> SomeBV bv
shift SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`shift` Int
i) SomeBV bv
s
  rotate :: SomeBV bv -> Int -> SomeBV bv
rotate SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`rotate` Int
i) SomeBV bv
s
  zeroBits :: SomeBV bv
zeroBits =
    String -> SomeBV bv
forall a. HasCallStack => String -> a
error (String -> SomeBV bv) -> String -> SomeBV bv
forall a b. (a -> b) -> a -> b
$
      String
"zeroBits is not defined for SomeBV as no bitwidth is known, use "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(bv <bitwidth> 0) or (SomeBV (zeroBits :: bv <bitwidth>)) instead"
  bit :: Int -> SomeBV bv
bit =
    String -> Int -> SomeBV bv
forall a. HasCallStack => String -> a
error (String -> Int -> SomeBV bv) -> String -> Int -> SomeBV bv
forall a b. (a -> b) -> a -> b
$
      String
"bit is not defined for SomeBV as no bitwidth is known, use "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(SomeBV (bit <bit> :: bv <bitwidth>)) instead"
  setBit :: SomeBV bv -> Int -> SomeBV bv
setBit SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`setBit` Int
i) SomeBV bv
s
  clearBit :: SomeBV bv -> Int -> SomeBV bv
clearBit SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`clearBit` Int
i) SomeBV bv
s
  complementBit :: SomeBV bv -> Int -> SomeBV bv
complementBit SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`complementBit` Int
i) SomeBV bv
s
  testBit :: SomeBV bv -> Int -> Bool
testBit SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Bool)
-> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV (bv n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i) SomeBV bv
s
  bitSizeMaybe :: SomeBV bv -> Maybe Int
bitSizeMaybe = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Maybe Int)
-> SomeBV bv -> Maybe Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Maybe Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Maybe Int
forall a. Bits a => a -> Maybe Int
bitSizeMaybe
  bitSize :: SomeBV bv -> Int
bitSize = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> (SomeBV bv -> Maybe Int) -> SomeBV bv -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Maybe Int)
-> SomeBV bv -> Maybe Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Maybe Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Maybe Int
forall a. Bits a => a -> Maybe Int
bitSizeMaybe
  isSigned :: SomeBV bv -> Bool
isSigned SomeBV bv
_ = Bool
False
  shiftL :: SomeBV bv -> Int -> SomeBV bv
shiftL SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i) SomeBV bv
s
  unsafeShiftL :: SomeBV bv -> Int -> SomeBV bv
unsafeShiftL SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
i) SomeBV bv
s
  shiftR :: SomeBV bv -> Int -> SomeBV bv
shiftR SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`shiftR` Int
i) SomeBV bv
s
  unsafeShiftR :: SomeBV bv -> Int -> SomeBV bv
unsafeShiftR SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`unsafeShiftR` Int
i) SomeBV bv
s
  rotateL :: SomeBV bv -> Int -> SomeBV bv
rotateL SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`rotateL` Int
i) SomeBV bv
s
  rotateR :: SomeBV bv -> Int -> SomeBV bv
rotateR SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`rotateR` Int
i) SomeBV bv
s
  popCount :: SomeBV bv -> Int
popCount = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int
forall a. Bits a => a -> Int
popCount

instance
  (forall n. (KnownNat n, 1 <= n) => FiniteBits (bv n)) =>
  FiniteBits (SomeBV bv)
  where
  finiteBitSize :: SomeBV bv -> Int
finiteBitSize = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
  {-# INLINE finiteBitSize #-}
  countLeadingZeros :: SomeBV bv -> Int
countLeadingZeros = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros
  {-# INLINE countLeadingZeros #-}
  countTrailingZeros :: SomeBV bv -> Int
countTrailingZeros = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int
forall b. FiniteBits b => b -> Int
countTrailingZeros
  {-# INLINE countTrailingZeros #-}

instance
  (forall n. (KnownNat n, 1 <= n) => Enum (bv n)) =>
  Enum (SomeBV bv)
  where
  toEnum :: Int -> SomeBV bv
toEnum =
    String -> Int -> SomeBV bv
forall a. HasCallStack => String -> a
error (String -> Int -> SomeBV bv) -> String -> Int -> SomeBV bv
forall a b. (a -> b) -> a -> b
$
      String
"toEnum is not defined for SomeBV, use "
        String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(SomeBV (toEnum <value> :: bv <bitwidth>)) instead"
  {-# INLINE toEnum #-}
  fromEnum :: SomeBV bv -> Int
fromEnum = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int
forall a. Enum a => a -> Int
fromEnum
  {-# INLINE fromEnum #-}

instance
  (forall n. (KnownNat n, 1 <= n) => Real (bv n)) =>
  Real (SomeBV bv)
  where
  toRational :: SomeBV bv -> Rational
toRational = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Rational)
-> SomeBV bv -> Rational
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Rational
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Rational
forall a. Real a => a -> Rational
toRational
  {-# INLINE toRational #-}

instance
  (forall n. (KnownNat n, 1 <= n) => Integral (bv n)) =>
  Integral (SomeBV bv)
  where
  toInteger :: SomeBV bv -> Integer
toInteger = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Integer)
-> SomeBV bv -> Integer
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Integer
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Integer
forall a. Integral a => a -> Integer
toInteger
  {-# INLINE toInteger #-}
  quot :: SomeBV bv -> SomeBV bv -> SomeBV bv
quot = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Integral a => a -> a -> a
quot
  {-# INLINE quot #-}
  rem :: SomeBV bv -> SomeBV bv -> SomeBV bv
rem = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Integral a => a -> a -> a
rem
  {-# INLINE rem #-}
  div :: SomeBV bv -> SomeBV bv -> SomeBV bv
div = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Integral a => a -> a -> a
div
  {-# INLINE div #-}
  mod :: SomeBV bv -> SomeBV bv -> SomeBV bv
mod = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Integral a => a -> a -> a
mod
  {-# INLINE mod #-}
  quotRem :: SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
quotRem = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
forall (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
binSomeBVR2 bv n -> bv n -> (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n)
forall a. Integral a => a -> a -> (a, a)
quotRem
  {-# INLINE quotRem #-}
  divMod :: SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
divMod = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
forall (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
binSomeBVR2 bv n -> bv n -> (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n)
forall a. Integral a => a -> a -> (a, a)
divMod
  {-# INLINE divMod #-}

instance (SizedBV bv) => BV (SomeBV bv) where
  bvConcat :: SomeBV bv -> SomeBV bv -> SomeBV bv
bvConcat (SomeBV (bv n
a :: bv l)) (SomeBV (bv n
b :: bv r)) =
    case ( Proxy n -> Proxy n -> LeqProof 1 (n + n)
forall (m :: Nat) (n :: Nat) (p :: Nat -> *) (q :: Nat -> *).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r),
           forall (m :: Nat) (n :: Nat).
KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd @l @r KnownProof n
forall (n :: Nat). KnownNat n => KnownProof n
KnownProof KnownProof n
forall (n :: Nat). KnownNat n => KnownProof n
KnownProof
         ) of
      (LeqProof 1 (n + n)
LeqProof, KnownProof (n + n)
KnownProof) ->
        bv (n + n) -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv (n + n) -> SomeBV bv) -> bv (n + n) -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> bv (n + n)
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat bv n
a bv n
b
  {-# INLINE bvConcat #-}
  bvZext :: Int -> SomeBV bv -> SomeBV bv
bvZext Int
l (SomeBV (bv n
a :: bv n))
    | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = String -> SomeBV bv
forall a. HasCallStack => String -> a
error String
"bvZext: trying to zero extend a value to a smaller size"
    | Bool
otherwise = Proxy n -> SomeBV bv
forall (l :: Nat). Proxy l -> SomeBV bv
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      res :: forall (l :: Nat). Proxy l -> SomeBV bv
      res :: forall (l :: Nat). Proxy l -> SomeBV bv
res Proxy l
p =
        case ( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @l (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l),
               forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l,
               forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @n @l
             ) of
          (KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> bv l -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv l -> SomeBV bv) -> bv l -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Proxy l -> bv n -> bv l
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv 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 Proxy l
p bv n
a
  {-# INLINE bvZext #-}
  bvSext :: Int -> SomeBV bv -> SomeBV bv
bvSext Int
l (SomeBV (bv n
a :: bv n))
    | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = String -> SomeBV bv
forall a. HasCallStack => String -> a
error String
"bvSext: trying to zero extend a value to a smaller size"
    | Bool
otherwise = Proxy n -> SomeBV bv
forall (l :: Nat). Proxy l -> SomeBV bv
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      res :: forall (l :: Nat). Proxy l -> SomeBV bv
      res :: forall (l :: Nat). Proxy l -> SomeBV bv
res Proxy l
p =
        case ( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @l (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l),
               forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l,
               forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @n @l
             ) of
          (KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> bv l -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv l -> SomeBV bv) -> bv l -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Proxy l -> bv n -> bv l
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv 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 Proxy l
p bv n
a
  {-# INLINE bvSext #-}
  bvExt :: Int -> SomeBV bv -> SomeBV bv
bvExt Int
l (SomeBV (bv n
a :: bv n))
    | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = String -> SomeBV bv
forall a. HasCallStack => String -> a
error String
"bvExt: trying to zero extend a value to a smaller size"
    | Bool
otherwise = Proxy n -> SomeBV bv
forall (l :: Nat). Proxy l -> SomeBV bv
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      res :: forall (l :: Nat). Proxy l -> SomeBV bv
      res :: forall (l :: Nat). Proxy l -> SomeBV bv
res Proxy l
p =
        case ( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @l (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l),
               forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l,
               forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @n @l
             ) of
          (KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> bv l -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv l -> SomeBV bv) -> bv l -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Proxy l -> bv n -> bv l
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv 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
sizedBVExt Proxy l
p bv n
a
  {-# INLINE bvExt #-}
  bvSelect :: Int -> Int -> SomeBV bv -> SomeBV bv
bvSelect Int
ix Int
w (SomeBV (bv n
a :: bv n))
    | Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n =
        String -> SomeBV bv
forall a. HasCallStack => String -> a
error (String -> SomeBV bv) -> String -> SomeBV bv
forall a b. (a -> b) -> a -> b
$
          String
"bvSelect: trying to select a bitvector outside the bounds of the "
            String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"input"
    | Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = String -> SomeBV bv
forall a. HasCallStack => String -> a
error String
"bvSelect: trying to select a bitvector of size 0"
    | Bool
otherwise = Proxy n -> Proxy n -> SomeBV bv
forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeBV bv
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeBV bv
      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeBV bv
res Proxy w
_ Proxy ix
_ =
        case ( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @ix (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
ix),
               forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @w (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
w),
               forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @w,
               forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(ix + w) @n
             ) of
          (KnownProof ix
KnownProof, KnownProof w
KnownProof, LeqProof 1 w
LeqProof, LeqProof (ix + w) n
LeqProof) ->
            bv w -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv w -> SomeBV bv) -> bv w -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Proxy ix -> Proxy w -> bv n -> bv w
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
       (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
sizedBVSelect (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @ix) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) bv n
a
  bv :: forall a. Integral a => Int -> a -> SomeBV bv
bv Int
n a
i = Int
-> (forall {proxy :: Nat -> *} {n :: Nat}.
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
forall (bv :: Nat -> *).
Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
unsafeSomeBV Int
n ((forall {proxy :: Nat -> *} {n :: Nat}.
  (KnownNat n, 1 <= n) =>
  proxy n -> bv n)
 -> SomeBV bv)
-> (forall {proxy :: Nat -> *} {n :: Nat}.
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
forall a b. (a -> b) -> a -> b
$ \proxy n
_ -> a -> bv n
forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> bv n
forall (bv :: Nat -> *) a (n :: Nat).
(SizedBV bv, Integral a, KnownNat n, 1 <= n) =>
a -> bv n
sizedBVFromIntegral a
i
  {-# INLINE bv #-}

instance
  (forall n. (KnownNat n, 1 <= n) => EvaluateSym (bv n)) =>
  EvaluateSym (SomeBV bv)
  where
  evaluateSym :: Bool -> Model -> SomeBV bv -> SomeBV bv
evaluateSym Bool
fillDefault Model
model = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (Bool -> Model -> bv n -> bv n
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model)
  {-# INLINE evaluateSym #-}

instance
  (forall n. (KnownNat n, 1 <= n) => ExtractSymbolics (bv n)) =>
  ExtractSymbolics (SomeBV bv)
  where
  extractSymbolics :: SomeBV bv -> SymbolSet
extractSymbolics = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> SymbolSet)
-> SomeBV bv -> SymbolSet
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> SymbolSet
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics
  {-# INLINE extractSymbolics #-}

instance
  (forall n. (KnownNat n, 1 <= n) => GPretty (bv n)) =>
  GPretty (SomeBV bv)
  where
  gpretty :: forall ann. SomeBV bv -> Doc ann
gpretty (SomeBV bv n
bv) = bv n -> Doc ann
forall ann. bv n -> Doc ann
forall a ann. GPretty a => a -> Doc ann
gpretty bv n
bv
  {-# INLINE gpretty #-}

data CompileTimeNat where
  CompileTimeNat :: (KnownNat n, 1 <= n) => Proxy n -> CompileTimeNat

instance Show CompileTimeNat where
  show :: CompileTimeNat -> String
show (CompileTimeNat (Proxy n
Proxy :: Proxy n)) = Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
  {-# INLINE show #-}

instance Eq CompileTimeNat where
  CompileTimeNat (Proxy n
Proxy :: Proxy n) == :: CompileTimeNat -> CompileTimeNat -> Bool
== CompileTimeNat (Proxy n
Proxy :: Proxy m) =
    case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) of
      Just n :~: n
Refl -> Bool
True
      Maybe (n :~: n)
Nothing -> Bool
False
  {-# INLINE (==) #-}

instance Ord CompileTimeNat where
  compare :: CompileTimeNat -> CompileTimeNat -> Ordering
compare
    (CompileTimeNat (Proxy n
Proxy :: Proxy n))
    (CompileTimeNat (Proxy n
Proxy :: Proxy m)) =
      Nat -> Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m))
  {-# INLINE compare #-}

instance
  (forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
  Mergeable (SomeBV bv)
  where
  rootStrategy :: MergingStrategy (SomeBV bv)
rootStrategy =
    forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy @CompileTimeNat
      (\(SomeBV (bv n
_ :: bv n)) -> Proxy n -> CompileTimeNat
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Proxy n -> CompileTimeNat
CompileTimeNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
      ( \(CompileTimeNat (Proxy n
_ :: proxy n)) ->
          MergingStrategy (bv n)
-> (bv n -> SomeBV bv)
-> (SomeBV bv -> bv n)
-> MergingStrategy (SomeBV bv)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy
            (forall a. Mergeable a => MergingStrategy a
rootStrategy @(bv n))
            bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV
            (\(SomeBV bv n
x) -> bv n -> bv n
forall a b. a -> b
unsafeCoerce bv n
x)
      )

instance (forall n. (KnownNat n, 1 <= n) => SEq (bv n)) => SEq (SomeBV bv) where
  .== :: SomeBV bv -> SomeBV bv -> SymBool
(.==) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SEq a => a -> a -> SymBool
(.==)
  {-# INLINE (.==) #-}
  ./= :: SomeBV bv -> SomeBV bv -> SymBool
(./=) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SEq a => a -> a -> SymBool
(./=)
  {-# INLINE (./=) #-}

instance
  (forall n. (KnownNat n, 1 <= n) => SOrd (bv n)) =>
  SOrd (SomeBV bv)
  where
  .< :: SomeBV bv -> SomeBV bv -> SymBool
(.<) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SOrd a => a -> a -> SymBool
(.<)
  {-# INLINE (.<) #-}
  .<= :: SomeBV bv -> SomeBV bv -> SymBool
(.<=) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SOrd a => a -> a -> SymBool
(.<=)
  {-# INLINE (.<=) #-}
  .> :: SomeBV bv -> SomeBV bv -> SymBool
(.>) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SOrd a => a -> a -> SymBool
(.>)
  {-# INLINE (.>) #-}
  .>= :: SomeBV bv -> SomeBV bv -> SymBool
(.>=) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SOrd a => a -> a -> SymBool
(.>=)
  {-# INLINE (.>=) #-}
  symCompare :: SomeBV bv -> SomeBV bv -> UnionM Ordering
symCompare = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> UnionM Ordering)
-> SomeBV bv -> SomeBV bv -> UnionM Ordering
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> UnionM Ordering
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> UnionM Ordering
forall a. SOrd a => a -> a -> UnionM Ordering
symCompare
  {-# INLINE symCompare #-}

instance
  (forall n. (KnownNat n, 1 <= n) => SubstituteSym (bv n)) =>
  SubstituteSym (SomeBV bv)
  where
  substituteSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> SomeBV bv -> SomeBV bv
substituteSym TypedSymbol cb
c sb
s = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (TypedSymbol cb -> sb -> bv n -> bv n
forall a cb sb.
(SubstituteSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> bv n -> bv n
substituteSym TypedSymbol cb
c sb
s)
  {-# INLINE substituteSym #-}

instance
  ( KnownNat n,
    1 <= n,
    forall m. (KnownNat m, 1 <= m) => GenSym () (bv m),
    Mergeable (SomeBV bv)
  ) =>
  GenSym (Proxy n) (SomeBV bv)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
Proxy n -> m (UnionM (SomeBV bv))
fresh Proxy n
_ =
    (\(UnionM (bv n)
i :: UnionM (bv n)) -> (bv n -> SomeBV bv) -> UnionM (bv n) -> UnionM (SomeBV bv)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV UnionM (bv n)
i) (UnionM (bv n) -> UnionM (SomeBV bv))
-> m (UnionM (bv n)) -> m (UnionM (SomeBV bv))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m (UnionM (bv n))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => () -> m (UnionM (bv n))
fresh ()
  {-# INLINE fresh #-}

instance
  ( KnownNat n,
    1 <= n,
    forall m. (KnownNat m, 1 <= m) => GenSymSimple () (bv m),
    Mergeable (SomeBV bv)
  ) =>
  GenSymSimple (Proxy n) (SomeBV bv)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => Proxy n -> m (SomeBV bv)
simpleFresh Proxy n
_ = (\(bv n
i :: bv n) -> bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n
i) (bv n -> SomeBV bv) -> m (bv n) -> m (SomeBV bv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m (bv n)
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m (bv n)
simpleFresh ()
  {-# INLINE simpleFresh #-}

instance
  ( forall m. (KnownNat m, 1 <= m) => GenSym () (bv m),
    Mergeable (SomeBV bv)
  ) =>
  GenSym (SomeBV bv) (SomeBV bv)
  where
  fresh :: forall (m :: * -> *).
MonadFresh m =>
SomeBV bv -> m (UnionM (SomeBV bv))
fresh (SomeBV (bv n
_ :: bv x)) = Proxy n -> m (UnionM (SomeBV bv))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *).
MonadFresh m =>
Proxy n -> m (UnionM (SomeBV bv))
fresh (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)
  {-# INLINE fresh #-}

instance
  ( forall m. (KnownNat m, 1 <= m) => GenSymSimple () (bv m),
    Mergeable (SomeBV bv)
  ) =>
  GenSymSimple (SomeBV bv) (SomeBV bv)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => SomeBV bv -> m (SomeBV bv)
simpleFresh (SomeBV (bv n
_ :: bv x)) = Proxy n -> m (SomeBV bv)
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => Proxy n -> m (SomeBV bv)
simpleFresh (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)
  {-# INLINE simpleFresh #-}

instance
  ( forall n. (KnownNat n, 1 <= n) => GenSym () (bv n),
    Mergeable (SomeBV bv)
  ) =>
  GenSym Int (SomeBV bv)
  where
  fresh :: forall (m :: * -> *). MonadFresh m => Int -> m (UnionM (SomeBV bv))
fresh Int
n
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> m (UnionM (SomeBV bv))
forall a. HasCallStack => String -> a
error String
"fresh: cannot generate a bitvector of non-positive size"
    | Bool
otherwise = case Nat -> SomePositiveNatRepr
mkPositiveNatRepr (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) of
        SomePositiveNatRepr (NatRepr n
_ :: NatRepr x) -> Proxy n -> m (UnionM (SomeBV bv))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *).
MonadFresh m =>
Proxy n -> m (UnionM (SomeBV bv))
fresh (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)
  {-# INLINE fresh #-}

instance
  ( forall n. (KnownNat n, 1 <= n) => GenSymSimple () (bv n),
    Mergeable (SomeBV bv)
  ) =>
  GenSymSimple Int (SomeBV bv)
  where
  simpleFresh :: forall (m :: * -> *). MonadFresh m => Int -> m (SomeBV bv)
simpleFresh Int
n
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> m (SomeBV bv)
forall a. HasCallStack => String -> a
error String
"fresh: cannot generate a bitvector of non-positive size"
    | Bool
otherwise = case Nat -> SomePositiveNatRepr
mkPositiveNatRepr (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) of
        SomePositiveNatRepr (NatRepr n
_ :: NatRepr x) -> Proxy n -> m (SomeBV bv)
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => Proxy n -> m (SomeBV bv)
simpleFresh (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)
  {-# INLINE simpleFresh #-}

instance
  ( forall n. (KnownNat n, 1 <= n) => SignConversion (ubv n) (sbv n),
    -- Add this to help the type checker resolve the functional dependency
    SignConversion (ubv 1) (sbv 1)
  ) =>
  SignConversion (SomeBV ubv) (SomeBV sbv)
  where
  toSigned :: SomeBV ubv -> SomeBV sbv
toSigned (SomeBV (ubv n
n :: ubv n)) = sbv n -> SomeBV sbv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (ubv n -> sbv n
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned ubv n
n :: sbv n)
  {-# INLINE toSigned #-}
  toUnsigned :: SomeBV sbv -> SomeBV ubv
toUnsigned (SomeBV (sbv n
n :: sbv n)) = ubv n -> SomeBV ubv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (sbv n -> ubv n
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned sbv n
n :: ubv n)
  {-# INLINE toUnsigned #-}

instance
  (forall n. (KnownNat n, 1 <= n) => ToCon (sbv n) (cbv n)) =>
  ToCon (SomeBV sbv) (SomeBV cbv)
  where
  toCon :: SomeBV sbv -> Maybe (SomeBV cbv)
toCon (SomeBV (sbv n
n :: sbv n)) = cbv n -> SomeBV cbv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (cbv n -> SomeBV cbv) -> Maybe (cbv n) -> Maybe (SomeBV cbv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (sbv n -> Maybe (cbv n)
forall a b. ToCon a b => a -> Maybe b
toCon sbv n
n :: Maybe (cbv n))
  {-# INLINE toCon #-}

instance
  (forall n. (KnownNat n, 1 <= n) => ToSym (cbv n) (sbv n)) =>
  ToSym (SomeBV cbv) (SomeBV sbv)
  where
  toSym :: SomeBV cbv -> SomeBV sbv
toSym (SomeBV (cbv n
n :: cbv n)) = sbv n -> SomeBV sbv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (cbv n -> sbv n
forall a b. ToSym a b => a -> b
toSym cbv n
n :: sbv n)
  {-# INLINE toSym #-}

instance
  ( forall n.
    (KnownNat n, 1 <= n) =>
    SafeDivision e (bv n) (ExceptT e m),
    MonadError (Either BitwidthMismatch e) m,
    TryMerge m,
    Mergeable e
  ) =>
  SafeDivision (Either BitwidthMismatch e) (SomeBV bv) m
  where
  safeDiv :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeDiv = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
safeDiv @e)
  {-# INLINE safeDiv #-}
  safeMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeMod = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
safeMod @e)
  {-# INLINE safeMod #-}
  safeQuot :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeQuot = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
safeQuot @e)
  {-# INLINE safeQuot #-}
  safeRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeRem = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
safeRem @e)
  {-# INLINE safeRem #-}
  safeDivMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
safeDivMod = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m (a, a)
safeDivMod @e)
  {-# INLINE safeDivMod #-}
  safeQuotRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
safeQuotRem = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m (a, a)
safeQuotRem @e)
  {-# INLINE safeQuotRem #-}

instance
  ( forall n.
    (KnownNat n, 1 <= n) =>
    SafeLinearArith e (bv n) (ExceptT e m),
    MonadError (Either BitwidthMismatch e) m,
    TryMerge m,
    Mergeable e
  ) =>
  SafeLinearArith (Either BitwidthMismatch e) (SomeBV bv) m
  where
  safeAdd :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeAdd = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeLinearArith e a m => a -> a -> m a
safeAdd @e)
  {-# INLINE safeAdd #-}
  safeSub :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSub = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeLinearArith e a m => a -> a -> m a
safeSub @e)
  {-# INLINE safeSub #-}
  safeNeg :: SomeBV bv -> m (SomeBV bv)
safeNeg = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> m (SomeBV bv))
-> SomeBV bv -> m (SomeBV bv)
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV ((bv n -> SomeBV bv) -> m (bv n) -> m (SomeBV bv)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (m (bv n) -> m (SomeBV bv))
-> (bv n -> m (bv n)) -> bv n -> m (SomeBV bv)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e -> Either BitwidthMismatch e) -> ExceptT e m (bv n) -> m (bv n)
forall e' (m :: * -> *) a e.
(MonadError e' m, TryMerge m, Mergeable a, Mergeable e,
 Mergeable e) =>
(e -> e') -> ExceptT e m a -> m a
mrgModifyError e -> Either BitwidthMismatch e
forall a b. b -> Either a b
Right (ExceptT e m (bv n) -> m (bv n))
-> (bv n -> ExceptT e m (bv n)) -> bv n -> m (bv n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a (m :: * -> *). SafeLinearArith e a m => a -> m a
safeNeg @e)
  {-# INLINE safeNeg #-}

instance
  (forall n. (KnownNat n, 1 <= n) => SymShift (bv n)) =>
  SymShift (SomeBV bv)
  where
  symShift :: SomeBV bv -> SomeBV bv -> SomeBV bv
symShift = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. SymShift a => a -> a -> a
symShift
  {-# INLINE symShift #-}
  symShiftNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv
symShiftNegated = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. SymShift a => a -> a -> a
symShiftNegated
  {-# INLINE symShiftNegated #-}

instance
  (forall n. (KnownNat n, 1 <= n) => SymRotate (bv n)) =>
  SymRotate (SomeBV bv)
  where
  symRotate :: SomeBV bv -> SomeBV bv -> SomeBV bv
symRotate = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. SymRotate a => a -> a -> a
symRotate
  {-# INLINE symRotate #-}
  symRotateNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv
symRotateNegated = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. SymRotate a => a -> a -> a
symRotateNegated
  {-# INLINE symRotateNegated #-}

instance
  ( forall n.
    (KnownNat n, 1 <= n) =>
    SafeSymShift e (bv n) (ExceptT e m),
    MonadError (Either BitwidthMismatch e) m,
    TryMerge m,
    Mergeable e
  ) =>
  SafeSymShift (Either BitwidthMismatch e) (SomeBV bv) m
  where
  safeSymShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymShiftL = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymShiftL @e)
  {-# INLINE safeSymShiftL #-}
  safeSymShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymShiftR = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymShiftR @e)
  {-# INLINE safeSymShiftR #-}
  safeSymStrictShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymStrictShiftL = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymStrictShiftL @e)
  {-# INLINE safeSymStrictShiftL #-}
  safeSymStrictShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymStrictShiftR = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymStrictShiftR @e)
  {-# INLINE safeSymStrictShiftR #-}

instance
  ( forall n.
    (KnownNat n, 1 <= n) =>
    SafeSymRotate e (bv n) (ExceptT e m),
    MonadError (Either BitwidthMismatch e) m,
    TryMerge m,
    Mergeable e
  ) =>
  SafeSymRotate (Either BitwidthMismatch e) (SomeBV bv) m
  where
  safeSymRotateL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymRotateL = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymRotate e a m => a -> a -> m a
safeSymRotateL @e)
  {-# INLINE safeSymRotateL #-}
  safeSymRotateR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymRotateR = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymRotate e a m => a -> a -> m a
safeSymRotateR @e)
  {-# INLINE safeSymRotateR #-}

instance
  (forall n. (KnownNat n, 1 <= n) => ITEOp (bv n)) =>
  ITEOp (SomeBV bv)
  where
  symIte :: SymBool -> SomeBV bv -> SomeBV bv -> SomeBV bv
symIte SymBool
cond = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 (SymBool -> bv n -> bv n -> bv n
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
cond)

instance
  (forall n. (KnownNat n, 1 <= n) => AllSyms (bv n)) =>
  AllSyms (SomeBV bv)
  where
  allSyms :: SomeBV bv -> [SomeSym]
allSyms = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> [SomeSym])
-> SomeBV bv -> [SomeSym]
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> [SomeSym]
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym]
allSyms
  {-# INLINE allSyms #-}
  allSymsS :: SomeBV bv -> [SomeSym] -> [SomeSym]
allSymsS = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> [SomeSym] -> [SomeSym])
-> SomeBV bv -> [SomeSym] -> [SomeSym]
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> [SomeSym] -> [SomeSym]
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS
  {-# INLINE allSymsS #-}

-- Synonyms

-- | Type synonym for 'SomeBV' with concrete signed bitvectors.
type SomeIntN = SomeBV IntN

-- | Pattern synonym for 'SomeBV' with concrete signed bitvectors.
pattern SomeIntN :: () => (KnownNat n, 1 <= n) => IntN n -> SomeIntN
pattern $mSomeIntN :: forall {r}.
SomeIntN
-> (forall {n :: Nat}. (KnownNat n, 1 <= n) => IntN n -> r)
-> ((# #) -> r)
-> r
$bSomeIntN :: forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN a = SomeBV a

-- | Type synonym for 'SomeBV' with concrete unsigned bitvectors.
type SomeWordN = SomeBV WordN

-- | Pattern synonym for 'SomeBV' with concrete unsigned bitvectors.
pattern SomeWordN :: () => (KnownNat n, 1 <= n) => WordN n -> SomeWordN
pattern $mSomeWordN :: forall {r}.
SomeWordN
-> (forall {n :: Nat}. (KnownNat n, 1 <= n) => WordN n -> r)
-> ((# #) -> r)
-> r
$bSomeWordN :: forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN a = SomeBV a

-- | Type synonym for 'SomeBV' with symbolic signed bitvectors.
type SomeSymIntN = SomeBV SymIntN

-- | Pattern synonym for 'SomeBV' with symbolic signed bitvectors.
pattern SomeSymIntN :: () => (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN
pattern $mSomeSymIntN :: forall {r}.
SomeSymIntN
-> (forall {n :: Nat}. (KnownNat n, 1 <= n) => SymIntN n -> r)
-> ((# #) -> r)
-> r
$bSomeSymIntN :: forall (n :: Nat). (KnownNat n, 1 <= n) => SymIntN n -> SomeSymIntN
SomeSymIntN a = SomeBV a

-- | Type synonym for 'SomeBV' with symbolic unsigned bitvectors.
type SomeSymWordN = SomeBV SymWordN

-- | Pattern synonym for 'SomeBV' with symbolic unsigned bitvectors.
pattern SomeSymWordN :: () => (KnownNat n, 1 <= n) => SymWordN n -> SomeSymWordN
pattern $mSomeSymWordN :: forall {r}.
SomeSymWordN
-> (forall {n :: Nat}. (KnownNat n, 1 <= n) => SymWordN n -> r)
-> ((# #) -> r)
-> r
$bSomeSymWordN :: forall (n :: Nat).
(KnownNat n, 1 <= n) =>
SymWordN n -> SomeSymWordN
SomeSymWordN a = SomeBV a

-- Construction

-- | Construct a 'SomeBV' with a given run-time bitwidth and a polymorphic
-- value for the underlying bitvector.
unsafeSomeBV ::
  forall bv.
  Int ->
  (forall proxy n. (KnownNat n, 1 <= n) => proxy n -> bv n) ->
  SomeBV bv
unsafeSomeBV :: forall (bv :: Nat -> *).
Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
unsafeSomeBV Int
n forall (proxy :: Nat -> *) (n :: Nat).
(KnownNat n, 1 <= n) =>
proxy n -> bv n
i
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> SomeBV bv
forall a. HasCallStack => String -> a
error String
"unsafeBV: trying to create a bitvector of non-positive size"
  | Bool
otherwise = case Nat -> SomePositiveNatRepr
mkPositiveNatRepr (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) of
      SomePositiveNatRepr (NatRepr n
_ :: NatRepr x) -> bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (Proxy n -> bv n
forall (proxy :: Nat -> *) (n :: Nat).
(KnownNat n, 1 <= n) =>
proxy n -> bv n
i (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x))

-- | Construct a symbolic 'SomeBV' with a given concrete 'SomeBV'. Similar to
-- 'con' but for 'SomeBV'.
--
-- >>> a = bv 8 0x12 :: SomeIntN
-- >>> conBV a :: SomeSymIntN
-- 0x12
conBV ::
  forall cbv bv.
  ( forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n),
    Solvable (cbv 1) (bv 1)
  ) =>
  SomeBV cbv ->
  SomeBV bv
conBV :: forall (cbv :: Nat -> *) (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 Solvable (cbv n) (bv n),
 Solvable (cbv 1) (bv 1)) =>
SomeBV cbv -> SomeBV bv
conBV (SomeBV (cbv n
v :: cbv n)) = bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv n -> SomeBV bv) -> bv n -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ forall c t. Solvable c t => c -> t
con @(cbv n) @(bv n) cbv n
v

-- | View pattern for symbolic 'SomeBV' to see if it contains a concrete value
-- and extract it. Similar to 'conView' but for 'SomeBV'.
--
-- >>> conBVView (bv 8 0x12 :: SomeSymIntN)
-- Just 0x12
-- >>> conBVView (ssymBV 4 "a" :: SomeSymIntN)
-- Nothing
conBVView ::
  forall cbv bv.
  ( forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n),
    Solvable (cbv 1) (bv 1)
  ) =>
  SomeBV bv ->
  Maybe (SomeBV cbv)
conBVView :: forall (cbv :: Nat -> *) (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 Solvable (cbv n) (bv n),
 Solvable (cbv 1) (bv 1)) =>
SomeBV bv -> Maybe (SomeBV cbv)
conBVView (SomeBV (bv n
bv :: bv n)) = case forall c t. Solvable c t => t -> Maybe c
conView @(cbv n) bv n
bv of
  Just cbv n
c -> SomeBV cbv -> Maybe (SomeBV cbv)
forall a. a -> Maybe a
Just (SomeBV cbv -> Maybe (SomeBV cbv))
-> SomeBV cbv -> Maybe (SomeBV cbv)
forall a b. (a -> b) -> a -> b
$ cbv n -> SomeBV cbv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV cbv n
c
  Maybe (cbv n)
Nothing -> Maybe (SomeBV cbv)
forall a. Maybe a
Nothing

-- | Pattern synonym for symbolic 'SomeBV' to see if it contains a concrete
-- value and extract it. Similar to 'Con' but for 'SomeBV'.
--
-- >>> case (bv 8 0x12 :: SomeSymIntN) of { ConBV c -> c; _ -> error "impossible" }
-- 0x12
pattern ConBV ::
  forall cbv bv.
  ( forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n),
    Solvable (cbv 1) (bv 1)
  ) =>
  SomeBV cbv ->
  SomeBV bv
pattern $mConBV :: forall {r} {cbv :: Nat -> *} {bv :: Nat -> *}.
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 Solvable (cbv n) (bv n),
 Solvable (cbv 1) (bv 1)) =>
SomeBV bv -> (SomeBV cbv -> r) -> ((# #) -> r) -> r
$bConBV :: forall (cbv :: Nat -> *) (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 Solvable (cbv n) (bv n),
 Solvable (cbv 1) (bv 1)) =>
SomeBV cbv -> SomeBV bv
ConBV c <- (conBVView -> Just c)
  where
    ConBV SomeBV cbv
c = SomeBV cbv -> SomeBV bv
forall (cbv :: Nat -> *) (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 Solvable (cbv n) (bv n),
 Solvable (cbv 1) (bv 1)) =>
SomeBV cbv -> SomeBV bv
conBV SomeBV cbv
c

-- | Construct a symbolic 'SomeBV' with a given run-time bitwidth and a symbol.
-- Similar to 'sym' but for 'SomeBV'.
--
-- >>> symBV 8 "a" :: SomeSymIntN
-- a
symBV ::
  forall cbv bv.
  ( forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n),
    Solvable (cbv 1) (bv 1)
  ) =>
  Int ->
  Symbol ->
  SomeBV bv
symBV :: forall (cbv :: Nat -> *) (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 Solvable (cbv n) (bv n),
 Solvable (cbv 1) (bv 1)) =>
Int -> Symbol -> SomeBV bv
symBV Int
n Symbol
s = Int
-> (forall {proxy :: Nat -> *} {n :: Nat}.
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
forall (bv :: Nat -> *).
Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
unsafeSomeBV Int
n ((forall {proxy :: Nat -> *} {n :: Nat}.
  (KnownNat n, 1 <= n) =>
  proxy n -> bv n)
 -> SomeBV bv)
-> (forall {proxy :: Nat -> *} {n :: Nat}.
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
forall a b. (a -> b) -> a -> b
$ \(proxy n
_ :: proxy n) -> forall c t. Solvable c t => Symbol -> t
sym @(cbv n) Symbol
s

-- | Construct a symbolic 'SomeBV' with a given run-time bitwidth and an
-- identifier. Similar to 'ssym' but for 'SomeBV'.
--
-- >>> ssymBV 8 "a" :: SomeSymIntN
-- a
ssymBV ::
  forall cbv bv.
  ( forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n),
    Solvable (cbv 1) (bv 1)
  ) =>
  Int ->
  Identifier ->
  SomeBV bv
ssymBV :: forall (cbv :: Nat -> *) (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 Solvable (cbv n) (bv n),
 Solvable (cbv 1) (bv 1)) =>
Int -> Identifier -> SomeBV bv
ssymBV Int
n Identifier
s = Int
-> (forall {proxy :: Nat -> *} {n :: Nat}.
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
forall (bv :: Nat -> *).
Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
unsafeSomeBV Int
n ((forall {proxy :: Nat -> *} {n :: Nat}.
  (KnownNat n, 1 <= n) =>
  proxy n -> bv n)
 -> SomeBV bv)
-> (forall {proxy :: Nat -> *} {n :: Nat}.
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
forall a b. (a -> b) -> a -> b
$ \(proxy n
_ :: proxy n) -> forall c t. Solvable c t => Identifier -> t
ssym @(cbv n) Identifier
s

-- | Construct a symbolic 'SomeBV' with a given run-time bitwidth, an identifier
-- and an index. Similar to 'isym' but for 'SomeBV'.
--
-- >>> isymBV 8 "a" 1 :: SomeSymIntN
-- a@1
isymBV ::
  forall cbv bv.
  ( forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n),
    Solvable (cbv 1) (bv 1)
  ) =>
  Int ->
  Identifier ->
  Int ->
  SomeBV bv
isymBV :: forall (cbv :: Nat -> *) (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 Solvable (cbv n) (bv n),
 Solvable (cbv 1) (bv 1)) =>
Int -> Identifier -> Int -> SomeBV bv
isymBV Int
n Identifier
s Int
i = Int
-> (forall {proxy :: Nat -> *} {n :: Nat}.
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
forall (bv :: Nat -> *).
Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
unsafeSomeBV Int
n ((forall {proxy :: Nat -> *} {n :: Nat}.
  (KnownNat n, 1 <= n) =>
  proxy n -> bv n)
 -> SomeBV bv)
-> (forall {proxy :: Nat -> *} {n :: Nat}.
    (KnownNat n, 1 <= n) =>
    proxy n -> bv n)
-> SomeBV bv
forall a b. (a -> b) -> a -> b
$ \(proxy n
_ :: proxy n) -> forall c t. Solvable c t => Identifier -> Int -> t
isym @(cbv n) Identifier
s Int
i

-- | Generate an arbitrary 'SomeBV' with a given run-time bitwidth.
arbitraryBV ::
  forall bv.
  (forall n. (KnownNat n, 1 <= n) => Arbitrary (bv n)) =>
  Int ->
  Gen (SomeBV bv)
arbitraryBV :: forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Arbitrary (bv n)) =>
Int -> Gen (SomeBV bv)
arbitraryBV Int
n
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 =
      String -> Gen (SomeBV bv)
forall a. HasCallStack => String -> a
error String
"arbitraryBV: trying to create a bitvector of non-positive size"
  | Bool
otherwise = case Nat -> SomePositiveNatRepr
mkPositiveNatRepr (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) of
      SomePositiveNatRepr (NatRepr n
_ :: NatRepr x) -> do
        bv n
v <- Gen (bv n)
forall a. Arbitrary a => Gen a
arbitrary :: Gen (bv x)
        SomeBV bv -> Gen (SomeBV bv)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeBV bv -> Gen (SomeBV bv)) -> SomeBV bv -> Gen (SomeBV bv)
forall a b. (a -> b) -> a -> b
$ bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n
v

-- Helpers

-- | Lift a unary operation on sized bitvectors that returns anything to
-- 'SomeBV'.
unarySomeBV :: forall bv r. (forall n. (KnownNat n, 1 <= n) => bv n -> r) -> SomeBV bv -> r
unarySomeBV :: forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r
f (SomeBV bv n
bv) = bv n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r
f bv n
bv
{-# INLINE unarySomeBV #-}

-- | Lift a unary operation on sized bitvectors that returns a bitvector to
-- 'SomeBV'. The result will also be wrapped with 'SomeBV'.
unarySomeBVR1 ::
  (forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 :: forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
f = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> SomeBV bv)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV (bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv n -> SomeBV bv) -> (bv n -> bv n) -> bv n -> SomeBV bv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
f)
{-# INLINE unarySomeBVR1 #-}

-- | Lift a binary operation on sized bitvectors that returns anything to
-- 'SomeBV'. Crash if the bitwidths do not match.
binSomeBV ::
  (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) ->
  SomeBV bv ->
  SomeBV bv ->
  r
binSomeBV :: forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r
f (SomeBV (bv n
l :: bv l)) (SomeBV (bv n
r :: bv r)) =
  case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> bv n -> bv n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r
f bv n
l bv n
bv n
r
    Maybe (n :~: n)
Nothing -> BitwidthMismatch -> r
forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeBV #-}

-- | Lift a binary operation on sized bitvectors that returns a bitvector to
-- 'SomeBV'. The result will also be wrapped with 'SomeBV'. Crash if the
-- bitwidths do not match.
binSomeBVR1 ::
  (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) ->
  SomeBV bv ->
  SomeBV bv ->
  SomeBV bv
binSomeBVR1 :: forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
f = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SomeBV bv)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV (\bv n
a bv n
b -> bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv n -> SomeBV bv) -> bv n -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
f bv n
a bv n
b)
{-# INLINE binSomeBVR1 #-}

-- | Lift a binary operation on sized bitvectors that returns two bitvectors to
-- 'SomeBV'. The results will also be wrapped with 'SomeBV'. Crash if the
-- bitwidths do not match.
binSomeBVR2 ::
  (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) ->
  SomeBV bv ->
  SomeBV bv ->
  (SomeBV bv, SomeBV bv)
binSomeBVR2 :: forall (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
binSomeBVR2 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n)
f = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> (SomeBV bv, SomeBV bv))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV (\bv n
a bv n
b -> let (bv n
x, bv n
y) = bv n -> bv n -> (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n)
f bv n
a bv n
b in (bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n
x, bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n
y))
{-# INLINE binSomeBVR2 #-}

-- | Lift a binary operation on sized bitvectors that returns anything wrapped
-- with 'ExceptT' to 'SomeBV'. If the bitwidths do not match, throw an
-- `BitwidthMismatch` error to the monadic context.
binSomeBVSafe ::
  ( MonadError (Either BitwidthMismatch e) m,
    TryMerge m,
    Mergeable e,
    Mergeable r
  ) =>
  (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) ->
  SomeBV bv ->
  SomeBV bv ->
  m r
binSomeBVSafe :: forall e (m :: * -> *) r (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 Mergeable r) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m r)
-> SomeBV bv -> SomeBV bv -> m r
binSomeBVSafe forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m r
f (SomeBV (bv n
l :: bv l)) (SomeBV (bv n
r :: bv r)) =
  case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> (e -> Either BitwidthMismatch e) -> ExceptT e m r -> m r
forall e' (m :: * -> *) a e.
(MonadError e' m, TryMerge m, Mergeable a, Mergeable e,
 Mergeable e) =>
(e -> e') -> ExceptT e m a -> m a
mrgModifyError e -> Either BitwidthMismatch e
forall a b. b -> Either a b
Right (ExceptT e m r -> m r) -> ExceptT e m r -> m r
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> ExceptT e m r
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m r
f bv n
l bv n
bv n
r
    Maybe (n :~: n)
Nothing -> Either BitwidthMismatch e -> m r
forall e (m :: * -> *) a.
(MonadError e m, TryMerge m, Mergeable a) =>
e -> m a
mrgThrowError (Either BitwidthMismatch e -> m r)
-> Either BitwidthMismatch e -> m r
forall a b. (a -> b) -> a -> b
$ BitwidthMismatch -> Either BitwidthMismatch e
forall a b. a -> Either a b
Left BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeBVSafe #-}

-- | Lift a binary operation on sized bitvectors that returns a bitvector
-- wrapped with 'ExceptT' to 'SomeBV'. The result will also be wrapped with
-- 'SomeBV'.
--
-- If the bitwidths do not match, throw an `BitwidthMismatch` error to the
-- monadic context.
binSomeBVSafeR1 ::
  ( MonadError (Either BitwidthMismatch e) m,
    TryMerge m,
    Mergeable e,
    forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)
  ) =>
  (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) ->
  SomeBV bv ->
  SomeBV bv ->
  m (SomeBV bv)
binSomeBVSafeR1 :: forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n)
f = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (SomeBV bv))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) r (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 Mergeable r) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m r)
-> SomeBV bv -> SomeBV bv -> m r
binSomeBVSafe (\bv n
l bv n
r -> (bv n -> SomeBV bv)
-> ExceptT e m (bv n) -> ExceptT e m (SomeBV bv)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (ExceptT e m (bv n) -> ExceptT e m (SomeBV bv))
-> ExceptT e m (bv n) -> ExceptT e m (SomeBV bv)
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> ExceptT e m (bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n)
f bv n
l bv n
r)
{-# INLINE binSomeBVSafeR1 #-}

-- | Lift a binary operation on sized bitvectors that returns two bitvectors
-- wrapped with 'ExceptT' to 'SomeBV'. The results will also be wrapped with
-- 'SomeBV'.
--
-- If the bitwidths do not match, throw an `BitwidthMismatch` error to the
-- monadic context.
binSomeBVSafeR2 ::
  ( MonadError (Either BitwidthMismatch e) m,
    TryMerge m,
    Mergeable e,
    forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)
  ) =>
  ( forall n.
    (KnownNat n, 1 <= n) =>
    bv n ->
    bv n ->
    ExceptT e m (bv n, bv n)
  ) ->
  SomeBV bv ->
  SomeBV bv ->
  m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2 :: forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n, bv n)
f =
  (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (SomeBV bv, SomeBV bv))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
forall e (m :: * -> *) r (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
 Mergeable r) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m r)
-> SomeBV bv -> SomeBV bv -> m r
binSomeBVSafe (\bv n
l bv n
r -> ((bv n, bv n) -> (SomeBV bv, SomeBV bv))
-> ExceptT e m (bv n, bv n) -> ExceptT e m (SomeBV bv, SomeBV bv)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap ((bv n -> SomeBV bv)
-> (bv n -> SomeBV bv) -> (bv n, bv n) -> (SomeBV bv, SomeBV bv)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV) (ExceptT e m (bv n, bv n) -> ExceptT e m (SomeBV bv, SomeBV bv))
-> ExceptT e m (bv n, bv n) -> ExceptT e m (SomeBV bv, SomeBV bv)
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> ExceptT e m (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n, bv n)
f bv n
l bv n
r)
{-# INLINE binSomeBVSafeR2 #-}