type-int-0.5.0.2: Type Level 2s- and 16s- Complement Integers

Portability non-portable (FD and MPTC) experimental Edward Kmett 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

data I a Source

Instances

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

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

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

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

Instances

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