haskus-binary-1.5: Haskus binary format manipulation

Safe HaskellNone
LanguageHaskell2010

Haskus.Number.BitNat

Contents

Description

Natural numbers

Synopsis

Documentation

data NatVal (t :: Nat) #

A natural value Proxy

Constructors

NatVal 
Instances
KnownNat t => Show (NatVal t) 
Instance details

Defined in Haskus.Utils.Types.Proxy

Methods

showsPrec :: Int -> NatVal t -> ShowS #

show :: NatVal t -> String #

showList :: [NatVal t] -> ShowS #

type Widen a b = (Assert (a <=? b) (() :: Constraint) ((((Text "Can't widen a natural of " :<>: ShowType a) :<>: Text " bits into a natural of ") :<>: ShowType b) :<>: Text " bits"), Integral (BitNatWord a), Integral (BitNatWord b)) Source #

widen :: forall b a. Widen a b => BitNat a -> BitNat b Source #

Widen a natural

>>> widen @7 (BitNat @5 25)
BitNat @7 25

type Narrow a b = (Assert (b <=? a) (() :: Constraint) ((((Text "Can't narrow a natural of " :<>: ShowType a) :<>: Text " bits into a natural of ") :<>: ShowType b) :<>: Text " bits"), Integral (BitNatWord a), Integral (BitNatWord b), Maskable b (BitNatWord b)) Source #

narrow :: forall b a. Narrow a b => BitNat a -> BitNat b Source #

Narrow a natural

>>> narrow @3 (BitNat @5 25)
BitNat @3 1

type IsBitNat b = (Num (BitNatWord b), Integral (BitNatWord b), Bitwise (BitNatWord b), IndexableBits (BitNatWord b)) Source #

data BitNat (b :: Nat) Source #

A natural on b bits

Instances
Eq (BitNatWord a) => Eq (BitNat a) Source # 
Instance details

Defined in Haskus.Number.BitNat

Methods

(==) :: BitNat a -> BitNat a -> Bool #

(/=) :: BitNat a -> BitNat a -> Bool #

Ord (BitNatWord a) => Ord (BitNat a) Source # 
Instance details

Defined in Haskus.Number.BitNat

Methods

compare :: BitNat a -> BitNat a -> Ordering #

(<) :: BitNat a -> BitNat a -> Bool #

(<=) :: BitNat a -> BitNat a -> Bool #

(>) :: BitNat a -> BitNat a -> Bool #

(>=) :: BitNat a -> BitNat a -> Bool #

max :: BitNat a -> BitNat a -> BitNat a #

min :: BitNat a -> BitNat a -> BitNat a #

(KnownNat b, Integral (BitNatWord b)) => Show (BitNat b) Source #

Show instance for BitNat

Instance details

Defined in Haskus.Number.BitNat

Methods

showsPrec :: Int -> BitNat b -> ShowS #

show :: BitNat b -> String #

showList :: [BitNat b] -> ShowS #

pattern BitNat :: forall (n :: Nat). (Integral (BitNatWord n), MakeBitNat n) => Natural -> BitNat n Source #

unsafeMakeBitNat :: forall a. Maskable a (BitNatWord a) => BitNatWord a -> BitNat a Source #

Create a natural

safeMakeBitNat :: forall a. MakeBitNat a => Natural -> Maybe (BitNat a) Source #

Create a natural (check overflow)

bitNat :: forall (v :: Nat) (n :: Nat). (n ~ NatBitCount v, Integral (BitNatWord n), MakeBitNat n, KnownNat v) => BitNat n Source #

Create a natural number with the minimal number of bits required to store it

>>> bitNat @5
BitNat @3 5

>>> bitNat @0
BitNat @1 0

>>> bitNat @158748521123465897456465
BitNat @78 158748521123465897456465

bitNatZero :: Num (BitNatWord a) => BitNat a Source #

Zero natural

bitNatOne :: Num (BitNatWord a) => BitNat a Source #

