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

-- |
-- Module      :   Grisette.Core.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.Core.Data.BV
  ( BitwidthMismatch (..),
    IntN (..),
    WordN (..),
    SomeIntN (..),
    SomeWordN (..),
    unarySomeIntN,
    unarySomeIntNR1,
    binSomeIntN,
    binSomeIntNR1,
    binSomeIntNR2,
    unarySomeWordN,
    unarySomeWordNR1,
    binSomeWordN,
    binSomeWordNR1,
    binSomeWordNR2,
  )
where

import Control.DeepSeq
import Control.Exception
import Data.Bits
import Data.CallStack
import Data.Hashable
import Data.Proxy
import Data.Typeable
import GHC.Enum
import GHC.Generics
import GHC.Read
import GHC.Real
import GHC.TypeNats
import Grisette.Core.Data.Class.BitVector
import Grisette.Utils.Parameterized
import Language.Haskell.TH.Syntax
import Numeric
import Text.Read
import qualified Text.Read.Lex as L

data BitwidthMismatch = BitwidthMismatch
  deriving (Int -> BitwidthMismatch -> ShowS
[BitwidthMismatch] -> ShowS
BitwidthMismatch -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BitwidthMismatch] -> ShowS
$cshowList :: [BitwidthMismatch] -> ShowS
show :: BitwidthMismatch -> String
$cshow :: BitwidthMismatch -> String
showsPrec :: Int -> BitwidthMismatch -> ShowS
$cshowsPrec :: Int -> BitwidthMismatch -> ShowS
Show, BitwidthMismatch -> BitwidthMismatch -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c/= :: BitwidthMismatch -> BitwidthMismatch -> Bool
== :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c== :: BitwidthMismatch -> BitwidthMismatch -> Bool
Eq, Eq BitwidthMismatch
BitwidthMismatch -> BitwidthMismatch -> Bool
BitwidthMismatch -> BitwidthMismatch -> Ordering
BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
$cmin :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
max :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
$cmax :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
>= :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c>= :: BitwidthMismatch -> BitwidthMismatch -> Bool
> :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c> :: BitwidthMismatch -> BitwidthMismatch -> Bool
<= :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c<= :: BitwidthMismatch -> BitwidthMismatch -> Bool
< :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c< :: BitwidthMismatch -> BitwidthMismatch -> Bool
compare :: BitwidthMismatch -> BitwidthMismatch -> Ordering
$ccompare :: BitwidthMismatch -> BitwidthMismatch -> Ordering
Ord, forall x. Rep BitwidthMismatch x -> BitwidthMismatch
forall x. BitwidthMismatch -> Rep BitwidthMismatch x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep BitwidthMismatch x -> BitwidthMismatch
$cfrom :: forall x. BitwidthMismatch -> Rep BitwidthMismatch x
Generic)

instance Exception BitwidthMismatch where
  displayException :: BitwidthMismatch -> String
displayException BitwidthMismatch
BitwidthMismatch = String
"Bit width does not match"

-- |
-- Symbolic unsigned bit vectors.
newtype WordN (n :: Nat) = WordN {forall (n :: Natural). WordN n -> Integer
unWordN :: Integer}
  deriving (WordN n -> WordN n -> Bool
forall (n :: Natural). WordN n -> WordN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WordN n -> WordN n -> Bool
$c/= :: forall (n :: Natural). WordN n -> WordN n -> Bool
== :: WordN n -> WordN n -> Bool
$c== :: forall (n :: Natural). WordN n -> WordN n -> Bool
Eq, WordN n -> WordN n -> Bool
WordN n -> WordN n -> Ordering
WordN n -> WordN n -> WordN n
forall (n :: Natural). Eq (WordN n)
forall (n :: Natural). WordN n -> WordN n -> Bool
forall (n :: Natural). WordN n -> WordN n -> Ordering
forall (n :: Natural). WordN n -> WordN n -> WordN n
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: WordN n -> WordN n -> WordN n
$cmin :: forall (n :: Natural). WordN n -> WordN n -> WordN n
max :: WordN n -> WordN n -> WordN n
$cmax :: forall (n :: Natural). WordN n -> WordN n -> WordN n
>= :: WordN n -> WordN n -> Bool
$c>= :: forall (n :: Natural). WordN n -> WordN n -> Bool
> :: WordN n -> WordN n -> Bool
$c> :: forall (n :: Natural). WordN n -> WordN n -> Bool
<= :: WordN n -> WordN n -> Bool
$c<= :: forall (n :: Natural). WordN n -> WordN n -> Bool
< :: WordN n -> WordN n -> Bool
$c< :: forall (n :: Natural). WordN n -> WordN n -> Bool
compare :: WordN n -> WordN n -> Ordering
$ccompare :: forall (n :: Natural). WordN n -> WordN n -> Ordering
Ord, forall (n :: Natural) x. Rep (WordN n) x -> WordN n
forall (n :: Natural) x. WordN n -> Rep (WordN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (n :: Natural) x. Rep (WordN n) x -> WordN n
$cfrom :: forall (n :: Natural) x. WordN n -> Rep (WordN n) x
Generic, forall (n :: Natural) (m :: * -> *). Quote m => WordN n -> m Exp
forall (n :: Natural) (m :: * -> *).
Quote m =>
WordN n -> Code m (WordN n)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
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 :: Natural) (m :: * -> *).
Quote m =>
WordN n -> Code m (WordN n)
lift :: forall (m :: * -> *). Quote m => WordN n -> m Exp
$clift :: forall (n :: Natural) (m :: * -> *). Quote m => WordN n -> m Exp
Lift, Int -> WordN n -> Int
WordN n -> Int
forall (n :: Natural). Eq (WordN n)
forall (n :: Natural). Int -> WordN n -> Int
forall (n :: Natural). WordN n -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: WordN n -> Int
$chash :: forall (n :: Natural). WordN n -> Int
hashWithSalt :: Int -> WordN n -> Int
$chashWithSalt :: forall (n :: Natural). Int -> WordN n -> Int
Hashable, WordN n -> ()
forall (n :: Natural). WordN n -> ()
forall a. (a -> ()) -> NFData a
rnf :: WordN n -> ()
$crnf :: forall (n :: Natural). WordN n -> ()
NFData)

