{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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 (..),
    SomeBVException (..),

    -- * 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 (Exception, throw)
import Control.Monad.Except (ExceptT, MonadError (throwError), runExceptT)
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 (catMaybes, fromJust, isJust)
import qualified Data.Text as T
import Data.Type.Equality (type (:~:) (Refl))
import GHC.Exception (Exception (displayException))
import GHC.Generics (Generic)
import GHC.TypeNats
  ( KnownNat,
    Nat,
    natVal,
    sameNat,
    type (+),
    type (<=),
  )
import Generics.Deriving (Default (Default))
import Grisette.Internal.Core.Control.Monad.Union (Union)
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.EvalSym
  ( EvalSym (evalSym),
  )
import Grisette.Internal.Core.Data.Class.ExtractSym
  ( ExtractSym (extractSymMaybe),
  )
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.PPrint
  ( PPrint (pformat),
  )
import Grisette.Internal.Core.Data.Class.SafeDiv
  ( DivOr (divModOr, divOr, modOr, quotOr, quotRemOr, remOr),
    SafeDiv (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.SubstSym
  ( SubstSym (substSym),
  )
import Grisette.Internal.Core.Data.Class.SymEq
  ( SymEq (symDistinct, (./=), (.==)),
  )
import Grisette.Internal.Core.Data.Class.SymOrd
  ( SymOrd (symCompare, (.<), (.<=), (.>), (.>=)),
  )
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, tryMerge)
import Grisette.Internal.Core.Data.Symbol (Identifier, Symbol)
import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSyms, allSymsS))
import Grisette.Internal.SymPrim.BV
  ( 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.Data.Functor (mrgFmap)
import Language.Haskell.TH.Syntax (Lift (liftTyped))
import Test.QuickCheck (Arbitrary (arbitrary), Gen)
import Unsafe.Coerce (unsafeCoerce)

-- | An exception that would be thrown when operations are performed on
-- incompatible bit widths.
data SomeBVException = BitwidthMismatch | UndeterminedBitwidth T.Text
  deriving (Int -> SomeBVException -> ShowS
[SomeBVException] -> ShowS
SomeBVException -> String
(Int -> SomeBVException -> ShowS)
-> (SomeBVException -> String)
-> ([SomeBVException] -> ShowS)
-> Show SomeBVException
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SomeBVException -> ShowS
showsPrec :: Int -> SomeBVException -> ShowS
$cshow :: SomeBVException -> String
show :: SomeBVException -> String
$cshowList :: [SomeBVException] -> ShowS
showList :: [SomeBVException] -> ShowS
Show, SomeBVException -> SomeBVException -> Bool
(SomeBVException -> SomeBVException -> Bool)
-> (SomeBVException -> SomeBVException -> Bool)
-> Eq SomeBVException
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SomeBVException -> SomeBVException -> Bool
== :: SomeBVException -> SomeBVException -> Bool
$c/= :: SomeBVException -> SomeBVException -> Bool
/= :: SomeBVException -> SomeBVException -> Bool
Eq, Eq SomeBVException
Eq SomeBVException =>
(SomeBVException -> SomeBVException -> Ordering)
-> (SomeBVException -> SomeBVException -> Bool)
-> (SomeBVException -> SomeBVException -> Bool)
-> (SomeBVException -> SomeBVException -> Bool)
-> (SomeBVException -> SomeBVException -> Bool)
-> (SomeBVException -> SomeBVException -> SomeBVException)
-> (SomeBVException -> SomeBVException -> SomeBVException)
-> Ord SomeBVException
SomeBVException -> SomeBVException -> Bool
SomeBVException -> SomeBVException -> Ordering
SomeBVException -> SomeBVException -> SomeBVException
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: SomeBVException -> SomeBVException -> Ordering
compare :: SomeBVException -> SomeBVException -> Ordering
$c< :: SomeBVException -> SomeBVException -> Bool
< :: SomeBVException -> SomeBVException -> Bool
$c<= :: SomeBVException -> SomeBVException -> Bool
<= :: SomeBVException -> SomeBVException -> Bool
$c> :: SomeBVException -> SomeBVException -> Bool
> :: SomeBVException -> SomeBVException -> Bool
$c>= :: SomeBVException -> SomeBVException -> Bool
>= :: SomeBVException -> SomeBVException -> Bool
$cmax :: SomeBVException -> SomeBVException -> SomeBVException
max :: SomeBVException -> SomeBVException -> SomeBVException
$cmin :: SomeBVException -> SomeBVException -> SomeBVException
min :: SomeBVException -> SomeBVException -> SomeBVException
Ord, (forall x. SomeBVException -> Rep SomeBVException x)
-> (forall x. Rep SomeBVException x -> SomeBVException)
-> Generic SomeBVException
forall x. Rep SomeBVException x -> SomeBVException
forall x. SomeBVException -> Rep SomeBVException x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. SomeBVException -> Rep SomeBVException x
from :: forall x. SomeBVException -> Rep SomeBVException x
$cto :: forall x. Rep SomeBVException x -> SomeBVException
to :: forall x. Rep SomeBVException x -> SomeBVException
Generic)
  deriving anyclass (Eq SomeBVException
Eq SomeBVException =>
(Int -> SomeBVException -> Int)
-> (SomeBVException -> Int) -> Hashable SomeBVException
Int -> SomeBVException -> Int
SomeBVException -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> SomeBVException -> Int
hashWithSalt :: Int -> SomeBVException -> Int
$chash :: SomeBVException -> Int
hash :: SomeBVException -> Int
Hashable, SomeBVException -> ()
(SomeBVException -> ()) -> NFData SomeBVException
forall a. (a -> ()) -> NFData a
$crnf :: SomeBVException -> ()
rnf :: SomeBVException -> ()
NFData)
  deriving
    ( MergingStrategy SomeBVException
MergingStrategy SomeBVException -> Mergeable SomeBVException
forall a. MergingStrategy a -> Mergeable a
$crootStrategy :: MergingStrategy SomeBVException
rootStrategy :: MergingStrategy SomeBVException
Mergeable,
      SomeBVException -> AnySymbolSet
(SomeBVException -> AnySymbolSet)
-> (forall (knd :: SymbolKind).
    IsSymbolKind knd =>
    SomeBVException -> Maybe (SymbolSet knd))
-> ExtractSym SomeBVException
forall a.
(a -> AnySymbolSet)
-> (forall (knd :: SymbolKind).
    IsSymbolKind knd =>
    a -> Maybe (SymbolSet knd))
-> ExtractSym a
forall (knd :: SymbolKind).
IsSymbolKind knd =>
SomeBVException -> Maybe (SymbolSet knd)
$cextractSym :: SomeBVException -> AnySymbolSet
extractSym :: SomeBVException -> AnySymbolSet
$cextractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
SomeBVException -> Maybe (SymbolSet knd)
extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
SomeBVException -> Maybe (SymbolSet knd)
ExtractSym,
      (forall ann. SomeBVException -> Doc ann)
-> (forall ann. Int -> SomeBVException -> Doc ann)
-> (forall ann. [SomeBVException] -> Doc ann)
-> PPrint SomeBVException
forall ann. Int -> SomeBVException -> Doc ann
forall ann. [SomeBVException] -> Doc ann
forall ann. SomeBVException -> Doc ann
forall a.
(forall ann. a -> Doc ann)
-> (forall ann. Int -> a -> Doc ann)
-> (forall ann. [a] -> Doc ann)
-> PPrint a
$cpformat :: forall ann. SomeBVException -> Doc ann
pformat :: forall ann. SomeBVException -> Doc ann
$cpformatPrec :: forall ann. Int -> SomeBVException -> Doc ann
pformatPrec :: forall ann. Int -> SomeBVException -> Doc ann
$cpformatList :: forall ann. [SomeBVException] -> Doc ann
pformatList :: forall ann. [SomeBVException] -> Doc ann
PPrint,
      (forall cb sb (knd :: SymbolKind).
 (LinkedRep cb sb, IsSymbolKind knd) =>
 TypedSymbol knd cb -> sb -> SomeBVException -> SomeBVException)
-> SubstSym SomeBVException
forall a.
(forall cb sb (knd :: SymbolKind).
 (LinkedRep cb sb, IsSymbolKind knd) =>
 TypedSymbol knd cb -> sb -> a -> a)
-> SubstSym a
forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> SomeBVException -> SomeBVException
$csubstSym :: forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> SomeBVException -> SomeBVException
substSym :: forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> SomeBVException -> SomeBVException
SubstSym,
      Bool -> Model -> SomeBVException -> SomeBVException
(Bool -> Model -> SomeBVException -> SomeBVException)
-> EvalSym SomeBVException
forall a. (Bool -> Model -> a -> a) -> EvalSym a
$cevalSym :: Bool -> Model -> SomeBVException -> SomeBVException
evalSym :: Bool -> Model -> SomeBVException -> SomeBVException
EvalSym,
      [SomeBVException] -> SymBool
SomeBVException -> SomeBVException -> SymBool
(SomeBVException -> SomeBVException -> SymBool)
-> (SomeBVException -> SomeBVException -> SymBool)
-> ([SomeBVException] -> SymBool)
-> SymEq SomeBVException
forall a.
(a -> a -> SymBool)
-> (a -> a -> SymBool) -> ([a] -> SymBool) -> SymEq a
$c.== :: SomeBVException -> SomeBVException -> SymBool
.== :: SomeBVException -> SomeBVException -> SymBool
$c./= :: SomeBVException -> SomeBVException -> SymBool
./= :: SomeBVException -> SomeBVException -> SymBool
$csymDistinct :: [SomeBVException] -> SymBool
symDistinct :: [SomeBVException] -> SymBool
SymEq,
      SymEq SomeBVException
SymEq SomeBVException =>
(SomeBVException -> SomeBVException -> SymBool)
-> (SomeBVException -> SomeBVException -> SymBool)
-> (SomeBVException -> SomeBVException -> SymBool)
-> (SomeBVException -> SomeBVException -> SymBool)
-> (SomeBVException -> SomeBVException -> Union Ordering)
-> SymOrd SomeBVException
SomeBVException -> SomeBVException -> SymBool
SomeBVException -> SomeBVException -> Union Ordering
forall a.
SymEq a =>
(a -> a -> SymBool)
-> (a -> a -> SymBool)
-> (a -> a -> SymBool)
-> (a -> a -> SymBool)
-> (a -> a -> Union Ordering)
-> SymOrd a
$c.< :: SomeBVException -> SomeBVException -> SymBool
.< :: SomeBVException -> SomeBVException -> SymBool
$c.<= :: SomeBVException -> SomeBVException -> SymBool
.<= :: SomeBVException -> SomeBVException -> SymBool
$c.> :: SomeBVException -> SomeBVException -> SymBool
.> :: SomeBVException -> SomeBVException -> SymBool
$c.>= :: SomeBVException -> SomeBVException -> SymBool
.>= :: SomeBVException -> SomeBVException -> SymBool
$csymCompare :: SomeBVException -> SomeBVException -> Union Ordering
symCompare :: SomeBVException -> SomeBVException -> Union Ordering
SymOrd,
      ToCon SomeBVException,
      ToSym SomeBVException
    )
    via (Default (SomeBVException))

instance Exception SomeBVException where
  displayException :: SomeBVException -> String
displayException SomeBVException
BitwidthMismatch = String
"Bit width does not match"
  displayException (UndeterminedBitwidth Text
msg) =
    String
"Cannot determine bit-width for literals: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
msg

assignBitWidthList ::
  forall bv.
  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>
  T.Text ->
  [SomeBV bv] ->
  Either SomeBVException [SomeBV bv]
assignBitWidthList :: forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
Text -> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
assignBitWidthList Text
msg [SomeBV bv]
bvs = case [Int]
allNonMaybeBitWidth of
  [] -> SomeBVException -> Either SomeBVException [SomeBV bv]
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException [SomeBV bv])
-> SomeBVException -> Either SomeBVException [SomeBV bv]
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
msg
  (Int
x : [Int]
xs) ->
    if (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
x) [Int]
xs
      then case [SomeBV bv]
