{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -funbox-strict-fields #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.BV
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.IR.SymPrim.Data.BV (IntN (..), WordN (..)) where

import Control.DeepSeq
import Control.Exception
import Data.Bits
import Data.Hashable
import Data.Proxy
import GHC.Enum
import GHC.Generics
import GHC.Real
import GHC.TypeNats
import Grisette.Core.Data.Class.BitVector
import Language.Haskell.TH.Syntax
import Numeric

-- |
-- Symbolic unsigned bit vectors.
newtype WordN (n :: Nat) = WordN {forall (n :: Nat). WordN n -> Integer
unWordN :: 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
Ord, (forall x. WordN n -> Rep (WordN n) x)
-> (forall x. Rep (WordN n) x -> WordN n) -> Generic (WordN n)
forall x. Rep (WordN n) x -> WordN n
forall x. WordN n -> Rep (WordN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: Nat) x. Rep (WordN n) x -> WordN n
forall (n :: Nat) x. WordN n -> Rep (WordN n) x
$cto :: forall (n :: Nat) x. Rep (WordN n) x -> WordN n
$cfrom :: forall (n :: Nat) x. WordN n -> Rep (WordN n) x
Generic, (forall (m :: * -> *). Quote m => WordN n -> m Exp)
-> (forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n))
-> Lift (WordN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (n :: Nat) (m :: * -> *). Quote m => WordN n -> m Exp
forall (n :: Nat) (m :: * -> *).
Quote m =>
WordN n -> Code m (WordN n)
forall (m :: * -> *). Quote m => WordN n -> m Exp
forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n)
liftTyped :: forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n)
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
WordN n -> Code m (WordN n)
lift :: forall (m :: * -> *). Quote m => WordN n -> m Exp
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => WordN n -> m Exp
Lift, Int -> WordN n -> Int
WordN n -> Int
(Int -> WordN n -> Int) -> (WordN n -> Int) -> Hashable (WordN n)
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall (n :: Nat). Int -> WordN n -> Int
forall (n :: Nat). WordN n -> Int
hash :: WordN n -> Int
$chash :: forall (n :: Nat). WordN n -> Int
hashWithSalt :: Int -> WordN n -> Int
$chashWithSalt :: forall (n :: Nat). Int -> WordN n -> Int
Hashable, WordN n -> ()
(WordN n -> ()) -> NFData (WordN n)
forall a. (a -> ()) -> NFData a
forall (n :: Nat). WordN n -> ()
rnf :: WordN n -> ()
$crnf :: forall (n :: Nat). WordN n -> ()
NFData)

instance (KnownNat n, 1 <= n) => Show (WordN n) where
  show :: WordN n -> String
show (WordN Integer
w) = if (Natural
bitwidth Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
4) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 then String
hexRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hexRep else String
binRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
binRep
    where
      bitwidth :: Natural
bitwidth = Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      hexRepPre :: String
hexRepPre = String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural
bitwidth Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
4) Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hexRep) Char
'0'
      hexRep :: String
hexRep = Integer -> ShowS
forall a. (Integral a, Show a) => a -> ShowS
showHex Integer
w String
""
      binRepPre :: String
binRepPre = String
"0b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
bitwidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
binRep) Char
'0'
      binRep :: String
binRep = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 (\Int
x -> if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Char
'0' else Char
'1') Integer
w String
""

