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

Data.Type.Binary.Internals

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

Documentation

data O a Source

Instances

TAddC' T T F (O T)
(TCBinary c a, XO a) => TCBinary c (O a)
TImplies F (O b) T
TOr T (O b) T
TAnd F (O b) F
(TShift' a b c, TShift' c b d) => TShift' a (O b) d
(TPow a k c, TMul c c d) => TPow a (O k) d
TMul (O a) b c => TMul a (O b) c
(TPow' a k c, TMul c c d) => TPow' a (O k) d
TSucc a b => TAddC' F (I a) T (O b)
TAddC' F (O a) T (I a)
TAddC' F (O a) F (O 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)
TImplies T (O b) (O b)
TXOr' F (O b) (O b)
TNot b c => TXOr' T (I b) (O c)
TNot b c => TXOr' T (O b) (I c)
TOr F (O b) (O b)
TAnd T (O b) (O b)
(TShift' a b c, TShift' c b d) => TShift' a (I b) (O d)
TBinary (O a) => Show (O a)	Show should express a value as legal haskell.
(TBinary a, XO a) => TBinary (O a)
(Trichotomy a b, XO a) => Trichotomy (I (O a)) b
Trichotomy (O T) Negative
(Trichotomy a b, XI a) => Trichotomy (O (I a)) b
(Trichotomy a b, XO a) => Trichotomy (O (O a)) b
TSucc (O T) T
TImplies (O a) F T
TOr (O a) T T
TAnd (O a) F F
TEq (O m) T F
TEq (O m) F F
(TCountBits' a n F, TSucc m n) => TCountBits' (O a) n T
TCountBits' a n F => TCountBits' (O a) n F
TShift' (O a) T a
TNF' (O F) F F
(TNF' (O a) c b, TIf b (O c) F d) => TNF' (O (O a)) d b
LSB (O a) F a => X (O a) F a
LSB (O T) F T
TSucc a b => TAddC' (I a) F T (O b)
TAddC' (I a) T F (O a)
TSucc b a => TAddC' (O a) T F (I b)
TAddC' (O a) F T (I a)
TAddC' (O a) T T (O a)
TAddC' (O a) F F (O a)
TImplies (O a) T (O a)
TNot b c => TXOr' (I b) T (O c)
TNot b c => TXOr' (O b) T (I c)
TXOr' (O b) F (O b)
TOr (O a) F (I a)
TAnd (O a) T (O a)
TShift' (O a) F (O a)
LSB (I (O n)) T (O n)
LSB (O (I n)) F (I n)
LSB (O (O n)) F (O n)
TNot a b => TNot (I a) (O b)
TNot a b => TNot (O a) (I b)	TNot preserves normalization trivially
(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))
THex2Binary' a b => THex2Binary' (DE a) (O (I (I (I b))))
THex2Binary' a b => THex2Binary' (DD a) (I (O (I (I b))))
THex2Binary' a b => THex2Binary' (DC a) (O (O (I (I b))))
THex2Binary' a b => THex2Binary' (DB a) (I (I (O (I b))))
THex2Binary' a b => THex2Binary' (DA a) (O (I (O (I b))))
THex2Binary' a b => THex2Binary' (D9 a) (I (O (O (I b))))
THex2Binary' a b => THex2Binary' (D8 a) (O (O (O (I b))))
THex2Binary' a b => THex2Binary' (D7 a) (I (I (I (O b))))
THex2Binary' a b => THex2Binary' (D6 a) (O (I (I (O b))))
THex2Binary' a b => THex2Binary' (D5 a) (I (O (I (O b))))
THex2Binary' a b => THex2Binary' (D4 a) (O (O (I (O b))))
THex2Binary' a b => THex2Binary' (D3 a) (I (I (O (O b))))
THex2Binary' a b => THex2Binary' (D2 a) (O (I (O (O b))))
THex2Binary' a b => THex2Binary' (D1 a) (I (O (O (O b))))
THex2Binary' a b => THex2Binary' (D0 a) (O (O (O (O b))))
(TImplies a b c, TNF (I c) c') => TImplies (I a) (O b) c'
(TImplies a b c, TNF (O c) c') => TImplies (O a) (O b) c'
(TImplies a b c, TNF (I c) c') => TImplies (O a) (I b) c'
(TXOr' a b c, TNF (I c) c') => TXOr' (I a) (O b) c'
(TXOr' a b c, TNF (O c) c') => TXOr' (O a) (O b) c'
(TXOr' a b c, TNF (I c) c') => TXOr' (O a) (I b) c'
(TOr a b c, TNF (I c) c') => TOr (I a) (O b) c'
(TOr a b c, TNF (O c) c') => TOr (O a) (O b) c'
(TOr a b c, TNF (I c) c') => TOr (O 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) (O b) c'
(TAnd a b c, TNF (O c) c') => TAnd (O a) (I b) c'
TEq (I m) (O n) F	Equality comparison. Note this does not equate numbers that are non-normalized with their normalized kin.
TEq m n b => TEq (O m) (O n) b
TEq (O m) (I n) F
TNF' (O a) c b => TNF' (I (O a)) (I c) T
TNF' (O T) (O T) T
TNF' (I a) c b => TNF' (O (I a)) (O c) T
TAddC' a b T c => TAddC' (I a) (I b) F (O c)
TAddC' a b T c => TAddC' (I a) (O b) T (O c)
TAddC' a b F c => TAddC' (I a) (O 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) (I b) F (I c)
TAddC' a b F c => TAddC' (O a) (O b) T (I c)
TAddC' a b F c => TAddC' (O a) (O b) F (O c)

data I a Source

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)
TImplies F (I b) T
TOr T (I b) T
TAnd F (I b) F
(TPow a k c, TMul c c d, TMul a d e) => TPow a (I k) e
(TMul (O a) b c, TAdd' a c d) => TMul a (I b) d
(TPow' a k c, TMul c c d, TMul a d e) => TPow' a (I k) e
TSucc a b => TAddC' F (I a) T (O b)
TAddC' F (I a) F (I 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)
TImplies T (I b) (I b)
TXOr' F (I b) (I b)
TNot b c => TXOr' T (I b) (O c)
TNot b c => TXOr' T (O b) (I c)
TOr F (I b) (I b)
TAnd T (I b) (I b)
(TShift' a b c, TShift' c b d) => TShift' a (I b) (O d)
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
TImplies (I a) F T
TOr (I a) T T
TAnd (I a) F F
TEq (I m) F F
TEq (I m) T F
(TCountBits' a n F, TSucc n m) => TCountBits' (I a) m F
TCountBits' a m F => TCountBits' (I a) m T
TShift' (I a) T a
TNF' (I T) T F
(TNF' (I a) c b, TIf b (I c) T d) => TNF' (I (I a)) d b
LSB (I a) T a => X (I a) T a
LSB (I F) T F
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' (I a) F F (I a)
TSucc b a => TAddC' (O a) T F (I b)
TAddC' (O a) F T (I a)
TImplies (I a) T (I a)
TNot b c => TXOr' (I b) T (O c)
TXOr' (I b) F (I b)
TNot b c => TXOr' (O b) T (I c)
TOr (I a) F (I a)
TOr (O a) F (I a)
TAnd (I a) T (I a)
TShift' (I a) F (I a)
LSB (I (I n)) T (I n)
LSB (I (O n)) T (O n)
LSB (O (I n)) F (I n)
TNot a b => TNot (I a) (O b)
TNot a b => TNot (O a) (I b)	TNot preserves normalization trivially
(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))
THex2Binary' a b => THex2Binary' (DF a) (I (I (I (I b))))
THex2Binary' a b => THex2Binary' (DE a) (O (I (I (I b))))
THex2Binary' a b => THex2Binary' (DD a) (I (O (I (I b))))
THex2Binary' a b => THex2Binary' (DC a) (O (O (I (I b))))
THex2Binary' a b => THex2Binary' (DB a) (I (I (O (I b))))
THex2Binary' a b => THex2Binary' (DA a) (O (I (O (I b))))
THex2Binary' a b => THex2Binary' (D9 a) (I (O (O (I b))))
THex2Binary' a b => THex2Binary' (D8 a) (O (O (O (I b))))
THex2Binary' a b => THex2Binary' (D7 a) (I (I (I (O b))))
THex2Binary' a b => THex2Binary' (D6 a) (O (I (I (O b))))
THex2Binary' a b => THex2Binary' (D5 a) (I (O (I (O b))))
THex2Binary' a b => THex2Binary' (D4 a) (O (O (I (O b))))
THex2Binary' a b => THex2Binary' (D3 a) (I (I (O (O b))))
THex2Binary' a b => THex2Binary' (D2 a) (O (I (O (O b))))
THex2Binary' a b => THex2Binary' (D1 a) (I (O (O (O b))))
(TImplies a b c, TNF (I c) c') => TImplies (I a) (O b) c'
(TImplies a b c, TNF (I c) c') => TImplies (I a) (I b) c'
(TImplies a b c, TNF (I c) c') => TImplies (O a) (I b) c'
(TXOr' a b c, TNF (I c) c') => TXOr' (I a) (O 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' (O 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 (I a) (I b) c'
(TOr a b c, TNF (I c) c') => TOr (O a) (I b) c'
(TAnd a b c, TNF (O c) c') => TAnd (I a) (O b) c'
(TAnd a b c, TNF (I c) c') => TAnd (I a) (I 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	Equality comparison. Note this does not equate numbers that are non-normalized with their normalized kin.
TEq (O m) (I n) F
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
TAddC' a b T c => TAddC' (I a) (I b) T (I c)
TAddC' a b T c => TAddC' (I a) (I b) F (O c)
TAddC' a b T c => TAddC' (I a) (O b) T (O c)
TAddC' a b F c => TAddC' (I a) (O 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) (I b) F (I c)
TAddC' a b F c => TAddC' (O a) (O b) T (I c)

class TSucc n m | n -> m, m -> nSource

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

tPred :: TSucc n m => m -> nSource

class TCBinary c a | a -> cSource

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 whereSource

We don't want to have to carry the closure parameter around explicitly everywhere, so we shed it here.

Methods

fromTBinary :: Integral b => a -> bSource

Instances

TBinary F
TBinary T
(TBinary a, XI a) => TBinary (I a)
(TBinary a, XO a) => TBinary (O a)

class TNeg a b | a -> b, b -> aSource

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

class TIsNegative n b | n -> bSource

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

class TIsPositive n b | n -> bSource

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

class TIsZero n b | n -> bSource

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

class TEven a b | a -> bSource

Returns true if the lsb of the number is true

Instances

LSB a b c => TEven a b

tEven :: TEven a b => a -> bSource

class TOdd a b | a -> bSource

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

class TAdd a b c | a b -> c, a c -> b, b c -> aSource

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

tSub :: TAdd a b c => c -> a -> bSource

class TMul a b c | a b -> cSource

Multiplication: a * b = c

Instances

TNeg a b => TMul a T b
TMul a F F
(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 -> cSource

class TPow a b c | a b -> cSource

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

class TShift a b c' | a b -> c'Source

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

class TGetBit a b c | a b -> cSource

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

class TSetBit a b c | a b -> cSource

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

class TChangeBit a b c d | a b c -> dSource

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

class TUnSetBit a b c | a b -> cSource

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

class TComplementBit a b c | a b -> cSource

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

class TCountBits a b | a -> bSource

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

class TAbs a b | a -> bSource

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

class TNF a b | a -> bSource

Shed the additional reduction parameter from TNF'

Instances

TNF' a b c => TNF a b

tNF :: TNF a b => a -> bSource

t2n :: TNF (O a) b => a -> bSource

t2np1 :: TNF (I a) b => a -> bSource

data Negative Source

Instances

TSign Negative
TCSign Closure Negative
Trichotomy T Negative
Trichotomy T Negative
TEq Positive Negative F
TEq SignZero Negative F
TEq Negative Positive F
TEq Negative SignZero F
TEq Negative Negative T
Trichotomy (O T) Negative
Trichotomy (DE T) Negative
Trichotomy (DD T) Negative
Trichotomy (DC T) Negative
Trichotomy (DB T) Negative
Trichotomy (DA T) Negative
Trichotomy (D9 T) Negative
Trichotomy (D8 T) Negative
Trichotomy (D7 T) Negative
Trichotomy (D6 T) Negative
Trichotomy (D5 T) Negative
Trichotomy (D4 T) Negative
Trichotomy (D3 T) Negative
Trichotomy (D2 T) Negative
Trichotomy (D1 T) Negative
Trichotomy (D0 T) Negative

data Positive Source

Instances

TSign Positive
TCSign Closure Positive
TEq Positive Positive T
TEq Positive SignZero F
TEq Positive Negative F
TEq SignZero Positive F
TEq Negative Positive F
Trichotomy (I F) Positive
Trichotomy (DF F) Positive
Trichotomy (DE F) Positive
Trichotomy (DD F) Positive
Trichotomy (DC F) Positive
Trichotomy (DB F) Positive
Trichotomy (DA F) Positive
Trichotomy (D9 F) Positive
Trichotomy (D8 F) Positive
Trichotomy (D7 F) Positive
Trichotomy (D6 F) Positive
Trichotomy (D5 F) Positive
Trichotomy (D4 F) Positive
Trichotomy (D3 F) Positive
Trichotomy (D2 F) Positive
Trichotomy (D1 F) Positive

data SignZero Source

Instances

TSign SignZero
TCSign Closure SignZero
Trichotomy F SignZero
Trichotomy F SignZero
TEq Positive SignZero F
TEq SignZero Positive F
TEq SignZero SignZero T
TEq SignZero Negative F
TEq Negative SignZero F

class TShift' a b c | a b -> cSource

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 cSource

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 T) T F
(TNF' (I a) c b, TIf b (I c) T d) => TNF' (I (I a)) d b
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' (O T) (O T) T
TNF' (I a) c b => TNF' (O (I a)) (O c) T

class TAddC' a b c d | a b c -> dSource

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)
TSucc a b => TAddC' F (I a) T (O b)
TAddC' F (I a) F (I a)
TAddC' F (O a) T (I a)
TAddC' F (O a) F (O 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)
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' (I a) F F (I a)
TSucc b a => TAddC' (O a) T F (I b)
TAddC' (O a) F T (I a)
TAddC' (O a) T T (O a)
TAddC' (O a) F F (O a)
TAddC' a b T c => TAddC' (I a) (I b) T (I c)
TAddC' a b T c => TAddC' (I a) (I b) F (O c)
TAddC' a b T c => TAddC' (I a) (O b) T (O c)
TAddC' a b F c => TAddC' (I a) (O 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) (I b) F (I c)
TAddC' a b F c => TAddC' (O a) (O b) T (I c)
TAddC' a b F c => TAddC' (O a) (O b) F (O c)

class TAdd' a b c | a b -> cSource

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

class TSub' a b c | a b -> cSource

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

class TCountBits' a b t | a t -> bSource

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, TSucc m n) => TCountBits' (O a) n T
TCountBits' a n F => TCountBits' (O a) n F

class TBool d => LSB a d a' | a -> d a', d a' -> aSource

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'Source

tBSL :: LSB a d a' => a' -> d -> aSource

class LSB (I a) T a => XI a Source

assert 2n+1 != n

Instances

LSB (I a) T a => XI a

class LSB (O a) F a => XO a Source

assert 2n != n

Instances

LSB (O a) F a => XO a