{-# 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 StandaloneDeriving #-}
{-# 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.Applicative (Alternative ((<|>)))
import Control.DeepSeq (NFData (rnf))
import Control.Exception
  ( ArithException (Overflow),
    Exception (displayException),
    throw,
  )
import Data.Bits
  ( Bits
      ( bit,
        bitSize,
        bitSizeMaybe,
        clearBit,
        complement,
        complementBit,
        isSigned,
        popCount,
        rotate,
        rotateL,
        rotateR,
        setBit,
        shift,
        shiftL,
        shiftR,
        testBit,
        unsafeShiftL,
        unsafeShiftR,
        xor,
        zeroBits,
        (.&.),
        (.|.)
      ),
    FiniteBits (countLeadingZeros, countTrailingZeros, finiteBitSize),
  )
import Data.Hashable (Hashable (hashWithSalt))
import Data.Maybe (fromMaybe, isJust)
import Data.Proxy (Proxy (Proxy))
import Data.Typeable (type (:~:) (Refl))
import GHC.Enum
  ( boundedEnumFrom,
    boundedEnumFromThen,
    predError,
    succError,
    toEnumError,
  )
import GHC.Generics (Generic)
import GHC.Read
  ( Read (readListPrec, readPrec),
    parens,
    readListDefault,
    readListPrecDefault,
    readNumber,
  )
import GHC.Real ((%))
import GHC.TypeNats
  ( KnownNat,
    Nat,
    natVal,
    sameNat,
    type (+),
    type (<=),
  )
import Grisette.Core.Data.Class.BitVector
  ( BV (bvConcat, bvExt, bvSelect, bvSext, bvZext),
    SizedBV
      ( sizedBVConcat,
        sizedBVExt,
        sizedBVSelect,
        sizedBVSext,
        sizedBVZext
      ),
  )
import Grisette.Core.Data.Class.SignConversion
  ( SignConversion (toSigned, toUnsigned),
  )
import Grisette.Core.Data.Class.SymRotate
  ( DefaultFiniteBitsSymRotate (DefaultFiniteBitsSymRotate),
    SymRotate,
  )
import Grisette.Core.Data.Class.SymShift
  ( DefaultFiniteBitsSymShift (DefaultFiniteBitsSymShift),
    SymShift,
  )
import Grisette.Utils.Parameterized
  ( KnownProof (KnownProof),
    LeqProof (LeqProof),
    knownAdd,
    leqAddPos,
    unsafeKnownProof,
    unsafeLeqProof,
  )
import Language.Haskell.TH.Syntax (Lift (liftTyped))
import Numeric (showHex, showIntAtBase)
import qualified Test.QuickCheck as QC
import Text.ParserCombinators.ReadP (string)
import Text.ParserCombinators.ReadPrec
  ( ReadPrec,
    get,
    look,
    pfail,
  )
import Text.Read (lift)
import qualified Text.Read.Lex as L

data BitwidthMismatch = BitwidthMismatch
  deriving (Int -> BitwidthMismatch -> ShowS
[BitwidthMismatch] -> ShowS
BitwidthMismatch -> String
(Int -> BitwidthMismatch -> ShowS)
-> (BitwidthMismatch -> String)
-> ([BitwidthMismatch] -> ShowS)
-> Show BitwidthMismatch
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BitwidthMismatch -> ShowS
showsPrec :: Int -> BitwidthMismatch -> ShowS
$cshow :: BitwidthMismatch -> String
show :: BitwidthMismatch -> String
$cshowList :: [BitwidthMismatch] -> ShowS
showList :: [BitwidthMismatch] -> ShowS
Show, BitwidthMismatch -> BitwidthMismatch -> Bool
(BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> Eq BitwidthMismatch
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BitwidthMismatch -> BitwidthMismatch -> Bool
== :: BitwidthMismatch -> BitwidthMismatch -> Bool
$c/= :: BitwidthMismatch -> BitwidthMismatch -> Bool
/= :: BitwidthMismatch -> BitwidthMismatch -> Bool
Eq, Eq BitwidthMismatch
Eq BitwidthMismatch =>
(BitwidthMismatch -> BitwidthMismatch -> Ordering)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> Bool)
-> (BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch)
-> (BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch)
-> Ord 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
$ccompare :: BitwidthMismatch -> BitwidthMismatch -> Ordering
compare :: BitwidthMismatch -> BitwidthMismatch -> Ordering
$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
>= :: BitwidthMismatch -> BitwidthMismatch -> Bool
$cmax :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
max :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
$cmin :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
min :: BitwidthMismatch -> BitwidthMismatch -> BitwidthMismatch
Ord, (forall x. BitwidthMismatch -> Rep BitwidthMismatch x)
-> (forall x. Rep BitwidthMismatch x -> BitwidthMismatch)
-> Generic BitwidthMismatch
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
$cfrom :: forall x. BitwidthMismatch -> Rep BitwidthMismatch x
from :: forall x. BitwidthMismatch -> Rep BitwidthMismatch x
$cto :: forall x. Rep BitwidthMismatch x -> BitwidthMismatch
to :: forall x. Rep BitwidthMismatch x -> BitwidthMismatch
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 :: Nat). WordN n -> Integer
unWordN :: Integer}
  deriving (WordN n -> WordN n -> Bool
(WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool) -> Eq (WordN n)
forall (n :: Nat). WordN n -> WordN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). WordN n -> WordN n -> Bool
== :: WordN n -> WordN n -> Bool
$c/= :: forall (n :: Nat). WordN n -> WordN n -> Bool
/= :: WordN n -> WordN n -> Bool
Eq, Eq (WordN n)
Eq (WordN n) =>
(WordN n -> WordN n -> Ordering)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> Bool)
-> (WordN n -> WordN n -> WordN n)
-> (WordN n -> WordN n -> WordN n)
-> Ord (WordN n)
WordN n -> WordN n -> Bool
WordN n -> WordN n -> Ordering
WordN n -> WordN n -> WordN n
forall (n :: Nat). Eq (WordN n)
forall (n :: Nat). WordN n -> WordN n -> Bool
forall (n :: Nat). WordN n -> WordN n -> Ordering
forall (n :: Nat). WordN n -> WordN n -> WordN n
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (n :: Nat). WordN n -> WordN n -> Ordering
compare :: WordN n -> WordN n -> Ordering
$c< :: forall (n :: Nat). WordN n -> WordN n -> Bool
< :: WordN n -> WordN n -> Bool
$c<= :: forall (n :: Nat). WordN n -> WordN n -> Bool
<= :: WordN n -> WordN n -> Bool
$c> :: forall (n :: Nat). WordN n -> WordN n -> Bool
> :: WordN n -> WordN n -> Bool
$c>= :: forall (n :: Nat). WordN n -> WordN n -> Bool
>= :: WordN n -> WordN n -> Bool
$cmax :: forall (n :: Nat). WordN n -> WordN n -> WordN n
max :: WordN n -> WordN n -> WordN n
$cmin :: forall (n :: Nat). WordN n -> WordN n -> WordN n
min :: WordN n -> WordN n -> WordN n
Ord, (forall x. WordN n -> Rep (WordN n) x)
-> (forall x. Rep (WordN n) x -> WordN n) -> Generic (WordN n)
forall (n :: Nat) x. Rep (WordN n) x -> WordN n
forall (n :: Nat) x. WordN n -> Rep (WordN n) x
forall x. Rep (WordN n) x -> WordN n
forall x. WordN n -> Rep (WordN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Nat) x. WordN n -> Rep (WordN n) x
from :: forall x. WordN n -> Rep (WordN n) x
$cto :: forall (n :: Nat) x. Rep (WordN n) x -> WordN n
to :: forall x. Rep (WordN n) x -> WordN n
Generic, (forall (m :: * -> *). Quote m => WordN n -> m Exp)
-> (forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n))
-> Lift (WordN n)
forall (n :: Nat) (m :: * -> *). Quote m => WordN n -> m Exp
forall (n :: Nat) (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)
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => WordN n -> m Exp
lift :: forall (m :: * -> *). Quote m => WordN n -> m Exp
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
WordN n -> Code m (WordN n)
liftTyped :: forall (m :: * -> *). Quote m => WordN n -> Code m (WordN n)
Lift, Eq (WordN n)
Eq (WordN n) =>
(Int -> WordN n -> Int) -> (WordN n -> Int) -> Hashable (WordN n)
Int -> WordN n -> Int
WordN n -> Int
forall (n :: Nat). Eq (WordN n)
forall (n :: Nat). Int -> WordN n -> Int
forall (n :: Nat). WordN n -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: forall (n :: Nat). Int -> WordN n -> Int
hashWithSalt :: Int -> WordN n -> Int
$chash :: forall (n :: Nat). WordN n -> Int
hash :: WordN n -> Int
Hashable, WordN n -> ()
(WordN n -> ()) -> NFData (WordN n)
forall (n :: Nat). WordN n -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Nat). WordN n -> ()
rnf :: WordN n -> ()
NFData)

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

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

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

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

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

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

