Data.Type.Binary.Internals

Portability	non-portable (FD and MPTC)
Stability	experimental
Maintainer	Edward Kmett <ekmett@gmail.com>

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

TAddC' T T F (O T)

(TCBinary c a, XO a) => TCBinary c (O a)

TAnd F (O b) F

TImplies F (O b) T

TMul (O a) b c => TMul a (O b) c

TOr T (O b) T

(TPow a k c, TMul c c d) => TPow a (O k) d

(TPow' a k c, TMul c c d) => TPow' a (O k) d

(TShift' a b c, TShift' c b d) => TShift' a (O b) d

TSucc a b => TAddC' F (I a) T (O b)

TAddC' F (O a) F (O a)

TAddC' F (O a) T (I a)

TAddC' T (I a) F (O a)

TSucc b a => TAddC' T (O a) F (I b)

TAddC' T (O a) T (O a)

TAnd T (O b) (O b)

TImplies T (O b) (O b)

TOr F (O b) (O b)

(TShift' a b c, TShift' c b d) => TShift' a (I b) (O d)

TXOr' F (O b) (O b)

TNot b c => TXOr' T (I b) (O c)

TNot b c => TXOr' T (O b) (I c)

TBinary (O a) => Show (O a)

(TBinary a, XO a) => TBinary (O a)

TSucc (O T) T

(Trichotomy a b, XO a) => Trichotomy (I (O a)) b

(Trichotomy a b, XI a) => Trichotomy (O (I a)) b

(Trichotomy a b, XO a) => Trichotomy (O (O a)) b

Trichotomy (O T) Negative

LSB (O T) F T

TAnd (O a) F F

TCountBits' a n F => TCountBits' (O a) n F

(TCountBits' a n F, TSucc m n) => TCountBits' (O a) n T

TEq (O m) F F

TEq (O m) T F

TImplies (O a) F T

TNF' (O F) F F

(TNF' (O a) c b, TIf b (O c) F d) => TNF' (O (O a)) d b

TOr (O a) T T

TShift' (O a) T a

LSB (O a) F a => X (O a) F a

TSucc a b => TAddC' (I a) F T (O b)

TAddC' (I a) T F (O a)

TAddC' (O a) F F (O a)

TAddC' (O a) F T (I a)

TSucc b a => TAddC' (O a) T F (I b)

TAddC' (O a) T T (O a)

LSB (I (O n)) T (O n)

LSB (O (I n)) F (I n)

LSB (O (O n)) F (O n)

TAnd (O a) T (O a)

TImplies (O a) T (O a)

TOr (O a) F (I a)

TShift' (O a) F (O a)

TNot b c => TXOr' (I b) T (O c)

TXOr' (O b) F (O b)

TNot b c => TXOr' (O b) T (I c)

THex2Binary' a b => THex2Binary' (D0 a) (O (O (O (O b))))

THex2Binary' a b => THex2Binary' (D1 a) (I (O (O (O b))))

THex2Binary' a b => THex2Binary' (D2 a) (O (I (O (O b))))

THex2Binary' a b => THex2Binary' (D3 a) (I (I (O (O b))))

THex2Binary' a b => THex2Binary' (D4 a) (O (O (I (O b))))

THex2Binary' a b => THex2Binary' (D5 a) (I (O (I (O b))))

THex2Binary' a b => THex2Binary' (D6 a) (O (I (I (O b))))

THex2Binary' a b => THex2Binary' (D7 a) (I (I (I (O b))))

THex2Binary' a b => THex2Binary' (D8 a) (O (O (O (I b))))

THex2Binary' a b => THex2Binary' (D9 a) (I (O (O (I b))))

THex2Binary' a b => THex2Binary' (DA a) (O (I (O (I b))))

THex2Binary' a b => THex2Binary' (DB a) (I (I (O (I b))))

THex2Binary' a b => THex2Binary' (DC a) (O (O (I (I b))))

THex2Binary' a b => THex2Binary' (DD a) (I (O (I (I b))))

THex2Binary' a b => THex2Binary' (DE a) (O (I (I (I b))))

TNot a b => TNot (I a) (O b)

TNot a b => TNot (O a) (I b)

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

(TAnd a b c, TNF (O c) c') => TAnd (I a) (O b) c'

(TAnd a b c, TNF (O c) c') => TAnd (O a) (I b) c'

(TAnd a b c, TNF (O c) c') => TAnd (O a) (O b) c'

TEq (I m) (O n) F

TEq (O m) (I n) F

TEq m n b => TEq (O m) (O n) b

(TImplies a b c, TNF (I c) c') => TImplies (I a) (O b) c'

(TImplies a b c, TNF (I c) c') => TImplies (O a) (I b) c'

(TImplies a b c, TNF (O c) c') => TImplies (O a) (O b) c'

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

(TOr a b c, TNF (I c) c') => TOr (I a) (O b) c'

(TOr a b c, TNF (I c) c') => TOr (O a) (I b) c'

(TOr a b c, TNF (O c) c') => TOr (O a) (O b) c'

(TXOr' a b c, TNF (I c) c') => TXOr' (I a) (O b) c'

(TXOr' a b c, TNF (I c) c') => TXOr' (O a) (I b) c'

(TXOr' a b c, TNF (O c) c') => TXOr' (O a) (O b) c'

TAddC' a b T c => TAddC' (I a) (I b) F (O c)

TAddC' a b F c => TAddC' (I a) (O b) F (I c)

TAddC' a b T c => TAddC' (I a) (O b) T (O c)

TAddC' a b F c => TAddC' (O a) (I b) F (I c)

TAddC' a b T c => TAddC' (O a) (I b) T (O c)

TAddC' a b F c => TAddC' (O a) (O b) F (O c)

TAddC' a b F c => TAddC' (O a) (O b) T (I c)

data I a

Instances

TAddC' F F T (I F)

TPow a F (I F)

(TCBinary c a, XI a) => TCBinary c (I a)

TSucc F (I F)

TAnd F (I b) F

TImplies F (I b) T

(TMul (O a) b c, TAdd' a c d) => TMul a (I b) d

TOr T (I b) T

(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, TMul a d e) => TPow' a (I k) e

TAddC' F (I a) F (I a)

TSucc a b => TAddC' F (I a) T (O b)

TAddC' F (O a) T (I a)

TAddC' T (I a) F (O a)

TAddC' T (I a) T (I a)

TSucc b a => TAddC' T (O a) F (I b)

TAnd T (I b) (I b)

TImplies T (I b) (I b)

TOr F (I b) (I b)

(TShift' a b c, TShift' c b d) => TShift' a (I b) (O d)

TXOr' F (I b) (I b)

TNot b c => TXOr' T (I b) (O c)

TNot b c => TXOr' T (O b) (I c)

TBinary (I a) => Show (I a)

(TBinary a, XI a) => TBinary (I a)

Trichotomy (I F) Positive

(Trichotomy a b, XI a) => Trichotomy (I (I a)) b

(Trichotomy a b, XO a) => Trichotomy (I (O a)) b

(Trichotomy a b, XI a) => Trichotomy (O (I a)) b

LSB (I F) T F

TAnd (I a) F F

(TCountBits' a n F, TSucc n m) => TCountBits' (I a) m F

TCountBits' a m F => TCountBits' (I a) m T

TEq (I m) F F

TEq (I m) T F

TImplies (I a) F T

(TNF' (I a) c b, TIf b (I c) T d) => TNF' (I (I a)) d b

TNF' (I T) T F

TOr (I a) T T

TShift' (I a) T a

LSB (I a) T a => X (I a) T a

TAddC' (I a) F F (I a)

TSucc a b => TAddC' (I a) F T (O b)

TAddC' (I a) T F (O a)

TAddC' (I a) T T (I a)

TAddC' (O a) F T (I a)

TSucc b a => TAddC' (O a) T F (I b)

LSB (I (I n)) T (I n)

LSB (I (O n)) T (O n)

LSB (O (I n)) F (I n)

TAnd (I a) T (I a)

TImplies (I a) T (I a)

TOr (I a) F (I a)

TOr (O a) F (I a)

TShift' (I a) F (I a)

TXOr' (I b) F (I b)

TNot b c => TXOr' (I b) T (O c)

TNot b c => TXOr' (O b) T (I c)

THex2Binary' a b => THex2Binary' (D1 a) (I (O (O (O b))))

THex2Binary' a b => THex2Binary' (D2 a) (O (I (O (O b))))

THex2Binary' a b => THex2Binary' (D3 a) (I (I (O (O b))))

THex2Binary' a b => THex2Binary' (D4 a) (O (O (I (O b))))

THex2Binary' a b => THex2Binary' (D5 a) (I (O (I (O b))))

THex2Binary' a b => THex2Binary' (D6 a) (O (I (I (O b))))

THex2Binary' a b => THex2Binary' (D7 a) (I (I (I (O b))))

THex2Binary' a b => THex2Binary' (D8 a) (O (O (O (I b))))

THex2Binary' a b => THex2Binary' (D9 a) (I (O (O (I b))))

THex2Binary' a b => THex2Binary' (DA a) (O (I (O (I b))))

THex2Binary' a b => THex2Binary' (DB a) (I (I (O (I b))))

THex2Binary' a b => THex2Binary' (DC a) (O (O (I (I b))))

THex2Binary' a b => THex2Binary' (DD a) (I (O (I (I b))))

THex2Binary' a b => THex2Binary' (DE a) (O (I (I (I b))))

THex2Binary' a b => THex2Binary' (DF a) (I (I (I (I b))))

TNot a b => TNot (I a) (O b)

TNot a b => TNot (O a) (I b)

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

(TAnd a b c, TNF (I c) c') => TAnd (I a) (I b) c'

(TAnd a b c, TNF (O c) c') => TAnd (I a) (O b) c'

(TAnd a b c, TNF (O c) c') => TAnd (O a) (I b) c'

TEq m n b => TEq (I m) (I n) b

TEq (I m) (O n) F

TEq (O m) (I n) F

(TImplies a b c, TNF (I c) c') => TImplies (I a) (I b) c'

(TImplies a b c, TNF (I c) c') => TImplies (I a) (O b) c'

(TImplies a b c, TNF (I c) c') => TImplies (O a) (I b) c'

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

(TOr a b c, TNF (I c) c') => TOr (I a) (I b) c'

(TOr a b c, TNF (I c) c') => TOr (I a) (O b) c'

(TOr a b c, TNF (I c) c') => TOr (O a) (I b) c'

(TXOr' a b c, TNF (O c) c') => TXOr' (I a) (I b) c'

(TXOr' a b c, TNF (I c) c') => TXOr' (I a) (O b) c'

(TXOr' a b c, TNF (I c) c') => TXOr' (O a) (I b) c'

TAddC' a b T c => TAddC' (I a) (I b) F (O c)

TAddC' a b T c => TAddC' (I a) (I b) T (I c)

TAddC' a b F c => TAddC' (I a) (O b) F (I c)

TAddC' a b T c => TAddC' (I a) (O b) T (O c)

TAddC' a b F c => TAddC' (O a) (I b) F (I c)

TAddC' a b T c => TAddC' (O a) (I b) T (O c)

TAddC' a b F c => TAddC' (O a) (O b) T (I c)

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

TAddC' F F F F

TAddC' F T F T

TAddC' F T T F

TAddC' T F F T

TAddC' T F T F

TAddC' T T T T

TAddC' F F T (I F)

TAddC' T T F (O T)

TAddC' F (I a) F (I a)

TSucc a b => TAddC' F (I a) T (O b)

TAddC' F (O a) F (O a)

TAddC' F (O a) T (I a)

TAddC' T (I a) F (O a)

TAddC' T (I a) T (I a)

TSucc b a => TAddC' T (O a) F (I b)

TAddC' T (O a) T (O a)

TAddC' (I a) F F (I a)

TSucc a b => TAddC' (I a) F T (O b)

TAddC' (I a) T F (O a)

TAddC' (I a) T T (I a)

TAddC' (O a) F F (O a)

TAddC' (O a) F T (I a)

TSucc b a => TAddC' (O a) T F (I b)

TAddC' (O a) T T (O a)

TAddC' a b T c => TAddC' (I a) (I b) F (O c)

TAddC' a b T c => TAddC' (I a) (I b) T (I c)

TAddC' a b F c => TAddC' (I a) (O b) F (I c)

TAddC' a b T c => TAddC' (I a) (O b) T (O c)

TAddC' a b F c => TAddC' (O a) (I b) F (I c)

TAddC' a b T c => TAddC' (O a) (I b) T (O c)

TAddC' a b F c => TAddC' (O a) (O b) F (O c)

TAddC' a b F c => TAddC' (O a) (O b) T (I c)

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