-- |
-- Symbolic signed bit vectors.
newtype IntN (n :: Nat) = IntN {forall (n :: Nat). IntN n -> Integer
unIntN :: 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, (forall x. IntN n -> Rep (IntN n) x)
-> (forall x. Rep (IntN n) x -> IntN n) -> Generic (IntN n)
forall x. Rep (IntN n) x -> IntN n
forall x. IntN n -> Rep (IntN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (n :: Nat) x. Rep (IntN n) x -> IntN n
forall (n :: Nat) x. IntN n -> Rep (IntN n) x
$cto :: forall (n :: Nat) x. Rep (IntN n) x -> IntN n
$cfrom :: forall (n :: Nat) x. IntN n -> Rep (IntN n) x
Generic, (forall (m :: * -> *). Quote m => IntN n -> m Exp)
-> (forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n))
-> Lift (IntN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (n :: Nat) (m :: * -> *). Quote m => IntN n -> m Exp
forall (n :: Nat) (m :: * -> *).
Quote m =>
IntN n -> Code m (IntN n)
forall (m :: * -> *). Quote m => IntN n -> m Exp
forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n)
liftTyped :: forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n)
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
IntN n -> Code m (IntN n)
lift :: forall (m :: * -> *). Quote m => IntN n -> m Exp
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => IntN n -> m Exp
Lift, Int -> IntN n -> Int
IntN n -> Int
(Int -> IntN n -> Int) -> (IntN n -> Int) -> Hashable (IntN n)
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall (n :: Nat). Int -> IntN n -> Int
forall (n :: Nat). IntN n -> Int
hash :: IntN n -> Int
$chash :: forall (n :: Nat). IntN n -> Int
hashWithSalt :: Int -> IntN n -> Int
$chashWithSalt :: forall (n :: Nat). Int -> IntN n -> Int
Hashable, IntN n -> ()
(IntN n -> ()) -> NFData (IntN n)
forall a. (a -> ()) -> NFData a
forall (n :: Nat). IntN n -> ()
rnf :: IntN n -> ()
$crnf :: forall (n :: Nat). IntN n -> ()
NFData)

instance (KnownNat n, 1 <= n) => Show (IntN n) where
  show :: IntN n -> String
show (IntN Integer
w) = if (Natural
bitwidth Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`mod` Natural
4) Natural -> Natural -> Bool
forall a. Eq a => a -> a -> Bool
== Natural
0 then String
hexRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
hexRep else String
binRepPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
binRep
    where
      bitwidth :: Natural
bitwidth = Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      hexRepPre :: String
hexRepPre = String
"0x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural
bitwidth Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`div` Natural
4) Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
hexRep) Char
'0'
      hexRep :: String
hexRep = Integer -> ShowS
forall a. (Integral a, Show a) => a -> ShowS
showHex Integer
w String
""
      binRepPre :: String
binRepPre = String
"0b" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
bitwidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
binRep) Char
'0'
      binRep :: String
binRep = Integer -> (Int -> Char) -> Integer -> ShowS
forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
showIntAtBase Integer
2 (\Int
x -> if Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Char
'0' else Char
'1') Integer
w String
""

instance (KnownNat n, 1 <= n) => Bits (WordN n) where
  WordN Integer
a .&. :: WordN n -> WordN n -> WordN n
.&. WordN Integer
b = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
b)
  WordN Integer
a .|. :: WordN n -> WordN n -> WordN n
.|. WordN Integer
b = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b)
  WordN Integer
a xor :: WordN n -> WordN n -> WordN n
`xor` WordN Integer
b = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b)
  complement :: WordN n -> WordN n
complement WordN n
a = WordN n
forall a. Bounded a => a
maxBound WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
`xor` WordN n
a

  -- shift use default implementation
  -- rotate use default implementation
  zeroBits :: WordN n
zeroBits = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
  bit :: Int -> WordN n
bit Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) = WordN n
forall a. Bits a => a
zeroBits
    | Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Int -> Integer
forall a. Bits a => Int -> a
bit Int
i)

  -- setBit use default implementation
  clearBit :: WordN n -> Int -> WordN n
clearBit (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
a Int
i)

  -- complementBit use default implementation
  testBit :: WordN n -> Int -> Bool
testBit (WordN Integer
a) = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a
  bitSizeMaybe :: WordN n -> Maybe Int
bitSizeMaybe WordN n
_ = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  bitSize :: WordN n -> Int
bitSize WordN n
_ = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  isSigned :: WordN n -> Bool
isSigned WordN n
_ = Bool
False
  shiftL :: WordN n -> Int -> WordN n
shiftL (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
i) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound

  -- unsafeShiftL use default implementation
  shiftR :: WordN n -> Int -> WordN n
shiftR (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
i)

  -- unsafeShiftR use default implementation
  rotateL :: WordN n -> Int -> WordN n
rotateL WordN n
a Int
0 = WordN n
a
  rotateL (WordN Integer
a) Int
k
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateL (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
a) (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n)
    | Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> Integer -> WordN n