instance Eq SomeWordN where
  SomeWordN (WordN n
l :: WordN l) == :: SomeWordN -> SomeWordN -> Bool
== SomeWordN (WordN n
r :: WordN r) =
    case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
      Just n :~: n
Refl -> WordN n
l WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
== WordN n
WordN n
r
      Maybe (n :~: n)
Nothing -> Bool
False
  {-# INLINE (==) #-}
  SomeWordN (WordN n
l :: WordN l) /= :: SomeWordN -> SomeWordN -> Bool
/= SomeWordN (WordN n
r :: WordN r) =
    case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
      Just n :~: n
Refl -> WordN n
l WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
/= WordN n
WordN n
r
      Maybe (n :~: n)
Nothing -> Bool
True
  {-# INLINE (/=) #-}

instance Ord SomeWordN where
  <= :: SomeWordN -> SomeWordN -> Bool
(<=) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> Bool)
-> SomeWordN -> SomeWordN -> Bool
forall r.
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN WordN n -> WordN n -> Bool
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
  {-# INLINE (<=) #-}
  < :: SomeWordN -> SomeWordN -> Bool
(<) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> Bool)
-> SomeWordN -> SomeWordN -> Bool
forall r.
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN WordN n -> WordN n -> Bool
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool
forall a. Ord a => a -> a -> Bool
(<)
  {-# INLINE (<) #-}
  >= :: SomeWordN -> SomeWordN -> Bool
(>=) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> Bool)
-> SomeWordN -> SomeWordN -> Bool
forall r.
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN WordN n -> WordN n -> Bool
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
  {-# INLINE (>=) #-}
  > :: SomeWordN -> SomeWordN -> Bool
(>) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> Bool)
-> SomeWordN -> SomeWordN -> Bool
forall r.
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN WordN n -> WordN n -> Bool
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Bool
forall a. Ord a => a -> a -> Bool
(>)
  {-# INLINE (>) #-}
  max :: SomeWordN -> SomeWordN -> SomeWordN
max = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Ord a => a -> a -> a
max
  {-# INLINE max #-}
  min :: SomeWordN -> SomeWordN -> SomeWordN
min = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Ord a => a -> a -> a
min
  {-# INLINE min #-}
  compare :: SomeWordN -> SomeWordN -> Ordering
compare = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> Ordering)
-> SomeWordN -> SomeWordN -> Ordering
forall r.
(forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> r)
-> SomeWordN -> SomeWordN -> r
binSomeWordN WordN n -> WordN n -> Ordering
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> Ordering
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) = [||WordN n -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN WordN n
w||]

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

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

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 = a -> ReadPrec a
forall a. a -> ReadPrec a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> a
forall a. Num a => Integer -> a
fromInteger Integer
i)
convertInt Lexeme
_ = ReadPrec a
forall a. ReadPrec a
pfail

readBinary :: (Num a) => ReadPrec a
readBinary :: forall a. Num a => ReadPrec a
readBinary = ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec a -> ReadPrec a) -> ReadPrec a -> ReadPrec a
forall a b. (a -> b) -> a -> b
$ do
  String
