Data.Type.Binary.Internals
 Portability non-portable (FD and MPTC) Stability experimental Maintainer Edward Kmett
Description

Simple type-level binary numbers, positive and negative with infinite precision. This forms a nice commutative ring with multiplicative identity like we would expect from a representation for Z.

The numbers are represented as a Boolean Ring over a countable set of variables, in which for every element in the set there exists an n in N and a b in {T,F} such that for all n'>=n in N, x_i = b.

For uniqueness we always choose the least such n when representing numbers this allows us to run most computations backwards. When we can't, and such a fundep would be implied, we obtain it by combining semi-operations that together yield the appropriate class fundep list.

Reuses T and F from the Type.Boolean as the infinite tail of the 2s complement binary number.

TODO: TDivMod, TGCD

Synopsis
data O a
data I a
class TSucc n m | n -> m, m -> n
tSucc :: TSucc n m => n -> m
tPred :: TSucc n m => m -> n
class TCBinary c a | a -> c
class TCBinary Closure a => TBinary a where
 fromTBinary :: Integral b => a -> b
fromTBinary :: (TBinary a, Integral b) => a -> b
class TNeg a b | a -> b, b -> a
tNeg :: TNeg a b => a -> b
class TIsNegative n b | n -> b
tIsNegative :: TIsNegative n b => n -> b
class TIsPositive n b | n -> b
tIsPositive :: TIsPositive n b => n -> b
class TIsZero n b | n -> b
tIsZero :: TIsZero n b => n -> b
class TEven a b | a -> b
tEven :: TEven a b => a -> b
class TOdd a b | a -> b
tOdd :: TOdd a b => a -> b
class TAdd a b c | a b -> c, a c -> b, b c -> a
tAdd :: TAdd a b c => a -> b -> c
tSub :: TAdd a b c => c -> a -> b
class TMul a b c | a b -> c
tMul :: TMul a b c => a -> b -> c
class TPow a b c | a b -> c
tPow :: TPow a b c => a -> b -> c
class TShift a b c' | a b -> c'
tShift :: TShift a b c => a -> b -> c
class TGetBit a b c | a b -> c
tGetBit :: TGetBit a b c => a -> b -> c
class TSetBit a b c | a b -> c
tSetBit :: TSetBit a b c => a -> b -> c
class TChangeBit a b c d | a b c -> d
tChangeBit :: TChangeBit a b c d => a -> b -> c -> d
class TUnSetBit a b c | a b -> c
tUnSetBit :: TUnSetBit a b c => a -> b -> c
class TComplementBit a b c | a b -> c
tComplementBit :: TComplementBit a b c => a -> b -> c
class TCountBits a b | a -> b
tCountBits :: TCountBits a b => a -> b
class TAbs a b | a -> b
tAbs :: TAbs a b => a -> b
class TNF a b | a -> b
tNF :: TNF a b => a -> b
t2n :: TNF (O a) b => a -> b
t2np1 :: TNF (I a) b => a -> b
class TShift' a b c | a b -> c
class TNF' a b c | a -> b c
class TAddC' a b c d | a b c -> d
class TAdd' a b c | a b -> c
tAdd' :: TAdd' a b c => a -> b -> c
class TSub' a b c | a b -> c
tSub' :: TSub' a b c => a -> b -> c
class TCountBits' a b t | a t -> b
class TBool d => LSB a d a' | a -> d a', d a' -> a
tLSB :: LSB a d a' => a -> d -> a'
tBSL :: LSB a d a' => a' -> d -> a
class LSB (I a) T a => XI a
class LSB (O a) F a => XO a
Documentation
data O a
Instances
data I a
Instances
class TSucc n m | n -> m, m -> n
Finds the unique successor for any normalized binary number
Instances
 TSucc T F TSucc F (I F) TSucc (O T) T (TSucc n m, XI n, XO m) => TSucc (I n) (O m) TSucc (O (I n)) (I (I n)) TSucc (O (O n)) (I (O n))