One natural

extractW :: BitNat a -> BitNatWord a Source #

Extract the primitive value

compareW :: forall a b. (Ord (BitNatWord (Max a b)), Widen a (Max a b), Widen b (Max a b)) => BitNat a -> BitNat b -> Ordering Source #

Compare two naturals

(.+.) :: forall a b m. (m ~ (Max a b + 1), Widen a m, Widen b m, Num (BitNatWord m)) => BitNat a -> BitNat b -> BitNat m Source #

Add two Naturals

>>> BitNat @5 25 .+. BitNat @2 3
BitNat @6 28

(.-.) :: forall a b m. (m ~ Max a b, Widen a m, Widen b m, Num (BitNatWord m)) => BitNat a -> BitNat b -> Maybe (BitNat m) Source #

Sub two Naturals

>>> BitNat @5 25 .-. BitNat @2 3
Just (BitNat @5 22)

>>> BitNat @5 2 .-. BitNat @2 3
Nothing

(.*.) :: forall a b m. (m ~ (a + b), Widen a m, Widen b m, Num (BitNatWord m)) => BitNat a -> BitNat b -> BitNat m Source #

Multiply two Naturals

>>> BitNat @5 25 .*. BitNat @2 3
BitNat @7 75

(./.) :: forall a b m. (m ~ Max a b, Widen a m, Widen b m, Num (BitNatWord (Min a b))) => BitNat a -> BitNat b -> Maybe (BitNat a, BitNat (Min a b)) Source #

Divide two Naturals, return (factor,rest)

>>> BitNat @5 25 ./. BitNat @2 3
Just (BitNat @5 8,BitNat @2 1)

>>> BitNat @5 25 ./. BitNat @2 0
Nothing

BitNat @2 3 ./. BitNat @5 25

Just (BitNat 2 0,BitNat 5 3)

type BitNatShiftLeft a s = (ShiftableBits (BitNatWord (a + s)), KnownNat s, Widen a (a + s)) Source #

type BitNatShiftRight a s = (ShiftableBits (BitNatWord a), KnownNat s, Narrow a (a - s)) Source #

(.<<.) :: forall (s :: Nat) a. BitNatShiftLeft a s => BitNat a -> NatVal s -> BitNat (a + s) Source #

Shift-left naturals

>>> let x = BitNat @5 25
>>> x .<<. NatVal @2
BitNat @7 100

>>> show (x .<<. NatVal @2) == show (x .*. BitNat @3 4)
False

>>> x .<<. NatVal @2 == narrow (x .*. BitNat @3 4)
True

(.>>.) :: forall (s :: Nat) a. BitNatShiftRight a s => BitNat a -> NatVal s -> BitNat (a - s) Source #

Shift-right naturals

>>> BitNat @5 25 .>>. NatVal @2
BitNat @3 6

bitNatTestBit :: IndexableBits (BitNatWord a) => BitNat a -> Word -> Bool Source #

Test a bit

bitNatXor :: forall a. IsBitNat a => BitNat a -> BitNat a -> BitNat a Source #

Xor

bitNatAnd :: forall a. IsBitNat a => BitNat a -> BitNat a -> BitNat a Source #

And

bitNatOr :: forall a. IsBitNat a => BitNat a -> BitNat a -> BitNat a Source #

Or

Internal

type family BitNatWord b where ... Source #

BitNat backing type

Equations

BitNatWord 0 = TypeError (Text "Naturals encoded on 0 bits are not allowed") 
BitNatWord b = BitNatWord' (b <=? 8) (b <=? 16) (b <=? 32) (b <=? 64) 

type MakeBitNat a = (Maskable a (BitNatWord a), ShiftableBits (BitNatWord a), Show (BitNatWord a), Eq (BitNatWord a), Num (BitNatWord a)) Source #

bitNatToNatural :: Integral (BitNatWord a) => BitNat a -> Natural Source #

Convert a BitNat into a Natural