-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Core.Sized
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Type-level sized bit-vectors. Thanks to Ben Blaxill for providing an
-- initial implementation of this idea.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Core.Sized (
        -- * Type-sized unsigned bit-vectors
          SWord, WordN, sWord, sWord_, sWords
        -- * Type-sized signed bit-vectors
        , SInt, IntN, sInt, sInt_, sInts
        -- * Bit-vector operations
        , bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake
       ) where

import Data.Bits
import Data.Maybe (fromJust)
import Data.Proxy (Proxy(..))

import GHC.TypeLits

import Data.SBV.Core.Data
import Data.SBV.Core.Kind
import Data.SBV.Core.Model
import Data.SBV.Core.Operations
import Data.SBV.Core.Symbolic

import Data.SBV.SMT.SMT

-- | An unsigned bit-vector carrying its size info
newtype WordN (n :: Nat) = WordN Integer deriving (WordN n -> WordN n -> Bool
forall (n :: Nat). WordN n -> WordN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WordN n -> WordN n -> Bool
$c/= :: forall (n :: Nat). WordN n -> WordN n -> Bool
== :: WordN n -> WordN n -> Bool
$c== :: forall (n :: Nat). WordN n -> WordN n -> Bool
Eq, WordN n -> WordN n -> Bool
WordN n -> WordN n -> Ordering
WordN n -> WordN n -> WordN n
forall (n :: Nat). Eq (WordN n)
forall (n :: Nat). WordN n -> WordN n -> Bool
forall (n :: Nat). WordN n -> WordN n -> Ordering
forall (n :: Nat). WordN n -> WordN n -> WordN n
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
min :: WordN n -> WordN n -> WordN n
$cmin :: forall (n :: Nat). WordN n -> WordN n -> WordN n
max :: WordN n -> WordN n -> WordN n
$cmax :: forall (n :: Nat). WordN n -> WordN n -> WordN n
>= :: WordN n -> WordN n -> Bool
$c>= :: forall (n :: Nat). WordN n -> WordN n -> Bool
> :: WordN n -> WordN n -> Bool
$c> :: forall (n :: Nat). WordN n -> WordN n -> Bool
<= :: WordN n -> WordN n -> Bool
$c<= :: forall (n :: Nat). WordN n -> WordN n -> Bool
< :: WordN n -> WordN n -> Bool
$c< :: forall (n :: Nat). WordN n -> WordN n -> Bool
compare :: WordN n -> WordN n -> Ordering
$ccompare :: forall (n :: Nat). WordN n -> WordN n -> Ordering
Ord)

-- | A symbolic unsigned bit-vector carrying its size info
type SWord (n :: Nat) = SBV (WordN n)

-- | Show instance for 'WordN'
instance Show (WordN n) where
  show :: WordN n -> String
show (WordN Integer
v) = forall a. Show a => a -> String
show Integer
v

-- | 'WordN' has a kind
instance (KnownNat n, BVIsNonZero n) => HasKind (WordN n) where
  kindOf :: WordN n -> Kind
kindOf WordN n
_ = Bool -> Int -> Kind
KBounded Bool
False (forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n))

-- | 'SymVal' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SymVal (WordN n) where
   literal :: WordN n -> SBV (WordN n)
literal  WordN n
x = forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (forall a. HasKind a => a -> Kind
kindOf WordN n
x) WordN n
x
   mkSymVal :: forall (m :: * -> *).
MonadSymbolic m =>
VarContext -> Maybe String -> m (SBV (WordN n))
mkSymVal   = forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (forall a. HasKind a => a -> Kind
kindOf (forall a. HasCallStack => a
undefined :: WordN n))
   fromCV :: CV -> WordN n
fromCV     = forall a. Integral a => CV -> a
genFromCV

