tfp (empty) → 0.1
raw patch · 18 files changed
+1964/−0 lines, 18 filesdep +basedep +template-haskellsetup-changed
Dependencies added: base, template-haskell
Files
- Data/SizedInt.hs +157/−0
- Data/SizedWord.hs +133/−0
- LICENSE +25/−0
- Setup.hs +2/−0
- Test.hs +155/−0
- Types.hs +13/−0
- Types/Base.hs +24/−0
- Types/Data/Bool.hs +70/−0
- Types/Data/List.hs +47/−0
- Types/Data/Num.hs +21/−0
- Types/Data/Num/Decimal.hs +9/−0
- Types/Data/Num/Decimal/Digits.hs +61/−0
- Types/Data/Num/Decimal/Literals.hs +8/−0
- Types/Data/Num/Decimal/Literals/TH.hs +30/−0
- Types/Data/Num/Decimal/Ops.hs +886/−0
- Types/Data/Num/Ops.hs +148/−0
- Types/Data/Ord.hs +114/−0
- tfp.cabal +61/−0
+ Data/SizedInt.hs view
@@ -0,0 +1,157 @@+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 view
@@ -0,0 +1,133 @@+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
+ LICENSE view
@@ -0,0 +1,25 @@+Copyright (c) 2008 Peter Gavin+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:+ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+ * Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.+ * Neither the name of the copyright holder nor the+ names of its contributors may be used to endorse or promote products+ derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDER ``AS IS'' AND ANY+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR+PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER BE+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR+BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,+WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE+OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN+IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Test.hs view
@@ -0,0 +1,155 @@+module Main where++import qualified Prelude++import Types.Data.Ord+import Types.Data.Num+import Types.Data.Num.Decimal.Literals.TH+import Types.Data.Bool+import Data.SizedWord++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++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++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++f :: n -> (n :+: D5)+f _ = Prelude.undefined++main :: Prelude.IO ()+main = Prelude.return ()
+ 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
+ Types/Base.hs view
@@ -0,0 +1,24 @@+-----------------------------------------------------------------------------+-- |+-- 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 view
@@ -0,0 +1,70 @@+-----------------------------------------------------------------------------+-- |+-- 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 :&&: x+andT _ _ = Prelude.undefined++type family x :||: y+type instance True :||: x = True+type instance False :||: x = x+orT :: x -> y -> x :||: x+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 view
@@ -0,0 +1,47 @@+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 view
@@ -0,0 +1,21 @@+-----------------------------------------------------------------------------+-- |+-- 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+ ) where++import Types.Data.Num.Ops+import Types.Data.Num.Decimal
+ Types/Data/Num/Decimal.hs view
@@ -0,0 +1,9 @@+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 view
@@ -0,0 +1,61 @@+-----------------------------------------------------------------------------+-- |+-- 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++-- | 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 view
@@ -0,0 +1,8 @@+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 view
@@ -0,0 +1,30 @@+module Types.Data.Num.Decimal.Literals.TH where++import Language.Haskell.TH++decLiteralT :: Integer -> Q Type+decLiteralT n = appT (conT (mkName "Dec")) (decLiteralT' n)+ where decLiteralT' n | n < 0 = appT (conT (mkName "Neg'")) (decLiteralT' (-n))+ | n == 0 = conT (mkName "DecN")+ | otherwise = appT (appT (conT (mkName ":.")) (decLiteralT' (n `div` 10))) (conT (mkName ("Dec" ++ show (n `mod` 10))))++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 view
@@ -0,0 +1,886 @@+-----------------------------------------------------------------------------+-- |+-- 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 IntegerT' x => IntegerT (Dec x) where+ fromIntegerT _ = fromIntegerT' (undefined :: x)++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 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)++---------------+-- 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 view
@@ -0,0 +1,148 @@+-----------------------------------------------------------------------------+-- |+-- 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+ , Succ+ , succT+ , Pred+ , predT+ , IsEven+ , isEvenT+ , IsOdd+ , isOddT+ , (:+:)+ , addT+ , (:-:)+ , subT+ , (:*:)+ , mulT+ , Mul2+ , mul2T+ , Pow2+ , pow2T+ , DivMod+ , divModT+ , Div+ , divT+ , Mod+ , modT+ , Div2+ , div2T+ , Fac+ , facT+ , IntegerT (..)+ , NaturalT+ , PositiveT+ , NegativeT+ ) 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 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++class IntegerT x => NaturalT x+instance (IntegerT x, IsNegative x ~ False) => 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 IntegerT x where+ fromIntegerT :: Num y => x -> y
+ Types/Data/Ord.hs view
@@ -0,0 +1,114 @@+-----------------------------------------------------------------------------+-- |+-- 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+ , (:<=:)+ , leT+ , (:==:)+ , eqT+ , (:>=:)+ , geT+ , (:>:)+ , gtT+ ) 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++type family x :<=: y+type instance x :<=: y = Not (x :>: y)+leT :: x -> y -> x :<=: y+leT _ _ = Prelude.undefined++type family x :==: y+type instance x :==: y = IsEQ (Compare x y)+eqT :: x -> y -> x :==: y+eqT _ _ = Prelude.undefined++type family x :/=: y+type instance x :/=: y = Not (x :==: y)+neT :: x -> y -> x :/=: y+neT _ _ = Prelude.undefined++type family x :>=: y+type instance x :>=: y = Not (x :<: y)+geT :: x -> y -> x :>=: y+geT _ _ = Prelude.undefined++type family x :>: y+type instance x :>: y = IsGT (Compare x y)+gtT :: x -> y -> x :>: y+gtT _ _ = 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
+ tfp.cabal view
@@ -0,0 +1,61 @@+name: tfp+version: 0.1+cabal-version: >= 1.2+build-type: Simple+license: BSD3+license-file: LICENSE+copyright: Copyright (c) 2008 Peter Gavin+author: Peter Gavin+maintainer: pgavin@gmail.com+homepage: http://code.haskell.org/~pgavin/tfp+stability: alpha+package-url: http://code.haskell.org/~pgavin/tfp+synopsis: Type-level programming library using type families+description: TFP (short for Type Family Programming) provides implementations of type-level integers and booleans,+ and (eventually) simple type-level data structures. It uses type families as functions to produce new types,+ which provides an intuitive way to parameterize data types and functions on numerical values at compile time.+category: Data+tested-with: GHC == 6.9.0++flag build-test+ description: Build the tfp-test test program+ default: False++library {+ extensions: TypeFamilies, UndecidableInstances, TypeOperators,+ EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,+ FlexibleInstances, TemplateHaskell, TypeSynonymInstances,+ MultiParamTypeClasses, GeneralizedNewtypeDeriving+ build-depends: base >= 3.0, template-haskell >= 2.0+ exposed-modules:+ Data.SizedInt,+ Data.SizedWord,+ Types,+ Types.Base,+ Types.Data.Bool,+ Types.Data.Num+ 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+ other-modules:+ Types.Data.Num.Decimal.Ops+}+++executable tfp-test {+ if flag(build-test) {+ buildable: True+ } else {+ buildable: False+ }+ extensions: TypeFamilies, UndecidableInstances, TypeOperators,+ EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,+ FlexibleInstances, TemplateHaskell, TypeSynonymInstances,+ MultiParamTypeClasses, GeneralizedNewtypeDeriving+ main-is: Test.hs+ build-depends: base >= 3.0, template-haskell >= 2.0+}