-----------------------------------------------------------------------------
-- |
-- 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
(WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool) -> Eq (WordN n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
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
Eq, Eq (WordN n)
Eq (WordN n)
-> (WordN n -> WordN n -> Ordering)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> WordN n)
-> (WordN n -> WordN n -> WordN n)
-> Ord (WordN n)
WordN n -> WordN n -> Bool
WordN n -> WordN n -> Ordering
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
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
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
$cp1Ord :: forall (n :: Nat). Eq (WordN n)
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) = Integer -> String
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 (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
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 = Kind -> WordN n -> SBV (WordN n)
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf WordN n
x) WordN n
x
   mkSymVal :: VarContext -> Maybe String -> m (SBV (WordN n))
mkSymVal   = Kind -> VarContext -> Maybe String -> m (SBV (WordN n))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (WordN n
forall a. HasCallStack => a
undefined :: WordN n))
   fromCV :: CV -> WordN n
fromCV     = CV -> WordN n
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
(IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool) -> Eq (IntN n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
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
Eq, Eq (IntN n)
Eq (IntN n)
-> (IntN n -> IntN n -> Ordering)
-> (IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> IntN n)
-> (IntN n -> IntN n -> IntN n)
-> Ord (IntN n)
IntN n -> IntN n -> Bool
IntN n -> IntN n -> Ordering
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
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
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
$cp1Ord :: forall (n :: Nat). Eq (IntN n)
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) = Integer -> String
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 (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
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 = Kind -> IntN n -> SBV (IntN n)
forall a b. Integral a => Kind -> a -> SBV b
genLiteral  (IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf IntN n
x) IntN n
x
   mkSymVal :: VarContext -> Maybe String -> m (SBV (IntN n))
mkSymVal   = Kind -> VarContext -> Maybe String -> m (SBV (IntN n))
forall (m :: * -> *) a.
MonadSymbolic m =>
Kind -> VarContext -> Maybe String -> m (SBV a)
genMkSymVar (IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (IntN n
forall a. HasCallStack => a
undefined :: IntN n))
   fromCV :: CV -> IntN n
fromCV     = CV -> IntN n
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 :: String -> (SVal -> SVal) -> bv n -> bv n
lift1 String
nm SVal -> SVal
op bv n
x = SVal -> bv n
uc (SVal -> bv n) -> SVal -> bv n
forall a b. (a -> b) -> a -> b
$ SVal -> SVal
op (bv n -> SVal
c bv n
x)
  where k :: Kind
k = bv n -> Kind
forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (bv n -> CV) -> bv n -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> CV
normCV (CV -> CV) -> (bv n -> CV) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bv n -> Integer
forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> bv n
uc (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
v)))) = Integer -> bv n
forall a. Num a => Integer -> a
fromInteger Integer
v
        uc SVal
r                                   = String -> bv n
forall a. HasCallStack => String -> a
error (String -> bv n) -> String -> bv n
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" over " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Kind, bv n, SVal) -> String
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 :: 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 (SVal -> bv n) -> SVal -> bv n
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 = bv n -> Kind
forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (bv n -> CV) -> bv n -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> CV
normCV (CV -> CV) -> (bv n -> CV) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bv n -> Integer
forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> bv n
uc (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
v)))) = Integer -> bv n
forall a. Num a => Integer -> a
fromInteger Integer
v
        uc SVal
r                                   = String -> bv n
forall a. HasCallStack => String -> a
error (String -> bv n) -> String -> bv n
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" over " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Kind, bv n, bv n, SVal) -> String
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 :: 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 (SVal -> bv n) -> SVal -> bv n
forall a b. (a -> b) -> a -> b
$ bv n -> SVal
c bv n
x SVal -> Int -> SVal
`op` Int
i
  where k :: Kind
k = bv n -> Kind
forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (bv n -> CV) -> bv n -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> CV
normCV (CV -> CV) -> (bv n -> CV) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bv n -> Integer
forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> bv n
uc (SVal Kind
_ (Left (CV Kind
_ (CInteger Integer
v)))) = Integer -> bv n
forall a. Num a => Integer -> a
fromInteger Integer
v
        uc SVal
