isobmff-builder-0.11.3.0: A (bytestring-) builder for the ISO-14496-12 base media file format

Safe HaskellNone
LanguageHaskell2010

Data.Type.BitRecords.Arithmetic

Contents

Synopsis

Documentation

type family Rem (x :: Nat) (y :: Nat) :: Nat where ... Source #

Get the remainder of the integer division of x and y, such that forall x y. exists k. (Rem x y) == x - y * k The algorithm is: count down x until zero, incrementing the accumulator at each step. Whenever the accumulator is equal to y set it to zero.

If the accumulator has reached y reset it. It is important to do this BEFORE checking if x == y and then returning the accumulator, for the case where x = k * y with k > 0. For example:

 6 Rem 3     = RemImpl 6 3 0
 RemImpl 6 3 0 = RemImpl (6-1) 3 (0+1)   -- RemImpl Clause 4
 RemImpl 5 3 1 = RemImpl (5-1) 3 (1+1)   -- RemImpl Clause 4
 RemImpl 4 3 2 = RemImpl (4-1) 3 (2+1)   -- RemImpl Clause 4
 RemImpl 3 3 3 = RemImpl 3 3 0           -- RemImpl Clause 2 !!!
 RemImpl 3 3 0 = 0                       -- RemImpl Clause 3 !!!

Equations

Rem x 1 = 0 
Rem x 0 = TypeError ((Text "divide by zero: " :<>: ShowType x) :<>: Text " `Rem` 0") 
Rem x y = RemImpl x y 0 

type family RemImpl (x :: Nat) (y :: nat) (acc :: Nat) :: Nat where ... Source #

Equations

RemImpl 0 y acc = acc 
RemImpl x y y = RemImpl x y 0 
RemImpl y y acc = acc 
RemImpl x y acc = RemImpl (x - 1) y (acc + 1) 

type RemPow2 x p = FromBits (TakeLastN p (ToBits x RemPow2Bits)) Source #

Efficient Rem operation for power of 2 values. Note that x must be representable by RemPow2Bits bits.

type TakeLastN n xs = TakeLastNImplRev n xs '[] Source #

type family TakeLastNImplRev (n :: Nat) (xs :: [t]) (acc :: [t]) :: [t] where ... Source #

Equations

TakeLastNImplRev n '[] acc = TakeLastNImplTakeNRev n acc '[] 
TakeLastNImplRev n (x ': xs) acc = TakeLastNImplRev n xs (x ': acc) 

type family TakeLastNImplTakeNRev (n :: Nat) (rs :: [t]) (acc :: [t]) :: [t] where ... Source #

Equations

TakeLastNImplTakeNRev n '[] acc = acc 
TakeLastNImplTakeNRev 0 rs acc = acc 
TakeLastNImplTakeNRev n (r ': rs) acc = TakeLastNImplTakeNRev (n - 1) rs (r ': acc) 

type RemPow2Bits = 32 Source #

Maximum number of bits an argument x of RemPow2 may occupy.

type Div x y = DivImpl (x - (x `Rem` y)) y 0 Source #

Integer division of x and y: Div x y ==> x / y, NOTE This only works for small numbers currently

type family DivImpl (x :: Nat) (y :: nat) (acc :: Nat) :: Nat where ... Source #

Equations

DivImpl 0 y acc = acc 
DivImpl x y acc = If ((x + 1) <=? y) acc (DivImpl (x - y) y (acc + 1)) 

Bit manipulation

type family TestHighBit (x :: Nat) (n :: Nat) :: Bool where ... Source #

Equations

TestHighBit x n = (2 ^ n) <=? x 

type ToBits x n = ToBits_ x n False Source #

type family ToBits_ (x :: Nat) (n :: Nat) (started :: Bool) :: [Bool] where ... Source #

Equations

ToBits_ x 0 started = '[] 
ToBits_ x n started = ToBitsInner (TestHighBit x (n - 1)) x (n - 1) started 

type family ToBitsInner (highBitSet :: Bool) (x :: Nat) (n :: Nat) (started :: Bool) :: [Bool] where ... Source #

Equations

ToBitsInner True x n started = True ': ToBits_ (x - (2 ^ n)) n True 
ToBitsInner False x n False = ToBits_ x n False 
ToBitsInner False x n True = False ': ToBits_ x n True 

type FromBits bits = FromBits_ bits 0 Source #

type family FromBits_ (bits :: [Bool]) (acc :: Nat) :: Nat where ... Source #

Equations

FromBits_ '[] acc = acc 
FromBits_ (False ': rest) acc = FromBits_ rest (acc + acc) 
FromBits_ (True ': rest) acc = FromBits_ rest ((1 + acc) + acc) 

type family ShiftBitsR (bits :: [Bool]) (n :: Nat) :: [Bool] where ... Source #

Equations

ShiftBitsR bits 0 = bits 
ShiftBitsR '[] n = '[] 
ShiftBitsR '[e] 1 = '[] 
ShiftBitsR (e ': rest) 1 = e ': ShiftBitsR rest 1 
ShiftBitsR (e ': rest) n = ShiftBitsR (ShiftBitsR (e ': rest) 1) (n - 1) 

type family GetMostSignificantBitIndex (highestBit :: Nat) (n :: Nat) :: Nat where ... Source #

Equations

GetMostSignificantBitIndex 0 n = 1 
GetMostSignificantBitIndex highestBit n = If ((2 ^ (highestBit + 1)) <=? n) (TypeError (((Text "number to big: " :<>: ShowType n) :<>: Text " >= ") :<>: ShowType (2 ^ (highestBit + 1)))) (If ((2 ^ highestBit) <=? n) highestBit (GetMostSignificantBitIndex (highestBit - 1) n)) 

type family ShiftR (xMaxBits :: Nat) (x :: Nat) (bits :: Nat) :: Nat where ... Source #

Shift a type level natural to the right. This useful for division by powers of two.

Equations

ShiftR xMaxBits x n = FromBits (ShiftBitsR (ToBits x (1 + GetMostSignificantBitIndex xMaxBits x)) n)