forall a b. (a -> b) -> a -> b
$ Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
h
    where
      n :: Int
n = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      s :: Int
s = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
      l :: Integer
l = Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
s
      h :: Integer
h = (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
l Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
s)) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
k
  rotateR :: WordN n -> Int -> WordN n
rotateR WordN n
a Int
0 = WordN n
a
  rotateR (WordN Integer
a) Int
k
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateR (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
a) (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n)
    | Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer -> WordN n) -> Integer -> WordN n
forall a b. (a -> b) -> a -> b
$ Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
h
    where
      n :: Int
n = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      s :: Int
s = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
      l :: Integer
l = Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k
      h :: Integer
h = (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
l Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
k)) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
s
  popCount :: WordN n -> Int
popCount (WordN Integer
n) = Integer -> Int
forall a. Bits a => a -> Int
popCount Integer
n

instance (KnownNat n, 1 <= n) => FiniteBits (WordN n) where
  finiteBitSize :: WordN n -> Int
finiteBitSize WordN n
_ = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

instance (KnownNat n, 1 <= n) => Bounded (WordN n) where
  maxBound :: WordN n
maxBound = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
  minBound :: WordN n
minBound = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0

instance (KnownNat n, 1 <= n) => Enum (WordN n) where
  succ :: WordN n -> WordN n
succ WordN n
x
    | WordN n
x WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
/= WordN n
forall a. Bounded a => a
maxBound = WordN n
x WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
+ WordN n
1
    | Bool
otherwise = String -> WordN n
forall a. String -> a
succError (String -> WordN n) -> String -> WordN n
forall a b. (a -> b) -> a -> b
$ String
"WordN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  pred :: WordN n -> WordN n
pred WordN n
x
    | WordN n
x WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
/= WordN n
forall a. Bounded a => a
minBound = WordN n
x WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
- WordN n
1
    | Bool
otherwise = String -> WordN n
forall a. String -> a
predError (String -> WordN n) -> String -> WordN n
forall a b. (a -> b) -> a -> b
$ String
"WordN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  toEnum :: Int -> WordN n
toEnum Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= WordN n -> Integer
forall a. Integral a => a -> Integer
toInteger (WordN n
forall a. Bounded a => a
maxBound :: WordN n) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i)
    | Bool