-- | A signed bit-vector carrying its size info
newtype IntN (n :: Nat) = IntN Integer deriving (IntN n -> IntN n -> Bool
forall (n :: Nat). IntN n -> IntN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: IntN n -> IntN n -> Bool
$c/= :: forall (n :: Nat). IntN n -> IntN n -> Bool
== :: IntN n -> IntN n -> Bool
$c== :: forall (n :: Nat). IntN n -> IntN n -> Bool
Eq, IntN n -> IntN n -> Bool
IntN n -> IntN n -> Ordering
IntN n -> IntN n -> IntN n
forall (n :: Nat). Eq (IntN n)
forall (n :: Nat). IntN n -> IntN n -> Bool
forall (n :: Nat). IntN n -> IntN n -> Ordering
forall (n :: Nat). IntN n -> IntN n -> IntN n
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
min :: IntN n -> IntN n -> IntN n
$cmin :: forall (n :: Nat). IntN n -> IntN n -> IntN n
max :: IntN n -> IntN n -> IntN n
$cmax :: forall (n :: Nat). IntN n -> IntN n -> IntN n
>= :: IntN n -> IntN n -> Bool
$c>= :: forall (n :: Nat). IntN n -> IntN n -> Bool
> :: IntN n -> IntN n -> Bool
$c> :: forall (n :: Nat). IntN n -> IntN n -> Bool
<= :: IntN n -> IntN n -> Bool
$c<= :: forall (n :: Nat). IntN n -> IntN n -> Bool
< :: IntN n -> IntN n -> Bool
$c< :: forall (n :: Nat). IntN n -> IntN n -> Bool
compare :: IntN n -> IntN n -> Ordering
$ccompare :: forall (n :: Nat). IntN n -> IntN n -> Ordering
Ord)

-- | A symbolic signed bit-vector carrying its size info
type SInt (n :: Nat) = SBV (IntN n)

-- | Show instance for 'IntN'
instance Show (IntN n) where
  show :: IntN n -> String
show (IntN Integer
v) = forall a. Show a => a -> String
show Integer
v

-- | 'IntN' has a kind
instance (KnownNat n, BVIsNonZero n) => HasKind (IntN n) where
  kindOf :: IntN n -> Kind
kindOf IntN n
_ = Bool -> Int -> Kind
KBounded Bool
True (forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n))

-- | 'SymVal' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SymVal (IntN n) where
   literal :: IntN n -> SBV (IntN n)
literal  IntN n
x = forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (forall a. HasKind a => a -> Kind
kindOf IntN n
x) IntN n
x
   mkSymVal :: forall (m :: * -> *).
MonadSymbolic m =>
VarContext -> Maybe String -> m (SBV (IntN n))
mkSymVal   = forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (forall a. HasKind a => a -> Kind
kindOf (forall a. HasCallStack => a
undefined :: IntN n))
   fromCV :: CV -> IntN n
fromCV     = forall a. Integral a => CV -> a
genFromCV

-- Lift a unary operation via SVal
lift1 :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal) -> bv n -> bv n
lift1 :: forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
nm SVal -> SVal
op bv n
x = SVal -> bv n
uc forall a b. (a -> b) -> a -> b
$ SVal -> SVal
op (bv n -> SVal
c bv n
x)
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> CV
normCV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> bv n
uc (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
v)))) = forall a. Num a => Integer -> a
fromInteger Integer
v
        uc SVal
r                                   = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
nm forall a. [a] -> [a] -> [a]
++ String
" over " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Kind
k, bv n
x, SVal
r)

-- Lift a binary operation via SVal
lift2 :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 :: forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
nm SVal -> SVal -> SVal
op bv n
x bv n
y = SVal -> bv n
uc forall a b. (a -> b) -> a -> b
$ bv n -> SVal
c bv n
x SVal -> SVal -> SVal
`op` bv n -> SVal
c bv n
y
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> CV
normCV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> bv n
uc (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
v)))) = forall a. Num a => Integer -> a
fromInteger Integer
v
        uc SVal
r                                   = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
nm forall a. [a] -> [a] -> [a]
++ String
" over " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Kind
k, bv n
x, bv n
y, SVal
r)

-- Lift a binary operation via SVal where second argument is an Int
lift2I :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I :: forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I String
nm SVal -> Int -> SVal
op bv n
x Int
i = SVal -> bv n
uc forall a b. (a -> b) -> a -> b
$ bv n -> SVal
c bv n
x SVal -> Int -> SVal
`op` Int
i
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> CV
normCV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> bv n
uc (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
v)))) = forall a. Num a => Integer -> a
fromInteger Integer
v
        uc SVal
r                                   = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
nm forall a. [a] -> [a] -> [a]
++ String
" over " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Kind
k, bv n
x, Int
i, SVal
r)