r                                   = String -> bv n
forall a. HasCallStack => String -> a
error (String -> bv n) -> String -> bv n
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" over " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Kind, bv n, Int, SVal) -> String
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 :: String -> (SVal -> Int -> SVal) -> bv n -> Int -> Bool
lift2IB String
nm SVal -> Int -> SVal
op bv n
x Int
i = SVal -> Bool
uc (SVal -> Bool) -> SVal -> Bool
forall a b. (a -> b) -> a -> b
$ bv n -> SVal
c bv n
x SVal -> Int -> SVal
`op` Int
i
  where k :: Kind
k = bv n -> Kind
forall a. HasKind a => a -> Kind
kindOf bv n
x
        c :: bv n -> SVal
c = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal)
-> (bv n -> Either CV (Cached SV)) -> bv n -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left (CV -> Either CV (Cached SV))
-> (bv n -> CV) -> bv n -> Either CV (Cached SV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> CV
normCV (CV -> CV) -> (bv n -> CV) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> (bv n -> CVal) -> bv n -> CV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> CVal
CInteger (Integer -> CVal) -> (bv n -> Integer) -> bv n -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. bv n -> Integer
forall a. Integral a => a -> Integer
toInteger
        uc :: SVal -> Bool
uc (SVal Kind
_ (Left CV
v)) = CV -> Bool
cvToBool CV
v
        uc SVal
r                 = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"Impossible happened while lifting " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" over " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Kind, bv n, Int, SVal) -> String
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 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
   maxBound :: WordN n
maxBound = let sz :: Int
sz = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n) in Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> Integer -> WordN n
forall a b. (a -> b) -> a -> b
$ Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz Integer -> Integer -> Integer
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 = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 in Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ - (Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz1)
   maxBound :: IntN n
maxBound = let sz1 :: Int
sz1 = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 in Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Int
sz1 Integer -> Integer -> Integer
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
(+)         = String -> (SVal -> SVal -> SVal) -> 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
   (-)         = String -> (SVal -> SVal -> SVal) -> 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
svMinus
   * :: WordN n -> WordN n -> WordN n
(*)         = String -> (SVal -> SVal -> SVal) -> 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      = String -> (SVal -> SVal) -> 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) -> bv n -> bv n
lift1 String
"signum" SVal -> SVal
svUNeg
   abs :: WordN n -> WordN n
abs         = String -> (SVal -> SVal) -> 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) -> bv n -> bv n
lift1 String
"abs"    SVal -> SVal
svAbs
   signum :: WordN n -> WordN n
signum      = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> (WordN n -> Integer) -> WordN n -> WordN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
signum   (Integer -> Integer) -> (WordN n -> Integer) -> WordN n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Integer
forall a. Integral a => a -> Integer
toInteger
   fromInteger :: Integer -> WordN n
fromInteger = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> (Integer -> Integer) -> Integer -> WordN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer -> Integer
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Integer -> Integer)
-> (Integer -> Maybe Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> Maybe Integer
svAsInteger (SVal -> Maybe Integer)
-> (Integer -> SVal) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Integer -> SVal
svInteger (WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (WordN n
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
(+)         = String -> (SVal -> SVal -> SVal) -> 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
   (-)         = String -> (SVal -> SVal -> SVal) -> 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
svMinus
   * :: IntN n -> IntN n -> IntN n
(*)         = String -> (SVal -> SVal -> SVal) -> 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      = String -> (SVal -> SVal) -> 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) -> bv n -> bv n
lift1 String
"signum" SVal -> SVal
svUNeg
   abs :: IntN n -> IntN n
abs         = String -> (SVal -> SVal) -> 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) -> bv n -> bv n
lift1 String
"abs"    SVal -> SVal
svAbs
   signum :: IntN n -> IntN n
signum      = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> (IntN n -> Integer) -> IntN n -> IntN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
signum   (Integer -> Integer) -> (IntN n -> Integer) -> IntN n -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger
   fromInteger :: Integer -> IntN n
fromInteger = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> (Integer -> Integer) -> Integer -> IntN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Integer -> Integer
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Integer -> Integer)
-> (Integer -> Maybe Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> Maybe Integer
svAsInteger (SVal -> Maybe Integer)
-> (Integer -> SVal) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Integer -> SVal
svInteger (IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (IntN n
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   = Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger  (Integer -> WordN n) -> (Int -> Integer) -> Int -> WordN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
   fromEnum :: WordN n -> Int
fromEnum = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> (WordN n -> Integer) -> WordN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Integer
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   = Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger  (Integer -> IntN n) -> (Int -> Integer) -> Int -> IntN n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger
   fromEnum :: IntN n -> Int
fromEnum = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> (IntN n -> Integer) -> IntN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Integer
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) = Integer -> Rational
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) = Integer -> Rational
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) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem Integer
x Integer
y in (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
q, Integer -> WordN n
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) = Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem Integer
x Integer
y in (Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
q, Integer -> IntN n
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
(.&.)        = String -> (SVal -> SVal -> SVal) -> 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
(.|.)        = String -> (SVal -> SVal -> SVal) -> 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          = String -> (SVal -> SVal -> SVal) -> 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
"xor"        SVal -> SVal -> SVal
svXOr
   complement :: WordN n -> WordN n
complement   = String -> (SVal -> SVal) -> 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) -> bv n -> bv n
lift1   String
"complement" SVal -> SVal
svNot
   shiftL :: WordN n -> Int -> WordN n