allHasBitWidth of
        (SomeBV (bv n
i :: bv i) : [SomeBV bv]
_) -> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
forall a b. b -> Either a b
Right ([SomeBV bv] -> Either SomeBVException [SomeBV bv])
-> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
forall a b. (a -> b) -> a -> b
$ (SomeBV bv -> SomeBV bv) -> [SomeBV bv] -> [SomeBV bv]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (bv n -> SomeBV bv -> SomeBV bv
forall (i :: Nat).
(KnownNat i, 1 <= i) =>
bv i -> SomeBV bv -> SomeBV bv
assignSingleBitWidth bv n
i) [SomeBV bv]
bvs
        [SomeBV bv]
_ -> String -> Either SomeBVException [SomeBV bv]
forall a. HasCallStack => String -> a
error String
"Should not happen"
      else SomeBVException -> Either SomeBVException [SomeBV bv]
forall a b. a -> Either a b
Left SomeBVException
BitwidthMismatch
  where
    maybeBitWidth :: SomeBV bv -> Maybe Int
    maybeBitWidth :: SomeBV bv -> Maybe Int
maybeBitWidth (SomeBV (bv n
_ :: bv n)) = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ 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)
    maybeBitWidth (SomeBVLit Integer
_) = Maybe Int
forall a. Maybe a
Nothing
    allMaybeBitWidth :: [Maybe Int]
allMaybeBitWidth = (SomeBV bv -> Maybe Int) -> [SomeBV bv] -> [Maybe Int]
forall a b. (a -> b) -> [a] -> [b]
map SomeBV bv -> Maybe Int
maybeBitWidth [SomeBV bv]
bvs
    allNonMaybeBitWidth :: [Int]
allNonMaybeBitWidth = [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Int]
allMaybeBitWidth
    allHasBitWidth :: [SomeBV bv]
allHasBitWidth = (SomeBV bv -> Bool) -> [SomeBV bv] -> [SomeBV bv]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Int -> Bool)
-> (SomeBV bv -> Maybe Int) -> SomeBV bv -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeBV bv -> Maybe Int
maybeBitWidth) [SomeBV bv]
bvs
    assignSingleBitWidth ::
      forall i. (KnownNat i, 1 <= i) => bv i -> SomeBV bv -> SomeBV bv
    assignSingleBitWidth :: forall (i :: Nat).
(KnownNat i, 1 <= i) =>
bv i -> SomeBV bv -> SomeBV bv
assignSingleBitWidth bv i
_ s :: SomeBV bv
s@(SomeBV bv n
_) = SomeBV bv
s
    assignSingleBitWidth bv i
_ (SomeBVLit Integer
i) = bv i -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (Integer -> bv i
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i :: bv i)

class AssignBitWidth a where
  assignBitWidth :: T.Text -> a -> Either SomeBVException a

instance
  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>
  AssignBitWidth (SomeBV bv, SomeBV bv)
  where
  assignBitWidth :: Text
-> (SomeBV bv, SomeBV bv)
-> Either SomeBVException (SomeBV bv, SomeBV bv)
assignBitWidth Text
msg (SomeBV bv
a, SomeBV bv
b) = do
    [SomeBV bv]
l <- Text -> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
Text -> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
assignBitWidthList Text
msg [SomeBV bv
a, SomeBV bv
b]
    case [SomeBV bv]