tSucc :: TSucc n m => n -> m
tPred :: TSucc n m => m -> n
class TCBinary c a | a -> c
Our set of digits is closed to retain the properties needed for most of the classes herein
Instances
 TCBinary Closure F TCBinary Closure T (TCBinary c a, XI a) => TCBinary c (I a) (TCBinary c a, XO a) => TCBinary c (O a)
class TCBinary Closure a => TBinary a where
We don't want to have to carry the closure parameter around explicitly everywhere, so we shed it here.
Methods
 fromTBinary :: Integral b => a -> b
Instances
 TBinary F TBinary T (TBinary a, XI a) => TBinary (I a) (TBinary a, XO a) => TBinary (O a)
fromTBinary :: (TBinary a, Integral b) => a -> b
class TNeg a b | a -> b, b -> a
TNeg obtains the 2s complement of a number and is reversible
Instances
 (TNot a b, TSucc b c) => TNeg a c
tNeg :: TNeg a b => a -> b
class TIsNegative n b | n -> b
Returns true if the number is less than zero
Instances
 (Trichotomy n s, TEq s Negative b) => TIsNegative n b
tIsNegative :: TIsNegative n b => n -> b
class TIsPositive n b | n -> b
Returns true if the number is greater than zero
Instances
 (Trichotomy n s, TEq s Positive b) => TIsPositive n b
tIsPositive :: TIsPositive n b => n -> b
class TIsZero n b | n -> b
Returns true if the number is equal to zero
Instances
 (Trichotomy n s, TEq s SignZero b) => TIsZero n b
tIsZero :: TIsZero n b => n -> b
class TEven a b | a -> b
Returns true if the lsb of the number is true
Instances
 LSB a b c => TEven a b
