-----------------------------------------------------------------------------
-- |
-- 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 UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Core.Sized (
        -- * Type-sized unsigned bit-vectors
          WordN
        -- * Type-sized signed bit-vectors
        , IntN
       ) where

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

import GHC.TypeLits

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

import Test.QuickCheck(Arbitrary(..))

-- | 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 (n :: Nat). WordN n -> WordN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
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 (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
$ccompare :: forall (n :: Nat). WordN n -> WordN n -> Ordering
compare :: WordN n -> WordN n -> Ordering
$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
>= :: WordN n -> WordN n -> Bool
$cmax :: forall (n :: Nat). WordN n -> WordN n -> WordN n
max :: WordN n -> WordN n -> WordN n
$cmin :: forall (n :: Nat). WordN n -> WordN n -> WordN n
min :: WordN n -> WordN n -> WordN n
Ord)

-- | Show instance for t'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

-- | t'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 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))

-- | 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 (n :: Nat). IntN n -> IntN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$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
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 (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
$ccompare :: forall (n :: Nat). IntN n -> IntN n -> Ordering
compare :: IntN n -> IntN n -> Ordering
$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
>= :: IntN n -> IntN n -> Bool
$cmax :: forall (n :: Nat). IntN n -> IntN n -> IntN n
max :: IntN n -> IntN n -> IntN n
$cmin :: forall (n :: Nat). IntN n -> IntN n -> IntN n
min :: IntN n -> IntN n -> IntN n
Ord)

-- | Show instance for t'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

-- | t'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 (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))

-- 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 (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 :: 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 (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 :: 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 (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 :: 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 (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 t'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 (forall (t :: Nat). Proxy t
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 t'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 (forall (t :: Nat). Proxy t
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 (forall (t :: Nat). Proxy t
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 t'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 t'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 t'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 t'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 t'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 t'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 t'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 t'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 t'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 (forall (t :: Nat). Proxy t
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 (forall (t :: Nat). Proxy t
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 t'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 (forall (t :: Nat). Proxy t
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 (forall (t :: Nat). Proxy t
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

-- | Quickcheck instance for WordN
instance KnownNat n => Arbitrary (WordN n) where
  arbitrary :: Gen (WordN n)
arbitrary = (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
. Integer -> Integer
norm (Integer -> Integer) -> (Integer -> Integer) -> Integer -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => a -> a
abs) (Integer -> WordN n) -> Gen Integer -> Gen (WordN n)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
    where sz :: Int
sz = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)

          norm :: Integer -> Integer
norm Integer
v | Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Integer
0
                 | Bool
True    = Integer
v Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. (((Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
sz) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

-- | Quickcheck instance for IntN
instance KnownNat n => Arbitrary (IntN n) where
  arbitrary :: Gen (IntN n)
arbitrary = (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
. Integer -> Integer
norm) (Integer -> IntN n) -> Gen Integer -> Gen (IntN n)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Gen Integer
forall a. Arbitrary a => Gen a
arbitrary
    where sz :: Int
sz = Proxy n -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)

          norm :: Integer -> Integer
norm Integer
v | Int
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Integer
0
                 | Bool
True  = let rg :: Integer
rg = Integer
2 Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
                           in case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod Integer
v Integer
rg of
                                     (Integer
a, Integer
b) | Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
a -> Integer
b
                                     (Integer
_, Integer
b)          -> Integer
b Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
rg