{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskellQuotes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
module Grisette.Internal.SymPrim.SomeBV
( SomeBV (..),
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 (throw)
import Control.Monad.Except (ExceptT, MonadError)
import Data.Bifunctor (Bifunctor (bimap))
import Data.Bits
( Bits
( bit,
bitSize,
bitSizeMaybe,
clearBit,
complement,
complementBit,
isSigned,
popCount,
rotate,
rotateL,
rotateR,
setBit,
shift,
shiftL,
shiftR,
testBit,
unsafeShiftL,
unsafeShiftR,
xor,
zeroBits,
(.&.),
(.|.)
),
FiniteBits (countLeadingZeros, countTrailingZeros, finiteBitSize),
)
import Data.Data (Proxy (Proxy))
import Data.Hashable (Hashable (hashWithSalt))
import Data.Maybe (fromJust)
import Data.Type.Equality (type (:~:) (Refl))
import GHC.TypeNats
( KnownNat,
Nat,
natVal,
sameNat,
type (+),
type (<=),
)
import Grisette.Internal.Core.Control.Monad.UnionM (UnionM)
import Grisette.Internal.Core.Data.Class.BitVector
( BV (bv, bvConcat, bvExt, bvSelect, bvSext, bvZext),
SizedBV
( sizedBVConcat,
sizedBVExt,
sizedBVFromIntegral,
sizedBVSelect,
sizedBVSext,
sizedBVZext
),
)
import Grisette.Internal.Core.Data.Class.EvaluateSym
( EvaluateSym (evaluateSym),
)
import Grisette.Internal.Core.Data.Class.ExtractSymbolics
( ExtractSymbolics (extractSymbolics),
)
import Grisette.Internal.Core.Data.Class.GPretty
( GPretty (gpretty),
)
import Grisette.Internal.Core.Data.Class.GenSym
( GenSym (fresh),
GenSymSimple (simpleFresh),
)
import Grisette.Internal.Core.Data.Class.ITEOp (ITEOp (symIte))
import Grisette.Internal.Core.Data.Class.Mergeable
( Mergeable (rootStrategy),
MergingStrategy (SortedStrategy),
wrapStrategy,
)
import Grisette.Internal.Core.Data.Class.SEq (SEq ((./=), (.==)))
import Grisette.Internal.Core.Data.Class.SOrd
( SOrd (symCompare, (.<), (.<=), (.>), (.>=)),
)
import Grisette.Internal.Core.Data.Class.SafeDivision
( SafeDivision (safeDiv, safeDivMod, safeMod, safeQuot, safeQuotRem, safeRem),
)
import Grisette.Internal.Core.Data.Class.SafeLinearArith
( SafeLinearArith (safeAdd, safeNeg, safeSub),
)
import Grisette.Internal.Core.Data.Class.SafeSymRotate
( SafeSymRotate (safeSymRotateL, safeSymRotateR),
)
import Grisette.Internal.Core.Data.Class.SafeSymShift
( SafeSymShift
( safeSymShiftL,
safeSymShiftR,
safeSymStrictShiftL,
safeSymStrictShiftR
),
)
import Grisette.Internal.Core.Data.Class.SignConversion
( SignConversion (toSigned, toUnsigned),
)
import Grisette.Internal.Core.Data.Class.Solvable
( Solvable (con, conView, isym, ssym, sym),
)
import Grisette.Internal.Core.Data.Class.SubstituteSym
( SubstituteSym (substituteSym),
)
import Grisette.Internal.Core.Data.Class.SymRotate (SymRotate (symRotate, symRotateNegated))
import Grisette.Internal.Core.Data.Class.SymShift (SymShift (symShift, symShiftNegated))
import Grisette.Internal.Core.Data.Class.ToCon (ToCon (toCon))
import Grisette.Internal.Core.Data.Class.ToSym (ToSym (toSym))
import Grisette.Internal.Core.Data.Class.TryMerge (TryMerge)
import Grisette.Internal.Core.Data.Symbol (Identifier, Symbol)
import Grisette.Internal.SymPrim.AllSyms (AllSyms (allSyms, allSymsS))
import Grisette.Internal.SymPrim.BV
( BitwidthMismatch (BitwidthMismatch),
IntN,
WordN,
)
import Grisette.Internal.SymPrim.SymBV
( SymIntN,
SymWordN,
)
import Grisette.Internal.Utils.Parameterized
( KnownProof (KnownProof),
LeqProof (LeqProof),
NatRepr,
SomePositiveNatRepr (SomePositiveNatRepr),
knownAdd,
leqAddPos,
mkPositiveNatRepr,
unsafeKnownProof,
unsafeLeqProof,
)
import Grisette.Lib.Control.Monad.Except (mrgModifyError, mrgThrowError)
import Grisette.Lib.Data.Functor (mrgFmap)
import Language.Haskell.TH.Syntax (Lift (liftTyped))
import Test.QuickCheck (Arbitrary (arbitrary), Gen)
import Unsafe.Coerce (unsafeCoerce)
data SomeBV bv where
SomeBV :: (KnownNat n, 1 <= n) => bv n -> SomeBV bv
instance
(forall n. (KnownNat n, 1 <= n) => Hashable (bv n)) =>
Hashable (SomeBV bv)
where
hashWithSalt :: Int -> SomeBV bv -> Int
hashWithSalt Int
s (SomeBV (bv n
bv :: bv n)) =
Int
s Int -> Nat -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) Int -> bv n -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` bv n
bv
{-# INLINE hashWithSalt #-}
instance
(forall n. (KnownNat n, 1 <= n) => Lift (bv n)) =>
Lift (SomeBV bv)
where
liftTyped :: forall (m :: * -> *). Quote m => SomeBV bv -> Code m (SomeBV bv)
liftTyped (SomeBV bv n
bv) = [||bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n
bv||]
instance
(forall n. (KnownNat n, 1 <= n) => Show (bv n)) =>
Show (SomeBV bv)
where
show :: SomeBV bv -> String
show (SomeBV bv n
bv) = bv n -> String
forall a. Show a => a -> String
show bv n
bv
{-# INLINE show #-}
instance
(forall n. (KnownNat n, 1 <= n) => NFData (bv n)) =>
NFData (SomeBV bv)
where
rnf :: SomeBV bv -> ()
rnf (SomeBV bv n
bv) = bv n -> ()
forall a. NFData a => a -> ()
rnf bv n
bv
{-# INLINE rnf #-}
instance (forall n. (KnownNat n, 1 <= n) => Eq (bv n)) => Eq (SomeBV bv) where
== :: SomeBV bv -> SomeBV bv -> Bool
(==) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Eq a => a -> a -> Bool
(==)
{-# INLINE (==) #-}
/= :: SomeBV bv -> SomeBV bv -> Bool
(/=) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Eq a => a -> a -> Bool
(/=)
{-# INLINE (/=) #-}
instance (forall n. (KnownNat n, 1 <= n) => Ord (bv n)) => Ord (SomeBV bv) where
< :: SomeBV bv -> SomeBV bv -> Bool
(<) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
(<)
{-# INLINE (<) #-}
<= :: SomeBV bv -> SomeBV bv -> Bool
(<=) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
{-# INLINE (<=) #-}
> :: SomeBV bv -> SomeBV bv -> Bool
(>) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
(>)
{-# INLINE (>) #-}
>= :: SomeBV bv -> SomeBV bv -> Bool
(>=) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool)
-> SomeBV bv -> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
{-# INLINE (>=) #-}
max :: SomeBV bv -> SomeBV bv -> SomeBV bv
max = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Ord a => a -> a -> a
max
{-# INLINE max #-}
min :: SomeBV bv -> SomeBV bv -> SomeBV bv
min = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Ord a => a -> a -> a
min
{-# INLINE min #-}
compare :: SomeBV bv -> SomeBV bv -> Ordering
compare = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> Ordering)
-> SomeBV bv -> SomeBV bv -> Ordering
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> Ordering
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> Ordering
forall a. Ord a => a -> a -> Ordering
compare
{-# INLINE compare #-}
instance (forall n. (KnownNat n, 1 <= n) => Num (bv n)) => Num (SomeBV bv) where
+ :: SomeBV bv -> SomeBV bv -> SomeBV bv
(+) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Num a => a -> a -> a
(+)
{-# INLINE (+) #-}
(-) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 (-)
{-# INLINE (-) #-}
* :: SomeBV bv -> SomeBV bv -> SomeBV bv
(*) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Num a => a -> a -> a
(*)
{-# INLINE (*) #-}
negate :: SomeBV bv -> SomeBV bv
negate = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
forall a. Num a => a -> a
negate
{-# INLINE negate #-}
abs :: SomeBV bv -> SomeBV bv
abs = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
forall a. Num a => a -> a
abs
{-# INLINE abs #-}
signum :: SomeBV bv -> SomeBV bv
signum = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
forall a. Num a => a -> a
signum
{-# INLINE signum #-}
fromInteger :: Integer -> SomeBV bv
fromInteger =
String -> Integer -> SomeBV bv
forall a. HasCallStack => String -> a
error (String -> Integer -> SomeBV bv) -> String -> Integer -> SomeBV bv
forall a b. (a -> b) -> a -> b
$
String
"fromInteger is not defined for SomeBV as no bitwidth is known, use "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(bv <bitwidth> <value>) instead"
{-# INLINE fromInteger #-}
instance
(forall n. (KnownNat n, 1 <= n) => Bits (bv n)) =>
Bits (SomeBV bv)
where
.&. :: SomeBV bv -> SomeBV bv -> SomeBV bv
(.&.) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Bits a => a -> a -> a
(.&.)
.|. :: SomeBV bv -> SomeBV bv -> SomeBV bv
(.|.) = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Bits a => a -> a -> a
(.|.)
xor :: SomeBV bv -> SomeBV bv -> SomeBV bv
xor = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Bits a => a -> a -> a
xor
complement :: SomeBV bv -> SomeBV bv
complement = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
forall a. Bits a => a -> a
complement
shift :: SomeBV bv -> Int -> SomeBV bv
shift SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`shift` Int
i) SomeBV bv
s
rotate :: SomeBV bv -> Int -> SomeBV bv
rotate SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`rotate` Int
i) SomeBV bv
s
zeroBits :: SomeBV bv
zeroBits =
String -> SomeBV bv
forall a. HasCallStack => String -> a
error (String -> SomeBV bv) -> String -> SomeBV bv
forall a b. (a -> b) -> a -> b
$
String
"zeroBits is not defined for SomeBV as no bitwidth is known, use "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(bv <bitwidth> 0) or (SomeBV (zeroBits :: bv <bitwidth>)) instead"
bit :: Int -> SomeBV bv
bit =
String -> Int -> SomeBV bv
forall a. HasCallStack => String -> a
error (String -> Int -> SomeBV bv) -> String -> Int -> SomeBV bv
forall a b. (a -> b) -> a -> b
$
String
"bit is not defined for SomeBV as no bitwidth is known, use "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(SomeBV (bit <bit> :: bv <bitwidth>)) instead"
setBit :: SomeBV bv -> Int -> SomeBV bv
setBit SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`setBit` Int
i) SomeBV bv
s
clearBit :: SomeBV bv -> Int -> SomeBV bv
clearBit SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`clearBit` Int
i) SomeBV bv
s
complementBit :: SomeBV bv -> Int -> SomeBV bv
complementBit SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`complementBit` Int
i) SomeBV bv
s
testBit :: SomeBV bv -> Int -> Bool
testBit SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Bool)
-> SomeBV bv -> Bool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV (bv n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i) SomeBV bv
s
bitSizeMaybe :: SomeBV bv -> Maybe Int
bitSizeMaybe = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Maybe Int)
-> SomeBV bv -> Maybe Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Maybe Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Maybe Int
forall a. Bits a => a -> Maybe Int
bitSizeMaybe
bitSize :: SomeBV bv -> Int
bitSize = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> (SomeBV bv -> Maybe Int) -> SomeBV bv -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Maybe Int)
-> SomeBV bv -> Maybe Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Maybe Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Maybe Int
forall a. Bits a => a -> Maybe Int
bitSizeMaybe
isSigned :: SomeBV bv -> Bool
isSigned SomeBV bv
_ = Bool
False
shiftL :: SomeBV bv -> Int -> SomeBV bv
shiftL SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i) SomeBV bv
s
unsafeShiftL :: SomeBV bv -> Int -> SomeBV bv
unsafeShiftL SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
i) SomeBV bv
s
shiftR :: SomeBV bv -> Int -> SomeBV bv
shiftR SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`shiftR` Int
i) SomeBV bv
s
unsafeShiftR :: SomeBV bv -> Int -> SomeBV bv
unsafeShiftR SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`unsafeShiftR` Int
i) SomeBV bv
s
rotateL :: SomeBV bv -> Int -> SomeBV bv
rotateL SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`rotateL` Int
i) SomeBV bv
s
rotateR :: SomeBV bv -> Int -> SomeBV bv
rotateR SomeBV bv
s Int
i = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (bv n -> Int -> bv n
forall a. Bits a => a -> Int -> a
`rotateR` Int
i) SomeBV bv
s
popCount :: SomeBV bv -> Int
popCount = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int
forall a. Bits a => a -> Int
popCount
instance
(forall n. (KnownNat n, 1 <= n) => FiniteBits (bv n)) =>
FiniteBits (SomeBV bv)
where
finiteBitSize :: SomeBV bv -> Int
finiteBitSize = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
{-# INLINE finiteBitSize #-}
countLeadingZeros :: SomeBV bv -> Int
countLeadingZeros = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros
{-# INLINE countLeadingZeros #-}
countTrailingZeros :: SomeBV bv -> Int
countTrailingZeros = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int
forall b. FiniteBits b => b -> Int
countTrailingZeros
{-# INLINE countTrailingZeros #-}
instance
(forall n. (KnownNat n, 1 <= n) => Enum (bv n)) =>
Enum (SomeBV bv)
where
toEnum :: Int -> SomeBV bv
toEnum =
String -> Int -> SomeBV bv
forall a. HasCallStack => String -> a
error (String -> Int -> SomeBV bv) -> String -> Int -> SomeBV bv
forall a b. (a -> b) -> a -> b
$
String
"toEnum is not defined for SomeBV, use "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"(SomeBV (toEnum <value> :: bv <bitwidth>)) instead"
{-# INLINE toEnum #-}
fromEnum :: SomeBV bv -> Int
fromEnum = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int)
-> SomeBV bv -> Int
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Int
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Int
forall a. Enum a => a -> Int
fromEnum
{-# INLINE fromEnum #-}
instance
(forall n. (KnownNat n, 1 <= n) => Real (bv n)) =>
Real (SomeBV bv)
where
toRational :: SomeBV bv -> Rational
toRational = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Rational)
-> SomeBV bv -> Rational
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Rational
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Rational
forall a. Real a => a -> Rational
toRational
{-# INLINE toRational #-}
instance
(forall n. (KnownNat n, 1 <= n) => Integral (bv n)) =>
Integral (SomeBV bv)
where
toInteger :: SomeBV bv -> Integer
toInteger = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Integer)
-> SomeBV bv -> Integer
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> Integer
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> Integer
forall a. Integral a => a -> Integer
toInteger
{-# INLINE toInteger #-}
quot :: SomeBV bv -> SomeBV bv -> SomeBV bv
quot = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Integral a => a -> a -> a
quot
{-# INLINE quot #-}
rem :: SomeBV bv -> SomeBV bv -> SomeBV bv
rem = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Integral a => a -> a -> a
rem
{-# INLINE rem #-}
div :: SomeBV bv -> SomeBV bv -> SomeBV bv
div = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Integral a => a -> a -> a
div
{-# INLINE div #-}
mod :: SomeBV bv -> SomeBV bv -> SomeBV bv
mod = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. Integral a => a -> a -> a
mod
{-# INLINE mod #-}
quotRem :: SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
quotRem = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
forall (bv :: Nat -> *).
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
binSomeBVR2 bv n -> bv n -> (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n)
forall a. Integral a => a -> a -> (a, a)
quotRem
{-# INLINE quotRem #-}
divMod :: SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
divMod = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
forall (bv :: Nat -> *).
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
binSomeBVR2 bv n -> bv n -> (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n)
forall a. Integral a => a -> a -> (a, a)
divMod
{-# INLINE divMod #-}
instance (SizedBV bv) => BV (SomeBV bv) where
bvConcat :: SomeBV bv -> SomeBV bv -> SomeBV bv
bvConcat (SomeBV (bv n
a :: bv l)) (SomeBV (bv n
b :: bv r)) =
case ( Proxy n -> Proxy n -> LeqProof 1 (n + n)
forall (m :: Nat) (n :: Nat) (p :: Nat -> *) (q :: Nat -> *).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r),
forall (m :: Nat) (n :: Nat).
KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd @l @r KnownProof n
forall (n :: Nat). KnownNat n => KnownProof n
KnownProof KnownProof n
forall (n :: Nat). KnownNat n => KnownProof n
KnownProof
) of
(LeqProof 1 (n + n)
LeqProof, KnownProof (n + n)
KnownProof) ->
bv (n + n) -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv (n + n) -> SomeBV bv) -> bv (n + n) -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> bv (n + n)
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat bv n
a bv n
b
{-# INLINE bvConcat #-}
bvZext :: Int -> SomeBV bv -> SomeBV bv
bvZext Int
l (SomeBV (bv n
a :: bv n))
| Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = String -> SomeBV bv
forall a. HasCallStack => String -> a
error String
"bvZext: trying to zero extend a value to a smaller size"
| Bool
otherwise = Proxy n -> SomeBV bv
forall (l :: Nat). Proxy l -> SomeBV bv
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
where
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
res :: forall (l :: Nat). Proxy l -> SomeBV bv
res :: forall (l :: Nat). Proxy l -> SomeBV bv
res Proxy l
p =
case ( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @l (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l),
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @n @l
) of
(KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> bv l -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv l -> SomeBV bv) -> bv l -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Proxy l -> bv n -> bv l
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext Proxy l
p bv n
a
{-# INLINE bvZext #-}
bvSext :: Int -> SomeBV bv -> SomeBV bv
bvSext Int
l (SomeBV (bv n
a :: bv n))
| Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = String -> SomeBV bv
forall a. HasCallStack => String -> a
error String
"bvSext: trying to zero extend a value to a smaller size"
| Bool
otherwise = Proxy n -> SomeBV bv
forall (l :: Nat). Proxy l -> SomeBV bv
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
where
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
res :: forall (l :: Nat). Proxy l -> SomeBV bv
res :: forall (l :: Nat). Proxy l -> SomeBV bv
res Proxy l
p =
case ( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @l (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l),
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @n @l
) of
(KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> bv l -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv l -> SomeBV bv) -> bv l -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Proxy l -> bv n -> bv l
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext Proxy l
p bv n
a
{-# INLINE bvSext #-}
bvExt :: Int -> SomeBV bv -> SomeBV bv
bvExt Int
l (SomeBV (bv n
a :: bv n))
| Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = String -> SomeBV bv
forall a. HasCallStack => String -> a
error String
"bvExt: trying to zero extend a value to a smaller size"
| Bool
otherwise = Proxy n -> SomeBV bv
forall (l :: Nat). Proxy l -> SomeBV bv
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
where
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
res :: forall (l :: Nat). Proxy l -> SomeBV bv
res :: forall (l :: Nat). Proxy l -> SomeBV bv
res Proxy l
p =
case ( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @l (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l),
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @n @l
) of
(KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> bv l -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv l -> SomeBV bv) -> bv l -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Proxy l -> bv n -> bv l
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVExt Proxy l
p bv n
a
{-# INLINE bvExt #-}
bvSelect :: Int -> Int -> SomeBV bv -> SomeBV bv
bvSelect Int
ix Int
w (SomeBV (bv n
a :: bv n))
| Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n =
String -> SomeBV bv
forall a. HasCallStack => String -> a
error (String -> SomeBV bv) -> String -> SomeBV bv
forall a b. (a -> b) -> a -> b
$
String
"bvSelect: trying to select a bitvector outside the bounds of the "
String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"input"
| Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = String -> SomeBV bv
forall a. HasCallStack => String -> a
error String
"bvSelect: trying to select a bitvector of size 0"
| Bool
otherwise = Proxy n -> Proxy n -> SomeBV bv
forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeBV bv
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
where
n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeBV bv
res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeBV bv
res Proxy w
_ Proxy ix
_ =
case ( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @ix (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
ix),
forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @w (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
w),
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @w,
forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(ix + w) @n
) of
(KnownProof ix
KnownProof, KnownProof w
KnownProof, LeqProof 1 w
LeqProof, LeqProof (ix + w) n
LeqProof) ->
bv w -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv w -> SomeBV bv) -> bv w -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ Proxy ix -> Proxy w -> bv n -> bv w
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
(q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
sizedBVSelect (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @ix) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) bv n
a
bv :: forall a. Integral a => Int -> a -> SomeBV bv
bv Int
n a
i = Int
-> (forall {proxy :: Nat -> *} {n :: Nat}.
(KnownNat n, 1 <= n) =>
proxy n -> bv n)
-> SomeBV bv
forall (bv :: Nat -> *).
Int
-> (forall (proxy :: Nat -> *) (n :: Nat).
(KnownNat n, 1 <= n) =>
proxy n -> bv n)
-> SomeBV bv
unsafeSomeBV Int
n ((forall {proxy :: Nat -> *} {n :: Nat}.
(KnownNat n, 1 <= n) =>
proxy n -> bv n)
-> SomeBV bv)
-> (forall {proxy :: Nat -> *} {n :: Nat}.
(KnownNat n, 1 <= n) =>
proxy n -> bv n)
-> SomeBV bv
forall a b. (a -> b) -> a -> b
$ \proxy n
_ -> a -> bv n
forall a (n :: Nat). (Integral a, KnownNat n, 1 <= n) => a -> bv n
forall (bv :: Nat -> *) a (n :: Nat).
(SizedBV bv, Integral a, KnownNat n, 1 <= n) =>
a -> bv n
sizedBVFromIntegral a
i
{-# INLINE bv #-}
instance
(forall n. (KnownNat n, 1 <= n) => EvaluateSym (bv n)) =>
EvaluateSym (SomeBV bv)
where
evaluateSym :: Bool -> Model -> SomeBV bv -> SomeBV bv
evaluateSym Bool
fillDefault Model
model = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (Bool -> Model -> bv n -> bv n
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model)
{-# INLINE evaluateSym #-}
instance
(forall n. (KnownNat n, 1 <= n) => ExtractSymbolics (bv n)) =>
ExtractSymbolics (SomeBV bv)
where
extractSymbolics :: SomeBV bv -> SymbolSet
extractSymbolics = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> SymbolSet)
-> SomeBV bv -> SymbolSet
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> SymbolSet
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics
{-# INLINE extractSymbolics #-}
instance
(forall n. (KnownNat n, 1 <= n) => GPretty (bv n)) =>
GPretty (SomeBV bv)
where
gpretty :: forall ann. SomeBV bv -> Doc ann
gpretty (SomeBV bv n
bv) = bv n -> Doc ann
forall ann. bv n -> Doc ann
forall a ann. GPretty a => a -> Doc ann
gpretty bv n
bv
{-# INLINE gpretty #-}
data CompileTimeNat where
CompileTimeNat :: (KnownNat n, 1 <= n) => Proxy n -> CompileTimeNat
instance Show CompileTimeNat where
show :: CompileTimeNat -> String
show (CompileTimeNat (Proxy n
Proxy :: Proxy n)) = Nat -> String
forall a. Show a => a -> String
show (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
{-# INLINE show #-}
instance Eq CompileTimeNat where
CompileTimeNat (Proxy n
Proxy :: Proxy n) == :: CompileTimeNat -> CompileTimeNat -> Bool
== CompileTimeNat (Proxy n
Proxy :: Proxy m) =
case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) of
Just n :~: n
Refl -> Bool
True
Maybe (n :~: n)
Nothing -> Bool
False
{-# INLINE (==) #-}
instance Ord CompileTimeNat where
compare :: CompileTimeNat -> CompileTimeNat -> Ordering
compare
(CompileTimeNat (Proxy n
Proxy :: Proxy n))
(CompileTimeNat (Proxy n
Proxy :: Proxy m)) =
Nat -> Nat -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m))
{-# INLINE compare #-}
instance
(forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
Mergeable (SomeBV bv)
where
rootStrategy :: MergingStrategy (SomeBV bv)
rootStrategy =
forall idx a.
(Ord idx, Typeable idx, Show idx) =>
(a -> idx) -> (idx -> MergingStrategy a) -> MergingStrategy a
SortedStrategy @CompileTimeNat
(\(SomeBV (bv n
_ :: bv n)) -> Proxy n -> CompileTimeNat
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Proxy n -> CompileTimeNat
CompileTimeNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
( \(CompileTimeNat (Proxy n
_ :: proxy n)) ->
MergingStrategy (bv n)
-> (bv n -> SomeBV bv)
-> (SomeBV bv -> bv n)
-> MergingStrategy (SomeBV bv)
forall a b.
MergingStrategy a -> (a -> b) -> (b -> a) -> MergingStrategy b
wrapStrategy
(forall a. Mergeable a => MergingStrategy a
rootStrategy @(bv n))
bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV
(\(SomeBV bv n
x) -> bv n -> bv n
forall a b. a -> b
unsafeCoerce bv n
x)
)
instance (forall n. (KnownNat n, 1 <= n) => SEq (bv n)) => SEq (SomeBV bv) where
.== :: SomeBV bv -> SomeBV bv -> SymBool
(.==) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SEq a => a -> a -> SymBool
(.==)
{-# INLINE (.==) #-}
./= :: SomeBV bv -> SomeBV bv -> SymBool
(./=) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SEq a => a -> a -> SymBool
(./=)
{-# INLINE (./=) #-}
instance
(forall n. (KnownNat n, 1 <= n) => SOrd (bv n)) =>
SOrd (SomeBV bv)
where
.< :: SomeBV bv -> SomeBV bv -> SymBool
(.<) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SOrd a => a -> a -> SymBool
(.<)
{-# INLINE (.<) #-}
.<= :: SomeBV bv -> SomeBV bv -> SymBool
(.<=) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SOrd a => a -> a -> SymBool
(.<=)
{-# INLINE (.<=) #-}
.> :: SomeBV bv -> SomeBV bv -> SymBool
(.>) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SOrd a => a -> a -> SymBool
(.>)
{-# INLINE (.>) #-}
.>= :: SomeBV bv -> SomeBV bv -> SymBool
(.>=) = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> SymBool)
-> SomeBV bv -> SomeBV bv -> SymBool
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> SymBool
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> SymBool
forall a. SOrd a => a -> a -> SymBool
(.>=)
{-# INLINE (.>=) #-}
symCompare :: SomeBV bv -> SomeBV bv -> UnionM Ordering
symCompare = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> UnionM Ordering)
-> SomeBV bv -> SomeBV bv -> UnionM Ordering
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV bv n -> bv n -> UnionM Ordering
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> UnionM Ordering
forall a. SOrd a => a -> a -> UnionM Ordering
symCompare
{-# INLINE symCompare #-}
instance
(forall n. (KnownNat n, 1 <= n) => SubstituteSym (bv n)) =>
SubstituteSym (SomeBV bv)
where
substituteSym :: forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> SomeBV bv -> SomeBV bv
substituteSym TypedSymbol cb
c sb
s = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 (TypedSymbol cb -> sb -> bv n -> bv n
forall a cb sb.
(SubstituteSym a, LinkedRep cb sb) =>
TypedSymbol cb -> sb -> a -> a
forall cb sb.
LinkedRep cb sb =>
TypedSymbol cb -> sb -> bv n -> bv n
substituteSym TypedSymbol cb
c sb
s)
{-# INLINE substituteSym #-}
instance
( KnownNat n,
1 <= n,
forall m. (KnownNat m, 1 <= m) => GenSym () (bv m),
Mergeable (SomeBV bv)
) =>
GenSym (Proxy n) (SomeBV bv)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
Proxy n -> m (UnionM (SomeBV bv))
fresh Proxy n
_ =
(\(UnionM (bv n)
i :: UnionM (bv n)) -> (bv n -> SomeBV bv) -> UnionM (bv n) -> UnionM (SomeBV bv)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV UnionM (bv n)
i) (UnionM (bv n) -> UnionM (SomeBV bv))
-> m (UnionM (bv n)) -> m (UnionM (SomeBV bv))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m (UnionM (bv n))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *). MonadFresh m => () -> m (UnionM (bv n))
fresh ()
{-# INLINE fresh #-}
instance
( KnownNat n,
1 <= n,
forall m. (KnownNat m, 1 <= m) => GenSymSimple () (bv m),
Mergeable (SomeBV bv)
) =>
GenSymSimple (Proxy n) (SomeBV bv)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => Proxy n -> m (SomeBV bv)
simpleFresh Proxy n
_ = (\(bv n
i :: bv n) -> bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n
i) (bv n -> SomeBV bv) -> m (bv n) -> m (SomeBV bv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> () -> m (bv n)
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => () -> m (bv n)
simpleFresh ()
{-# INLINE simpleFresh #-}
instance
( forall m. (KnownNat m, 1 <= m) => GenSym () (bv m),
Mergeable (SomeBV bv)
) =>
GenSym (SomeBV bv) (SomeBV bv)
where
fresh :: forall (m :: * -> *).
MonadFresh m =>
SomeBV bv -> m (UnionM (SomeBV bv))
fresh (SomeBV (bv n
_ :: bv x)) = Proxy n -> m (UnionM (SomeBV bv))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *).
MonadFresh m =>
Proxy n -> m (UnionM (SomeBV bv))
fresh (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)
{-# INLINE fresh #-}
instance
( forall m. (KnownNat m, 1 <= m) => GenSymSimple () (bv m),
Mergeable (SomeBV bv)
) =>
GenSymSimple (SomeBV bv) (SomeBV bv)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => SomeBV bv -> m (SomeBV bv)
simpleFresh (SomeBV (bv n
_ :: bv x)) = Proxy n -> m (SomeBV bv)
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => Proxy n -> m (SomeBV bv)
simpleFresh (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)
{-# INLINE simpleFresh #-}
instance
( forall n. (KnownNat n, 1 <= n) => GenSym () (bv n),
Mergeable (SomeBV bv)
) =>
GenSym Int (SomeBV bv)
where
fresh :: forall (m :: * -> *). MonadFresh m => Int -> m (UnionM (SomeBV bv))
fresh Int
n
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> m (UnionM (SomeBV bv))
forall a. HasCallStack => String -> a
error String
"fresh: cannot generate a bitvector of non-positive size"
| Bool
otherwise = case Nat -> SomePositiveNatRepr
mkPositiveNatRepr (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) of
SomePositiveNatRepr (NatRepr n
_ :: NatRepr x) -> Proxy n -> m (UnionM (SomeBV bv))
forall spec a (m :: * -> *).
(GenSym spec a, MonadFresh m) =>
spec -> m (UnionM a)
forall (m :: * -> *).
MonadFresh m =>
Proxy n -> m (UnionM (SomeBV bv))
fresh (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)
{-# INLINE fresh #-}
instance
( forall n. (KnownNat n, 1 <= n) => GenSymSimple () (bv n),
Mergeable (SomeBV bv)
) =>
GenSymSimple Int (SomeBV bv)
where
simpleFresh :: forall (m :: * -> *). MonadFresh m => Int -> m (SomeBV bv)
simpleFresh Int
n
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> m (SomeBV bv)
forall a. HasCallStack => String -> a
error String
"fresh: cannot generate a bitvector of non-positive size"
| Bool
otherwise = case Nat -> SomePositiveNatRepr
mkPositiveNatRepr (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) of
SomePositiveNatRepr (NatRepr n
_ :: NatRepr x) -> Proxy n -> m (SomeBV bv)
forall spec a (m :: * -> *).
(GenSymSimple spec a, MonadFresh m) =>
spec -> m a
forall (m :: * -> *). MonadFresh m => Proxy n -> m (SomeBV bv)
simpleFresh (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @x)
{-# INLINE simpleFresh #-}
instance
( forall n. (KnownNat n, 1 <= n) => SignConversion (ubv n) (sbv n),
SignConversion (ubv 1) (sbv 1)
) =>
SignConversion (SomeBV ubv) (SomeBV sbv)
where
toSigned :: SomeBV ubv -> SomeBV sbv
toSigned (SomeBV (ubv n
n :: ubv n)) = sbv n -> SomeBV sbv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (ubv n -> sbv n
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned ubv n
n :: sbv n)
{-# INLINE toSigned #-}
toUnsigned :: SomeBV sbv -> SomeBV ubv
toUnsigned (SomeBV (sbv n
n :: sbv n)) = ubv n -> SomeBV ubv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (sbv n -> ubv n
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned sbv n
n :: ubv n)
{-# INLINE toUnsigned #-}
instance
(forall n. (KnownNat n, 1 <= n) => ToCon (sbv n) (cbv n)) =>
ToCon (SomeBV sbv) (SomeBV cbv)
where
toCon :: SomeBV sbv -> Maybe (SomeBV cbv)
toCon (SomeBV (sbv n
n :: sbv n)) = cbv n -> SomeBV cbv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (cbv n -> SomeBV cbv) -> Maybe (cbv n) -> Maybe (SomeBV cbv)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (sbv n -> Maybe (cbv n)
forall a b. ToCon a b => a -> Maybe b
toCon sbv n
n :: Maybe (cbv n))
{-# INLINE toCon #-}
instance
(forall n. (KnownNat n, 1 <= n) => ToSym (cbv n) (sbv n)) =>
ToSym (SomeBV cbv) (SomeBV sbv)
where
toSym :: SomeBV cbv -> SomeBV sbv
toSym (SomeBV (cbv n
n :: cbv n)) = sbv n -> SomeBV sbv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (cbv n -> sbv n
forall a b. ToSym a b => a -> b
toSym cbv n
n :: sbv n)
{-# INLINE toSym #-}
instance
( forall n.
(KnownNat n, 1 <= n) =>
SafeDivision e (bv n) (ExceptT e m),
MonadError (Either BitwidthMismatch e) m,
TryMerge m,
Mergeable e
) =>
SafeDivision (Either BitwidthMismatch e) (SomeBV bv) m
where
safeDiv :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeDiv = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
safeDiv @e)
{-# INLINE safeDiv #-}
safeMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeMod = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
safeMod @e)
{-# INLINE safeMod #-}
safeQuot :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeQuot = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
safeQuot @e)
{-# INLINE safeQuot #-}
safeRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeRem = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m a
safeRem @e)
{-# INLINE safeRem #-}
safeDivMod :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
safeDivMod = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m (a, a)
safeDivMod @e)
{-# INLINE safeDivMod #-}
safeQuotRem :: SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
safeQuotRem = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2 (forall e a (m :: * -> *). SafeDivision e a m => a -> a -> m (a, a)
safeQuotRem @e)
{-# INLINE safeQuotRem #-}
instance
( forall n.
(KnownNat n, 1 <= n) =>
SafeLinearArith e (bv n) (ExceptT e m),
MonadError (Either BitwidthMismatch e) m,
TryMerge m,
Mergeable e
) =>
SafeLinearArith (Either BitwidthMismatch e) (SomeBV bv) m
where
safeAdd :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeAdd = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeLinearArith e a m => a -> a -> m a
safeAdd @e)
{-# INLINE safeAdd #-}
safeSub :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSub = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeLinearArith e a m => a -> a -> m a
safeSub @e)
{-# INLINE safeSub #-}
safeNeg :: SomeBV bv -> m (SomeBV bv)
safeNeg = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> m (SomeBV bv))
-> SomeBV bv -> m (SomeBV bv)
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV ((bv n -> SomeBV bv) -> m (bv n) -> m (SomeBV bv)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (m (bv n) -> m (SomeBV bv))
-> (bv n -> m (bv n)) -> bv n -> m (SomeBV bv)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e -> Either BitwidthMismatch e) -> ExceptT e m (bv n) -> m (bv n)
forall e' (m :: * -> *) a e.
(MonadError e' m, TryMerge m, Mergeable a, Mergeable e,
Mergeable e) =>
(e -> e') -> ExceptT e m a -> m a
mrgModifyError e -> Either BitwidthMismatch e
forall a b. b -> Either a b
Right (ExceptT e m (bv n) -> m (bv n))
-> (bv n -> ExceptT e m (bv n)) -> bv n -> m (bv n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e a (m :: * -> *). SafeLinearArith e a m => a -> m a
safeNeg @e)
{-# INLINE safeNeg #-}
instance
(forall n. (KnownNat n, 1 <= n) => SymShift (bv n)) =>
SymShift (SomeBV bv)
where
symShift :: SomeBV bv -> SomeBV bv -> SomeBV bv
symShift = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. SymShift a => a -> a -> a
symShift
{-# INLINE symShift #-}
symShiftNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv
symShiftNegated = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. SymShift a => a -> a -> a
symShiftNegated
{-# INLINE symShiftNegated #-}
instance
(forall n. (KnownNat n, 1 <= n) => SymRotate (bv n)) =>
SymRotate (SomeBV bv)
where
symRotate :: SomeBV bv -> SomeBV bv -> SomeBV bv
symRotate = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. SymRotate a => a -> a -> a
symRotate
{-# INLINE symRotate #-}
symRotateNegated :: SomeBV bv -> SomeBV bv -> SomeBV bv
symRotateNegated = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
forall a. SymRotate a => a -> a -> a
symRotateNegated
{-# INLINE symRotateNegated #-}
instance
( forall n.
(KnownNat n, 1 <= n) =>
SafeSymShift e (bv n) (ExceptT e m),
MonadError (Either BitwidthMismatch e) m,
TryMerge m,
Mergeable e
) =>
SafeSymShift (Either BitwidthMismatch e) (SomeBV bv) m
where
safeSymShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymShiftL = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymShiftL @e)
{-# INLINE safeSymShiftL #-}
safeSymShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymShiftR = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymShiftR @e)
{-# INLINE safeSymShiftR #-}
safeSymStrictShiftL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymStrictShiftL = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymStrictShiftL @e)
{-# INLINE safeSymStrictShiftL #-}
safeSymStrictShiftR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymStrictShiftR = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymShift e a m => a -> a -> m a
safeSymStrictShiftR @e)
{-# INLINE safeSymStrictShiftR #-}
instance
( forall n.
(KnownNat n, 1 <= n) =>
SafeSymRotate e (bv n) (ExceptT e m),
MonadError (Either BitwidthMismatch e) m,
TryMerge m,
Mergeable e
) =>
SafeSymRotate (Either BitwidthMismatch e) (SomeBV bv) m
where
safeSymRotateL :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymRotateL = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymRotate e a m => a -> a -> m a
safeSymRotateL @e)
{-# INLINE safeSymRotateL #-}
safeSymRotateR :: SomeBV bv -> SomeBV bv -> m (SomeBV bv)
safeSymRotateR = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 (forall e a (m :: * -> *). SafeSymRotate e a m => a -> a -> m a
safeSymRotateR @e)
{-# INLINE safeSymRotateR #-}
instance
(forall n. (KnownNat n, 1 <= n) => ITEOp (bv n)) =>
ITEOp (SomeBV bv)
where
symIte :: SymBool -> SomeBV bv -> SomeBV bv -> SomeBV bv
symIte SymBool
cond = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 (SymBool -> bv n -> bv n -> bv n
forall v. ITEOp v => SymBool -> v -> v -> v
symIte SymBool
cond)
instance
(forall n. (KnownNat n, 1 <= n) => AllSyms (bv n)) =>
AllSyms (SomeBV bv)
where
allSyms :: SomeBV bv -> [SomeSym]
allSyms = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> [SomeSym])
-> SomeBV bv -> [SomeSym]
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> [SomeSym]
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym]
allSyms
{-# INLINE allSyms #-}
allSymsS :: SomeBV bv -> [SomeSym] -> [SomeSym]
allSymsS = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> [SomeSym] -> [SomeSym])
-> SomeBV bv -> [SomeSym] -> [SomeSym]
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV bv n -> [SomeSym] -> [SomeSym]
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> [SomeSym] -> [SomeSym]
forall a. AllSyms a => a -> [SomeSym] -> [SomeSym]
allSymsS
{-# INLINE allSymsS #-}
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
conBVView ::
forall cbv bv.
( forall n. (KnownNat n, 1 <= n) => Solvable (cbv n) (bv n),
Solvable (cbv 1) (bv 1)
) =>
SomeBV bv ->
Maybe (SomeBV cbv)
conBVView :: forall (cbv :: Nat -> *) (bv :: Nat -> *).
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
Solvable (cbv n) (bv n),
Solvable (cbv 1) (bv 1)) =>
SomeBV bv -> Maybe (SomeBV cbv)
conBVView (SomeBV (bv n
bv :: bv n)) = case forall c t. Solvable c t => t -> Maybe c
conView @(cbv n) bv n
bv of
Just cbv n
c -> SomeBV cbv -> Maybe (SomeBV cbv)
forall a. a -> Maybe a
Just (SomeBV cbv -> Maybe (SomeBV cbv))
-> SomeBV cbv -> Maybe (SomeBV cbv)
forall a b. (a -> b) -> a -> b
$ cbv n -> SomeBV cbv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV cbv n
c
Maybe (cbv n)
Nothing -> Maybe (SomeBV cbv)
forall a. Maybe a
Nothing
pattern 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) -> SomeBV bv -> r
unarySomeBV :: forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r
f (SomeBV bv n
bv) = bv n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r
f bv n
bv
{-# INLINE unarySomeBV #-}
unarySomeBVR1 ::
(forall n. (KnownNat n, 1 <= n) => bv n -> bv n) -> SomeBV bv -> SomeBV bv
unarySomeBVR1 :: forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n)
-> SomeBV bv -> SomeBV bv
unarySomeBVR1 forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
f = (forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> SomeBV bv)
-> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> r)
-> SomeBV bv -> r
unarySomeBV (bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv n -> SomeBV bv) -> (bv n -> bv n) -> bv n -> SomeBV bv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n
f)
{-# INLINE unarySomeBVR1 #-}
binSomeBV ::
(forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> r) ->
SomeBV bv ->
SomeBV bv ->
r
binSomeBV :: forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r
f (SomeBV (bv n
l :: bv l)) (SomeBV (bv n
r :: bv r)) =
case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> bv n -> bv n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r
f bv n
l bv n
bv n
r
Maybe (n :~: n)
Nothing -> BitwidthMismatch -> r
forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeBV #-}
binSomeBVR1 ::
(forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> bv n) ->
SomeBV bv ->
SomeBV bv ->
SomeBV bv
binSomeBVR1 :: forall (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
binSomeBVR1 forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
f = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> SomeBV bv)
-> SomeBV bv -> SomeBV bv -> SomeBV bv
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV (\bv n
a bv n
b -> bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (bv n -> SomeBV bv) -> bv n -> SomeBV bv
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> bv n
forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> bv n
f bv n
a bv n
b)
{-# INLINE binSomeBVR1 #-}
binSomeBVR2 ::
(forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> (bv n, bv n)) ->
SomeBV bv ->
SomeBV bv ->
(SomeBV bv, SomeBV bv)
binSomeBVR2 :: forall (bv :: Nat -> *).
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
binSomeBVR2 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n)
f = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (SomeBV bv, SomeBV bv))
-> SomeBV bv -> SomeBV bv -> (SomeBV bv, SomeBV bv)
forall (bv :: Nat -> *) r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => bv n -> bv n -> r)
-> SomeBV bv -> SomeBV bv -> r
binSomeBV (\bv n
a bv n
b -> let (bv n
x, bv n
y) = bv n -> bv n -> (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> (bv n, bv n)
f bv n
a bv n
b in (bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n
x, bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n
y))
{-# INLINE binSomeBVR2 #-}
binSomeBVSafe ::
( MonadError (Either BitwidthMismatch e) m,
TryMerge m,
Mergeable e,
Mergeable r
) =>
(forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m r) ->
SomeBV bv ->
SomeBV bv ->
m r
binSomeBVSafe :: forall e (m :: * -> *) r (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
Mergeable r) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m r)
-> SomeBV bv -> SomeBV bv -> m r
binSomeBVSafe forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m r
f (SomeBV (bv n
l :: bv l)) (SomeBV (bv n
r :: bv r)) =
case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
Just n :~: n
Refl -> (e -> Either BitwidthMismatch e) -> ExceptT e m r -> m r
forall e' (m :: * -> *) a e.
(MonadError e' m, TryMerge m, Mergeable a, Mergeable e,
Mergeable e) =>
(e -> e') -> ExceptT e m a -> m a
mrgModifyError e -> Either BitwidthMismatch e
forall a b. b -> Either a b
Right (ExceptT e m r -> m r) -> ExceptT e m r -> m r
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> ExceptT e m r
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m r
f bv n
l bv n
bv n
r
Maybe (n :~: n)
Nothing -> Either BitwidthMismatch e -> m r
forall e (m :: * -> *) a.
(MonadError e m, TryMerge m, Mergeable a) =>
e -> m a
mrgThrowError (Either BitwidthMismatch e -> m r)
-> Either BitwidthMismatch e -> m r
forall a b. (a -> b) -> a -> b
$ BitwidthMismatch -> Either BitwidthMismatch e
forall a b. a -> Either a b
Left BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeBVSafe #-}
binSomeBVSafeR1 ::
( MonadError (Either BitwidthMismatch e) m,
TryMerge m,
Mergeable e,
forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)
) =>
(forall n. (KnownNat n, 1 <= n) => bv n -> bv n -> ExceptT e m (bv n)) ->
SomeBV bv ->
SomeBV bv ->
m (SomeBV bv)
binSomeBVSafeR1 :: forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
binSomeBVSafeR1 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n)
f = (forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (SomeBV bv))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv)
forall e (m :: * -> *) r (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
Mergeable r) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m r)
-> SomeBV bv -> SomeBV bv -> m r
binSomeBVSafe (\bv n
l bv n
r -> (bv n -> SomeBV bv)
-> ExceptT e m (bv n) -> ExceptT e m (SomeBV bv)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV (ExceptT e m (bv n) -> ExceptT e m (SomeBV bv))
-> ExceptT e m (bv n) -> ExceptT e m (SomeBV bv)
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> ExceptT e m (bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n)
f bv n
l bv n
r)
{-# INLINE binSomeBVSafeR1 #-}
binSomeBVSafeR2 ::
( MonadError (Either BitwidthMismatch e) m,
TryMerge m,
Mergeable e,
forall n. (KnownNat n, 1 <= n) => Mergeable (bv n)
) =>
( forall n.
(KnownNat n, 1 <= n) =>
bv n ->
bv n ->
ExceptT e m (bv n, bv n)
) ->
SomeBV bv ->
SomeBV bv ->
m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2 :: forall e (m :: * -> *) (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
forall (n :: Nat). (KnownNat n, 1 <= n) => Mergeable (bv n)) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n, bv n))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
binSomeBVSafeR2 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n, bv n)
f =
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (SomeBV bv, SomeBV bv))
-> SomeBV bv -> SomeBV bv -> m (SomeBV bv, SomeBV bv)
forall e (m :: * -> *) r (bv :: Nat -> *).
(MonadError (Either BitwidthMismatch e) m, TryMerge m, Mergeable e,
Mergeable r) =>
(forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m r)
-> SomeBV bv -> SomeBV bv -> m r
binSomeBVSafe (\bv n
l bv n
r -> ((bv n, bv n) -> (SomeBV bv, SomeBV bv))
-> ExceptT e m (bv n, bv n) -> ExceptT e m (SomeBV bv, SomeBV bv)
forall (f :: * -> *) a b.
(TryMerge f, Mergeable a, Mergeable b, Functor f) =>
(a -> b) -> f a -> f b
mrgFmap ((bv n -> SomeBV bv)
-> (bv n -> SomeBV bv) -> (bv n, bv n) -> (SomeBV bv, SomeBV bv)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV bv n -> SomeBV bv
forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, 1 <= n) =>
bv n -> SomeBV bv
SomeBV) (ExceptT e m (bv n, bv n) -> ExceptT e m (SomeBV bv, SomeBV bv))
-> ExceptT e m (bv n, bv n) -> ExceptT e m (SomeBV bv, SomeBV bv)
forall a b. (a -> b) -> a -> b
$ bv n -> bv n -> ExceptT e m (bv n, bv n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
bv n -> bv n -> ExceptT e m (bv n, bv n)
f bv n
l bv n
r)
{-# INLINE binSomeBVSafeR2 #-}