shiftL       = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
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       = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
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      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
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      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> WordN n
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      = String -> (SVal -> Int -> SVal) -> WordN n -> Int -> Bool
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 = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (WordN n -> Int) -> WordN n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> WordN n -> Int
forall a b. a -> b -> a
const (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
   bitSize :: WordN n -> Int
bitSize WordN n
_    = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
   isSigned :: WordN n -> Bool
isSigned     = Kind -> Bool
forall a. HasKind a => a -> Bool
hasSign (Kind -> Bool) -> (WordN n -> Kind) -> WordN n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf
   bit :: Int -> WordN n
bit Int
i        = WordN n
1 WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i
   popCount :: WordN n -> Int
popCount     = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> (WordN n -> Int) -> WordN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Bits a => a -> Int
popCount (Integer -> Int) -> (WordN n -> Integer) -> WordN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Integer
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
(.&.)        = String -> (SVal -> SVal -> SVal) -> 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
(.|.)        = String -> (SVal -> SVal -> SVal) -> 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          = String -> (SVal -> SVal -> SVal) -> 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
"xor"        SVal -> SVal -> SVal
svXOr
   complement :: IntN n -> IntN n
complement   = String -> (SVal -> SVal) -> 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) -> bv n -> bv n
lift1   String
"complement" SVal -> SVal
svNot
   shiftL :: IntN n -> Int -> IntN n
shiftL       = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
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       = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
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      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
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      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> IntN n
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      = String -> (SVal -> Int -> SVal) -> IntN n -> Int -> Bool
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 = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (IntN n -> Int) -> IntN n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntN n -> Int
forall a b. a -> b -> a
const (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n))
   bitSize :: IntN n -> Int
bitSize IntN n
_    = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
   isSigned :: IntN n -> Bool
isSigned     = Kind -> Bool
forall a. HasKind a => a -> Bool
hasSign (Kind -> Bool) -> (IntN n -> Kind) -> IntN n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf
   bit :: Int -> IntN n
bit Int
i        = IntN n
1 IntN n -> Int -> IntN n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i
   popCount :: IntN n -> Int