-- |
-- A non-indexed version of 'WordN'.
data SomeWordN where
  SomeWordN :: (KnownNat n, 1 <= n) => WordN n -> SomeWordN

unarySomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> r) -> SomeWordN -> r
unarySomeWordN :: forall r.
HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r
op (SomeWordN (WordN n
w :: WordN w)) = forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r
op WordN n
w
{-# INLINE unarySomeWordN #-}

unarySomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n) -> SomeWordN -> SomeWordN
unarySomeWordNR1 :: HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n
op (SomeWordN (WordN n
w :: WordN w)) = forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n
op WordN n
w
{-# INLINE unarySomeWordNR1 #-}

binSomeWordN :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> r) -> SomeWordN -> SomeWordN -> r
binSomeWordN :: forall r.
HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> r
op (SomeWordN (WordN n
l :: WordN l)) (SomeWordN (WordN n
r :: WordN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> r
op WordN n
l WordN n
r
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeWordN #-}

binSomeWordNR1 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> WordN n) -> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 :: HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
op (SomeWordN (WordN n
l :: WordN l)) (SomeWordN (WordN n
r :: WordN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
op WordN n
l WordN n
r
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeWordNR1 #-}

binSomeWordNR2 :: HasCallStack => (forall n. (KnownNat n, 1 <= n) => WordN n -> WordN n -> (WordN n, WordN n)) -> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 :: HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n)
op (SomeWordN (WordN n
l :: WordN l)) (SomeWordN (WordN n
r :: WordN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl ->
      case forall (n :: Natural).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n)
op WordN n
l WordN n
r of
        (WordN n
a, WordN n
b) -> (forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN WordN n
a, forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN WordN n
b)
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeWordNR2 #-}

instance Eq SomeWordN where
  == :: SomeWordN -> SomeWordN -> Bool
(==) = forall r.
HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Eq a => a -> a -> Bool
(==)
  {-# INLINE (==) #-}
  /= :: SomeWordN -> SomeWordN -> Bool
(/=) = forall r.
HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Eq a => a -> a -> Bool
(/=)
  {-# INLINE (/=) #-}

instance Ord SomeWordN where
  <= :: SomeWordN -> SomeWordN -> Bool
(<=) = forall r.
HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Ord a => a -> a -> Bool
(<=)
  {-# INLINE (<=) #-}
  < :: SomeWordN -> SomeWordN -> Bool
(<) = forall r.
HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Ord a => a -> a -> Bool
(<)
  {-# INLINE (<) #-}
  >= :: SomeWordN -> SomeWordN -> Bool
(>=) = forall r.
HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Ord a => a -> a -> Bool
(>=)
  {-# INLINE (>=) #-}
  > :: SomeWordN -> SomeWordN -> Bool
(>) = forall r.
HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Ord a => a -> a -> Bool
(>)
  {-# INLINE (>) #-}
  max :: SomeWordN -> SomeWordN -> SomeWordN
max = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Ord a => a -> a -> a
max
  {-# INLINE max #-}
  min :: SomeWordN -> SomeWordN -> SomeWordN
min = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Ord a => a -> a -> a
min
  {-# INLINE min #-}
  compare :: SomeWordN -> SomeWordN -> Ordering
compare = forall r.
HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN forall a. Ord a => a -> a -> Ordering
compare
  {-# INLINE compare #-}

instance Lift SomeWordN where
  liftTyped :: forall (m :: * -> *). Quote m => SomeWordN -> Code m SomeWordN
liftTyped (SomeWordN WordN n
w) = [||SomeWordN w||]

instance Hashable SomeWordN where
  Int
s hashWithSalt :: Int -> SomeWordN -> Int
`hashWithSalt` (SomeWordN (WordN n
w :: WordN n)) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` WordN n
w

instance NFData SomeWordN where
  rnf :: SomeWordN -> ()
rnf (SomeWordN WordN n
w) = forall a. NFData a => a -> ()
rnf WordN n
w

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

convertInt :: Num a => L.Lexeme -> ReadPrec a
convertInt :: forall a. Num a => Lexeme -> ReadPrec a
convertInt (L.Number Number
n)
  | Just Integer
i <- Number -> Maybe Integer
L.numberToInteger Number
n = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Num a => Integer -> a
fromInteger Integer
i)
convertInt Lexeme
_ = forall a. ReadPrec a
pfail

instance (KnownNat n, 1 <= n) => Read (WordN n) where
  readPrec :: ReadPrec (WordN n)
readPrec = forall a. Num a => (Lexeme -> ReadPrec a) -> ReadPrec a
readNumber forall a. Num a => Lexeme -> ReadPrec a
convertInt
  readListPrec :: ReadPrec [WordN n]
readListPrec = forall a. Read a => ReadPrec [a]
readListPrecDefault
  readList :: ReadS [WordN n]
readList = forall a. Read a => ReadS [a]
readListDefault

instance Show SomeWordN where
  show :: SomeWordN -> String
show (SomeWordN WordN n
w) = forall a. Show a => a -> String
show WordN n
w

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

-- |
-- A non-indexed version of 'IntN'.
data SomeIntN where
  SomeIntN :: (KnownNat n, 1 <= n) => IntN n -> SomeIntN

unarySomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> r) -> SomeIntN -> r
unarySomeIntN :: forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r
op (SomeIntN (IntN n
w :: IntN w)) = forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r
op IntN n
w
{-# INLINE unarySomeIntN #-}

unarySomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n) -> SomeIntN -> SomeIntN
unarySomeIntNR1 :: (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n
op (SomeIntN (IntN n
w :: IntN w)) = forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n
op IntN n
w
{-# INLINE unarySomeIntNR1 #-}

binSomeIntN :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> r) -> SomeIntN -> SomeIntN -> r
binSomeIntN :: forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> r
op (SomeIntN (IntN n
l :: IntN l)) (SomeIntN (IntN n
r :: IntN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> r
op IntN n
l IntN n
r
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeIntN #-}

binSomeIntNR1 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> IntN n) -> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 :: (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
op (SomeIntN (IntN n
l :: IntN l)) (SomeIntN (IntN n
r :: IntN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
op IntN n
l IntN n
r
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeIntNR1 #-}

binSomeIntNR2 :: (forall n. (KnownNat n, 1 <= n) => IntN n -> IntN n -> (IntN n, IntN n)) -> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 :: (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n)
op (SomeIntN (IntN n
l :: IntN l)) (SomeIntN (IntN n
r :: IntN r)) =
  case forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> *)
       (proxy2 :: Natural -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl ->
      case forall (n :: Natural).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n)
op IntN n
l IntN n
r of
        (IntN n
a, IntN n
b) -> (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN IntN n
a, forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN IntN n
b)
    Maybe (n :~: n)
Nothing -> forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeIntNR2 #-}

instance Eq SomeIntN where
  == :: SomeIntN -> SomeIntN -> Bool
(==) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Eq a => a -> a -> Bool
(==)
  {-# INLINE (==) #-}
  /= :: SomeIntN -> SomeIntN -> Bool
(/=) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Eq a => a -> a -> Bool
(/=)
  {-# INLINE (/=) #-}

instance Ord SomeIntN where
  <= :: SomeIntN -> SomeIntN -> Bool
(<=) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Ord a => a -> a -> Bool
(<=)
  {-# INLINE (<=) #-}
  < :: SomeIntN -> SomeIntN -> Bool
(<) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Ord a => a -> a -> Bool
(<)
  {-# INLINE (<) #-}
  >= :: SomeIntN -> SomeIntN -> Bool
(>=) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Ord a => a -> a -> Bool
(>=)
  {-# INLINE (>=) #-}
  > :: SomeIntN -> SomeIntN -> Bool
(>) = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Ord a => a -> a -> Bool
(>)
  {-# INLINE (>) #-}
  max :: SomeIntN -> SomeIntN -> SomeIntN
max = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Ord a => a -> a -> a
max
  {-# INLINE max #-}
  min :: SomeIntN -> SomeIntN -> SomeIntN
min = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Ord a => a -> a -> a
min
  {-# INLINE min #-}
  compare :: SomeIntN -> SomeIntN -> Ordering
compare = forall r.
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall a. Ord a => a -> a -> Ordering
compare
  {-# INLINE compare #-}

instance Lift SomeIntN where
  liftTyped :: forall (m :: * -> *). Quote m => SomeIntN -> Code m SomeIntN
liftTyped (SomeIntN IntN n
w) = [||SomeIntN w||]

instance Hashable SomeIntN where
  Int
s hashWithSalt :: Int -> SomeIntN -> Int
`hashWithSalt` (SomeIntN (IntN n
w :: IntN n)) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` IntN n
w

instance NFData SomeIntN where
  rnf :: SomeIntN -> ()
rnf (SomeIntN IntN n
w) = forall a. NFData a => a -> ()
rnf IntN n
w

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

instance (KnownNat n, 1 <= n) => Read (IntN n) where
  readPrec :: ReadPrec (IntN n)
readPrec = forall a. Num a => (Lexeme -> ReadPrec a) -> ReadPrec a
readNumber forall a. Num a => Lexeme -> ReadPrec a
convertInt
  readListPrec :: ReadPrec [IntN n]
readListPrec = forall a. Read a => ReadPrec [a]
readListPrecDefault
  readList :: ReadS [IntN n]
readList = forall a. Read a => ReadS [a]
readListDefault

instance Show SomeIntN where
  show :: SomeIntN -> String
show (SomeIntN IntN n
w) = forall a. Show a => a -> String
show IntN n
w

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

  -- shift use default implementation
  -- rotate use default implementation
  zeroBits :: WordN n
zeroBits = forall (n :: Natural). Integer -> WordN n
WordN Integer
0
  bit :: Int -> WordN n
bit Int
i
    | Int
i forall a. Ord a => a -> a -> Bool
< Int
0 Bool -> Bool -> Bool
|| Int
i forall a. Ord a => a -> a -> Bool
>= forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) = forall a. Bits a => a
zeroBits
    | Bool
otherwise = forall (n :: Natural). Integer -> WordN n
WordN (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 = forall (n :: Natural). Integer -> WordN n
WordN (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) = forall a. Bits a => a -> Int -> Bool
testBit Integer
a
  bitSizeMaybe :: WordN n -> Maybe Int
bitSizeMaybe WordN n
_ = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  bitSize :: WordN n -> Int
bitSize WordN n
_ = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (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 = forall (n :: Natural). Integer -> WordN n
WordN (Integer
a forall a. Bits a => a -> Int -> a
`shiftL` Int
i) forall a. Bits a => a -> a -> a
.&. forall a. Bounded a => a
maxBound

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

instance Bits SomeWordN where
  .&. :: SomeWordN -> SomeWordN -> SomeWordN
(.&.) = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Bits a => a -> a -> a
(.&.)
  .|. :: SomeWordN -> SomeWordN -> SomeWordN
(.|.) = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Bits a => a -> a -> a
(.|.)
  xor :: SomeWordN -> SomeWordN -> SomeWordN
xor = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Bits a => a -> a -> a
xor
  complement :: SomeWordN -> SomeWordN
complement = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall a. Bits a => a -> a
complement
  shift :: SomeWordN -> Int -> SomeWordN
shift SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`shift` Int
i) SomeWordN
s
  rotate :: SomeWordN -> Int -> SomeWordN
rotate SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`rotate` Int
i) SomeWordN
s
  zeroBits :: SomeWordN
zeroBits = forall a. HasCallStack => String -> a
error String
"zeroBits is not defined for SomeWordN as no bitwidth is known"
  bit :: Int -> SomeWordN
bit = forall a. HasCallStack => String -> a
error String
"bit is not defined for SomeWordN as no bitwidth is known"
  setBit :: SomeWordN -> Int -> SomeWordN
setBit SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`setBit` Int
i) SomeWordN
s
  clearBit :: SomeWordN -> Int -> SomeWordN
clearBit SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`clearBit` Int
i) SomeWordN
s
  complementBit :: SomeWordN -> Int -> SomeWordN
complementBit SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`complementBit` Int
i) SomeWordN
s
  testBit :: SomeWordN -> Int -> Bool
testBit SomeWordN
s Int
i = forall r.
HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN (forall a. Bits a => a -> Int -> Bool
`testBit` Int
i) SomeWordN
s
  bitSizeMaybe :: SomeWordN -> Maybe Int
bitSizeMaybe (SomeWordN (WordN n
n :: WordN n)) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal WordN n
n
  bitSize :: SomeWordN -> Int
bitSize (SomeWordN (WordN n
n :: WordN n)) = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal WordN n
n
  isSigned :: SomeWordN -> Bool
isSigned SomeWordN
_ = Bool
False
  shiftL :: SomeWordN -> Int -> SomeWordN
shiftL SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`shiftL` Int
i) SomeWordN
s
  unsafeShiftL :: SomeWordN -> Int -> SomeWordN
unsafeShiftL SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
i) SomeWordN
s
  shiftR :: SomeWordN -> Int -> SomeWordN
shiftR SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`shiftR` Int
i) SomeWordN
s
  unsafeShiftR :: SomeWordN -> Int -> SomeWordN
unsafeShiftR SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`unsafeShiftR` Int
i) SomeWordN
s
  rotateL :: SomeWordN -> Int -> SomeWordN
rotateL SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`rotateL` Int
i) SomeWordN
s
  rotateR :: SomeWordN -> Int -> SomeWordN
rotateR SomeWordN
s Int
i = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 (forall a. Bits a => a -> Int -> a
`rotateR` Int
i) SomeWordN
s
  popCount :: SomeWordN -> Int
popCount = forall r.
HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall a. Bits a => a -> Int
popCount

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

instance FiniteBits SomeWordN where
  finiteBitSize :: SomeWordN -> Int
finiteBitSize (SomeWordN (WordN n
n :: WordN n)) = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal WordN n
n
  countLeadingZeros :: SomeWordN -> Int
countLeadingZeros = forall r.
HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall b. FiniteBits b => b -> Int
countLeadingZeros
  countTrailingZeros :: SomeWordN -> Int
countTrailingZeros = forall r.
HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall b. FiniteBits b => b -> Int
countTrailingZeros

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

instance Enum SomeWordN where
  toEnum :: Int -> SomeWordN
toEnum = forall a. HasCallStack => String -> a
error String
"SomeWordN is not really a Enum type as the bit width is unknown, please consider using WordN instead"
  fromEnum :: SomeWordN -> Int
fromEnum = forall a. HasCallStack => String -> a
error String
"SomeWordN is not really a Enum type as the bit width is unknown, please consider using WordN instead"

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

instance Real SomeWordN where
  toRational :: SomeWordN -> Rational
toRational = forall r.
HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall a. Real a => a -> Rational
toRational

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

instance Integral SomeWordN where
  quot :: SomeWordN -> SomeWordN -> SomeWordN
quot = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Integral a => a -> a -> a
quot
  rem :: SomeWordN -> SomeWordN -> SomeWordN
rem = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Integral a => a -> a -> a
rem
  quotRem :: SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
quotRem = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 forall a. Integral a => a -> a -> (a, a)
quotRem
  div :: SomeWordN -> SomeWordN -> SomeWordN
div = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Integral a => a -> a -> a
div
  mod :: SomeWordN -> SomeWordN -> SomeWordN
mod = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Integral a => a -> a -> a
mod
  divMod :: SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
divMod = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 forall a. Integral a => a -> a -> (a, a)
divMod
  toInteger :: SomeWordN -> Integer
toInteger = forall r.
HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN forall a. Integral a => a -> Integer
toInteger

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

instance Num SomeWordN where
  + :: SomeWordN -> SomeWordN -> SomeWordN
(+) = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Num a => a -> a -> a
(+)
  (-) = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 (-)
  * :: SomeWordN -> SomeWordN -> SomeWordN
(*) = HasCallStack =>
(forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 forall a. Num a => a -> a -> a
(*)
  negate :: SomeWordN -> SomeWordN
negate = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall a. Num a => a -> a
negate
  abs :: SomeWordN -> SomeWordN
abs = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall a. Num a => a -> a
abs
  signum :: SomeWordN -> SomeWordN
signum = HasCallStack =>
(forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> WordN n)
-> SomeWordN -> SomeWordN
unarySomeWordNR1 forall a. Num a => a -> a
signum
  fromInteger :: Integer -> SomeWordN
fromInteger = forall a. HasCallStack => String -> a
error String
"fromInteger is not defined for SomeWordN as no bitwidth is known"

minusOneIntN :: forall proxy n. KnownNat n => proxy n -> IntN n
minusOneIntN :: forall (proxy :: Natural -> *) (n :: Natural).
KnownNat n =>
proxy n -> IntN n
minusOneIntN proxy n
_ = forall (n :: Natural). Integer -> IntN n
IntN (Integer
1 forall a. Bits a => a -> Int -> a
`shiftL` forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) 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 = forall (n :: Natural). Integer -> IntN n
IntN (Integer
a forall a. Bits a => a -> a -> a
.&. Integer
b)
  IntN Integer
a .|. :: IntN n -> IntN n -> IntN n
.|. IntN Integer
b = forall (n :: Natural). Integer -> IntN n
IntN (Integer
a forall a. Bits a => a -> a -> a
.|. Integer
b)
  IntN Integer
a xor :: IntN n -> IntN n -> IntN n
`xor` IntN Integer
b = forall (n :: Natural). Integer -> IntN n
IntN (Integer
a forall a. Bits a => a -> a -> a
`xor` Integer
b)
  complement :: IntN n -> IntN n
complement IntN n
a = forall (proxy :: Natural -> *) (n :: Natural).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (forall {k} (t :: k). Proxy t
Proxy :: Proxy n) forall a. Bits a => a -> a -> a
`xor` IntN n
a

  -- shift use default implementation
  -- rotate use default implementation
  zeroBits :: IntN n
zeroBits = forall (n :: Natural). Integer -> IntN n
IntN Integer
0
  bit :: Int -> IntN n
bit Int
i = forall (n :: Natural). Integer -> IntN n
IntN (forall (n :: Natural). WordN n -> Integer
unWordN (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 = forall (n :: Natural). Integer -> IntN n
IntN (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) = forall a. Bits a => a -> Int -> Bool
testBit Integer
a
  bitSizeMaybe :: IntN n -> Maybe Int
bitSizeMaybe IntN n
_ = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
  bitSize :: IntN n -> Int
bitSize IntN n
_ = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (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 = forall (n :: Natural). Integer -> IntN n
IntN (forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ (forall (n :: Natural). Integer -> WordN n
WordN Integer
a :: 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 forall a. Ord a => a -> a -> Bool
>= Int
n = if Bool
b then forall (n :: Natural). Integer -> IntN n
IntN (Integer
maxi forall a. Num a => a -> a -> a
- Integer
1) else forall (n :: Natural). Integer -> IntN n
IntN Integer
0
    | Bool
otherwise = if Bool
b then forall (n :: Natural). Integer -> IntN n
IntN (Integer
maxi forall a. Num a => a -> a -> a
- Integer
noi forall a. Num a => a -> a -> a
+ (Integer
i forall a. Bits a => a -> Int -> a
`shiftR` Int
k)) else forall (n :: Natural). Integer -> IntN n
IntN (Integer
i forall a. Bits a => a -> Int -> a
`shiftR` Int
k)
    where
      b :: Bool
b = forall a. Bits a => a -> Int -> Bool
testBit Integer
i (Int
n forall a. Num a => a -> a -> a
- Int
1)
      n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
      maxi :: Integer
maxi = (Integer
1 :: Integer) forall a. Bits a => a -> Int -> a
`shiftL` Int
n
      noi :: Integer
noi = (Integer
1 :: Integer) forall a. Bits a => a -> Int -> a
`shiftL` (Int
n 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 = forall (n :: Natural). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> a
rotateL (forall (n :: Natural). Integer -> WordN n
WordN Integer
i :: WordN n) Int
k
  rotateR :: IntN n -> Int -> IntN n
rotateR (IntN Integer
i) Int
k = forall (n :: Natural). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> a
rotateR (forall (n :: Natural). Integer -> WordN n
WordN Integer
i :: WordN n) Int
k
  popCount :: IntN n -> Int
popCount (IntN Integer
i) = forall a. Bits a => a -> Int
popCount Integer
i

instance Bits SomeIntN where
  .&. :: SomeIntN -> SomeIntN -> SomeIntN
(.&.) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Bits a => a -> a -> a
(.&.)
  .|. :: SomeIntN -> SomeIntN -> SomeIntN
(.|.) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Bits a => a -> a -> a
(.|.)
  xor :: SomeIntN -> SomeIntN -> SomeIntN
xor = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Bits a => a -> a -> a
xor
  complement :: SomeIntN -> SomeIntN
complement = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall a. Bits a => a -> a
complement
  shift :: SomeIntN -> Int -> SomeIntN
shift SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`shift` Int
i) SomeIntN
s
  rotate :: SomeIntN -> Int -> SomeIntN
rotate SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`rotate` Int
i) SomeIntN
s
  zeroBits :: SomeIntN
zeroBits = forall a. HasCallStack => String -> a
error String
"zeroBits is not defined for SomeIntN as no bitwidth is known"
  bit :: Int -> SomeIntN
bit = forall a. HasCallStack => String -> a
error String
"bit is not defined for SomeIntN as no bitwidth is known"
  setBit :: SomeIntN -> Int -> SomeIntN
setBit SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`setBit` Int
i) SomeIntN
s
  clearBit :: SomeIntN -> Int -> SomeIntN
clearBit SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`clearBit` Int
i) SomeIntN
s
  complementBit :: SomeIntN -> Int -> SomeIntN
complementBit SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`complementBit` Int
i) SomeIntN
s
  testBit :: SomeIntN -> Int -> Bool
testBit SomeIntN
s Int
i = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN (forall a. Bits a => a -> Int -> Bool
`testBit` Int
i) SomeIntN
s
  bitSizeMaybe :: SomeIntN -> Maybe Int
bitSizeMaybe (SomeIntN (IntN n
n :: IntN n)) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal IntN n
n
  bitSize :: SomeIntN -> Int
bitSize (SomeIntN (IntN n
n :: IntN n)) = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal IntN n
n
  isSigned :: SomeIntN -> Bool
isSigned SomeIntN
_ = Bool
False
  shiftL :: SomeIntN -> Int -> SomeIntN
shiftL SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`shiftL` Int
i) SomeIntN
s
  unsafeShiftL :: SomeIntN -> Int -> SomeIntN
unsafeShiftL SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`unsafeShiftL` Int
i) SomeIntN
s
  shiftR :: SomeIntN -> Int -> SomeIntN
shiftR SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`shiftR` Int
i) SomeIntN
s
  unsafeShiftR :: SomeIntN -> Int -> SomeIntN
unsafeShiftR SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`unsafeShiftR` Int
i) SomeIntN
s
  rotateL :: SomeIntN -> Int -> SomeIntN
rotateL SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`rotateL` Int
i) SomeIntN
s
  rotateR :: SomeIntN -> Int -> SomeIntN