r0 <- ReadPrec String
look
  case String
r0 of
    (Char
'-' : String
_) -> do
      Char
_ <- ReadPrec Char
get
      a -> a
forall a. Num a => a -> a
negate (a -> a) -> ReadPrec a -> ReadPrec a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadPrec a -> ReadPrec a
forall a. ReadPrec a -> ReadPrec a
parens ReadPrec a
parse0b
    String
_ -> ReadPrec a
parse0b
  where
    isDigit :: Char -> Bool
isDigit Char
c = Maybe Integer -> Bool
forall a. Maybe a -> Bool
isJust (Char -> Maybe Integer
forall {a}. Num a => Char -> Maybe a
valDig Char
c)
    valDigit :: Char -> a
valDigit Char
c = a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe a
0 (Char -> Maybe a
forall {a}. Num a => Char -> Maybe a
valDig Char
c)
    valDig :: Char -> Maybe a
valDig Char
'0' = a -> Maybe a
forall a. a -> Maybe a
Just a
0
    valDig Char
'1' = a -> Maybe a
forall a. a -> Maybe a
Just a
1
    valDig Char
_ = Maybe a
forall a. Maybe a
Nothing
    parse0b :: ReadPrec a
parse0b = do
      String
_ <- ReadP String -> ReadPrec String
forall a. ReadP a -> ReadPrec a
Text.Read.lift (ReadP String -> ReadPrec String)
-> ReadP String -> ReadPrec String
forall a b. (a -> b) -> a -> b
$ String -> ReadP String
string String
"0b"
      Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> ReadPrec Integer -> ReadPrec a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReadP Integer -> ReadPrec Integer
forall a. ReadP a -> ReadPrec a
Text.Read.lift (Integer -> (Char -> Bool) -> (Char -> Int) -> ReadP Integer
forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadP a
L.readIntP Integer
2 Char -> Bool
isDigit Char -> Int
forall {a}. Num a => Char -> a
valDigit)

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

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

