{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, ScopedTypeVariables, FlexibleContexts, FlexibleInstances, EmptyDataDecls #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Type.Binary.Internals -- Copyright : (C) 2006-2007 Edward Kmett -- License : BSD-style (see the file libraries/base/LICENSE) -- -- Maintainer : Edward Kmett <ekmett@gmail.com> -- Stability : experimental -- Portability : non-portable (FD and MPTC) -- -- 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 ---------------------------------------------------------------------------- module Data.Type.Binary.Internals ( O, I, -- T, tT, -- F, tF, TSucc, tSucc, tPred, TCBinary, TBinary, fromTBinary, -- TNot, TNeg, tNeg, TIsNegative, tIsNegative, TIsPositive, tIsPositive, TIsZero, tIsZero, TEven, tEven, TOdd, tOdd, TAdd, tAdd, tSub, TMul, tMul, TPow, tPow, -- TAnd, TOr, TXOr, TImplies, -- tAnd, tOr, tXOr, tImplies, TShift, tShift, TGetBit, tGetBit, TSetBit, tSetBit, TChangeBit, tChangeBit, TUnSetBit, tUnSetBit, TComplementBit, tComplementBit, TCountBits, tCountBits, {- TReverse, tReverse, -} TAbs, tAbs, TNF, tNF, -- put a number into normal form t2n, t2np1, -- prepend a 0 or 1 -- TEq, TLt, tEq, tLt, -- from Type.Sign Negative, Positive, SignZero, -- internal interfaces below here -- these require knowledge of the internal representation TShift', -- non-normalizing shifter TNF', -- case tracking normalizer for a number. TAddC', -- non-normalizing full-adder TAdd', tAdd', -- semi-adder TSub', tSub', -- semi-sub TCountBits', -- sign-tracking intermediary for TCountBits LSB, tLSB, tBSL, -- extract the LSB and tail of a number XI, XO, -- indicates that the number can be extended -- by a I or O without leaving normal form ) where import Data.Type.Boolean import Data.Type.Ord import Data.Type.Sign data O a data I a -- | Internal closure, not exposed data Closure class Closed a | -> a instance Closed Closure -- | Extracts the least significant bit of a as d and returns a'. -- Can also be used to prepend bit d onto a' obtaining a. class (TBool d) => LSB a d a' | a -> d a', d a' -> a instance LSB F F F instance LSB T T T instance LSB (O T) F T instance LSB (I F) T F instance LSB (O (O n)) F (O n) instance LSB (O (I n)) F (I n) instance LSB (I (O n)) T (O n) instance LSB (I (I n)) T (I n) tLSB :: LSB a d a' => a -> d -> a'; tLSB = undefined tBSL :: LSB a d a' => a' -> d -> a; tBSL = undefined -- | extract the lsb and assert we aren't at the long tail class LSB a d a' => X a d a' | a -> d a', d a' -> a, a a' -> d instance (LSB (O a) F a) => X (O a) F a instance (LSB (I a) T a) => X (I a) T a -- | assert 2n != n class LSB (O a) F a => XO a instance (LSB (O a) F a) => XO a -- | assert 2n+1 != n class LSB (I a) T a => XI a instance (LSB (I a) T a) => XI a -- | Finds the unique successor for any normalized binary number class TSucc n m | n -> m, m -> n instance TSucc T F instance TSucc F (I F) instance TSucc (O T) T instance TSucc (O (I n)) (I (I n)) instance TSucc (O (O n)) (I (O n)) instance (TSucc n m, XI n, XO m) => TSucc (I n) (O m) tSucc :: TSucc n m => n -> m; tSucc = undefined tPred :: TSucc n m => m -> n; tPred = undefined -- | Our set of digits is closed to retain the properties needed for most of the classes herein class TCBinary c a | a -> c instance TCBinary Closure F instance TCBinary Closure T instance (TCBinary c a, XO a) => TCBinary c (O a) instance (TCBinary c a, XI a) => TCBinary c (I a) -- | We don't want to have to carry the closure parameter around explicitly everywhere, so we -- shed it here. class TCBinary Closure a => TBinary a where fromTBinary :: Integral b => a -> b instance TBinary F where fromTBinary _ = fromInteger 0 instance TBinary T where fromTBinary _ = fromInteger (-1) instance (TBinary a, XO a) => TBinary (O a) where fromTBinary _ = let x = fromTBinary (undefined::a) in x+x instance (TBinary a, XI a) => TBinary (I a) where fromTBinary _ = let x = fromTBinary (undefined::a) in succ(x+x) -- | Show should express a value as legal haskell. instance TBinary (O a) => Show (O a) where show n = "$(binaryE "++(show $ fromTBinary n)++")" instance TBinary (I a) => Show (I a) where show n = "$(binaryE "++(show $ fromTBinary n)++")" {- instance Show (O F) where show n = "({-error-} O F)"; instance Show (I T) where show n = "({-error-} I T)"; instance Show (I F) where show n = "I F"; instance Show (O T) where show n = "O T"; instance (Show (I t)) => Show (O (I t)) where show n = "O (" ++ show (undefined::I t) ++ ")" instance (Show (I t)) => Show (I (I t)) where show n = "I (" ++ show (undefined::I t) ++ ")" instance (Show (O t)) => Show (O (O t)) where show n = "O (" ++ show (undefined::O t) ++ ")" instance (Show (O t)) => Show (I (O t)) where show n = "I (" ++ show (undefined::O t) ++ ")" -} -- | TNot preserves normalization trivially instance (TNot a b) => TNot (O a) (I b) instance (TNot a b) => TNot (I a) (O b) -- | TNeg obtains the 2s complement of a number and is reversible class TNeg a b | a -> b, b -> a instance (TNot a b, TSucc b c) => TNeg a c tNeg :: TNeg a b => a -> b; tNeg = undefined -- | Express a corrolary to the trichotomy law, every number is either negative, positive or zero. class Trichotomy n s | n -> s instance Trichotomy T Negative instance Trichotomy F SignZero instance Trichotomy (I F) Positive instance Trichotomy (O T) Negative instance (Trichotomy a b, XI a) => Trichotomy (I (I a)) b instance (Trichotomy a b, XI a) => Trichotomy (O (I a)) b instance (Trichotomy a b, XO a) => Trichotomy (I (O a)) b instance (Trichotomy a b, XO a) => Trichotomy (O (O a)) b -- | Returns true if the number is greater than zero class TIsPositive n b | n -> b instance (Trichotomy n s, TEq s Positive b) => TIsPositive n b tIsPositive :: TIsPositive n b => n -> b; tIsPositive = undefined -- | Returns true if the number is less than zero class TIsNegative n b | n -> b instance (Trichotomy n s, TEq s Negative b) => TIsNegative n b tIsNegative :: TIsNegative n b => n -> b; tIsNegative = undefined -- | Returns true if the number is equal to zero class TIsZero n b | n -> b instance (Trichotomy n s, TEq s SignZero b) => TIsZero n b tIsZero :: TIsZero n b => n -> b; tIsZero = undefined -- | Returns true if the lsb of the number is true class TEven a b | a -> b instance LSB a b c => TEven a b tEven :: (TEven a b) => a -> b; tEven = undefined -- | Returns true if the lsb of the number if false class TOdd a b | a -> b instance (LSB a b c, TNot b b') => TOdd a b' tOdd :: (TOdd a b) => a -> b; tOdd = undefined -- | A symmetrical full adder, that does not yield normal form answers. class TAddC' a b c d | a b c -> d instance TAddC' F F F F instance TAddC' T F T F instance TAddC' F T F T instance TAddC' T T T T instance TAddC' T F F T instance TAddC' F T T F instance TAddC' F F T (I F) instance TAddC' T T F (O T) instance TAddC' F (O a) F (O a) instance TAddC' T (O a) T (O a) instance TAddC' F (I a) F (I a) instance TAddC' T (I a) T (I a) instance TAddC' (O a) F F (O a) instance TAddC' (O a) T T (O a) instance TAddC' (I a) F F (I a) instance TAddC' (I a) T T (I a) instance TAddC' F (O a) T (I a) instance TAddC' T (I a) F (O a) instance TAddC' (O a) F T (I a) instance TAddC' (I a) T F (O a) instance TSucc a b => TAddC' F (I a) T (O b) instance TSucc b a => TAddC' T (O a) F (I b) instance TSucc a b => TAddC' (I a) F T (O b) instance TSucc b a => TAddC' (O a) T F (I b) instance TAddC' a b F c => TAddC' (O a) (O b) F (O c) instance TAddC' a b F c => TAddC' (O a) (O b) T (I c) instance TAddC' a b F c => TAddC' (I a) (O b) F (I c) instance TAddC' a b T c => TAddC' (I a) (O b) T (O c) instance TAddC' a b F c => TAddC' (O a) (I b) F (I c) instance TAddC' a b T c => TAddC' (O a) (I b) T (O c) instance TAddC' a b T c => TAddC' (I a) (I b) F (O c) instance TAddC' a b T c => TAddC' (I a) (I b) T (I c) -- | Transform a number into normal form, but track whether further reductions -- may be necessary if this number is extended for efficiency. class TNF' a b c | a -> b c instance TNF' F F F instance TNF' T T F instance TNF' (O F) F F instance TNF' (I T) T F instance TNF' (I F) (I F) T instance TNF' (O T) (O T) T instance (TNF' (O a) c b) => TNF' (I (O a)) (I c) T instance (TNF' (I a) c b) => TNF' (O (I a)) (O c) T instance (TNF' (I a) c b, TIf b (I c) T d) => TNF' (I (I a)) d b instance (TNF' (O a) c b, TIf b (O c) F d) => TNF' (O (O a)) d b -- | Shed the additional reduction parameter from TNF' class TNF a b | a -> b instance TNF' a b c => TNF a b tNF :: TNF a b => a -> b; tNF = undefined t2n :: TNF (O a) b => a -> b; t2n = undefined t2np1 :: TNF (I a) b => a -> b; t2np1 = undefined -- | Equality comparison. Note this does not equate numbers that -- are non-normalized with their normalized kin. instance TEq (I m) (O n) F instance TEq (O m) (I n) F instance TEq (O m) F F instance TEq (O m) T F instance TEq (I m) T F instance TEq (I m) F F instance (TEq m n b) => TEq (I m) (I n) b instance (TEq m n b) => TEq (O m) (O n) b -- | We have a total order. instance (TBool d, TNeg b b', TAdd' a b' c, TIsNegative c d) => TLt a b d -- | Non-reversible addition. Kept for efficiency purposes. class TAdd' a b c | a b -> c instance (TAddC' a b F d, TNF d d') => TAdd' a b d' tAdd' :: (TAdd' a b c ) => a -> b -> c; tAdd' = undefined -- | Non-reversible subtraction. Kept for efficiency purposes. class TSub' a b c | a b -> c instance (TNeg b b', TAdd' a b' c) => TSub' a b c tSub' :: TSub' a b c => a -> b -> c; tSub' = undefined -- | Reversible adder with extra fundeps. class TAdd a b c | a b -> c, a c -> b, b c -> a instance (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; tAdd = undefined tSub :: (TAdd a b c) => c -> a -> b; tSub = undefined -- | Multiplication: a * b = c class TMul a b c | a b -> c instance TMul a F F instance TNeg a b => TMul a T b instance (TMul (O a) b c) => TMul a (O b) c instance (TMul (O a) b c, TAdd' a c d) => TMul a (I b) d tMul :: TMul a b c => a -> b -> c; tMul = undefined -- | Exponentiation: a^b = c (only defined for non-negative exponents) class TPow a b c | a b -> c instance TPow a F (I F) instance (TPow a k c, TMul c c d) => TPow a (O k) d instance (TPow a k c, TMul c c d, TMul a d e) => TPow a (I k) e tPow :: TPow a b c => a -> b -> c; tPow = undefined {- -- | Reverse the finite head of the number. non-normalizing, needs seed sign class TReverse'' a b c | a b -> b instance TReverse'' F b b instance TReverse'' T b b instance TReverse'' a (O b) c => TReverse (O a) b c instance TReverse'' a (I b) c => TReverse (I a) b c -- | Reverse the finite head of a number yielding a normal form answer class TReverse' a b | a -> b instance (TIsNegative a b, TReverse' a b c, TNF c c') => TReverse' a c' -- | Reverse the finite head of a number, invertably class TReverse a b | a -> b, b -> a instance (TReverse' a b, TReverse' b a) => TReverse a b tReverse :: TReverse a b => a -> b; tReverse = undefined -} -- | Return the absolute value of a class TAbs a b | a -> b instance (TIsNegative a s, TNeg a a', TIf s a' a a'') => TAbs a a'' tAbs :: TAbs a b => a -> b; tAbs = undefined instance TAnd F (I b) F instance TAnd F (O b) F instance TAnd (I a) F F instance TAnd (O a) F F instance TAnd T (I b) (I b) instance TAnd T (O b) (O b) instance TAnd (I a) T (I a) instance TAnd (O a) T (O a) instance (TAnd a b c, TNF (I c) c') => TAnd (I a) (I b) c' instance (TAnd a b c, TNF (O c) c') => TAnd (O a) (I b) c' instance (TAnd a b c, TNF (O c) c') => TAnd (I a) (O b) c' instance (TAnd a b c, TNF (O c) c') => TAnd (O a) (O b) c' instance TOr F (I b) (I b) instance TOr F (O b) (O b) instance TOr (I a) F (I a) instance TOr (O a) F (I a) instance TOr T (I b) T instance TOr T (O b) T instance TOr (I a) T T instance TOr (O a) T T instance (TOr a b c, TNF (I c) c') => TOr (I a) (I b) c' instance (TOr a b c, TNF (I c) c') => TOr (O a) (I b) c' instance (TOr a b c, TNF (I c) c') => TOr (I a) (O b) c' instance (TOr a b c, TNF (O c) c') => TOr (O a) (O b) c' instance TXOr' F (I b) (I b) instance TXOr' F (O b) (O b) instance TXOr' (I b) F (I b) instance TXOr' (O b) F (O b) instance TNot b c => TXOr' T (I b) (O c) instance TNot b c => TXOr' T (O b) (I c) instance TNot b c => TXOr' (I b) T (O c) instance TNot b c => TXOr' (O b) T (I c) instance (TXOr' a b c, TNF (O c) c') => TXOr' (I a) (I b) c' instance (TXOr' a b c, TNF (I c) c') => TXOr' (I a) (O b) c' instance (TXOr' a b c, TNF (I c) c') => TXOr' (O a) (I b) c' instance (TXOr' a b c, TNF (O c) c') => TXOr' (O a) (O b) c' instance TImplies F (I b) T instance TImplies F (O b) T instance TImplies (I a) F T instance TImplies (O a) F T instance TImplies T (I b) (I b) instance TImplies T (O b) (O b) instance TImplies (I a) T (I a) instance TImplies (O a) T (O a) instance (TImplies a b c, TNF (I c) c') => TImplies (I a) (I b) c' instance (TImplies a b c, TNF (I c) c') => TImplies (O a) (I b) c' instance (TImplies a b c, TNF (I c) c') => TImplies (I a) (O b) c' instance (TImplies a b c, TNF (O c) c') => TImplies (O a) (O b) c' -- | Shift a right b places obtaining c. If b is negative then we shift left. -- | TShift' does not yield normal form answers. class TShift' a b c | a b -> c instance TShift' F F F instance TShift' T F T instance TShift' (I a) F (I a) instance TShift' (O a) F (O a) instance TShift' (I a) T a instance TShift' (O a) T a instance TShift' F T F instance TShift' T T T instance (TShift' a b c, TShift' c b d) => TShift' a (O b) d instance (TShift' a b c, TShift' c b d) => TShift' a (I b) (O d) -- | Shift a right b places obtaining c in normal form. -- | If b is negative then we shift left. class TShift a b c' | a b -> c' instance (TShift' a b c, TNF c c') => TShift a b c' tShift :: TShift a b c => a -> b -> c; tShift = undefined -- | get bit #b in a as c in {T,F} class TGetBit a b c | a b -> c instance (TNeg b b', TShift a b' c, LSB c d e) => TGetBit a b d tGetBit :: TGetBit a b c => a -> b -> c; tGetBit = undefined -- | set bit #b in a to T, yielding c. class TSetBit a b c | a b -> c instance (TShift (I F) b c, TOr a c d) => TSetBit a b d tSetBit :: TSetBit a b c => a -> b -> c; tSetBit = undefined -- | set bit #b in a to F, yielding c class TUnSetBit a b c | a b -> c instance (TShift (O T) b c, TAnd a c d) => TUnSetBit a b d tUnSetBit :: TUnSetBit a b c => a -> b -> c; tUnSetBit = undefined -- | change bit #b in a to c in {T,F}, yielding d. class TChangeBit a b c d | a b c -> d instance (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; tChangeBit = undefined -- | toggle the value of bit #b in a, yielding c class TComplementBit a b c | a b -> c instance (TShift (I F) b c, TXOr' a c d) => TComplementBit a b d tComplementBit :: TComplementBit a b c => a -> b -> c; tComplementBit = undefined -- | 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. class TCountBits' a b t | a t -> b instance TCountBits' T T T instance TCountBits' F F F instance TCountBits' a n F => TCountBits' (O a) n F instance TCountBits' a m F => TCountBits' (I a) m T instance (TCountBits' a n F,TSucc n m) => TCountBits' (I a) m F instance (TCountBits' a n F,TSucc m n) => TCountBits' (O a) n T -- | 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. class TCountBits a b | a -> b instance (TIsNegative a t, TCountBits' a b t) => TCountBits a b tCountBits :: TCountBits a b => a -> b; tCountBits = undefined