Safe Haskell	None
Language	GHC2021

Raehik.GHC.TypeNats.Bits

Description

Type-level Data.Bits definitions, over GHC opaque type-level Naturals.

Synopsis

type ShiftL (x :: Natural) (i :: Natural) = x * (2 ^ i)
type ShiftR (x :: Natural) (i :: Natural) = Div x (2 ^ i)
type Xor (n :: Natural) (m :: Natural) = XorLoop 1 0 n m
type family XorLoop (factor :: Natural) (acc :: Natural) (n :: Natural) (m :: Natural) :: Natural where ...
type family BitXor (n :: Natural) (m :: Natural) :: Natural where ...

Documentation

type ShiftL (x :: Natural) (i :: Natural) = x * (2 ^ i) Source #

Left shift.

type ShiftR (x :: Natural) (i :: Natural) = Div x (2 ^ i) Source #

Logical right shift. (But these are nats, is arithmetic shiftR even diff??)

type Xor (n :: Natural) (m :: Natural) = XorLoop 1 0 n m Source #

The exclusive or of the binary representation of two Naturals.

type family XorLoop (factor :: Natural) (acc :: Natural) (n :: Natural) (m :: Natural) :: Natural where ... Source #

Equations

XorLoop factor acc 0 0 = acc
XorLoop factor acc n m = XorLoop (factor * 2) (acc + (factor * BitXor (Mod n 2) (Mod m 2))) (Div n 2) (Div m 2)

type family BitXor (n :: Natural) (m :: Natural) :: Natural where ... Source #

Exclusive or on two "bit" Naturals.

Both Naturals must be either 0 or 1, or it emits a type error.

Equations

BitXor 0 0 = 0
BitXor 0 1 = 1
BitXor 1 0 = 1
BitXor 1 1 = 0
BitXor n m = TypeError ('Text "BitXor: got non-bit Naturals") :: Natural