otherwise = String -> Int -> (WordN n, WordN n) -> WordN n
forall a b. Show a => String -> Int -> (a, a) -> b
toEnumError (String
"WordN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Int
i (WordN n
forall a. Bounded a => a
minBound :: WordN n, WordN n
forall a. Bounded a => a
maxBound :: WordN n)
  fromEnum :: WordN n -> Int
fromEnum (WordN Integer
n) = Integer -> Int
forall a. Enum a => a -> Int
fromEnum Integer
n
  enumFrom :: WordN n -> [WordN n]
enumFrom = WordN n -> [WordN n]
forall a. (Enum a, Bounded a) => a -> [a]
boundedEnumFrom
  {-# INLINE enumFrom #-}
  enumFromThen :: WordN n -> WordN n -> [WordN n]
enumFromThen = WordN n -> WordN n -> [WordN n]
forall a. (Enum a, Bounded a) => a -> a -> [a]
boundedEnumFromThen
  {-# INLINE enumFromThen #-}

instance (KnownNat n, 1 <= n) => Real (WordN n) where
  toRational :: WordN n -> Rational
toRational (WordN Integer
n) = Integer
n Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1

instance (KnownNat n, 1 <= n) => Integral (WordN n) where
  quot :: WordN n -> WordN n -> WordN n
quot (WordN Integer
x) (WordN Integer
y) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
y)
  rem :: WordN n -> WordN n -> WordN n
rem (WordN Integer
x) (WordN Integer
y) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` Integer
y)
  quotRem :: WordN n -> WordN n -> (WordN n, WordN n)
quotRem (WordN Integer
x) (WordN Integer
y) = case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem Integer
x Integer
y of
    (Integer
q, Integer
r) -> (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
q, Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
r)
  div :: WordN n -> WordN n -> WordN n
div = WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
quot
  mod :: WordN n -> WordN n -> WordN n
mod = WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
rem
  divMod :: WordN n -> WordN n -> (WordN n, WordN n)
divMod = WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
quotRem
  toInteger :: WordN n -> Integer
toInteger (WordN Integer
n) = Integer
n

instance (KnownNat n, 1 <= n) => Num (WordN n) where
  WordN Integer
x + :: WordN n -> WordN n -> WordN n
+ WordN Integer
y = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound
  WordN Integer
x * :: WordN n -> WordN n -> WordN n
* WordN Integer
y = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound
  WordN Integer
x - :: WordN n -> WordN n -> WordN n
- WordN Integer
y
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
y = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
    | Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
  negate :: WordN n -> WordN n
negate (WordN Integer
0) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
  negate WordN n
a = WordN n -> WordN n
forall a. Bits a => a -> a
complement WordN n
a WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
+ Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
1
  abs :: WordN n -> WordN n
abs WordN n
x = WordN n
x
  signum :: WordN n -> WordN n
signum (WordN Integer
0) = WordN n
0
  signum WordN n
_ = WordN n
1
  fromInteger :: Integer -> WordN n
fromInteger !Integer
x
    | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n
forall a. Bounded a => a
maxBound :: WordN n))
    | Bool
otherwise = -Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger (-Integer
x)

minusOneIntN :: forall proxy n. KnownNat n => proxy n -> IntN n
minusOneIntN :: forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN proxy n
_ = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)

instance (KnownNat n, 1 <= n) => Bits (IntN n) where
  IntN Integer
a .&. :: IntN n -> IntN n -> IntN n
.&. IntN Integer
b = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
b)
  IntN Integer
a .|. :: IntN n -> IntN n -> IntN n
.|. IntN Integer
b = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b)
  IntN Integer
a xor :: IntN n -> IntN n -> IntN n
`xor` IntN Integer
b = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b)
  complement :: IntN n -> IntN n
complement IntN n
a = Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
`xor` IntN n
a

  -- shift use default implementation
  -- rotate use default implementation
  zeroBits :: IntN n
zeroBits = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
  bit :: Int -> IntN n
bit Int
i = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (Int -> WordN n
forall a. Bits a => Int -> a
bit Int
i :: WordN n))

  -- setBit use default implementation
  clearBit :: IntN n -> Int -> IntN n
clearBit (IntN Integer
a) Int
i = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
clearBit Integer
a Int
i)

  -- complementBit use default implementation
  testBit :: IntN n -> Int -> Bool
testBit (IntN Integer
a) = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a
  bitSizeMaybe :: IntN n -> Maybe Int
bitSizeMaybe IntN n
_ = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  bitSize :: IntN n -> Int
bitSize IntN n
_ = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  isSigned :: IntN n -> Bool
isSigned IntN n
_ = Bool
True

  shiftL :: IntN n -> Int -> IntN n
shiftL (IntN Integer
a) Int
i = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n -> Integer) -> WordN n -> Integer
forall a b. (a -> b) -> a -> b
$ (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
a :: WordN n) WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
`shiftL` Int
i)

  -- unsafeShiftL use default implementation
  shiftR :: IntN n -> Int -> IntN n
shiftR IntN n
i Int
0 = IntN n
i
  shiftR (IntN Integer
i) Int
k
    | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n = if Bool
b then Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
maxi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) else Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
    | Bool
otherwise = if Bool
b then Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
maxi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
noi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k)) else Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
i Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
k)
    where
      b :: Bool
b = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
i (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      n :: Int
n = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      maxi :: Integer
maxi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
n
      noi :: Integer
noi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k)

  -- unsafeShiftR use default implementation
  rotateL :: IntN n -> Int -> IntN n
rotateL (IntN Integer
i) Int
k = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n -> Integer) -> WordN n -> Integer
forall a b. (a -> b) -> a -> b
$ WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateL (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
i :: WordN n) Int
k
  rotateR :: IntN n -> Int -> IntN n
rotateR (IntN Integer
i) Int
k = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n -> Integer) -> WordN n -> Integer
forall a b. (a -> b) -> a -> b
$ WordN n -> Int -> WordN n
forall a. Bits a => a -> Int -> a
rotateR (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
i :: WordN n) Int
k
  popCount :: IntN n -> Int
popCount (IntN Integer
i) = Integer -> Int
forall a. Bits a => a -> Int
popCount Integer
i

instance (KnownNat n, 1 <= n) => FiniteBits (IntN n) where
  finiteBitSize :: IntN n -> Int
finiteBitSize IntN n
_ = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))

instance (KnownNat n, 1 <= n) => Bounded (IntN n) where
  maxBound :: IntN n
maxBound = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
  minBound :: IntN n
minBound = IntN n
forall a. Bounded a => a
maxBound IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ IntN n
1

instance (KnownNat n, 1 <= n) => Enum (IntN n) where
  succ :: IntN n -> IntN n
succ IntN n
x
    | IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
/= IntN n
forall a. Bounded a => a
maxBound = IntN n
x IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ IntN n
1
    | Bool
otherwise = String -> IntN n
forall a. String -> a
succError (String -> IntN n) -> String -> IntN n
forall a b. (a -> b) -> a -> b
$ String
"IntN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  pred :: IntN n -> IntN n
pred IntN n
x
    | IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
/= IntN n
forall a. Bounded a => a
minBound = IntN n
x IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
- IntN n
1
    | Bool
otherwise = String -> IntN n
forall a. String -> a
predError (String -> IntN n) -> String -> IntN n
forall a b. (a -> b) -> a -> b
$ String
"IntN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  toEnum :: Int -> IntN n
toEnum Int
i
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= IntN n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n
forall a. Bounded a => a
minBound :: IntN n) Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= IntN n -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (IntN n
forall a. Bounded a => a
maxBound :: IntN n) = Int -> IntN n
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i
    | Bool
otherwise = String -> Int -> (WordN n, WordN n) -> IntN n
forall a b. Show a => String -> Int -> (a, a) -> b
toEnumError (String
"IntN " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Int
i (WordN n
forall a. Bounded a => a
minBound :: WordN n, WordN n
forall a. Bounded a => a
maxBound :: WordN n)
  fromEnum :: IntN n -> Int
fromEnum = Integer -> Int
forall a. Enum a => a -> Int
fromEnum (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
  enumFrom :: IntN n -> [IntN n]
enumFrom = IntN n -> [IntN n]
forall a. (Enum a, Bounded a) => a -> [a]
boundedEnumFrom
  {-# INLINE enumFrom #-}
  enumFromThen :: IntN n -> IntN n -> [IntN n]
enumFromThen = IntN n -> IntN n -> [IntN n]
forall a. (Enum a, Bounded a) => a -> a -> [a]
boundedEnumFromThen
  {-# INLINE enumFromThen #-}

instance (KnownNat n, 1 <= n) => Real (IntN n) where
  toRational :: IntN n -> Rational
toRational IntN n
i = IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
i Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1

instance (KnownNat n, 1 <= n) => Integral (IntN n) where
  quot :: IntN n -> IntN n -> IntN n
quot IntN n
x IntN n
y =
    if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
      then ArithException -> IntN n
forall a e. Exception e => e -> a
throw ArithException
Overflow
      else Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
  rem :: IntN n -> IntN n -> IntN n
rem IntN n
x IntN n
y =
    if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
      then ArithException -> IntN n
forall a e. Exception e => e -> a
throw ArithException
Overflow
      else Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`rem` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
  quotRem :: IntN n -> IntN n -> (IntN n, IntN n)
quotRem IntN n
x IntN n
y =
    if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
      then ArithException -> (IntN n, IntN n)
forall a e. Exception e => e -> a
throw ArithException
Overflow
      else case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
quotRem (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x) (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y) of
        (Integer
q, Integer
r) -> (Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
q, Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
r)
  div :: IntN n -> IntN n -> IntN n
div IntN n
x IntN n
y =
    if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
      then ArithException -> IntN n
forall a e. Exception e => e -> a
throw ArithException
Overflow
      else Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
  mod :: IntN n -> IntN n -> IntN n
mod IntN n
x IntN n
y =
    if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
      then ArithException -> IntN n
forall a e. Exception e => e -> a
throw ArithException
Overflow
      else Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y)
  divMod :: IntN n -> IntN n -> (IntN n, IntN n)
divMod IntN n
x IntN n
y =
    if IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
forall a. Bounded a => a
minBound Bool -> Bool -> Bool
&& IntN n
y IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1
      then ArithException -> (IntN n, IntN n)
forall a e. Exception e => e -> a
throw ArithException
Overflow
      else case Integer -> Integer -> (Integer, Integer)
forall a. Integral a => a -> a -> (a, a)
divMod (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x) (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
y) of
        (Integer
q, Integer
r) -> (Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
q, Integer -> IntN n
forall a. Num a => Integer -> a
fromInteger Integer
r)
  toInteger :: IntN n -> Integer
toInteger i :: IntN n
i@(IntN Integer
n) = case IntN n -> IntN n
forall a. Num a => a -> a
signum IntN n
i of
    IntN n
0 -> Integer
0
    IntN n
1 -> Integer
n
    -1 ->
      let x :: IntN n
x = IntN n -> IntN n
forall a. Num a => a -> a
negate IntN n
i
       in if IntN n -> IntN n
forall a. Num a => a -> a
signum IntN n
x IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== -IntN n
1 then -Integer
n else Integer -> Integer
forall a. Num a => a -> a
negate (IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
x)
    IntN n
_ -> Integer
forall a. HasCallStack => a
undefined

instance (KnownNat n, 1 <= n) => Num (IntN n) where
  IntN Integer
x + :: IntN n -> IntN n -> IntN n
+ IntN Integer
y = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
.&. Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
  IntN Integer
x * :: IntN n -> IntN n -> IntN n
* IntN Integer
y = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
.&. Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
  IntN Integer
x - :: IntN n -> IntN n -> IntN n
- IntN Integer
y
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
y = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
    | Bool
otherwise = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
  negate :: IntN n -> IntN n
negate (IntN Integer
0) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
  negate IntN n
a = IntN n -> IntN n
forall a. Bits a => a -> a
complement IntN n
a IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
1
  abs :: IntN n -> IntN n
abs IntN n
x = if IntN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit IntN n
x (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) then IntN n -> IntN n
forall a. Num a => a -> a
negate IntN n
x else IntN n
x
  signum :: IntN n -> IntN n
signum (IntN Integer
0) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
  signum IntN n
i = if IntN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit IntN n
i (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1) then -IntN n
1 else IntN n
1
  fromInteger :: Integer -> IntN n
fromInteger !Integer
x = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ if Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Integer
v else (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
v
    where
      v :: Integer
v = WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
maxn) :: WordN n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
maxn
      n :: Int
n = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
      maxn :: Integer
maxn = Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1

instance (KnownNat n, 1 <= n) => Ord (IntN n) where
  IntN Integer
a <= :: IntN n -> IntN n -> Bool
<= IntN Integer
b
    | Bool
as Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
bs = Bool
True
    | Bool -> Bool
not Bool
as Bool -> Bool -> Bool
&& Bool
bs = Bool
False
    | Bool
otherwise = Integer
a Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
b
    where
      n :: Int
n = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
      as :: Bool
as = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      bs :: Bool
bs = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
b (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

instance
  (KnownNat n, 1 <= n, KnownNat m, 1 <= m, KnownNat w, 1 <= w, w ~ (n + m)) =>
  BVConcat (WordN n) (WordN m) (WordN w)
  where
  bvconcat :: WordN n -> WordN m -> WordN w
bvconcat (WordN Integer
a) (WordN Integer
b) = Integer -> WordN w
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy m -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy m
forall {k} (t :: k). Proxy t
Proxy :: Proxy m))) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b)

instance
  (KnownNat n, 1 <= n, KnownNat m, 1 <= m, KnownNat w, 1 <= w, w ~ (n + m)) =>
  BVConcat (IntN n) (IntN m) (IntN w)
  where
  bvconcat :: IntN n -> IntN m -> IntN w
bvconcat (IntN Integer
a) (IntN Integer
b) = Integer -> IntN w
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN w) -> Integer -> IntN w
forall a b. (a -> b) -> a -> b
$ WordN w -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN w -> Integer) -> WordN w -> Integer
forall a b. (a -> b) -> a -> b
$ WordN n -> WordN m -> WordN w
forall bv1 bv2 bv3. BVConcat bv1 bv2 bv3 => bv1 -> bv2 -> bv3
bvconcat (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
a :: WordN n) (Integer -> WordN m
forall (n :: Nat). Integer -> WordN n
WordN Integer
b :: WordN m)

instance (KnownNat n, 1 <= n, KnownNat r, n <= r) => BVExtend (WordN n) r (WordN r) where
  bvzeroExtend :: forall (proxy :: Nat -> *). proxy r -> WordN n -> WordN r
bvzeroExtend proxy r
_ (WordN Integer
v) = Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN Integer
v
  bvsignExtend :: forall (proxy :: Nat -> *). proxy r -> WordN n -> WordN r
bvsignExtend proxy r
pr (WordN Integer
v) = if Bool
s then Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN (Integer
maxi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
noi Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
v) else Integer -> WordN r
forall (n :: Nat). Integer -> WordN n
WordN Integer
v
    where
      r :: Int
r = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ proxy r -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal proxy r
pr
      n :: Int
n = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      s :: Bool
s = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
v (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      maxi :: Integer
maxi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
r
      noi :: Integer
noi = (Integer
1 :: Integer) Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
n
  bvextend :: forall (proxy :: Nat -> *). proxy r -> WordN n -> WordN r
bvextend = proxy r -> WordN n -> WordN r
forall bv1 (n :: Nat) bv2 (proxy :: Nat -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvzeroExtend

instance (KnownNat n, 1 <= n, KnownNat r, n <= r) => BVExtend (IntN n) r (IntN r) where
  bvzeroExtend :: forall (proxy :: Nat -> *). proxy r -> IntN n -> IntN r
bvzeroExtend proxy r
_ (IntN Integer
v) = Integer -> IntN r
forall (n :: Nat). Integer -> IntN n
IntN Integer
v
  bvsignExtend :: forall (proxy :: Nat -> *). proxy r -> IntN n -> IntN r
bvsignExtend proxy r
pr (IntN Integer
v) = Integer -> IntN r
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN r) -> Integer -> IntN r
forall a b. (a -> b) -> a -> b
$ WordN r -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN r -> Integer) -> WordN r -> Integer
forall a b. (a -> b) -> a -> b
$ proxy r -> WordN n -> WordN r
forall bv1 (n :: Nat) bv2 (proxy :: Nat -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvsignExtend proxy r
pr (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
v :: WordN n)
  bvextend :: forall (proxy :: Nat -> *). proxy r -> IntN n -> IntN r
bvextend = proxy r -> IntN n -> IntN r
forall bv1 (n :: Nat) bv2 (proxy :: Nat -> *).
BVExtend bv1 n bv2 =>
proxy n -> bv1 -> bv2
bvsignExtend

instance (KnownNat n, 1 <= n, KnownNat ix, KnownNat w, 1 <= w, ix + w <= n) => BVSelect (WordN n) ix w (WordN w) where
  bvselect :: forall (proxy :: Nat -> *).
proxy ix -> proxy w -> WordN n -> WordN w
bvselect proxy ix
pix proxy w
pw (WordN Integer
v) = Integer -> WordN w
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
v Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
ix) Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
mask)
    where
      ix :: Int
ix = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ proxy ix -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal proxy ix
pix
      w :: Int
w = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ proxy w -> Natural
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Natural
natVal proxy w
pw
      mask :: Integer
mask = (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
w) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1

instance (KnownNat n, 1 <= n, KnownNat ix, KnownNat w, 1 <= w, ix + w <= n) => BVSelect (IntN n) ix w (IntN w) where
  bvselect :: forall (proxy :: Nat -> *). proxy ix -> proxy w -> IntN n -> IntN w
bvselect proxy ix
pix proxy w
pw (IntN Integer
v) = Integer -> IntN w
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN w) -> Integer -> IntN w
forall a b. (a -> b) -> a -> b
$ WordN w -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN w -> Integer) -> WordN w -> Integer
forall a b. (a -> b) -> a -> b
$ proxy ix -> proxy w -> WordN n -> WordN w
forall bv1 (ix :: Nat) (w :: Nat) bv2 (proxy :: Nat -> *).
BVSelect bv1 ix w bv2 =>
proxy ix -> proxy w -> bv1 -> bv2
bvselect proxy ix
pix proxy w
pw (Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
v :: WordN n)