-- Lift a binary operation via SVal where second argument is an Int and returning a Bool
lift2IB :: (KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n), Show (bv n)) => String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
lift2IB :: forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
lift2IB String
nm SVal -> Int -> SVal
op bv n
x Int
i = SVal -> Bool
uc forall a b. (a -> b) -> a -> b
$ bv n -> SVal
c bv n
x SVal -> Int -> SVal
`op` Int
i
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> CV
normCV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> Bool
uc (SVal Kind
_ (Left CV
v)) = CV -> Bool
cvToBool CV
v
        uc SVal
r                 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
nm forall a. [a] -> [a] -> [a]
++ String
" over " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Kind
k, bv n
x, Int
i, SVal
r)

-- | 'Bounded' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Bounded (WordN n) where
   minBound :: WordN n
minBound = forall (n :: Nat). Integer -> WordN n
WordN Integer
0
   maxBound :: WordN n
maxBound = let sz :: Int
sz = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n) in forall (n :: Nat). Integer -> WordN n
WordN forall a b. (a -> b) -> a -> b
$ Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz forall a. Num a => a -> a -> a
- Integer
1

-- | 'Bounded' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Bounded (IntN n) where
   minBound :: IntN n
minBound = let sz1 :: Int
sz1 = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n) forall a. Num a => a -> a -> a
- Int
1 in forall (n :: Nat). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ - (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz1)
   maxBound :: IntN n
maxBound = let sz1 :: Int
sz1 = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n) forall a. Num a => a -> a -> a
- Int
1 in forall (n :: Nat). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz1 forall a. Num a => a -> a -> a
- Integer
1

-- | 'Num' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Num (WordN n) where
   + :: WordN n -> WordN n -> WordN n
(+)         = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(+)"    SVal -> SVal -> SVal
svPlus
   (-)         = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(*)"    SVal -> SVal -> SVal
svMinus
   * :: WordN n -> WordN n -> WordN n
(*)         = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(*)"    SVal -> SVal -> SVal
svTimes
   negate :: WordN n -> WordN n
negate      = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
"signum" SVal -> SVal
svUNeg
   abs :: WordN n -> WordN n
abs         = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
"abs"    SVal -> SVal
svAbs
   signum :: WordN n -> WordN n
signum      = forall (n :: Nat). Integer -> WordN n
WordN forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
signum   forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
   fromInteger :: Integer -> WordN n
fromInteger = forall (n :: Nat). Integer -> WordN n
WordN forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> Maybe Integer
svAsInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Integer -> SVal
svInteger (forall a. HasKind a => a -> Kind
kindOf (forall a. HasCallStack => a
undefined :: WordN n))

-- | 'Num' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Num (IntN n) where
   + :: IntN n -> IntN n -> IntN n
(+)         = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(+)"    SVal -> SVal -> SVal
svPlus
   (-)         = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(*)"    SVal -> SVal -> SVal
svMinus
   * :: IntN n -> IntN n -> IntN n
(*)         = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2 String
"(*)"    SVal -> SVal -> SVal
svTimes
   negate :: IntN n -> IntN n
negate      = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
"signum" SVal -> SVal
svUNeg
   abs :: IntN n -> IntN n
abs         = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
"abs"    SVal -> SVal
svAbs
   signum :: IntN n -> IntN n
signum      = forall (n :: Nat). Integer -> IntN n
IntN forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Num a => a -> a
signum   forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
   fromInteger :: Integer -> IntN n
fromInteger = forall (n :: Nat). Integer -> IntN n
IntN forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> Maybe Integer
svAsInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Integer -> SVal
svInteger (forall a. HasKind a => a -> Kind
kindOf (forall a. HasCallStack => a
undefined :: IntN n))

-- | 'Enum' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Enum (WordN n) where
   toEnum :: Int -> WordN n
toEnum   = forall a. Num a => Integer -> a
fromInteger  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
   fromEnum :: WordN n -> Int
fromEnum = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

-- | 'Enum' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Enum (IntN n) where
   toEnum :: Int -> IntN n
toEnum   = forall a. Num a => Integer -> a
fromInteger  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
   fromEnum :: IntN n -> Int
fromEnum = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

-- | 'Real' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Real (WordN n) where
   toRational :: WordN n -> Rational
toRational (WordN Integer
x) = forall a. Real a => a -> Rational
toRational Integer
x

-- | 'Real' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Real (IntN n) where
   toRational :: IntN n -> Rational