l of
      [SomeBV bv
a', SomeBV bv
b'] -> (SomeBV bv, SomeBV bv)
-> Either SomeBVException (SomeBV bv, SomeBV bv)
forall a b. b -> Either a b
Right (SomeBV bv
a', SomeBV bv
b')
      [SomeBV bv]
_ -> String -> Either SomeBVException (SomeBV bv, SomeBV bv)
forall a. HasCallStack => String -> a
error String
"Should not happen"

instance
  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>
  AssignBitWidth (SomeBV bv, SomeBV bv, SomeBV bv)
  where
  assignBitWidth :: Text
-> (SomeBV bv, SomeBV bv, SomeBV bv)
-> Either SomeBVException (SomeBV bv, SomeBV bv, SomeBV bv)
assignBitWidth Text
msg (SomeBV bv
a, SomeBV bv
b, SomeBV bv
c) = do
    [SomeBV bv]
l <- Text -> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
Text -> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
assignBitWidthList Text
msg [SomeBV bv
a, SomeBV bv
b, SomeBV bv
c]
    case [SomeBV bv]
l of
      [SomeBV bv
a', SomeBV bv
b', SomeBV bv
c'] -> (SomeBV bv, SomeBV bv, SomeBV bv)
-> Either SomeBVException (SomeBV bv, SomeBV bv, SomeBV bv)
forall a b. b -> Either a b
Right (SomeBV bv
a', SomeBV bv
b', SomeBV bv
c')
      [SomeBV bv]
_ -> String -> Either SomeBVException (SomeBV bv, SomeBV bv, SomeBV bv)
forall a. HasCallStack => String -> a
error String
"Should not happen"

instance
  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>
  AssignBitWidth (SomeBV bv, SomeBV bv, SomeBV bv, SomeBV bv)
  where
  assignBitWidth :: Text
-> (SomeBV bv, SomeBV bv, SomeBV bv, SomeBV bv)
-> Either
     SomeBVException (SomeBV bv, SomeBV bv, SomeBV bv, SomeBV bv)
assignBitWidth Text
msg (SomeBV bv
a, SomeBV bv
b, SomeBV bv
c, SomeBV bv
d) = do
    [SomeBV bv]
l <- Text -> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
Text -> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
assignBitWidthList Text
msg [SomeBV bv
a, SomeBV bv
b, SomeBV bv
c, SomeBV bv
d]
    case [SomeBV bv]
l of
      [SomeBV bv
a', SomeBV bv
b', SomeBV bv
c', SomeBV bv
d'] -> (SomeBV bv, SomeBV bv, SomeBV bv, SomeBV bv)
-> Either
     SomeBVException (SomeBV bv, SomeBV bv, SomeBV bv, SomeBV bv)
forall a b. b -> Either a b
Right (SomeBV bv
a', SomeBV bv
b', SomeBV bv
c', SomeBV bv
d')
      [SomeBV bv]
_ -> String
-> Either
     SomeBVException (SomeBV bv, SomeBV bv, SomeBV bv, SomeBV bv)
forall a. HasCallStack => String -> a
error String
"Should not happen"

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim

-- | Non-indexed bitvectors.
--
-- The creation of t'SomeBV' can be done with the `bv` function with a positive
-- bit width and a value:
--
-- >>> bv 4 0xf :: SomeBV IntN
-- 0xf
--
-- Operations on two t'SomeBV' values require the bitwidths to be the same. So
-- you should check for the bit width (via `finiteBitSize`) before performing
-- operations:
--
-- >>> bv 4 0x3 + bv 4 0x3 :: SomeBV IntN
-- 0x6
-- >>> bv 4 0x3 + bv 8 0x3 :: SomeBV IntN
-- *** Exception: BitwidthMismatch
--
-- One exception is that the equality testing (both concrete and symbolic via
-- 'SymEq') does not require the bitwidths to be the same. Different bitwidths
-- means the values are not equal:
--
-- >>> (bv 4 0x3 :: SomeBV IntN) == (bv 8 0x3)
-- False
--
-- __Note__: t'SomeBV' can be constructed out of integer literals without the
-- bit width provided. Further binary operations will usually require at least
-- one operand has the bit-width, and will use that as the bit-width for the
-- result.
--
-- For example:
--
-- 3 :: SomeBV IntN
-- bvlit(3)
-- >>> bv 4 0x1 + 3 :: SomeBV IntN
-- 0x4
-- >>> 3 * bv 4 0x1  :: SomeBV IntN
-- 0x3
-- >>> 3 * 3 :: SomeBV IntN
-- *** Exception: UndeterminedBitwidth "(*)"
--
-- Some operations allows the literals to be used without the bit-width, such as
-- '(+)', '(-)', 'negate', 'toUnsigned', 'toSigned', '.&.', '.|.', 'xor',
-- 'complement', 'setBit', 'clearBit', 'complementBit', 'shiftL', and
-- 'unsafeShiftL'.
--
-- >>> 3 + 3 :: SomeBV IntN
-- bvlit(6)
data SomeBV bv where
  SomeBV :: (KnownNat n, 1 <= n) => bv n -> SomeBV bv
  SomeBVLit :: Integer -> SomeBV bv

instance
  ( forall n. (KnownNat n, 1 <= n) => Hashable (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (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
  hashWithSalt Int
s (SomeBVLit Integer
i) = Int
s Int -> Integer -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Integer
i
  {-# 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||]
  liftTyped (SomeBVLit Integer
i) = [||Integer -> SomeBV bv
forall (bv :: Nat -> *). Integer -> SomeBV bv
SomeBVLit Integer
i||]
  {-# INLINE liftTyped #-}

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
  show (SomeBVLit Integer
i) = String
"bvlit(" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Integer -> String
forall a. Show a => a -> String
show Integer
i String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")"
  {-# 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
  rnf (SomeBVLit Integer
i) = Integer -> ()
forall a. NFData a => a -> ()
rnf Integer
i
  {-# INLINE rnf #-}

instance
  ( forall n. (KnownNat n, 1 <= n) => Eq (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  Eq (SomeBV bv)
  where
  SomeBV (bv n
l :: bv l) == :: SomeBV bv -> SomeBV bv -> Bool
== 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
l bv n -> bv n -> Bool
forall a. Eq a => a -> a -> Bool
== bv n
bv n
r
      Maybe (n :~: n)
Nothing -> Bool
False
  SomeBV (bv n
l :: bv l) == SomeBVLit Integer
r = bv n
l bv n -> bv n -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> bv n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
r
  SomeBVLit Integer
l == SomeBV bv n
r = Integer -> bv n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
l bv n -> bv n -> Bool
forall a. Eq a => a -> a -> Bool
== bv n
r
  SomeBVLit Integer
_ == SomeBVLit Integer
_ = SomeBVException -> Bool
forall a e. Exception e => e -> a
throw (SomeBVException -> Bool) -> SomeBVException -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"=="
  {-# INLINE (==) #-}
  SomeBV (bv n
l :: bv l) /= :: SomeBV bv -> SomeBV bv -> Bool
/= 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
l bv n -> bv n -> Bool
forall a. Eq a => a -> a -> Bool
/= bv n
bv n
r
      Maybe (n :~: n)
Nothing -> Bool
True
  SomeBV (bv n
l :: bv l) /= SomeBVLit Integer
r = bv n
l bv n -> bv n -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer -> bv n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
r
  SomeBVLit Integer
l /= SomeBV bv n
r = Integer -> bv n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
l bv n -> bv n -> Bool
forall a. Eq a => a -> a -> Bool
/= bv n
r
  SomeBVLit Integer
_ /= SomeBVLit Integer
_ = SomeBVException -> Bool
forall a e. Exception e => e -> a
throw (SomeBVException -> Bool) -> SomeBVException -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"/="
  {-# INLINE (/=) #-}

instance
  ( forall n. (KnownNat n, 1 <= n) => Ord (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  Ord (SomeBV bv)
  where
  < :: SomeBV bv -> SomeBV bv -> Bool
(<) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> (Integer -> Integer -> Bool) -> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> 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
(<) ((Integer -> Bool) -> Integer -> Integer -> Bool
forall a b. a -> b -> a
const ((Integer -> Bool) -> Integer -> Integer -> Bool)
-> (Integer -> Bool) -> Integer -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Integer -> Bool
forall a b. a -> b -> a
const (Bool -> Integer -> Bool) -> Bool -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Bool
forall a e. Exception e => e -> a
throw (SomeBVException -> Bool) -> SomeBVException -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"<")
  {-# INLINE (<) #-}
  <= :: SomeBV bv -> SomeBV bv -> Bool
(<=) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> (Integer -> Integer -> Bool) -> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> 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
(<=) ((Integer -> Bool) -> Integer -> Integer -> Bool
forall a b. a -> b -> a
const ((Integer -> Bool) -> Integer -> Integer -> Bool)
-> (Integer -> Bool) -> Integer -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Integer -> Bool
forall a b. a -> b -> a
const (Bool -> Integer -> Bool) -> Bool -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Bool
forall a e. Exception e => e -> a
throw (SomeBVException -> Bool) -> SomeBVException -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"(<=)")
  {-# INLINE (<=) #-}
  > :: SomeBV bv -> SomeBV bv -> Bool
(>) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> (Integer -> Integer -> Bool) -> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> 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
(>) ((Integer -> Bool) -> Integer -> Integer -> Bool
forall a b. a -> b -> a
const ((Integer -> Bool) -> Integer -> Integer -> Bool)
-> (Integer -> Bool) -> Integer -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Integer -> Bool
forall a b. a -> b -> a
const (Bool -> Integer -> Bool) -> Bool -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Bool
forall a e. Exception e => e -> a
throw (SomeBVException -> Bool) -> SomeBVException -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
">")
  {-# INLINE (>) #-}
  >= :: SomeBV bv -> SomeBV bv -> Bool
(>=) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> (Integer -> Integer -> Bool) -> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> 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
(>=) ((Integer -> Bool) -> Integer -> Integer -> Bool
forall a b. a -> b -> a
const ((Integer -> Bool) -> Integer -> Integer -> Bool)
-> (Integer -> Bool) -> Integer -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Integer -> Bool
forall a b. a -> b -> a
const (Bool -> Integer -> Bool) -> Bool -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Bool
forall a e. Exception e => e -> a
throw (SomeBVException -> Bool) -> SomeBVException -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"(>=)")
  {-# INLINE (>=) #-}
  max :: SomeBV bv -> SomeBV bv -> SomeBV bv
max = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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 ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"max")
  {-# INLINE max #-}
  min :: SomeBV bv -> SomeBV bv -> SomeBV bv
min = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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 ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"min")
  {-# INLINE min #-}
  compare :: SomeBV bv -> SomeBV bv -> Ordering
compare =
    (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> Ordering)
-> (Integer -> Integer -> Ordering)
-> SomeBV bv
-> SomeBV bv
-> Ordering
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> 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 ((Integer -> Ordering) -> Integer -> Integer -> Ordering
forall a b. a -> b -> a
const ((Integer -> Ordering) -> Integer -> Integer -> Ordering)
-> (Integer -> Ordering) -> Integer -> Integer -> Ordering
forall a b. (a -> b) -> a -> b
$ Ordering -> Integer -> Ordering
forall a b. a -> b -> a
const (Ordering -> Integer -> Ordering)
-> Ordering -> Integer -> Ordering
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Ordering
forall a e. Exception e => e -> a
throw (SomeBVException -> Ordering) -> SomeBVException -> Ordering
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"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)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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
(+) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+)
  {-# INLINE (+) #-}
  (-) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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
(*) ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"(*)")
  {-# INLINE (*) #-}
  negate :: SomeBV bv -> SomeBV bv
negate = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> 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 Integer -> Integer
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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> 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 (Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"abs")
  {-# INLINE abs #-}
  signum :: SomeBV bv -> SomeBV bv
signum = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> 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 (Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"signum")
  {-# INLINE signum #-}
  fromInteger :: Integer -> SomeBV bv
fromInteger = Integer -> SomeBV bv
forall (bv :: Nat -> *). Integer -> SomeBV bv
SomeBVLit
  {-# INLINE fromInteger #-}

instance
  ( forall n. (KnownNat n, 1 <= n) => Bits (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (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)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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
(.&.) Integer -> Integer -> Integer
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)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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
(.|.) Integer -> Integer -> Integer
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)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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 Integer -> Integer -> Integer
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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> 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 Integer -> Integer
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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`shift` Int
i) (Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"shift") 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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`rotate` Int
i) (Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"rotate") 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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`setBit` Int
i) (Integer -> Int -> Integer
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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`clearBit` Int
i) (Integer -> Int -> Integer
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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`complementBit` Int
i) (Integer -> Int -> Integer
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)
-> (Integer -> Bool) -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> r) -> SomeBV bv -> r
unarySomeBV (bv n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i) (Bool -> Integer -> Bool
forall a b. a -> b -> a
const (Bool -> Integer -> Bool) -> Bool -> Integer -> Bool
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Bool
forall a e. Exception e => e -> a
throw (SomeBVException -> Bool) -> SomeBVException -> Bool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"testBit") SomeBV bv
s
  bitSizeMaybe :: SomeBV bv -> Maybe Int
bitSizeMaybe =
    (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Maybe Int)
-> (Integer -> Maybe Int) -> SomeBV bv -> Maybe Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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
      (Maybe Int -> Integer -> Maybe Int
forall a b. a -> b -> a
const (Maybe Int -> Integer -> Maybe Int)
-> Maybe Int -> Integer -> Maybe Int
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Maybe Int
forall a e. Exception e => e -> a
throw (SomeBVException -> Maybe Int) -> SomeBVException -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"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)
-> (Integer -> Maybe Int) -> SomeBV bv -> Maybe Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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
        (Maybe Int -> Integer -> Maybe Int
forall a b. a -> b -> a
const (Maybe Int -> Integer -> Maybe Int)
-> Maybe Int -> Integer -> Maybe Int
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Maybe Int
forall a e. Exception e => e -> a
throw (SomeBVException -> Maybe Int) -> SomeBVException -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"bitSize")
  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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i) (Integer -> Int -> Integer
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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
i) (Integer -> Int -> Integer
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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`shiftR` Int
i) (Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"shiftR") 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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1
      (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`unsafeShiftR` Int
i)
      (Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"unsafeShiftR")
      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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1
      (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`rotateL` Int
i)
      (Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"rotateL")
      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)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1
      (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`rotateR` Int
i)
      (Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"rotateR")
      SomeBV bv
s
  popCount :: SomeBV bv -> Int
popCount =
    (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> (Integer -> Int) -> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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 (Int -> Integer -> Int
forall a b. a -> b -> a
const (Int -> Integer -> Int) -> Int -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Int
forall a e. Exception e => e -> a
throw (SomeBVException -> Int) -> SomeBVException -> Int
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"popCount")

instance
  ( forall n. (KnownNat n, 1 <= n) => FiniteBits (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  FiniteBits (SomeBV bv)
  where
  finiteBitSize :: SomeBV bv -> Int
finiteBitSize =
    (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> (Integer -> Int) -> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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
      (Int -> Integer -> Int
forall a b. a -> b -> a
const (Int -> Integer -> Int) -> Int -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Int
forall a e. Exception e => e -> a
throw (SomeBVException -> Int) -> SomeBVException -> Int
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"finiteBitSize")
  {-# INLINE finiteBitSize #-}
  countLeadingZeros :: SomeBV bv -> Int
countLeadingZeros =
    (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> (Integer -> Int) -> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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
      (Int -> Integer -> Int
forall a b. a -> b -> a
const (Int -> Integer -> Int) -> Int -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Int
forall a e. Exception e => e -> a
throw (SomeBVException -> Int) -> SomeBVException -> Int
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"countLeadingZeros")
  {-# INLINE countLeadingZeros #-}
  countTrailingZeros :: SomeBV bv -> Int
countTrailingZeros =
    (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> (Integer -> Int) -> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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
      (Int -> Integer -> Int
forall a b. a -> b -> a
const (Int -> Integer -> Int) -> Int -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Int
forall a e. Exception e => e -> a
throw (SomeBVException -> Int) -> SomeBVException -> Int
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"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)
-> (Integer -> Int) -> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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 (Int -> Integer -> Int
forall a b. a -> b -> a
const (Int -> Integer -> Int) -> Int -> Integer -> Int
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Int
forall a e. Exception e => e -> a
throw (SomeBVException -> Int) -> SomeBVException -> Int
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"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)
-> (Integer -> Rational) -> SomeBV bv -> Rational
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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 (Rational -> Integer -> Rational
forall a b. a -> b -> a
const (Rational -> Integer -> Rational)
-> Rational -> Integer -> Rational
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Rational
forall a e. Exception e => e -> a
throw (SomeBVException -> Rational) -> SomeBVException -> Rational
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"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)
-> (Integer -> Integer) -> SomeBV bv -> Integer
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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
      (Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"toInteger")
  {-# INLINE toInteger #-}
  quot :: SomeBV bv -> SomeBV bv -> SomeBV bv
quot = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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 ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer -> Integer)
-> SomeBVException -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"quot")
  {-# INLINE quot #-}
  rem :: SomeBV bv -> SomeBV bv -> SomeBV bv
rem = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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 ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer -> Integer)
-> SomeBVException -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"rem")
  {-# INLINE rem #-}
  div :: SomeBV bv -> SomeBV bv -> SomeBV bv
div = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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 ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer -> Integer)
-> SomeBVException -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"div")
  {-# INLINE div #-}
  mod :: SomeBV bv -> SomeBV bv -> SomeBV bv
mod = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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 ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer -> Integer)
-> SomeBVException -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"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))
-> (Integer -> Integer -> (Integer, Integer))
-> SomeBV bv
-> SomeBV bv
-> (SomeBV bv, SomeBV bv)
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> (bv n, bv n))
-> (Integer -> Integer -> (Integer, Integer))
-> 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 ((Integer -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
forall a b. a -> b -> a
const ((Integer -> (Integer, Integer))
 -> Integer -> Integer -> (Integer, Integer))
-> (Integer -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer -> (Integer, Integer)
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer -> (Integer, Integer))
-> SomeBVException -> Integer -> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"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))
-> (Integer -> Integer -> (Integer, Integer))
-> SomeBV bv
-> SomeBV bv
-> (SomeBV bv, SomeBV bv)
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> (bv n, bv n))
-> (Integer -> Integer -> (Integer, Integer))
-> 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 ((Integer -> (Integer, Integer))
-> Integer -> Integer -> (Integer, Integer)
forall a b. a -> b -> a
const ((Integer -> (Integer, Integer))
 -> Integer -> Integer -> (Integer, Integer))
-> (Integer -> (Integer, Integer))
-> Integer
-> Integer
-> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer -> (Integer, Integer)
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer -> (Integer, Integer))
-> SomeBVException -> Integer -> (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"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
  bvConcat SomeBV bv
_ SomeBV bv
_ = SomeBVException -> SomeBV bv
forall a e. Exception e => e -> a
throw (SomeBVException -> SomeBV bv) -> SomeBVException -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"bvConcat"
  {-# 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
  bvZext Int
_ SomeBV bv
_ = SomeBVException -> SomeBV bv
forall a e. Exception e => e -> a
throw (SomeBVException -> SomeBV bv) -> SomeBVException -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"bvZext"
  {-# 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
  bvSext Int
_ SomeBV bv
_ = SomeBVException -> SomeBV bv
forall a e. Exception e => e -> a
throw (SomeBVException -> SomeBV bv) -> SomeBVException -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"bvSext"
  {-# 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
  bvExt Int
_ SomeBV bv
_ = SomeBVException -> SomeBV bv
forall a e. Exception e => e -> a
throw (SomeBVException -> SomeBV bv) -> SomeBVException -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"bvExt"
  {-# 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
  bvSelect Int
_ Int
_ SomeBV bv
_ = SomeBVException -> SomeBV bv
forall a e. Exception e => e -> a
throw (SomeBVException -> SomeBV bv) -> SomeBVException -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"bvSelect"
  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) => EvalSym (bv n)) =>
  EvalSym (SomeBV bv)
  where
  evalSym :: Bool -> Model -> SomeBV bv -> SomeBV bv
evalSym Bool
fillDefault Model
model = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 (Bool -> Model -> bv n -> bv n
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
fillDefault Model
model) Integer -> Integer
forall a. a -> a
id
  {-# INLINE evalSym #-}

instance
  (forall n. (KnownNat n, 1 <= n) => ExtractSym (bv n)) =>
  ExtractSym (SomeBV bv)
  where
  extractSymMaybe :: forall (knd :: SymbolKind).
IsSymbolKind knd =>
SomeBV bv -> Maybe (SymbolSet knd)
extractSymMaybe = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> Maybe (SymbolSet knd))
-> (Integer -> Maybe (SymbolSet knd))
-> SomeBV bv
-> Maybe (SymbolSet knd)
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> r) -> SomeBV bv -> r
unarySomeBV bv n -> Maybe (SymbolSet knd)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
bv n -> Maybe (SymbolSet knd)
extractSymMaybe Integer -> Maybe (SymbolSet knd)
forall a (knd :: SymbolKind).
(ExtractSym a, IsSymbolKind knd) =>
a -> Maybe (SymbolSet knd)
forall (knd :: SymbolKind).
IsSymbolKind knd =>
Integer -> Maybe (SymbolSet knd)
extractSymMaybe
  {-# INLINE extractSymMaybe #-}

instance
  (forall n. (KnownNat n, 1 <= n) => PPrint (bv n)) =>
  PPrint (SomeBV bv)
  where
  pformat :: forall ann. SomeBV bv -> Doc ann
pformat (SomeBV bv n
bv) = bv n -> Doc ann
forall ann. bv n -> Doc ann
forall a ann. PPrint a => a -> Doc ann
pformat bv n
bv
  pformat (SomeBVLit Integer
i) = Doc ann
"bvlit(" Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Integer -> Doc ann
forall ann. Integer -> Doc ann
forall a ann. PPrint a => a -> Doc ann
pformat Integer
i Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> Doc ann
")"
  {-# INLINE pformat #-}

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)
      )

-- | The 'symDistinct' instance for t'SomeBV' will have the following behavior:
--
-- * If the list is empty or has only one element, it will return 'True'.
-- * If none of the elements have a bit-width, it will throw
--   'UndeterminedBitwidth' exception.
-- * If the elements have different bit-widths, it will throw a
--   'BitwidthMismatch' exception.
-- * If there are at least one element have a bit-width, and all elements with
--   known bit-width have the same bit-width, it will generate a single symbolic
--   formula using @distinct@.
instance
  ( forall n. (KnownNat n, 1 <= n) => SymEq (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  SymEq (SomeBV bv)
  where
  SomeBV (bv n
l :: bv l) .== :: SomeBV bv -> SomeBV bv -> SymBool
.== 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
l bv n -> bv n -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== bv n
bv n
r
      Maybe (n :~: n)
Nothing -> Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
False
  SomeBV (bv n
l :: bv l) .== SomeBVLit Integer
r = bv n
l bv n -> bv n -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== Integer -> bv n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
r
  SomeBVLit Integer
l .== SomeBV (bv n
r :: bv r) = Integer -> bv n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
l bv n -> bv n -> SymBool
forall a. SymEq a => a -> a -> SymBool
.== bv n
r
  SomeBVLit Integer
_ .== SomeBVLit Integer
_ = SomeBVException -> SymBool
forall a e. Exception e => e -> a
throw (SomeBVException -> SymBool) -> SomeBVException -> SymBool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
".=="
  {-# INLINE (.==) #-}
  SomeBV (bv n
l :: bv l) ./= :: SomeBV bv -> SomeBV bv -> SymBool
./= 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
l bv n -> bv n -> SymBool
forall a. SymEq a => a -> a -> SymBool
./= bv n
bv n
r
      Maybe (n :~: n)
Nothing -> Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
  SomeBV (bv n
l :: bv l) ./= SomeBVLit Integer
r = bv n
l bv n -> bv n -> SymBool
forall a. SymEq a => a -> a -> SymBool
./= Integer -> bv n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
r
  SomeBVLit Integer
l ./= SomeBV (bv n
r :: bv r) = Integer -> bv n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
l bv n -> bv n -> SymBool
forall a. SymEq a => a -> a -> SymBool
./= bv n
r
  SomeBVLit Integer
_ ./= SomeBVLit Integer
_ = SomeBVException -> SymBool
forall a e. Exception e => e -> a
throw (SomeBVException -> SymBool) -> SomeBVException -> SymBool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"./="
  symDistinct :: [SomeBV bv] -> SymBool
symDistinct [SomeBV bv]
l = case [SomeBV bv]
l of
    [] -> Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
    [SomeBV bv
_] -> Bool -> SymBool
forall c t. Solvable c t => c -> t
con Bool
True
    [SomeBV bv]
_ -> case Text -> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
Text -> [SomeBV bv] -> Either SomeBVException [SomeBV bv]
assignBitWidthList Text
"symDistinct" [SomeBV bv]
l of
      Right (SomeBV (bv n
a :: bv a) : [SomeBV bv]
l) -> [bv n] -> SymBool
forall a. SymEq a => [a] -> SymBool
symDistinct ([bv n] -> SymBool) -> [bv n] -> SymBool
forall a b. (a -> b) -> a -> b
$ bv n
a bv n -> [bv n] -> [bv n]
forall a. a -> [a] -> [a]
: [SomeBV bv] -> [bv n]
go [SomeBV bv]
l
        where
          go :: [SomeBV bv] -> [bv a]
          go :: [SomeBV bv] -> [bv n]
go [] = []
          go (SomeBV (bv n
x :: bv x) : [SomeBV bv]
xs) = 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 @x) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @a) of
            Just n :~: n
Refl -> bv n
bv n
x bv n -> [bv n] -> [bv n]
forall a. a -> [a] -> [a]
: [SomeBV bv] -> [bv n]
go [SomeBV bv]
xs
            Maybe (n :~: n)
Nothing -> String -> [bv n]
forall a. HasCallStack => String -> a
error String
"Should not happen"
          go (SomeBVLit Integer
_ : [SomeBV bv]
_) = String -> [bv n]
forall a. HasCallStack => String -> a
error String
"Should not happen"
      Right [SomeBV bv]
_ -> String -> SymBool
forall a. HasCallStack => String -> a
error String
"Should not happen"
      Left UndeterminedBitwidth {} -> SomeBVException -> SymBool
forall a e. Exception e => e -> a
throw (SomeBVException -> SymBool) -> SomeBVException -> SymBool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"symDistinct"
      Left SomeBVException
BitwidthMismatch -> SomeBVException -> SymBool
forall a e. Exception e => e -> a
throw SomeBVException
BitwidthMismatch
  {-# INLINE (./=) #-}

instance
  ( forall n. (KnownNat n, 1 <= n) => SymOrd (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  SymOrd (SomeBV bv)
  where
  .< :: SomeBV bv -> SomeBV bv -> SymBool
(.<) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SymBool)
-> (Integer -> Integer -> SymBool)
-> SomeBV bv
-> SomeBV bv
-> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> 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. SymOrd a => a -> a -> SymBool
(.<) ((Integer -> SymBool) -> Integer -> Integer -> SymBool
forall a b. a -> b -> a
const ((Integer -> SymBool) -> Integer -> Integer -> SymBool)
-> (Integer -> SymBool) -> Integer -> Integer -> SymBool
forall a b. (a -> b) -> a -> b
$ SymBool -> Integer -> SymBool
forall a b. a -> b -> a
const (SymBool -> Integer -> SymBool) -> SymBool -> Integer -> SymBool
forall a b. (a -> b) -> a -> b
$ SomeBVException -> SymBool
forall a e. Exception e => e -> a
throw (SomeBVException -> SymBool) -> SomeBVException -> SymBool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"(.<)")
  {-# INLINE (.<) #-}
  .<= :: SomeBV bv -> SomeBV bv -> SymBool
(.<=) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SymBool)
-> (Integer -> Integer -> SymBool)
-> SomeBV bv
-> SomeBV bv
-> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> 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. SymOrd a => a -> a -> SymBool
(.<=) ((Integer -> SymBool) -> Integer -> Integer -> SymBool
forall a b. a -> b -> a
const ((Integer -> SymBool) -> Integer -> Integer -> SymBool)
-> (Integer -> SymBool) -> Integer -> Integer -> SymBool
forall a b. (a -> b) -> a -> b
$ SymBool -> Integer -> SymBool
forall a b. a -> b -> a
const (SymBool -> Integer -> SymBool) -> SymBool -> Integer -> SymBool
forall a b. (a -> b) -> a -> b
$ SomeBVException -> SymBool
forall a e. Exception e => e -> a
throw (SomeBVException -> SymBool) -> SomeBVException -> SymBool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"(.<=)")
  {-# INLINE (.<=) #-}
  .> :: SomeBV bv -> SomeBV bv -> SymBool
(.>) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SymBool)
-> (Integer -> Integer -> SymBool)
-> SomeBV bv
-> SomeBV bv
-> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> 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. SymOrd a => a -> a -> SymBool
(.>) ((Integer -> SymBool) -> Integer -> Integer -> SymBool
forall a b. a -> b -> a
const ((Integer -> SymBool) -> Integer -> Integer -> SymBool)
-> (Integer -> SymBool) -> Integer -> Integer -> SymBool
forall a b. (a -> b) -> a -> b
$ SymBool -> Integer -> SymBool
forall a b. a -> b -> a
const (SymBool -> Integer -> SymBool) -> SymBool -> Integer -> SymBool
forall a b. (a -> b) -> a -> b
$ SomeBVException -> SymBool
forall a e. Exception e => e -> a
throw (SomeBVException -> SymBool) -> SomeBVException -> SymBool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"(.>)")
  {-# INLINE (.>) #-}
  .>= :: SomeBV bv -> SomeBV bv -> SymBool
(.>=) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> SymBool)
-> (Integer -> Integer -> SymBool)
-> SomeBV bv
-> SomeBV bv
-> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> 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. SymOrd a => a -> a -> SymBool
(.>=) ((Integer -> SymBool) -> Integer -> Integer -> SymBool
forall a b. a -> b -> a
const ((Integer -> SymBool) -> Integer -> Integer -> SymBool)
-> (Integer -> SymBool) -> Integer -> Integer -> SymBool
forall a b. (a -> b) -> a -> b
$ SymBool -> Integer -> SymBool
forall a b. a -> b -> a
const (SymBool -> Integer -> SymBool) -> SymBool -> Integer -> SymBool
forall a b. (a -> b) -> a -> b
$ SomeBVException -> SymBool
forall a e. Exception e => e -> a
throw (SomeBVException -> SymBool) -> SomeBVException -> SymBool
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"(.>=)")
  {-# INLINE (.>=) #-}
  symCompare :: SomeBV bv -> SomeBV bv -> Union Ordering
symCompare =
    (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> Union Ordering)
-> (Integer -> Integer -> Union Ordering)
-> SomeBV bv
-> SomeBV bv
-> Union Ordering
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> r) -> SomeBV bv -> SomeBV bv -> r
binSomeBV
      bv n -> bv n -> Union Ordering
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> Union Ordering
forall a. SymOrd a => a -> a -> Union Ordering
symCompare
      ((Integer -> Union Ordering) -> Integer -> Integer -> Union Ordering
forall a b. a -> b -> a
const ((Integer -> Union Ordering)
 -> Integer -> Integer -> Union Ordering)
-> (Integer -> Union Ordering)
-> Integer
-> Integer
-> Union Ordering
forall a b. (a -> b) -> a -> b
$ Union Ordering -> Integer -> Union Ordering
forall a b. a -> b -> a
const (Union Ordering -> Integer -> Union Ordering)
-> Union Ordering -> Integer -> Union Ordering
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Union Ordering
forall a e. Exception e => e -> a
throw (SomeBVException -> Union Ordering)
-> SomeBVException -> Union Ordering
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"symCompare")
  {-# INLINE symCompare #-}

instance
  (forall n. (KnownNat n, 1 <= n) => SubstSym (bv n)) =>
  SubstSym (SomeBV bv)
  where
  substSym :: forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> SomeBV bv -> SomeBV bv
substSym TypedSymbol knd cb
c sb
s = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> (Integer -> Integer) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 (TypedSymbol knd cb -> sb -> bv n -> bv n
forall a cb sb (knd :: SymbolKind).
(SubstSym a, LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> a -> a
forall cb sb (knd :: SymbolKind).
(LinkedRep cb sb, IsSymbolKind knd) =>
TypedSymbol knd cb -> sb -> bv n -> bv n
substSym TypedSymbol knd cb
c sb
s) Integer -> Integer
forall a. a -> a
id
  {-# INLINE substSym #-}

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 (Union (SomeBV bv))
fresh Proxy n
_ =
    (\(Union (bv n)
i :: Union (bv n)) -> (bv n -> SomeBV bv) -> Union (bv n) -> Union (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 Union (bv n)
i) (Union (bv n) -> Union (SomeBV bv))
-> m (Union (bv n)) -> m (Union (SomeBV bv))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m (Union (bv n))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (Union a)
forall (m :: * -> *). MonadFresh m => () -> m (Union (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 (Union (SomeBV bv))
fresh (SomeBV (bv n
_ :: bv x)) = Proxy n -> m (Union (SomeBV bv))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (Union a)
forall (m :: * -> *).
MonadFresh m =>
Proxy n -> m (Union (SomeBV bv))
fresh (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)
  fresh (SomeBVLit Integer
_) = SomeBVException -> m (Union (SomeBV bv))
forall a e. Exception e => e -> a
throw (SomeBVException -> m (Union (SomeBV bv)))
-> SomeBVException -> m (Union (SomeBV bv))
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"fresh"
  {-# 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)
  simpleFresh (SomeBVLit Integer
_) = SomeBVException -> m (SomeBV bv)
forall a e. Exception e => e -> a
throw (SomeBVException -> m (SomeBV bv))
-> SomeBVException -> m (SomeBV bv)
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"simpleFresh"
  {-# 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 (Union (SomeBV bv))
fresh Int
n
    | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> m (Union (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 (Union (SomeBV bv))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (Union a)
forall (m :: * -> *).
MonadFresh m =>
Proxy n -> m (Union (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)
  toSigned (SomeBVLit Integer
i) = Integer -> SomeBV sbv
forall (bv :: Nat -> *). Integer -> SomeBV bv
SomeBVLit Integer
i
  {-# 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)
  toUnsigned (SomeBVLit Integer
i) = Integer -> SomeBV ubv
forall (bv :: Nat -> *). Integer -> SomeBV bv
SomeBVLit Integer
i
  {-# 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))
  toCon (SomeBVLit Integer
i) = 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
$ Integer -> SomeBV cbv
forall (bv :: Nat -> *). Integer -> SomeBV bv
SomeBVLit Integer
i
  {-# 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)
  toSym (SomeBVLit Integer
i) = Integer -> SomeBV sbv
forall (bv :: Nat -> *). Integer -> SomeBV bv
SomeBVLit Integer
i
  {-# INLINE toSym #-}

divRemOrBase0 ::
  ( forall n.
    (KnownNat n, 1 <= n) =>
    (bv n, bv n) ->
    bv n ->
    bv n ->
    (bv n, bv n)
  ) ->
  (SomeBV bv, SomeBV bv) ->
  SomeBV bv ->
  SomeBV bv ->
  (SomeBV bv, SomeBV bv)
divRemOrBase0 :: forall (bv :: Nat -> *).
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 (bv n, bv n) -> bv n -> bv n -> (bv n, bv n))
-> (SomeBV bv, SomeBV bv)
-> SomeBV bv
-> SomeBV bv
-> (SomeBV bv, SomeBV bv)
divRemOrBase0
  forall (n :: Nat).
(KnownNat n, 1 <= n) =>
(bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
f
  (SomeBV (bv n
dd :: bv dd), SomeBV (bv n
dm :: bv dm))
  (SomeBV (bv n
a :: bv a))
  (SomeBV (bv n
b :: bv b)) =
    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 @a) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @b),
           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 @a) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @dd),
           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 @a) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @dm)
         ) of
      (Just n :~: n
Refl, Just n :~: n
Refl, Just n :~: n
Refl) -> (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 ((bv n, bv n) -> (SomeBV bv, SomeBV bv))
-> (bv n, bv n) -> (SomeBV bv, SomeBV bv)
forall a b. (a -> b) -> a -> b
$ (bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
(bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
f (bv n
dd, bv n
bv n
dm) bv n
bv n
a bv n
bv n
b
      (Maybe (n :~: n), Maybe (n :~: n), Maybe (n :~: n))
_ -> String -> (SomeBV bv, SomeBV bv)
forall a. HasCallStack => String -> a
error String
"Should not happen"
divRemOrBase0 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
(bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
_ (SomeBV bv, SomeBV bv)
_ SomeBV bv
_ SomeBV bv
_ = String -> (SomeBV bv, SomeBV bv)
forall a. HasCallStack => String -> a
error String
"Should not happen"
{-# INLINE divRemOrBase0 #-}

divRemOrBase ::
  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>
  ( forall n.
    (KnownNat n, 1 <= n) =>
    (bv n, bv n) ->
    bv n ->
    bv n ->
    (bv n, bv n)
  ) ->
  (SomeBV bv, SomeBV bv) ->
  SomeBV bv ->
  SomeBV bv ->
  (SomeBV bv, SomeBV bv)
divRemOrBase :: forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 (bv n, bv n) -> bv n -> bv n -> (bv n, bv n))
-> (SomeBV bv, SomeBV bv)
-> SomeBV bv
-> SomeBV bv
-> (SomeBV bv, SomeBV bv)
divRemOrBase forall (n :: Nat).
(KnownNat n, 1 <= n) =>
(bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
f (SomeBV bv
a, SomeBV bv
b) SomeBV bv
c SomeBV bv
d =
  case Text
-> (SomeBV bv, SomeBV bv, SomeBV bv, SomeBV bv)
-> Either
     SomeBVException (SomeBV bv, SomeBV bv, SomeBV bv, SomeBV bv)
forall a. AssignBitWidth a => Text -> a -> Either SomeBVException a
assignBitWidth Text
"divRemOrBase" (SomeBV bv
a, SomeBV bv
b, SomeBV bv
c, SomeBV bv
d) of
    Right (SomeBV bv
a', SomeBV bv
b', SomeBV bv
c', SomeBV bv
d') -> (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 (bv n, bv n) -> bv n -> bv n -> (bv n, bv n))
-> (SomeBV bv, SomeBV bv)
-> 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 -> (bv n, bv n))
-> (SomeBV bv, SomeBV bv)
-> SomeBV bv
-> SomeBV bv
-> (SomeBV bv, SomeBV bv)
divRemOrBase0 (bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
(bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
f (SomeBV bv
a', SomeBV bv
b') SomeBV bv
c' SomeBV bv
d'
    Left SomeBVException
e -> SomeBVException -> (SomeBV bv, SomeBV bv)
forall a e. Exception e => e -> a
throw SomeBVException
e

instance
  ( forall n. (KnownNat n, 1 <= n) => DivOr (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  DivOr (SomeBV bv)
  where
  divOr :: SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv
divOr = (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) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv
ternSomeBVR1 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. DivOr a => a -> a -> a -> a
divOr
  {-# INLINE divOr #-}
  modOr :: SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv
modOr = (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) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv
ternSomeBVR1 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. DivOr a => a -> a -> a -> a
modOr
  {-# INLINE modOr #-}
  quotOr :: SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv
quotOr = (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) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv
ternSomeBVR1 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. DivOr a => a -> a -> a -> a
quotOr
  {-# INLINE quotOr #-}
  remOr :: SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv
remOr = (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) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv
ternSomeBVR1 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. DivOr a => a -> a -> a -> a
remOr
  {-# INLINE remOr #-}
  divModOr :: (SomeBV bv, SomeBV bv)
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
divModOr = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 (bv n, bv n) -> bv n -> bv n -> (bv n, bv n))
-> (SomeBV bv, SomeBV bv)
-> SomeBV bv
-> SomeBV bv
-> (SomeBV bv, SomeBV bv)
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 (bv n, bv n) -> bv n -> bv n -> (bv n, bv n))
-> (SomeBV bv, SomeBV bv)
-> SomeBV bv
-> SomeBV bv
-> (SomeBV bv, SomeBV bv)
divRemOrBase (bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
(bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
forall a. DivOr a => (a, a) -> a -> a -> (a, a)
divModOr
  {-# INLINE divModOr #-}
  quotRemOr :: (SomeBV bv, SomeBV bv)
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
quotRemOr = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 (bv n, bv n) -> bv n -> bv n -> (bv n, bv n))
-> (SomeBV bv, SomeBV bv)
-> SomeBV bv
-> SomeBV bv
-> (SomeBV bv, SomeBV bv)
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 (bv n, bv n) -> bv n -> bv n -> (bv n, bv n))
-> (SomeBV bv, SomeBV bv)
-> SomeBV bv
-> SomeBV bv
-> (SomeBV bv, SomeBV bv)
divRemOrBase (bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
(bv n, bv n) -> bv n -> bv n -> (bv n, bv n)
forall a. DivOr a => (a, a) -> a -> a -> (a, a)
quotRemOr
  {-# INLINE quotRemOr #-}

instance
  ( forall n.
    (KnownNat n, 1 <= n) =>
    SafeDiv e (bv n) (ExceptT e m),
    MonadError (Either SomeBVException e) m,
    TryMerge m,
    Mergeable e,
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  SafeDiv (Either SomeBVException 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeDiv @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeDiv")
  {-# 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeMod @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeMod")
  {-# 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeQuot @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeQuot")
  {-# 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m a
safeRem @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeRem")
  {-# 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))
-> (Integer
    -> Integer
    -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv, SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n, bv n))
-> (Integer
    -> Integer
    -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2
      (forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m (a, a)
safeDivMod @e)
      ((Integer
 -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a b. a -> b -> a
const ((Integer
  -> ExceptT (Either SomeBVException e) m (Integer, Integer))
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> (Integer
    -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m (Integer, Integer)
-> Integer
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m (Integer, Integer)
 -> Integer
 -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
-> Integer
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeDivMod")
  {-# 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))
-> (Integer
    -> Integer
    -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv, SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n, bv n))
-> (Integer
    -> Integer
    -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2
      (forall e a (m :: * -> *). SafeDiv e a m => a -> a -> m (a, a)
safeQuotRem @e)
      ((Integer
 -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a b. a -> b -> a
const ((Integer
  -> ExceptT (Either SomeBVException e) m (Integer, Integer))
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> (Integer
    -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m (Integer, Integer)
-> Integer
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m (Integer, Integer)
 -> Integer
 -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
-> Integer
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeQuotRem")
  {-# INLINE safeQuotRem #-}

instance
  ( forall n.
    (KnownNat n, 1 <= n) =>
    SafeLinearArith e (bv n) (ExceptT e m),
    MonadError (Either SomeBVException e) m,
    TryMerge m,
    Mergeable e,
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  SafeLinearArith (Either SomeBVException 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeLinearArith e a m => a -> a -> m a
safeAdd @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeAdd")
  {-# 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeLinearArith e a m => a -> a -> m a
safeSub @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeSub")
  {-# INLINE safeSub #-}
  safeNeg :: SomeBV bv -> m (SomeBV bv)
safeNeg =
    (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> m (SomeBV bv))
-> (Integer -> m (SomeBV bv)) -> SomeBV bv -> m (SomeBV bv)
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> r) -> SomeBV bv -> r
unarySomeBV
      ( \bv n
v ->
          (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)) -> m (bv n) -> m (SomeBV bv)
forall a b. (a -> b) -> a -> b
$
            ExceptT e m (bv n) -> m (Either e (bv n))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (forall e a (m :: * -> *). SafeLinearArith e a m => a -> m a
safeNeg @e bv n
v) m (Either e (bv n)) -> (Either e (bv n) -> m (bv n)) -> m (bv n)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (e -> m (bv n))
-> (bv n -> m (bv n)) -> Either e (bv n) -> m (bv n)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either SomeBVException e -> m (bv n)
forall a. Either SomeBVException e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e -> m (bv n))
-> (e -> Either SomeBVException e) -> e -> m (bv n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either SomeBVException e
forall a b. b -> Either a b
Right) bv n -> m (bv n)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      )
      (m (SomeBV bv) -> Integer -> m (SomeBV bv)
forall a b. a -> b -> a
const (m (SomeBV bv) -> Integer -> m (SomeBV bv))
-> m (SomeBV bv) -> Integer -> m (SomeBV bv)
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e -> m (SomeBV bv)
forall a. Either SomeBVException e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e -> m (SomeBV bv))
-> Either SomeBVException e -> m (SomeBV bv)
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeNeg")
  {-# INLINE safeNeg #-}

instance
  ( forall n. (KnownNat n, 1 <= n) => SymShift (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (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)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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
      ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeShift")
  {-# INLINE symShift #-}
  symShiftNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv
symShiftNegated =
    (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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
      ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeShiftNegated")
  {-# INLINE symShiftNegated #-}

instance
  ( forall n. (KnownNat n, 1 <= n) => SymRotate (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (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)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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
      ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeRotate")
  {-# INLINE symRotate #-}
  symRotateNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv
symRotateNegated =
    (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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
      ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeRotateNegated")
  {-# INLINE symRotateNegated #-}

instance
  ( forall n.
    (KnownNat n, 1 <= n) =>
    SafeSymShift e (bv n) (ExceptT e m),
    MonadError (Either SomeBVException e) m,
    TryMerge m,
    Mergeable e,
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  SafeSymShift (Either SomeBVException 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymShiftL @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeSymShiftL")
  {-# 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymShiftR @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeSymShiftR")
  {-# 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymStrictShiftL @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeSymStrictShiftL")
  {-# 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymStrictShiftR @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeSymStrictShiftR")
  {-# INLINE safeSymStrictShiftR #-}

instance
  ( forall n.
    (KnownNat n, 1 <= n) =>
    SafeSymRotate e (bv n) (ExceptT e m),
    MonadError (Either SomeBVException e) m,
    TryMerge m,
    Mergeable e,
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  SafeSymRotate (Either SomeBVException 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeSymRotate e a m => a -> a -> m a
safeSymRotateL @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeSymRotateL")
  {-# 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))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n))
-> (Integer
    -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv)
binSomeBVSafeR1
      (forall e a (m :: * -> *). SafeSymRotate e a m => a -> a -> m a
safeSymRotateR @e)
      ((Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const ((Integer -> ExceptT (Either SomeBVException e) m Integer)
 -> Integer
 -> Integer
 -> ExceptT (Either SomeBVException e) m Integer)
-> (Integer -> ExceptT (Either SomeBVException e) m Integer)
-> Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m Integer
-> Integer -> ExceptT (Either SomeBVException e) m Integer
forall a b. a -> b -> a
const (ExceptT (Either SomeBVException e) m Integer
 -> Integer -> ExceptT (Either SomeBVException e) m Integer)
-> ExceptT (Either SomeBVException e) m Integer
-> Integer
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a.
Either SomeBVException e -> ExceptT (Either SomeBVException e) m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e
 -> ExceptT (Either SomeBVException e) m Integer)
-> Either SomeBVException e
-> ExceptT (Either SomeBVException e) m Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left (SomeBVException -> Either SomeBVException e)
-> SomeBVException -> Either SomeBVException e
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"safeSymRotateR")
  {-# INLINE safeSymRotateR #-}

instance
  ( forall n. (KnownNat n, 1 <= n) => ITEOp (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (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)
-> (Integer -> Integer -> Integer)
-> SomeBV bv
-> SomeBV bv
-> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> (Integer -> Integer -> Integer)
-> 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)
      ((Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. a -> b -> a
const ((Integer -> Integer) -> Integer -> Integer -> Integer)
-> (Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Integer
forall a b. a -> b -> a
const (Integer -> Integer -> Integer) -> Integer -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Integer
forall a e. Exception e => e -> a
throw (SomeBVException -> Integer) -> SomeBVException -> Integer
forall a b. (a -> b) -> a -> b
$ Text -> SomeBVException
UndeterminedBitwidth Text
"symIte")

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])
-> (Integer -> [SomeSym]) -> SomeBV bv -> [SomeSym]
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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 Integer -> [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])
-> (Integer -> [SomeSym] -> [SomeSym])
-> SomeBV bv
-> [SomeSym]
-> [SomeSym]
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> 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 Integer -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS
  {-# INLINE allSymsS #-}

-- Synonyms

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

-- | Pattern synonym for t'SomeBV' for 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 t'SomeBV' for concrete unsigned bitvectors.
type SomeWordN = SomeBV WordN

-- | Pattern synonym for t'SomeBV' for 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 t'SomeBV' for symbolic signed bitvectors.
type SomeSymIntN = SomeBV SymIntN

-- | Pattern synonym for t'SomeBV' for 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 t'SomeBV' for symbolic unsigned bitvectors.
type SomeSymWordN = SomeBV SymWordN

-- | Pattern synonym for t'SomeBV' for 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 t'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 t'SomeBV' with a given concrete t'SomeBV'. Similar to
-- 'con' but for t'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
conBV (SomeBVLit Integer
i) = Integer -> SomeBV bv
forall (bv :: Nat -> *). Integer -> SomeBV bv
SomeBVLit Integer
i

-- | View pattern for symbolic t'SomeBV' to see if it contains a concrete value
-- and extract it. Similar to 'conView' but for t'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
conBVView (SomeBVLit Integer
i) = 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
$ Integer -> SomeBV cbv
forall (bv :: Nat -> *). Integer -> SomeBV bv
SomeBVLit Integer
i

-- | Pattern synonym for symbolic t'SomeBV' to see if it contains a concrete
-- value and extract it. Similar to 'Grisette.Core.Con' but for t'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 t'SomeBV' with a given run-time bitwidth and a symbol.
-- Similar to 'sym' but for t'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 t'SomeBV' with a given run-time bitwidth and an
-- identifier. Similar to 'ssym' but for t'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 t'SomeBV' with a given run-time bitwidth, an identifier
-- and an index. Similar to 'isym' but for t'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 t'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
-- t'SomeBV'.
unarySomeBV ::
  forall bv r.
  (forall n. (KnownNat n, 1 <= n) => bv n -> r) ->
  (Integer -> r) ->
  SomeBV bv ->
  r
unarySomeBV :: forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> (Integer -> r) -> SomeBV bv -> r
unarySomeBV forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r
f Integer -> r
_ (SomeBV bv n
bv) = bv n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r
f bv n
bv
unarySomeBV forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r
_ Integer -> r
g (SomeBVLit Integer
i) = Integer -> r
g Integer
i
{-# INLINE unarySomeBV #-}

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

-- | Lift a binary operation on sized bitvectors that returns anything to
-- t'SomeBV'. Crash if the bitwidths do not match.
binSomeBV ::
  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>
  (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) ->
  (Integer -> Integer -> r) ->
  SomeBV bv ->
  SomeBV bv ->
  r
binSomeBV :: forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> (Integer -> Integer -> r) -> SomeBV bv -> SomeBV bv -> r
binSomeBV forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r
f Integer -> Integer -> r
_ (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 -> SomeBVException -> r
forall a e. Exception e => e -> a
throw SomeBVException
BitwidthMismatch
binSomeBV forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r
f Integer -> Integer -> r
_ (SomeBV (bv n
l :: bv l)) (SomeBVLit Integer
r) = bv n -> bv n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r
f bv n
l (bv n -> r) -> bv n -> r
forall a b. (a -> b) -> a -> b
$ Integer -> bv n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
r
binSomeBV forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r
f Integer -> Integer -> r
_ (SomeBVLit Integer
l) (SomeBV (bv n
r :: bv r)) = bv n -> bv n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r
f (Integer -> bv n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
l) bv n
r
binSomeBV forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r
_ Integer -> Integer -> r
g (SomeBVLit Integer
l) (SomeBVLit Integer
r) = Integer -> Integer -> r
g Integer
l Integer
r
{-# INLINE binSomeBV #-}

-- | Lift a ternary operation on sized bitvectors that returns anything to
-- t'SomeBV'. Crash if the bitwidths do not match.
ternSomeBV ::
  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>
  (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n -> r) ->
  SomeBV bv ->
  SomeBV bv ->
  SomeBV bv ->
  r
ternSomeBV :: forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> SomeBV bv -> r
ternSomeBV forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> bv n -> r
f (SomeBV (bv n
a :: bv a)) (SomeBV (bv n
b :: bv b)) (SomeBV (bv n
c :: bv c)) =
  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 @a) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @b), 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 @a) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @c)) of
    (Just n :~: n
Refl, Just n :~: n
Refl) -> bv n -> bv n -> bv n -> r
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> bv n -> r
f bv n
a bv n
bv n
b bv n
bv n
c
    (Maybe (n :~: n), Maybe (n :~: n))
_ -> SomeBVException -> r
forall a e. Exception e => e -> a
throw SomeBVException
BitwidthMismatch
ternSomeBV forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> bv n -> r
f SomeBV bv
a SomeBV bv
b SomeBV bv
c =
  case Text
-> (SomeBV bv, SomeBV bv, SomeBV bv)
-> Either SomeBVException (SomeBV bv, SomeBV bv, SomeBV bv)
forall a. AssignBitWidth a => Text -> a -> Either SomeBVException a
assignBitWidth Text
"ternSomeBV" (SomeBV bv
a, SomeBV bv
b, SomeBV bv
c) of
    Right (SomeBV bv
a', SomeBV bv
b', SomeBV bv
c') -> (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> SomeBV bv -> r
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> SomeBV bv -> r
ternSomeBV bv n -> bv n -> bv n -> r
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> bv n -> r
f SomeBV bv
a' SomeBV bv
b' SomeBV bv
c'
    Left SomeBVException
e -> SomeBVException -> r
forall a e. Exception e => e -> a
throw SomeBVException
e
{-# INLINE ternSomeBV #-}

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

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

-- | Lift a ternary operation on sized bitvectors that returns a bitvector to
-- t'SomeBV'. The result will also be wrapped with t'SomeBV'. Crash if the
-- bitwidths do not match.
ternSomeBVR1 ::
  (forall n. (KnownNat n, 1 <= n) => Num (bv n)) =>
  (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n -> bv n) ->
  SomeBV bv ->
  SomeBV bv ->
  SomeBV bv ->
  SomeBV bv
ternSomeBVR1 :: forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv
ternSomeBVR1 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 -> bv n -> SomeBV bv)
-> SomeBV bv -> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> SomeBV bv -> r
ternSomeBV (\bv n
a bv n
b bv n
c -> 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 -> bv n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> bv n -> bv n
f bv n
a bv n
b bv n
c)
{-# INLINE ternSomeBVR1 #-}

-- | Lift a binary operation on sized bitvectors that returns anything wrapped
-- with 'ExceptT' to t'SomeBV'. If the bitwidths do not match, throw an
-- 'BitwidthMismatch' error to the monadic context.
binSomeBVSafe ::
  ( MonadError (Either SomeBVException e) m,
    TryMerge m,
    Mergeable e,
    Mergeable r,
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  (forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) ->
  (Integer -> Integer -> ExceptT (Either SomeBVException e) m r) ->
  SomeBV bv ->
  SomeBV bv ->
  m r
binSomeBVSafe :: forall e (m :: * -> *) r (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 Mergeable r,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m r)
-> (Integer -> Integer -> ExceptT (Either SomeBVException 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 Integer -> Integer -> ExceptT (Either SomeBVException e) m r
_ (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 ->
      m r -> m r
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ ExceptT e m r -> m (Either e r)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (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) m (Either e r) -> (Either e r -> m r) -> m r
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (e -> m r) -> (r -> m r) -> Either e r -> m r
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Either SomeBVException e -> m r
forall a. Either SomeBVException e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e -> m r)
-> (e -> Either SomeBVException e) -> e -> m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Either SomeBVException e
forall a b. b -> Either a b
Right) r -> m r
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    Maybe (n :~: n)
Nothing -> m r -> m r
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e -> m r
forall a. Either SomeBVException e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e -> m r)
-> Either SomeBVException e -> m r
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left SomeBVException
BitwidthMismatch
binSomeBVSafe forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m r
_ Integer -> Integer -> ExceptT (Either SomeBVException e) m r
g (SomeBVLit Integer
l) (SomeBVLit Integer
r) =
  m r -> m r
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ ExceptT (Either SomeBVException e) m r
-> m (Either (Either SomeBVException e) r)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (Integer -> Integer -> ExceptT (Either SomeBVException e) m r
g Integer
l Integer
r) m (Either (Either SomeBVException e) r)
-> (Either (Either SomeBVException e) r -> m r) -> m r
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Either SomeBVException e -> m r)
-> (r -> m r) -> Either (Either SomeBVException e) r -> m r
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Either SomeBVException e -> m r
forall a. Either SomeBVException e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError r -> m r
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
binSomeBVSafe forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m r
f Integer -> Integer -> ExceptT (Either SomeBVException e) m r
g SomeBV bv
l SomeBV bv
r =
  case Text
-> (SomeBV bv, SomeBV bv)
-> Either SomeBVException (SomeBV bv, SomeBV bv)
forall a. AssignBitWidth a => Text -> a -> Either SomeBVException a
assignBitWidth Text
"binSomeBVSafe" (SomeBV bv
l, SomeBV bv
r) of
    Right (SomeBV bv
l', SomeBV bv
r') -> (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m r)
-> (Integer -> Integer -> ExceptT (Either SomeBVException e) m r)
-> SomeBV bv
-> SomeBV bv
-> m r
forall e (m :: * -> *) r (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 Mergeable r,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m r)
-> (Integer -> Integer -> ExceptT (Either SomeBVException e) m r)
-> SomeBV bv
-> SomeBV bv
-> m r
binSomeBVSafe bv n -> bv n -> ExceptT e m r
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m r
f Integer -> Integer -> ExceptT (Either SomeBVException e) m r
g SomeBV bv
l' SomeBV bv
r'
    Left SomeBVException
e -> m r -> m r
forall (m :: * -> *) a. (TryMerge m, Mergeable a) => m a -> m a
tryMerge (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ Either SomeBVException e -> m r
forall a. Either SomeBVException e -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Either SomeBVException e -> m r)
-> Either SomeBVException e -> m r
forall a b. (a -> b) -> a -> b
$ SomeBVException -> Either SomeBVException e
forall a b. a -> Either a b
Left SomeBVException
e
{-# INLINE binSomeBVSafe #-}

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

-- | Lift a binary operation on sized bitvectors that returns two bitvectors
-- wrapped with 'ExceptT' to t'SomeBV'. The results will also be wrapped with
-- t'SomeBV'.
--
-- If the bitwidths do not match, throw an 'BitwidthMismatch' error to the
-- monadic context.
binSomeBVSafeR2 ::
  ( MonadError (Either SomeBVException e) m,
    TryMerge m,
    Mergeable e,
    forall n. (KnownNat n, 1 <= n) => Mergeable (bv n),
    forall n. (KnownNat n, 1 <= n) => Num (bv n)
  ) =>
  ( forall n.
    (KnownNat n, 1 <= n) =>
    bv n ->
    bv n ->
    ExceptT e m (bv n, bv n)
  ) ->
  ( Integer ->
    Integer ->
    ExceptT (Either SomeBVException e) m (Integer, Integer)
  ) ->
  SomeBV bv ->
  SomeBV bv ->
  m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2 :: forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n),
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (bv n, bv n))
-> (Integer
    -> Integer
    -> ExceptT (Either SomeBVException e) m (Integer, Integer))
-> 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 Integer
-> Integer
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
g =
  (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m (SomeBV bv, SomeBV bv))
-> (Integer
    -> Integer
    -> ExceptT (Either SomeBVException e) m (SomeBV bv, SomeBV bv))
-> SomeBV bv
-> SomeBV bv
-> m (SomeBV bv, SomeBV bv)
forall e (m :: * -> *) r (bv :: Nat -> *).
(MonadError (Either SomeBVException e) m, TryMerge m, Mergeable e,
 Mergeable r,
 forall (n :: Nat). (KnownNat n, 1 <= n) => Num (bv n)) =>
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 bv n -> bv n -> ExceptT e m r)
-> (Integer -> Integer -> ExceptT (Either SomeBVException 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)
    (\Integer
l Integer
r -> ((Integer, Integer) -> (SomeBV bv, SomeBV bv))
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
-> ExceptT (Either SomeBVException 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 ((Integer -> SomeBV bv)
-> (Integer -> SomeBV bv)
-> (Integer, Integer)
-> (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 Integer -> SomeBV bv
forall (bv :: Nat -> *). Integer -> SomeBV bv
SomeBVLit Integer -> SomeBV bv
forall (bv :: Nat -> *). Integer -> SomeBV bv
SomeBVLit) (ExceptT (Either SomeBVException e) m (Integer, Integer)
 -> ExceptT (Either SomeBVException e) m (SomeBV bv, SomeBV bv))
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
-> ExceptT (Either SomeBVException e) m (SomeBV bv, SomeBV bv)
forall a b. (a -> b) -> a -> b
$ Integer
-> Integer
-> ExceptT (Either SomeBVException e) m (Integer, Integer)
g Integer
l Integer
r)
{-# INLINE binSomeBVSafeR2 #-}