packages feed

tfp 0.7 → 0.8

raw patch · 30 files changed

+3281/−2181 lines, 30 filesdep +tfpdep −template-haskelldep ~base

Dependencies added: tfp

Dependencies removed: template-haskell

Dependency ranges changed: base

Files

− Data/SizedInt.hs 
@@ -1,157 +0,0 @@-module Data.SizedInt-    ( SizedInt ) where--import Data.Bits-import Types--newtype (NaturalT nT) => SizedInt nT = SizedInt Integer--sizeT :: SizedInt nT-      -> nT-sizeT _ = undefined--mask :: forall nT . NaturalT nT-     => nT-     -> Integer-mask _ = bit (fromIntegerT (undefined :: nT)) - 1--signBit :: forall nT . NaturalT nT-        => nT-        -> Int-signBit _ = fromIntegerT (undefined :: nT) - 1--isNegative :: forall nT . NaturalT nT-           => SizedInt nT-           -> Bool-isNegative (SizedInt x) =-    testBit x $ signBit (undefined :: nT)--instance NaturalT nT => Eq (SizedInt nT) where-    (SizedInt x) == (SizedInt y) = x == y-    (SizedInt x) /= (SizedInt y) = x /= y--instance NaturalT nT => Show (SizedInt nT) where-    showsPrec prec n =-        showsPrec prec $ toInteger n--instance NaturalT nT => Read (SizedInt nT) where-    readsPrec prec str =-        [ (fromInteger n, str)-        | (n, str) <- readsPrec prec str ]--instance NaturalT nT => Ord (SizedInt nT) where-    a `compare` b = toInteger a `compare` toInteger b--instance NaturalT nT => Bounded (SizedInt nT) where-    minBound = SizedInt $ negate $ 1 `shiftL` (fromIntegerT (undefined :: nT) - 1)-    maxBound = SizedInt $ (1 `shiftL` (fromIntegerT (undefined :: nT) - 1)) - 1--instance NaturalT nT => Enum (SizedInt nT) where-    succ x-       | x == maxBound  = error $ "Enum.succ{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `succ' of maxBound"-       | otherwise      = x + 1-    pred x-       | x == minBound  = error $ "Enum.succ{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `pred' of minBound"-       | otherwise      = x - 1-    -    fromEnum (SizedInt x)-        | x > toInteger (maxBound :: Int) =-            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: Int"-        | x < toInteger (minBound :: Int) =-            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: Int"-        | otherwise =-            fromInteger x-    toEnum x-        | x' > toInteger (maxBound :: SizedInt nT) =-            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: SizedInt " ++ show (fromIntegerT (undefined :: nT))-        | x' < toInteger (minBound :: SizedInt nT) =-            error $ "Enum.fromEnum{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: SizedInt " ++ show (fromIntegerT (undefined :: nT))-        | otherwise =-            fromInteger x'-            where x' = toInteger x--instance NaturalT nT => Num (SizedInt nT) where-    (SizedInt a) + (SizedInt b) =-        fromInteger $ a + b-    (SizedInt a) * (SizedInt b) =-        fromInteger $ a * b-    negate (SizedInt n) =-        fromInteger $ (n `xor` mask (undefined :: nT)) + 1-    a - b =-        a + (negate b)-    -    fromInteger n-      | n > 0 =-        SizedInt $ n .&. mask (undefined :: nT)-    fromInteger n-      | n < 0 =-        negate $ fromInteger $ negate n-    fromInteger _ =-        SizedInt 0-    -    abs s-      | isNegative s =-          negate s-      | otherwise =-          s-    signum s-      | isNegative s =-          -1-      | s == 0 =-          0-      | otherwise =-          1--instance NaturalT nT => Real (SizedInt nT) where-    toRational n = toRational $ toInteger n--instance NaturalT nT => Integral (SizedInt nT) where-    a `quot` b =-        fromInteger $ toInteger a `quot` toInteger b-    a `rem` b =-        fromInteger $ toInteger a `rem` toInteger b-    a `div` b =-        fromInteger $ toInteger a `div` toInteger b-    a `mod` b =-        fromInteger $ toInteger a `mod` toInteger b-    a `quotRem` b =-        let (quot, rem) = toInteger a `quotRem` toInteger b-        in (fromInteger quot, fromInteger rem)-    a `divMod` b =-        let (div, mod) = toInteger a `divMod` toInteger b-        in (fromInteger div, fromInteger mod)-    toInteger s@(SizedInt x) =-        if isNegative s-           then let SizedInt x' = negate s in negate x'-           else x--instance NaturalT nT => Bits (SizedInt nT) where-    (SizedInt a) .&. (SizedInt b) = SizedInt $ a .&. b-    (SizedInt a) .|. (SizedInt b) = SizedInt $ a .|. b-    (SizedInt a) `xor` SizedInt b = SizedInt $ a `xor` b-    complement (SizedInt x) = SizedInt $ x `xor` mask (undefined :: nT)-    (SizedInt x) `shiftL` b-      | b < 0 = error $ "Bits.shiftL{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to shift by negative amount"-      | otherwise =-        SizedInt $ mask (undefined :: nT) .&. (x `shiftL` b)-    s@(SizedInt x) `shiftR` b-      | b < 0 = error $ "Bits.shiftR{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to shift by negative amount"-      | isNegative s =-        SizedInt $ mask (undefined :: nT) .&.-            ((x `shiftR` b) .|. (mask (undefined :: nT) `shiftL` (fromIntegerT (undefined :: nT) - b)))-      | otherwise =-        SizedInt $ (mask (undefined :: nT)) .&. (x `shiftR` b)-    (SizedInt a) `rotateL` b-      | b < 0 =-        error $ "Bits.rotateL{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to rotate by negative amount"-      | otherwise =-        SizedInt $ mask (undefined :: nT) .&.-            ((a `shiftL` b) .|. (a `shiftR` (fromIntegerT (undefined :: nT) - b)))-    (SizedInt a) `rotateR` b-      | b < 0 =-        error $ "Bits.rotateR{SizedInt " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to rotate by negative amount"-      | otherwise =-        SizedInt $ mask (undefined :: nT) .&.-            ((a `shiftR` b) .|. (a `shiftL` (fromIntegerT (undefined :: nT) - b)))-    bitSize _ = fromIntegerT (undefined :: nT)-    isSigned _ = True
− Data/SizedWord.hs 
@@ -1,133 +0,0 @@-module Data.SizedWord-    ( SizedWord ) where--import Data.Bits-import Types--newtype (NaturalT nT) => SizedWord nT = SizedWord Integer--sizeT :: SizedWord nT-      -> nT-sizeT _ = undefined--mask :: forall nT . NaturalT nT-     => nT-     -> Integer-mask _ = bit (fromIntegerT (undefined :: nT)) - 1--instance NaturalT nT => Eq (SizedWord nT) where-    (SizedWord x) == (SizedWord y) = x == y-    (SizedWord x) /= (SizedWord y) = x /= y--instance NaturalT nT => Show (SizedWord nT) where-    showsPrec prec n =-        showsPrec prec $ toInteger n--instance NaturalT nT => Read (SizedWord nT) where-    readsPrec prec str =-        [ (fromInteger n, str)-        | (n, str) <- readsPrec prec str ]--instance NaturalT nT => Ord (SizedWord nT) where-    a `compare` b = toInteger a `compare` toInteger b--instance NaturalT nT => Bounded (SizedWord nT) where-    minBound = 0-    maxBound = SizedWord $ (1 `shiftL` (fromIntegerT (undefined :: nT))) - 1--instance NaturalT nT => Enum (SizedWord nT) where-    succ x-       | x == maxBound  = error $ "Enum.succ{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `succ' of maxBound"-       | otherwise      = x + 1-    pred x-       | x == minBound  = error $ "Enum.succ{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `pred' of minBound"-       | otherwise      = x - 1-    -    fromEnum (SizedWord x)-        | x > toInteger (maxBound :: Int) =-            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: Int"-        | x < toInteger (minBound :: Int) =-            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: Int"-        | otherwise =-            fromInteger x-    toEnum x-        | x > fromIntegral (maxBound :: SizedWord nT) =-            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: SizedWord " ++ show (fromIntegerT (undefined :: nT))-        | x < fromIntegral (minBound :: SizedWord nT) =-            error $ "Enum.fromEnum{SizedWord " ++ show (fromIntegerT (undefined :: nT)) ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: SizedWord " ++ show (fromIntegerT (undefined :: nT))-        | otherwise =-            fromInteger $ toInteger x--instance NaturalT nT => Num (SizedWord nT) where-    (SizedWord a) + (SizedWord b) =-        fromInteger $ a + b-    (SizedWord a) * (SizedWord b) =-        fromInteger $ a * b-    negate s@(SizedWord n) =-        fromInteger $ (n `xor` mask (sizeT s)) + 1-    a - b =-        a + (negate b)-    -    fromInteger n-      | n > 0 =-        SizedWord $ n .&. mask (undefined :: nT)-    fromInteger n-      | n < 0 =-        negate $ fromInteger $ negate n-    fromInteger _ =-        SizedWord 0-    -    abs s = s-    signum s-      | s == 0 =-          0-      | otherwise =-          1--instance NaturalT nT => Real (SizedWord nT) where-    toRational n = toRational $ toInteger n--instance NaturalT nT => Integral (SizedWord nT) where-    a `quot` b =-        fromInteger $ toInteger a `quot` toInteger b-    a `rem` b =-        fromInteger $ toInteger a `rem` toInteger b-    a `div` b =-        fromInteger $ toInteger a `div` toInteger b-    a `mod` b =-        fromInteger $ toInteger a `mod` toInteger b-    a `quotRem` b =-        let (quot, rem) = toInteger a `quotRem` toInteger b-        in (fromInteger quot, fromInteger rem)-    a `divMod` b =-        let (div, mod) = toInteger a `divMod` toInteger b-        in (fromInteger div, fromInteger mod)-    toInteger s@(SizedWord x) = x--instance NaturalT nT => Bits (SizedWord nT) where-    (SizedWord a) .&. (SizedWord b) = SizedWord $ a .&. b-    (SizedWord a) .|. (SizedWord b) = SizedWord $ a .|. b-    (SizedWord a) `xor` SizedWord b = SizedWord $ a `xor` b-    complement (SizedWord x) = SizedWord $ x `xor` mask (undefined :: nT)-    s@(SizedWord x) `shiftL` b-      | b < 0 = error $ "Bits.shiftL{SizedWord " ++ show (bitSize s) ++ "}: tried to shift by negative amount"-      | otherwise =-        SizedWord $ mask (undefined :: nT) .&. (x `shiftL` b)-    s@(SizedWord x) `shiftR` b-      | b < 0 = error $ "Bits.shiftR{SizedWord " ++ show (bitSize s) ++ "}: tried to shift by negative amount"-      | otherwise =-        SizedWord $ (x `shiftR` b)-    s@(SizedWord x) `rotateL` b-      | b < 0 =-        error $ "Bits.rotateL{SizedWord " ++ show (bitSize s) ++ "}: tried to rotate by negative amount"-      | otherwise =-        SizedWord $ mask (undefined :: nT) .&.-            ((x `shiftL` b) .|. (x `shiftR` (bitSize s - b)))-    s@(SizedWord x) `rotateR` b-      | b < 0 =-        error $ "Bits.rotateR{SizedWord " ++ show (bitSize s) ++ "}: tried to rotate by negative amount"-      | otherwise =-        SizedWord $ mask (undefined :: nT) .&.-            ((x `shiftR` b) .|. (x `shiftL` (bitSize s - b)))-    bitSize _ = fromIntegerT (undefined :: nT)-    isSigned _ = False
− Test.hs 
@@ -1,252 +0,0 @@-module Main where--import qualified Test.QuickCheck as Q--import qualified Prelude-import Data.Char (intToDigit)-import Control.Monad (when)--import Types-import Types.Data.Num.Decimal.Literals.TH--testIsPositive1 :: IsPositive D1 -> True-testIsPositive1 = Prelude.id-testIsPositive2 :: IsPositive D0 -> False-testIsPositive2 = Prelude.id-testIsPositive3 :: IsPositive DN1 -> False-testIsPositive3 = Prelude.id-testIsPositive4 :: IsPositive D10 -> True-testIsPositive4 = Prelude.id-testIsPositive5 :: IsPositive DN10 -> False-testIsPositive5 = Prelude.id--testIsNegative1 :: IsNegative D1 -> False-testIsNegative1 = Prelude.id-testIsNegative2 :: IsNegative D0 -> False-testIsNegative2 = Prelude.id-testIsNegative3 :: IsNegative DN1 -> True-testIsNegative3 = Prelude.id-testIsNegative4 :: IsNegative D10 -> False-testIsNegative4 = Prelude.id-testIsNegative5 :: IsNegative DN10 -> True-testIsNegative5 = Prelude.id--testIsZero1 :: IsZero D1 -> False-testIsZero1 = Prelude.id-testIsZero2 :: IsZero D0 -> True-testIsZero2 = Prelude.id-testIsZero3 :: IsZero DN1 -> False-testIsZero3 = Prelude.id-testIsZero4 :: IsZero D10 -> False-testIsZero4 = Prelude.id-testIsZero5 :: IsZero DN10 -> False-testIsZero5 = Prelude.id--testSucc1 :: Succ D0 -> D1-testSucc1 = Prelude.id-testSucc2 :: Succ D9 -> D10-testSucc2 = Prelude.id-testSucc3 :: Succ DN1 -> D0-testSucc3 = Prelude.id-testSucc4 :: Succ D99 -> D100-testSucc4 = Prelude.id-testSucc5 :: Succ DN100 -> DN99-testSucc5 = Prelude.id-testSucc6 :: Succ D100 -> D101-testSucc6 = Prelude.id-testSucc7 :: Succ DN101 -> DN100-testSucc7 = Prelude.id-testSucc8 :: Succ D0 -> D1 :+: D0-testSucc8 = Prelude.id-testSucc9 :: Succ D0 -> D0 :+: D1-testSucc9 = Prelude.id-testSucc10 :: Succ D9 -> D1 :+: D9-testSucc10 = Prelude.id-testSucc11 :: Succ D9 -> D9 :+: D1-testSucc11 = Prelude.id--testPred1 :: Pred D1 -> D0-testPred1 = Prelude.id-testPred2 :: Pred D0 -> DN1-testPred2 = Prelude.id-testPred3 :: Pred DN1 -> DN2-testPred3 = Prelude.id-testPred4 :: Pred DN9 -> DN10-testPred4 = Prelude.id-testPred5 :: Pred D10 -> D9-testPred5 = Prelude.id-testPred6 :: Pred DN99 -> DN100-testPred6 = Prelude.id-testPred7 :: Pred D100 -> D99-testPred7 = Prelude.id-testPred8 :: Pred D0 -> D0 :-: D1-testPred8 = Prelude.id-testPred9 :: Pred D10 -> D10 :-: D1-testPred9 = Prelude.id-testPred10 :: Pred D9 -> D8-testPred10 = Prelude.id-testPred11 :: Pred D8 -> D7-testPred11 = Prelude.id-testPred12 :: Pred D7 -> D6-testPred12 = Prelude.id-testPred13 :: Pred D6 -> D5-testPred13 = Prelude.id-testPred14 :: Pred D5 -> D4-testPred14 = Prelude.id-testPred15 :: Pred D4 -> D3-testPred15 = Prelude.id-testPred16 :: Pred D3 -> D2-testPred16 = Prelude.id-testPred17 :: Pred D2 -> D1-testPred17 = Prelude.id-testPred18 :: Pred D1 -> D0-testPred18 = Prelude.id--testAdd1 :: D0 :+: D0 -> D0-testAdd1 = Prelude.id-testAdd2 :: DN1 :+: D1 -> D0-testAdd2 = Prelude.id-testAdd3 :: D1 :+: DN1 -> D0-testAdd3 = Prelude.id-testAdd4 :: D1 :+: D1 -> D2-testAdd4 = Prelude.id-testAdd5 :: D9 :+: D1 -> D10-testAdd5 = Prelude.id-testAdd6 :: D10 :+: DN1 -> D9-testAdd6 = Prelude.id-testAdd7 :: D100 :+: DN1 -> D99-testAdd7 = Prelude.id-testAdd8 :: D100 :+: DN10 -> D90-testAdd8 = Prelude.id--testSub1 :: D0 :-: D0 -> D0-testSub1 = Prelude.id-testSub2 :: D1 :-: D0 -> D1-testSub2 = Prelude.id-testSub3 :: D0 :-: D1 -> DN1-testSub3 = Prelude.id-testSub4 :: DN1 :-: D0 -> DN1-testSub4 = Prelude.id-testSub5 :: D0 :-: DN1 -> D1-testSub5 = Prelude.id-testSub6 :: D100 :-: D1 -> D99-testSub6 = Prelude.id-testSub7 :: DN100 :-: D1 -> DN101-testSub7 = Prelude.id-testSub8 :: D100 :-: DN1 -> D101-testSub8 = Prelude.id-testSub9 :: DN100 :-: DN1 -> DN99-testSub9 = Prelude.id-testSub10 :: D1 :-: D100 -> DN99-testSub10 = Prelude.id-testSub11 :: DN1 :-: D100 -> DN101-testSub11 = Prelude.id-testSub12 :: D1 :-: DN100 -> D101-testSub12 = Prelude.id-testSub13 :: DN1 :-: DN100 -> D99-testSub13 = Prelude.id-testSub14 :: D57 :-: D58 -> DN1-testSub14 = Prelude.id-testSub15 :: D1000 :-: D11 -> D989-testSub15 = Prelude.id--testMul1 :: D0 :*: D0 -> D0-testMul1 = Prelude.id-testMul2 :: D1 :*: D1 -> D1-testMul2 = Prelude.id-testMul3 :: D0 :*: D1 -> D0-testMul3 = Prelude.id-testMul4 :: D1 :*: D0 -> D0-testMul4 = Prelude.id-testMul5 :: D1 :*: DN1 -> DN1-testMul5 = Prelude.id-testMul6 :: DN1 :*: D1 -> DN1-testMul6 = Prelude.id-testMul7 :: DN1 :*: DN1 -> D1-testMul7 = Prelude.id-testMul8 :: D100 :*: D100 -> D10000-testMul8 = Prelude.id-testMul9 :: D17 :*: D31 -> D527-testMul9 = Prelude.id--testFac1 :: Fac D0 -> D1-testFac1 = Prelude.id-testFac2 :: Fac D1 -> D1-testFac2 = Prelude.id-testFac3 :: Fac D6 -> D720-testFac3 = Prelude.id-$( decLiteralD "D" "d" 3628800 )-testFac4 :: Fac D10 -> D3628800-testFac4 = Prelude.id--testEQ1 :: D0 :==: D0 -> True-testEQ1 = Prelude.id-testEQ2 :: D0 :==: Pred D1 -> True-testEQ2 = Prelude.id-testEQ3 :: (D1 :+: D9) :==: D10 -> True-testEQ3 = Prelude.id-testEQ4 :: (D1 :+: D9) :==: D11 -> False-testEQ4 = Prelude.id-testEQ5 :: D9 :==: D0 -> False-testEQ5 = Prelude.id-testEQ6 :: D8 :==: D0 -> False-testEQ6 = Prelude.id-testEQ7 :: D7 :==: D0 -> False-testEQ7 = Prelude.id-testEQ8 :: D6 :==: D0 -> False-testEQ8 = Prelude.id-testEQ9 :: D5 :==: D0 -> False-testEQ9 = Prelude.id-testEQ10 :: D4 :==: D0 -> False-testEQ10 = Prelude.id-testEQ11 :: D3 :==: D0 -> False-testEQ11 = Prelude.id-testEQ12 :: D2 :==: D0 -> False-testEQ12 = Prelude.id-testEQ13 :: D1 :==: D0 -> False-testEQ13 = Prelude.id--testMin1 :: Min D0 D5 -> D0-testMin1 = Prelude.id-testMin2 :: Min D5 D0 -> D0-testMin2 = Prelude.id-testMin3 :: Min DN5 D5 -> DN5-testMin3 = Prelude.id--testMax1 :: Max D1 D6 -> D6-testMax1 = Prelude.id-testMax2 :: Max DN6 D6 -> D6-testMax2 = Prelude.id-testMax3 :: Max D6 D1 -> D6-testMax3 = Prelude.id--testLog1 :: Log2Ceil D8 -> D3-testLog1 = Prelude.id-testLog2 :: Log2Ceil D9 -> D4-testLog2 = Prelude.id-testLog3 :: Log2Ceil D2 -> D1-testLog3 = Prelude.id-testLog4 :: Log2Ceil D1 -> D0-testLog4 = Prelude.id--class TestIter n zero where-    testIter :: n -> zero -> Prelude.String--instance ( NaturalT n-         , (n :==: D0) ~ True )-  => TestIter n True where-    testIter _ _ = ""--instance ( NaturalT n-         , (n :==: D0) ~ False-         , TestIter (Pred n) ((Pred n) :==: D0) )-  => TestIter n False where-    testIter n _ =-        intToDigit (fromIntegerT n) : testIter (_T :: (Pred n)) (_T :: ((Pred n) :==: D0))--main = do-  let testIterResult = testIter d9 (_T :: False)-  when (testIterResult Prelude./= "987654321") (Prelude.putStrLn ("testIter failed, got: " Prelude.++ testIterResult))-  Q.quickCheck prop_reifyIntegral--prop_reifyIntegral i = reifyIntegral (Prelude.undefined :: Decimal) i fromIntegerT Prelude.== i
− Types.hs 
@@ -1,13 +0,0 @@-module Types-    ( module Types.Base-    , module Types.Data.Bool-    , module Types.Data.Num-    , module Types.Data.List-    , module Types.Data.Ord-    ) where--import Types.Base-import Types.Data.Bool-import Types.Data.Num-import Types.Data.List-import Types.Data.Ord
− Types/Base.hs 
@@ -1,24 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Types.Data.Decimal.Ops--- Copyright   :  (c) 2008 Peter Gavin--- License     :  BSD-style (see the file LICENSE)--- --- Maintainer  :  pgavin@gmail.com--- Stability   :  experimental--- Portability :  non-portable (type families, requires ghc >= 6.9)------ Type-level numerical operations using type families.--- -------------------------------------------------------------------------------module Types.Base-    where--import qualified Prelude--type family Id x-type instance Id x = x--_T :: a-_T = Prelude.undefined
− Types/Data/Bool.hs 
@@ -1,70 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Types.Data.Bool--- Copyright   :  (c) 2008 Peter Gavin--- License     :  BSD-style (see the file LICENSE)--- --- Maintainer  :  pgavin@gmail.com--- Stability   :  experimental--- Portability :  non-portable (type families, requires ghc >= 6.9)------ Type-level numerical operations using type families.--- -------------------------------------------------------------------------------module Types.Data.Bool-    ( True-    , trueT-    , False-    , falseT-    , Not-    , notT-    , (:&&:)-    , andT-    , (:||:)-    , orT-    , IfT(..)-    ) where--import Data.Typeable--import qualified Prelude--data True deriving (Typeable)-trueT :: True-trueT = Prelude.undefined-instance Prelude.Show True where-    show _ = "True"-data False deriving (Typeable)-falseT :: False-falseT = Prelude.undefined-instance Prelude.Show False where-    show _ = "False"--type family Not x-type instance Not False = True-type instance Not True  = False-notT :: x -> Not x-notT _ = Prelude.undefined--type family x :&&: y-type instance False :&&: x = False-type instance True  :&&: x = x-andT :: x -> y -> x :&&: y-andT _ _ = Prelude.undefined--type family x :||: y-type instance True  :||: x = True-type instance False :||: x = x-orT :: x -> y -> x :||: y-orT _ _ = Prelude.undefined--class IfT x y z where-    type If x y z-    ifT :: x -> y -> z -> If x y z-instance IfT True y z where-    type If True y z = y-    ifT _ y _ = y-instance IfT False y z where-    type If False y z = z-    ifT _ _ z = z
− Types/Data/List.hs 
@@ -1,47 +0,0 @@-module Types.Data.List-    ( Cons-    , Null-    , IsNull-    , Head-    , Tail-    , Reverse-    , Append-    ) where--import qualified Prelude--import Data.Typeable--import Types.Data.Bool--data Cons car cdr deriving (Typeable)-instance (Prelude.Show car, Prelude.Show cdr) => Prelude.Show (Cons car cdr) where-    show = showCons--showCons :: forall car cdr . (Prelude.Show car, Prelude.Show cdr) => Cons car cdr -> Prelude.String-showCons _ = "Cons (" Prelude.++ Prelude.show (Prelude.undefined :: car) Prelude.++ ") (" Prelude.++ Prelude.show (Prelude.undefined :: cdr) Prelude.++ ")"--data Null deriving (Typeable)-instance Prelude.Show Null where-    show _ = ""--type family IsNull l-type instance IsNull (Cons car cdr) = False-type instance IsNull Null = True--type family Head l-type instance Head (Cons car cdr) = car--type family Tail l-type instance Tail (Cons car cdr) = cdr--type family Reverse l-type instance Reverse l = Reverse' l Null--type family Reverse' l a-type instance Reverse' Null a = a-type instance Reverse' (Cons car cdr) a = Reverse' cdr (Cons car a)--type family Append l1 l2-type instance Append Null l2 = l2-type instance Append (Cons car1 cdr2) l2 = Cons car1 (Append cdr2 l2)
− Types/Data/Num.hs 
@@ -1,55 +0,0 @@-{-# LANGUAGE CPP #-}--------------------------------------------------------------------------------- |--- Module      :  Types.Data.Num--- Copyright   :  (c) 2008 Peter Gavin--- License     :  BSD-style (see the file LICENSE)--- --- Maintainer  :  pgavin@gmail.com--- Stability   :  experimental--- Portability :  non-portable (type families, requires ghc >= 6.9)------ Type-level numerical operations using type families.--- -------------------------------------------------------------------------------module Types.Data.Num-    ( module Types.Data.Num.Ops-    , module Types.Data.Num.Decimal-#if __GLASGOW_HASKELL__ >= 704 || __GLASGOW_HASKELL__ < 700-    , reifyIntegralD-    , reifyPositiveD-    , reifyNegativeD-    , reifyNaturalD-#endif-    ) where--import Types.Data.Num.Ops-import Types.Data.Num.Decimal---- An explanation of the following is in order:---- Versions of GHC prior to 7.0 (e.g., 6.12.3) will compile this code--- as long as the type signature isn't there.--- Versions 7.0 and later, but before 7.4 will not compile it at all,--- with or without the type signature.--- Version 7.4 and later handles everything just fine.--#if __GLASGOW_HASKELL__ >= 704 || __GLASGOW_HASKELL__ < 700-#if __GLASGOW_HASKELL__ >= 704-reifyIntegralD :: Integer -> (forall s. (IntegerT s, Repr s ~ Decimal) => s -> a) -> a-#endif-reifyIntegralD = reifyIntegral decimal-#if __GLASGOW_HASKELL__ >= 704-reifyPositiveD :: Integer -> (forall s. (PositiveT s, Repr s ~ Decimal) => s -> a) -> Maybe a-#endif-reifyPositiveD = reifyPositive decimal-#if __GLASGOW_HASKELL__ >= 704-reifyNegativeD :: Integer -> (forall s. (NegativeT s, Repr s ~ Decimal) => s -> a) -> Maybe a-#endif-reifyNegativeD = reifyNegative decimal-#if __GLASGOW_HASKELL__ >= 704-reifyNaturalD :: Integer -> (forall s. (NaturalT s, Repr s ~ Decimal) => s -> a) -> Maybe a-#endif-reifyNaturalD = reifyNatural decimal-#endif
− Types/Data/Num/Decimal.hs 
@@ -1,9 +0,0 @@-module Types.Data.Num.Decimal-    ( module Types.Data.Num.Decimal.Digits-    , module Types.Data.Num.Decimal.Literals-    , module Types.Data.Num.Decimal.Ops-    ) where--import Types.Data.Num.Decimal.Digits-import Types.Data.Num.Decimal.Literals-import Types.Data.Num.Decimal.Ops ()
− Types/Data/Num/Decimal/Digits.hs 
@@ -1,65 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Types.Data.Num.Decimal.Digits--- Copyright   :  (c) 2008 Peter Gavin--- License     :  BSD-style (see the file LICENSE)--- --- Maintainer  :  pgavin@gmail.com--- Stability   :  experimental--- Portability :  non-portable (type families, requires ghc >= 6.9)------ Type-level numerical operations using type families.--- -------------------------------------------------------------------------------module Types.Data.Num.Decimal.Digits-    where--import Data.Typeable--import Types.Data.List-import Types.Data.Num.Ops---- | Representation name for decimal type level numbers.-data Decimal-decimal = undefined :: Decimal---- | The wrapper type for decimal type level numbers.-data Dec x-data Neg' x---- | The terminator type for decimal digit lists.-data DecN-instance Show DecN where-    show _ = ""--data Dec0 deriving (Typeable)-instance Show Dec0 where-    show _ = "0"-data Dec1 deriving (Typeable)-instance Show Dec1 where-    show _ = "1"-data Dec2 deriving (Typeable)-instance Show Dec2 where-    show _ = "2"-data Dec3 deriving (Typeable)-instance Show Dec3 where-    show _ = "3"-data Dec4 deriving (Typeable)-instance Show Dec4 where-    show _ = "4"-data Dec5 deriving (Typeable)-instance Show Dec5 where-    show _ = "5"-data Dec6 deriving (Typeable)-instance Show Dec6 where-    show _ = "6"-data Dec7 deriving (Typeable)-instance Show Dec7 where-    show _ = "7"-data Dec8 deriving (Typeable)-instance Show Dec8 where-    show _ = "8"-data Dec9 deriving (Typeable)-instance Show Dec9 where-    show _ = "9"
− Types/Data/Num/Decimal/Literals.hs 
@@ -1,8 +0,0 @@-module Types.Data.Num.Decimal.Literals where--import Types.Data.Num.Decimal.Literals.TH--import Types.Data.Num.Decimal.Digits-import Types.Data.Num.Ops--$( decLiteralsD "D" "d" (-10000) (10000) )
− Types/Data/Num/Decimal/Literals/TH.hs 
@@ -1,46 +0,0 @@-module Types.Data.Num.Decimal.Literals.TH where--import Language.Haskell.TH--import qualified Types.Data.Num.Decimal.Digits as D-import qualified Types.Data.Num.Ops as O--decLiteralT :: Integer -> Q Type-decLiteralT n = appT (conT (''D.Dec)) (decLiteralT' n)-    where decLiteralT' n | n < 0     = appT (conT ''D.Neg') (decLiteralT' (-n))-                         | n == 0    = conT ''D.DecN-                         | otherwise = appT (appT (conT ''(O.:.)) (decLiteralT' (n `div` 10))) (conT (case n `mod` 10 of-                                                  0 -> ''D.Dec0 -                                                  1 -> ''D.Dec1-                                                  2 -> ''D.Dec2-                                                  3 -> ''D.Dec3-                                                  4 -> ''D.Dec4-                                                  5 -> ''D.Dec5-                                                  6 -> ''D.Dec6-                                                  7 -> ''D.Dec7-                                                  8 -> ''D.Dec8-                                                  9 -> ''D.Dec9))--decLiteralV :: Integer -> Q Exp-decLiteralV n = sigE [| undefined |] (decLiteralT n)--decLiteralD :: String-            -> String-            -> Integer-            -> Q [Dec]-decLiteralD typePrefix valPrefix n =-    do let suffix = if n < 0 then "N" ++ show (-n) else show n-           typeName = mkName $ typePrefix ++ suffix-           valName = mkName $ valPrefix ++ suffix-       tySyn <- tySynD typeName [] (decLiteralT n)-       sig   <- sigD valName (conT typeName)-       val   <- valD (varP valName) (normalB [| undefined |]) []-       return [ tySyn, sig, val ]--decLiteralsD :: String-             -> String-             -> Integer-             -> Integer-             -> Q [Dec]-decLiteralsD typePrefix valPrefix from to =-    fmap concat $ sequence $ [ decLiteralD typePrefix valPrefix n | n <- [from..to] ]
− Types/Data/Num/Decimal/Ops.hs 
@@ -1,924 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Types.Data.Num.Decimal.Ops--- Copyright   :  (c) 2008 Peter Gavin--- License     :  BSD-style (see the file LICENSE)--- --- Maintainer  :  pgavin@gmail.com--- Stability   :  experimental--- Portability :  non-portable (type families, requires ghc >= 6.9)------ Type-level numerical operations using type families.--- -------------------------------------------------------------------------------module Types.Data.Num.Decimal.Ops ()-    where--import Types.Base-import Types.Data.Bool-import Types.Data.Ord-import Types.Data.Num.Ops-import Types.Data.Num.Decimal.Literals-import Types.Data.Num.Decimal.Digits--instance IntegerR Decimal where-    reifyIntegral _ i k = reifyIntegral' i (\(_ :: s) -> k (undefined :: Dec s))--reifyIntegral' :: Integer -> (forall s. IntegerT' s => s -> w) -> w-reifyIntegral' i k | i <  0    = go (negate i) (\(_ :: s) -> k (undefined :: Neg' s)) -                   | otherwise = go i k-  where-   go :: Integer -> (forall s. IntegerT' s => s -> w) -> w-   go 0 k = k (undefined :: DecN)-   go i k = let (j, d) =  quotRem i 10 in case d of-     0 -> go j (\(_ :: s) -> k (undefined :: s :. Dec0))-     1 -> go j (\(_ :: s) -> k (undefined :: s :. Dec1))-     2 -> go j (\(_ :: s) -> k (undefined :: s :. Dec2))-     3 -> go j (\(_ :: s) -> k (undefined :: s :. Dec3))-     4 -> go j (\(_ :: s) -> k (undefined :: s :. Dec4))-     5 -> go j (\(_ :: s) -> k (undefined :: s :. Dec5))-     6 -> go j (\(_ :: s) -> k (undefined :: s :. Dec6))-     7 -> go j (\(_ :: s) -> k (undefined :: s :. Dec7))-     8 -> go j (\(_ :: s) -> k (undefined :: s :. Dec8))-     9 -> go j (\(_ :: s) -> k (undefined :: s :. Dec9))--instance IntegerT' x => IntegerT (Dec x) where-    fromIntegerT _ = fromIntegerT' (undefined :: x)-    type Repr (Dec x) = Decimal--class IntegerT' x where-    fromIntegerT' :: Num y => x -> y-instance IntegerT' DecN where-    fromIntegerT' _ = 0-instance IntegerT' x => IntegerT' (Neg' x) where-    fromIntegerT' _ = negate (fromIntegerT' (undefined :: x))-instance IntegerT' xh => IntegerT' (xh :. Dec0) where-    fromIntegerT' _ = 0 + 10 * fromIntegerT' (undefined :: xh)-instance IntegerT' xh => IntegerT' (xh :. Dec1) where-    fromIntegerT' _ = 1 + 10 * fromIntegerT' (undefined :: xh)-instance IntegerT' xh => IntegerT' (xh :. Dec2) where-    fromIntegerT' _ = 2 + 10 * fromIntegerT' (undefined :: xh)-instance IntegerT' xh => IntegerT' (xh :. Dec3) where-    fromIntegerT' _ = 3 + 10 * fromIntegerT' (undefined :: xh)-instance IntegerT' xh => IntegerT' (xh :. Dec4) where-    fromIntegerT' _ = 4 + 10 * fromIntegerT' (undefined :: xh)-instance IntegerT' xh => IntegerT' (xh :. Dec5) where-    fromIntegerT' _ = 5 + 10 * fromIntegerT' (undefined :: xh)-instance IntegerT' xh => IntegerT' (xh :. Dec6) where-    fromIntegerT' _ = 6 + 10 * fromIntegerT' (undefined :: xh)-instance IntegerT' xh => IntegerT' (xh :. Dec7) where-    fromIntegerT' _ = 7 + 10 * fromIntegerT' (undefined :: xh)-instance IntegerT' xh => IntegerT' (xh :. Dec8) where-    fromIntegerT' _ = 8 + 10 * fromIntegerT' (undefined :: xh)-instance IntegerT' xh => IntegerT' (xh :. Dec9) where-    fromIntegerT' _ = 9 + 10 * fromIntegerT' (undefined :: xh)--type family Normalize x-type instance Normalize (Dec x) = Dec (Normalize' x)--type family Normalize' x-type instance Normalize' DecN       = DecN-type instance Normalize' (xh :. xl) = NormalizePos (xh :. xl)-type instance Normalize' (Neg' x)   = NormalizeNeg x--type family NormalizePos x-type instance NormalizePos x = NormalizePos' (ReverseDigits x)-type family NormalizePos' x-type instance NormalizePos' DecN         = DecN-type instance NormalizePos' (xh :. Dec0) = NormalizePos' xh-type instance NormalizePos' (xh :. Dec1) = ReverseDigits (xh :. Dec1)-type instance NormalizePos' (xh :. Dec2) = ReverseDigits (xh :. Dec2)-type instance NormalizePos' (xh :. Dec3) = ReverseDigits (xh :. Dec3)-type instance NormalizePos' (xh :. Dec4) = ReverseDigits (xh :. Dec4)-type instance NormalizePos' (xh :. Dec5) = ReverseDigits (xh :. Dec5)-type instance NormalizePos' (xh :. Dec6) = ReverseDigits (xh :. Dec6)-type instance NormalizePos' (xh :. Dec7) = ReverseDigits (xh :. Dec7)-type instance NormalizePos' (xh :. Dec8) = ReverseDigits (xh :. Dec8)-type instance NormalizePos' (xh :. Dec9) = ReverseDigits (xh :. Dec9)--type family ReverseDigits x-type instance ReverseDigits DecN       = DecN-type instance ReverseDigits (xh :. xl) = ReverseDigits' (xh :. xl) DecN--type family ReverseDigits' x y-type instance ReverseDigits' DecN y = y-type instance ReverseDigits' (xh :. xl) y = ReverseDigits' xh (y :. xl)--type family NormalizeNeg x-type instance NormalizeNeg (Neg' x)   = Normalize' x -- negate . negate == id-type instance NormalizeNeg DecN       = DecN         -- negate 0 = 0-type instance NormalizeNeg (xh :. xl) = NormalizeNeg' (NormalizePos (xh :. xl))--type family NormalizeNeg' x-type instance NormalizeNeg' DecN = DecN-type instance NormalizeNeg' (xh :. xl) = Neg' (xh :. xl)---- type family IsPositive x-type instance IsPositive (Dec x) = IsPositive' x-type family IsPositive' x-type instance IsPositive' (Neg' x)   = False-type instance IsPositive' DecN       = False-type instance IsPositive' (xh :. xl) = True---- type family IsZero x-type instance IsZero (Dec x) = IsZero' x-type family IsZero' x-type instance IsZero' (Neg' x)   = False-type instance IsZero' DecN       = True-type instance IsZero' (xh :. xl) = False---- type family IsNegative x-type instance IsNegative (Dec x) = IsNegative' x-type family IsNegative' x-type instance IsNegative' (Neg' x)   = True-type instance IsNegative' DecN       = False-type instance IsNegative' (xh :. xl) = False---- type family IsNatural x-type instance IsNatural (Dec x) = IsNatural' x-type family IsNatural' x-type instance IsNatural' (Neg' x)   = False-type instance IsNatural' DecN       = True-type instance IsNatural' (xh :. xl) = True---- type family Neg x-type instance Neg (Dec DecN)     = Dec DecN-type instance Neg (Dec (Neg' x)) = Dec x-type instance Neg (Dec (xh :. xl)) = Dec (Neg' (xh :. xl))---- type family Succ x-type instance Succ (Dec x) = Dec (Succ' x)--type family Succ' x-type instance Succ' (Neg' x   ) = Normalize' (Neg' (Pred'' x))-type instance Succ' (DecN     ) = DecN :. Dec1-type instance Succ' (x :. Dec0) = x :. Dec1-type instance Succ' (x :. Dec1) = x :. Dec2-type instance Succ' (x :. Dec2) = x :. Dec3-type instance Succ' (x :. Dec3) = x :. Dec4-type instance Succ' (x :. Dec4) = x :. Dec5-type instance Succ' (x :. Dec5) = x :. Dec6-type instance Succ' (x :. Dec6) = x :. Dec7-type instance Succ' (x :. Dec7) = x :. Dec8-type instance Succ' (x :. Dec8) = x :. Dec9-type instance Succ' (x :. Dec9) = Succ' x :. Dec0---- type family Pred x-type instance Pred (Dec x)     = Dec (Pred' x)--type family Pred' x-type instance Pred' x = Normalize' (Pred'' x)-type family Pred'' x-type instance Pred'' (Neg' x   ) = Neg' (Succ' x)-type instance Pred'' (DecN     ) = Neg' (DecN :. Dec1)-type instance Pred'' (x :. Dec0) = Pred'' x :. Dec9-type instance Pred'' (x :. Dec1) = x :. Dec0-type instance Pred'' (x :. Dec2) = x :. Dec1-type instance Pred'' (x :. Dec3) = x :. Dec2-type instance Pred'' (x :. Dec4) = x :. Dec3-type instance Pred'' (x :. Dec5) = x :. Dec4-type instance Pred'' (x :. Dec6) = x :. Dec5-type instance Pred'' (x :. Dec7) = x :. Dec6-type instance Pred'' (x :. Dec8) = x :. Dec7-type instance Pred'' (x :. Dec9) = x :. Dec8------------------------- Addition--type family AddDigit x y--- putStr $ unlines $ concat $ [ [ "type instance AddDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x+y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]-type instance AddDigit Dec0 Dec0 = Dec0-type instance AddDigit Dec0 Dec1 = Dec1-type instance AddDigit Dec0 Dec2 = Dec2-type instance AddDigit Dec0 Dec3 = Dec3-type instance AddDigit Dec0 Dec4 = Dec4-type instance AddDigit Dec0 Dec5 = Dec5-type instance AddDigit Dec0 Dec6 = Dec6-type instance AddDigit Dec0 Dec7 = Dec7-type instance AddDigit Dec0 Dec8 = Dec8-type instance AddDigit Dec0 Dec9 = Dec9--type instance AddDigit Dec1 Dec0 = Dec1-type instance AddDigit Dec1 Dec1 = Dec2-type instance AddDigit Dec1 Dec2 = Dec3-type instance AddDigit Dec1 Dec3 = Dec4-type instance AddDigit Dec1 Dec4 = Dec5-type instance AddDigit Dec1 Dec5 = Dec6-type instance AddDigit Dec1 Dec6 = Dec7-type instance AddDigit Dec1 Dec7 = Dec8-type instance AddDigit Dec1 Dec8 = Dec9-type instance AddDigit Dec1 Dec9 = Dec0--type instance AddDigit Dec2 Dec0 = Dec2-type instance AddDigit Dec2 Dec1 = Dec3-type instance AddDigit Dec2 Dec2 = Dec4-type instance AddDigit Dec2 Dec3 = Dec5-type instance AddDigit Dec2 Dec4 = Dec6-type instance AddDigit Dec2 Dec5 = Dec7-type instance AddDigit Dec2 Dec6 = Dec8-type instance AddDigit Dec2 Dec7 = Dec9-type instance AddDigit Dec2 Dec8 = Dec0-type instance AddDigit Dec2 Dec9 = Dec1--type instance AddDigit Dec3 Dec0 = Dec3-type instance AddDigit Dec3 Dec1 = Dec4-type instance AddDigit Dec3 Dec2 = Dec5-type instance AddDigit Dec3 Dec3 = Dec6-type instance AddDigit Dec3 Dec4 = Dec7-type instance AddDigit Dec3 Dec5 = Dec8-type instance AddDigit Dec3 Dec6 = Dec9-type instance AddDigit Dec3 Dec7 = Dec0-type instance AddDigit Dec3 Dec8 = Dec1-type instance AddDigit Dec3 Dec9 = Dec2--type instance AddDigit Dec4 Dec0 = Dec4-type instance AddDigit Dec4 Dec1 = Dec5-type instance AddDigit Dec4 Dec2 = Dec6-type instance AddDigit Dec4 Dec3 = Dec7-type instance AddDigit Dec4 Dec4 = Dec8-type instance AddDigit Dec4 Dec5 = Dec9-type instance AddDigit Dec4 Dec6 = Dec0-type instance AddDigit Dec4 Dec7 = Dec1-type instance AddDigit Dec4 Dec8 = Dec2-type instance AddDigit Dec4 Dec9 = Dec3--type instance AddDigit Dec5 Dec0 = Dec5-type instance AddDigit Dec5 Dec1 = Dec6-type instance AddDigit Dec5 Dec2 = Dec7-type instance AddDigit Dec5 Dec3 = Dec8-type instance AddDigit Dec5 Dec4 = Dec9-type instance AddDigit Dec5 Dec5 = Dec0-type instance AddDigit Dec5 Dec6 = Dec1-type instance AddDigit Dec5 Dec7 = Dec2-type instance AddDigit Dec5 Dec8 = Dec3-type instance AddDigit Dec5 Dec9 = Dec4--type instance AddDigit Dec6 Dec0 = Dec6-type instance AddDigit Dec6 Dec1 = Dec7-type instance AddDigit Dec6 Dec2 = Dec8-type instance AddDigit Dec6 Dec3 = Dec9-type instance AddDigit Dec6 Dec4 = Dec0-type instance AddDigit Dec6 Dec5 = Dec1-type instance AddDigit Dec6 Dec6 = Dec2-type instance AddDigit Dec6 Dec7 = Dec3-type instance AddDigit Dec6 Dec8 = Dec4-type instance AddDigit Dec6 Dec9 = Dec5--type instance AddDigit Dec7 Dec0 = Dec7-type instance AddDigit Dec7 Dec1 = Dec8-type instance AddDigit Dec7 Dec2 = Dec9-type instance AddDigit Dec7 Dec3 = Dec0-type instance AddDigit Dec7 Dec4 = Dec1-type instance AddDigit Dec7 Dec5 = Dec2-type instance AddDigit Dec7 Dec6 = Dec3-type instance AddDigit Dec7 Dec7 = Dec4-type instance AddDigit Dec7 Dec8 = Dec5-type instance AddDigit Dec7 Dec9 = Dec6--type instance AddDigit Dec8 Dec0 = Dec8-type instance AddDigit Dec8 Dec1 = Dec9-type instance AddDigit Dec8 Dec2 = Dec0-type instance AddDigit Dec8 Dec3 = Dec1-type instance AddDigit Dec8 Dec4 = Dec2-type instance AddDigit Dec8 Dec5 = Dec3-type instance AddDigit Dec8 Dec6 = Dec4-type instance AddDigit Dec8 Dec7 = Dec5-type instance AddDigit Dec8 Dec8 = Dec6-type instance AddDigit Dec8 Dec9 = Dec7--type instance AddDigit Dec9 Dec0 = Dec9-type instance AddDigit Dec9 Dec1 = Dec0-type instance AddDigit Dec9 Dec2 = Dec1-type instance AddDigit Dec9 Dec3 = Dec2-type instance AddDigit Dec9 Dec4 = Dec3-type instance AddDigit Dec9 Dec5 = Dec4-type instance AddDigit Dec9 Dec6 = Dec5-type instance AddDigit Dec9 Dec7 = Dec6-type instance AddDigit Dec9 Dec8 = Dec7-type instance AddDigit Dec9 Dec9 = Dec8---- | If adding @x@ and @y@ would not carry, then---   @AddCarry x y z@ evaluates to @z@.  Otherwise,---   @AddCarry x y z@ evaluates to @Succ' z@-type family AddCarry x y z--- putStr $ unlines $ concat $ [ [ "type instance AddCarry Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x + y >= 10 then "Succ'" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]-type instance AddCarry Dec0 Dec0 x = Id x-type instance AddCarry Dec0 Dec1 x = Id x-type instance AddCarry Dec0 Dec2 x = Id x-type instance AddCarry Dec0 Dec3 x = Id x-type instance AddCarry Dec0 Dec4 x = Id x-type instance AddCarry Dec0 Dec5 x = Id x-type instance AddCarry Dec0 Dec6 x = Id x-type instance AddCarry Dec0 Dec7 x = Id x-type instance AddCarry Dec0 Dec8 x = Id x-type instance AddCarry Dec0 Dec9 x = Id x--type instance AddCarry Dec1 Dec0 x = Id x-type instance AddCarry Dec1 Dec1 x = Id x-type instance AddCarry Dec1 Dec2 x = Id x-type instance AddCarry Dec1 Dec3 x = Id x-type instance AddCarry Dec1 Dec4 x = Id x-type instance AddCarry Dec1 Dec5 x = Id x-type instance AddCarry Dec1 Dec6 x = Id x-type instance AddCarry Dec1 Dec7 x = Id x-type instance AddCarry Dec1 Dec8 x = Id x-type instance AddCarry Dec1 Dec9 x = Succ' x--type instance AddCarry Dec2 Dec0 x = Id x-type instance AddCarry Dec2 Dec1 x = Id x-type instance AddCarry Dec2 Dec2 x = Id x-type instance AddCarry Dec2 Dec3 x = Id x-type instance AddCarry Dec2 Dec4 x = Id x-type instance AddCarry Dec2 Dec5 x = Id x-type instance AddCarry Dec2 Dec6 x = Id x-type instance AddCarry Dec2 Dec7 x = Id x-type instance AddCarry Dec2 Dec8 x = Succ' x-type instance AddCarry Dec2 Dec9 x = Succ' x--type instance AddCarry Dec3 Dec0 x = Id x-type instance AddCarry Dec3 Dec1 x = Id x-type instance AddCarry Dec3 Dec2 x = Id x-type instance AddCarry Dec3 Dec3 x = Id x-type instance AddCarry Dec3 Dec4 x = Id x-type instance AddCarry Dec3 Dec5 x = Id x-type instance AddCarry Dec3 Dec6 x = Id x-type instance AddCarry Dec3 Dec7 x = Succ' x-type instance AddCarry Dec3 Dec8 x = Succ' x-type instance AddCarry Dec3 Dec9 x = Succ' x--type instance AddCarry Dec4 Dec0 x = Id x-type instance AddCarry Dec4 Dec1 x = Id x-type instance AddCarry Dec4 Dec2 x = Id x-type instance AddCarry Dec4 Dec3 x = Id x-type instance AddCarry Dec4 Dec4 x = Id x-type instance AddCarry Dec4 Dec5 x = Id x-type instance AddCarry Dec4 Dec6 x = Succ' x-type instance AddCarry Dec4 Dec7 x = Succ' x-type instance AddCarry Dec4 Dec8 x = Succ' x-type instance AddCarry Dec4 Dec9 x = Succ' x--type instance AddCarry Dec5 Dec0 x = Id x-type instance AddCarry Dec5 Dec1 x = Id x-type instance AddCarry Dec5 Dec2 x = Id x-type instance AddCarry Dec5 Dec3 x = Id x-type instance AddCarry Dec5 Dec4 x = Id x-type instance AddCarry Dec5 Dec5 x = Succ' x-type instance AddCarry Dec5 Dec6 x = Succ' x-type instance AddCarry Dec5 Dec7 x = Succ' x-type instance AddCarry Dec5 Dec8 x = Succ' x-type instance AddCarry Dec5 Dec9 x = Succ' x--type instance AddCarry Dec6 Dec0 x = Id x-type instance AddCarry Dec6 Dec1 x = Id x-type instance AddCarry Dec6 Dec2 x = Id x-type instance AddCarry Dec6 Dec3 x = Id x-type instance AddCarry Dec6 Dec4 x = Succ' x-type instance AddCarry Dec6 Dec5 x = Succ' x-type instance AddCarry Dec6 Dec6 x = Succ' x-type instance AddCarry Dec6 Dec7 x = Succ' x-type instance AddCarry Dec6 Dec8 x = Succ' x-type instance AddCarry Dec6 Dec9 x = Succ' x--type instance AddCarry Dec7 Dec0 x = Id x-type instance AddCarry Dec7 Dec1 x = Id x-type instance AddCarry Dec7 Dec2 x = Id x-type instance AddCarry Dec7 Dec3 x = Succ' x-type instance AddCarry Dec7 Dec4 x = Succ' x-type instance AddCarry Dec7 Dec5 x = Succ' x-type instance AddCarry Dec7 Dec6 x = Succ' x-type instance AddCarry Dec7 Dec7 x = Succ' x-type instance AddCarry Dec7 Dec8 x = Succ' x-type instance AddCarry Dec7 Dec9 x = Succ' x--type instance AddCarry Dec8 Dec0 x = Id x-type instance AddCarry Dec8 Dec1 x = Id x-type instance AddCarry Dec8 Dec2 x = Succ' x-type instance AddCarry Dec8 Dec3 x = Succ' x-type instance AddCarry Dec8 Dec4 x = Succ' x-type instance AddCarry Dec8 Dec5 x = Succ' x-type instance AddCarry Dec8 Dec6 x = Succ' x-type instance AddCarry Dec8 Dec7 x = Succ' x-type instance AddCarry Dec8 Dec8 x = Succ' x-type instance AddCarry Dec8 Dec9 x = Succ' x--type instance AddCarry Dec9 Dec0 x = Id x-type instance AddCarry Dec9 Dec1 x = Succ' x-type instance AddCarry Dec9 Dec2 x = Succ' x-type instance AddCarry Dec9 Dec3 x = Succ' x-type instance AddCarry Dec9 Dec4 x = Succ' x-type instance AddCarry Dec9 Dec5 x = Succ' x-type instance AddCarry Dec9 Dec6 x = Succ' x-type instance AddCarry Dec9 Dec7 x = Succ' x-type instance AddCarry Dec9 Dec8 x = Succ' x-type instance AddCarry Dec9 Dec9 x = Succ' x---- type family x :+: y-type instance Dec x :+: Dec y = Dec (Add x y)--type family Add x y-type instance Add (DecN    ) (DecN    ) = DecN-type instance Add (xh :. xl) (DecN    ) = (xh :. xl)-type instance Add (DecN    ) (yh :. yl) = (yh :. yl)-type instance Add (Neg' x  ) (Neg' y  ) = Neg' (Add x y)-type instance Add (xh :. xl) (Neg' y  ) = Sub (xh :. xl) y-type instance Add (Neg' x  ) (yh :. yl) = Sub (yh :. yl) x-type instance Add (xh :. xl) (yh :. yl) = (AddCarry xl yl (Add xh yh)) :. (AddDigit xl yl)------------------------- Subtraction--type family SubDigit x y--- putStr $ unlines $ concat $ [ [ "type instance SubDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x-y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]-type instance SubDigit Dec0 Dec0 = Dec0-type instance SubDigit Dec0 Dec1 = Dec9-type instance SubDigit Dec0 Dec2 = Dec8-type instance SubDigit Dec0 Dec3 = Dec7-type instance SubDigit Dec0 Dec4 = Dec6-type instance SubDigit Dec0 Dec5 = Dec5-type instance SubDigit Dec0 Dec6 = Dec4-type instance SubDigit Dec0 Dec7 = Dec3-type instance SubDigit Dec0 Dec8 = Dec2-type instance SubDigit Dec0 Dec9 = Dec1--type instance SubDigit Dec1 Dec0 = Dec1-type instance SubDigit Dec1 Dec1 = Dec0-type instance SubDigit Dec1 Dec2 = Dec9-type instance SubDigit Dec1 Dec3 = Dec8-type instance SubDigit Dec1 Dec4 = Dec7-type instance SubDigit Dec1 Dec5 = Dec6-type instance SubDigit Dec1 Dec6 = Dec5-type instance SubDigit Dec1 Dec7 = Dec4-type instance SubDigit Dec1 Dec8 = Dec3-type instance SubDigit Dec1 Dec9 = Dec2--type instance SubDigit Dec2 Dec0 = Dec2-type instance SubDigit Dec2 Dec1 = Dec1-type instance SubDigit Dec2 Dec2 = Dec0-type instance SubDigit Dec2 Dec3 = Dec9-type instance SubDigit Dec2 Dec4 = Dec8-type instance SubDigit Dec2 Dec5 = Dec7-type instance SubDigit Dec2 Dec6 = Dec6-type instance SubDigit Dec2 Dec7 = Dec5-type instance SubDigit Dec2 Dec8 = Dec4-type instance SubDigit Dec2 Dec9 = Dec3--type instance SubDigit Dec3 Dec0 = Dec3-type instance SubDigit Dec3 Dec1 = Dec2-type instance SubDigit Dec3 Dec2 = Dec1-type instance SubDigit Dec3 Dec3 = Dec0-type instance SubDigit Dec3 Dec4 = Dec9-type instance SubDigit Dec3 Dec5 = Dec8-type instance SubDigit Dec3 Dec6 = Dec7-type instance SubDigit Dec3 Dec7 = Dec6-type instance SubDigit Dec3 Dec8 = Dec5-type instance SubDigit Dec3 Dec9 = Dec4--type instance SubDigit Dec4 Dec0 = Dec4-type instance SubDigit Dec4 Dec1 = Dec3-type instance SubDigit Dec4 Dec2 = Dec2-type instance SubDigit Dec4 Dec3 = Dec1-type instance SubDigit Dec4 Dec4 = Dec0-type instance SubDigit Dec4 Dec5 = Dec9-type instance SubDigit Dec4 Dec6 = Dec8-type instance SubDigit Dec4 Dec7 = Dec7-type instance SubDigit Dec4 Dec8 = Dec6-type instance SubDigit Dec4 Dec9 = Dec5--type instance SubDigit Dec5 Dec0 = Dec5-type instance SubDigit Dec5 Dec1 = Dec4-type instance SubDigit Dec5 Dec2 = Dec3-type instance SubDigit Dec5 Dec3 = Dec2-type instance SubDigit Dec5 Dec4 = Dec1-type instance SubDigit Dec5 Dec5 = Dec0-type instance SubDigit Dec5 Dec6 = Dec9-type instance SubDigit Dec5 Dec7 = Dec8-type instance SubDigit Dec5 Dec8 = Dec7-type instance SubDigit Dec5 Dec9 = Dec6--type instance SubDigit Dec6 Dec0 = Dec6-type instance SubDigit Dec6 Dec1 = Dec5-type instance SubDigit Dec6 Dec2 = Dec4-type instance SubDigit Dec6 Dec3 = Dec3-type instance SubDigit Dec6 Dec4 = Dec2-type instance SubDigit Dec6 Dec5 = Dec1-type instance SubDigit Dec6 Dec6 = Dec0-type instance SubDigit Dec6 Dec7 = Dec9-type instance SubDigit Dec6 Dec8 = Dec8-type instance SubDigit Dec6 Dec9 = Dec7--type instance SubDigit Dec7 Dec0 = Dec7-type instance SubDigit Dec7 Dec1 = Dec6-type instance SubDigit Dec7 Dec2 = Dec5-type instance SubDigit Dec7 Dec3 = Dec4-type instance SubDigit Dec7 Dec4 = Dec3-type instance SubDigit Dec7 Dec5 = Dec2-type instance SubDigit Dec7 Dec6 = Dec1-type instance SubDigit Dec7 Dec7 = Dec0-type instance SubDigit Dec7 Dec8 = Dec9-type instance SubDigit Dec7 Dec9 = Dec8--type instance SubDigit Dec8 Dec0 = Dec8-type instance SubDigit Dec8 Dec1 = Dec7-type instance SubDigit Dec8 Dec2 = Dec6-type instance SubDigit Dec8 Dec3 = Dec5-type instance SubDigit Dec8 Dec4 = Dec4-type instance SubDigit Dec8 Dec5 = Dec3-type instance SubDigit Dec8 Dec6 = Dec2-type instance SubDigit Dec8 Dec7 = Dec1-type instance SubDigit Dec8 Dec8 = Dec0-type instance SubDigit Dec8 Dec9 = Dec9--type instance SubDigit Dec9 Dec0 = Dec9-type instance SubDigit Dec9 Dec1 = Dec8-type instance SubDigit Dec9 Dec2 = Dec7-type instance SubDigit Dec9 Dec3 = Dec6-type instance SubDigit Dec9 Dec4 = Dec5-type instance SubDigit Dec9 Dec5 = Dec4-type instance SubDigit Dec9 Dec6 = Dec3-type instance SubDigit Dec9 Dec7 = Dec2-type instance SubDigit Dec9 Dec8 = Dec1-type instance SubDigit Dec9 Dec9 = Dec0---- | If subtracting @y@ from @x@ would not borrow, then---   @Borrow x y z@ evaluates to @z@.  Otherwise,---   @Borrow x y z@ evaluates to @Pred' z@-type family Borrow x y z--- putStr $ unlines $ concat $ [ [ "type instance Borrow Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x < y then "Pred'" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]-type instance Borrow Dec0 Dec0 x = Id x-type instance Borrow Dec0 Dec1 x = Pred' x-type instance Borrow Dec0 Dec2 x = Pred' x-type instance Borrow Dec0 Dec3 x = Pred' x-type instance Borrow Dec0 Dec4 x = Pred' x-type instance Borrow Dec0 Dec5 x = Pred' x-type instance Borrow Dec0 Dec6 x = Pred' x-type instance Borrow Dec0 Dec7 x = Pred' x-type instance Borrow Dec0 Dec8 x = Pred' x-type instance Borrow Dec0 Dec9 x = Pred' x--type instance Borrow Dec1 Dec0 x = Id x-type instance Borrow Dec1 Dec1 x = Id x-type instance Borrow Dec1 Dec2 x = Pred' x-type instance Borrow Dec1 Dec3 x = Pred' x-type instance Borrow Dec1 Dec4 x = Pred' x-type instance Borrow Dec1 Dec5 x = Pred' x-type instance Borrow Dec1 Dec6 x = Pred' x-type instance Borrow Dec1 Dec7 x = Pred' x-type instance Borrow Dec1 Dec8 x = Pred' x-type instance Borrow Dec1 Dec9 x = Pred' x--type instance Borrow Dec2 Dec0 x = Id x-type instance Borrow Dec2 Dec1 x = Id x-type instance Borrow Dec2 Dec2 x = Id x-type instance Borrow Dec2 Dec3 x = Pred' x-type instance Borrow Dec2 Dec4 x = Pred' x-type instance Borrow Dec2 Dec5 x = Pred' x-type instance Borrow Dec2 Dec6 x = Pred' x-type instance Borrow Dec2 Dec7 x = Pred' x-type instance Borrow Dec2 Dec8 x = Pred' x-type instance Borrow Dec2 Dec9 x = Pred' x--type instance Borrow Dec3 Dec0 x = Id x-type instance Borrow Dec3 Dec1 x = Id x-type instance Borrow Dec3 Dec2 x = Id x-type instance Borrow Dec3 Dec3 x = Id x-type instance Borrow Dec3 Dec4 x = Pred' x-type instance Borrow Dec3 Dec5 x = Pred' x-type instance Borrow Dec3 Dec6 x = Pred' x-type instance Borrow Dec3 Dec7 x = Pred' x-type instance Borrow Dec3 Dec8 x = Pred' x-type instance Borrow Dec3 Dec9 x = Pred' x--type instance Borrow Dec4 Dec0 x = Id x-type instance Borrow Dec4 Dec1 x = Id x-type instance Borrow Dec4 Dec2 x = Id x-type instance Borrow Dec4 Dec3 x = Id x-type instance Borrow Dec4 Dec4 x = Id x-type instance Borrow Dec4 Dec5 x = Pred' x-type instance Borrow Dec4 Dec6 x = Pred' x-type instance Borrow Dec4 Dec7 x = Pred' x-type instance Borrow Dec4 Dec8 x = Pred' x-type instance Borrow Dec4 Dec9 x = Pred' x--type instance Borrow Dec5 Dec0 x = Id x-type instance Borrow Dec5 Dec1 x = Id x-type instance Borrow Dec5 Dec2 x = Id x-type instance Borrow Dec5 Dec3 x = Id x-type instance Borrow Dec5 Dec4 x = Id x-type instance Borrow Dec5 Dec5 x = Id x-type instance Borrow Dec5 Dec6 x = Pred' x-type instance Borrow Dec5 Dec7 x = Pred' x-type instance Borrow Dec5 Dec8 x = Pred' x-type instance Borrow Dec5 Dec9 x = Pred' x--type instance Borrow Dec6 Dec0 x = Id x-type instance Borrow Dec6 Dec1 x = Id x-type instance Borrow Dec6 Dec2 x = Id x-type instance Borrow Dec6 Dec3 x = Id x-type instance Borrow Dec6 Dec4 x = Id x-type instance Borrow Dec6 Dec5 x = Id x-type instance Borrow Dec6 Dec6 x = Id x-type instance Borrow Dec6 Dec7 x = Pred' x-type instance Borrow Dec6 Dec8 x = Pred' x-type instance Borrow Dec6 Dec9 x = Pred' x--type instance Borrow Dec7 Dec0 x = Id x-type instance Borrow Dec7 Dec1 x = Id x-type instance Borrow Dec7 Dec2 x = Id x-type instance Borrow Dec7 Dec3 x = Id x-type instance Borrow Dec7 Dec4 x = Id x-type instance Borrow Dec7 Dec5 x = Id x-type instance Borrow Dec7 Dec6 x = Id x-type instance Borrow Dec7 Dec7 x = Id x-type instance Borrow Dec7 Dec8 x = Pred' x-type instance Borrow Dec7 Dec9 x = Pred' x--type instance Borrow Dec8 Dec0 x = Id x-type instance Borrow Dec8 Dec1 x = Id x-type instance Borrow Dec8 Dec2 x = Id x-type instance Borrow Dec8 Dec3 x = Id x-type instance Borrow Dec8 Dec4 x = Id x-type instance Borrow Dec8 Dec5 x = Id x-type instance Borrow Dec8 Dec6 x = Id x-type instance Borrow Dec8 Dec7 x = Id x-type instance Borrow Dec8 Dec8 x = Id x-type instance Borrow Dec8 Dec9 x = Pred' x--type instance Borrow Dec9 Dec0 x = Id x-type instance Borrow Dec9 Dec1 x = Id x-type instance Borrow Dec9 Dec2 x = Id x-type instance Borrow Dec9 Dec3 x = Id x-type instance Borrow Dec9 Dec4 x = Id x-type instance Borrow Dec9 Dec5 x = Id x-type instance Borrow Dec9 Dec6 x = Id x-type instance Borrow Dec9 Dec7 x = Id x-type instance Borrow Dec9 Dec8 x = Id x-type instance Borrow Dec9 Dec9 x = Id x---- type family x :-: y-type instance Dec x :-: Dec y = Dec (Sub x y)--type family Sub x y-type instance Sub x y = Normalize' (Sub' x y)--type family Sub' x y-type instance Sub' (Neg' x  ) (Neg' y  ) = Sub' y x-type instance Sub' (Neg' x  ) (DecN    ) = Neg' x-type instance Sub' (Neg' x  ) (yh :. yl) = Neg' (Add x (yh :. yl))-type instance Sub' (DecN    ) (Neg' x  ) = x-type instance Sub' (DecN    ) (DecN    ) = DecN-type instance Sub' (DecN    ) (yh :. yl) = Neg' (yh :. yl)-type instance Sub' (xh :. xl) (Neg' y  ) = Add (xh :. xl) y-type instance Sub' (xh :. xl) (DecN    ) = xh :. xl-type instance Sub' (xh :. xl) (yh :. yl) = Sub'' (xh :. xl) (yh :. yl) (Compare' (xh :. xl) (yh :. yl))--type family Sub'' x y c-type instance Sub'' x y GT = SubPos x y DecN-type instance Sub'' x y EQ = DecN-type instance Sub'' x y LT = Neg' (SubPos y x DecN)--type family SubPos x y z-type instance SubPos (xh :. xl) (yh :. yl) z = SubPos (Borrow xl yl xh) yh (z :. SubDigit xl yl)-type instance SubPos (xh :. xl) DecN       z = SubPos xh DecN (z :. xl)-type instance SubPos DecN       DecN       z = ReverseDigits z------------------------- Multiplication---- type family Mul2 x-type instance Mul2 (Dec x) = Mul2' x-type family Mul2' x-type instance Mul2' x = Add x x---- type family x :*: y-type instance (Dec x) :*: (Dec y) = Dec (Mul x y)---- Peasant style-type family Mul x y-type instance Mul DecN       DecN       = DecN            -- 0 * 0 = 0-type instance Mul (xh :. xl) DecN       = DecN            -- x * 0 = 0-type instance Mul DecN       (yh :. yl) = DecN            -- 0 * x = 0-type instance Mul (Neg' x)   (Neg' y)   = Mul x y        -- -x * -y = x*y-type instance Mul (xh :. xl) (Neg' y)   = Neg' (Mul (xh :. xl) y)  -- x * -y = -(x*y)-type instance Mul (Neg' x)   (yh :. yl) = Neg' (Mul x (yh :. yl))  -- -x * y = -(x*y)-type instance Mul (xh :. xl) (yh :. yl) = Mul' (xh :. xl) (yh :. yl) DecN -- x & y positive--type family Mul' x y z-type instance Mul' x DecN       z = z-type instance Mul' x (yh :. yl) z = Mul' (Mul2' x) (Div2' (yh :. yl)) (If (IsEven' (yh :. yl)) z (Add z x))---- type family Fac x-type instance Fac x = Fac' x (IsZero x)-type family Fac' x is0-type instance Fac' x True = D1-type instance Fac' x False = x :*: Fac (Pred x)---------------- Division / Modulus---- type family IsEven x-type instance IsEven (Dec x) = IsEven' x-type family IsEven' x-type instance IsEven' DecN = True-type instance IsEven' (Neg' x) = IsEven' x-type instance IsEven' (xh :. Dec0) = True-type instance IsEven' (xh :. Dec1) = False-type instance IsEven' (xh :. Dec2) = True-type instance IsEven' (xh :. Dec3) = False-type instance IsEven' (xh :. Dec4) = True-type instance IsEven' (xh :. Dec5) = False-type instance IsEven' (xh :. Dec6) = True-type instance IsEven' (xh :. Dec7) = False-type instance IsEven' (xh :. Dec8) = True-type instance IsEven' (xh :. Dec9) = False---- type family Div2 x-type instance Div2 (Dec x) = Dec (Div2' x)--type family Div2Digit x-type instance Div2Digit Dec0 = Dec0-type instance Div2Digit Dec1 = Dec0-type instance Div2Digit Dec2 = Dec1-type instance Div2Digit Dec3 = Dec1-type instance Div2Digit Dec4 = Dec2-type instance Div2Digit Dec5 = Dec2-type instance Div2Digit Dec6 = Dec3-type instance Div2Digit Dec7 = Dec3-type instance Div2Digit Dec8 = Dec4-type instance Div2Digit Dec9 = Dec4--type family Div2' x-type instance Div2' DecN       = DecN-type instance Div2' (Neg' x)   = Neg' (Div2Pos x)-type instance Div2' (xh :. xl) = Div2Pos (xh :. xl)--type family Div2Pos x-type instance Div2Pos (xh :. xl) = Normalize' (Div2Pos' xh (Div2Digit xl) (If (IsEven' xh) Dec0 Dec5))--type family Div2Pos' xh xl' rem-type instance Div2Pos' xh xl' rem =-    (AddCarry xl' rem (Div2' xh)) :. (AddDigit xl' rem)-------------------- Exponentiation--type instance Pow2 (Dec x) = Dec (Pow2' x (DecN :. Dec1))--type family Pow2' x y-type instance Pow2' (Neg' x)   y = DecN-type instance Pow2' DecN       y = y-type instance Pow2' (xh :. xl) y = Pow2' (Pred' (xh :. xl)) (Mul2' y)-------------------- Logarithm-type instance Log2Ceil (Dec x) = Dec (Log2C' (Pred' x) DecN)--type family Log2C' x y-type instance Log2C' (Neg' x) y   = DecN-type instance Log2C' DecN     y   = y-type instance Log2C' (xh :. xl) y = Log2C' (Div2' (xh :. xl)) (Succ' y)-------------------- Compare--type family CompareDigit x y--- putStr $ unlines $ concat $ [ [ "type instance CompareDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = " ++ (if x < y then "LT" else (if x > y then "GT" else "EQ")) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]-type instance CompareDigit Dec0 Dec0 = EQ-type instance CompareDigit Dec0 Dec1 = LT-type instance CompareDigit Dec0 Dec2 = LT-type instance CompareDigit Dec0 Dec3 = LT-type instance CompareDigit Dec0 Dec4 = LT-type instance CompareDigit Dec0 Dec5 = LT-type instance CompareDigit Dec0 Dec6 = LT-type instance CompareDigit Dec0 Dec7 = LT-type instance CompareDigit Dec0 Dec8 = LT-type instance CompareDigit Dec0 Dec9 = LT--type instance CompareDigit Dec1 Dec0 = GT-type instance CompareDigit Dec1 Dec1 = EQ-type instance CompareDigit Dec1 Dec2 = LT-type instance CompareDigit Dec1 Dec3 = LT-type instance CompareDigit Dec1 Dec4 = LT-type instance CompareDigit Dec1 Dec5 = LT-type instance CompareDigit Dec1 Dec6 = LT-type instance CompareDigit Dec1 Dec7 = LT-type instance CompareDigit Dec1 Dec8 = LT-type instance CompareDigit Dec1 Dec9 = LT--type instance CompareDigit Dec2 Dec0 = GT-type instance CompareDigit Dec2 Dec1 = GT-type instance CompareDigit Dec2 Dec2 = EQ-type instance CompareDigit Dec2 Dec3 = LT-type instance CompareDigit Dec2 Dec4 = LT-type instance CompareDigit Dec2 Dec5 = LT-type instance CompareDigit Dec2 Dec6 = LT-type instance CompareDigit Dec2 Dec7 = LT-type instance CompareDigit Dec2 Dec8 = LT-type instance CompareDigit Dec2 Dec9 = LT--type instance CompareDigit Dec3 Dec0 = GT-type instance CompareDigit Dec3 Dec1 = GT-type instance CompareDigit Dec3 Dec2 = GT-type instance CompareDigit Dec3 Dec3 = EQ-type instance CompareDigit Dec3 Dec4 = LT-type instance CompareDigit Dec3 Dec5 = LT-type instance CompareDigit Dec3 Dec6 = LT-type instance CompareDigit Dec3 Dec7 = LT-type instance CompareDigit Dec3 Dec8 = LT-type instance CompareDigit Dec3 Dec9 = LT--type instance CompareDigit Dec4 Dec0 = GT-type instance CompareDigit Dec4 Dec1 = GT-type instance CompareDigit Dec4 Dec2 = GT-type instance CompareDigit Dec4 Dec3 = GT-type instance CompareDigit Dec4 Dec4 = EQ-type instance CompareDigit Dec4 Dec5 = LT-type instance CompareDigit Dec4 Dec6 = LT-type instance CompareDigit Dec4 Dec7 = LT-type instance CompareDigit Dec4 Dec8 = LT-type instance CompareDigit Dec4 Dec9 = LT--type instance CompareDigit Dec5 Dec0 = GT-type instance CompareDigit Dec5 Dec1 = GT-type instance CompareDigit Dec5 Dec2 = GT-type instance CompareDigit Dec5 Dec3 = GT-type instance CompareDigit Dec5 Dec4 = GT-type instance CompareDigit Dec5 Dec5 = EQ-type instance CompareDigit Dec5 Dec6 = LT-type instance CompareDigit Dec5 Dec7 = LT-type instance CompareDigit Dec5 Dec8 = LT-type instance CompareDigit Dec5 Dec9 = LT--type instance CompareDigit Dec6 Dec0 = GT-type instance CompareDigit Dec6 Dec1 = GT-type instance CompareDigit Dec6 Dec2 = GT-type instance CompareDigit Dec6 Dec3 = GT-type instance CompareDigit Dec6 Dec4 = GT-type instance CompareDigit Dec6 Dec5 = GT-type instance CompareDigit Dec6 Dec6 = EQ-type instance CompareDigit Dec6 Dec7 = LT-type instance CompareDigit Dec6 Dec8 = LT-type instance CompareDigit Dec6 Dec9 = LT--type instance CompareDigit Dec7 Dec0 = GT-type instance CompareDigit Dec7 Dec1 = GT-type instance CompareDigit Dec7 Dec2 = GT-type instance CompareDigit Dec7 Dec3 = GT-type instance CompareDigit Dec7 Dec4 = GT-type instance CompareDigit Dec7 Dec5 = GT-type instance CompareDigit Dec7 Dec6 = GT-type instance CompareDigit Dec7 Dec7 = EQ-type instance CompareDigit Dec7 Dec8 = LT-type instance CompareDigit Dec7 Dec9 = LT--type instance CompareDigit Dec8 Dec0 = GT-type instance CompareDigit Dec8 Dec1 = GT-type instance CompareDigit Dec8 Dec2 = GT-type instance CompareDigit Dec8 Dec3 = GT-type instance CompareDigit Dec8 Dec4 = GT-type instance CompareDigit Dec8 Dec5 = GT-type instance CompareDigit Dec8 Dec6 = GT-type instance CompareDigit Dec8 Dec7 = GT-type instance CompareDigit Dec8 Dec8 = EQ-type instance CompareDigit Dec8 Dec9 = LT--type instance CompareDigit Dec9 Dec0 = GT-type instance CompareDigit Dec9 Dec1 = GT-type instance CompareDigit Dec9 Dec2 = GT-type instance CompareDigit Dec9 Dec3 = GT-type instance CompareDigit Dec9 Dec4 = GT-type instance CompareDigit Dec9 Dec5 = GT-type instance CompareDigit Dec9 Dec6 = GT-type instance CompareDigit Dec9 Dec7 = GT-type instance CompareDigit Dec9 Dec8 = GT-type instance CompareDigit Dec9 Dec9 = EQ--type instance Compare (Dec x) (Dec y) = Compare' x y-type family Compare' x y-type instance Compare' (Neg' x)   (Neg' y)   = CompareNeg (ComparePos x y EQ)-type instance Compare' (Neg' x)   DecN       = LT-type instance Compare' (Neg' x)   (yh :. yl) = LT-type instance Compare' DecN       (Neg' y)   = GT-type instance Compare' DecN       DecN       = EQ-type instance Compare' DecN       (yh :. yl) = LT-type instance Compare' (xh :. xl) (Neg' y)   = GT-type instance Compare' (xh :. xl) DecN       = GT-type instance Compare' (xh :. xl) (yh :. yl) = ComparePos (xh :. xl) (yh :. yl) EQ--type family ComparePos x y c-type instance ComparePos DecN       DecN       c = c-type instance ComparePos DecN       (yh :. yl) c = LT-type instance ComparePos (xh :. xl) DecN       c = GT-type instance ComparePos (xh :. xl) (yh :. yl) GT = ComparePos' xh yh (CompareDigit xl yl) GT-type instance ComparePos (xh :. xl) (yh :. yl) EQ = ComparePos xh yh (CompareDigit xl yl)-type instance ComparePos (xh :. xl) (yh :. yl) LT = ComparePos' xh yh (CompareDigit xl yl) LT--type family ComparePos' x y c l-type instance ComparePos' x y LT c = ComparePos x y LT-type instance ComparePos' x y EQ c = ComparePos x y c-type instance ComparePos' x y GT c = ComparePos x y GT--type family CompareNeg c-type instance CompareNeg LT = GT-type instance CompareNeg EQ = EQ-type instance CompareNeg GT = LT
− Types/Data/Num/Ops.hs 
@@ -1,216 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Types.Data.Decimal.Ops--- Copyright   :  (c) 2008 Peter Gavin--- License     :  BSD-style (see the file LICENSE)--- --- Maintainer  :  pgavin@gmail.com--- Stability   :  experimental--- Portability :  non-portable (type families, requires ghc >= 6.9)------ Type-level numerical operations using type families.--- -------------------------------------------------------------------------------module Types.Data.Num.Ops-    ( (:.)-    , Neg-    , negT-    , IsPositive-    , isPositiveT-    , IsZero-    , isZeroT-    , IsNegative-    , isNegativeT-    , IsNatural-    , isNaturalT-    , Succ-    , succT-    , Pred-    , predT-    , IsEven-    , isEvenT-    , IsOdd-    , isOddT-    , (:+:)-    , addT-    , (:-:)-    , subT-    , (:*:)-    , mulT-    , Mul2-    , mul2T-    , Pow2-    , pow2T-    , Log2Ceil-    , log2CeilT-    , DivMod-    , divModT-    , Div-    , divT-    , Mod-    , modT-    , Div2-    , div2T-    , Fac-    , facT-    , IntegerR (..)-    , IntegerT (..)-    , NaturalT-    , PositiveT-    , NegativeT-    , reifyPositive-    , reifyNegative-    , reifyNatural-    ) where--import Types.Data.Bool--data ds :. d-instance (Show ds, Show d) => Show (ds :. d) where-    show _ = show (undefined :: ds) ++ show (undefined :: d)---- | @Neg x@ evaluates to the additive inverse of (i.e., minus) @x@.-type family Neg x-negT :: x -> Neg x-negT _ = undefined--type family IsPositive x-isPositiveT :: x -> IsPositive x-isPositiveT _ = undefined--type family IsZero x-isZeroT :: x -> IsZero x-isZeroT _ = undefined--type family IsNegative x-isNegativeT :: x -> IsNegative x-isNegativeT _ = undefined--type family IsNatural x-isNaturalT :: x -> IsNatural x-isNaturalT _ = undefined--type family Succ x-succT :: x -> Succ x-succT _ = undefined--type family Pred x-predT :: x -> Pred x-predT _ = undefined--type family IsEven x-isEvenT :: x -> IsEven x-isEvenT _ = undefined--type family IsOdd x-type instance IsOdd x = Not (IsEven x)-isOddT :: x -> IsOdd x-isOddT _ = undefined--type family x :+: y-addT :: x -> y -> x :+: y-addT _ _ = undefined--type family x :-: y-subT :: x -> y -> x :-: y-subT _ _ = undefined--type family x :*: y-mulT :: x -> y -> x :*: y-mulT _ _ = undefined--type family Mul2 x-mul2T :: x -> Mul2 x-mul2T _ = undefined--type family DivMod x y-divModT :: x -> y -> DivMod x y-divModT _ _ = undefined--type family Div x y-divT :: x -> y -> Div x y-divT _ _ = undefined--type family Mod x y-modT :: x -> y -> Mod x y-modT _ _ = undefined--type family Div2 x-div2T :: x -> Div2 x-div2T _ = undefined--type family Fac x-facT :: x -> Fac x-facT _ = undefined--type family Pow2 x-pow2T :: x -> Pow2 x-pow2T _ = undefined--type family Log2Ceil x-log2CeilT :: x -> Log2Ceil x-log2CeilT _ = undefined--class IntegerT x => NaturalT x-instance (IntegerT x, IsNatural x  ~ True) => NaturalT x-class IntegerT x => PositiveT x-instance (IntegerT x, IsPositive x ~ True) => PositiveT x-class IntegerT x => NegativeT x-instance (IntegerT x, IsNegative x ~ True) => NegativeT x--class (IntegerR (Repr x)) => IntegerT x where-    fromIntegerT :: Num y => x -> y-    type Repr x--class IntegerR r where-    reifyIntegral :: r -> Integer -> (forall s. (IntegerT s, Repr s ~ r) => s -> a) -> a------ positive and negative assertions: unsafe, in a trusted kernel-data AssertPos x-data AssertNeg x-data AssertNat x--assertPos :: x -> AssertPos x-assertPos _ = undefined--assertNeg :: x -> AssertNeg x-assertNeg _ = undefined--assertNat :: x -> AssertNat x-assertNat _ = undefined--type instance IsPositive (AssertPos x) = True-type instance IsPositive (AssertNeg x) = False--type instance IsNegative (AssertPos x) = False-type instance IsNegative (AssertNeg x) = True-type instance IsNegative (AssertNat x) = False--type instance IsNatural  (AssertPos x) = True-type instance IsNatural  (AssertNeg x) = False-type instance IsNatural  (AssertNat x) = True--instance IntegerT x => IntegerT (AssertPos x) where -    fromIntegerT _ = fromIntegerT (undefined :: x)-    type Repr (AssertPos x) = Repr x--instance IntegerT x => IntegerT (AssertNeg x) where-    fromIntegerT _ = fromIntegerT (undefined :: x)-    type Repr (AssertNeg x) = Repr x--instance IntegerT x => IntegerT (AssertNat x) where-    fromIntegerT _ = fromIntegerT (undefined :: x)-    type Repr (AssertNat x) = Repr x--reifyPositive :: IntegerR r => r -> Integer -> (forall s. (PositiveT s, Repr s ~ r) => s -> a) -> Maybe a-reifyPositive r n k | n > 0     = Just (reifyIntegral r n (k . assertPos))-                    | otherwise = Nothing--reifyNegative :: IntegerR r => r -> Integer -> (forall s. (NegativeT s, Repr s ~ r) => s -> a) -> Maybe a-reifyNegative r n k | n < 0     = Just (reifyIntegral r n (k . assertNeg))-                    | otherwise = Nothing-reifyNatural :: IntegerR r => r -> Integer -> (forall s. (NaturalT s, Repr s ~ r) => s -> a) -> Maybe a-reifyNatural r n k | n >= 0     = Just (reifyIntegral r n (k . assertNat))-                    | otherwise = Nothing
− Types/Data/Ord.hs 
@@ -1,145 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Types.Data.Decimal.Digits--- Copyright   :  (c) 2008 Peter Gavin--- License     :  BSD-style (see the file LICENSE)--- --- Maintainer  :  pgavin@gmail.com--- Stability   :  experimental--- Portability :  non-portable (type families, requires ghc >= 6.9)------ Type-level numerical operations using type families.--- -------------------------------------------------------------------------------module Types.Data.Ord-    ( Compare-    , compareT-    , LT-    , EQ-    , GT-    , IsLT-    , isLTT-    , IsEQ-    , isEQT-    , IsGT-    , isGTT-    , (:<:)-    , ltT-    , LTT-    , (:<=:)-    , leT-    , LET-    , (:==:)-    , eqT-    , EQT-    , (:>=:)-    , geT-    , GET-    , (:>:)-    , gtT-    , GTT-    , Min-    , minT-    , Max-    , maxT-    ) where--import qualified Prelude--import Types.Data.Bool--type family Compare x y-data LT-data EQ-data GT-compareT :: x -> y -> Compare x y-compareT _ _ = Prelude.undefined--type family IsLT c-type instance IsLT LT = True-type instance IsLT EQ = False-type instance IsLT GT = False-isLTT :: c -> IsLT c-isLTT _ = Prelude.undefined--type family IsEQ c-type instance IsEQ LT = False-type instance IsEQ EQ = True-type instance IsEQ GT = False-isEQT :: c -> IsEQ c-isEQT _ = Prelude.undefined--type family IsGT c-type instance IsGT LT = False-type instance IsGT EQ = False-type instance IsGT GT = True-isGTT :: c -> IsGT c-isGTT _ = Prelude.undefined--type instance Compare LT LT = EQ-type instance Compare LT EQ = LT-type instance Compare LT GT = LT-type instance Compare EQ LT = GT-type instance Compare EQ EQ = EQ-type instance Compare EQ GT = LT-type instance Compare GT LT = GT-type instance Compare GT EQ = GT-type instance Compare GT GT = EQ--type family x :<: y-type instance x :<: y = IsLT (Compare x y)-ltT :: x -> y -> x :<: y-ltT _ _ = Prelude.undefined-class LTT x y-instance ((x :<: y) ~ True) => LTT x y--type family x :<=: y-type instance x :<=: y = Not (x :>: y)-leT :: x -> y -> x :<=: y-leT _ _ = Prelude.undefined-class LET x y-instance ((x :<=: y) ~ True) => LET x y--type family x :==: y-type instance x :==: y = IsEQ (Compare x y)-eqT :: x -> y -> x :==: y-eqT _ _ = Prelude.undefined-class EQT x y-instance ((x :==: y) ~ True) => EQT x y--type family x :/=: y-type instance x :/=: y = Not (x :==: y)-neT :: x -> y -> x :/=: y-neT _ _ = Prelude.undefined-class NET x y-instance ((x :/=: y) ~ True) => NET x y--type family x :>=: y-type instance x :>=: y = Not (x :<: y)-geT :: x -> y -> x :>=: y-geT _ _ = Prelude.undefined-class GET x y-instance ((x :>=: y) ~ True) => GET x y--type family x :>: y-type instance x :>: y = IsGT (Compare x y)-gtT :: x -> y -> x :>: y-gtT _ _ = Prelude.undefined-class GTT x y-instance ((x :>: y) ~ True) => GTT x y--type family Min x y-type instance Min x y = If (x :<=: y) x y-minT :: x -> y -> Min x y-minT _ _ = Prelude.undefined--type family Max x y-type instance Max x y = If (x :>=: y) x y-maxT :: x -> y -> Max x y-maxT _ _ = Prelude.undefined--type instance Compare False False = EQ-type instance Compare False True  = LT-type instance Compare True  False = GT-type instance Compare True  True  = EQ
+ src/Data/SizedInt.hs view
@@ -0,0 +1,176 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Data.SizedInt+    ( SizedInt ) where++import Data.Bits+          (Bits, shiftL, shiftR, rotateL, rotateR, bit, testBit, popCount,+           complement, xor, bitSize, isSigned, (.&.), (.|.), )+import Types++newtype SizedInt nT = SizedInt Integer++_sizeT :: SizedInt nT -> nT+_sizeT _ = undefined++mask :: forall nT . NaturalT nT+     => nT+     -> Integer+mask _ = bit (fromIntegerT (undefined :: nT)) - 1++signBit :: forall nT . NaturalT nT+        => nT+        -> Int+signBit _ = fromIntegerT (undefined :: nT) - 1++isNegative :: forall nT . NaturalT nT+           => SizedInt nT+           -> Bool+isNegative (SizedInt x) =+    testBit x $ signBit (undefined :: nT)++instance NaturalT nT => Eq (SizedInt nT) where+    (SizedInt x) == (SizedInt y) = x == y+    (SizedInt x) /= (SizedInt y) = x /= y++instance NaturalT nT => Show (SizedInt nT) where+    showsPrec prec n =+        showsPrec prec $ toInteger n++instance NaturalT nT => Read (SizedInt nT) where+    readsPrec prec str0 =+        [ (fromInteger n, str)+        | (n, str) <- readsPrec prec str0 ]++instance NaturalT nT => Ord (SizedInt nT) where+    a `compare` b = toInteger a `compare` toInteger b++instance NaturalT nT => Bounded (SizedInt nT) where+    minBound = SizedInt $ negate $ 1 `shiftL` (fromIntegerT (undefined :: nT) - 1)+    maxBound = SizedInt $ (1 `shiftL` (fromIntegerT (undefined :: nT) - 1)) - 1++instance NaturalT nT => Enum (SizedInt nT) where+    succ x+       | x == maxBound  = error $ "Enum.succ{" ++ showSizedIntType x ++ "}: tried to take `succ' of maxBound"+       | otherwise      = x + 1+    pred x+       | x == minBound  = error $ "Enum.succ{" ++ showSizedIntType x ++ "}: tried to take `pred' of minBound"+       | otherwise      = x - 1+    +    fromEnum s@(SizedInt x)+        | x > toInteger (maxBound :: Int) =+            error $ "Enum.fromEnum{" ++ showSizedIntType s ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: Int"+        | x < toInteger (minBound :: Int) =+            error $ "Enum.fromEnum{" ++ showSizedIntType s ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: Int"+        | otherwise =+            fromInteger x+    toEnum x+        | x' > toInteger (maxBound :: SizedInt nT) =+            error $ "Enum.fromEnum{" ++ showSizedIntType s ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: " ++ showSizedIntType s+        | x' < toInteger (minBound :: SizedInt nT) =+            error $ "Enum.fromEnum{" ++ showSizedIntType s ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: " ++ showSizedIntType s+        | otherwise =+            fromInteger x'+            where x' = toInteger x+                  s = undefined :: SizedInt nT++instance NaturalT nT => Num (SizedInt nT) where+    (SizedInt a) + (SizedInt b) =+        fromInteger $ a + b+    (SizedInt a) * (SizedInt b) =+        fromInteger $ a * b+    negate (SizedInt n) =+        fromInteger $ (n `xor` mask (undefined :: nT)) + 1+    a - b =+        a + (negate b)++    fromInteger n =+      let fromCardinal m = SizedInt $ m .&. mask (undefined :: nT)+      in  if n>=0+            then fromCardinal n+            else negate $ fromCardinal $ negate n++    abs s+      | isNegative s =+          negate s+      | otherwise =+          s+    signum s+      | isNegative s =+          -1+      | s == 0 =+          0+      | otherwise =+          1++instance NaturalT nT => Real (SizedInt nT) where+    toRational n = toRational $ toInteger n++instance NaturalT nT => Integral (SizedInt nT) where+    a `quot` b =+        fromInteger $ toInteger a `quot` toInteger b+    a `rem` b =+        fromInteger $ toInteger a `rem` toInteger b+    a `div` b =+        fromInteger $ toInteger a `div` toInteger b+    a `mod` b =+        fromInteger $ toInteger a `mod` toInteger b+    a `quotRem` b =+        let (quot_, rem_) = toInteger a `quotRem` toInteger b+        in (fromInteger quot_, fromInteger rem_)+    a `divMod` b =+        let (div_, mod_) = toInteger a `divMod` toInteger b+        in (fromInteger div_, fromInteger mod_)+    toInteger s@(SizedInt x) =+        if isNegative s+           then let SizedInt x' = negate s in negate x'+           else x++instance NaturalT nT => Bits (SizedInt nT) where+    (SizedInt a) .&. (SizedInt b) = SizedInt $ a .&. b+    (SizedInt a) .|. (SizedInt b) = SizedInt $ a .|. b+    (SizedInt a) `xor` SizedInt b = SizedInt $ a `xor` b+    complement (SizedInt x) = SizedInt $ x `xor` mask (undefined :: nT)+    bit b =+      case SizedInt $ bit b of+        s | b < 0 -> error $ "Bits.bit{" ++ showSizedIntType s ++ "}: tried to set negative position"+          | b >= bitSize s -> error $ "Bits.bit{" ++ showSizedIntType s ++ "}: tried to set too large position"+          | otherwise -> s+    s@(SizedInt x) `testBit` b+      | b < 0 = error $ "Bits.testBit{" ++ showSizedIntType s ++ "}: tried to test negative position"+      | b >= bitSize s = error $ "Bits.testBit{" ++ showSizedIntType s ++ "}: tried to test too large position"+      | otherwise =+         testBit x b+    s@(SizedInt x) `shiftL` b+      | b < 0 = error $ "Bits.shiftL{" ++ showSizedIntType s ++ "}: tried to shift by negative amount"+      | otherwise =+        SizedInt $ mask (undefined :: nT) .&. (x `shiftL` b)+    s@(SizedInt x) `shiftR` b+      | b < 0 = error $ "Bits.shiftR{" ++ showSizedIntType s ++ "}: tried to shift by negative amount"+      | isNegative s =+        SizedInt $ mask (undefined :: nT) .&.+            ((x `shiftR` b) .|. (mask (undefined :: nT) `shiftL` (fromIntegerT (undefined :: nT) - b)))+      | otherwise =+        SizedInt $ (mask (undefined :: nT)) .&. (x `shiftR` b)+    s@(SizedInt a) `rotateL` b+      | b < 0 =+        error $ "Bits.rotateL{" ++ showSizedIntType s ++ "}: tried to rotate by negative amount"+      | otherwise =+        SizedInt $ mask (undefined :: nT) .&.+            ((a `shiftL` b) .|. (a `shiftR` (fromIntegerT (undefined :: nT) - b)))+    s@(SizedInt a) `rotateR` b+      | b < 0 =+        error $ "Bits.rotateR{" ++ showSizedIntType s ++ "}: tried to rotate by negative amount"+      | otherwise =+        SizedInt $ mask (undefined :: nT) .&.+            ((a `shiftR` b) .|. (a `shiftL` (fromIntegerT (undefined :: nT) - b)))+    popCount (SizedInt x) = popCount x+    bitSize _ = fromIntegerT (undefined :: nT)+    isSigned _ = True+++showSizedIntType :: forall nT. NaturalT nT => SizedInt nT -> String+showSizedIntType _ =+   "SizedInt " ++ show (fromIntegerT (undefined :: nT) :: Integer)
+ src/Data/SizedWord.hs view
@@ -0,0 +1,152 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Data.SizedWord+    ( SizedWord ) where++import Data.Bits+          (Bits, shiftL, shiftR, rotateL, rotateR, bit, testBit, popCount,+           complement, xor, bitSize, isSigned, (.&.), (.|.), )+import Types++newtype SizedWord nT = SizedWord Integer++sizeT :: SizedWord nT+      -> nT+sizeT _ = undefined++mask :: forall nT . NaturalT nT+     => nT+     -> Integer+mask _ = bit (fromIntegerT (undefined :: nT)) - 1++instance NaturalT nT => Eq (SizedWord nT) where+    (SizedWord x) == (SizedWord y) = x == y+    (SizedWord x) /= (SizedWord y) = x /= y++instance NaturalT nT => Show (SizedWord nT) where+    showsPrec prec n =+        showsPrec prec $ toInteger n++instance NaturalT nT => Read (SizedWord nT) where+    readsPrec prec str0 =+        [ (fromInteger n, str)+        | (n, str) <- readsPrec prec str0 ]++instance NaturalT nT => Ord (SizedWord nT) where+    a `compare` b = toInteger a `compare` toInteger b++instance NaturalT nT => Bounded (SizedWord nT) where+    minBound = 0+    maxBound = SizedWord $ (1 `shiftL` (fromIntegerT (undefined :: nT))) - 1++instance NaturalT nT => Enum (SizedWord nT) where+    succ x+       | x == maxBound  = error $ "Enum.succ{" ++ showSizedWordType x ++ "}: tried to take `succ' of maxBound"+       | otherwise      = x + 1+    pred x+       | x == minBound  = error $ "Enum.succ{" ++ showSizedWordType x ++ "}: tried to take `pred' of minBound"+       | otherwise      = x - 1+    +    fromEnum s@(SizedWord x)+        | x > toInteger (maxBound :: Int) =+            error $ "Enum.fromEnum{" ++ showSizedWordType s ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: Int"+        | x < toInteger (minBound :: Int) =+            error $ "Enum.fromEnum{" ++ showSizedWordType s ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: Int"+        | otherwise =+            fromInteger x+    toEnum x+        | x > fromIntegral (maxBound :: SizedWord nT) =+            error $ "Enum.fromEnum{" ++ showSizedWordType s ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: " ++ showSizedWordType s+        | x < fromIntegral (minBound :: SizedWord nT) =+            error $ "Enum.fromEnum{" ++ showSizedWordType s ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: " ++ showSizedWordType s+        | otherwise =+            fromInteger $ toInteger x+            where s = undefined :: SizedWord nT++instance NaturalT nT => Num (SizedWord nT) where+    (SizedWord a) + (SizedWord b) =+        fromInteger $ a + b+    (SizedWord a) * (SizedWord b) =+        fromInteger $ a * b+    negate s@(SizedWord n) =+        fromInteger $ (n `xor` mask (sizeT s)) + 1+    a - b =+        a + (negate b)++    fromInteger n =+      let fromCardinal m = SizedWord $ m .&. mask (undefined :: nT)+      in  if n>=0+            then fromCardinal n+            else negate $ fromCardinal $ negate n++    abs s = s+    signum s+      | s == 0 =+          0+      | otherwise =+          1++instance NaturalT nT => Real (SizedWord nT) where+    toRational n = toRational $ toInteger n++instance NaturalT nT => Integral (SizedWord nT) where+    a `quot` b =+        fromInteger $ toInteger a `quot` toInteger b+    a `rem` b =+        fromInteger $ toInteger a `rem` toInteger b+    a `div` b =+        fromInteger $ toInteger a `div` toInteger b+    a `mod` b =+        fromInteger $ toInteger a `mod` toInteger b+    a `quotRem` b =+        let (quot_, rem_) = toInteger a `quotRem` toInteger b+        in (fromInteger quot_, fromInteger rem_)+    a `divMod` b =+        let (div_, mod_) = toInteger a `divMod` toInteger b+        in (fromInteger div_, fromInteger mod_)+    toInteger (SizedWord x) = x++instance NaturalT nT => Bits (SizedWord nT) where+    (SizedWord a) .&. (SizedWord b) = SizedWord $ a .&. b+    (SizedWord a) .|. (SizedWord b) = SizedWord $ a .|. b+    (SizedWord a) `xor` SizedWord b = SizedWord $ a `xor` b+    complement (SizedWord x) = SizedWord $ x `xor` mask (undefined :: nT)+    bit b =+      case SizedWord $ bit b of+        s | b < 0 -> error $ "Bits.bit{" ++ showSizedWordType s ++ "}: tried to set negative position"+          | b >= bitSize s -> error $ "Bits.bit{" ++ showSizedWordType s ++ "}: tried to set too large position"+          | otherwise -> s+    s@(SizedWord x) `testBit` b+      | b < 0 = error $ "Bits.testBit{" ++ showSizedWordType s ++ "}: tried to test negative position"+      | b >= bitSize s = error $ "Bits.testBit{" ++ showSizedWordType s ++ "}: tried to test too large position"+      | otherwise =+         testBit x b+    s@(SizedWord x) `shiftL` b+      | b < 0 = error $ "Bits.shiftL{" ++ showSizedWordType s ++ "}: tried to shift by negative amount"+      | otherwise =+        SizedWord $ mask (undefined :: nT) .&. (x `shiftL` b)+    s@(SizedWord x) `shiftR` b+      | b < 0 = error $ "Bits.shiftR{" ++ showSizedWordType s ++ "}: tried to shift by negative amount"+      | otherwise =+        SizedWord $ (x `shiftR` b)+    s@(SizedWord x) `rotateL` b+      | b < 0 =+        error $ "Bits.rotateL{" ++ showSizedWordType s ++ "}: tried to rotate by negative amount"+      | otherwise =+        SizedWord $ mask (undefined :: nT) .&.+            ((x `shiftL` b) .|. (x `shiftR` (bitSize s - b)))+    s@(SizedWord x) `rotateR` b+      | b < 0 =+        error $ "Bits.rotateR{" ++ showSizedWordType s ++ "}: tried to rotate by negative amount"+      | otherwise =+        SizedWord $ mask (undefined :: nT) .&.+            ((x `shiftR` b) .|. (x `shiftL` (bitSize s - b)))+    popCount (SizedWord x) = popCount x+    bitSize _ = fromIntegerT (undefined :: nT)+    isSigned _ = False++showSizedWordType :: forall nT. NaturalT nT => SizedWord nT -> String+showSizedWordType _ =+   "SizedWord " ++ show (fromIntegerT (undefined :: nT) :: Integer)
+ src/Types.hs view
@@ -0,0 +1,13 @@+module Types+    ( module Types.Base+    , module Types.Data.Bool+    , module Types.Data.Num+    , module Types.Data.List+    , module Types.Data.Ord+    ) where++import Types.Base+import Types.Data.Bool+import Types.Data.Num+import Types.Data.List+import Types.Data.Ord
+ src/Types/Base.hs view
@@ -0,0 +1,26 @@+{-# LANGUAGE TypeFamilies #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Types.Data.Decimal.Ops+-- Copyright   :  (c) 2008 Peter Gavin+-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  pgavin@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (type families, requires ghc >= 6.9)+--+-- Type-level numerical operations using type families.+-- +----------------------------------------------------------------------------++module Types.Base+    where++import qualified Prelude++type family Id x+type instance Id x = x++_T :: a+_T = Prelude.undefined
+ src/Types/Data/Bool.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DeriveDataTypeable #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Types.Data.Bool+-- Copyright   :  (c) 2008 Peter Gavin+-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  pgavin@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (type families, requires ghc >= 6.9)+--+-- Type-level numerical operations using type families.+-- +----------------------------------------------------------------------------++module Types.Data.Bool+    ( True+    , trueT+    , False+    , falseT+    , Not+    , notT+    , (:&&:)+    , andT+    , (:||:)+    , orT+    , IfT(..)+    ) where++import Data.Typeable++import qualified Prelude++data True deriving (Typeable)+trueT :: True+trueT = Prelude.undefined+instance Prelude.Show True where+    show _ = "True"+data False deriving (Typeable)+falseT :: False+falseT = Prelude.undefined+instance Prelude.Show False where+    show _ = "False"++type family Not x+type instance Not False = True+type instance Not True  = False+notT :: x -> Not x+notT _ = Prelude.undefined++type family x :&&: y+type instance False :&&: x = False+type instance True  :&&: x = x+andT :: x -> y -> x :&&: y+andT _ _ = Prelude.undefined++type family x :||: y+type instance True  :||: x = True+type instance False :||: x = x+orT :: x -> y -> x :||: y+orT _ _ = Prelude.undefined++class IfT x y z where+    type If x y z+    ifT :: x -> y -> z -> If x y z+instance IfT True y z where+    type If True y z = y+    ifT _ y _ = y+instance IfT False y z where+    type If False y z = z+    ifT _ _ z = z
+ src/Types/Data/List.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DeriveDataTypeable #-}+module Types.Data.List+    ( Cons+    , Null+    , IsNull+    , Head+    , Tail+    , Reverse+    , Append+    ) where++import qualified Prelude++import Data.Typeable++import Types.Data.Bool++data Cons car cdr deriving (Typeable)+instance (Prelude.Show car, Prelude.Show cdr) => Prelude.Show (Cons car cdr) where+    show = showCons++showCons :: forall car cdr . (Prelude.Show car, Prelude.Show cdr) => Cons car cdr -> Prelude.String+showCons _ = "Cons (" Prelude.++ Prelude.show (Prelude.undefined :: car) Prelude.++ ") (" Prelude.++ Prelude.show (Prelude.undefined :: cdr) Prelude.++ ")"++data Null deriving (Typeable)+instance Prelude.Show Null where+    show _ = ""++type family IsNull l+type instance IsNull (Cons car cdr) = False+type instance IsNull Null = True++type family Head l+type instance Head (Cons car cdr) = car++type family Tail l+type instance Tail (Cons car cdr) = cdr++type family Reverse l+type instance Reverse l = Reverse' l Null++type family Reverse' l a+type instance Reverse' Null a = a+type instance Reverse' (Cons car cdr) a = Reverse' cdr (Cons car a)++type family Append l1 l2+type instance Append Null l2 = l2+type instance Append (Cons car1 cdr2) l2 = Cons car1 (Append cdr2 l2)
+ src/Types/Data/Num.hs view
@@ -0,0 +1,58 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE CPP #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Types.Data.Num+-- Copyright   :  (c) 2008 Peter Gavin+-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  pgavin@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (type families, requires ghc >= 6.9)+--+-- Type-level numerical operations using type families.+-- +----------------------------------------------------------------------------++module Types.Data.Num+    ( module Types.Data.Num.Ops+    , module Types.Data.Num.Decimal+#if __GLASGOW_HASKELL__ >= 704 || __GLASGOW_HASKELL__ < 700+    , reifyIntegralD+    , reifyPositiveD+    , reifyNegativeD+    , reifyNaturalD+#endif+    ) where++import Types.Data.Num.Ops+import Types.Data.Num.Decimal++-- An explanation of the following is in order:++-- Versions of GHC prior to 7.0 (e.g., 6.12.3) will compile this code+-- as long as the type signature isn't there.+-- Versions 7.0 and later, but before 7.4 will not compile it at all,+-- with or without the type signature.+-- Version 7.4 and later handles everything just fine.++#if __GLASGOW_HASKELL__ >= 704 || __GLASGOW_HASKELL__ < 700+#if __GLASGOW_HASKELL__ >= 704+reifyIntegralD :: Integer -> (forall s. (IntegerT s, Repr s ~ Decimal) => s -> a) -> a+#endif+reifyIntegralD = reifyIntegral decimal+#if __GLASGOW_HASKELL__ >= 704+reifyPositiveD :: Integer -> (forall s. (PositiveT s, Repr s ~ Decimal) => s -> a) -> Maybe a+#endif+reifyPositiveD = reifyPositive decimal+#if __GLASGOW_HASKELL__ >= 704+reifyNegativeD :: Integer -> (forall s. (NegativeT s, Repr s ~ Decimal) => s -> a) -> Maybe a+#endif+reifyNegativeD = reifyNegative decimal+#if __GLASGOW_HASKELL__ >= 704+reifyNaturalD :: Integer -> (forall s. (NaturalT s, Repr s ~ Decimal) => s -> a) -> Maybe a+#endif+reifyNaturalD = reifyNatural decimal+#endif
+ src/Types/Data/Num/Decimal.hs view
@@ -0,0 +1,8 @@+module Types.Data.Num.Decimal+    ( module Types.Data.Num.Decimal.Digits+    , module Types.Data.Num.Decimal.Literals+    ) where++import Types.Data.Num.Decimal.Digits+import Types.Data.Num.Decimal.Literals+import Types.Data.Num.Decimal.Ops ()
+ src/Types/Data/Num/Decimal/Digits.hs view
@@ -0,0 +1,65 @@+{-# LANGUAGE DeriveDataTypeable #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Types.Data.Num.Decimal.Digits+-- Copyright   :  (c) 2008 Peter Gavin+-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  pgavin@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (type families, requires ghc >= 6.9)+--+-- Type-level numerical operations using type families.+-- +----------------------------------------------------------------------------++module Types.Data.Num.Decimal.Digits+    where++import Data.Typeable++-- | Representation name for decimal type level numbers.+data Decimal+decimal :: Decimal+decimal = undefined++-- | The wrapper type for decimal type level numbers.+data Dec x+data Neg' x++-- | The terminator type for decimal digit lists.+data DecN+instance Show DecN where+    show _ = ""++data Dec0 deriving (Typeable)+instance Show Dec0 where+    show _ = "0"+data Dec1 deriving (Typeable)+instance Show Dec1 where+    show _ = "1"+data Dec2 deriving (Typeable)+instance Show Dec2 where+    show _ = "2"+data Dec3 deriving (Typeable)+instance Show Dec3 where+    show _ = "3"+data Dec4 deriving (Typeable)+instance Show Dec4 where+    show _ = "4"+data Dec5 deriving (Typeable)+instance Show Dec5 where+    show _ = "5"+data Dec6 deriving (Typeable)+instance Show Dec6 where+    show _ = "6"+data Dec7 deriving (Typeable)+instance Show Dec7 where+    show _ = "7"+data Dec8 deriving (Typeable)+instance Show Dec8 where+    show _ = "8"+data Dec9 deriving (Typeable)+instance Show Dec9 where+    show _ = "9"
+ src/Types/Data/Num/Decimal/Literals.hs view
@@ -0,0 +1,1060 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++module Types.Data.Num.Decimal.Literals where++import Types.Data.Num.Decimal.Digits+import Types.Data.Num.Ops+++type DecPos1 p0 = Dec (DecN :. p0)+type DecPos2 p1 p0 = Dec (DecN :. p1 :. p0)+type DecPos3 p2 p1 p0 = Dec (DecN :. p2 :. p1 :. p0)+type DecPos4 p3 p2 p1 p0 = Dec (DecN :. p3 :. p2 :. p1 :. p0)+type DecPos5 p4 p3 p2 p1 p0 = Dec (DecN :. p4 :. p3 :. p2 :. p1 :. p0)+type DecPos6 p5 p4 p3 p2 p1 p0 = Dec (DecN :. p5 :. p4 :. p3 :. p2 :. p1 :. p0)+type DecPos7 p6 p5 p4 p3 p2 p1 p0 = Dec (DecN :. p6 :. p5 :. p4 :. p3 :. p2 :. p1 :. p0)++type DecNeg n = Dec (Neg' n)++type DecNeg1 p0 = DecNeg (DecN :. p0)+type DecNeg2 p1 p0 = DecNeg (DecN :. p1 :. p0)+type DecNeg3 p2 p1 p0 = DecNeg (DecN :. p2 :. p1 :. p0)+type DecNeg4 p3 p2 p1 p0 = DecNeg (DecN :. p3 :. p2 :. p1 :. p0)+type DecNeg5 p4 p3 p2 p1 p0 = DecNeg (DecN :. p4 :. p3 :. p2 :. p1 :. p0)+type DecNeg6 p5 p4 p3 p2 p1 p0 = DecNeg (DecN :. p5 :. p4 :. p3 :. p2 :. p1 :. p0)+type DecNeg7 p6 p5 p4 p3 p2 p1 p0 = DecNeg (DecN :. p6 :. p5 :. p4 :. p3 :. p2 :. p1 :. p0)+++type D0 = Dec DecN++type D1 = DecPos1 Dec1+type D2 = DecPos1 Dec2+type D3 = DecPos1 Dec3+type D4 = DecPos1 Dec4+type D5 = DecPos1 Dec5+type D6 = DecPos1 Dec6+type D7 = DecPos1 Dec7+type D8 = DecPos1 Dec8+type D9 = DecPos1 Dec9+type D10 = DecPos2 Dec1 Dec0+type D11 = DecPos2 Dec1 Dec1+type D12 = DecPos2 Dec1 Dec2+type D13 = DecPos2 Dec1 Dec3+type D14 = DecPos2 Dec1 Dec4+type D15 = DecPos2 Dec1 Dec5+type D16 = DecPos2 Dec1 Dec6+type D17 = DecPos2 Dec1 Dec7+type D18 = DecPos2 Dec1 Dec8+type D19 = DecPos2 Dec1 Dec9+type D20 = DecPos2 Dec2 Dec0+type D21 = DecPos2 Dec2 Dec1+type D22 = DecPos2 Dec2 Dec2+type D23 = DecPos2 Dec2 Dec3+type D24 = DecPos2 Dec2 Dec4+type D25 = DecPos2 Dec2 Dec5+type D26 = DecPos2 Dec2 Dec6+type D27 = DecPos2 Dec2 Dec7+type D28 = DecPos2 Dec2 Dec8+type D29 = DecPos2 Dec2 Dec9+type D30 = DecPos2 Dec3 Dec0+type D31 = DecPos2 Dec3 Dec1+type D32 = DecPos2 Dec3 Dec2+type D33 = DecPos2 Dec3 Dec3+type D34 = DecPos2 Dec3 Dec4+type D35 = DecPos2 Dec3 Dec5+type D36 = DecPos2 Dec3 Dec6+type D37 = DecPos2 Dec3 Dec7+type D38 = DecPos2 Dec3 Dec8+type D39 = DecPos2 Dec3 Dec9+type D40 = DecPos2 Dec4 Dec0+type D41 = DecPos2 Dec4 Dec1+type D42 = DecPos2 Dec4 Dec2+type D43 = DecPos2 Dec4 Dec3+type D44 = DecPos2 Dec4 Dec4+type D45 = DecPos2 Dec4 Dec5+type D46 = DecPos2 Dec4 Dec6+type D47 = DecPos2 Dec4 Dec7+type D48 = DecPos2 Dec4 Dec8+type D49 = DecPos2 Dec4 Dec9+type D50 = DecPos2 Dec5 Dec0+type D51 = DecPos2 Dec5 Dec1+type D52 = DecPos2 Dec5 Dec2+type D53 = DecPos2 Dec5 Dec3+type D54 = DecPos2 Dec5 Dec4+type D55 = DecPos2 Dec5 Dec5+type D56 = DecPos2 Dec5 Dec6+type D57 = DecPos2 Dec5 Dec7+type D58 = DecPos2 Dec5 Dec8+type D59 = DecPos2 Dec5 Dec9+type D60 = DecPos2 Dec6 Dec0+type D61 = DecPos2 Dec6 Dec1+type D62 = DecPos2 Dec6 Dec2+type D63 = DecPos2 Dec6 Dec3+type D64 = DecPos2 Dec6 Dec4+type D65 = DecPos2 Dec6 Dec5+type D66 = DecPos2 Dec6 Dec6+type D67 = DecPos2 Dec6 Dec7+type D68 = DecPos2 Dec6 Dec8+type D69 = DecPos2 Dec6 Dec9+type D70 = DecPos2 Dec7 Dec0+type D71 = DecPos2 Dec7 Dec1+type D72 = DecPos2 Dec7 Dec2+type D73 = DecPos2 Dec7 Dec3+type D74 = DecPos2 Dec7 Dec4+type D75 = DecPos2 Dec7 Dec5+type D76 = DecPos2 Dec7 Dec6+type D77 = DecPos2 Dec7 Dec7+type D78 = DecPos2 Dec7 Dec8+type D79 = DecPos2 Dec7 Dec9+type D80 = DecPos2 Dec8 Dec0+type D81 = DecPos2 Dec8 Dec1+type D82 = DecPos2 Dec8 Dec2+type D83 = DecPos2 Dec8 Dec3+type D84 = DecPos2 Dec8 Dec4+type D85 = DecPos2 Dec8 Dec5+type D86 = DecPos2 Dec8 Dec6+type D87 = DecPos2 Dec8 Dec7+type D88 = DecPos2 Dec8 Dec8+type D89 = DecPos2 Dec8 Dec9+type D90 = DecPos2 Dec9 Dec0+type D91 = DecPos2 Dec9 Dec1+type D92 = DecPos2 Dec9 Dec2+type D93 = DecPos2 Dec9 Dec3+type D94 = DecPos2 Dec9 Dec4+type D95 = DecPos2 Dec9 Dec5+type D96 = DecPos2 Dec9 Dec6+type D97 = DecPos2 Dec9 Dec7+type D98 = DecPos2 Dec9 Dec8+type D99 = DecPos2 Dec9 Dec9+type D100 = DecPos3 Dec1 Dec0 Dec0+type D101 = DecPos3 Dec1 Dec0 Dec1+type D102 = DecPos3 Dec1 Dec0 Dec2+type D103 = DecPos3 Dec1 Dec0 Dec3+type D104 = DecPos3 Dec1 Dec0 Dec4+type D105 = DecPos3 Dec1 Dec0 Dec5+type D106 = DecPos3 Dec1 Dec0 Dec6+type D107 = DecPos3 Dec1 Dec0 Dec7+type D108 = DecPos3 Dec1 Dec0 Dec8+type D109 = DecPos3 Dec1 Dec0 Dec9+type D110 = DecPos3 Dec1 Dec1 Dec0+type D111 = DecPos3 Dec1 Dec1 Dec1+type D112 = DecPos3 Dec1 Dec1 Dec2+type D113 = DecPos3 Dec1 Dec1 Dec3+type D114 = DecPos3 Dec1 Dec1 Dec4+type D115 = DecPos3 Dec1 Dec1 Dec5+type D116 = DecPos3 Dec1 Dec1 Dec6+type D117 = DecPos3 Dec1 Dec1 Dec7+type D118 = DecPos3 Dec1 Dec1 Dec8+type D119 = DecPos3 Dec1 Dec1 Dec9+type D120 = DecPos3 Dec1 Dec2 Dec0+type D121 = DecPos3 Dec1 Dec2 Dec1+type D122 = DecPos3 Dec1 Dec2 Dec2+type D123 = DecPos3 Dec1 Dec2 Dec3+type D124 = DecPos3 Dec1 Dec2 Dec4+type D125 = DecPos3 Dec1 Dec2 Dec5+type D126 = DecPos3 Dec1 Dec2 Dec6+type D127 = DecPos3 Dec1 Dec2 Dec7+type D128 = DecPos3 Dec1 Dec2 Dec8+type D129 = DecPos3 Dec1 Dec2 Dec9+type D130 = DecPos3 Dec1 Dec3 Dec0+type D131 = DecPos3 Dec1 Dec3 Dec1+type D132 = DecPos3 Dec1 Dec3 Dec2+type D133 = DecPos3 Dec1 Dec3 Dec3+type D134 = DecPos3 Dec1 Dec3 Dec4+type D135 = DecPos3 Dec1 Dec3 Dec5+type D136 = DecPos3 Dec1 Dec3 Dec6+type D137 = DecPos3 Dec1 Dec3 Dec7+type D138 = DecPos3 Dec1 Dec3 Dec8+type D139 = DecPos3 Dec1 Dec3 Dec9+type D140 = DecPos3 Dec1 Dec4 Dec0+type D141 = DecPos3 Dec1 Dec4 Dec1+type D142 = DecPos3 Dec1 Dec4 Dec2+type D143 = DecPos3 Dec1 Dec4 Dec3+type D144 = DecPos3 Dec1 Dec4 Dec4+type D145 = DecPos3 Dec1 Dec4 Dec5+type D146 = DecPos3 Dec1 Dec4 Dec6+type D147 = DecPos3 Dec1 Dec4 Dec7+type D148 = DecPos3 Dec1 Dec4 Dec8+type D149 = DecPos3 Dec1 Dec4 Dec9+type D150 = DecPos3 Dec1 Dec5 Dec0+type D151 = DecPos3 Dec1 Dec5 Dec1+type D152 = DecPos3 Dec1 Dec5 Dec2+type D153 = DecPos3 Dec1 Dec5 Dec3+type D154 = DecPos3 Dec1 Dec5 Dec4+type D155 = DecPos3 Dec1 Dec5 Dec5+type D156 = DecPos3 Dec1 Dec5 Dec6+type D157 = DecPos3 Dec1 Dec5 Dec7+type D158 = DecPos3 Dec1 Dec5 Dec8+type D159 = DecPos3 Dec1 Dec5 Dec9+type D160 = DecPos3 Dec1 Dec6 Dec0+type D161 = DecPos3 Dec1 Dec6 Dec1+type D162 = DecPos3 Dec1 Dec6 Dec2+type D163 = DecPos3 Dec1 Dec6 Dec3+type D164 = DecPos3 Dec1 Dec6 Dec4+type D165 = DecPos3 Dec1 Dec6 Dec5+type D166 = DecPos3 Dec1 Dec6 Dec6+type D167 = DecPos3 Dec1 Dec6 Dec7+type D168 = DecPos3 Dec1 Dec6 Dec8+type D169 = DecPos3 Dec1 Dec6 Dec9+type D170 = DecPos3 Dec1 Dec7 Dec0+type D171 = DecPos3 Dec1 Dec7 Dec1+type D172 = DecPos3 Dec1 Dec7 Dec2+type D173 = DecPos3 Dec1 Dec7 Dec3+type D174 = DecPos3 Dec1 Dec7 Dec4+type D175 = DecPos3 Dec1 Dec7 Dec5+type D176 = DecPos3 Dec1 Dec7 Dec6+type D177 = DecPos3 Dec1 Dec7 Dec7+type D178 = DecPos3 Dec1 Dec7 Dec8+type D179 = DecPos3 Dec1 Dec7 Dec9+type D180 = DecPos3 Dec1 Dec8 Dec0+type D181 = DecPos3 Dec1 Dec8 Dec1+type D182 = DecPos3 Dec1 Dec8 Dec2+type D183 = DecPos3 Dec1 Dec8 Dec3+type D184 = DecPos3 Dec1 Dec8 Dec4+type D185 = DecPos3 Dec1 Dec8 Dec5+type D186 = DecPos3 Dec1 Dec8 Dec6+type D187 = DecPos3 Dec1 Dec8 Dec7+type D188 = DecPos3 Dec1 Dec8 Dec8+type D189 = DecPos3 Dec1 Dec8 Dec9+type D190 = DecPos3 Dec1 Dec9 Dec0+type D191 = DecPos3 Dec1 Dec9 Dec1+type D192 = DecPos3 Dec1 Dec9 Dec2+type D193 = DecPos3 Dec1 Dec9 Dec3+type D194 = DecPos3 Dec1 Dec9 Dec4+type D195 = DecPos3 Dec1 Dec9 Dec5+type D196 = DecPos3 Dec1 Dec9 Dec6+type D197 = DecPos3 Dec1 Dec9 Dec7+type D198 = DecPos3 Dec1 Dec9 Dec8+type D199 = DecPos3 Dec1 Dec9 Dec9+type D200 = DecPos3 Dec2 Dec0 Dec0+type D201 = DecPos3 Dec2 Dec0 Dec1+type D202 = DecPos3 Dec2 Dec0 Dec2+type D203 = DecPos3 Dec2 Dec0 Dec3+type D204 = DecPos3 Dec2 Dec0 Dec4+type D205 = DecPos3 Dec2 Dec0 Dec5+type D206 = DecPos3 Dec2 Dec0 Dec6+type D207 = DecPos3 Dec2 Dec0 Dec7+type D208 = DecPos3 Dec2 Dec0 Dec8+type D209 = DecPos3 Dec2 Dec0 Dec9+type D210 = DecPos3 Dec2 Dec1 Dec0+type D211 = DecPos3 Dec2 Dec1 Dec1+type D212 = DecPos3 Dec2 Dec1 Dec2+type D213 = DecPos3 Dec2 Dec1 Dec3+type D214 = DecPos3 Dec2 Dec1 Dec4+type D215 = DecPos3 Dec2 Dec1 Dec5+type D216 = DecPos3 Dec2 Dec1 Dec6+type D217 = DecPos3 Dec2 Dec1 Dec7+type D218 = DecPos3 Dec2 Dec1 Dec8+type D219 = DecPos3 Dec2 Dec1 Dec9+type D220 = DecPos3 Dec2 Dec2 Dec0+type D221 = DecPos3 Dec2 Dec2 Dec1+type D222 = DecPos3 Dec2 Dec2 Dec2+type D223 = DecPos3 Dec2 Dec2 Dec3+type D224 = DecPos3 Dec2 Dec2 Dec4+type D225 = DecPos3 Dec2 Dec2 Dec5+type D226 = DecPos3 Dec2 Dec2 Dec6+type D227 = DecPos3 Dec2 Dec2 Dec7+type D228 = DecPos3 Dec2 Dec2 Dec8+type D229 = DecPos3 Dec2 Dec2 Dec9+type D230 = DecPos3 Dec2 Dec3 Dec0+type D231 = DecPos3 Dec2 Dec3 Dec1+type D232 = DecPos3 Dec2 Dec3 Dec2+type D233 = DecPos3 Dec2 Dec3 Dec3+type D234 = DecPos3 Dec2 Dec3 Dec4+type D235 = DecPos3 Dec2 Dec3 Dec5+type D236 = DecPos3 Dec2 Dec3 Dec6+type D237 = DecPos3 Dec2 Dec3 Dec7+type D238 = DecPos3 Dec2 Dec3 Dec8+type D239 = DecPos3 Dec2 Dec3 Dec9+type D240 = DecPos3 Dec2 Dec4 Dec0+type D241 = DecPos3 Dec2 Dec4 Dec1+type D242 = DecPos3 Dec2 Dec4 Dec2+type D243 = DecPos3 Dec2 Dec4 Dec3+type D244 = DecPos3 Dec2 Dec4 Dec4+type D245 = DecPos3 Dec2 Dec4 Dec5+type D246 = DecPos3 Dec2 Dec4 Dec6+type D247 = DecPos3 Dec2 Dec4 Dec7+type D248 = DecPos3 Dec2 Dec4 Dec8+type D249 = DecPos3 Dec2 Dec4 Dec9+type D250 = DecPos3 Dec2 Dec5 Dec0+type D251 = DecPos3 Dec2 Dec5 Dec1+type D252 = DecPos3 Dec2 Dec5 Dec2+type D253 = DecPos3 Dec2 Dec5 Dec3+type D254 = DecPos3 Dec2 Dec5 Dec4+type D255 = DecPos3 Dec2 Dec5 Dec5+type D256 = DecPos3 Dec2 Dec5 Dec6++type DN1 = DecNeg1 Dec1+type DN2 = DecNeg1 Dec2+type DN3 = DecNeg1 Dec3+type DN4 = DecNeg1 Dec4+type DN5 = DecNeg1 Dec5+type DN6 = DecNeg1 Dec6+type DN7 = DecNeg1 Dec7+type DN8 = DecNeg1 Dec8+type DN9 = DecNeg1 Dec9+type DN10 = DecNeg2 Dec1 Dec0+type DN11 = DecNeg2 Dec1 Dec1+type DN12 = DecNeg2 Dec1 Dec2+type DN13 = DecNeg2 Dec1 Dec3+type DN14 = DecNeg2 Dec1 Dec4+type DN15 = DecNeg2 Dec1 Dec5+type DN16 = DecNeg2 Dec1 Dec6+type DN17 = DecNeg2 Dec1 Dec7+type DN18 = DecNeg2 Dec1 Dec8+type DN19 = DecNeg2 Dec1 Dec9+type DN20 = DecNeg2 Dec2 Dec0+type DN21 = DecNeg2 Dec2 Dec1+type DN22 = DecNeg2 Dec2 Dec2+type DN23 = DecNeg2 Dec2 Dec3+type DN24 = DecNeg2 Dec2 Dec4+type DN25 = DecNeg2 Dec2 Dec5+type DN26 = DecNeg2 Dec2 Dec6+type DN27 = DecNeg2 Dec2 Dec7+type DN28 = DecNeg2 Dec2 Dec8+type DN29 = DecNeg2 Dec2 Dec9+type DN30 = DecNeg2 Dec3 Dec0+type DN31 = DecNeg2 Dec3 Dec1+type DN32 = DecNeg2 Dec3 Dec2+type DN33 = DecNeg2 Dec3 Dec3+type DN34 = DecNeg2 Dec3 Dec4+type DN35 = DecNeg2 Dec3 Dec5+type DN36 = DecNeg2 Dec3 Dec6+type DN37 = DecNeg2 Dec3 Dec7+type DN38 = DecNeg2 Dec3 Dec8+type DN39 = DecNeg2 Dec3 Dec9+type DN40 = DecNeg2 Dec4 Dec0+type DN41 = DecNeg2 Dec4 Dec1+type DN42 = DecNeg2 Dec4 Dec2+type DN43 = DecNeg2 Dec4 Dec3+type DN44 = DecNeg2 Dec4 Dec4+type DN45 = DecNeg2 Dec4 Dec5+type DN46 = DecNeg2 Dec4 Dec6+type DN47 = DecNeg2 Dec4 Dec7+type DN48 = DecNeg2 Dec4 Dec8+type DN49 = DecNeg2 Dec4 Dec9+type DN50 = DecNeg2 Dec5 Dec0+type DN51 = DecNeg2 Dec5 Dec1+type DN52 = DecNeg2 Dec5 Dec2+type DN53 = DecNeg2 Dec5 Dec3+type DN54 = DecNeg2 Dec5 Dec4+type DN55 = DecNeg2 Dec5 Dec5+type DN56 = DecNeg2 Dec5 Dec6+type DN57 = DecNeg2 Dec5 Dec7+type DN58 = DecNeg2 Dec5 Dec8+type DN59 = DecNeg2 Dec5 Dec9+type DN60 = DecNeg2 Dec6 Dec0+type DN61 = DecNeg2 Dec6 Dec1+type DN62 = DecNeg2 Dec6 Dec2+type DN63 = DecNeg2 Dec6 Dec3+type DN64 = DecNeg2 Dec6 Dec4+type DN65 = DecNeg2 Dec6 Dec5+type DN66 = DecNeg2 Dec6 Dec6+type DN67 = DecNeg2 Dec6 Dec7+type DN68 = DecNeg2 Dec6 Dec8+type DN69 = DecNeg2 Dec6 Dec9+type DN70 = DecNeg2 Dec7 Dec0+type DN71 = DecNeg2 Dec7 Dec1+type DN72 = DecNeg2 Dec7 Dec2+type DN73 = DecNeg2 Dec7 Dec3+type DN74 = DecNeg2 Dec7 Dec4+type DN75 = DecNeg2 Dec7 Dec5+type DN76 = DecNeg2 Dec7 Dec6+type DN77 = DecNeg2 Dec7 Dec7+type DN78 = DecNeg2 Dec7 Dec8+type DN79 = DecNeg2 Dec7 Dec9+type DN80 = DecNeg2 Dec8 Dec0+type DN81 = DecNeg2 Dec8 Dec1+type DN82 = DecNeg2 Dec8 Dec2+type DN83 = DecNeg2 Dec8 Dec3+type DN84 = DecNeg2 Dec8 Dec4+type DN85 = DecNeg2 Dec8 Dec5+type DN86 = DecNeg2 Dec8 Dec6+type DN87 = DecNeg2 Dec8 Dec7+type DN88 = DecNeg2 Dec8 Dec8+type DN89 = DecNeg2 Dec8 Dec9+type DN90 = DecNeg2 Dec9 Dec0+type DN91 = DecNeg2 Dec9 Dec1+type DN92 = DecNeg2 Dec9 Dec2+type DN93 = DecNeg2 Dec9 Dec3+type DN94 = DecNeg2 Dec9 Dec4+type DN95 = DecNeg2 Dec9 Dec5+type DN96 = DecNeg2 Dec9 Dec6+type DN97 = DecNeg2 Dec9 Dec7+type DN98 = DecNeg2 Dec9 Dec8+type DN99 = DecNeg2 Dec9 Dec9+type DN100 = DecNeg3 Dec1 Dec0 Dec0+type DN101 = DecNeg3 Dec1 Dec0 Dec1+type DN102 = DecNeg3 Dec1 Dec0 Dec2+type DN103 = DecNeg3 Dec1 Dec0 Dec3+type DN104 = DecNeg3 Dec1 Dec0 Dec4+type DN105 = DecNeg3 Dec1 Dec0 Dec5+type DN106 = DecNeg3 Dec1 Dec0 Dec6+type DN107 = DecNeg3 Dec1 Dec0 Dec7+type DN108 = DecNeg3 Dec1 Dec0 Dec8+type DN109 = DecNeg3 Dec1 Dec0 Dec9+type DN110 = DecNeg3 Dec1 Dec1 Dec0+type DN111 = DecNeg3 Dec1 Dec1 Dec1+type DN112 = DecNeg3 Dec1 Dec1 Dec2+type DN113 = DecNeg3 Dec1 Dec1 Dec3+type DN114 = DecNeg3 Dec1 Dec1 Dec4+type DN115 = DecNeg3 Dec1 Dec1 Dec5+type DN116 = DecNeg3 Dec1 Dec1 Dec6+type DN117 = DecNeg3 Dec1 Dec1 Dec7+type DN118 = DecNeg3 Dec1 Dec1 Dec8+type DN119 = DecNeg3 Dec1 Dec1 Dec9+type DN120 = DecNeg3 Dec1 Dec2 Dec0+type DN121 = DecNeg3 Dec1 Dec2 Dec1+type DN122 = DecNeg3 Dec1 Dec2 Dec2+type DN123 = DecNeg3 Dec1 Dec2 Dec3+type DN124 = DecNeg3 Dec1 Dec2 Dec4+type DN125 = DecNeg3 Dec1 Dec2 Dec5+type DN126 = DecNeg3 Dec1 Dec2 Dec6+type DN127 = DecNeg3 Dec1 Dec2 Dec7+type DN128 = DecNeg3 Dec1 Dec2 Dec8+type DN129 = DecNeg3 Dec1 Dec2 Dec9+type DN130 = DecNeg3 Dec1 Dec3 Dec0+type DN131 = DecNeg3 Dec1 Dec3 Dec1+type DN132 = DecNeg3 Dec1 Dec3 Dec2+type DN133 = DecNeg3 Dec1 Dec3 Dec3+type DN134 = DecNeg3 Dec1 Dec3 Dec4+type DN135 = DecNeg3 Dec1 Dec3 Dec5+type DN136 = DecNeg3 Dec1 Dec3 Dec6+type DN137 = DecNeg3 Dec1 Dec3 Dec7+type DN138 = DecNeg3 Dec1 Dec3 Dec8+type DN139 = DecNeg3 Dec1 Dec3 Dec9+type DN140 = DecNeg3 Dec1 Dec4 Dec0+type DN141 = DecNeg3 Dec1 Dec4 Dec1+type DN142 = DecNeg3 Dec1 Dec4 Dec2+type DN143 = DecNeg3 Dec1 Dec4 Dec3+type DN144 = DecNeg3 Dec1 Dec4 Dec4+type DN145 = DecNeg3 Dec1 Dec4 Dec5+type DN146 = DecNeg3 Dec1 Dec4 Dec6+type DN147 = DecNeg3 Dec1 Dec4 Dec7+type DN148 = DecNeg3 Dec1 Dec4 Dec8+type DN149 = DecNeg3 Dec1 Dec4 Dec9+type DN150 = DecNeg3 Dec1 Dec5 Dec0+type DN151 = DecNeg3 Dec1 Dec5 Dec1+type DN152 = DecNeg3 Dec1 Dec5 Dec2+type DN153 = DecNeg3 Dec1 Dec5 Dec3+type DN154 = DecNeg3 Dec1 Dec5 Dec4+type DN155 = DecNeg3 Dec1 Dec5 Dec5+type DN156 = DecNeg3 Dec1 Dec5 Dec6+type DN157 = DecNeg3 Dec1 Dec5 Dec7+type DN158 = DecNeg3 Dec1 Dec5 Dec8+type DN159 = DecNeg3 Dec1 Dec5 Dec9+type DN160 = DecNeg3 Dec1 Dec6 Dec0+type DN161 = DecNeg3 Dec1 Dec6 Dec1+type DN162 = DecNeg3 Dec1 Dec6 Dec2+type DN163 = DecNeg3 Dec1 Dec6 Dec3+type DN164 = DecNeg3 Dec1 Dec6 Dec4+type DN165 = DecNeg3 Dec1 Dec6 Dec5+type DN166 = DecNeg3 Dec1 Dec6 Dec6+type DN167 = DecNeg3 Dec1 Dec6 Dec7+type DN168 = DecNeg3 Dec1 Dec6 Dec8+type DN169 = DecNeg3 Dec1 Dec6 Dec9+type DN170 = DecNeg3 Dec1 Dec7 Dec0+type DN171 = DecNeg3 Dec1 Dec7 Dec1+type DN172 = DecNeg3 Dec1 Dec7 Dec2+type DN173 = DecNeg3 Dec1 Dec7 Dec3+type DN174 = DecNeg3 Dec1 Dec7 Dec4+type DN175 = DecNeg3 Dec1 Dec7 Dec5+type DN176 = DecNeg3 Dec1 Dec7 Dec6+type DN177 = DecNeg3 Dec1 Dec7 Dec7+type DN178 = DecNeg3 Dec1 Dec7 Dec8+type DN179 = DecNeg3 Dec1 Dec7 Dec9+type DN180 = DecNeg3 Dec1 Dec8 Dec0+type DN181 = DecNeg3 Dec1 Dec8 Dec1+type DN182 = DecNeg3 Dec1 Dec8 Dec2+type DN183 = DecNeg3 Dec1 Dec8 Dec3+type DN184 = DecNeg3 Dec1 Dec8 Dec4+type DN185 = DecNeg3 Dec1 Dec8 Dec5+type DN186 = DecNeg3 Dec1 Dec8 Dec6+type DN187 = DecNeg3 Dec1 Dec8 Dec7+type DN188 = DecNeg3 Dec1 Dec8 Dec8+type DN189 = DecNeg3 Dec1 Dec8 Dec9+type DN190 = DecNeg3 Dec1 Dec9 Dec0+type DN191 = DecNeg3 Dec1 Dec9 Dec1+type DN192 = DecNeg3 Dec1 Dec9 Dec2+type DN193 = DecNeg3 Dec1 Dec9 Dec3+type DN194 = DecNeg3 Dec1 Dec9 Dec4+type DN195 = DecNeg3 Dec1 Dec9 Dec5+type DN196 = DecNeg3 Dec1 Dec9 Dec6+type DN197 = DecNeg3 Dec1 Dec9 Dec7+type DN198 = DecNeg3 Dec1 Dec9 Dec8+type DN199 = DecNeg3 Dec1 Dec9 Dec9+type DN200 = DecNeg3 Dec2 Dec0 Dec0+type DN201 = DecNeg3 Dec2 Dec0 Dec1+type DN202 = DecNeg3 Dec2 Dec0 Dec2+type DN203 = DecNeg3 Dec2 Dec0 Dec3+type DN204 = DecNeg3 Dec2 Dec0 Dec4+type DN205 = DecNeg3 Dec2 Dec0 Dec5+type DN206 = DecNeg3 Dec2 Dec0 Dec6+type DN207 = DecNeg3 Dec2 Dec0 Dec7+type DN208 = DecNeg3 Dec2 Dec0 Dec8+type DN209 = DecNeg3 Dec2 Dec0 Dec9+type DN210 = DecNeg3 Dec2 Dec1 Dec0+type DN211 = DecNeg3 Dec2 Dec1 Dec1+type DN212 = DecNeg3 Dec2 Dec1 Dec2+type DN213 = DecNeg3 Dec2 Dec1 Dec3+type DN214 = DecNeg3 Dec2 Dec1 Dec4+type DN215 = DecNeg3 Dec2 Dec1 Dec5+type DN216 = DecNeg3 Dec2 Dec1 Dec6+type DN217 = DecNeg3 Dec2 Dec1 Dec7+type DN218 = DecNeg3 Dec2 Dec1 Dec8+type DN219 = DecNeg3 Dec2 Dec1 Dec9+type DN220 = DecNeg3 Dec2 Dec2 Dec0+type DN221 = DecNeg3 Dec2 Dec2 Dec1+type DN222 = DecNeg3 Dec2 Dec2 Dec2+type DN223 = DecNeg3 Dec2 Dec2 Dec3+type DN224 = DecNeg3 Dec2 Dec2 Dec4+type DN225 = DecNeg3 Dec2 Dec2 Dec5+type DN226 = DecNeg3 Dec2 Dec2 Dec6+type DN227 = DecNeg3 Dec2 Dec2 Dec7+type DN228 = DecNeg3 Dec2 Dec2 Dec8+type DN229 = DecNeg3 Dec2 Dec2 Dec9+type DN230 = DecNeg3 Dec2 Dec3 Dec0+type DN231 = DecNeg3 Dec2 Dec3 Dec1+type DN232 = DecNeg3 Dec2 Dec3 Dec2+type DN233 = DecNeg3 Dec2 Dec3 Dec3+type DN234 = DecNeg3 Dec2 Dec3 Dec4+type DN235 = DecNeg3 Dec2 Dec3 Dec5+type DN236 = DecNeg3 Dec2 Dec3 Dec6+type DN237 = DecNeg3 Dec2 Dec3 Dec7+type DN238 = DecNeg3 Dec2 Dec3 Dec8+type DN239 = DecNeg3 Dec2 Dec3 Dec9+type DN240 = DecNeg3 Dec2 Dec4 Dec0+type DN241 = DecNeg3 Dec2 Dec4 Dec1+type DN242 = DecNeg3 Dec2 Dec4 Dec2+type DN243 = DecNeg3 Dec2 Dec4 Dec3+type DN244 = DecNeg3 Dec2 Dec4 Dec4+type DN245 = DecNeg3 Dec2 Dec4 Dec5+type DN246 = DecNeg3 Dec2 Dec4 Dec6+type DN247 = DecNeg3 Dec2 Dec4 Dec7+type DN248 = DecNeg3 Dec2 Dec4 Dec8+type DN249 = DecNeg3 Dec2 Dec4 Dec9+type DN250 = DecNeg3 Dec2 Dec5 Dec0+type DN251 = DecNeg3 Dec2 Dec5 Dec1+type DN252 = DecNeg3 Dec2 Dec5 Dec2+type DN253 = DecNeg3 Dec2 Dec5 Dec3+type DN254 = DecNeg3 Dec2 Dec5 Dec4+type DN255 = DecNeg3 Dec2 Dec5 Dec5+type DN256 = DecNeg3 Dec2 Dec5 Dec6+++d0 :: D0; d0 = undefined++d1 :: D1; d1 = undefined+d2 :: D2; d2 = undefined+d3 :: D3; d3 = undefined+d4 :: D4; d4 = undefined+d5 :: D5; d5 = undefined+d6 :: D6; d6 = undefined+d7 :: D7; d7 = undefined+d8 :: D8; d8 = undefined+d9 :: D9; d9 = undefined+d10 :: D10; d10 = undefined+d11 :: D11; d11 = undefined+d12 :: D12; d12 = undefined+d13 :: D13; d13 = undefined+d14 :: D14; d14 = undefined+d15 :: D15; d15 = undefined+d16 :: D16; d16 = undefined+d17 :: D17; d17 = undefined+d18 :: D18; d18 = undefined+d19 :: D19; d19 = undefined+d20 :: D20; d20 = undefined+d21 :: D21; d21 = undefined+d22 :: D22; d22 = undefined+d23 :: D23; d23 = undefined+d24 :: D24; d24 = undefined+d25 :: D25; d25 = undefined+d26 :: D26; d26 = undefined+d27 :: D27; d27 = undefined+d28 :: D28; d28 = undefined+d29 :: D29; d29 = undefined+d30 :: D30; d30 = undefined+d31 :: D31; d31 = undefined+d32 :: D32; d32 = undefined+d33 :: D33; d33 = undefined+d34 :: D34; d34 = undefined+d35 :: D35; d35 = undefined+d36 :: D36; d36 = undefined+d37 :: D37; d37 = undefined+d38 :: D38; d38 = undefined+d39 :: D39; d39 = undefined+d40 :: D40; d40 = undefined+d41 :: D41; d41 = undefined+d42 :: D42; d42 = undefined+d43 :: D43; d43 = undefined+d44 :: D44; d44 = undefined+d45 :: D45; d45 = undefined+d46 :: D46; d46 = undefined+d47 :: D47; d47 = undefined+d48 :: D48; d48 = undefined+d49 :: D49; d49 = undefined+d50 :: D50; d50 = undefined+d51 :: D51; d51 = undefined+d52 :: D52; d52 = undefined+d53 :: D53; d53 = undefined+d54 :: D54; d54 = undefined+d55 :: D55; d55 = undefined+d56 :: D56; d56 = undefined+d57 :: D57; d57 = undefined+d58 :: D58; d58 = undefined+d59 :: D59; d59 = undefined+d60 :: D60; d60 = undefined+d61 :: D61; d61 = undefined+d62 :: D62; d62 = undefined+d63 :: D63; d63 = undefined+d64 :: D64; d64 = undefined+d65 :: D65; d65 = undefined+d66 :: D66; d66 = undefined+d67 :: D67; d67 = undefined+d68 :: D68; d68 = undefined+d69 :: D69; d69 = undefined+d70 :: D70; d70 = undefined+d71 :: D71; d71 = undefined+d72 :: D72; d72 = undefined+d73 :: D73; d73 = undefined+d74 :: D74; d74 = undefined+d75 :: D75; d75 = undefined+d76 :: D76; d76 = undefined+d77 :: D77; d77 = undefined+d78 :: D78; d78 = undefined+d79 :: D79; d79 = undefined+d80 :: D80; d80 = undefined+d81 :: D81; d81 = undefined+d82 :: D82; d82 = undefined+d83 :: D83; d83 = undefined+d84 :: D84; d84 = undefined+d85 :: D85; d85 = undefined+d86 :: D86; d86 = undefined+d87 :: D87; d87 = undefined+d88 :: D88; d88 = undefined+d89 :: D89; d89 = undefined+d90 :: D90; d90 = undefined+d91 :: D91; d91 = undefined+d92 :: D92; d92 = undefined+d93 :: D93; d93 = undefined+d94 :: D94; d94 = undefined+d95 :: D95; d95 = undefined+d96 :: D96; d96 = undefined+d97 :: D97; d97 = undefined+d98 :: D98; d98 = undefined+d99 :: D99; d99 = undefined+d100 :: D100; d100 = undefined+d101 :: D101; d101 = undefined+d102 :: D102; d102 = undefined+d103 :: D103; d103 = undefined+d104 :: D104; d104 = undefined+d105 :: D105; d105 = undefined+d106 :: D106; d106 = undefined+d107 :: D107; d107 = undefined+d108 :: D108; d108 = undefined+d109 :: D109; d109 = undefined+d110 :: D110; d110 = undefined+d111 :: D111; d111 = undefined+d112 :: D112; d112 = undefined+d113 :: D113; d113 = undefined+d114 :: D114; d114 = undefined+d115 :: D115; d115 = undefined+d116 :: D116; d116 = undefined+d117 :: D117; d117 = undefined+d118 :: D118; d118 = undefined+d119 :: D119; d119 = undefined+d120 :: D120; d120 = undefined+d121 :: D121; d121 = undefined+d122 :: D122; d122 = undefined+d123 :: D123; d123 = undefined+d124 :: D124; d124 = undefined+d125 :: D125; d125 = undefined+d126 :: D126; d126 = undefined+d127 :: D127; d127 = undefined+d128 :: D128; d128 = undefined+d129 :: D129; d129 = undefined+d130 :: D130; d130 = undefined+d131 :: D131; d131 = undefined+d132 :: D132; d132 = undefined+d133 :: D133; d133 = undefined+d134 :: D134; d134 = undefined+d135 :: D135; d135 = undefined+d136 :: D136; d136 = undefined+d137 :: D137; d137 = undefined+d138 :: D138; d138 = undefined+d139 :: D139; d139 = undefined+d140 :: D140; d140 = undefined+d141 :: D141; d141 = undefined+d142 :: D142; d142 = undefined+d143 :: D143; d143 = undefined+d144 :: D144; d144 = undefined+d145 :: D145; d145 = undefined+d146 :: D146; d146 = undefined+d147 :: D147; d147 = undefined+d148 :: D148; d148 = undefined+d149 :: D149; d149 = undefined+d150 :: D150; d150 = undefined+d151 :: D151; d151 = undefined+d152 :: D152; d152 = undefined+d153 :: D153; d153 = undefined+d154 :: D154; d154 = undefined+d155 :: D155; d155 = undefined+d156 :: D156; d156 = undefined+d157 :: D157; d157 = undefined+d158 :: D158; d158 = undefined+d159 :: D159; d159 = undefined+d160 :: D160; d160 = undefined+d161 :: D161; d161 = undefined+d162 :: D162; d162 = undefined+d163 :: D163; d163 = undefined+d164 :: D164; d164 = undefined+d165 :: D165; d165 = undefined+d166 :: D166; d166 = undefined+d167 :: D167; d167 = undefined+d168 :: D168; d168 = undefined+d169 :: D169; d169 = undefined+d170 :: D170; d170 = undefined+d171 :: D171; d171 = undefined+d172 :: D172; d172 = undefined+d173 :: D173; d173 = undefined+d174 :: D174; d174 = undefined+d175 :: D175; d175 = undefined+d176 :: D176; d176 = undefined+d177 :: D177; d177 = undefined+d178 :: D178; d178 = undefined+d179 :: D179; d179 = undefined+d180 :: D180; d180 = undefined+d181 :: D181; d181 = undefined+d182 :: D182; d182 = undefined+d183 :: D183; d183 = undefined+d184 :: D184; d184 = undefined+d185 :: D185; d185 = undefined+d186 :: D186; d186 = undefined+d187 :: D187; d187 = undefined+d188 :: D188; d188 = undefined+d189 :: D189; d189 = undefined+d190 :: D190; d190 = undefined+d191 :: D191; d191 = undefined+d192 :: D192; d192 = undefined+d193 :: D193; d193 = undefined+d194 :: D194; d194 = undefined+d195 :: D195; d195 = undefined+d196 :: D196; d196 = undefined+d197 :: D197; d197 = undefined+d198 :: D198; d198 = undefined+d199 :: D199; d199 = undefined+d200 :: D200; d200 = undefined+d201 :: D201; d201 = undefined+d202 :: D202; d202 = undefined+d203 :: D203; d203 = undefined+d204 :: D204; d204 = undefined+d205 :: D205; d205 = undefined+d206 :: D206; d206 = undefined+d207 :: D207; d207 = undefined+d208 :: D208; d208 = undefined+d209 :: D209; d209 = undefined+d210 :: D210; d210 = undefined+d211 :: D211; d211 = undefined+d212 :: D212; d212 = undefined+d213 :: D213; d213 = undefined+d214 :: D214; d214 = undefined+d215 :: D215; d215 = undefined+d216 :: D216; d216 = undefined+d217 :: D217; d217 = undefined+d218 :: D218; d218 = undefined+d219 :: D219; d219 = undefined+d220 :: D220; d220 = undefined+d221 :: D221; d221 = undefined+d222 :: D222; d222 = undefined+d223 :: D223; d223 = undefined+d224 :: D224; d224 = undefined+d225 :: D225; d225 = undefined+d226 :: D226; d226 = undefined+d227 :: D227; d227 = undefined+d228 :: D228; d228 = undefined+d229 :: D229; d229 = undefined+d230 :: D230; d230 = undefined+d231 :: D231; d231 = undefined+d232 :: D232; d232 = undefined+d233 :: D233; d233 = undefined+d234 :: D234; d234 = undefined+d235 :: D235; d235 = undefined+d236 :: D236; d236 = undefined+d237 :: D237; d237 = undefined+d238 :: D238; d238 = undefined+d239 :: D239; d239 = undefined+d240 :: D240; d240 = undefined+d241 :: D241; d241 = undefined+d242 :: D242; d242 = undefined+d243 :: D243; d243 = undefined+d244 :: D244; d244 = undefined+d245 :: D245; d245 = undefined+d246 :: D246; d246 = undefined+d247 :: D247; d247 = undefined+d248 :: D248; d248 = undefined+d249 :: D249; d249 = undefined+d250 :: D250; d250 = undefined+d251 :: D251; d251 = undefined+d252 :: D252; d252 = undefined+d253 :: D253; d253 = undefined+d254 :: D254; d254 = undefined+d255 :: D255; d255 = undefined+d256 :: D256; d256 = undefined++dn1 :: DN1; dn1 = undefined+dn2 :: DN2; dn2 = undefined+dn3 :: DN3; dn3 = undefined+dn4 :: DN4; dn4 = undefined+dn5 :: DN5; dn5 = undefined+dn6 :: DN6; dn6 = undefined+dn7 :: DN7; dn7 = undefined+dn8 :: DN8; dn8 = undefined+dn9 :: DN9; dn9 = undefined+dn10 :: DN10; dn10 = undefined+dn11 :: DN11; dn11 = undefined+dn12 :: DN12; dn12 = undefined+dn13 :: DN13; dn13 = undefined+dn14 :: DN14; dn14 = undefined+dn15 :: DN15; dn15 = undefined+dn16 :: DN16; dn16 = undefined+dn17 :: DN17; dn17 = undefined+dn18 :: DN18; dn18 = undefined+dn19 :: DN19; dn19 = undefined+dn20 :: DN20; dn20 = undefined+dn21 :: DN21; dn21 = undefined+dn22 :: DN22; dn22 = undefined+dn23 :: DN23; dn23 = undefined+dn24 :: DN24; dn24 = undefined+dn25 :: DN25; dn25 = undefined+dn26 :: DN26; dn26 = undefined+dn27 :: DN27; dn27 = undefined+dn28 :: DN28; dn28 = undefined+dn29 :: DN29; dn29 = undefined+dn30 :: DN30; dn30 = undefined+dn31 :: DN31; dn31 = undefined+dn32 :: DN32; dn32 = undefined+dn33 :: DN33; dn33 = undefined+dn34 :: DN34; dn34 = undefined+dn35 :: DN35; dn35 = undefined+dn36 :: DN36; dn36 = undefined+dn37 :: DN37; dn37 = undefined+dn38 :: DN38; dn38 = undefined+dn39 :: DN39; dn39 = undefined+dn40 :: DN40; dn40 = undefined+dn41 :: DN41; dn41 = undefined+dn42 :: DN42; dn42 = undefined+dn43 :: DN43; dn43 = undefined+dn44 :: DN44; dn44 = undefined+dn45 :: DN45; dn45 = undefined+dn46 :: DN46; dn46 = undefined+dn47 :: DN47; dn47 = undefined+dn48 :: DN48; dn48 = undefined+dn49 :: DN49; dn49 = undefined+dn50 :: DN50; dn50 = undefined+dn51 :: DN51; dn51 = undefined+dn52 :: DN52; dn52 = undefined+dn53 :: DN53; dn53 = undefined+dn54 :: DN54; dn54 = undefined+dn55 :: DN55; dn55 = undefined+dn56 :: DN56; dn56 = undefined+dn57 :: DN57; dn57 = undefined+dn58 :: DN58; dn58 = undefined+dn59 :: DN59; dn59 = undefined+dn60 :: DN60; dn60 = undefined+dn61 :: DN61; dn61 = undefined+dn62 :: DN62; dn62 = undefined+dn63 :: DN63; dn63 = undefined+dn64 :: DN64; dn64 = undefined+dn65 :: DN65; dn65 = undefined+dn66 :: DN66; dn66 = undefined+dn67 :: DN67; dn67 = undefined+dn68 :: DN68; dn68 = undefined+dn69 :: DN69; dn69 = undefined+dn70 :: DN70; dn70 = undefined+dn71 :: DN71; dn71 = undefined+dn72 :: DN72; dn72 = undefined+dn73 :: DN73; dn73 = undefined+dn74 :: DN74; dn74 = undefined+dn75 :: DN75; dn75 = undefined+dn76 :: DN76; dn76 = undefined+dn77 :: DN77; dn77 = undefined+dn78 :: DN78; dn78 = undefined+dn79 :: DN79; dn79 = undefined+dn80 :: DN80; dn80 = undefined+dn81 :: DN81; dn81 = undefined+dn82 :: DN82; dn82 = undefined+dn83 :: DN83; dn83 = undefined+dn84 :: DN84; dn84 = undefined+dn85 :: DN85; dn85 = undefined+dn86 :: DN86; dn86 = undefined+dn87 :: DN87; dn87 = undefined+dn88 :: DN88; dn88 = undefined+dn89 :: DN89; dn89 = undefined+dn90 :: DN90; dn90 = undefined+dn91 :: DN91; dn91 = undefined+dn92 :: DN92; dn92 = undefined+dn93 :: DN93; dn93 = undefined+dn94 :: DN94; dn94 = undefined+dn95 :: DN95; dn95 = undefined+dn96 :: DN96; dn96 = undefined+dn97 :: DN97; dn97 = undefined+dn98 :: DN98; dn98 = undefined+dn99 :: DN99; dn99 = undefined+dn100 :: DN100; dn100 = undefined+dn101 :: DN101; dn101 = undefined+dn102 :: DN102; dn102 = undefined+dn103 :: DN103; dn103 = undefined+dn104 :: DN104; dn104 = undefined+dn105 :: DN105; dn105 = undefined+dn106 :: DN106; dn106 = undefined+dn107 :: DN107; dn107 = undefined+dn108 :: DN108; dn108 = undefined+dn109 :: DN109; dn109 = undefined+dn110 :: DN110; dn110 = undefined+dn111 :: DN111; dn111 = undefined+dn112 :: DN112; dn112 = undefined+dn113 :: DN113; dn113 = undefined+dn114 :: DN114; dn114 = undefined+dn115 :: DN115; dn115 = undefined+dn116 :: DN116; dn116 = undefined+dn117 :: DN117; dn117 = undefined+dn118 :: DN118; dn118 = undefined+dn119 :: DN119; dn119 = undefined+dn120 :: DN120; dn120 = undefined+dn121 :: DN121; dn121 = undefined+dn122 :: DN122; dn122 = undefined+dn123 :: DN123; dn123 = undefined+dn124 :: DN124; dn124 = undefined+dn125 :: DN125; dn125 = undefined+dn126 :: DN126; dn126 = undefined+dn127 :: DN127; dn127 = undefined+dn128 :: DN128; dn128 = undefined+dn129 :: DN129; dn129 = undefined+dn130 :: DN130; dn130 = undefined+dn131 :: DN131; dn131 = undefined+dn132 :: DN132; dn132 = undefined+dn133 :: DN133; dn133 = undefined+dn134 :: DN134; dn134 = undefined+dn135 :: DN135; dn135 = undefined+dn136 :: DN136; dn136 = undefined+dn137 :: DN137; dn137 = undefined+dn138 :: DN138; dn138 = undefined+dn139 :: DN139; dn139 = undefined+dn140 :: DN140; dn140 = undefined+dn141 :: DN141; dn141 = undefined+dn142 :: DN142; dn142 = undefined+dn143 :: DN143; dn143 = undefined+dn144 :: DN144; dn144 = undefined+dn145 :: DN145; dn145 = undefined+dn146 :: DN146; dn146 = undefined+dn147 :: DN147; dn147 = undefined+dn148 :: DN148; dn148 = undefined+dn149 :: DN149; dn149 = undefined+dn150 :: DN150; dn150 = undefined+dn151 :: DN151; dn151 = undefined+dn152 :: DN152; dn152 = undefined+dn153 :: DN153; dn153 = undefined+dn154 :: DN154; dn154 = undefined+dn155 :: DN155; dn155 = undefined+dn156 :: DN156; dn156 = undefined+dn157 :: DN157; dn157 = undefined+dn158 :: DN158; dn158 = undefined+dn159 :: DN159; dn159 = undefined+dn160 :: DN160; dn160 = undefined+dn161 :: DN161; dn161 = undefined+dn162 :: DN162; dn162 = undefined+dn163 :: DN163; dn163 = undefined+dn164 :: DN164; dn164 = undefined+dn165 :: DN165; dn165 = undefined+dn166 :: DN166; dn166 = undefined+dn167 :: DN167; dn167 = undefined+dn168 :: DN168; dn168 = undefined+dn169 :: DN169; dn169 = undefined+dn170 :: DN170; dn170 = undefined+dn171 :: DN171; dn171 = undefined+dn172 :: DN172; dn172 = undefined+dn173 :: DN173; dn173 = undefined+dn174 :: DN174; dn174 = undefined+dn175 :: DN175; dn175 = undefined+dn176 :: DN176; dn176 = undefined+dn177 :: DN177; dn177 = undefined+dn178 :: DN178; dn178 = undefined+dn179 :: DN179; dn179 = undefined+dn180 :: DN180; dn180 = undefined+dn181 :: DN181; dn181 = undefined+dn182 :: DN182; dn182 = undefined+dn183 :: DN183; dn183 = undefined+dn184 :: DN184; dn184 = undefined+dn185 :: DN185; dn185 = undefined+dn186 :: DN186; dn186 = undefined+dn187 :: DN187; dn187 = undefined+dn188 :: DN188; dn188 = undefined+dn189 :: DN189; dn189 = undefined+dn190 :: DN190; dn190 = undefined+dn191 :: DN191; dn191 = undefined+dn192 :: DN192; dn192 = undefined+dn193 :: DN193; dn193 = undefined+dn194 :: DN194; dn194 = undefined+dn195 :: DN195; dn195 = undefined+dn196 :: DN196; dn196 = undefined+dn197 :: DN197; dn197 = undefined+dn198 :: DN198; dn198 = undefined+dn199 :: DN199; dn199 = undefined+dn200 :: DN200; dn200 = undefined+dn201 :: DN201; dn201 = undefined+dn202 :: DN202; dn202 = undefined+dn203 :: DN203; dn203 = undefined+dn204 :: DN204; dn204 = undefined+dn205 :: DN205; dn205 = undefined+dn206 :: DN206; dn206 = undefined+dn207 :: DN207; dn207 = undefined+dn208 :: DN208; dn208 = undefined+dn209 :: DN209; dn209 = undefined+dn210 :: DN210; dn210 = undefined+dn211 :: DN211; dn211 = undefined+dn212 :: DN212; dn212 = undefined+dn213 :: DN213; dn213 = undefined+dn214 :: DN214; dn214 = undefined+dn215 :: DN215; dn215 = undefined+dn216 :: DN216; dn216 = undefined+dn217 :: DN217; dn217 = undefined+dn218 :: DN218; dn218 = undefined+dn219 :: DN219; dn219 = undefined+dn220 :: DN220; dn220 = undefined+dn221 :: DN221; dn221 = undefined+dn222 :: DN222; dn222 = undefined+dn223 :: DN223; dn223 = undefined+dn224 :: DN224; dn224 = undefined+dn225 :: DN225; dn225 = undefined+dn226 :: DN226; dn226 = undefined+dn227 :: DN227; dn227 = undefined+dn228 :: DN228; dn228 = undefined+dn229 :: DN229; dn229 = undefined+dn230 :: DN230; dn230 = undefined+dn231 :: DN231; dn231 = undefined+dn232 :: DN232; dn232 = undefined+dn233 :: DN233; dn233 = undefined+dn234 :: DN234; dn234 = undefined+dn235 :: DN235; dn235 = undefined+dn236 :: DN236; dn236 = undefined+dn237 :: DN237; dn237 = undefined+dn238 :: DN238; dn238 = undefined+dn239 :: DN239; dn239 = undefined+dn240 :: DN240; dn240 = undefined+dn241 :: DN241; dn241 = undefined+dn242 :: DN242; dn242 = undefined+dn243 :: DN243; dn243 = undefined+dn244 :: DN244; dn244 = undefined+dn245 :: DN245; dn245 = undefined+dn246 :: DN246; dn246 = undefined+dn247 :: DN247; dn247 = undefined+dn248 :: DN248; dn248 = undefined+dn249 :: DN249; dn249 = undefined+dn250 :: DN250; dn250 = undefined+dn251 :: DN251; dn251 = undefined+dn252 :: DN252; dn252 = undefined+dn253 :: DN253; dn253 = undefined+dn254 :: DN254; dn254 = undefined+dn255 :: DN255; dn255 = undefined+dn256 :: DN256; dn256 = undefined
+ src/Types/Data/Num/Decimal/Ops.hs view
@@ -0,0 +1,932 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Types.Data.Num.Decimal.Ops+-- Copyright   :  (c) 2008 Peter Gavin+-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  pgavin@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (type families, requires ghc >= 6.9)+--+-- Type-level numerical operations using type families.+-- +----------------------------------------------------------------------------++module Types.Data.Num.Decimal.Ops ()+    where++import Types.Base+import Types.Data.Bool+import Types.Data.Ord+import Types.Data.Num.Ops+import Types.Data.Num.Decimal.Literals (D1)+import Types.Data.Num.Decimal.Digits++instance IntegerR Decimal where+    reifyIntegral _ i k = reifyIntegral' i (\(_ :: s) -> k (undefined :: Dec s))++reifyIntegral' :: Integer -> (forall s. IntegerT' s => s -> w) -> w+reifyIntegral' n f | n <  0    = go (negate n) (\(_ :: s) -> f (undefined :: Neg' s)) +                   | otherwise = go n f+  where+   go :: Integer -> (forall s. IntegerT' s => s -> w) -> w+   go 0 k = k (undefined :: DecN)+   go i k = let (j, d) =  quotRem i 10 in case d of+     0 -> go j (\(_ :: s) -> k (undefined :: s :. Dec0))+     1 -> go j (\(_ :: s) -> k (undefined :: s :. Dec1))+     2 -> go j (\(_ :: s) -> k (undefined :: s :. Dec2))+     3 -> go j (\(_ :: s) -> k (undefined :: s :. Dec3))+     4 -> go j (\(_ :: s) -> k (undefined :: s :. Dec4))+     5 -> go j (\(_ :: s) -> k (undefined :: s :. Dec5))+     6 -> go j (\(_ :: s) -> k (undefined :: s :. Dec6))+     7 -> go j (\(_ :: s) -> k (undefined :: s :. Dec7))+     8 -> go j (\(_ :: s) -> k (undefined :: s :. Dec8))+     9 -> go j (\(_ :: s) -> k (undefined :: s :. Dec9))+     _ -> error "quotRem should always return a number from 0 to 9"++instance IntegerT' x => IntegerT (Dec x) where+    fromIntegerT _ = fromIntegerT' (undefined :: x)+    type Repr (Dec x) = Decimal++class IntegerT' x where+    fromIntegerT' :: Num y => x -> y+instance IntegerT' DecN where+    fromIntegerT' _ = 0+instance IntegerT' x => IntegerT' (Neg' x) where+    fromIntegerT' _ = negate (fromIntegerT' (undefined :: x))+instance IntegerT' xh => IntegerT' (xh :. Dec0) where+    fromIntegerT' _ = 0 + 10 * fromIntegerT' (undefined :: xh)+instance IntegerT' xh => IntegerT' (xh :. Dec1) where+    fromIntegerT' _ = 1 + 10 * fromIntegerT' (undefined :: xh)+instance IntegerT' xh => IntegerT' (xh :. Dec2) where+    fromIntegerT' _ = 2 + 10 * fromIntegerT' (undefined :: xh)+instance IntegerT' xh => IntegerT' (xh :. Dec3) where+    fromIntegerT' _ = 3 + 10 * fromIntegerT' (undefined :: xh)+instance IntegerT' xh => IntegerT' (xh :. Dec4) where+    fromIntegerT' _ = 4 + 10 * fromIntegerT' (undefined :: xh)+instance IntegerT' xh => IntegerT' (xh :. Dec5) where+    fromIntegerT' _ = 5 + 10 * fromIntegerT' (undefined :: xh)+instance IntegerT' xh => IntegerT' (xh :. Dec6) where+    fromIntegerT' _ = 6 + 10 * fromIntegerT' (undefined :: xh)+instance IntegerT' xh => IntegerT' (xh :. Dec7) where+    fromIntegerT' _ = 7 + 10 * fromIntegerT' (undefined :: xh)+instance IntegerT' xh => IntegerT' (xh :. Dec8) where+    fromIntegerT' _ = 8 + 10 * fromIntegerT' (undefined :: xh)+instance IntegerT' xh => IntegerT' (xh :. Dec9) where+    fromIntegerT' _ = 9 + 10 * fromIntegerT' (undefined :: xh)++type family Normalize x+type instance Normalize (Dec x) = Dec (Normalize' x)++type family Normalize' x+type instance Normalize' DecN       = DecN+type instance Normalize' (xh :. xl) = NormalizePos (xh :. xl)+type instance Normalize' (Neg' x)   = NormalizeNeg x++type family NormalizePos x+type instance NormalizePos x = NormalizePos' (ReverseDigits x)+type family NormalizePos' x+type instance NormalizePos' DecN         = DecN+type instance NormalizePos' (xh :. Dec0) = NormalizePos' xh+type instance NormalizePos' (xh :. Dec1) = ReverseDigits (xh :. Dec1)+type instance NormalizePos' (xh :. Dec2) = ReverseDigits (xh :. Dec2)+type instance NormalizePos' (xh :. Dec3) = ReverseDigits (xh :. Dec3)+type instance NormalizePos' (xh :. Dec4) = ReverseDigits (xh :. Dec4)+type instance NormalizePos' (xh :. Dec5) = ReverseDigits (xh :. Dec5)+type instance NormalizePos' (xh :. Dec6) = ReverseDigits (xh :. Dec6)+type instance NormalizePos' (xh :. Dec7) = ReverseDigits (xh :. Dec7)+type instance NormalizePos' (xh :. Dec8) = ReverseDigits (xh :. Dec8)+type instance NormalizePos' (xh :. Dec9) = ReverseDigits (xh :. Dec9)++type family ReverseDigits x+type instance ReverseDigits DecN       = DecN+type instance ReverseDigits (xh :. xl) = ReverseDigits' (xh :. xl) DecN++type family ReverseDigits' x y+type instance ReverseDigits' DecN y = y+type instance ReverseDigits' (xh :. xl) y = ReverseDigits' xh (y :. xl)++type family NormalizeNeg x+type instance NormalizeNeg (Neg' x)   = Normalize' x -- negate . negate == id+type instance NormalizeNeg DecN       = DecN         -- negate 0 = 0+type instance NormalizeNeg (xh :. xl) = NormalizeNeg' (NormalizePos (xh :. xl))++type family NormalizeNeg' x+type instance NormalizeNeg' DecN = DecN+type instance NormalizeNeg' (xh :. xl) = Neg' (xh :. xl)++-- type family IsPositive x+type instance IsPositive (Dec x) = IsPositive' x+type family IsPositive' x+type instance IsPositive' (Neg' x)   = False+type instance IsPositive' DecN       = False+type instance IsPositive' (xh :. xl) = True++-- type family IsZero x+type instance IsZero (Dec x) = IsZero' x+type family IsZero' x+type instance IsZero' (Neg' x)   = False+type instance IsZero' DecN       = True+type instance IsZero' (xh :. xl) = False++-- type family IsNegative x+type instance IsNegative (Dec x) = IsNegative' x+type family IsNegative' x+type instance IsNegative' (Neg' x)   = True+type instance IsNegative' DecN       = False+type instance IsNegative' (xh :. xl) = False++-- type family IsNatural x+type instance IsNatural (Dec x) = IsNatural' x+type family IsNatural' x+type instance IsNatural' (Neg' x)   = False+type instance IsNatural' DecN       = True+type instance IsNatural' (xh :. xl) = True++-- type family Neg x+type instance Neg (Dec DecN)     = Dec DecN+type instance Neg (Dec (Neg' x)) = Dec x+type instance Neg (Dec (xh :. xl)) = Dec (Neg' (xh :. xl))++-- type family Succ x+type instance Succ (Dec x) = Dec (Succ' x)++type family Succ' x+type instance Succ' (Neg' x   ) = Normalize' (Neg' (Pred'' x))+type instance Succ' (DecN     ) = DecN :. Dec1+type instance Succ' (x :. Dec0) = x :. Dec1+type instance Succ' (x :. Dec1) = x :. Dec2+type instance Succ' (x :. Dec2) = x :. Dec3+type instance Succ' (x :. Dec3) = x :. Dec4+type instance Succ' (x :. Dec4) = x :. Dec5+type instance Succ' (x :. Dec5) = x :. Dec6+type instance Succ' (x :. Dec6) = x :. Dec7+type instance Succ' (x :. Dec7) = x :. Dec8+type instance Succ' (x :. Dec8) = x :. Dec9+type instance Succ' (x :. Dec9) = Succ' x :. Dec0++-- type family Pred x+type instance Pred (Dec x)     = Dec (Pred' x)++type family Pred' x+type instance Pred' x = Normalize' (Pred'' x)+type family Pred'' x+type instance Pred'' (Neg' x   ) = Neg' (Succ' x)+type instance Pred'' (DecN     ) = Neg' (DecN :. Dec1)+type instance Pred'' (x :. Dec0) = Pred'' x :. Dec9+type instance Pred'' (x :. Dec1) = x :. Dec0+type instance Pred'' (x :. Dec2) = x :. Dec1+type instance Pred'' (x :. Dec3) = x :. Dec2+type instance Pred'' (x :. Dec4) = x :. Dec3+type instance Pred'' (x :. Dec5) = x :. Dec4+type instance Pred'' (x :. Dec6) = x :. Dec5+type instance Pred'' (x :. Dec7) = x :. Dec6+type instance Pred'' (x :. Dec8) = x :. Dec7+type instance Pred'' (x :. Dec9) = x :. Dec8++--------------------+-- Addition++type family AddDigit x y+-- putStr $ unlines $ concat $ [ [ "type instance AddDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x+y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]+type instance AddDigit Dec0 Dec0 = Dec0+type instance AddDigit Dec0 Dec1 = Dec1+type instance AddDigit Dec0 Dec2 = Dec2+type instance AddDigit Dec0 Dec3 = Dec3+type instance AddDigit Dec0 Dec4 = Dec4+type instance AddDigit Dec0 Dec5 = Dec5+type instance AddDigit Dec0 Dec6 = Dec6+type instance AddDigit Dec0 Dec7 = Dec7+type instance AddDigit Dec0 Dec8 = Dec8+type instance AddDigit Dec0 Dec9 = Dec9++type instance AddDigit Dec1 Dec0 = Dec1+type instance AddDigit Dec1 Dec1 = Dec2+type instance AddDigit Dec1 Dec2 = Dec3+type instance AddDigit Dec1 Dec3 = Dec4+type instance AddDigit Dec1 Dec4 = Dec5+type instance AddDigit Dec1 Dec5 = Dec6+type instance AddDigit Dec1 Dec6 = Dec7+type instance AddDigit Dec1 Dec7 = Dec8+type instance AddDigit Dec1 Dec8 = Dec9+type instance AddDigit Dec1 Dec9 = Dec0++type instance AddDigit Dec2 Dec0 = Dec2+type instance AddDigit Dec2 Dec1 = Dec3+type instance AddDigit Dec2 Dec2 = Dec4+type instance AddDigit Dec2 Dec3 = Dec5+type instance AddDigit Dec2 Dec4 = Dec6+type instance AddDigit Dec2 Dec5 = Dec7+type instance AddDigit Dec2 Dec6 = Dec8+type instance AddDigit Dec2 Dec7 = Dec9+type instance AddDigit Dec2 Dec8 = Dec0+type instance AddDigit Dec2 Dec9 = Dec1++type instance AddDigit Dec3 Dec0 = Dec3+type instance AddDigit Dec3 Dec1 = Dec4+type instance AddDigit Dec3 Dec2 = Dec5+type instance AddDigit Dec3 Dec3 = Dec6+type instance AddDigit Dec3 Dec4 = Dec7+type instance AddDigit Dec3 Dec5 = Dec8+type instance AddDigit Dec3 Dec6 = Dec9+type instance AddDigit Dec3 Dec7 = Dec0+type instance AddDigit Dec3 Dec8 = Dec1+type instance AddDigit Dec3 Dec9 = Dec2++type instance AddDigit Dec4 Dec0 = Dec4+type instance AddDigit Dec4 Dec1 = Dec5+type instance AddDigit Dec4 Dec2 = Dec6+type instance AddDigit Dec4 Dec3 = Dec7+type instance AddDigit Dec4 Dec4 = Dec8+type instance AddDigit Dec4 Dec5 = Dec9+type instance AddDigit Dec4 Dec6 = Dec0+type instance AddDigit Dec4 Dec7 = Dec1+type instance AddDigit Dec4 Dec8 = Dec2+type instance AddDigit Dec4 Dec9 = Dec3++type instance AddDigit Dec5 Dec0 = Dec5+type instance AddDigit Dec5 Dec1 = Dec6+type instance AddDigit Dec5 Dec2 = Dec7+type instance AddDigit Dec5 Dec3 = Dec8+type instance AddDigit Dec5 Dec4 = Dec9+type instance AddDigit Dec5 Dec5 = Dec0+type instance AddDigit Dec5 Dec6 = Dec1+type instance AddDigit Dec5 Dec7 = Dec2+type instance AddDigit Dec5 Dec8 = Dec3+type instance AddDigit Dec5 Dec9 = Dec4++type instance AddDigit Dec6 Dec0 = Dec6+type instance AddDigit Dec6 Dec1 = Dec7+type instance AddDigit Dec6 Dec2 = Dec8+type instance AddDigit Dec6 Dec3 = Dec9+type instance AddDigit Dec6 Dec4 = Dec0+type instance AddDigit Dec6 Dec5 = Dec1+type instance AddDigit Dec6 Dec6 = Dec2+type instance AddDigit Dec6 Dec7 = Dec3+type instance AddDigit Dec6 Dec8 = Dec4+type instance AddDigit Dec6 Dec9 = Dec5++type instance AddDigit Dec7 Dec0 = Dec7+type instance AddDigit Dec7 Dec1 = Dec8+type instance AddDigit Dec7 Dec2 = Dec9+type instance AddDigit Dec7 Dec3 = Dec0+type instance AddDigit Dec7 Dec4 = Dec1+type instance AddDigit Dec7 Dec5 = Dec2+type instance AddDigit Dec7 Dec6 = Dec3+type instance AddDigit Dec7 Dec7 = Dec4+type instance AddDigit Dec7 Dec8 = Dec5+type instance AddDigit Dec7 Dec9 = Dec6++type instance AddDigit Dec8 Dec0 = Dec8+type instance AddDigit Dec8 Dec1 = Dec9+type instance AddDigit Dec8 Dec2 = Dec0+type instance AddDigit Dec8 Dec3 = Dec1+type instance AddDigit Dec8 Dec4 = Dec2+type instance AddDigit Dec8 Dec5 = Dec3+type instance AddDigit Dec8 Dec6 = Dec4+type instance AddDigit Dec8 Dec7 = Dec5+type instance AddDigit Dec8 Dec8 = Dec6+type instance AddDigit Dec8 Dec9 = Dec7++type instance AddDigit Dec9 Dec0 = Dec9+type instance AddDigit Dec9 Dec1 = Dec0+type instance AddDigit Dec9 Dec2 = Dec1+type instance AddDigit Dec9 Dec3 = Dec2+type instance AddDigit Dec9 Dec4 = Dec3+type instance AddDigit Dec9 Dec5 = Dec4+type instance AddDigit Dec9 Dec6 = Dec5+type instance AddDigit Dec9 Dec7 = Dec6+type instance AddDigit Dec9 Dec8 = Dec7+type instance AddDigit Dec9 Dec9 = Dec8++-- | If adding @x@ and @y@ would not carry, then+--   @AddCarry x y z@ evaluates to @z@.  Otherwise,+--   @AddCarry x y z@ evaluates to @Succ' z@+type family AddCarry x y z+-- putStr $ unlines $ concat $ [ [ "type instance AddCarry Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x + y >= 10 then "Succ'" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]+type instance AddCarry Dec0 Dec0 x = Id x+type instance AddCarry Dec0 Dec1 x = Id x+type instance AddCarry Dec0 Dec2 x = Id x+type instance AddCarry Dec0 Dec3 x = Id x+type instance AddCarry Dec0 Dec4 x = Id x+type instance AddCarry Dec0 Dec5 x = Id x+type instance AddCarry Dec0 Dec6 x = Id x+type instance AddCarry Dec0 Dec7 x = Id x+type instance AddCarry Dec0 Dec8 x = Id x+type instance AddCarry Dec0 Dec9 x = Id x++type instance AddCarry Dec1 Dec0 x = Id x+type instance AddCarry Dec1 Dec1 x = Id x+type instance AddCarry Dec1 Dec2 x = Id x+type instance AddCarry Dec1 Dec3 x = Id x+type instance AddCarry Dec1 Dec4 x = Id x+type instance AddCarry Dec1 Dec5 x = Id x+type instance AddCarry Dec1 Dec6 x = Id x+type instance AddCarry Dec1 Dec7 x = Id x+type instance AddCarry Dec1 Dec8 x = Id x+type instance AddCarry Dec1 Dec9 x = Succ' x++type instance AddCarry Dec2 Dec0 x = Id x+type instance AddCarry Dec2 Dec1 x = Id x+type instance AddCarry Dec2 Dec2 x = Id x+type instance AddCarry Dec2 Dec3 x = Id x+type instance AddCarry Dec2 Dec4 x = Id x+type instance AddCarry Dec2 Dec5 x = Id x+type instance AddCarry Dec2 Dec6 x = Id x+type instance AddCarry Dec2 Dec7 x = Id x+type instance AddCarry Dec2 Dec8 x = Succ' x+type instance AddCarry Dec2 Dec9 x = Succ' x++type instance AddCarry Dec3 Dec0 x = Id x+type instance AddCarry Dec3 Dec1 x = Id x+type instance AddCarry Dec3 Dec2 x = Id x+type instance AddCarry Dec3 Dec3 x = Id x+type instance AddCarry Dec3 Dec4 x = Id x+type instance AddCarry Dec3 Dec5 x = Id x+type instance AddCarry Dec3 Dec6 x = Id x+type instance AddCarry Dec3 Dec7 x = Succ' x+type instance AddCarry Dec3 Dec8 x = Succ' x+type instance AddCarry Dec3 Dec9 x = Succ' x++type instance AddCarry Dec4 Dec0 x = Id x+type instance AddCarry Dec4 Dec1 x = Id x+type instance AddCarry Dec4 Dec2 x = Id x+type instance AddCarry Dec4 Dec3 x = Id x+type instance AddCarry Dec4 Dec4 x = Id x+type instance AddCarry Dec4 Dec5 x = Id x+type instance AddCarry Dec4 Dec6 x = Succ' x+type instance AddCarry Dec4 Dec7 x = Succ' x+type instance AddCarry Dec4 Dec8 x = Succ' x+type instance AddCarry Dec4 Dec9 x = Succ' x++type instance AddCarry Dec5 Dec0 x = Id x+type instance AddCarry Dec5 Dec1 x = Id x+type instance AddCarry Dec5 Dec2 x = Id x+type instance AddCarry Dec5 Dec3 x = Id x+type instance AddCarry Dec5 Dec4 x = Id x+type instance AddCarry Dec5 Dec5 x = Succ' x+type instance AddCarry Dec5 Dec6 x = Succ' x+type instance AddCarry Dec5 Dec7 x = Succ' x+type instance AddCarry Dec5 Dec8 x = Succ' x+type instance AddCarry Dec5 Dec9 x = Succ' x++type instance AddCarry Dec6 Dec0 x = Id x+type instance AddCarry Dec6 Dec1 x = Id x+type instance AddCarry Dec6 Dec2 x = Id x+type instance AddCarry Dec6 Dec3 x = Id x+type instance AddCarry Dec6 Dec4 x = Succ' x+type instance AddCarry Dec6 Dec5 x = Succ' x+type instance AddCarry Dec6 Dec6 x = Succ' x+type instance AddCarry Dec6 Dec7 x = Succ' x+type instance AddCarry Dec6 Dec8 x = Succ' x+type instance AddCarry Dec6 Dec9 x = Succ' x++type instance AddCarry Dec7 Dec0 x = Id x+type instance AddCarry Dec7 Dec1 x = Id x+type instance AddCarry Dec7 Dec2 x = Id x+type instance AddCarry Dec7 Dec3 x = Succ' x+type instance AddCarry Dec7 Dec4 x = Succ' x+type instance AddCarry Dec7 Dec5 x = Succ' x+type instance AddCarry Dec7 Dec6 x = Succ' x+type instance AddCarry Dec7 Dec7 x = Succ' x+type instance AddCarry Dec7 Dec8 x = Succ' x+type instance AddCarry Dec7 Dec9 x = Succ' x++type instance AddCarry Dec8 Dec0 x = Id x+type instance AddCarry Dec8 Dec1 x = Id x+type instance AddCarry Dec8 Dec2 x = Succ' x+type instance AddCarry Dec8 Dec3 x = Succ' x+type instance AddCarry Dec8 Dec4 x = Succ' x+type instance AddCarry Dec8 Dec5 x = Succ' x+type instance AddCarry Dec8 Dec6 x = Succ' x+type instance AddCarry Dec8 Dec7 x = Succ' x+type instance AddCarry Dec8 Dec8 x = Succ' x+type instance AddCarry Dec8 Dec9 x = Succ' x++type instance AddCarry Dec9 Dec0 x = Id x+type instance AddCarry Dec9 Dec1 x = Succ' x+type instance AddCarry Dec9 Dec2 x = Succ' x+type instance AddCarry Dec9 Dec3 x = Succ' x+type instance AddCarry Dec9 Dec4 x = Succ' x+type instance AddCarry Dec9 Dec5 x = Succ' x+type instance AddCarry Dec9 Dec6 x = Succ' x+type instance AddCarry Dec9 Dec7 x = Succ' x+type instance AddCarry Dec9 Dec8 x = Succ' x+type instance AddCarry Dec9 Dec9 x = Succ' x++-- type family x :+: y+type instance Dec x :+: Dec y = Dec (Add x y)++type family Add x y+type instance Add (DecN    ) (DecN    ) = DecN+type instance Add (xh :. xl) (DecN    ) = (xh :. xl)+type instance Add (DecN    ) (yh :. yl) = (yh :. yl)+type instance Add (Neg' x  ) (Neg' y  ) = Neg' (Add x y)+type instance Add (xh :. xl) (Neg' y  ) = Sub (xh :. xl) y+type instance Add (Neg' x  ) (yh :. yl) = Sub (yh :. yl) x+type instance Add (xh :. xl) (yh :. yl) = (AddCarry xl yl (Add xh yh)) :. (AddDigit xl yl)++--------------------+-- Subtraction++type family SubDigit x y+-- putStr $ unlines $ concat $ [ [ "type instance SubDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x-y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]+type instance SubDigit Dec0 Dec0 = Dec0+type instance SubDigit Dec0 Dec1 = Dec9+type instance SubDigit Dec0 Dec2 = Dec8+type instance SubDigit Dec0 Dec3 = Dec7+type instance SubDigit Dec0 Dec4 = Dec6+type instance SubDigit Dec0 Dec5 = Dec5+type instance SubDigit Dec0 Dec6 = Dec4+type instance SubDigit Dec0 Dec7 = Dec3+type instance SubDigit Dec0 Dec8 = Dec2+type instance SubDigit Dec0 Dec9 = Dec1++type instance SubDigit Dec1 Dec0 = Dec1+type instance SubDigit Dec1 Dec1 = Dec0+type instance SubDigit Dec1 Dec2 = Dec9+type instance SubDigit Dec1 Dec3 = Dec8+type instance SubDigit Dec1 Dec4 = Dec7+type instance SubDigit Dec1 Dec5 = Dec6+type instance SubDigit Dec1 Dec6 = Dec5+type instance SubDigit Dec1 Dec7 = Dec4+type instance SubDigit Dec1 Dec8 = Dec3+type instance SubDigit Dec1 Dec9 = Dec2++type instance SubDigit Dec2 Dec0 = Dec2+type instance SubDigit Dec2 Dec1 = Dec1+type instance SubDigit Dec2 Dec2 = Dec0+type instance SubDigit Dec2 Dec3 = Dec9+type instance SubDigit Dec2 Dec4 = Dec8+type instance SubDigit Dec2 Dec5 = Dec7+type instance SubDigit Dec2 Dec6 = Dec6+type instance SubDigit Dec2 Dec7 = Dec5+type instance SubDigit Dec2 Dec8 = Dec4+type instance SubDigit Dec2 Dec9 = Dec3++type instance SubDigit Dec3 Dec0 = Dec3+type instance SubDigit Dec3 Dec1 = Dec2+type instance SubDigit Dec3 Dec2 = Dec1+type instance SubDigit Dec3 Dec3 = Dec0+type instance SubDigit Dec3 Dec4 = Dec9+type instance SubDigit Dec3 Dec5 = Dec8+type instance SubDigit Dec3 Dec6 = Dec7+type instance SubDigit Dec3 Dec7 = Dec6+type instance SubDigit Dec3 Dec8 = Dec5+type instance SubDigit Dec3 Dec9 = Dec4++type instance SubDigit Dec4 Dec0 = Dec4+type instance SubDigit Dec4 Dec1 = Dec3+type instance SubDigit Dec4 Dec2 = Dec2+type instance SubDigit Dec4 Dec3 = Dec1+type instance SubDigit Dec4 Dec4 = Dec0+type instance SubDigit Dec4 Dec5 = Dec9+type instance SubDigit Dec4 Dec6 = Dec8+type instance SubDigit Dec4 Dec7 = Dec7+type instance SubDigit Dec4 Dec8 = Dec6+type instance SubDigit Dec4 Dec9 = Dec5++type instance SubDigit Dec5 Dec0 = Dec5+type instance SubDigit Dec5 Dec1 = Dec4+type instance SubDigit Dec5 Dec2 = Dec3+type instance SubDigit Dec5 Dec3 = Dec2+type instance SubDigit Dec5 Dec4 = Dec1+type instance SubDigit Dec5 Dec5 = Dec0+type instance SubDigit Dec5 Dec6 = Dec9+type instance SubDigit Dec5 Dec7 = Dec8+type instance SubDigit Dec5 Dec8 = Dec7+type instance SubDigit Dec5 Dec9 = Dec6++type instance SubDigit Dec6 Dec0 = Dec6+type instance SubDigit Dec6 Dec1 = Dec5+type instance SubDigit Dec6 Dec2 = Dec4+type instance SubDigit Dec6 Dec3 = Dec3+type instance SubDigit Dec6 Dec4 = Dec2+type instance SubDigit Dec6 Dec5 = Dec1+type instance SubDigit Dec6 Dec6 = Dec0+type instance SubDigit Dec6 Dec7 = Dec9+type instance SubDigit Dec6 Dec8 = Dec8+type instance SubDigit Dec6 Dec9 = Dec7++type instance SubDigit Dec7 Dec0 = Dec7+type instance SubDigit Dec7 Dec1 = Dec6+type instance SubDigit Dec7 Dec2 = Dec5+type instance SubDigit Dec7 Dec3 = Dec4+type instance SubDigit Dec7 Dec4 = Dec3+type instance SubDigit Dec7 Dec5 = Dec2+type instance SubDigit Dec7 Dec6 = Dec1+type instance SubDigit Dec7 Dec7 = Dec0+type instance SubDigit Dec7 Dec8 = Dec9+type instance SubDigit Dec7 Dec9 = Dec8++type instance SubDigit Dec8 Dec0 = Dec8+type instance SubDigit Dec8 Dec1 = Dec7+type instance SubDigit Dec8 Dec2 = Dec6+type instance SubDigit Dec8 Dec3 = Dec5+type instance SubDigit Dec8 Dec4 = Dec4+type instance SubDigit Dec8 Dec5 = Dec3+type instance SubDigit Dec8 Dec6 = Dec2+type instance SubDigit Dec8 Dec7 = Dec1+type instance SubDigit Dec8 Dec8 = Dec0+type instance SubDigit Dec8 Dec9 = Dec9++type instance SubDigit Dec9 Dec0 = Dec9+type instance SubDigit Dec9 Dec1 = Dec8+type instance SubDigit Dec9 Dec2 = Dec7+type instance SubDigit Dec9 Dec3 = Dec6+type instance SubDigit Dec9 Dec4 = Dec5+type instance SubDigit Dec9 Dec5 = Dec4+type instance SubDigit Dec9 Dec6 = Dec3+type instance SubDigit Dec9 Dec7 = Dec2+type instance SubDigit Dec9 Dec8 = Dec1+type instance SubDigit Dec9 Dec9 = Dec0++-- | If subtracting @y@ from @x@ would not borrow, then+--   @Borrow x y z@ evaluates to @z@.  Otherwise,+--   @Borrow x y z@ evaluates to @Pred' z@+type family Borrow x y z+-- putStr $ unlines $ concat $ [ [ "type instance Borrow Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x < y then "Pred'" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]+type instance Borrow Dec0 Dec0 x = Id x+type instance Borrow Dec0 Dec1 x = Pred' x+type instance Borrow Dec0 Dec2 x = Pred' x+type instance Borrow Dec0 Dec3 x = Pred' x+type instance Borrow Dec0 Dec4 x = Pred' x+type instance Borrow Dec0 Dec5 x = Pred' x+type instance Borrow Dec0 Dec6 x = Pred' x+type instance Borrow Dec0 Dec7 x = Pred' x+type instance Borrow Dec0 Dec8 x = Pred' x+type instance Borrow Dec0 Dec9 x = Pred' x++type instance Borrow Dec1 Dec0 x = Id x+type instance Borrow Dec1 Dec1 x = Id x+type instance Borrow Dec1 Dec2 x = Pred' x+type instance Borrow Dec1 Dec3 x = Pred' x+type instance Borrow Dec1 Dec4 x = Pred' x+type instance Borrow Dec1 Dec5 x = Pred' x+type instance Borrow Dec1 Dec6 x = Pred' x+type instance Borrow Dec1 Dec7 x = Pred' x+type instance Borrow Dec1 Dec8 x = Pred' x+type instance Borrow Dec1 Dec9 x = Pred' x++type instance Borrow Dec2 Dec0 x = Id x+type instance Borrow Dec2 Dec1 x = Id x+type instance Borrow Dec2 Dec2 x = Id x+type instance Borrow Dec2 Dec3 x = Pred' x+type instance Borrow Dec2 Dec4 x = Pred' x+type instance Borrow Dec2 Dec5 x = Pred' x+type instance Borrow Dec2 Dec6 x = Pred' x+type instance Borrow Dec2 Dec7 x = Pred' x+type instance Borrow Dec2 Dec8 x = Pred' x+type instance Borrow Dec2 Dec9 x = Pred' x++type instance Borrow Dec3 Dec0 x = Id x+type instance Borrow Dec3 Dec1 x = Id x+type instance Borrow Dec3 Dec2 x = Id x+type instance Borrow Dec3 Dec3 x = Id x+type instance Borrow Dec3 Dec4 x = Pred' x+type instance Borrow Dec3 Dec5 x = Pred' x+type instance Borrow Dec3 Dec6 x = Pred' x+type instance Borrow Dec3 Dec7 x = Pred' x+type instance Borrow Dec3 Dec8 x = Pred' x+type instance Borrow Dec3 Dec9 x = Pred' x++type instance Borrow Dec4 Dec0 x = Id x+type instance Borrow Dec4 Dec1 x = Id x+type instance Borrow Dec4 Dec2 x = Id x+type instance Borrow Dec4 Dec3 x = Id x+type instance Borrow Dec4 Dec4 x = Id x+type instance Borrow Dec4 Dec5 x = Pred' x+type instance Borrow Dec4 Dec6 x = Pred' x+type instance Borrow Dec4 Dec7 x = Pred' x+type instance Borrow Dec4 Dec8 x = Pred' x+type instance Borrow Dec4 Dec9 x = Pred' x++type instance Borrow Dec5 Dec0 x = Id x+type instance Borrow Dec5 Dec1 x = Id x+type instance Borrow Dec5 Dec2 x = Id x+type instance Borrow Dec5 Dec3 x = Id x+type instance Borrow Dec5 Dec4 x = Id x+type instance Borrow Dec5 Dec5 x = Id x+type instance Borrow Dec5 Dec6 x = Pred' x+type instance Borrow Dec5 Dec7 x = Pred' x+type instance Borrow Dec5 Dec8 x = Pred' x+type instance Borrow Dec5 Dec9 x = Pred' x++type instance Borrow Dec6 Dec0 x = Id x+type instance Borrow Dec6 Dec1 x = Id x+type instance Borrow Dec6 Dec2 x = Id x+type instance Borrow Dec6 Dec3 x = Id x+type instance Borrow Dec6 Dec4 x = Id x+type instance Borrow Dec6 Dec5 x = Id x+type instance Borrow Dec6 Dec6 x = Id x+type instance Borrow Dec6 Dec7 x = Pred' x+type instance Borrow Dec6 Dec8 x = Pred' x+type instance Borrow Dec6 Dec9 x = Pred' x++type instance Borrow Dec7 Dec0 x = Id x+type instance Borrow Dec7 Dec1 x = Id x+type instance Borrow Dec7 Dec2 x = Id x+type instance Borrow Dec7 Dec3 x = Id x+type instance Borrow Dec7 Dec4 x = Id x+type instance Borrow Dec7 Dec5 x = Id x+type instance Borrow Dec7 Dec6 x = Id x+type instance Borrow Dec7 Dec7 x = Id x+type instance Borrow Dec7 Dec8 x = Pred' x+type instance Borrow Dec7 Dec9 x = Pred' x++type instance Borrow Dec8 Dec0 x = Id x+type instance Borrow Dec8 Dec1 x = Id x+type instance Borrow Dec8 Dec2 x = Id x+type instance Borrow Dec8 Dec3 x = Id x+type instance Borrow Dec8 Dec4 x = Id x+type instance Borrow Dec8 Dec5 x = Id x+type instance Borrow Dec8 Dec6 x = Id x+type instance Borrow Dec8 Dec7 x = Id x+type instance Borrow Dec8 Dec8 x = Id x+type instance Borrow Dec8 Dec9 x = Pred' x++type instance Borrow Dec9 Dec0 x = Id x+type instance Borrow Dec9 Dec1 x = Id x+type instance Borrow Dec9 Dec2 x = Id x+type instance Borrow Dec9 Dec3 x = Id x+type instance Borrow Dec9 Dec4 x = Id x+type instance Borrow Dec9 Dec5 x = Id x+type instance Borrow Dec9 Dec6 x = Id x+type instance Borrow Dec9 Dec7 x = Id x+type instance Borrow Dec9 Dec8 x = Id x+type instance Borrow Dec9 Dec9 x = Id x++-- type family x :-: y+type instance Dec x :-: Dec y = Dec (Sub x y)++type family Sub x y+type instance Sub x y = Normalize' (Sub' x y)++type family Sub' x y+type instance Sub' (Neg' x  ) (Neg' y  ) = Sub' y x+type instance Sub' (Neg' x  ) (DecN    ) = Neg' x+type instance Sub' (Neg' x  ) (yh :. yl) = Neg' (Add x (yh :. yl))+type instance Sub' (DecN    ) (Neg' x  ) = x+type instance Sub' (DecN    ) (DecN    ) = DecN+type instance Sub' (DecN    ) (yh :. yl) = Neg' (yh :. yl)+type instance Sub' (xh :. xl) (Neg' y  ) = Add (xh :. xl) y+type instance Sub' (xh :. xl) (DecN    ) = xh :. xl+type instance Sub' (xh :. xl) (yh :. yl) = Sub'' (xh :. xl) (yh :. yl) (Compare' (xh :. xl) (yh :. yl))++type family Sub'' x y c+type instance Sub'' x y GT = SubPos x y DecN+type instance Sub'' x y EQ = DecN+type instance Sub'' x y LT = Neg' (SubPos y x DecN)++type family SubPos x y z+type instance SubPos (xh :. xl) (yh :. yl) z = SubPos (Borrow xl yl xh) yh (z :. SubDigit xl yl)+type instance SubPos (xh :. xl) DecN       z = SubPos xh DecN (z :. xl)+type instance SubPos DecN       DecN       z = ReverseDigits z++--------------------+-- Multiplication++-- type family Mul2 x+type instance Mul2 (Dec x) = Mul2' x+type family Mul2' x+type instance Mul2' x = Add x x++-- type family x :*: y+type instance (Dec x) :*: (Dec y) = Dec (Mul x y)++-- Peasant style+type family Mul x y+type instance Mul DecN       DecN       = DecN            -- 0 * 0 = 0+type instance Mul (xh :. xl) DecN       = DecN            -- x * 0 = 0+type instance Mul DecN       (yh :. yl) = DecN            -- 0 * x = 0+type instance Mul (Neg' x)   (Neg' y)   = Mul x y        -- -x * -y = x*y+type instance Mul (xh :. xl) (Neg' y)   = Neg' (Mul (xh :. xl) y)  -- x * -y = -(x*y)+type instance Mul (Neg' x)   (yh :. yl) = Neg' (Mul x (yh :. yl))  -- -x * y = -(x*y)+type instance Mul (xh :. xl) (yh :. yl) = Mul' (xh :. xl) (yh :. yl) DecN -- x & y positive++type family Mul' x y z+type instance Mul' x DecN       z = z+type instance Mul' x (yh :. yl) z = Mul' (Mul2' x) (Div2' (yh :. yl)) (If (IsEven' (yh :. yl)) z (Add z x))++-- type family Fac x+type instance Fac x = Fac' x (IsZero x)+type family Fac' x is0+type instance Fac' x True = D1+type instance Fac' x False = x :*: Fac (Pred x)++-----------+-- Division / Modulus++-- type family IsEven x+type instance IsEven (Dec x) = IsEven' x+type family IsEven' x+type instance IsEven' DecN = True+type instance IsEven' (Neg' x) = IsEven' x+type instance IsEven' (xh :. Dec0) = True+type instance IsEven' (xh :. Dec1) = False+type instance IsEven' (xh :. Dec2) = True+type instance IsEven' (xh :. Dec3) = False+type instance IsEven' (xh :. Dec4) = True+type instance IsEven' (xh :. Dec5) = False+type instance IsEven' (xh :. Dec6) = True+type instance IsEven' (xh :. Dec7) = False+type instance IsEven' (xh :. Dec8) = True+type instance IsEven' (xh :. Dec9) = False++-- type family Div2 x+type instance Div2 (Dec x) = Dec (Div2' x)++type family Div2Digit x+type instance Div2Digit Dec0 = Dec0+type instance Div2Digit Dec1 = Dec0+type instance Div2Digit Dec2 = Dec1+type instance Div2Digit Dec3 = Dec1+type instance Div2Digit Dec4 = Dec2+type instance Div2Digit Dec5 = Dec2+type instance Div2Digit Dec6 = Dec3+type instance Div2Digit Dec7 = Dec3+type instance Div2Digit Dec8 = Dec4+type instance Div2Digit Dec9 = Dec4++type family Div2' x+type instance Div2' DecN       = DecN+type instance Div2' (Neg' x)   = Neg' (Div2Pos x)+type instance Div2' (xh :. xl) = Div2Pos (xh :. xl)++type family Div2Pos x+type instance Div2Pos (xh :. xl) = Normalize' (Div2Pos' xh (Div2Digit xl) (If (IsEven' xh) Dec0 Dec5))++type family Div2Pos' xh xl' rem+type instance Div2Pos' xh xl' rem =+    (AddCarry xl' rem (Div2' xh)) :. (AddDigit xl' rem)++---------------+-- Exponentiation++type instance Pow2 (Dec x) = Dec (Pow2' x (DecN :. Dec1))++type family Pow2' x y+type instance Pow2' (Neg' x)   y = DecN+type instance Pow2' DecN       y = y+type instance Pow2' (xh :. xl) y = Pow2' (Pred' (xh :. xl)) (Mul2' y)++---------------+-- Logarithm+type instance Log2Ceil (Dec x) = Dec (Log2C' (Pred' x) DecN)++type family Log2C' x y+type instance Log2C' (Neg' x) y   = DecN+type instance Log2C' DecN     y   = y+type instance Log2C' (xh :. xl) y = Log2C' (Div2' (xh :. xl)) (Succ' y)++---------------+-- Compare++type family CompareDigit x y+-- putStr $ unlines $ concat $ [ [ "type instance CompareDigit Dec" ++ show x ++ " Dec" ++ show y ++ " = " ++ (if x < y then "LT" else (if x > y then "GT" else "EQ")) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]+type instance CompareDigit Dec0 Dec0 = EQ+type instance CompareDigit Dec0 Dec1 = LT+type instance CompareDigit Dec0 Dec2 = LT+type instance CompareDigit Dec0 Dec3 = LT+type instance CompareDigit Dec0 Dec4 = LT+type instance CompareDigit Dec0 Dec5 = LT+type instance CompareDigit Dec0 Dec6 = LT+type instance CompareDigit Dec0 Dec7 = LT+type instance CompareDigit Dec0 Dec8 = LT+type instance CompareDigit Dec0 Dec9 = LT++type instance CompareDigit Dec1 Dec0 = GT+type instance CompareDigit Dec1 Dec1 = EQ+type instance CompareDigit Dec1 Dec2 = LT+type instance CompareDigit Dec1 Dec3 = LT+type instance CompareDigit Dec1 Dec4 = LT+type instance CompareDigit Dec1 Dec5 = LT+type instance CompareDigit Dec1 Dec6 = LT+type instance CompareDigit Dec1 Dec7 = LT+type instance CompareDigit Dec1 Dec8 = LT+type instance CompareDigit Dec1 Dec9 = LT++type instance CompareDigit Dec2 Dec0 = GT+type instance CompareDigit Dec2 Dec1 = GT+type instance CompareDigit Dec2 Dec2 = EQ+type instance CompareDigit Dec2 Dec3 = LT+type instance CompareDigit Dec2 Dec4 = LT+type instance CompareDigit Dec2 Dec5 = LT+type instance CompareDigit Dec2 Dec6 = LT+type instance CompareDigit Dec2 Dec7 = LT+type instance CompareDigit Dec2 Dec8 = LT+type instance CompareDigit Dec2 Dec9 = LT++type instance CompareDigit Dec3 Dec0 = GT+type instance CompareDigit Dec3 Dec1 = GT+type instance CompareDigit Dec3 Dec2 = GT+type instance CompareDigit Dec3 Dec3 = EQ+type instance CompareDigit Dec3 Dec4 = LT+type instance CompareDigit Dec3 Dec5 = LT+type instance CompareDigit Dec3 Dec6 = LT+type instance CompareDigit Dec3 Dec7 = LT+type instance CompareDigit Dec3 Dec8 = LT+type instance CompareDigit Dec3 Dec9 = LT++type instance CompareDigit Dec4 Dec0 = GT+type instance CompareDigit Dec4 Dec1 = GT+type instance CompareDigit Dec4 Dec2 = GT+type instance CompareDigit Dec4 Dec3 = GT+type instance CompareDigit Dec4 Dec4 = EQ+type instance CompareDigit Dec4 Dec5 = LT+type instance CompareDigit Dec4 Dec6 = LT+type instance CompareDigit Dec4 Dec7 = LT+type instance CompareDigit Dec4 Dec8 = LT+type instance CompareDigit Dec4 Dec9 = LT++type instance CompareDigit Dec5 Dec0 = GT+type instance CompareDigit Dec5 Dec1 = GT+type instance CompareDigit Dec5 Dec2 = GT+type instance CompareDigit Dec5 Dec3 = GT+type instance CompareDigit Dec5 Dec4 = GT+type instance CompareDigit Dec5 Dec5 = EQ+type instance CompareDigit Dec5 Dec6 = LT+type instance CompareDigit Dec5 Dec7 = LT+type instance CompareDigit Dec5 Dec8 = LT+type instance CompareDigit Dec5 Dec9 = LT++type instance CompareDigit Dec6 Dec0 = GT+type instance CompareDigit Dec6 Dec1 = GT+type instance CompareDigit Dec6 Dec2 = GT+type instance CompareDigit Dec6 Dec3 = GT+type instance CompareDigit Dec6 Dec4 = GT+type instance CompareDigit Dec6 Dec5 = GT+type instance CompareDigit Dec6 Dec6 = EQ+type instance CompareDigit Dec6 Dec7 = LT+type instance CompareDigit Dec6 Dec8 = LT+type instance CompareDigit Dec6 Dec9 = LT++type instance CompareDigit Dec7 Dec0 = GT+type instance CompareDigit Dec7 Dec1 = GT+type instance CompareDigit Dec7 Dec2 = GT+type instance CompareDigit Dec7 Dec3 = GT+type instance CompareDigit Dec7 Dec4 = GT+type instance CompareDigit Dec7 Dec5 = GT+type instance CompareDigit Dec7 Dec6 = GT+type instance CompareDigit Dec7 Dec7 = EQ+type instance CompareDigit Dec7 Dec8 = LT+type instance CompareDigit Dec7 Dec9 = LT++type instance CompareDigit Dec8 Dec0 = GT+type instance CompareDigit Dec8 Dec1 = GT+type instance CompareDigit Dec8 Dec2 = GT+type instance CompareDigit Dec8 Dec3 = GT+type instance CompareDigit Dec8 Dec4 = GT+type instance CompareDigit Dec8 Dec5 = GT+type instance CompareDigit Dec8 Dec6 = GT+type instance CompareDigit Dec8 Dec7 = GT+type instance CompareDigit Dec8 Dec8 = EQ+type instance CompareDigit Dec8 Dec9 = LT++type instance CompareDigit Dec9 Dec0 = GT+type instance CompareDigit Dec9 Dec1 = GT+type instance CompareDigit Dec9 Dec2 = GT+type instance CompareDigit Dec9 Dec3 = GT+type instance CompareDigit Dec9 Dec4 = GT+type instance CompareDigit Dec9 Dec5 = GT+type instance CompareDigit Dec9 Dec6 = GT+type instance CompareDigit Dec9 Dec7 = GT+type instance CompareDigit Dec9 Dec8 = GT+type instance CompareDigit Dec9 Dec9 = EQ++type instance Compare (Dec x) (Dec y) = Compare' x y+type family Compare' x y+type instance Compare' (Neg' x)   (Neg' y)   = CompareNeg (ComparePos x y EQ)+type instance Compare' (Neg' x)   DecN       = LT+type instance Compare' (Neg' x)   (yh :. yl) = LT+type instance Compare' DecN       (Neg' y)   = GT+type instance Compare' DecN       DecN       = EQ+type instance Compare' DecN       (yh :. yl) = LT+type instance Compare' (xh :. xl) (Neg' y)   = GT+type instance Compare' (xh :. xl) DecN       = GT+type instance Compare' (xh :. xl) (yh :. yl) = ComparePos (xh :. xl) (yh :. yl) EQ++type family ComparePos x y c+type instance ComparePos DecN       DecN       c = c+type instance ComparePos DecN       (yh :. yl) c = LT+type instance ComparePos (xh :. xl) DecN       c = GT+type instance ComparePos (xh :. xl) (yh :. yl) GT = ComparePos' xh yh (CompareDigit xl yl) GT+type instance ComparePos (xh :. xl) (yh :. yl) EQ = ComparePos xh yh (CompareDigit xl yl)+type instance ComparePos (xh :. xl) (yh :. yl) LT = ComparePos' xh yh (CompareDigit xl yl) LT++type family ComparePos' x y c l+type instance ComparePos' x y LT c = ComparePos x y LT+type instance ComparePos' x y EQ c = ComparePos x y c+type instance ComparePos' x y GT c = ComparePos x y GT++type family CompareNeg c+type instance CompareNeg LT = GT+type instance CompareNeg EQ = EQ+type instance CompareNeg GT = LT
+ src/Types/Data/Num/Ops.hs view
@@ -0,0 +1,227 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Types.Data.Decimal.Ops+-- Copyright   :  (c) 2008 Peter Gavin+-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  pgavin@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (type families, requires ghc >= 6.9)+--+-- Type-level numerical operations using type families.+-- +----------------------------------------------------------------------------++module Types.Data.Num.Ops+    ( (:.)+    , Neg+    , negT+    , IsPositive+    , isPositiveT+    , IsZero+    , isZeroT+    , IsNegative+    , isNegativeT+    , IsNatural+    , isNaturalT+    , Succ+    , succT+    , Pred+    , predT+    , IsEven+    , isEvenT+    , IsOdd+    , isOddT+    , (:+:)+    , addT+    , (:-:)+    , subT+    , (:*:)+    , mulT+    , Mul2+    , mul2T+    , Pow2+    , pow2T+    , Log2Ceil+    , log2CeilT+    , DivMod+    , divModT+    , Div+    , divT+    , Mod+    , modT+    , Div2+    , div2T+    , Fac+    , facT+    , IntegerR (..)+    , IntegerT (..)+    , NaturalT+    , PositiveT+    , NegativeT+    , reifyPositive+    , reifyNegative+    , reifyNatural+    ) where++import Types.Data.Bool+++infixl 9 :.++data ds :. d+instance (Show ds, Show d) => Show (ds :. d) where+    show _ = show (undefined :: ds) ++ show (undefined :: d)++-- | @Neg x@ evaluates to the additive inverse of (i.e., minus) @x@.+type family Neg x+negT :: x -> Neg x+negT _ = undefined++type family IsPositive x+isPositiveT :: x -> IsPositive x+isPositiveT _ = undefined++type family IsZero x+isZeroT :: x -> IsZero x+isZeroT _ = undefined++type family IsNegative x+isNegativeT :: x -> IsNegative x+isNegativeT _ = undefined++type family IsNatural x+isNaturalT :: x -> IsNatural x+isNaturalT _ = undefined++type family Succ x+succT :: x -> Succ x+succT _ = undefined++type family Pred x+predT :: x -> Pred x+predT _ = undefined++type family IsEven x+isEvenT :: x -> IsEven x+isEvenT _ = undefined++type family IsOdd x+type instance IsOdd x = Not (IsEven x)+isOddT :: x -> IsOdd x+isOddT _ = undefined++type family x :+: y+addT :: x -> y -> x :+: y+addT _ _ = undefined++type family x :-: y+subT :: x -> y -> x :-: y+subT _ _ = undefined++type family x :*: y+mulT :: x -> y -> x :*: y+mulT _ _ = undefined++type family Mul2 x+mul2T :: x -> Mul2 x+mul2T _ = undefined++type family DivMod x y+divModT :: x -> y -> DivMod x y+divModT _ _ = undefined++type family Div x y+divT :: x -> y -> Div x y+divT _ _ = undefined++type family Mod x y+modT :: x -> y -> Mod x y+modT _ _ = undefined++type family Div2 x+div2T :: x -> Div2 x+div2T _ = undefined++type family Fac x+facT :: x -> Fac x+facT _ = undefined++type family Pow2 x+pow2T :: x -> Pow2 x+pow2T _ = undefined++type family Log2Ceil x+log2CeilT :: x -> Log2Ceil x+log2CeilT _ = undefined++class IntegerT x => NaturalT x+instance (IntegerT x, IsNatural x  ~ True) => NaturalT x+class IntegerT x => PositiveT x+instance (IntegerT x, IsPositive x ~ True) => PositiveT x+class IntegerT x => NegativeT x+instance (IntegerT x, IsNegative x ~ True) => NegativeT x++class (IntegerR (Repr x)) => IntegerT x where+    fromIntegerT :: Num y => x -> y+    type Repr x++class IntegerR r where+    reifyIntegral :: r -> Integer -> (forall s. (IntegerT s, Repr s ~ r) => s -> a) -> a+++--- positive and negative assertions: unsafe, in a trusted kernel+data AssertPos x+data AssertNeg x+data AssertNat x++assertPos :: x -> AssertPos x+assertPos _ = undefined++assertNeg :: x -> AssertNeg x+assertNeg _ = undefined++assertNat :: x -> AssertNat x+assertNat _ = undefined++type instance IsPositive (AssertPos x) = True+type instance IsPositive (AssertNeg x) = False++type instance IsNegative (AssertPos x) = False+type instance IsNegative (AssertNeg x) = True+type instance IsNegative (AssertNat x) = False++type instance IsNatural  (AssertPos x) = True+type instance IsNatural  (AssertNeg x) = False+type instance IsNatural  (AssertNat x) = True++instance IntegerT x => IntegerT (AssertPos x) where +    fromIntegerT _ = fromIntegerT (undefined :: x)+    type Repr (AssertPos x) = Repr x++instance IntegerT x => IntegerT (AssertNeg x) where+    fromIntegerT _ = fromIntegerT (undefined :: x)+    type Repr (AssertNeg x) = Repr x++instance IntegerT x => IntegerT (AssertNat x) where+    fromIntegerT _ = fromIntegerT (undefined :: x)+    type Repr (AssertNat x) = Repr x++reifyPositive :: IntegerR r => r -> Integer -> (forall s. (PositiveT s, Repr s ~ r) => s -> a) -> Maybe a+reifyPositive r n k | n > 0     = Just (reifyIntegral r n (k . assertPos))+                    | otherwise = Nothing++reifyNegative :: IntegerR r => r -> Integer -> (forall s. (NegativeT s, Repr s ~ r) => s -> a) -> Maybe a+reifyNegative r n k | n < 0     = Just (reifyIntegral r n (k . assertNeg))+                    | otherwise = Nothing+reifyNatural :: IntegerR r => r -> Integer -> (forall s. (NaturalT s, Repr s ~ r) => s -> a) -> Maybe a+reifyNatural r n k | n >= 0     = Just (reifyIntegral r n (k . assertNat))+                    | otherwise = Nothing
+ src/Types/Data/Ord.hs view
@@ -0,0 +1,154 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE UndecidableInstances #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  Types.Data.Decimal.Digits+-- Copyright   :  (c) 2008 Peter Gavin+-- License     :  BSD-style (see the file LICENSE)+-- +-- Maintainer  :  pgavin@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable (type families, requires ghc >= 6.9)+--+-- Type-level numerical operations using type families.+-- +----------------------------------------------------------------------------++module Types.Data.Ord+    ( Compare+    , compareT+    , LT+    , EQ+    , GT+    , IsLT+    , isLTT+    , IsEQ+    , isEQT+    , IsGT+    , isGTT+    , (:<:)+    , ltT+    , LTT+    , (:<=:)+    , leT+    , LET+    , (:==:)+    , eqT+    , EQT+    , (:/=:)+    , neT+    , NET+    , (:>=:)+    , geT+    , GET+    , (:>:)+    , gtT+    , GTT+    , Min+    , minT+    , Max+    , maxT+    ) where++import qualified Prelude++import Types.Data.Bool++type family Compare x y+data LT+data EQ+data GT+compareT :: x -> y -> Compare x y+compareT _ _ = Prelude.undefined++type family IsLT c+type instance IsLT LT = True+type instance IsLT EQ = False+type instance IsLT GT = False+isLTT :: c -> IsLT c+isLTT _ = Prelude.undefined++type family IsEQ c+type instance IsEQ LT = False+type instance IsEQ EQ = True+type instance IsEQ GT = False+isEQT :: c -> IsEQ c+isEQT _ = Prelude.undefined++type family IsGT c+type instance IsGT LT = False+type instance IsGT EQ = False+type instance IsGT GT = True+isGTT :: c -> IsGT c+isGTT _ = Prelude.undefined++type instance Compare LT LT = EQ+type instance Compare LT EQ = LT+type instance Compare LT GT = LT+type instance Compare EQ LT = GT+type instance Compare EQ EQ = EQ+type instance Compare EQ GT = LT+type instance Compare GT LT = GT+type instance Compare GT EQ = GT+type instance Compare GT GT = EQ++type family x :<: y+type instance x :<: y = IsLT (Compare x y)+ltT :: x -> y -> x :<: y+ltT _ _ = Prelude.undefined+class LTT x y+instance ((x :<: y) ~ True) => LTT x y++type family x :<=: y+type instance x :<=: y = Not (x :>: y)+leT :: x -> y -> x :<=: y+leT _ _ = Prelude.undefined+class LET x y+instance ((x :<=: y) ~ True) => LET x y++type family x :==: y+type instance x :==: y = IsEQ (Compare x y)+eqT :: x -> y -> x :==: y+eqT _ _ = Prelude.undefined+class EQT x y+instance ((x :==: y) ~ True) => EQT x y++type family x :/=: y+type instance x :/=: y = Not (x :==: y)+neT :: x -> y -> x :/=: y+neT _ _ = Prelude.undefined+class NET x y+instance ((x :/=: y) ~ True) => NET x y++type family x :>=: y+type instance x :>=: y = Not (x :<: y)+geT :: x -> y -> x :>=: y+geT _ _ = Prelude.undefined+class GET x y+instance ((x :>=: y) ~ True) => GET x y++type family x :>: y+type instance x :>: y = IsGT (Compare x y)+gtT :: x -> y -> x :>: y+gtT _ _ = Prelude.undefined+class GTT x y+instance ((x :>: y) ~ True) => GTT x y++type family Min x y+type instance Min x y = If (x :<=: y) x y+minT :: x -> y -> Min x y+minT _ _ = Prelude.undefined++type family Max x y+type instance Max x y = If (x :>=: y) x y+maxT :: x -> y -> Max x y+maxT _ _ = Prelude.undefined++type instance Compare False False = EQ+type instance Compare False True  = LT+type instance Compare True  False = GT+type instance Compare True  True  = EQ
+ test/Test.hs view
@@ -0,0 +1,267 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Main where++import qualified Test.QuickCheck as Q++import qualified Prelude+import Data.Char (intToDigit)+import Control.Monad (when)++import Types+++type D527 = DecPos3 Dec5 Dec2 Dec7+type D720 = DecPos3 Dec7 Dec2 Dec0+type D989 = DecPos3 Dec9 Dec8 Dec9+type D1000 = DecPos4 Dec1 Dec0 Dec0 Dec0+type D10000 = DecPos5 Dec1 Dec0 Dec0 Dec0 Dec0+type D3628800 = DecPos7 Dec3 Dec6 Dec2 Dec8 Dec8 Dec0 Dec0++testIsPositive1 :: IsPositive D1 -> True+testIsPositive1 = Prelude.id+testIsPositive2 :: IsPositive D0 -> False+testIsPositive2 = Prelude.id+testIsPositive3 :: IsPositive DN1 -> False+testIsPositive3 = Prelude.id+testIsPositive4 :: IsPositive D10 -> True+testIsPositive4 = Prelude.id+testIsPositive5 :: IsPositive DN10 -> False+testIsPositive5 = Prelude.id++testIsNegative1 :: IsNegative D1 -> False+testIsNegative1 = Prelude.id+testIsNegative2 :: IsNegative D0 -> False+testIsNegative2 = Prelude.id+testIsNegative3 :: IsNegative DN1 -> True+testIsNegative3 = Prelude.id+testIsNegative4 :: IsNegative D10 -> False+testIsNegative4 = Prelude.id+testIsNegative5 :: IsNegative DN10 -> True+testIsNegative5 = Prelude.id++testIsZero1 :: IsZero D1 -> False+testIsZero1 = Prelude.id+testIsZero2 :: IsZero D0 -> True+testIsZero2 = Prelude.id+testIsZero3 :: IsZero DN1 -> False+testIsZero3 = Prelude.id+testIsZero4 :: IsZero D10 -> False+testIsZero4 = Prelude.id+testIsZero5 :: IsZero DN10 -> False+testIsZero5 = Prelude.id++testSucc1 :: Succ D0 -> D1+testSucc1 = Prelude.id+testSucc2 :: Succ D9 -> D10+testSucc2 = Prelude.id+testSucc3 :: Succ DN1 -> D0+testSucc3 = Prelude.id+testSucc4 :: Succ D99 -> D100+testSucc4 = Prelude.id+testSucc5 :: Succ DN100 -> DN99+testSucc5 = Prelude.id+testSucc6 :: Succ D100 -> D101+testSucc6 = Prelude.id+testSucc7 :: Succ DN101 -> DN100+testSucc7 = Prelude.id+testSucc8 :: Succ D0 -> D1 :+: D0+testSucc8 = Prelude.id+testSucc9 :: Succ D0 -> D0 :+: D1+testSucc9 = Prelude.id+testSucc10 :: Succ D9 -> D1 :+: D9+testSucc10 = Prelude.id+testSucc11 :: Succ D9 -> D9 :+: D1+testSucc11 = Prelude.id++testPred1 :: Pred D1 -> D0+testPred1 = Prelude.id+testPred2 :: Pred D0 -> DN1+testPred2 = Prelude.id+testPred3 :: Pred DN1 -> DN2+testPred3 = Prelude.id+testPred4 :: Pred DN9 -> DN10+testPred4 = Prelude.id+testPred5 :: Pred D10 -> D9+testPred5 = Prelude.id+testPred6 :: Pred DN99 -> DN100+testPred6 = Prelude.id+testPred7 :: Pred D100 -> D99+testPred7 = Prelude.id+testPred8 :: Pred D0 -> D0 :-: D1+testPred8 = Prelude.id+testPred9 :: Pred D10 -> D10 :-: D1+testPred9 = Prelude.id+testPred10 :: Pred D9 -> D8+testPred10 = Prelude.id+testPred11 :: Pred D8 -> D7+testPred11 = Prelude.id+testPred12 :: Pred D7 -> D6+testPred12 = Prelude.id+testPred13 :: Pred D6 -> D5+testPred13 = Prelude.id+testPred14 :: Pred D5 -> D4+testPred14 = Prelude.id+testPred15 :: Pred D4 -> D3+testPred15 = Prelude.id+testPred16 :: Pred D3 -> D2+testPred16 = Prelude.id+testPred17 :: Pred D2 -> D1+testPred17 = Prelude.id+testPred18 :: Pred D1 -> D0+testPred18 = Prelude.id++testAdd1 :: D0 :+: D0 -> D0+testAdd1 = Prelude.id+testAdd2 :: DN1 :+: D1 -> D0+testAdd2 = Prelude.id+testAdd3 :: D1 :+: DN1 -> D0+testAdd3 = Prelude.id+testAdd4 :: D1 :+: D1 -> D2+testAdd4 = Prelude.id+testAdd5 :: D9 :+: D1 -> D10+testAdd5 = Prelude.id+testAdd6 :: D10 :+: DN1 -> D9+testAdd6 = Prelude.id+testAdd7 :: D100 :+: DN1 -> D99+testAdd7 = Prelude.id+testAdd8 :: D100 :+: DN10 -> D90+testAdd8 = Prelude.id++testSub1 :: D0 :-: D0 -> D0+testSub1 = Prelude.id+testSub2 :: D1 :-: D0 -> D1+testSub2 = Prelude.id+testSub3 :: D0 :-: D1 -> DN1+testSub3 = Prelude.id+testSub4 :: DN1 :-: D0 -> DN1+testSub4 = Prelude.id+testSub5 :: D0 :-: DN1 -> D1+testSub5 = Prelude.id+testSub6 :: D100 :-: D1 -> D99+testSub6 = Prelude.id+testSub7 :: DN100 :-: D1 -> DN101+testSub7 = Prelude.id+testSub8 :: D100 :-: DN1 -> D101+testSub8 = Prelude.id+testSub9 :: DN100 :-: DN1 -> DN99+testSub9 = Prelude.id+testSub10 :: D1 :-: D100 -> DN99+testSub10 = Prelude.id+testSub11 :: DN1 :-: D100 -> DN101+testSub11 = Prelude.id+testSub12 :: D1 :-: DN100 -> D101+testSub12 = Prelude.id+testSub13 :: DN1 :-: DN100 -> D99+testSub13 = Prelude.id+testSub14 :: D57 :-: D58 -> DN1+testSub14 = Prelude.id+testSub15 :: D1000 :-: D11 -> D989+testSub15 = Prelude.id++testMul1 :: D0 :*: D0 -> D0+testMul1 = Prelude.id+testMul2 :: D1 :*: D1 -> D1+testMul2 = Prelude.id+testMul3 :: D0 :*: D1 -> D0+testMul3 = Prelude.id+testMul4 :: D1 :*: D0 -> D0+testMul4 = Prelude.id+testMul5 :: D1 :*: DN1 -> DN1+testMul5 = Prelude.id+testMul6 :: DN1 :*: D1 -> DN1+testMul6 = Prelude.id+testMul7 :: DN1 :*: DN1 -> D1+testMul7 = Prelude.id+testMul8 :: D100 :*: D100 -> D10000+testMul8 = Prelude.id+testMul9 :: D17 :*: D31 -> D527+testMul9 = Prelude.id++testFac1 :: Fac D0 -> D1+testFac1 = Prelude.id+testFac2 :: Fac D1 -> D1+testFac2 = Prelude.id+testFac3 :: Fac D6 -> D720+testFac3 = Prelude.id+testFac4 :: Fac D10 -> D3628800+testFac4 = Prelude.id++testEQ1 :: D0 :==: D0 -> True+testEQ1 = Prelude.id+testEQ2 :: D0 :==: Pred D1 -> True+testEQ2 = Prelude.id+testEQ3 :: (D1 :+: D9) :==: D10 -> True+testEQ3 = Prelude.id+testEQ4 :: (D1 :+: D9) :==: D11 -> False+testEQ4 = Prelude.id+testEQ5 :: D9 :==: D0 -> False+testEQ5 = Prelude.id+testEQ6 :: D8 :==: D0 -> False+testEQ6 = Prelude.id+testEQ7 :: D7 :==: D0 -> False+testEQ7 = Prelude.id+testEQ8 :: D6 :==: D0 -> False+testEQ8 = Prelude.id+testEQ9 :: D5 :==: D0 -> False+testEQ9 = Prelude.id+testEQ10 :: D4 :==: D0 -> False+testEQ10 = Prelude.id+testEQ11 :: D3 :==: D0 -> False+testEQ11 = Prelude.id+testEQ12 :: D2 :==: D0 -> False+testEQ12 = Prelude.id+testEQ13 :: D1 :==: D0 -> False+testEQ13 = Prelude.id++testMin1 :: Min D0 D5 -> D0+testMin1 = Prelude.id+testMin2 :: Min D5 D0 -> D0+testMin2 = Prelude.id+testMin3 :: Min DN5 D5 -> DN5+testMin3 = Prelude.id++testMax1 :: Max D1 D6 -> D6+testMax1 = Prelude.id+testMax2 :: Max DN6 D6 -> D6+testMax2 = Prelude.id+testMax3 :: Max D6 D1 -> D6+testMax3 = Prelude.id++testLog1 :: Log2Ceil D8 -> D3+testLog1 = Prelude.id+testLog2 :: Log2Ceil D9 -> D4+testLog2 = Prelude.id+testLog3 :: Log2Ceil D2 -> D1+testLog3 = Prelude.id+testLog4 :: Log2Ceil D1 -> D0+testLog4 = Prelude.id++class TestIter n zero where+    testIter :: n -> zero -> Prelude.String++instance ( NaturalT n+         , (n :==: D0) ~ True )+  => TestIter n True where+    testIter _ _ = ""++instance ( NaturalT n+         , (n :==: D0) ~ False+         , TestIter (Pred n) ((Pred n) :==: D0) )+  => TestIter n False where+    testIter n _ =+        intToDigit (fromIntegerT n) : testIter (_T :: (Pred n)) (_T :: ((Pred n) :==: D0))++main :: Prelude.IO ()+main = do+  let testIterResult = testIter d9 (_T :: False)+  when (testIterResult Prelude./= "987654321") (Prelude.putStrLn ("testIter failed, got: " Prelude.++ testIterResult))+  Q.quickCheck prop_reifyIntegral++prop_reifyIntegral :: Prelude.Integer -> Prelude.Bool+prop_reifyIntegral i = reifyIntegral (Prelude.undefined :: Decimal) i fromIntegerT Prelude.== i
tfp.cabal view
@@ -1,5 +1,5 @@ name:           tfp-version:        0.7+version:        0.8 build-type:     Simple license:        BSD3 license-file:   LICENSE@@ -17,15 +17,15 @@   which provides an intuitive way to parameterize data types   and functions on numerical values at compile time. category:       Type System-tested-with:    GHC == 7.4.2-cabal-version:  >= 1.6+tested-with:    GHC == 7.4.2, GHC == 7.6.3+cabal-version:  >= 1.14  source-repository head   type:         darcs   location:     http://code.haskell.org/~thielema/tfp/  source-repository this-  tag:          0.7+  tag:          0.8   type:         darcs   location:     http://code.haskell.org/~thielema/tfp/ @@ -35,12 +35,10 @@   default: False  library {-  extensions:     TypeFamilies, UndecidableInstances, TypeOperators,-                  EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,-                  FlexibleInstances, TemplateHaskell, TypeSynonymInstances,-                  MultiParamTypeClasses, GeneralizedNewtypeDeriving,-                  Rank2Types, FlexibleContexts-  build-depends:  base >= 3.0 && < 5, template-haskell >= 2.0+  default-language: Haskell2010+  build-depends:  base >= 3.0 && < 5+  ghc-options:    -Wall+  hs-source-dirs: src   exposed-modules:     Data.SizedInt     Data.SizedWord@@ -51,7 +49,6 @@     Types.Data.Num.Ops     Types.Data.Num.Decimal     Types.Data.Num.Decimal.Literals-    Types.Data.Num.Decimal.Literals.TH     Types.Data.Num.Decimal.Digits     Types.Data.List     Types.Data.Ord@@ -63,14 +60,15 @@ executable tfp-test {   if flag(build-test) {     buildable: True-    build-depends:  base >= 3.0 && < 5, template-haskell >= 2.0, QuickCheck >= 1.2.0.0+    build-depends:+      tfp,+      QuickCheck >= 1.2.0.0,+      base >= 3.0 && < 5   } else {     buildable: False   }-  extensions:     TypeFamilies, UndecidableInstances, TypeOperators,-                  EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,-                  FlexibleInstances, TemplateHaskell, TypeSynonymInstances,-                  MultiParamTypeClasses, GeneralizedNewtypeDeriving,-                  FunctionalDependencies, Rank2Types, FlexibleContexts+  default-language: Haskell2010+  ghc-options:    -Wall   main-is: Test.hs+  hs-source-dirs: test }