toRational (IntN Integer
x) = forall a. Real a => a -> Rational
toRational Integer
x

-- | 'Integral' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Integral (WordN n) where
   toInteger :: WordN n -> Integer
toInteger (WordN Integer
x)           = Integer
x
   quotRem :: WordN n -> WordN n -> (WordN n, WordN n)
quotRem   (WordN Integer
x) (WordN Integer
y) = let (Integer
q, Integer
r) = forall a. Integral a => a -> a -> (a, a)
quotRem Integer
x Integer
y in (forall (n :: Nat). Integer -> WordN n
WordN Integer
q, forall (n :: Nat). Integer -> WordN n
WordN Integer
r)

-- | 'Integral' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Integral (IntN n) where
   toInteger :: IntN n -> Integer
toInteger (IntN Integer
x)          = Integer
x
   quotRem :: IntN n -> IntN n -> (IntN n, IntN n)
quotRem   (IntN Integer
x) (IntN Integer
y) = let (Integer
q, Integer
r) = forall a. Integral a => a -> a -> (a, a)
quotRem Integer
x Integer
y in (forall (n :: Nat). Integer -> IntN n
IntN Integer
q, forall (n :: Nat). Integer -> IntN n
IntN Integer
r)

--  'Bits' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => Bits (WordN n) where
   .&. :: WordN n -> WordN n -> WordN n
(.&.)        = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"(.&.)"      SVal -> SVal -> SVal
svAnd
   .|. :: WordN n -> WordN n -> WordN n
(.|.)        = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"(.|.)"      SVal -> SVal -> SVal
svOr
   xor :: WordN n -> WordN n -> WordN n
xor          = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"xor"        SVal -> SVal -> SVal
svXOr
   complement :: WordN n -> WordN n
complement   = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1   String
"complement" SVal -> SVal
svNot
   shiftL :: WordN n -> Int -> WordN n
shiftL       = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"shiftL"     SVal -> Int -> SVal
svShl
   shiftR :: WordN n -> Int -> WordN n
shiftR       = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"shiftR"     SVal -> Int -> SVal
svShr
   rotateL :: WordN n -> Int -> WordN n
rotateL      = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"rotateL"    SVal -> Int -> SVal
svRol
   rotateR :: WordN n -> Int -> WordN n
rotateR      = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"rotateR"    SVal -> Int -> SVal
svRor
   testBit :: WordN n -> Int -> Bool
testBit      = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
lift2IB String
"svTestBit"  SVal -> Int -> SVal
svTestBit
   bitSizeMaybe :: WordN n -> Maybe Int
bitSizeMaybe = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const (forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n))
   bitSize :: WordN n -> Int
bitSize WordN n
_    = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n)
   isSigned :: WordN n -> Bool
isSigned     = forall a. HasKind a => a -> Bool
hasSign forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasKind a => a -> Kind
kindOf
   bit :: Int -> WordN n
bit Int
i        = WordN n
1 forall a. Bits a => a -> Int -> a
`shiftL` Int
i
   popCount :: WordN n -> Int
popCount     = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bits a => a -> Int
popCount forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

--  'Bits' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => Bits (IntN n) where
   .&. :: IntN n -> IntN n -> IntN n
(.&.)        = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"(.&.)"      SVal -> SVal -> SVal
svAnd
   .|. :: IntN n -> IntN n -> IntN n
(.|.)        = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"(.|.)"      SVal -> SVal -> SVal
svOr
   xor :: IntN n -> IntN n -> IntN n
xor          = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal -> SVal) -> bv n -> bv n -> bv n
lift2   String
"xor"        SVal -> SVal -> SVal
svXOr
   complement :: IntN n -> IntN n
complement   = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> SVal) -> bv n -> bv n
lift1   String
"complement" SVal -> SVal
svNot
   shiftL :: IntN n -> Int -> IntN n
shiftL       = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"shiftL"     SVal -> Int -> SVal
svShl
   shiftR :: IntN n -> Int -> IntN n
shiftR       = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"shiftR"     SVal -> Int -> SVal
svShr
   rotateL :: IntN n -> Int -> IntN n
rotateL      = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"rotateL"    SVal -> Int -> SVal
svRol
   rotateR :: IntN n -> Int -> IntN n
rotateR      = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> bv n
lift2I  String
"rotateR"    SVal -> Int -> SVal
svRor
   testBit :: IntN n -> Int -> Bool