tEven :: TEven a b => a -> b
class TOdd a b | a -> b
Returns true if the lsb of the number if false
Instances
 (LSB a b c, TNot b b') => TOdd a b'
tOdd :: TOdd a b => a -> b
class TAdd a b c | a b -> c, a c -> b, b c -> a
Reversible adder with extra fundeps.
Instances
 (TAdd' a b c, TNeg b b', TAdd' c b' a, TNeg a a', TAdd' c a' b) => TAdd a b c
tAdd :: TAdd a b c => a -> b -> c
tSub :: TAdd a b c => c -> a -> b
class TMul a b c | a b -> c
Multiplication: a * b = c
Instances
 TMul a F F TNeg a b => TMul a T b (TMul (O a) b c, TAdd' a c d) => TMul a (I b) d TMul (O a) b c => TMul a (O b) c
tMul :: TMul a b c => a -> b -> c
class TPow a b c | a b -> c
Exponentiation: a^b = c (only defined for non-negative exponents)
Instances
 TPow a F (I F) (TPow a k c, TMul c c d, TMul a d e) => TPow a (I k) e (TPow a k c, TMul c c d) => TPow a (O k) d
tPow :: TPow a b c => a -> b -> c
class TShift a b c' | a b -> c'
Shift a right b places obtaining c in normal form. | If b is negative then we shift left.
Instances
 (TShift' a b c, TNF c c') => TShift a b c'
tShift :: TShift a b c => a -> b -> c
class TGetBit a b c | a b -> c
get bit #b in a as c in {T,F}
Instances
 (TNeg b b', TShift a b' c, LSB c d e) => TGetBit a b d
tGetBit :: TGetBit a b c => a -> b -> c
class TSetBit a b c | a b -> c
set bit #b in a to T, yielding c.
Instances
 (TShift (I F) b c, TOr a c d) => TSetBit a b d
tSetBit :: TSetBit a b c => a -> b -> c
class TChangeBit a b c d | a b c -> d
change bit #b in a to c in {T,F}, yielding d.
Instances
 (TSetBit a b d, TUnSetBit a b e, TIf c d e f) => TChangeBit a b c f
tChangeBit :: TChangeBit a b c d => a -> b -> c -> d
class TUnSetBit a b c | a b -> c
set bit #b in a to F, yielding c
Instances
 (TShift (O T) b c, TAnd a c d) => TUnSetBit a b d
tUnSetBit :: TUnSetBit a b c => a -> b -> c
class TComplementBit a b c | a b -> c
toggle the value of bit #b in a, yielding c
Instances
 (TShift (I F) b c, TXOr' a c d) => TComplementBit a b d
tComplementBit :: TComplementBit a b c => a -> b -> c
class TCountBits a b | a -> b
Count the number of bits set. Since we may have an infinite tail of 1s, we return a negative number in such cases indicating how many bits are NOT set.
Instances
 (TIsNegative a t, TCountBits' a b t) => TCountBits a b
tCountBits :: TCountBits a b => a -> b
class TAbs a b | a -> b
Return the absolute value of a
Instances
 (TIsNegative a s, TNeg a a', TIf s a' a a'') => TAbs a a''
tAbs :: TAbs a b => a -> b
class TNF a b | a -> b
Shed the additional reduction parameter from TNF'
Instances
 TNF' a b c => TNF a b
tNF :: TNF a b => a -> b
t2n :: TNF (O a) b => a -> b
t2np1 :: TNF (I a) b => a -> b
class TShift' a b c | a b -> c
Shift a right b places obtaining c. If b is negative then we shift left. | TShift' does not yield normal form answers.
Instances
 TShift' F F F TShift' F T F TShift' T F T TShift' T T T (TShift' a b c, TShift' c b d) => TShift' a (O b) d (TShift' a b c, TShift' c b d) => TShift' a (I b) (O d) TShift' (I a) T a TShift' (O a) T a TShift' (I a) F (I a) TShift' (O a) F (O a)
class TNF' a b c | a -> b c
Transform a number into normal form, but track whether further reductions may be necessary if this number is extended for efficiency.
Instances
 TNF' F F F TNF' T T F (TNF' (I a) c b, TIf b (I c) T d) => TNF' (I (I a)) d b TNF' (I T) T F TNF' (O F) F F (TNF' (O a) c b, TIf b (O c) F d) => TNF' (O (O a)) d b TNF' (I F) (I F) T TNF' (O a) c b => TNF' (I (O a)) (I c) T TNF' (I a) c b => TNF' (O (I a)) (O c) T TNF' (O T) (O T) T
class TAddC' a b c d | a b c -> d
A symmetrical full adder, that does not yield normal form answers.
Instances
class TAdd' a b c | a b -> c
Non-reversible addition. Kept for efficiency purposes.
Instances
 (TAddC' a b F d, TNF d d') => TAdd' a b d'
tAdd' :: TAdd' a b c => a -> b -> c
class TSub' a b c | a b -> c
Non-reversible subtraction. Kept for efficiency purposes.
Instances
 (TNeg b b', TAdd' a b' c) => TSub' a b c
tSub' :: TSub' a b c => a -> b -> c
class TCountBits' a b t | a t -> b
Count the number of bits set, but track whether the number is positive or negative to simplify casing. Since we may have an infinite tail of 1s, we return a negative number in such cases indicating how many bits are NOT set.
Instances
 TCountBits' F F F TCountBits' T T T (TCountBits' a n F, TSucc n m) => TCountBits' (I a) m F TCountBits' a m F => TCountBits' (I a) m T TCountBits' a n F => TCountBits' (O a) n F (TCountBits' a n F, TSucc m n) => TCountBits' (O a) n T
class TBool d => LSB a d a' | a -> d a', d a' -> a
Extracts the least significant bit of a as d and returns a'. Can also be used to prepend bit d onto a' obtaining a.
Instances
 LSB F F F LSB T T T LSB (I F) T F LSB (O T) F T LSB (I (I n)) T (I n) LSB (I (O n)) T (O n) LSB (O (I n)) F (I n) LSB (O (O n)) F (O n)
tLSB :: LSB a d a' => a -> d -> a'
tBSL :: LSB a d a' => a' -> d -> a
class LSB (I a) T a => XI a
assert 2n+1 != n
Instances
 LSB (I a) T a => XI a
class LSB (O a) F a => XO a
assert 2n != n
Instances
 LSB (O a) F a => XO a
Produced by Haddock version 0.8