-- |
-- Symbolic signed bit vectors.
newtype IntN (n :: Nat) = IntN {forall (n :: Nat). IntN n -> Integer
unIntN :: Integer}
  deriving (IntN n -> IntN n -> Bool
(IntN n -> IntN n -> Bool)
-> (IntN n -> IntN n -> Bool) -> Eq (IntN n)
forall (n :: Nat). IntN n -> IntN n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Nat). IntN n -> IntN n -> Bool
== :: IntN n -> IntN n -> Bool
$c/= :: forall (n :: Nat). IntN n -> IntN n -> Bool
/= :: IntN n -> IntN n -> Bool
Eq, (forall x. IntN n -> Rep (IntN n) x)
-> (forall x. Rep (IntN n) x -> IntN n) -> Generic (IntN n)
forall (n :: Nat) x. Rep (IntN n) x -> IntN n
forall (n :: Nat) x. IntN n -> Rep (IntN n) x
forall x. Rep (IntN n) x -> IntN n
forall x. IntN n -> Rep (IntN n) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Nat) x. IntN n -> Rep (IntN n) x
from :: forall x. IntN n -> Rep (IntN n) x
$cto :: forall (n :: Nat) x. Rep (IntN n) x -> IntN n
to :: forall x. Rep (IntN n) x -> IntN n
Generic, (forall (m :: * -> *). Quote m => IntN n -> m Exp)
-> (forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n))
-> Lift (IntN n)
forall (n :: Nat) (m :: * -> *). Quote m => IntN n -> m Exp
forall (n :: Nat) (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)
$clift :: forall (n :: Nat) (m :: * -> *). Quote m => IntN n -> m Exp
lift :: forall (m :: * -> *). Quote m => IntN n -> m Exp
$cliftTyped :: forall (n :: Nat) (m :: * -> *).
Quote m =>
IntN n -> Code m (IntN n)
liftTyped :: forall (m :: * -> *). Quote m => IntN n -> Code m (IntN n)
Lift, Eq (IntN n)
Eq (IntN n) =>
(Int -> IntN n -> Int) -> (IntN n -> Int) -> Hashable (IntN n)
Int -> IntN n -> Int
IntN n -> Int
forall (n :: Nat). Eq (IntN n)
forall (n :: Nat). Int -> IntN n -> Int
forall (n :: Nat). IntN n -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: forall (n :: Nat). Int -> IntN n -> Int
hashWithSalt :: Int -> IntN n -> Int
$chash :: forall (n :: Nat). IntN n -> Int
hash :: IntN n -> Int
Hashable, IntN n -> ()
(IntN n -> ()) -> NFData (IntN n)
forall (n :: Nat). IntN n -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall (n :: Nat). IntN n -> ()
rnf :: 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 :: Nat). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> r
op (SomeIntN (IntN n
w :: IntN w)) = IntN n -> r
forall (n :: Nat). (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 :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n
op (SomeIntN (IntN n
w :: IntN w)) = IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN (IntN n -> SomeIntN) -> IntN n -> SomeIntN
forall a b. (a -> b) -> a -> b
$ IntN n -> IntN n
forall (n :: Nat). (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 :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r
op (SomeIntN (IntN n
l :: IntN l)) (SomeIntN (IntN n
r :: IntN r)) =
  case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> IntN n -> IntN n -> r
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r
op IntN n
l IntN n
IntN n
r
    Maybe (n :~: n)
Nothing -> BitwidthMismatch -> r
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 :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
op (SomeIntN (IntN n
l :: IntN l)) (SomeIntN (IntN n
r :: IntN r)) =
  case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl -> IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN (IntN n -> SomeIntN) -> IntN n -> SomeIntN
forall a b. (a -> b) -> a -> b
$ IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
op IntN n
l IntN n
IntN n
r
    Maybe (n :~: n)
Nothing -> BitwidthMismatch -> SomeIntN
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 :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 forall (n :: Nat).
(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 Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
    Just n :~: n
Refl ->
      case IntN n -> IntN n -> (IntN n, IntN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n)
op IntN n
l IntN n
IntN n
r of
        (IntN n
a, IntN n
b) -> (IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN IntN n
a, IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN IntN n
b)
    Maybe (n :~: n)
Nothing -> BitwidthMismatch -> (SomeIntN, SomeIntN)
forall a e. Exception e => e -> a
throw BitwidthMismatch
BitwidthMismatch
{-# INLINE binSomeIntNR2 #-}

instance Eq SomeIntN where
  SomeIntN (IntN n
l :: IntN l) == :: SomeIntN -> SomeIntN -> Bool
== SomeIntN (IntN n
r :: IntN r) =
    case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
      Just n :~: n
Refl -> IntN n
l IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
IntN n
r
      Maybe (n :~: n)
Nothing -> Bool
False
  {-# INLINE (==) #-}
  SomeIntN (IntN n
l :: IntN l) /= :: SomeIntN -> SomeIntN -> Bool
/= SomeIntN (IntN n
r :: IntN r) =
    case Proxy n -> Proxy n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
       (proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
sameNat (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r) of
      Just n :~: n
Refl -> IntN n
l IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
/= IntN n
IntN n
r
      Maybe (n :~: n)
Nothing -> Bool
True
  {-# INLINE (/=) #-}

instance Ord SomeIntN where
  <= :: SomeIntN -> SomeIntN -> Bool
(<=) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> Bool)
-> SomeIntN -> SomeIntN -> Bool
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN IntN n -> IntN n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
  {-# INLINE (<=) #-}
  < :: SomeIntN -> SomeIntN -> Bool
(<) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> Bool)
-> SomeIntN -> SomeIntN -> Bool
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN IntN n -> IntN n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> Bool
forall a. Ord a => a -> a -> Bool
(<)
  {-# INLINE (<) #-}
  >= :: SomeIntN -> SomeIntN -> Bool
(>=) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> Bool)
-> SomeIntN -> SomeIntN -> Bool
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN IntN n -> IntN n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> Bool
forall a. Ord a => a -> a -> Bool
(>=)
  {-# INLINE (>=) #-}
  > :: SomeIntN -> SomeIntN -> Bool
(>) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> Bool)
-> SomeIntN -> SomeIntN -> Bool
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN IntN n -> IntN n -> Bool
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> Bool
forall a. Ord a => a -> a -> Bool
(>)
  {-# INLINE (>) #-}
  max :: SomeIntN -> SomeIntN -> SomeIntN
max = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Ord a => a -> a -> a
max
  {-# INLINE max #-}
  min :: SomeIntN -> SomeIntN -> SomeIntN
min = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Ord a => a -> a -> a
min
  {-# INLINE min #-}
  compare :: SomeIntN -> SomeIntN -> Ordering
compare = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> Ordering)
-> SomeIntN -> SomeIntN -> Ordering
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n -> r)
-> SomeIntN -> SomeIntN -> r
binSomeIntN IntN n -> IntN n -> Ordering
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> Ordering
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) = [||IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN IntN n
w||]

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

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

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

instance Show SomeIntN where
  show :: SomeIntN -> String
show (SomeIntN IntN n
w) = IntN n -> String
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 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. Integer
b)
  WordN Integer
a .|. :: WordN n -> WordN n -> WordN n
.|. WordN Integer
b = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.|. Integer
b)
  WordN Integer
a xor :: WordN n -> WordN n -> WordN n
`xor` WordN Integer
b = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
`xor` Integer
b)
  complement :: WordN n -> WordN n
complement WordN n
a = WordN n
forall a. Bounded a => a
maxBound WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
`xor` WordN n
a

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

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

  -- complementBit use default implementation
  testBit :: WordN n -> Int -> Bool
testBit (WordN Integer
a) = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a
  bitSizeMaybe :: WordN n -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (WordN n -> Int) -> WordN n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
  bitSize :: WordN n -> Int
bitSize = WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
  isSigned :: WordN n -> Bool
isSigned WordN n
_ = Bool
False
  shiftL :: WordN n -> Int -> WordN n
shiftL WordN n
w Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize WordN n
w = WordN n
0
  shiftL (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
i) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound

  -- unsafeShiftL use default implementation
  shiftR :: WordN n -> Int -> WordN n
shiftR WordN n
w Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= WordN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize WordN n
w = WordN n
0
  shiftR (WordN Integer
a) Int
i = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
a Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftR` Int
i)

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

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

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

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

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

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

instance Enum SomeWordN where
  toEnum :: Int -> SomeWordN
toEnum = String -> Int -> SomeWordN
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 = String -> SomeWordN -> Int
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 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1

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

instance Integral SomeWordN where
  quot :: SomeWordN -> SomeWordN -> SomeWordN
quot = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
quot
  rem :: SomeWordN -> SomeWordN -> SomeWordN
rem = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
rem
  quotRem :: SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
quotRem = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 WordN n -> WordN n -> (WordN n, WordN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
quotRem
  div :: SomeWordN -> SomeWordN -> SomeWordN
div = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
div
  mod :: SomeWordN -> SomeWordN -> SomeWordN
mod = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> WordN n)
-> SomeWordN -> SomeWordN -> SomeWordN
binSomeWordNR1 WordN n -> WordN n -> WordN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> WordN n
forall a. Integral a => a -> a -> a
mod
  divMod :: SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
divMod = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 WordN n -> WordN n -> (WordN n, WordN n))
-> SomeWordN -> SomeWordN -> (SomeWordN, SomeWordN)
binSomeWordNR2 WordN n -> WordN n -> (WordN n, WordN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
WordN n -> WordN n -> (WordN n, WordN n)
forall a. Integral a => a -> a -> (a, a)
divMod
  toInteger :: SomeWordN -> Integer
toInteger = (forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Integer)
-> SomeWordN -> Integer
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> r)
-> SomeWordN -> r
unarySomeWordN WordN n -> Integer
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> Integer
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 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound
  WordN Integer
x * :: WordN n -> WordN n -> WordN n
* WordN Integer
y = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) WordN n -> WordN n -> WordN n
forall a. Bits a => a -> a -> a
.&. WordN n
forall a. Bounded a => a
maxBound
  WordN Integer
x - :: WordN n -> WordN n -> WordN n
- WordN Integer
y
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
y = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
    | Bool
otherwise = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
  negate :: WordN n -> WordN n
negate (WordN Integer
0) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
  negate WordN n
a = WordN n -> WordN n
forall a. Bits a => a -> a
complement WordN n
a WordN n -> WordN n -> WordN n
forall a. Num a => a -> a -> a
+ Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
1
  abs :: WordN n -> WordN n
abs WordN n
x = WordN n
x
  signum :: WordN n -> WordN n
signum (WordN Integer
0) = WordN n
0
  signum WordN n
_ = WordN n
1
  fromInteger :: Integer -> WordN n
fromInteger !Integer
x
    | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
0
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN (Integer
x Integer -> Integer -> Integer
forall a. Bits a => a -> a -> a
.&. WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (WordN n
forall a. Bounded a => a
maxBound :: WordN n))
    | Bool
otherwise = -Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger (-Integer
x)

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

instance (KnownNat n, 1 <= n) => QC.Arbitrary (WordN n) where
  arbitrary :: Gen (WordN n)
arbitrary = Gen (WordN n)
forall a. (Bounded a, Integral a) => Gen a
QC.arbitrarySizedBoundedIntegral

  -- QC.shrinkIntegral assumes that 2 is representable by the number, which is
  -- not the case for 1-bit bit vector.
  shrink :: WordN n -> [WordN n]
shrink WordN n
i
    | WordN n
i WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
== WordN n
0 = []
    | WordN n
i WordN n -> WordN n -> Bool
forall a. Eq a => a -> a -> Bool
== WordN n
1 = [WordN n
0]
    | Bool
otherwise = WordN n -> [WordN n]
forall a. Integral a => a -> [a]
QC.shrinkIntegral WordN n
i

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

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

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

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

  -- complementBit use default implementation
  testBit :: IntN n -> Int -> Bool
testBit (IntN Integer
a) = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a
  bitSizeMaybe :: IntN n -> Maybe Int
bitSizeMaybe = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (IntN n -> Int) -> IntN n -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
  bitSize :: IntN n -> Int
bitSize = IntN n -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize
  isSigned :: IntN n -> Bool
isSigned IntN n
_ = Bool
True

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

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

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

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

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

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

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

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

instance Enum SomeIntN where
  toEnum :: Int -> SomeIntN
toEnum = String -> Int -> SomeIntN
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 = String -> SomeIntN -> Int
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 = IntN n -> Integer
forall a. Integral a => a -> Integer
toInteger IntN n
i Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
1

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

instance Integral SomeIntN where
  quot :: SomeIntN -> SomeIntN -> SomeIntN
quot = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
quot
  rem :: SomeIntN -> SomeIntN -> SomeIntN
rem = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
rem
  quotRem :: SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
quotRem = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 IntN n -> IntN n -> (IntN n, IntN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n)
forall a. Integral a => a -> a -> (a, a)
quotRem
  div :: SomeIntN -> SomeIntN -> SomeIntN
div = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
div
  mod :: SomeIntN -> SomeIntN -> SomeIntN
mod = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Integral a => a -> a -> a
mod
  divMod :: SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
divMod = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> (IntN n, IntN n))
-> SomeIntN -> SomeIntN -> (SomeIntN, SomeIntN)
binSomeIntNR2 IntN n -> IntN n -> (IntN n, IntN n)
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> (IntN n, IntN n)
forall a. Integral a => a -> a -> (a, a)
divMod
  toInteger :: SomeIntN -> Integer
toInteger = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Integer)
-> SomeIntN -> Integer
forall r.
(forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> r)
-> SomeIntN -> r
unarySomeIntN IntN n -> Integer
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> Integer
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 = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
y) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
.&. Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
  IntN Integer
x * :: IntN n -> IntN n -> IntN n
* IntN Integer
y = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
y) IntN n -> IntN n -> IntN n
forall a. Bits a => a -> a -> a
.&. Proxy n -> IntN n
forall (proxy :: Nat -> *) (n :: Nat).
KnownNat n =>
proxy n -> IntN n
minusOneIntN (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
  IntN Integer
x - :: IntN n -> IntN n -> IntN n
- IntN Integer
y
    | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
y = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
    | Bool
otherwise = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN ((Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
y)
  negate :: IntN n -> IntN n
negate (IntN Integer
0) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
  negate IntN n
a = IntN n -> IntN n
forall a. Bits a => a -> a
complement IntN n
a IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
+ Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
1
  abs :: IntN n -> IntN n
abs IntN n
x = if IntN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit IntN n
x (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) then IntN n -> IntN n
forall a. Num a => a -> a
negate IntN n
x else IntN n
x
  signum :: IntN n -> IntN n
signum (IntN Integer
0) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
0
  signum IntN n
i = if IntN n -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit IntN n
i (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) then -IntN n
1 else IntN n
1
  fromInteger :: Integer -> IntN n
fromInteger !Integer
x = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN (Integer -> IntN n) -> Integer -> IntN n
forall a b. (a -> b) -> a -> b
$ if Integer
v Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then Integer
v else (Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` Int
n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
v
    where
      v :: Integer
v = WordN n -> Integer
forall (n :: Nat). WordN n -> Integer
unWordN (Integer -> WordN n
forall a. Num a => Integer -> a
fromInteger (Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
maxn) :: WordN n) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
maxn
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
      maxn :: Integer
maxn = Integer
1 Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
`shiftL` (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1

instance Num SomeIntN where
  + :: SomeIntN -> SomeIntN -> SomeIntN
(+) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
(+)
  (-) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 (-)
  * :: SomeIntN -> SomeIntN -> SomeIntN
(*) = (forall (n :: Nat).
 (KnownNat n, 1 <= n) =>
 IntN n -> IntN n -> IntN n)
-> SomeIntN -> SomeIntN -> SomeIntN
binSomeIntNR1 IntN n -> IntN n -> IntN n
forall (n :: Nat).
(KnownNat n, 1 <= n) =>
IntN n -> IntN n -> IntN n
forall a. Num a => a -> a -> a
(*)
  negate :: SomeIntN -> SomeIntN
negate = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 IntN n -> IntN n
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n
forall a. Num a => a -> a
negate
  abs :: SomeIntN -> SomeIntN
abs = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 IntN n -> IntN n
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n
forall a. Num a => a -> a
abs
  signum :: SomeIntN -> SomeIntN
signum = (forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n)
-> SomeIntN -> SomeIntN
unarySomeIntNR1 IntN n -> IntN n
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> IntN n
forall a. Num a => a -> a
signum
  fromInteger :: Integer -> SomeIntN
fromInteger = String -> Integer -> SomeIntN
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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
b
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
      as :: Bool
as = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
a (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      bs :: Bool
bs = Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Integer
b (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

instance (KnownNat n, 1 <= n) => QC.Arbitrary (IntN n) where
  arbitrary :: Gen (IntN n)
arbitrary = Gen (IntN n)
forall a. (Bounded a, Integral a) => Gen a
QC.arbitrarySizedBoundedIntegral

  -- QC.shrinkIntegral assumes that 2 is representable by the number, which is
  -- not the case for 1-bit bit vector.
  shrink :: IntN n -> [IntN n]
shrink IntN n
i
    | IntN n
i IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
0 = []
    | IntN n
i IntN n -> IntN n -> Bool
forall a. Eq a => a -> a -> Bool
== IntN n
1 = [IntN n
0]
    | Bool
otherwise = IntN n -> [IntN n]
forall a. Integral a => a -> [a]
QC.shrinkIntegral IntN n
i

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

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

instance BV SomeWordN where
  bvConcat :: SomeWordN -> SomeWordN -> SomeWordN
bvConcat (SomeWordN (WordN n
a :: WordN l)) (SomeWordN (WordN n
b :: WordN r)) =
    case (Proxy n -> Proxy n -> LeqProof 1 (n + n)
forall (m :: Nat) (n :: Nat) (p :: Nat -> *) (q :: Nat -> *).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @l) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @r), forall (m :: Nat) (n :: Nat).
KnownProof m -> KnownProof n -> KnownProof (m + n)
knownAdd @l @r KnownProof n
forall (n :: Nat). KnownNat n => KnownProof n
KnownProof KnownProof n
forall (n :: Nat). KnownNat n => KnownProof n
KnownProof) of
      (LeqProof 1 (n + n)
LeqProof, KnownProof (n + n)
KnownProof) ->
        WordN (n + n) -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN (n + n) -> SomeWordN) -> WordN (n + n) -> SomeWordN
forall a b. (a -> b) -> a -> b
$ WordN n -> WordN n -> WordN (n + n)
forall (l :: Nat) (r :: Nat).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
WordN l -> WordN r -> WordN (l + r)
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
bv l -> bv r -> bv (l + r)
sizedBVConcat WordN n
a WordN n
b
  {-# INLINE bvConcat #-}
  bvZext :: Int -> SomeWordN -> SomeWordN
bvZext Int
l (SomeWordN (WordN n
a :: WordN n))
    | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = String -> SomeWordN
forall a. HasCallStack => String -> a
error String
"bvZext: trying to zero extend a value to a smaller size"
    | Bool
otherwise = Proxy n -> SomeWordN
forall (l :: Nat). Proxy l -> SomeWordN
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      res :: forall (l :: Nat). Proxy l -> SomeWordN
      res :: forall (l :: Nat). Proxy l -> SomeWordN
res Proxy l
p =
        case (forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @l (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l), forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @n @l) of
          (KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> WordN l -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN l -> SomeWordN) -> WordN l -> SomeWordN
forall a b. (a -> b) -> a -> b
$ Proxy l -> WordN n -> WordN l
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVZext Proxy l
p WordN n
a
  bvSext :: Int -> SomeWordN -> SomeWordN
bvSext Int
l (SomeWordN (WordN n
a :: WordN n))
    | Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n = String -> SomeWordN
forall a. HasCallStack => String -> a
error String
"bvSext: trying to zero extend a value to a smaller size"
    | Bool
otherwise = Proxy n -> SomeWordN
forall (l :: Nat). Proxy l -> SomeWordN
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      res :: forall (l :: Nat). Proxy l -> SomeWordN
      res :: forall (l :: Nat). Proxy l -> SomeWordN
res Proxy l
p =
        case (forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @l (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l), forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @l, forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @n @l) of
          (KnownProof l
KnownProof, LeqProof 1 l
LeqProof, LeqProof n l
LeqProof) -> WordN l -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN l -> SomeWordN) -> WordN l -> SomeWordN
forall a b. (a -> b) -> a -> b
$ Proxy l -> WordN n -> WordN l
forall (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> WordN l -> WordN r
forall (bv :: Nat -> *) (l :: Nat) (r :: Nat) (proxy :: Nat -> *).
(SizedBV bv, KnownNat l, KnownNat r, 1 <= l, KnownNat r, l <= r) =>
proxy r -> bv l -> bv r
sizedBVSext Proxy l
p WordN n
a
  bvExt :: Int -> SomeWordN -> SomeWordN
bvExt = Int -> SomeWordN -> SomeWordN
forall bv. BV bv => Int -> bv -> bv
bvZext
  bvSelect :: Int -> Int -> SomeWordN -> SomeWordN
bvSelect Int
ix Int
w (SomeWordN (WordN n
a :: WordN n))
    | Int
ix Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
n = String -> SomeWordN
forall a. HasCallStack => String -> a
error String
"bvSelect: trying to select a bitvector outside the bounds of the input"
    | Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = String -> SomeWordN
forall a. HasCallStack => String -> a
error String
"bvSelect: trying to select a bitvector of size 0"
    | Bool
otherwise = Proxy n -> Proxy n -> SomeWordN
forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN
res (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
    where
      n :: Int
n = Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)
      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN
      res :: forall (w :: Nat) (ix :: Nat). Proxy w -> Proxy ix -> SomeWordN
res Proxy w
_ Proxy ix
_ =
        case ( forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @ix (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
ix),
               forall (n :: Nat). Nat -> KnownProof n
unsafeKnownProof @w (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
w),
               forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @1 @w,
               forall (m :: Nat) (n :: Nat). LeqProof m n
unsafeLeqProof @(ix + w) @n
             ) of
          (KnownProof ix
KnownProof, KnownProof w
KnownProof, LeqProof 1 w
LeqProof, LeqProof (ix + w) n
LeqProof) ->
            WordN w -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN w -> SomeWordN) -> WordN w -> SomeWordN
forall a b. (a -> b) -> a -> b
$ Proxy ix -> Proxy w -> WordN n -> WordN w
forall (n :: Nat) (ix :: Nat) (w :: Nat) (p :: Nat -> *)
       (q :: Nat -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> WordN n -> WordN w
forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
       (p :: Nat -> *) (q :: Nat -> *).
(SizedBV bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> bv n -> bv w
sizedBVSelect (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @ix) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @w) WordN n
a

instance BV SomeIntN where
  bvConcat :: SomeIntN -> SomeIntN -> SomeIntN
bvConcat SomeIntN
l SomeIntN
r = SomeWordN -> SomeIntN
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned (SomeWordN -> SomeIntN) -> SomeWordN -> SomeIntN
forall a b. (a -> b) -> a -> b
$ SomeWordN -> SomeWordN -> SomeWordN
forall bv. BV bv => bv -> bv -> bv
bvConcat (SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned SomeIntN
l) (SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned SomeIntN
r)
  {-# INLINE bvConcat #-}
  bvZext :: Int -> SomeIntN -> SomeIntN
bvZext Int
l = SomeWordN -> SomeIntN
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned (SomeWordN -> SomeIntN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeIntN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SomeWordN -> SomeWordN
forall bv. BV bv => Int -> bv -> bv
bvZext Int
l (SomeWordN -> SomeWordN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeWordN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned
  {-# INLINE bvZext #-}
  bvSext :: Int -> SomeIntN -> SomeIntN
bvSext Int
l = SomeWordN -> SomeIntN
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned (SomeWordN -> SomeIntN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeIntN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SomeWordN -> SomeWordN
forall bv. BV bv => Int -> bv -> bv
bvSext Int
l (SomeWordN -> SomeWordN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeWordN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned
  {-# INLINE bvSext #-}
  bvExt :: Int -> SomeIntN -> SomeIntN
bvExt Int
l = SomeWordN -> SomeIntN
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned (SomeWordN -> SomeIntN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeIntN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SomeWordN -> SomeWordN
forall bv. BV bv => Int -> bv -> bv
bvExt Int
l (SomeWordN -> SomeWordN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeWordN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned
  {-# INLINE bvExt #-}
  bvSelect :: Int -> Int -> SomeIntN -> SomeIntN
bvSelect Int
ix Int
w = SomeWordN -> SomeIntN
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned (SomeWordN -> SomeIntN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeIntN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> SomeWordN -> SomeWordN
forall bv. BV bv => Int -> Int -> bv -> bv
bvSelect Int
ix Int
w (SomeWordN -> SomeWordN)
-> (SomeIntN -> SomeWordN) -> SomeIntN -> SomeWordN
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeIntN -> SomeWordN
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned
  {-# INLINE bvSelect #-}

instance (KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) where
  toSigned :: WordN n -> IntN n
toSigned (WordN Integer
i) = Integer -> IntN n
forall (n :: Nat). Integer -> IntN n
IntN Integer
i
  toUnsigned :: IntN n -> WordN n
toUnsigned (IntN Integer
i) = Integer -> WordN n
forall (n :: Nat). Integer -> WordN n
WordN Integer
i

instance SignConversion SomeWordN SomeIntN where
  toSigned :: SomeWordN -> SomeIntN
toSigned (SomeWordN WordN n
i) = IntN n -> SomeIntN
forall (n :: Nat). (KnownNat n, 1 <= n) => IntN n -> SomeIntN
SomeIntN (IntN n -> SomeIntN) -> IntN n -> SomeIntN
forall a b. (a -> b) -> a -> b
$ WordN n -> IntN n
forall ubv sbv. SignConversion ubv sbv => ubv -> sbv
toSigned WordN n
i
  toUnsigned :: SomeIntN -> SomeWordN
toUnsigned (SomeIntN IntN n
i) = WordN n -> SomeWordN
forall (n :: Nat). (KnownNat n, 1 <= n) => WordN n -> SomeWordN
SomeWordN (WordN n -> SomeWordN) -> WordN n -> SomeWordN
forall a b. (a -> b) -> a -> b
$ IntN n -> WordN n
forall ubv sbv. SignConversion ubv sbv => sbv -> ubv
toUnsigned IntN n
i

deriving via
  (DefaultFiniteBitsSymShift (IntN n))
  instance
    (KnownNat n, 1 <= n) => SymShift (IntN n)

deriving via
  (DefaultFiniteBitsSymShift (WordN n))
  instance
    (KnownNat n, 1 <= n) => SymShift (WordN n)

deriving via
  (DefaultFiniteBitsSymRotate (IntN n))
  instance
    (KnownNat n, 1 <= n) => SymRotate (IntN n)

deriving via
  (DefaultFiniteBitsSymRotate (WordN n))
  instance
    (KnownNat n, 1 <= n) => SymRotate (WordN n)