testBit      = forall (n :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, HasKind (bv n), Integral (bv n),
 Show (bv n)) =>
String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
lift2IB String
"svTestBit"  SVal -> Int -> SVal
svTestBit
   bitSizeMaybe :: IntN n -> Maybe Int
bitSizeMaybe = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> a
const (forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n))
   bitSize :: IntN n -> Int
bitSize IntN n
_    = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n)
   isSigned :: IntN n -> Bool
isSigned     = forall a. HasKind a => a -> Bool
hasSign forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasKind a => a -> Kind
kindOf
   bit :: Int -> IntN n
bit Int
i        = IntN n
1 forall a. Bits a => a -> Int -> a
`shiftL` Int
i
   popCount :: IntN n -> Int
popCount     = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Bits a => a -> Int
popCount forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

-- | 'SIntegral' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SIntegral (WordN n)

-- | 'SIntegral' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SIntegral (IntN n)

-- | 'SDivisible' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SDivisible (WordN n) where
  sQuotRem :: WordN n -> WordN n -> (WordN n, WordN n)
sQuotRem WordN n
x WordN n
0 = (WordN n
0, WordN n
x)
  sQuotRem WordN n
x WordN n
y = WordN n
x forall a. Integral a => a -> a -> (a, a)
`quotRem` WordN n
y
  sDivMod :: WordN n -> WordN n -> (WordN n, WordN n)
sDivMod  WordN n
x WordN n
0 = (WordN n
0, WordN n
x)
  sDivMod  WordN n
x WordN n
y = WordN n
x forall a. Integral a => a -> a -> (a, a)
`divMod` WordN n
y

-- | 'SDivisible' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SDivisible (IntN n) where
  sQuotRem :: IntN n -> IntN n -> (IntN n, IntN n)
sQuotRem IntN n
x IntN n
0 = (IntN n
0, IntN n
x)
  sQuotRem IntN n
x IntN n
y = IntN n
x forall a. Integral a => a -> a -> (a, a)
`quotRem` IntN n
y
  sDivMod :: IntN n -> IntN n -> (IntN n, IntN n)
sDivMod  IntN n
x IntN n
0 = (IntN n
0, IntN n
x)
  sDivMod  IntN n
x IntN n
y = IntN n
x forall a. Integral a => a -> a -> (a, a)
`divMod` IntN n
y

-- | 'SDivisible' instance for 'SWord'
instance (KnownNat n, BVIsNonZero n) => SDivisible (SWord n) where
  sQuotRem :: SWord n -> SWord n -> (SWord n, SWord n)
sQuotRem = forall a. (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
liftQRem
  sDivMod :: SWord n -> SWord n -> (SWord n, SWord n)
sDivMod  = forall a.
(Ord a, SymVal a, Num a, SDivisible (SBV a)) =>
SBV a -> SBV a -> (SBV a, SBV a)
liftDMod

-- | 'SDivisible' instance for 'SInt'
instance (KnownNat n, BVIsNonZero n) => SDivisible (SInt n) where
  sQuotRem :: SInt n -> SInt n -> (SInt n, SInt n)
sQuotRem = forall a. (Eq a, SymVal a) => SBV a -> SBV a -> (SBV a, SBV a)
liftQRem
  sDivMod :: SInt n -> SInt n -> (SInt n, SInt n)
sDivMod  = forall a.
(Ord a, SymVal a, Num a, SDivisible (SBV a)) =>
SBV a -> SBV a -> (SBV a, SBV a)
liftDMod

-- | 'SFiniteBits' instance for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SFiniteBits (WordN n) where
   sFiniteBitSize :: SBV (WordN n) -> Int
sFiniteBitSize SBV (WordN n)
_ = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n)

-- | 'SFiniteBits' instance for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SFiniteBits (IntN n) where
   sFiniteBitSize :: SBV (IntN n) -> Int
sFiniteBitSize SBV (IntN n)
_ = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n)

