Haskus.Number.BitNat

Natural numbers

Documentation

data NatVal (t :: Nat)

A natural value Proxy

Constructors

NatVal

Instances

KnownNat t => Show (NatVal t)

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))

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

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))

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

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))

data BitNat (b :: Nat)

A natural on b bits

Instances

Eq (BitNatWord a) => Eq (BitNat a)

Defined in Haskus.Number.BitNat

Methods

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

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

Ord (BitNatWord a) => Ord (BitNat a)

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)

Show instance for BitNat

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

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

Create a natural

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

Create a natural (check overflow)

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

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

Zero natural

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

One natural

extractW :: BitNat a -> BitNatWord a

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

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

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)

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

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))

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))

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

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

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)

Shift-right naturals

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

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

Test a bit

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

Xor

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

And

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

Or

Internal

type family BitNatWord b where ...

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))

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

Convert a BitNat into a Natural