rotateR SomeIntN
s Int
i = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 (forall a. Bits a => a -> Int -> a
`rotateR` Int
i) SomeIntN
s
  popCount :: SomeIntN -> Int
popCount = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall a. Bits a => a -> Int
popCount

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

instance FiniteBits SomeIntN where
  finiteBitSize :: SomeIntN -> Int
finiteBitSize (SomeIntN (IntN n
n :: IntN n)) = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal IntN n
n
  countLeadingZeros :: SomeIntN -> Int
countLeadingZeros = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall b. FiniteBits b => b -> Int
countLeadingZeros
  countTrailingZeros :: SomeIntN -> Int
countTrailingZeros = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall b. FiniteBits b => b -> Int
countTrailingZeros

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

instance Enum SomeIntN where
  toEnum :: Int -> SomeIntN
toEnum = forall a. HasCallStack => String -> a
error String
"SomeIntN is not really a Enum type as the bit width is unknown, please consider using IntN instead"
  fromEnum :: SomeIntN -> Int
fromEnum = forall a. HasCallStack => String -> a
error String
"SomeIntN is not really a Enum type as the bit width is unknown, please consider using IntN instead"

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

instance Real SomeIntN where
  toRational :: SomeIntN -> Rational
toRational = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall a. Real a => a -> Rational
toRational

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