-- | Constructing models for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SatModel (WordN n) where
  parseCVs :: [CV] -> Maybe (WordN n, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (forall a. HasKind a => a -> Kind
kindOf (forall a. HasCallStack => a
undefined :: WordN n))

-- | Constructing models for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SatModel (IntN n) where
  parseCVs :: [CV] -> Maybe (IntN n, [CV])
parseCVs = forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (forall a. HasKind a => a -> Kind
kindOf (forall a. HasCallStack => a
undefined :: IntN n))

-- | Optimizing 'WordN'
instance (KnownNat n, BVIsNonZero n) => Metric (WordN n)

-- | Optimizing 'IntN'
instance (KnownNat n, BVIsNonZero n) => Metric (IntN n) where
  type MetricSpace (IntN n) = WordN n
  toMetricSpace :: SBV (IntN n) -> SBV (MetricSpace (IntN n))
toMetricSpace    SBV (IntN n)
x        = forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV (IntN n)
x forall a. Num a => a -> a -> a
+ SBV (WordN n)
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n) forall a. Num a => a -> a -> a
- Int
1)
  fromMetricSpace :: SBV (MetricSpace (IntN n)) -> SBV (IntN n)
fromMetricSpace  SBV (MetricSpace (IntN n))
x        = forall a b.
(Integral a, HasKind a, Num a, SymVal a, HasKind b, Num b,
 SymVal b) =>
SBV a -> SBV b
sFromIntegral SBV (MetricSpace (IntN n))
x forall a. Num a => a -> a -> a
- SBV (IntN n)
2 forall a b. (Num a, Integral b) => a -> b -> a
^ (forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n) forall a. Num a => a -> a -> a
- Int
1)

-- | Generalization of 'Data.SBV.sWord'
sWord :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SWord n)
sWord :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
String -> m (SWord n)
sWord = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sWord_'
sWord_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SWord n)
sWord_ :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
m (SWord n)
sWord_ = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sWord64s'
sWords :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SWord n]
sWords :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
[String] -> m [SWord n]
sWords = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Generalization of 'Data.SBV.sInt'
sInt :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => String -> m (SInt n)
sInt :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
String -> m (SInt n)
sInt = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
symbolic

-- | Generalization of 'Data.SBV.sInt_'
sInt_ :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => m (SInt n)
sInt_ :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
m (SInt n)
sInt_ = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
free_

-- | Generalization of 'Data.SBV.sInts'
sInts :: (KnownNat n, BVIsNonZero n) => MonadSymbolic m => [String] -> m [SInt n]
sInts :: forall (n :: Nat) (m :: * -> *).
(KnownNat n, BVIsNonZero n, MonadSymbolic m) =>
[String] -> m [SInt n]
sInts = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
[String] -> m [SBV a]
symbolics

-- | Extract a portion of bits to form a smaller bit-vector.
bvExtract :: forall i j n bv proxy. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                                    , KnownNat i
                                    , KnownNat j
                                    , i + 1 <= n
                                    , j <= i
                                    , BVIsNonZero (i - j + 1)
                                    ) => proxy i                -- ^ @i@: Start position, numbered from @n-1@ to @0@
                                      -> proxy j                -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold
                                      -> SBV (bv n)             -- ^ Input bit vector of size @n@
                                      -> SBV (bv (i - j + 1))   -- ^ Output is of size @i - j + 1@
bvExtract :: forall (i :: Nat) (j :: Nat) (n :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat i, KnownNat j,
 (i + 1) <= n, j <= i, BVIsNonZero ((i - j) + 1)) =>
proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract proxy i
start proxy j
end = forall a. SVal -> SBV a
SBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
i Int
j forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SBV a -> SVal
unSBV
   where i :: Int
i  = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
start)
         j :: Int
j  = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy j
end)

-- | Join two bitvectors.
(#) :: ( KnownNat n, BVIsNonZero n, SymVal (bv n)
       , KnownNat m, BVIsNonZero m, SymVal (bv m)
       ) => SBV (bv n)                     -- ^ First input, of size @n@, becomes the left side
         -> SBV (bv m)                     -- ^ Second input, of size @m@, becomes the right side
         -> SBV (bv (n + m))               -- ^ Concatenation, of size @n+m@
SBV (bv n)
n # :: forall (n :: Nat) (bv :: Nat -> *) (m :: Nat).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m)) =>
SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SBV (bv m)
m = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
svJoin (forall a. SBV a -> SVal
unSBV SBV (bv n)
n) (forall a. SBV a -> SVal
unSBV SBV (bv m)
m)
infixr 5 #

