{-# 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
( SomeBV (..),
SomeBVException (..),
unsafeSomeBV,
conBV,
conBVView,
pattern ConBV,
symBV,
ssymBV,
isymBV,
arbitraryBV,
pattern SomeIntN,
type SomeIntN,
pattern SomeWordN,
type SomeWordN,
pattern SomeSymIntN,
type SomeSymIntN,
pattern SomeSymWordN,
type SomeSymWordN,
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)
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"
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)
)
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),
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 #-}
type SomeIntN = SomeBV IntN
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 SomeWordN = SomeBV WordN
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 SomeSymIntN = SomeBV SymIntN
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 SomeSymWordN = SomeBV SymWordN
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
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))
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
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 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
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
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
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
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
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}