instance Integral SomeIntN where
  quot :: SomeIntN -> SomeIntN -> SomeIntN
quot = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Integral a => a -> a -> a
quot
  rem :: SomeIntN -> SomeIntN -> SomeIntN
rem = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Integral a => a -> a -> a
rem
  quotRem :: SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
quotRem = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 forall a. Integral a => a -> a -> (a, a)
quotRem
  div :: SomeIntN -> SomeIntN -> SomeIntN
div = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Integral a => a -> a -> a
div
  mod :: SomeIntN -> SomeIntN -> SomeIntN
mod = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Integral a => a -> a -> a
mod
  divMod :: SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
divMod = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 forall a. Integral a => a -> a -> (a, a)
divMod
  toInteger :: SomeIntN -> Integer
toInteger = forall r.
(forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall a. Integral a => a -> Integer
toInteger

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

instance Num SomeIntN where
  + :: SomeIntN -> SomeIntN -> SomeIntN
(+) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Num a => a -> a -> a
(+)
  (-) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 (-)
  * :: SomeIntN -> SomeIntN -> SomeIntN
(*) = (forall (n :: Natural).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall a. Num a => a -> a -> a
(*)
  negate :: SomeIntN -> SomeIntN
negate = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall a. Num a => a -> a
negate
  abs :: SomeIntN -> SomeIntN
abs = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall a. Num a => a -> a
abs
  signum :: SomeIntN -> SomeIntN
signum = (forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall a. Num a => a -> a
signum
  fromInteger :: Integer -> SomeIntN
fromInteger = forall a. HasCallStack => String -> a
error String
"fromInteger is not defined for SomeIntN as no bitwidth is known"

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 forall a. Ord a => a -> a -> Bool
<= Integer
b
    where
      n :: Int
n = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
      as :: Bool
as = forall a. Bits a => a -> Int -> Bool
testBit Integer
a (Int
n forall a. Num a => a -> a -> a
- Int
1)
      bs :: Bool
bs = forall a. Bits a => a -> Int -> Bool
testBit Integer
b (Int
n forall a. Num a => a -> a -> a
- Int
1)

instance SizedBV WordN where
  sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r)
  sizedBVConcat :: forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
sizedBVConcat (WordN Integer
a) (WordN Integer
b) = forall (n :: Natural). Integer -> WordN n
WordN ((Integer
a forall a. Bits a => a -> Int -> a
`shiftL` forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy r))) forall a. Bits a => a -> a -> a
.|. Integer
b)
  sizedBVZext :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVZext proxy r