popCount     = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Int) -> (IntN n -> Int) -> IntN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int
forall a. Bits a => a -> Int
popCount (Integer -> Int) -> (IntN n -> Integer) -> IntN n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Integer
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 WordN n -> WordN n -> (WordN n, WordN n)
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 WordN n -> WordN n -> (WordN n, WordN n)
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 IntN n -> IntN n -> (IntN n, IntN n)
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 IntN n -> IntN n -> (IntN n, IntN n)
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 = SWord n -> SWord n -> (SWord n, SWord n)
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  = SWord n -> SWord n -> (SWord n, SWord n)
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 = SInt n -> SInt n -> (SInt n, SInt n)
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  = SInt n -> SInt n -> (SInt n, SInt n)
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)
_ = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
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)
_ = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
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 = Kind -> [CV] -> Maybe (WordN n, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (WordN n
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 = Kind -> [CV] -> Maybe (IntN n, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (IntN n
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        = SBV (IntN n) -> SBV (WordN n)
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 SBV (WordN n) -> SBV (WordN n) -> SBV (WordN n)
forall a. Num a => a -> a -> a
+ SBV (WordN n)
2 SBV (WordN n) -> Int -> SBV (WordN n)
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  fromMetricSpace :: SBV (MetricSpace (IntN n)) -> SBV (IntN n)
fromMetricSpace  SBV (MetricSpace (IntN n))
x        = SBV (WordN n) -> SBV (IntN n)
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))
SBV (WordN n)
x SBV (IntN n) -> SBV (IntN n) -> SBV (IntN n)
forall a. Num a => a -> a -> a
- SBV (IntN n)
2 SBV (IntN n) -> Int -> SBV (IntN n)
forall a b. (Num a, Integral b) => a -> b -> a
^ (Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n) Int -> Int -> Int
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 :: String -> m (SWord n)
sWord = String -> m (SWord n)
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_ :: m (SWord n)
sWord_ = m (SWord n)
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 :: [String] -> m [SWord n]
sWords = [String] -> m [SWord n]
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 :: String -> m (SInt n)
sInt = String -> m (SInt n)
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_ :: m (SInt n)
sInt_ = m (SInt n)
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 :: [String] -> m [SInt n]
sInts = [String] -> m [SInt n]
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 :: proxy i -> proxy j -> SBV (bv n) -> SBV (bv ((i - j) + 1))
bvExtract proxy i
start proxy j
end = SVal -> SBV (bv ((i - j) + 1))
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv ((i - j) + 1)))
-> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv ((i - j) + 1))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
i Int
j (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV
   where i :: Int
i  = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
start)
         j :: Int
j  = Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy j -> Integer
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 # :: SBV (bv n) -> SBV (bv m) -> SBV (bv (n + m))
# SBV (bv m)
m = SVal -> SBV (bv (n + m))
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv (n + m))) -> SVal -> SBV (bv (n + m))
forall a b. (a -> b) -> a -> b
$ SVal -> SVal -> SVal
svJoin (SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv n)
n) (SBV (bv m) -> SVal
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 :: SBV (bv n) -> SBV (bv m)
zeroExtend SBV (bv n)
n = SVal -> SBV (bv m)
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv m)) -> SVal -> SBV (bv m)
forall a b. (a -> b) -> a -> b
$ Int -> SVal -> SVal
svZeroExtend Int
i (SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv n)
n)
  where nv :: Int
nv = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
        mv :: Int
mv = Proxy m -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy m
forall k (t :: k). Proxy t
Proxy @m)
        i :: Int
i  = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
mv Int -> Int -> Int
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 :: SBV (bv n) -> SBV (bv m)
signExtend SBV (bv n)
n = SVal -> SBV (bv m)
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv m)) -> SVal -> SBV (bv m)
forall a b. (a -> b) -> a -> b
$ Int -> SVal -> SVal
svSignExtend Int
i (SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV SBV (bv n)
n)
  where nv :: Int
nv = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
        mv :: Int
mv = Proxy m -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy m
forall k (t :: k). Proxy t
Proxy @m)
        i :: Int
i  = Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
mv Int -> Int -> Int
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 :: proxy i -> SBV (bv n) -> SBV (bv m)
bvDrop proxy i
i = SVal -> SBV (bv m)
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv m))
-> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
start Int
0 (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV
  where nv :: Int
nv    = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
        start :: Int
start = Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
i) Int -> Int -> Int
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 :: proxy i -> SBV (bv n) -> SBV (bv i)
bvTake proxy i
i = SVal -> SBV (bv i)
forall a. SVal -> SBV a
SBV (SVal -> SBV (bv i))
-> (SBV (bv n) -> SVal) -> SBV (bv n) -> SBV (bv i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SVal -> SVal
svExtract Int
start Int
end (SVal -> SVal) -> (SBV (bv n) -> SVal) -> SBV (bv n) -> SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SBV (bv n) -> SVal
forall a. SBV a -> SVal
unSBV
  where nv :: Int
nv    = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (Proxy n
forall k (t :: k). Proxy t
Proxy @n)
        start :: Int
start = Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
        end :: Int
end   = Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
- Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (proxy i -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal proxy i
i) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1