Data.Type.Hex

Type-level hexadecimal numbers, positive and negative with infinite precision. Should work out to about 2^72 without changing the default context length limit in GHC.

TODO: TDivMod, TImplies, TGCD, T*Bit, and the boolean operators

Documentation

hexE :: Integral a => a -> Exp

$(hexE n) returns an undefined value of the appropriate THex instance

hexT :: Integral a => a -> Type

$(hexT n) returns the appropriate THex instance

class TIsZero n b | n -> b

Instances

(Trichotomy n s, TEq s SignZero b) => TIsZero n b

class TIsPositive n b | n -> b

Instances

(Trichotomy n s, TEq s Positive b) => TIsPositive n b

class TIsNegative n b | n -> b

Instances

(Trichotomy n s, TEq s Negative b) => TIsNegative n b

tIsZero :: TIsZero n b => n -> b

tIsPositive :: TIsPositive n b => n -> b

tIsNegative :: TIsNegative n b => n -> b

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

Instances

(TNot a b, TSucc b c) => TNeg a c

tNeg :: TNeg a b => a -> b

tSucc :: TSucc n m => n -> m

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

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

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

A simple peasant multiplier. TODO: exploit 2s complement and reverse the worst cases

Instances

TNeg a b => TMul a T b

TMul a F F

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, SHR1 H0 a4 a8, TAdd' a4 a8 aC, TAdd' a2 aC aE, TAdd' a1 aE aF, TAdd' aF c d) => TMul a1 (DF b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, SHR1 H0 a4 a8, TAdd' a4 a8 aC, TAdd' a2 aC aE, TAdd' aE c d) => TMul a1 (DE b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, SHR1 H0 a4 a8, TAdd' a4 a8 aC, TAdd' a1 aC aD, TAdd' aD c d) => TMul a1 (DD b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, SHR1 H0 a4 a8, TAdd' a4 a8 aC, TAdd' aC c d) => TMul a1 (DC b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, SHR1 H0 a4 a8, TAdd' a2 a8 a0, TAdd' a1 a0 aB, TAdd' aB c d) => TMul a1 (DB b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, SHR1 H0 a4 a8, TAdd' a2 a8 aA, TAdd' aA c d) => TMul a1 (DA b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, SHR1 H0 a4 a8, TAdd' a1 a8 a9, TAdd' a9 c d) => TMul a1 (D9 b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, SHR1 H0 a4 a8, TAdd' a8 c d) => TMul a1 (D8 b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, TAdd' a2 a4 a6, TAdd' a1 a6 a7, TAdd' a7 c d) => TMul a1 (D7 b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, TAdd' a2 a4 a6, TAdd' a6 c d) => TMul a1 (D6 b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, TAdd' a1 a4 a5, TAdd' a5 c d) => TMul a1 (D5 b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, SHR1 H0 a2 a4, TAdd' a4 c d) => TMul a1 (D4 b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, TAdd' a1 a2 a3, TAdd' a3 c d) => TMul a1 (D3 b) d

(TMul (D0 a1) b c, SHR1 H0 a1 a2, TAdd' a2 c d) => TMul a1 (D2 b) d

(TMul (D0 a1) b c, TAdd' a1 c d) => TMul a1 (D1 b) d

TMul (D0 a1) b c => TMul a1 (D0 b) c

tMul :: TMul a b c => a -> b -> c

class TPow a b c | a b -> c

peasant exponentiator

Instances

(THex2Binary b b', TPow' a b' c) => TPow a b c

tPow :: TPow a b c => a -> b -> c

class TNF a b | a -> b

Instances

TNF' a b c => TNF a b

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

class THexBinary a b | a -> b, b -> a

Instances

(THex2Binary a b, TBinary2Hex b a) => THexBinary a b

module Data.Type.Boolean

module Data.Type.Ord

module Data.Type.Hex.Stage1

module Data.Type.Hex.Stage2