_ (WordN Integer
v) = forall (n :: Natural). Integer -> WordN n
WordN Integer
v
  sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> WordN l -> WordN r
  sizedBVSext :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVSext proxy r
pr (WordN Integer
v) = if Bool
s then forall (n :: Natural). Integer -> WordN n
WordN (Integer
maxi forall a. Num a => a -> a -> a
- Integer
noi forall a. Num a => a -> a -> a
+ Integer
v) else forall (n :: Natural). Integer -> WordN n
WordN Integer
v
    where
      r :: Int
r = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal proxy r
pr
      l :: Int
l = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy l)
      s :: Bool
s = forall a. Bits a => a -> Int -> Bool
testBit Integer
v (Int
l forall a. Num a => a -> a -> a
- Int
1)
      maxi :: Integer
maxi = (Integer
1 :: Integer) forall a. Bits a => a -> Int -> a
`shiftL` Int
r
      noi :: Integer
noi = (Integer
1 :: Integer) forall a. Bits a => a -> Int -> a
`shiftL` Int
l
  sizedBVExt :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
sizedBVExt = forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext
  sizedBVSelect ::
    forall n ix w proxy.
    (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>
    proxy ix ->
    proxy w ->
    WordN n ->
    WordN w
  sizedBVSelect :: forall (n :: Natural) (ix :: Natural) (w :: Natural)
       (proxy :: Natural -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
proxy ix -> proxy w -> WordN n -> WordN w
sizedBVSelect proxy ix
pix proxy w
pw (WordN Integer
v) = forall (n :: Natural). Integer -> WordN n
WordN ((Integer
v forall a. Bits a => a -> Int -> a
`shiftR` Int
ix) forall a. Bits a => a -> a -> a
.&. Integer
mask)
    where
      ix :: Int
ix = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal proxy ix
pix
      w :: Int
w = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal proxy w
pw
      mask :: Integer
mask = (Integer
1 forall a. Bits a => a -> Int -> a
`shiftL` Int
w) forall a. Num a => a -> a -> a
- Integer
1

instance SizedBV IntN where
  sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => IntN l -> IntN r -> IntN (l + r)
  sizedBVConcat :: forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
IntN l -> IntN r -> IntN (l + r)
sizedBVConcat (IntN Integer
a) (IntN Integer
b) = forall (n :: Natural). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat (forall (n :: Natural). Integer -> WordN n
WordN Integer
a :: WordN l) (forall (n :: Natural). Integer -> WordN n
WordN Integer
b :: WordN r)
  sizedBVZext :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVZext proxy r
_ (IntN Integer
v) = forall (n :: Natural). Integer -> IntN n
IntN Integer
v
  sizedBVSext :: forall l r proxy. (KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) => proxy r -> IntN l -> IntN r
  sizedBVSext :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVSext proxy r
pr (IntN Integer
v) = forall (n :: Natural). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext proxy r
pr (forall (n :: Natural). Integer -> WordN n
WordN Integer
v :: WordN l)
  sizedBVExt :: forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> IntN l -> IntN r
sizedBVExt = forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext
  sizedBVSelect ::
    forall n ix w proxy.
    (KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w, ix + w <= n) =>
    proxy ix ->
    proxy w ->
    IntN n ->
    IntN w
  sizedBVSelect :: forall (n :: Natural) (ix :: Natural) (w :: Natural)
       (proxy :: Natural -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
proxy ix -> proxy w -> IntN n -> IntN w
sizedBVSelect proxy ix
pix proxy w
pw (IntN Integer
v) = forall (n :: Natural). Integer -> IntN n
IntN forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). WordN n -> Integer
unWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural) (proxy :: Natural -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
proxy ix -> proxy w -> bv n -> bv w
sizedBVSelect proxy ix
pix proxy w
pw (forall (n :: Natural). Integer -> WordN n
WordN Integer
v :: WordN n)

instance SomeBV SomeWordN where
  someBVConcat :: SomeWordN -> SomeWordN -> SomeWordN
someBVConcat (SomeWordN (WordN n
a :: WordN l)) (SomeWordN (WordN n
b :: WordN r)) =
    case (forall (m :: Natural) (n :: Natural) (p :: Natural -> *)
       (q :: Natural -> *).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r), forall {k} (m :: Natural) (n :: Natural) (r :: k).
KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd @l @r forall (n :: Natural). KnownNat n => KnownProof n
KnownProof forall (n :: Natural). KnownNat n => KnownProof n
KnownProof) of
      (LeqProof 1 (n + n)
LeqProof, KnownProof (n + n)
KnownProof) ->
        forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat WordN n
a WordN n
b
  someBVZext :: forall (p :: Natural -> *) (l :: Natural).
KnownNat l =>
p l -> SomeWordN -> SomeWordN
someBVZext (p l
p :: p l) (SomeWordN (WordN n
a :: WordN n))
    | Natural
l forall a. Ord a => a -> a -> Bool
< Natural
n = forall a. HasCallStack => String -> a
error String
"someBVZext: trying to zero extend a value to a smaller size"
    | Bool
otherwise =
        case (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @n @l) of
          (LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext p l
p WordN n
a
    where
      l :: Natural
l = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal p l
p
      n :: Natural
n = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
  someBVSext :: forall (p :: Natural -> *) (l :: Natural).
KnownNat l =>
p l -> SomeWordN -> SomeWordN
someBVSext (p l
p :: p l) (SomeWordN (WordN n
a :: WordN n))
    | Natural
l forall a. Ord a => a -> a -> Bool
< Natural
n = forall a. HasCallStack => String -> a
error String
"someBVSext: trying to zero extend a value to a smaller size"
    | Bool
otherwise =
        case (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @n @l) of
          (LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext p l
p WordN n
a
    where
      l :: Natural
l = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal p l
p
      n :: Natural
n = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
  someBVExt :: forall (p :: Natural -> *) (l :: Natural).
KnownNat l =>
p l -> SomeWordN -> SomeWordN
someBVExt = forall bv (p :: Natural -> *) (l :: Natural).
(SomeBV bv, KnownNat l) =>
p l -> bv -> bv
someBVZext
  someBVSelect :: forall (p :: Natural -> *) (ix :: Natural) (q :: Natural -> *)
       (w :: Natural).
(KnownNat ix, KnownNat w) =>
p ix -> q w -> SomeWordN -> SomeWordN
someBVSelect (p ix
p :: p ix) (q w
q :: q w) (SomeWordN (WordN n
a :: WordN n))
    | Natural
ix forall a. Num a => a -> a -> a
+ Natural
w forall a. Ord a => a -> a -> Bool
> Natural
n = forall a. HasCallStack => String -> a
error String
"someBVSelect: trying to select a bitvector outside the bounds of the input"
    | Natural
w forall a. Eq a => a -> a -> Bool
== Natural
0 = forall a. HasCallStack => String -> a
error String
"someBVSelect: trying to select a bitvector of size 0"
    | Bool
otherwise =
        case (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @w, forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @(ix + w) @n) of
          (LeqProof 1 w
LeqProof, LeqProof (ix + w) n
LeqProof) -> forall (n :: Natural). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural) (proxy :: Natural -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
proxy ix -> proxy w -> bv n -> bv w
sizedBVSelect (forall {k} (t :: k). Proxy t
Proxy @ix) (forall {k} (t :: k). Proxy t
Proxy @w) WordN n
a
    where
      ix :: Natural
ix = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal p ix
p
      w :: Natural
w = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal q w
q
      n :: Natural
n = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n)

instance SomeBV SomeIntN where
  someBVConcat :: SomeIntN -> SomeIntN -> SomeIntN
someBVConcat (SomeIntN (IntN n
a :: IntN l)) (SomeIntN (IntN n
b :: IntN r)) =
    case (forall (m :: Natural) (n :: Natural) (p :: Natural -> *)
       (q :: Natural -> *).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos (forall {k} (t :: k). Proxy t
Proxy @l) (forall {k} (t :: k). Proxy t
Proxy @r), forall {k} (m :: Natural) (n :: Natural) (r :: k).
KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd (forall (n :: Natural). KnownNat n => KnownProof n
KnownProof @l) (forall (n :: Natural). KnownNat n => KnownProof n
KnownProof @r)) of
      (LeqProof 1 (n + n)
LeqProof, KnownProof (n + n)
KnownProof) ->
        forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat IntN n
a IntN n
b
  someBVZext :: forall (p :: Natural -> *) (l :: Natural).
KnownNat l =>
p l -> SomeIntN -> SomeIntN
someBVZext (p l
p :: p l) (SomeIntN (IntN n
a :: IntN n))
    | Natural
l forall a. Ord a => a -> a -> Bool
< Natural
n = forall a. HasCallStack => String -> a
error String
"someBVZext: trying to zero extend a value to a smaller size"
    | Bool
otherwise =
        case (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @n @l) of
          (LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext p l
p IntN n
a
    where
      l :: Natural
l = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal p l
p
      n :: Natural
n = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
  someBVSext :: forall (p :: Natural -> *) (l :: Natural).
KnownNat l =>
p l -> SomeIntN -> SomeIntN
someBVSext (p l
p :: p l) (SomeIntN (IntN n
a :: IntN n))
    | Natural
l forall a. Ord a => a -> a -> Bool
< Natural
n = forall a. HasCallStack => String -> a
error String
"someBVSext: trying to zero extend a value to a smaller size"
    | Bool
otherwise =
        case (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @n @l) of
          (LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext p l
p IntN n
a
    where
      l :: Natural
l = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal p l
p
      n :: Natural
n = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n)
  someBVExt :: forall (p :: Natural -> *) (l :: Natural).
KnownNat l =>
p l -> SomeIntN -> SomeIntN
someBVExt = forall bv (p :: Natural -> *) (l :: Natural).
(SomeBV bv, KnownNat l) =>
p l -> bv -> bv
someBVZext
  someBVSelect :: forall (p :: Natural -> *) (ix :: Natural) (q :: Natural -> *)
       (w :: Natural).
(KnownNat ix, KnownNat w) =>
p ix -> q w -> SomeIntN -> SomeIntN
someBVSelect (p ix
p :: p ix) (q w
q :: q w) (SomeIntN (IntN n
a :: IntN n))
    | Natural
ix forall a. Num a => a -> a -> a
+ Natural
w forall a. Ord a => a -> a -> Bool
> Natural
n = forall a. HasCallStack => String -> a
error String
"someBVSelect: trying to select a bitvector outside the bounds of the input"
    | Natural
w forall a. Eq a => a -> a -> Bool
== Natural
0 = forall a. HasCallStack => String -> a
error String
"someBVSelect: trying to select a bitvector of size 0"
    | Bool
otherwise =
        case (forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @1 @w, forall (m :: Natural) (n :: Natural). LeqProof m n
unsafeLeqProof @(ix + w) @n) of
          (LeqProof 1 w
LeqProof, LeqProof (ix + w) n
LeqProof) -> forall (n :: Natural). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN forall a b. (a -> b) -> a -> b
$ forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural) (proxy :: Natural -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
proxy ix -> proxy w -> bv n -> bv w
sizedBVSelect (forall {k} (t :: k). Proxy t
Proxy @ix) (forall {k} (t :: k). Proxy t
Proxy @w) IntN n
a
    where
      ix :: Natural
ix = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal p ix
p
      w :: Natural
w = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal q w
q
      n :: Natural
n = forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal (forall {k} (t :: k). Proxy t
Proxy @n)