-- | Zero extend a bit-vector.
zeroExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                             , KnownNat m, BVIsNonZero m, SymVal (bv m)
                             , n + 1 <= m
                             , SIntegral   (bv (m - n))
                             , BVIsNonZero (m - n)
                             ) => SBV (bv n)    -- ^ Input, of size @n@
                               -> SBV (bv m)    -- ^ Output, of size @m@. @n < m@ must hold
zeroExtend :: forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SIntegral (bv (m - n)),
 BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
zeroExtend SBV (bv n)
n = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Int -> SVal -> SVal
svZeroExtend Int
i (forall a. SBV a -> SVal
unSBV SBV (bv n)
n)
  where nv :: Int
nv = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n)
        mv :: Int
mv = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @m)
        i :: Int
i  = forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
mv forall a. Num a => a -> a -> a
- Int
nv)

-- | Sign extend a bit-vector.
signExtend :: forall n m bv. ( KnownNat n, BVIsNonZero n, SymVal (bv n)
                             , KnownNat m, BVIsNonZero m, SymVal (bv m)
                             , n + 1 <= m
                             , SFiniteBits (bv n)
                             , SIntegral   (bv (m - n))
                             , BVIsNonZero (m - n)
                             ) => SBV (bv n)  -- ^ Input, of size @n@
                               -> SBV (bv m)  -- ^ Output, of size @m@. @n < m@ must hold
signExtend :: forall (n :: Nat) (m :: Nat) (bv :: Nat -> *).
(KnownNat n, BVIsNonZero n, SymVal (bv n), KnownNat m,
 BVIsNonZero m, SymVal (bv m), (n + 1) <= m, SFiniteBits (bv n),
 SIntegral (bv (m - n)), BVIsNonZero (m - n)) =>
SBV (bv n) -> SBV (bv m)
signExtend SBV (bv n)
n = forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Int -> SVal -> SVal
svSignExtend Int
i (forall a. SBV a -> SVal
unSBV SBV (bv n)
n)
  where nv :: Int
nv = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n)
        mv :: Int
mv = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @m)
        i :: Int
i  = forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
mv forall a. Num a => a -> a -> a
- Int
nv)

-- | Drop bits from the top of a bit-vector.
bvDrop :: forall i n m bv proxy. ( KnownNat n, BVIsNonZero n
                                 , KnownNat i
                                 , i + 1 <= n
                                 , i + m - n <= 0
                                 , BVIsNonZero (n - i)
                                 ) => proxy i                    -- ^ @i@: Number of bits to drop. @i < n@ must hold.
                                   -> SBV (bv n)                 -- ^ Input, of size @n@
                                   -> SBV (bv m)                 -- ^ Output, of size @m@. @m = n - i@ holds.
bvDrop :: forall (i :: Nat) (n :: Nat) (m :: Nat) (bv :: Nat -> *)
       (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownNat i, (i + 1) <= n,
 ((i + m) - n) <= 0, BVIsNonZero (n - i)) =>
proxy i -> SBV (bv n) -> SBV (bv m)
bvDrop proxy i
i = forall a. SVal -> SBV a
SBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
start Int
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SBV a -> SVal
unSBV
  where nv :: Int
nv    = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n)
        start :: Int
start = Int
nv forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
i) forall a. Num a => a -> a -> a
- Int
1

-- | Take bits from the top of a bit-vector.
bvTake :: forall i n bv proxy. ( KnownNat n, BVIsNonZero n
                               , KnownNat i, BVIsNonZero i
                               , i <= n
                               ) => proxy i                  -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold.
                                 -> SBV (bv n)               -- ^ Input, of size @n@
                                 -> SBV (bv i)               -- ^ Output, of size @i@
bvTake :: forall (i :: Nat) (n :: Nat) (bv :: Nat -> *) (proxy :: Nat -> *).
(KnownNat n, BVIsNonZero n, KnownNat i, BVIsNonZero i, i <= n) =>
proxy i -> SBV (bv n) -> SBV (bv i)
bvTake proxy i
i = forall a. SVal -> SBV a
SBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
start Int
end forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. SBV a -> SVal
unSBV
  where nv :: Int
nv    = forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall {k} (t :: k). Proxy t
Proxy @n)
        start :: Int
start = Int
nv forall a. Num a => a -> a -> a
- Int
1
        end :: Int
end   = Int
start forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
i) forall a. Num a => a -> a -> a
+ Int
1