tfp 0.3 → 1.0.2
raw patch · 35 files changed
Files
- Changes.md +19/−0
- Data/SizedInt.hs +0/−157
- Data/SizedWord.hs +0/−133
- LICENSE +1/−0
- Test.hs +0/−243
- Types.hs +0/−13
- Types/Base.hs +0/−24
- Types/Data/Bool.hs +0/−70
- Types/Data/List.hs +0/−47
- Types/Data/Num.hs +0/−28
- Types/Data/Num/Decimal.hs +0/−9
- Types/Data/Num/Decimal/Digits.hs +0/−65
- Types/Data/Num/Decimal/Literals.hs +0/−8
- Types/Data/Num/Decimal/Literals/TH.hs +0/−46
- Types/Data/Num/Decimal/Ops.hs +0/−908
- Types/Data/Num/Ops.hs +0/−185
- Types/Data/Ord.hs +0/−128
- src/Data/SizedInt.hs +178/−0
- src/Data/SizedWord.hs +155/−0
- src/Type/Base/Proxy.hs +24/−0
- src/Type/Data/Bool.hs +76/−0
- src/Type/Data/List.hs +52/−0
- src/Type/Data/Num.hs +267/−0
- src/Type/Data/Num/Decimal.hs +7/−0
- src/Type/Data/Num/Decimal/Digit.hs +140/−0
- src/Type/Data/Num/Decimal/Digit/Proof.hs +69/−0
- src/Type/Data/Num/Decimal/Literal.hs +1061/−0
- src/Type/Data/Num/Decimal/Number.hs +1516/−0
- src/Type/Data/Num/Decimal/Proof.hs +89/−0
- src/Type/Data/Num/Unary.hs +147/−0
- src/Type/Data/Num/Unary/Literal.hs +138/−0
- src/Type/Data/Num/Unary/Proof.hs +167/−0
- src/Type/Data/Ord.hs +135/−0
- test/Test.hs +369/−0
- tfp.cabal +59/−53
+ Changes.md view
@@ -0,0 +1,19 @@+1.0:++* Change representation of decimals to an inherently normalized form+ that is symmetric with respect to positive and negative numbers.++* singularize module names++* separate Decimal and general representation++* use Proxys instead of plain types for data functions+ This is also consistent with new Nat kind,+ where types of kind Nat have no data values.++* Ord: make infix operators classes and prefix functions type functions+ It seems to be more natural to me to write+ x :<: y and GTT x y ~ True++* Num, Bool, Ord: remove T suffixes from functions+ Use qualification instead.
− 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
LICENSE view
@@ -1,3 +1,4 @@+Copyright (c) 2013 Henning Thielemann Copyright (c) 2008 Peter Gavin All rights reserved.
− Test.hs
@@ -1,243 +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--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,28 +0,0 @@--------------------------------------------------------------------------------- |--- 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- , reifyIntegralD- , reifyPositiveD- , reifyNegativeD- ) where--import Types.Data.Num.Ops-import Types.Data.Num.Decimal--reifyIntegralD = reifyIntegral decimal-reifyPositiveD = reifyPositive decimal-reifyNegativeD = reifyNegative decimal
− 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,908 +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 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
@@ -1,185 +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- , 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- , IntegerR (..)- , IntegerT (..)- , NaturalT- , PositiveT- , NegativeT- , reifyPositive- , reifyNegative- ) 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 (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--assertPos :: x -> AssertPos x-assertPos _ = undefined--assertNeg :: x -> AssertNeg x-assertNeg _ = undefined--type instance IsPositive (AssertPos x) = True-type instance IsNegative (AssertNeg 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--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
− Types/Data/Ord.hs
@@ -1,128 +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- , (:<=:)- , leT- , (:==:)- , eqT- , (:>=:)- , geT- , (:>:)- , 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--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 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,178 @@+{-# 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 qualified Type.Data.Num as Num+import Type.Base.Proxy (Proxy(Proxy))+++newtype SizedInt nT = SizedInt Integer++_sizeT :: SizedInt nT -> Proxy nT+_sizeT _ = Proxy++mask :: forall nT . Num.Natural nT => Proxy nT -> Integer+mask n = bit (Num.fromInteger n) - 1++signBit :: forall nT . Num.Natural nT => Proxy nT -> Int+signBit n = Num.fromInteger n - 1++isNegative :: forall nT . Num.Natural nT+ => SizedInt nT+ -> Bool+isNegative (SizedInt x) =+ testBit x $ signBit (Proxy :: Proxy nT)++instance Num.Natural nT => Eq (SizedInt nT) where+ (SizedInt x) == (SizedInt y) = x == y+ (SizedInt x) /= (SizedInt y) = x /= y++instance Num.Natural nT => Show (SizedInt nT) where+ showsPrec prec n =+ showsPrec prec $ toInteger n++instance Num.Natural nT => Read (SizedInt nT) where+ readsPrec prec str0 =+ [ (fromInteger n, str)+ | (n, str) <- readsPrec prec str0 ]++instance Num.Natural nT => Ord (SizedInt nT) where+ a `compare` b = toInteger a `compare` toInteger b++instance Num.Natural nT => Bounded (SizedInt nT) where+ minBound = SizedInt $ negate $ 1 `shiftL` (Num.fromInteger (Proxy :: Proxy nT) - 1)+ maxBound = SizedInt $ (1 `shiftL` (Num.fromInteger (Proxy :: Proxy nT) - 1)) - 1++instance Num.Natural 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{" ++ showSizedIntTypeProxy n ++ "}: tried to take `fromEnum' on SizedInt greater than maxBound :: " ++ showSizedIntTypeProxy n+ | x' < toInteger (minBound :: SizedInt nT) =+ error $ "Enum.fromEnum{" ++ showSizedIntTypeProxy n ++ "}: tried to take `fromEnum' on SizedInt smaller than minBound :: " ++ showSizedIntTypeProxy n+ | otherwise =+ fromInteger x'+ where x' = toInteger x+ n = Proxy :: Proxy nT++instance Num.Natural 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 (Proxy :: Proxy nT)) + 1+ a - b =+ a + (negate b)++ fromInteger n =+ let fromCardinal m = SizedInt $ m .&. mask (Proxy :: Proxy 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 Num.Natural nT => Real (SizedInt nT) where+ toRational n = toRational $ toInteger n++instance Num.Natural 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 Num.Natural 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 (Proxy :: Proxy 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 (Proxy :: Proxy 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 (Proxy :: Proxy nT) .&.+ ((x `shiftR` b) .|. (mask (Proxy :: Proxy nT) `shiftL` (Num.fromInteger (Proxy :: Proxy nT) - b)))+ | otherwise =+ SizedInt $ (mask (Proxy :: Proxy 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 (Proxy :: Proxy nT) .&.+ ((a `shiftL` b) .|. (a `shiftR` (Num.fromInteger (Proxy :: Proxy nT) - b)))+ s@(SizedInt a) `rotateR` b+ | b < 0 =+ error $ "Bits.rotateR{" ++ showSizedIntType s ++ "}: tried to rotate by negative amount"+ | otherwise =+ SizedInt $ mask (Proxy :: Proxy nT) .&.+ ((a `shiftR` b) .|. (a `shiftL` (Num.fromInteger (Proxy :: Proxy nT) - b)))+ popCount (SizedInt x) = popCount x+ bitSize _ = Num.fromInteger (Proxy :: Proxy nT)+ isSigned _ = True+++showSizedIntTypeProxy :: forall nT. Num.Natural nT => Proxy nT -> String+showSizedIntTypeProxy n =+ "SizedInt " ++ show (Num.fromInteger n :: Integer)++showSizedIntType :: forall nT. Num.Natural nT => SizedInt nT -> String+showSizedIntType _ = showSizedIntTypeProxy (Proxy :: Proxy nT)
+ src/Data/SizedWord.hs view
@@ -0,0 +1,155 @@+{-# 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 qualified Type.Data.Num as Num+import Type.Base.Proxy (Proxy(Proxy))+++newtype SizedWord nT = SizedWord Integer++sizeT :: SizedWord nT -> Proxy nT+sizeT _ = Proxy++mask :: forall nT . Num.Natural nT => Proxy nT -> Integer+mask n = bit (Num.fromInteger n) - 1++instance Num.Natural nT => Eq (SizedWord nT) where+ (SizedWord x) == (SizedWord y) = x == y+ (SizedWord x) /= (SizedWord y) = x /= y++instance Num.Natural nT => Show (SizedWord nT) where+ showsPrec prec n =+ showsPrec prec $ toInteger n++instance Num.Natural nT => Read (SizedWord nT) where+ readsPrec prec str0 =+ [ (fromInteger n, str)+ | (n, str) <- readsPrec prec str0 ]++instance Num.Natural nT => Ord (SizedWord nT) where+ a `compare` b = toInteger a `compare` toInteger b++instance Num.Natural nT => Bounded (SizedWord nT) where+ minBound = 0+ maxBound = SizedWord $ (1 `shiftL` (Num.fromInteger (Proxy :: Proxy nT))) - 1++instance Num.Natural 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{" ++ showSizedWordTypeProxy n ++ "}: tried to take `fromEnum' on SizedWord greater than maxBound :: " ++ showSizedWordTypeProxy n+ | x < fromIntegral (minBound :: SizedWord nT) =+ error $ "Enum.fromEnum{" ++ showSizedWordTypeProxy n ++ "}: tried to take `fromEnum' on SizedWord smaller than minBound :: " ++ showSizedWordTypeProxy n+ | otherwise =+ fromInteger $ toInteger x+ where n = Proxy :: Proxy nT++instance Num.Natural 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 (Proxy :: Proxy nT)+ in if n>=0+ then fromCardinal n+ else negate $ fromCardinal $ negate n++ abs s = s+ signum s+ | s == 0 =+ 0+ | otherwise =+ 1++instance Num.Natural nT => Real (SizedWord nT) where+ toRational n = toRational $ toInteger n++instance Num.Natural 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 Num.Natural 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 (Proxy :: Proxy 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 (Proxy :: Proxy 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 (Proxy :: Proxy 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 (Proxy :: Proxy nT) .&.+ ((x `shiftR` b) .|. (x `shiftL` (bitSize s - b)))+ popCount (SizedWord x) = popCount x+ bitSize _ = Num.fromInteger (Proxy :: Proxy nT)+ isSigned _ = False++showSizedWordTypeProxy :: forall nT. Num.Natural nT => Proxy nT -> String+showSizedWordTypeProxy n =+ "SizedWord " ++ show (Num.fromInteger n :: Integer)++showSizedWordType :: forall nT. Num.Natural nT => SizedWord nT -> String+showSizedWordType _ = showSizedWordTypeProxy (Proxy :: Proxy nT)
+ src/Type/Base/Proxy.hs view
@@ -0,0 +1,24 @@+module Type.Base.Proxy where++import Control.Applicative (Applicative, pure, (<*>), )++import qualified Prelude as P+import Prelude (String, Eq, Functor, fmap)+++data Proxy a = Proxy+ deriving (Eq)++instance Functor Proxy where+ fmap _f Proxy = Proxy++instance Applicative Proxy where+ pure _ = Proxy+ Proxy <*> Proxy = Proxy+++class Show a where+ showsPrec :: P.Int -> Proxy a -> P.ShowS++instance Show a => P.Show (Proxy a) where+ showsPrec = showsPrec
+ src/Type/Data/Bool.hs view
@@ -0,0 +1,76 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE GADTs #-}++module Type.Data.Bool+ ( C(switch)+ , Singleton(False, True)+ , singleton+ , True+ , true+ , False+ , false+ , Not+ , not+ , (:&&:)+ , and+ , (:||:)+ , or+ , If+ , if_+ ) where++import Type.Base.Proxy (Proxy(Proxy))+import Data.Typeable (Typeable)++import qualified Prelude+++class C bool where switch :: f False -> f True -> f bool+instance C False where switch f _ = f+instance C True where switch _ f = f++data Singleton bool where+ False :: Singleton False+ True :: Singleton True++singleton :: (C bool) => Singleton bool+singleton = switch False True++data True deriving (Typeable)+true :: Proxy True+true = Proxy+instance Prelude.Show True where+ show _ = "True"+data False deriving (Typeable)+false :: Proxy False+false = Proxy+instance Prelude.Show False where+ show _ = "False"++type family Not x+type instance Not False = True+type instance Not True = False+not :: Proxy x -> Proxy (Not x)+not Proxy = Proxy++type family x :&&: y+type instance False :&&: _x = False+type instance True :&&: x = x+and :: Proxy x -> Proxy y -> Proxy (x :&&: y)+and Proxy Proxy = Proxy++type family x :||: y+type instance True :||: _x = True+type instance False :||: x = x+or :: Proxy x -> Proxy y -> Proxy (x :||: y)+or Proxy Proxy = Proxy++type family If x y z+type instance If True y _z = y+type instance If False _y z = z+if_ :: Proxy x -> Proxy y -> Proxy z -> Proxy (If x y z)+if_ Proxy Proxy Proxy = Proxy
+ src/Type/Data/List.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DeriveDataTypeable #-}+module Type.Data.List+ ( Cons+ , Null+ , IsNull+ , Head+ , Tail+ , Reverse+ , Append+ ) where++import qualified Prelude++import Data.Typeable++import Type.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/Type/Data/Num.hs view
@@ -0,0 +1,267 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Type.Data.Num+ ( Negate+ , negate+ , IsPositive+ , isPositive+ , IsZero+ , isZero+ , IsNegative+ , isNegative+ , IsNatural+ , isNatural+ , One+ , one+ , Succ+ , succ+ , Pred+ , pred+ , IsEven+ , isEven+ , IsOdd+ , isOdd+ , (:+:)+ , add+ , (:-:)+ , sub+ , (:*:)+ , mul+ , Mul2+ , mul2+ , Pow2+ , pow2+ , Log2Ceil+ , log2Ceil+ , DivMod+ , divMod+ , Div+ , div+ , Mod+ , mod+ , Div2+ , div2+ , Fac+ , fac+ , Singleton(..)+ , Representation (..)+ , Integer (..)+ , Natural+ , Positive+ , Negative+ , integerFromSingleton+ , integralFromSingleton+ , singletonFromProxy+ , integralFromProxy+ , fromInteger+ , reifyPositive+ , reifyNegative+ , reifyNatural+ ) where++import Type.Data.Bool (False, True, Not)+import Type.Base.Proxy (Proxy(Proxy))+import Data.Maybe.HT (toMaybe)++import qualified Prelude as P+import Prelude (Num, Maybe, (.), (<), (>), (>=))+++-- | @Negate x@ evaluates to the additive inverse of (i.e., minus) @x@.+type family Negate x+negate :: Proxy x -> Proxy (Negate x)+negate Proxy = Proxy++type family IsPositive x+isPositive :: Proxy x -> Proxy (IsPositive x)+isPositive Proxy = Proxy++type family IsZero x+isZero :: Proxy x -> Proxy (IsZero x)+isZero Proxy = Proxy++type family IsNegative x+isNegative :: Proxy x -> Proxy (IsNegative x)+isNegative Proxy = Proxy++type family IsNatural x+isNatural :: Proxy x -> Proxy (IsNatural x)+isNatural Proxy = Proxy++type family One repr+one :: Proxy repr -> Proxy (One repr)+one Proxy = Proxy++type family Succ x+succ :: Proxy x -> Proxy (Succ x)+succ Proxy = Proxy++type family Pred x+pred :: Proxy x -> Proxy (Pred x)+pred Proxy = Proxy++type family IsEven x+isEven :: Proxy x -> Proxy (IsEven x)+isEven Proxy = Proxy++type family IsOdd x+type instance IsOdd x = Not (IsEven x)+isOdd :: Proxy x -> Proxy (IsOdd x)+isOdd Proxy = Proxy++type family x :+: y+add :: Proxy x -> Proxy y -> Proxy (x :+: y)+add Proxy Proxy = Proxy++type family x :-: y+sub :: Proxy x -> Proxy y -> Proxy (x :-: y)+sub Proxy Proxy = Proxy++type family x :*: y+mul :: Proxy x -> Proxy y -> Proxy (x :*: y)+mul Proxy Proxy = Proxy++type family Mul2 x+mul2 :: Proxy x -> Proxy (Mul2 x)+mul2 Proxy = Proxy++type family DivMod x y+divMod :: Proxy x -> Proxy y -> Proxy (DivMod x y)+divMod Proxy Proxy = Proxy++type family Div x y+div :: Proxy x -> Proxy y -> Proxy (Div x y)+div Proxy Proxy = Proxy++type family Mod x y+mod :: Proxy x -> Proxy y -> Proxy (Mod x y)+mod Proxy Proxy = Proxy++type family Div2 x+div2 :: Proxy x -> Proxy (Div2 x)+div2 Proxy = Proxy++type family Fac x+fac :: Proxy x -> Proxy (Fac x)+fac Proxy = Proxy++type instance Fac x = FacRec x (IsZero x)+type family FacRec x is0+type instance FacRec x True = One (Repr x)+-- peasant multiplication is faster if second factor is small+type instance FacRec x False = Fac (Pred x) :*: x++++type family Pow2 x+pow2 :: Proxy x -> Proxy (Pow2 x)+pow2 Proxy = Proxy++type family Log2Ceil x+log2Ceil :: Proxy x -> Proxy (Log2Ceil x)+log2Ceil Proxy = Proxy++class Integer x => Natural x+instance (Integer x, IsNatural x ~ True) => Natural x+class Integer x => Positive x+instance (Integer x, IsPositive x ~ True) => Positive x+class Integer x => Negative x+instance (Integer x, IsNegative x ~ True) => Negative x++class (Representation (Repr x)) => Integer x where+ singleton :: Singleton x+ type Repr x++class Representation r where+ reifyIntegral ::+ Proxy r -> P.Integer ->+ (forall s. (Integer s, Repr s ~ r) => Proxy s -> a) ->+ a+++newtype Singleton d = Singleton P.Integer+++integerFromSingleton :: (Integer x) => Singleton x -> P.Integer+integerFromSingleton (Singleton n) = n++integralFromSingleton :: (Integer x, Num y) => Singleton x -> y+integralFromSingleton = P.fromInteger . integerFromSingleton++singletonFromProxy :: (Integer x) => Proxy x -> Singleton x+singletonFromProxy Proxy = singleton++integralFromProxy :: (Integer x, Num y) => Proxy x -> y+integralFromProxy = integralFromSingleton . singletonFromProxy++-- | synonym for 'integralFromProxy', kept for backward compatibility+fromInteger :: (Integer x, Num y) => Proxy x -> y+fromInteger = integralFromProxy+++--- positive and negative assertions: unsafe, in a trusted kernel+data AssertPos x+data AssertNeg x+data AssertNat x++assertPos :: Proxy x -> Proxy (AssertPos x)+assertPos Proxy = Proxy++assertNeg :: Proxy x -> Proxy (AssertNeg x)+assertNeg Proxy = Proxy++assertNat :: Proxy x -> Proxy (AssertNat x)+assertNat Proxy = Proxy++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 Integer x => Integer (AssertPos x) where + singleton = case singleton :: Singleton x of Singleton n -> Singleton n+ type Repr (AssertPos x) = Repr x++instance Integer x => Integer (AssertNeg x) where+ singleton = case singleton :: Singleton x of Singleton n -> Singleton n+ type Repr (AssertNeg x) = Repr x++instance Integer x => Integer (AssertNat x) where+ singleton = case singleton :: Singleton x of Singleton n -> Singleton n+ type Repr (AssertNat x) = Repr x++reifyPositive ::+ Representation r =>+ Proxy r -> P.Integer ->+ (forall s. (Positive s, Repr s ~ r) => Proxy s -> a) ->+ Maybe a+reifyPositive r n k =+ toMaybe (n > 0) (reifyIntegral r n (k . assertPos))++reifyNegative ::+ Representation r =>+ Proxy r -> P.Integer ->+ (forall s. (Negative s, Repr s ~ r) => Proxy s -> a) ->+ Maybe a+reifyNegative r n k =+ toMaybe (n < 0) (reifyIntegral r n (k . assertNeg))++reifyNatural ::+ Representation r =>+ Proxy r -> P.Integer ->+ (forall s. (Natural s, Repr s ~ r) => Proxy s -> a) ->+ Maybe a+reifyNatural r n k =+ toMaybe (n >= 0) (reifyIntegral r n (k . assertNat))
+ src/Type/Data/Num/Decimal.hs view
@@ -0,0 +1,7 @@+module Type.Data.Num.Decimal+ ( module Type.Data.Num.Decimal.Literal+ , module Type.Data.Num.Decimal.Number+ ) where++import Type.Data.Num.Decimal.Literal+import Type.Data.Num.Decimal.Number
+ src/Type/Data/Num/Decimal/Digit.hs view
@@ -0,0 +1,140 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE DeriveDataTypeable #-}++module Type.Data.Num.Decimal.Digit where++import qualified Type.Data.Num.Unary.Literal as UnaryLit++import Type.Base.Proxy (Proxy(Proxy))++import Data.Typeable (Typeable)+++newtype Singleton d = Singleton Int++singleton :: (C d) => Singleton d+singleton =+ switch+ (Singleton 0)+ (Singleton 1)+ (Singleton 2)+ (Singleton 3)+ (Singleton 4)+ (Singleton 5)+ (Singleton 6)+ (Singleton 7)+ (Singleton 8)+ (Singleton 9)++class C d where+ switch ::+ f Dec0 ->+ f Dec1 ->+ f Dec2 ->+ f Dec3 ->+ f Dec4 ->+ f Dec5 ->+ f Dec6 ->+ f Dec7 ->+ f Dec8 ->+ f Dec9 ->+ f d++class C d => Pos d where+ switchPos ::+ f Dec1 ->+ f Dec2 ->+ f Dec3 ->+ f Dec4 ->+ f Dec5 ->+ f Dec6 ->+ f Dec7 ->+ f Dec8 ->+ f Dec9 ->+ f d++data Dec0 deriving (Typeable)+instance C Dec0 where switch x _ _ _ _ _ _ _ _ _ = x+instance Show Dec0 where show _ = "0"++data Dec1 deriving (Typeable)+instance Pos Dec1 where switchPos x _ _ _ _ _ _ _ _ = x+instance C Dec1 where switch _ x _ _ _ _ _ _ _ _ = x+instance Show Dec1 where show _ = "1"++data Dec2 deriving (Typeable)+instance Pos Dec2 where switchPos _ x _ _ _ _ _ _ _ = x+instance C Dec2 where switch _ _ x _ _ _ _ _ _ _ = x+instance Show Dec2 where show _ = "2"++data Dec3 deriving (Typeable)+instance Pos Dec3 where switchPos _ _ x _ _ _ _ _ _ = x+instance C Dec3 where switch _ _ _ x _ _ _ _ _ _ = x+instance Show Dec3 where show _ = "3"++data Dec4 deriving (Typeable)+instance Pos Dec4 where switchPos _ _ _ x _ _ _ _ _ = x+instance C Dec4 where switch _ _ _ _ x _ _ _ _ _ = x+instance Show Dec4 where show _ = "4"++data Dec5 deriving (Typeable)+instance Pos Dec5 where switchPos _ _ _ _ x _ _ _ _ = x+instance C Dec5 where switch _ _ _ _ _ x _ _ _ _ = x+instance Show Dec5 where show _ = "5"++data Dec6 deriving (Typeable)+instance Pos Dec6 where switchPos _ _ _ _ _ x _ _ _ = x+instance C Dec6 where switch _ _ _ _ _ _ x _ _ _ = x+instance Show Dec6 where show _ = "6"++data Dec7 deriving (Typeable)+instance Pos Dec7 where switchPos _ _ _ _ _ _ x _ _ = x+instance C Dec7 where switch _ _ _ _ _ _ _ x _ _ = x+instance Show Dec7 where show _ = "7"++data Dec8 deriving (Typeable)+instance Pos Dec8 where switchPos _ _ _ _ _ _ _ x _ = x+instance C Dec8 where switch _ _ _ _ _ _ _ _ x _ = x+instance Show Dec8 where show _ = "8"++data Dec9 deriving (Typeable)+instance Pos Dec9 where switchPos _ _ _ _ _ _ _ _ x = x+instance C Dec9 where switch _ _ _ _ _ _ _ _ _ x = x+instance Show Dec9 where show _ = "9"+++reify :: Integer -> (forall d. C d => Proxy d -> w) -> w+reify n f =+ if n==0+ then f (Proxy :: Proxy Dec0)+ else reifyPos n f++reifyPos :: Integer -> (forall d. Pos d => Proxy d -> w) -> w+reifyPos n f =+ case n of+ 1 -> f (Proxy :: Proxy Dec1)+ 2 -> f (Proxy :: Proxy Dec2)+ 3 -> f (Proxy :: Proxy Dec3)+ 4 -> f (Proxy :: Proxy Dec4)+ 5 -> f (Proxy :: Proxy Dec5)+ 6 -> f (Proxy :: Proxy Dec6)+ 7 -> f (Proxy :: Proxy Dec7)+ 8 -> f (Proxy :: Proxy Dec8)+ 9 -> f (Proxy :: Proxy Dec9)+ _ -> error "digit must be a number from 0 to 9"+++type family ToUnary n+type instance ToUnary Dec0 = UnaryLit.U0+type instance ToUnary Dec1 = UnaryLit.U1+type instance ToUnary Dec2 = UnaryLit.U2+type instance ToUnary Dec3 = UnaryLit.U3+type instance ToUnary Dec4 = UnaryLit.U4+type instance ToUnary Dec5 = UnaryLit.U5+type instance ToUnary Dec6 = UnaryLit.U6+type instance ToUnary Dec7 = UnaryLit.U7+type instance ToUnary Dec8 = UnaryLit.U8+type instance ToUnary Dec9 = UnaryLit.U9
+ src/Type/Data/Num/Decimal/Digit/Proof.hs view
@@ -0,0 +1,69 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}+module Type.Data.Num.Decimal.Digit.Proof (+ Nat(Nat), Pos(Pos),+ UnaryNat(UnaryNat), unaryNat, unaryNatImpl,+ UnaryPos(UnaryPos), unaryPos, unaryPosImpl,+ ) where++import qualified Type.Data.Num.Unary as Unary+import qualified Type.Data.Num.Unary.Proof as UnaryProof+import qualified Type.Data.Num.Decimal.Digit as Digit+++data Nat d = (Digit.C d) => Nat+data Pos d = (Digit.Pos d) => Pos++newtype UnaryNatTheorem d =+ UnaryNatTheorem {+ runUnaryNatTheorem :: Nat d -> UnaryProof.Nat (Digit.ToUnary d)+ }++unaryNatTheorem :: (Unary.Natural (Digit.ToUnary d)) => UnaryNatTheorem d+unaryNatTheorem = UnaryNatTheorem (\Nat -> UnaryProof.Nat)++unaryNatImpl :: Nat d -> UnaryProof.Nat (Digit.ToUnary d)+unaryNatImpl d@Nat =+ runUnaryNatTheorem+ (Digit.switch+ unaryNatTheorem unaryNatTheorem unaryNatTheorem unaryNatTheorem+ unaryNatTheorem unaryNatTheorem unaryNatTheorem unaryNatTheorem+ unaryNatTheorem unaryNatTheorem)+ d+++newtype UnaryPosTheorem d =+ UnaryPosTheorem {+ runUnaryPosTheorem :: Pos d -> UnaryProof.Pos (Digit.ToUnary d)+ }++unaryPosTheorem :: (Unary.Positive (Digit.ToUnary d)) => UnaryPosTheorem d+unaryPosTheorem = UnaryPosTheorem (\Pos -> UnaryProof.Pos)++unaryPosImpl :: Pos d -> UnaryProof.Pos (Digit.ToUnary d)+unaryPosImpl d@Pos =+ runUnaryPosTheorem+ (Digit.switchPos+ unaryPosTheorem unaryPosTheorem unaryPosTheorem unaryPosTheorem+ unaryPosTheorem unaryPosTheorem unaryPosTheorem unaryPosTheorem+ unaryPosTheorem)+ d++++data UnaryNat d = Unary.Natural (Digit.ToUnary d) => UnaryNat++unaryNat :: (Digit.C d) => UnaryNat d+unaryNat =+ Digit.switch+ UnaryNat UnaryNat UnaryNat UnaryNat UnaryNat+ UnaryNat UnaryNat UnaryNat UnaryNat UnaryNat+++data UnaryPos d = Unary.Positive (Digit.ToUnary d) => UnaryPos++unaryPos :: (Digit.Pos d) => UnaryPos d+unaryPos =+ Digit.switchPos+ UnaryPos UnaryPos UnaryPos UnaryPos+ UnaryPos UnaryPos UnaryPos UnaryPos UnaryPos
+ src/Type/Data/Num/Decimal/Literal.hs view
@@ -0,0 +1,1061 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++module Type.Data.Num.Decimal.Literal where++import Type.Data.Num.Decimal.Digit+ (Dec0, Dec1, Dec2, Dec3, Dec4, Dec5, Dec6, Dec7, Dec8, Dec9)+import Type.Data.Num.Decimal.Number (Zero, Pos, Neg, EndDesc, (:>))++import Type.Base.Proxy (Proxy(Proxy))+++type Pos1 p0 = Pos p0 (EndDesc)+type Pos2 p1 p0 = Pos p1 (p0 :> EndDesc)+type Pos3 p2 p1 p0 = Pos p2 (p1 :> p0 :> EndDesc)+type Pos4 p3 p2 p1 p0 = Pos p3 (p2 :> p1 :> p0 :> EndDesc)+type Pos5 p4 p3 p2 p1 p0 = Pos p4 (p3 :> p2 :> p1 :> p0 :> EndDesc)+type Pos6 p5 p4 p3 p2 p1 p0 = Pos p5 (p4 :> p3 :> p2 :> p1 :> p0 :> EndDesc)+type Pos7 p6 p5 p4 p3 p2 p1 p0 = Pos p6 (p5 :> p4 :> p3 :> p2 :> p1 :> p0 :> EndDesc)++type Neg1 p0 = Neg p0 (EndDesc)+type Neg2 p1 p0 = Neg p1 (p0 :> EndDesc)+type Neg3 p2 p1 p0 = Neg p2 (p1 :> p0 :> EndDesc)+type Neg4 p3 p2 p1 p0 = Neg p3 (p2 :> p1 :> p0 :> EndDesc)+type Neg5 p4 p3 p2 p1 p0 = Neg p4 (p3 :> p2 :> p1 :> p0 :> EndDesc)+type Neg6 p5 p4 p3 p2 p1 p0 = Neg p5 (p4 :> p3 :> p2 :> p1 :> p0 :> EndDesc)+type Neg7 p6 p5 p4 p3 p2 p1 p0 = Neg p6 (p5 :> p4 :> p3 :> p2 :> p1 :> p0 :> EndDesc)+++type D0 = Zero++type D1 = Pos1 Dec1+type D2 = Pos1 Dec2+type D3 = Pos1 Dec3+type D4 = Pos1 Dec4+type D5 = Pos1 Dec5+type D6 = Pos1 Dec6+type D7 = Pos1 Dec7+type D8 = Pos1 Dec8+type D9 = Pos1 Dec9+type D10 = Pos2 Dec1 Dec0+type D11 = Pos2 Dec1 Dec1+type D12 = Pos2 Dec1 Dec2+type D13 = Pos2 Dec1 Dec3+type D14 = Pos2 Dec1 Dec4+type D15 = Pos2 Dec1 Dec5+type D16 = Pos2 Dec1 Dec6+type D17 = Pos2 Dec1 Dec7+type D18 = Pos2 Dec1 Dec8+type D19 = Pos2 Dec1 Dec9+type D20 = Pos2 Dec2 Dec0+type D21 = Pos2 Dec2 Dec1+type D22 = Pos2 Dec2 Dec2+type D23 = Pos2 Dec2 Dec3+type D24 = Pos2 Dec2 Dec4+type D25 = Pos2 Dec2 Dec5+type D26 = Pos2 Dec2 Dec6+type D27 = Pos2 Dec2 Dec7+type D28 = Pos2 Dec2 Dec8+type D29 = Pos2 Dec2 Dec9+type D30 = Pos2 Dec3 Dec0+type D31 = Pos2 Dec3 Dec1+type D32 = Pos2 Dec3 Dec2+type D33 = Pos2 Dec3 Dec3+type D34 = Pos2 Dec3 Dec4+type D35 = Pos2 Dec3 Dec5+type D36 = Pos2 Dec3 Dec6+type D37 = Pos2 Dec3 Dec7+type D38 = Pos2 Dec3 Dec8+type D39 = Pos2 Dec3 Dec9+type D40 = Pos2 Dec4 Dec0+type D41 = Pos2 Dec4 Dec1+type D42 = Pos2 Dec4 Dec2+type D43 = Pos2 Dec4 Dec3+type D44 = Pos2 Dec4 Dec4+type D45 = Pos2 Dec4 Dec5+type D46 = Pos2 Dec4 Dec6+type D47 = Pos2 Dec4 Dec7+type D48 = Pos2 Dec4 Dec8+type D49 = Pos2 Dec4 Dec9+type D50 = Pos2 Dec5 Dec0+type D51 = Pos2 Dec5 Dec1+type D52 = Pos2 Dec5 Dec2+type D53 = Pos2 Dec5 Dec3+type D54 = Pos2 Dec5 Dec4+type D55 = Pos2 Dec5 Dec5+type D56 = Pos2 Dec5 Dec6+type D57 = Pos2 Dec5 Dec7+type D58 = Pos2 Dec5 Dec8+type D59 = Pos2 Dec5 Dec9+type D60 = Pos2 Dec6 Dec0+type D61 = Pos2 Dec6 Dec1+type D62 = Pos2 Dec6 Dec2+type D63 = Pos2 Dec6 Dec3+type D64 = Pos2 Dec6 Dec4+type D65 = Pos2 Dec6 Dec5+type D66 = Pos2 Dec6 Dec6+type D67 = Pos2 Dec6 Dec7+type D68 = Pos2 Dec6 Dec8+type D69 = Pos2 Dec6 Dec9+type D70 = Pos2 Dec7 Dec0+type D71 = Pos2 Dec7 Dec1+type D72 = Pos2 Dec7 Dec2+type D73 = Pos2 Dec7 Dec3+type D74 = Pos2 Dec7 Dec4+type D75 = Pos2 Dec7 Dec5+type D76 = Pos2 Dec7 Dec6+type D77 = Pos2 Dec7 Dec7+type D78 = Pos2 Dec7 Dec8+type D79 = Pos2 Dec7 Dec9+type D80 = Pos2 Dec8 Dec0+type D81 = Pos2 Dec8 Dec1+type D82 = Pos2 Dec8 Dec2+type D83 = Pos2 Dec8 Dec3+type D84 = Pos2 Dec8 Dec4+type D85 = Pos2 Dec8 Dec5+type D86 = Pos2 Dec8 Dec6+type D87 = Pos2 Dec8 Dec7+type D88 = Pos2 Dec8 Dec8+type D89 = Pos2 Dec8 Dec9+type D90 = Pos2 Dec9 Dec0+type D91 = Pos2 Dec9 Dec1+type D92 = Pos2 Dec9 Dec2+type D93 = Pos2 Dec9 Dec3+type D94 = Pos2 Dec9 Dec4+type D95 = Pos2 Dec9 Dec5+type D96 = Pos2 Dec9 Dec6+type D97 = Pos2 Dec9 Dec7+type D98 = Pos2 Dec9 Dec8+type D99 = Pos2 Dec9 Dec9+type D100 = Pos3 Dec1 Dec0 Dec0+type D101 = Pos3 Dec1 Dec0 Dec1+type D102 = Pos3 Dec1 Dec0 Dec2+type D103 = Pos3 Dec1 Dec0 Dec3+type D104 = Pos3 Dec1 Dec0 Dec4+type D105 = Pos3 Dec1 Dec0 Dec5+type D106 = Pos3 Dec1 Dec0 Dec6+type D107 = Pos3 Dec1 Dec0 Dec7+type D108 = Pos3 Dec1 Dec0 Dec8+type D109 = Pos3 Dec1 Dec0 Dec9+type D110 = Pos3 Dec1 Dec1 Dec0+type D111 = Pos3 Dec1 Dec1 Dec1+type D112 = Pos3 Dec1 Dec1 Dec2+type D113 = Pos3 Dec1 Dec1 Dec3+type D114 = Pos3 Dec1 Dec1 Dec4+type D115 = Pos3 Dec1 Dec1 Dec5+type D116 = Pos3 Dec1 Dec1 Dec6+type D117 = Pos3 Dec1 Dec1 Dec7+type D118 = Pos3 Dec1 Dec1 Dec8+type D119 = Pos3 Dec1 Dec1 Dec9+type D120 = Pos3 Dec1 Dec2 Dec0+type D121 = Pos3 Dec1 Dec2 Dec1+type D122 = Pos3 Dec1 Dec2 Dec2+type D123 = Pos3 Dec1 Dec2 Dec3+type D124 = Pos3 Dec1 Dec2 Dec4+type D125 = Pos3 Dec1 Dec2 Dec5+type D126 = Pos3 Dec1 Dec2 Dec6+type D127 = Pos3 Dec1 Dec2 Dec7+type D128 = Pos3 Dec1 Dec2 Dec8+type D129 = Pos3 Dec1 Dec2 Dec9+type D130 = Pos3 Dec1 Dec3 Dec0+type D131 = Pos3 Dec1 Dec3 Dec1+type D132 = Pos3 Dec1 Dec3 Dec2+type D133 = Pos3 Dec1 Dec3 Dec3+type D134 = Pos3 Dec1 Dec3 Dec4+type D135 = Pos3 Dec1 Dec3 Dec5+type D136 = Pos3 Dec1 Dec3 Dec6+type D137 = Pos3 Dec1 Dec3 Dec7+type D138 = Pos3 Dec1 Dec3 Dec8+type D139 = Pos3 Dec1 Dec3 Dec9+type D140 = Pos3 Dec1 Dec4 Dec0+type D141 = Pos3 Dec1 Dec4 Dec1+type D142 = Pos3 Dec1 Dec4 Dec2+type D143 = Pos3 Dec1 Dec4 Dec3+type D144 = Pos3 Dec1 Dec4 Dec4+type D145 = Pos3 Dec1 Dec4 Dec5+type D146 = Pos3 Dec1 Dec4 Dec6+type D147 = Pos3 Dec1 Dec4 Dec7+type D148 = Pos3 Dec1 Dec4 Dec8+type D149 = Pos3 Dec1 Dec4 Dec9+type D150 = Pos3 Dec1 Dec5 Dec0+type D151 = Pos3 Dec1 Dec5 Dec1+type D152 = Pos3 Dec1 Dec5 Dec2+type D153 = Pos3 Dec1 Dec5 Dec3+type D154 = Pos3 Dec1 Dec5 Dec4+type D155 = Pos3 Dec1 Dec5 Dec5+type D156 = Pos3 Dec1 Dec5 Dec6+type D157 = Pos3 Dec1 Dec5 Dec7+type D158 = Pos3 Dec1 Dec5 Dec8+type D159 = Pos3 Dec1 Dec5 Dec9+type D160 = Pos3 Dec1 Dec6 Dec0+type D161 = Pos3 Dec1 Dec6 Dec1+type D162 = Pos3 Dec1 Dec6 Dec2+type D163 = Pos3 Dec1 Dec6 Dec3+type D164 = Pos3 Dec1 Dec6 Dec4+type D165 = Pos3 Dec1 Dec6 Dec5+type D166 = Pos3 Dec1 Dec6 Dec6+type D167 = Pos3 Dec1 Dec6 Dec7+type D168 = Pos3 Dec1 Dec6 Dec8+type D169 = Pos3 Dec1 Dec6 Dec9+type D170 = Pos3 Dec1 Dec7 Dec0+type D171 = Pos3 Dec1 Dec7 Dec1+type D172 = Pos3 Dec1 Dec7 Dec2+type D173 = Pos3 Dec1 Dec7 Dec3+type D174 = Pos3 Dec1 Dec7 Dec4+type D175 = Pos3 Dec1 Dec7 Dec5+type D176 = Pos3 Dec1 Dec7 Dec6+type D177 = Pos3 Dec1 Dec7 Dec7+type D178 = Pos3 Dec1 Dec7 Dec8+type D179 = Pos3 Dec1 Dec7 Dec9+type D180 = Pos3 Dec1 Dec8 Dec0+type D181 = Pos3 Dec1 Dec8 Dec1+type D182 = Pos3 Dec1 Dec8 Dec2+type D183 = Pos3 Dec1 Dec8 Dec3+type D184 = Pos3 Dec1 Dec8 Dec4+type D185 = Pos3 Dec1 Dec8 Dec5+type D186 = Pos3 Dec1 Dec8 Dec6+type D187 = Pos3 Dec1 Dec8 Dec7+type D188 = Pos3 Dec1 Dec8 Dec8+type D189 = Pos3 Dec1 Dec8 Dec9+type D190 = Pos3 Dec1 Dec9 Dec0+type D191 = Pos3 Dec1 Dec9 Dec1+type D192 = Pos3 Dec1 Dec9 Dec2+type D193 = Pos3 Dec1 Dec9 Dec3+type D194 = Pos3 Dec1 Dec9 Dec4+type D195 = Pos3 Dec1 Dec9 Dec5+type D196 = Pos3 Dec1 Dec9 Dec6+type D197 = Pos3 Dec1 Dec9 Dec7+type D198 = Pos3 Dec1 Dec9 Dec8+type D199 = Pos3 Dec1 Dec9 Dec9+type D200 = Pos3 Dec2 Dec0 Dec0+type D201 = Pos3 Dec2 Dec0 Dec1+type D202 = Pos3 Dec2 Dec0 Dec2+type D203 = Pos3 Dec2 Dec0 Dec3+type D204 = Pos3 Dec2 Dec0 Dec4+type D205 = Pos3 Dec2 Dec0 Dec5+type D206 = Pos3 Dec2 Dec0 Dec6+type D207 = Pos3 Dec2 Dec0 Dec7+type D208 = Pos3 Dec2 Dec0 Dec8+type D209 = Pos3 Dec2 Dec0 Dec9+type D210 = Pos3 Dec2 Dec1 Dec0+type D211 = Pos3 Dec2 Dec1 Dec1+type D212 = Pos3 Dec2 Dec1 Dec2+type D213 = Pos3 Dec2 Dec1 Dec3+type D214 = Pos3 Dec2 Dec1 Dec4+type D215 = Pos3 Dec2 Dec1 Dec5+type D216 = Pos3 Dec2 Dec1 Dec6+type D217 = Pos3 Dec2 Dec1 Dec7+type D218 = Pos3 Dec2 Dec1 Dec8+type D219 = Pos3 Dec2 Dec1 Dec9+type D220 = Pos3 Dec2 Dec2 Dec0+type D221 = Pos3 Dec2 Dec2 Dec1+type D222 = Pos3 Dec2 Dec2 Dec2+type D223 = Pos3 Dec2 Dec2 Dec3+type D224 = Pos3 Dec2 Dec2 Dec4+type D225 = Pos3 Dec2 Dec2 Dec5+type D226 = Pos3 Dec2 Dec2 Dec6+type D227 = Pos3 Dec2 Dec2 Dec7+type D228 = Pos3 Dec2 Dec2 Dec8+type D229 = Pos3 Dec2 Dec2 Dec9+type D230 = Pos3 Dec2 Dec3 Dec0+type D231 = Pos3 Dec2 Dec3 Dec1+type D232 = Pos3 Dec2 Dec3 Dec2+type D233 = Pos3 Dec2 Dec3 Dec3+type D234 = Pos3 Dec2 Dec3 Dec4+type D235 = Pos3 Dec2 Dec3 Dec5+type D236 = Pos3 Dec2 Dec3 Dec6+type D237 = Pos3 Dec2 Dec3 Dec7+type D238 = Pos3 Dec2 Dec3 Dec8+type D239 = Pos3 Dec2 Dec3 Dec9+type D240 = Pos3 Dec2 Dec4 Dec0+type D241 = Pos3 Dec2 Dec4 Dec1+type D242 = Pos3 Dec2 Dec4 Dec2+type D243 = Pos3 Dec2 Dec4 Dec3+type D244 = Pos3 Dec2 Dec4 Dec4+type D245 = Pos3 Dec2 Dec4 Dec5+type D246 = Pos3 Dec2 Dec4 Dec6+type D247 = Pos3 Dec2 Dec4 Dec7+type D248 = Pos3 Dec2 Dec4 Dec8+type D249 = Pos3 Dec2 Dec4 Dec9+type D250 = Pos3 Dec2 Dec5 Dec0+type D251 = Pos3 Dec2 Dec5 Dec1+type D252 = Pos3 Dec2 Dec5 Dec2+type D253 = Pos3 Dec2 Dec5 Dec3+type D254 = Pos3 Dec2 Dec5 Dec4+type D255 = Pos3 Dec2 Dec5 Dec5+type D256 = Pos3 Dec2 Dec5 Dec6++type DN1 = Neg1 Dec1+type DN2 = Neg1 Dec2+type DN3 = Neg1 Dec3+type DN4 = Neg1 Dec4+type DN5 = Neg1 Dec5+type DN6 = Neg1 Dec6+type DN7 = Neg1 Dec7+type DN8 = Neg1 Dec8+type DN9 = Neg1 Dec9+type DN10 = Neg2 Dec1 Dec0+type DN11 = Neg2 Dec1 Dec1+type DN12 = Neg2 Dec1 Dec2+type DN13 = Neg2 Dec1 Dec3+type DN14 = Neg2 Dec1 Dec4+type DN15 = Neg2 Dec1 Dec5+type DN16 = Neg2 Dec1 Dec6+type DN17 = Neg2 Dec1 Dec7+type DN18 = Neg2 Dec1 Dec8+type DN19 = Neg2 Dec1 Dec9+type DN20 = Neg2 Dec2 Dec0+type DN21 = Neg2 Dec2 Dec1+type DN22 = Neg2 Dec2 Dec2+type DN23 = Neg2 Dec2 Dec3+type DN24 = Neg2 Dec2 Dec4+type DN25 = Neg2 Dec2 Dec5+type DN26 = Neg2 Dec2 Dec6+type DN27 = Neg2 Dec2 Dec7+type DN28 = Neg2 Dec2 Dec8+type DN29 = Neg2 Dec2 Dec9+type DN30 = Neg2 Dec3 Dec0+type DN31 = Neg2 Dec3 Dec1+type DN32 = Neg2 Dec3 Dec2+type DN33 = Neg2 Dec3 Dec3+type DN34 = Neg2 Dec3 Dec4+type DN35 = Neg2 Dec3 Dec5+type DN36 = Neg2 Dec3 Dec6+type DN37 = Neg2 Dec3 Dec7+type DN38 = Neg2 Dec3 Dec8+type DN39 = Neg2 Dec3 Dec9+type DN40 = Neg2 Dec4 Dec0+type DN41 = Neg2 Dec4 Dec1+type DN42 = Neg2 Dec4 Dec2+type DN43 = Neg2 Dec4 Dec3+type DN44 = Neg2 Dec4 Dec4+type DN45 = Neg2 Dec4 Dec5+type DN46 = Neg2 Dec4 Dec6+type DN47 = Neg2 Dec4 Dec7+type DN48 = Neg2 Dec4 Dec8+type DN49 = Neg2 Dec4 Dec9+type DN50 = Neg2 Dec5 Dec0+type DN51 = Neg2 Dec5 Dec1+type DN52 = Neg2 Dec5 Dec2+type DN53 = Neg2 Dec5 Dec3+type DN54 = Neg2 Dec5 Dec4+type DN55 = Neg2 Dec5 Dec5+type DN56 = Neg2 Dec5 Dec6+type DN57 = Neg2 Dec5 Dec7+type DN58 = Neg2 Dec5 Dec8+type DN59 = Neg2 Dec5 Dec9+type DN60 = Neg2 Dec6 Dec0+type DN61 = Neg2 Dec6 Dec1+type DN62 = Neg2 Dec6 Dec2+type DN63 = Neg2 Dec6 Dec3+type DN64 = Neg2 Dec6 Dec4+type DN65 = Neg2 Dec6 Dec5+type DN66 = Neg2 Dec6 Dec6+type DN67 = Neg2 Dec6 Dec7+type DN68 = Neg2 Dec6 Dec8+type DN69 = Neg2 Dec6 Dec9+type DN70 = Neg2 Dec7 Dec0+type DN71 = Neg2 Dec7 Dec1+type DN72 = Neg2 Dec7 Dec2+type DN73 = Neg2 Dec7 Dec3+type DN74 = Neg2 Dec7 Dec4+type DN75 = Neg2 Dec7 Dec5+type DN76 = Neg2 Dec7 Dec6+type DN77 = Neg2 Dec7 Dec7+type DN78 = Neg2 Dec7 Dec8+type DN79 = Neg2 Dec7 Dec9+type DN80 = Neg2 Dec8 Dec0+type DN81 = Neg2 Dec8 Dec1+type DN82 = Neg2 Dec8 Dec2+type DN83 = Neg2 Dec8 Dec3+type DN84 = Neg2 Dec8 Dec4+type DN85 = Neg2 Dec8 Dec5+type DN86 = Neg2 Dec8 Dec6+type DN87 = Neg2 Dec8 Dec7+type DN88 = Neg2 Dec8 Dec8+type DN89 = Neg2 Dec8 Dec9+type DN90 = Neg2 Dec9 Dec0+type DN91 = Neg2 Dec9 Dec1+type DN92 = Neg2 Dec9 Dec2+type DN93 = Neg2 Dec9 Dec3+type DN94 = Neg2 Dec9 Dec4+type DN95 = Neg2 Dec9 Dec5+type DN96 = Neg2 Dec9 Dec6+type DN97 = Neg2 Dec9 Dec7+type DN98 = Neg2 Dec9 Dec8+type DN99 = Neg2 Dec9 Dec9+type DN100 = Neg3 Dec1 Dec0 Dec0+type DN101 = Neg3 Dec1 Dec0 Dec1+type DN102 = Neg3 Dec1 Dec0 Dec2+type DN103 = Neg3 Dec1 Dec0 Dec3+type DN104 = Neg3 Dec1 Dec0 Dec4+type DN105 = Neg3 Dec1 Dec0 Dec5+type DN106 = Neg3 Dec1 Dec0 Dec6+type DN107 = Neg3 Dec1 Dec0 Dec7+type DN108 = Neg3 Dec1 Dec0 Dec8+type DN109 = Neg3 Dec1 Dec0 Dec9+type DN110 = Neg3 Dec1 Dec1 Dec0+type DN111 = Neg3 Dec1 Dec1 Dec1+type DN112 = Neg3 Dec1 Dec1 Dec2+type DN113 = Neg3 Dec1 Dec1 Dec3+type DN114 = Neg3 Dec1 Dec1 Dec4+type DN115 = Neg3 Dec1 Dec1 Dec5+type DN116 = Neg3 Dec1 Dec1 Dec6+type DN117 = Neg3 Dec1 Dec1 Dec7+type DN118 = Neg3 Dec1 Dec1 Dec8+type DN119 = Neg3 Dec1 Dec1 Dec9+type DN120 = Neg3 Dec1 Dec2 Dec0+type DN121 = Neg3 Dec1 Dec2 Dec1+type DN122 = Neg3 Dec1 Dec2 Dec2+type DN123 = Neg3 Dec1 Dec2 Dec3+type DN124 = Neg3 Dec1 Dec2 Dec4+type DN125 = Neg3 Dec1 Dec2 Dec5+type DN126 = Neg3 Dec1 Dec2 Dec6+type DN127 = Neg3 Dec1 Dec2 Dec7+type DN128 = Neg3 Dec1 Dec2 Dec8+type DN129 = Neg3 Dec1 Dec2 Dec9+type DN130 = Neg3 Dec1 Dec3 Dec0+type DN131 = Neg3 Dec1 Dec3 Dec1+type DN132 = Neg3 Dec1 Dec3 Dec2+type DN133 = Neg3 Dec1 Dec3 Dec3+type DN134 = Neg3 Dec1 Dec3 Dec4+type DN135 = Neg3 Dec1 Dec3 Dec5+type DN136 = Neg3 Dec1 Dec3 Dec6+type DN137 = Neg3 Dec1 Dec3 Dec7+type DN138 = Neg3 Dec1 Dec3 Dec8+type DN139 = Neg3 Dec1 Dec3 Dec9+type DN140 = Neg3 Dec1 Dec4 Dec0+type DN141 = Neg3 Dec1 Dec4 Dec1+type DN142 = Neg3 Dec1 Dec4 Dec2+type DN143 = Neg3 Dec1 Dec4 Dec3+type DN144 = Neg3 Dec1 Dec4 Dec4+type DN145 = Neg3 Dec1 Dec4 Dec5+type DN146 = Neg3 Dec1 Dec4 Dec6+type DN147 = Neg3 Dec1 Dec4 Dec7+type DN148 = Neg3 Dec1 Dec4 Dec8+type DN149 = Neg3 Dec1 Dec4 Dec9+type DN150 = Neg3 Dec1 Dec5 Dec0+type DN151 = Neg3 Dec1 Dec5 Dec1+type DN152 = Neg3 Dec1 Dec5 Dec2+type DN153 = Neg3 Dec1 Dec5 Dec3+type DN154 = Neg3 Dec1 Dec5 Dec4+type DN155 = Neg3 Dec1 Dec5 Dec5+type DN156 = Neg3 Dec1 Dec5 Dec6+type DN157 = Neg3 Dec1 Dec5 Dec7+type DN158 = Neg3 Dec1 Dec5 Dec8+type DN159 = Neg3 Dec1 Dec5 Dec9+type DN160 = Neg3 Dec1 Dec6 Dec0+type DN161 = Neg3 Dec1 Dec6 Dec1+type DN162 = Neg3 Dec1 Dec6 Dec2+type DN163 = Neg3 Dec1 Dec6 Dec3+type DN164 = Neg3 Dec1 Dec6 Dec4+type DN165 = Neg3 Dec1 Dec6 Dec5+type DN166 = Neg3 Dec1 Dec6 Dec6+type DN167 = Neg3 Dec1 Dec6 Dec7+type DN168 = Neg3 Dec1 Dec6 Dec8+type DN169 = Neg3 Dec1 Dec6 Dec9+type DN170 = Neg3 Dec1 Dec7 Dec0+type DN171 = Neg3 Dec1 Dec7 Dec1+type DN172 = Neg3 Dec1 Dec7 Dec2+type DN173 = Neg3 Dec1 Dec7 Dec3+type DN174 = Neg3 Dec1 Dec7 Dec4+type DN175 = Neg3 Dec1 Dec7 Dec5+type DN176 = Neg3 Dec1 Dec7 Dec6+type DN177 = Neg3 Dec1 Dec7 Dec7+type DN178 = Neg3 Dec1 Dec7 Dec8+type DN179 = Neg3 Dec1 Dec7 Dec9+type DN180 = Neg3 Dec1 Dec8 Dec0+type DN181 = Neg3 Dec1 Dec8 Dec1+type DN182 = Neg3 Dec1 Dec8 Dec2+type DN183 = Neg3 Dec1 Dec8 Dec3+type DN184 = Neg3 Dec1 Dec8 Dec4+type DN185 = Neg3 Dec1 Dec8 Dec5+type DN186 = Neg3 Dec1 Dec8 Dec6+type DN187 = Neg3 Dec1 Dec8 Dec7+type DN188 = Neg3 Dec1 Dec8 Dec8+type DN189 = Neg3 Dec1 Dec8 Dec9+type DN190 = Neg3 Dec1 Dec9 Dec0+type DN191 = Neg3 Dec1 Dec9 Dec1+type DN192 = Neg3 Dec1 Dec9 Dec2+type DN193 = Neg3 Dec1 Dec9 Dec3+type DN194 = Neg3 Dec1 Dec9 Dec4+type DN195 = Neg3 Dec1 Dec9 Dec5+type DN196 = Neg3 Dec1 Dec9 Dec6+type DN197 = Neg3 Dec1 Dec9 Dec7+type DN198 = Neg3 Dec1 Dec9 Dec8+type DN199 = Neg3 Dec1 Dec9 Dec9+type DN200 = Neg3 Dec2 Dec0 Dec0+type DN201 = Neg3 Dec2 Dec0 Dec1+type DN202 = Neg3 Dec2 Dec0 Dec2+type DN203 = Neg3 Dec2 Dec0 Dec3+type DN204 = Neg3 Dec2 Dec0 Dec4+type DN205 = Neg3 Dec2 Dec0 Dec5+type DN206 = Neg3 Dec2 Dec0 Dec6+type DN207 = Neg3 Dec2 Dec0 Dec7+type DN208 = Neg3 Dec2 Dec0 Dec8+type DN209 = Neg3 Dec2 Dec0 Dec9+type DN210 = Neg3 Dec2 Dec1 Dec0+type DN211 = Neg3 Dec2 Dec1 Dec1+type DN212 = Neg3 Dec2 Dec1 Dec2+type DN213 = Neg3 Dec2 Dec1 Dec3+type DN214 = Neg3 Dec2 Dec1 Dec4+type DN215 = Neg3 Dec2 Dec1 Dec5+type DN216 = Neg3 Dec2 Dec1 Dec6+type DN217 = Neg3 Dec2 Dec1 Dec7+type DN218 = Neg3 Dec2 Dec1 Dec8+type DN219 = Neg3 Dec2 Dec1 Dec9+type DN220 = Neg3 Dec2 Dec2 Dec0+type DN221 = Neg3 Dec2 Dec2 Dec1+type DN222 = Neg3 Dec2 Dec2 Dec2+type DN223 = Neg3 Dec2 Dec2 Dec3+type DN224 = Neg3 Dec2 Dec2 Dec4+type DN225 = Neg3 Dec2 Dec2 Dec5+type DN226 = Neg3 Dec2 Dec2 Dec6+type DN227 = Neg3 Dec2 Dec2 Dec7+type DN228 = Neg3 Dec2 Dec2 Dec8+type DN229 = Neg3 Dec2 Dec2 Dec9+type DN230 = Neg3 Dec2 Dec3 Dec0+type DN231 = Neg3 Dec2 Dec3 Dec1+type DN232 = Neg3 Dec2 Dec3 Dec2+type DN233 = Neg3 Dec2 Dec3 Dec3+type DN234 = Neg3 Dec2 Dec3 Dec4+type DN235 = Neg3 Dec2 Dec3 Dec5+type DN236 = Neg3 Dec2 Dec3 Dec6+type DN237 = Neg3 Dec2 Dec3 Dec7+type DN238 = Neg3 Dec2 Dec3 Dec8+type DN239 = Neg3 Dec2 Dec3 Dec9+type DN240 = Neg3 Dec2 Dec4 Dec0+type DN241 = Neg3 Dec2 Dec4 Dec1+type DN242 = Neg3 Dec2 Dec4 Dec2+type DN243 = Neg3 Dec2 Dec4 Dec3+type DN244 = Neg3 Dec2 Dec4 Dec4+type DN245 = Neg3 Dec2 Dec4 Dec5+type DN246 = Neg3 Dec2 Dec4 Dec6+type DN247 = Neg3 Dec2 Dec4 Dec7+type DN248 = Neg3 Dec2 Dec4 Dec8+type DN249 = Neg3 Dec2 Dec4 Dec9+type DN250 = Neg3 Dec2 Dec5 Dec0+type DN251 = Neg3 Dec2 Dec5 Dec1+type DN252 = Neg3 Dec2 Dec5 Dec2+type DN253 = Neg3 Dec2 Dec5 Dec3+type DN254 = Neg3 Dec2 Dec5 Dec4+type DN255 = Neg3 Dec2 Dec5 Dec5+type DN256 = Neg3 Dec2 Dec5 Dec6+++d0 :: Proxy D0; d0 = Proxy++d1 :: Proxy D1; d1 = Proxy+d2 :: Proxy D2; d2 = Proxy+d3 :: Proxy D3; d3 = Proxy+d4 :: Proxy D4; d4 = Proxy+d5 :: Proxy D5; d5 = Proxy+d6 :: Proxy D6; d6 = Proxy+d7 :: Proxy D7; d7 = Proxy+d8 :: Proxy D8; d8 = Proxy+d9 :: Proxy D9; d9 = Proxy+d10 :: Proxy D10; d10 = Proxy+d11 :: Proxy D11; d11 = Proxy+d12 :: Proxy D12; d12 = Proxy+d13 :: Proxy D13; d13 = Proxy+d14 :: Proxy D14; d14 = Proxy+d15 :: Proxy D15; d15 = Proxy+d16 :: Proxy D16; d16 = Proxy+d17 :: Proxy D17; d17 = Proxy+d18 :: Proxy D18; d18 = Proxy+d19 :: Proxy D19; d19 = Proxy+d20 :: Proxy D20; d20 = Proxy+d21 :: Proxy D21; d21 = Proxy+d22 :: Proxy D22; d22 = Proxy+d23 :: Proxy D23; d23 = Proxy+d24 :: Proxy D24; d24 = Proxy+d25 :: Proxy D25; d25 = Proxy+d26 :: Proxy D26; d26 = Proxy+d27 :: Proxy D27; d27 = Proxy+d28 :: Proxy D28; d28 = Proxy+d29 :: Proxy D29; d29 = Proxy+d30 :: Proxy D30; d30 = Proxy+d31 :: Proxy D31; d31 = Proxy+d32 :: Proxy D32; d32 = Proxy+d33 :: Proxy D33; d33 = Proxy+d34 :: Proxy D34; d34 = Proxy+d35 :: Proxy D35; d35 = Proxy+d36 :: Proxy D36; d36 = Proxy+d37 :: Proxy D37; d37 = Proxy+d38 :: Proxy D38; d38 = Proxy+d39 :: Proxy D39; d39 = Proxy+d40 :: Proxy D40; d40 = Proxy+d41 :: Proxy D41; d41 = Proxy+d42 :: Proxy D42; d42 = Proxy+d43 :: Proxy D43; d43 = Proxy+d44 :: Proxy D44; d44 = Proxy+d45 :: Proxy D45; d45 = Proxy+d46 :: Proxy D46; d46 = Proxy+d47 :: Proxy D47; d47 = Proxy+d48 :: Proxy D48; d48 = Proxy+d49 :: Proxy D49; d49 = Proxy+d50 :: Proxy D50; d50 = Proxy+d51 :: Proxy D51; d51 = Proxy+d52 :: Proxy D52; d52 = Proxy+d53 :: Proxy D53; d53 = Proxy+d54 :: Proxy D54; d54 = Proxy+d55 :: Proxy D55; d55 = Proxy+d56 :: Proxy D56; d56 = Proxy+d57 :: Proxy D57; d57 = Proxy+d58 :: Proxy D58; d58 = Proxy+d59 :: Proxy D59; d59 = Proxy+d60 :: Proxy D60; d60 = Proxy+d61 :: Proxy D61; d61 = Proxy+d62 :: Proxy D62; d62 = Proxy+d63 :: Proxy D63; d63 = Proxy+d64 :: Proxy D64; d64 = Proxy+d65 :: Proxy D65; d65 = Proxy+d66 :: Proxy D66; d66 = Proxy+d67 :: Proxy D67; d67 = Proxy+d68 :: Proxy D68; d68 = Proxy+d69 :: Proxy D69; d69 = Proxy+d70 :: Proxy D70; d70 = Proxy+d71 :: Proxy D71; d71 = Proxy+d72 :: Proxy D72; d72 = Proxy+d73 :: Proxy D73; d73 = Proxy+d74 :: Proxy D74; d74 = Proxy+d75 :: Proxy D75; d75 = Proxy+d76 :: Proxy D76; d76 = Proxy+d77 :: Proxy D77; d77 = Proxy+d78 :: Proxy D78; d78 = Proxy+d79 :: Proxy D79; d79 = Proxy+d80 :: Proxy D80; d80 = Proxy+d81 :: Proxy D81; d81 = Proxy+d82 :: Proxy D82; d82 = Proxy+d83 :: Proxy D83; d83 = Proxy+d84 :: Proxy D84; d84 = Proxy+d85 :: Proxy D85; d85 = Proxy+d86 :: Proxy D86; d86 = Proxy+d87 :: Proxy D87; d87 = Proxy+d88 :: Proxy D88; d88 = Proxy+d89 :: Proxy D89; d89 = Proxy+d90 :: Proxy D90; d90 = Proxy+d91 :: Proxy D91; d91 = Proxy+d92 :: Proxy D92; d92 = Proxy+d93 :: Proxy D93; d93 = Proxy+d94 :: Proxy D94; d94 = Proxy+d95 :: Proxy D95; d95 = Proxy+d96 :: Proxy D96; d96 = Proxy+d97 :: Proxy D97; d97 = Proxy+d98 :: Proxy D98; d98 = Proxy+d99 :: Proxy D99; d99 = Proxy+d100 :: Proxy D100; d100 = Proxy+d101 :: Proxy D101; d101 = Proxy+d102 :: Proxy D102; d102 = Proxy+d103 :: Proxy D103; d103 = Proxy+d104 :: Proxy D104; d104 = Proxy+d105 :: Proxy D105; d105 = Proxy+d106 :: Proxy D106; d106 = Proxy+d107 :: Proxy D107; d107 = Proxy+d108 :: Proxy D108; d108 = Proxy+d109 :: Proxy D109; d109 = Proxy+d110 :: Proxy D110; d110 = Proxy+d111 :: Proxy D111; d111 = Proxy+d112 :: Proxy D112; d112 = Proxy+d113 :: Proxy D113; d113 = Proxy+d114 :: Proxy D114; d114 = Proxy+d115 :: Proxy D115; d115 = Proxy+d116 :: Proxy D116; d116 = Proxy+d117 :: Proxy D117; d117 = Proxy+d118 :: Proxy D118; d118 = Proxy+d119 :: Proxy D119; d119 = Proxy+d120 :: Proxy D120; d120 = Proxy+d121 :: Proxy D121; d121 = Proxy+d122 :: Proxy D122; d122 = Proxy+d123 :: Proxy D123; d123 = Proxy+d124 :: Proxy D124; d124 = Proxy+d125 :: Proxy D125; d125 = Proxy+d126 :: Proxy D126; d126 = Proxy+d127 :: Proxy D127; d127 = Proxy+d128 :: Proxy D128; d128 = Proxy+d129 :: Proxy D129; d129 = Proxy+d130 :: Proxy D130; d130 = Proxy+d131 :: Proxy D131; d131 = Proxy+d132 :: Proxy D132; d132 = Proxy+d133 :: Proxy D133; d133 = Proxy+d134 :: Proxy D134; d134 = Proxy+d135 :: Proxy D135; d135 = Proxy+d136 :: Proxy D136; d136 = Proxy+d137 :: Proxy D137; d137 = Proxy+d138 :: Proxy D138; d138 = Proxy+d139 :: Proxy D139; d139 = Proxy+d140 :: Proxy D140; d140 = Proxy+d141 :: Proxy D141; d141 = Proxy+d142 :: Proxy D142; d142 = Proxy+d143 :: Proxy D143; d143 = Proxy+d144 :: Proxy D144; d144 = Proxy+d145 :: Proxy D145; d145 = Proxy+d146 :: Proxy D146; d146 = Proxy+d147 :: Proxy D147; d147 = Proxy+d148 :: Proxy D148; d148 = Proxy+d149 :: Proxy D149; d149 = Proxy+d150 :: Proxy D150; d150 = Proxy+d151 :: Proxy D151; d151 = Proxy+d152 :: Proxy D152; d152 = Proxy+d153 :: Proxy D153; d153 = Proxy+d154 :: Proxy D154; d154 = Proxy+d155 :: Proxy D155; d155 = Proxy+d156 :: Proxy D156; d156 = Proxy+d157 :: Proxy D157; d157 = Proxy+d158 :: Proxy D158; d158 = Proxy+d159 :: Proxy D159; d159 = Proxy+d160 :: Proxy D160; d160 = Proxy+d161 :: Proxy D161; d161 = Proxy+d162 :: Proxy D162; d162 = Proxy+d163 :: Proxy D163; d163 = Proxy+d164 :: Proxy D164; d164 = Proxy+d165 :: Proxy D165; d165 = Proxy+d166 :: Proxy D166; d166 = Proxy+d167 :: Proxy D167; d167 = Proxy+d168 :: Proxy D168; d168 = Proxy+d169 :: Proxy D169; d169 = Proxy+d170 :: Proxy D170; d170 = Proxy+d171 :: Proxy D171; d171 = Proxy+d172 :: Proxy D172; d172 = Proxy+d173 :: Proxy D173; d173 = Proxy+d174 :: Proxy D174; d174 = Proxy+d175 :: Proxy D175; d175 = Proxy+d176 :: Proxy D176; d176 = Proxy+d177 :: Proxy D177; d177 = Proxy+d178 :: Proxy D178; d178 = Proxy+d179 :: Proxy D179; d179 = Proxy+d180 :: Proxy D180; d180 = Proxy+d181 :: Proxy D181; d181 = Proxy+d182 :: Proxy D182; d182 = Proxy+d183 :: Proxy D183; d183 = Proxy+d184 :: Proxy D184; d184 = Proxy+d185 :: Proxy D185; d185 = Proxy+d186 :: Proxy D186; d186 = Proxy+d187 :: Proxy D187; d187 = Proxy+d188 :: Proxy D188; d188 = Proxy+d189 :: Proxy D189; d189 = Proxy+d190 :: Proxy D190; d190 = Proxy+d191 :: Proxy D191; d191 = Proxy+d192 :: Proxy D192; d192 = Proxy+d193 :: Proxy D193; d193 = Proxy+d194 :: Proxy D194; d194 = Proxy+d195 :: Proxy D195; d195 = Proxy+d196 :: Proxy D196; d196 = Proxy+d197 :: Proxy D197; d197 = Proxy+d198 :: Proxy D198; d198 = Proxy+d199 :: Proxy D199; d199 = Proxy+d200 :: Proxy D200; d200 = Proxy+d201 :: Proxy D201; d201 = Proxy+d202 :: Proxy D202; d202 = Proxy+d203 :: Proxy D203; d203 = Proxy+d204 :: Proxy D204; d204 = Proxy+d205 :: Proxy D205; d205 = Proxy+d206 :: Proxy D206; d206 = Proxy+d207 :: Proxy D207; d207 = Proxy+d208 :: Proxy D208; d208 = Proxy+d209 :: Proxy D209; d209 = Proxy+d210 :: Proxy D210; d210 = Proxy+d211 :: Proxy D211; d211 = Proxy+d212 :: Proxy D212; d212 = Proxy+d213 :: Proxy D213; d213 = Proxy+d214 :: Proxy D214; d214 = Proxy+d215 :: Proxy D215; d215 = Proxy+d216 :: Proxy D216; d216 = Proxy+d217 :: Proxy D217; d217 = Proxy+d218 :: Proxy D218; d218 = Proxy+d219 :: Proxy D219; d219 = Proxy+d220 :: Proxy D220; d220 = Proxy+d221 :: Proxy D221; d221 = Proxy+d222 :: Proxy D222; d222 = Proxy+d223 :: Proxy D223; d223 = Proxy+d224 :: Proxy D224; d224 = Proxy+d225 :: Proxy D225; d225 = Proxy+d226 :: Proxy D226; d226 = Proxy+d227 :: Proxy D227; d227 = Proxy+d228 :: Proxy D228; d228 = Proxy+d229 :: Proxy D229; d229 = Proxy+d230 :: Proxy D230; d230 = Proxy+d231 :: Proxy D231; d231 = Proxy+d232 :: Proxy D232; d232 = Proxy+d233 :: Proxy D233; d233 = Proxy+d234 :: Proxy D234; d234 = Proxy+d235 :: Proxy D235; d235 = Proxy+d236 :: Proxy D236; d236 = Proxy+d237 :: Proxy D237; d237 = Proxy+d238 :: Proxy D238; d238 = Proxy+d239 :: Proxy D239; d239 = Proxy+d240 :: Proxy D240; d240 = Proxy+d241 :: Proxy D241; d241 = Proxy+d242 :: Proxy D242; d242 = Proxy+d243 :: Proxy D243; d243 = Proxy+d244 :: Proxy D244; d244 = Proxy+d245 :: Proxy D245; d245 = Proxy+d246 :: Proxy D246; d246 = Proxy+d247 :: Proxy D247; d247 = Proxy+d248 :: Proxy D248; d248 = Proxy+d249 :: Proxy D249; d249 = Proxy+d250 :: Proxy D250; d250 = Proxy+d251 :: Proxy D251; d251 = Proxy+d252 :: Proxy D252; d252 = Proxy+d253 :: Proxy D253; d253 = Proxy+d254 :: Proxy D254; d254 = Proxy+d255 :: Proxy D255; d255 = Proxy+d256 :: Proxy D256; d256 = Proxy++dn1 :: Proxy DN1; dn1 = Proxy+dn2 :: Proxy DN2; dn2 = Proxy+dn3 :: Proxy DN3; dn3 = Proxy+dn4 :: Proxy DN4; dn4 = Proxy+dn5 :: Proxy DN5; dn5 = Proxy+dn6 :: Proxy DN6; dn6 = Proxy+dn7 :: Proxy DN7; dn7 = Proxy+dn8 :: Proxy DN8; dn8 = Proxy+dn9 :: Proxy DN9; dn9 = Proxy+dn10 :: Proxy DN10; dn10 = Proxy+dn11 :: Proxy DN11; dn11 = Proxy+dn12 :: Proxy DN12; dn12 = Proxy+dn13 :: Proxy DN13; dn13 = Proxy+dn14 :: Proxy DN14; dn14 = Proxy+dn15 :: Proxy DN15; dn15 = Proxy+dn16 :: Proxy DN16; dn16 = Proxy+dn17 :: Proxy DN17; dn17 = Proxy+dn18 :: Proxy DN18; dn18 = Proxy+dn19 :: Proxy DN19; dn19 = Proxy+dn20 :: Proxy DN20; dn20 = Proxy+dn21 :: Proxy DN21; dn21 = Proxy+dn22 :: Proxy DN22; dn22 = Proxy+dn23 :: Proxy DN23; dn23 = Proxy+dn24 :: Proxy DN24; dn24 = Proxy+dn25 :: Proxy DN25; dn25 = Proxy+dn26 :: Proxy DN26; dn26 = Proxy+dn27 :: Proxy DN27; dn27 = Proxy+dn28 :: Proxy DN28; dn28 = Proxy+dn29 :: Proxy DN29; dn29 = Proxy+dn30 :: Proxy DN30; dn30 = Proxy+dn31 :: Proxy DN31; dn31 = Proxy+dn32 :: Proxy DN32; dn32 = Proxy+dn33 :: Proxy DN33; dn33 = Proxy+dn34 :: Proxy DN34; dn34 = Proxy+dn35 :: Proxy DN35; dn35 = Proxy+dn36 :: Proxy DN36; dn36 = Proxy+dn37 :: Proxy DN37; dn37 = Proxy+dn38 :: Proxy DN38; dn38 = Proxy+dn39 :: Proxy DN39; dn39 = Proxy+dn40 :: Proxy DN40; dn40 = Proxy+dn41 :: Proxy DN41; dn41 = Proxy+dn42 :: Proxy DN42; dn42 = Proxy+dn43 :: Proxy DN43; dn43 = Proxy+dn44 :: Proxy DN44; dn44 = Proxy+dn45 :: Proxy DN45; dn45 = Proxy+dn46 :: Proxy DN46; dn46 = Proxy+dn47 :: Proxy DN47; dn47 = Proxy+dn48 :: Proxy DN48; dn48 = Proxy+dn49 :: Proxy DN49; dn49 = Proxy+dn50 :: Proxy DN50; dn50 = Proxy+dn51 :: Proxy DN51; dn51 = Proxy+dn52 :: Proxy DN52; dn52 = Proxy+dn53 :: Proxy DN53; dn53 = Proxy+dn54 :: Proxy DN54; dn54 = Proxy+dn55 :: Proxy DN55; dn55 = Proxy+dn56 :: Proxy DN56; dn56 = Proxy+dn57 :: Proxy DN57; dn57 = Proxy+dn58 :: Proxy DN58; dn58 = Proxy+dn59 :: Proxy DN59; dn59 = Proxy+dn60 :: Proxy DN60; dn60 = Proxy+dn61 :: Proxy DN61; dn61 = Proxy+dn62 :: Proxy DN62; dn62 = Proxy+dn63 :: Proxy DN63; dn63 = Proxy+dn64 :: Proxy DN64; dn64 = Proxy+dn65 :: Proxy DN65; dn65 = Proxy+dn66 :: Proxy DN66; dn66 = Proxy+dn67 :: Proxy DN67; dn67 = Proxy+dn68 :: Proxy DN68; dn68 = Proxy+dn69 :: Proxy DN69; dn69 = Proxy+dn70 :: Proxy DN70; dn70 = Proxy+dn71 :: Proxy DN71; dn71 = Proxy+dn72 :: Proxy DN72; dn72 = Proxy+dn73 :: Proxy DN73; dn73 = Proxy+dn74 :: Proxy DN74; dn74 = Proxy+dn75 :: Proxy DN75; dn75 = Proxy+dn76 :: Proxy DN76; dn76 = Proxy+dn77 :: Proxy DN77; dn77 = Proxy+dn78 :: Proxy DN78; dn78 = Proxy+dn79 :: Proxy DN79; dn79 = Proxy+dn80 :: Proxy DN80; dn80 = Proxy+dn81 :: Proxy DN81; dn81 = Proxy+dn82 :: Proxy DN82; dn82 = Proxy+dn83 :: Proxy DN83; dn83 = Proxy+dn84 :: Proxy DN84; dn84 = Proxy+dn85 :: Proxy DN85; dn85 = Proxy+dn86 :: Proxy DN86; dn86 = Proxy+dn87 :: Proxy DN87; dn87 = Proxy+dn88 :: Proxy DN88; dn88 = Proxy+dn89 :: Proxy DN89; dn89 = Proxy+dn90 :: Proxy DN90; dn90 = Proxy+dn91 :: Proxy DN91; dn91 = Proxy+dn92 :: Proxy DN92; dn92 = Proxy+dn93 :: Proxy DN93; dn93 = Proxy+dn94 :: Proxy DN94; dn94 = Proxy+dn95 :: Proxy DN95; dn95 = Proxy+dn96 :: Proxy DN96; dn96 = Proxy+dn97 :: Proxy DN97; dn97 = Proxy+dn98 :: Proxy DN98; dn98 = Proxy+dn99 :: Proxy DN99; dn99 = Proxy+dn100 :: Proxy DN100; dn100 = Proxy+dn101 :: Proxy DN101; dn101 = Proxy+dn102 :: Proxy DN102; dn102 = Proxy+dn103 :: Proxy DN103; dn103 = Proxy+dn104 :: Proxy DN104; dn104 = Proxy+dn105 :: Proxy DN105; dn105 = Proxy+dn106 :: Proxy DN106; dn106 = Proxy+dn107 :: Proxy DN107; dn107 = Proxy+dn108 :: Proxy DN108; dn108 = Proxy+dn109 :: Proxy DN109; dn109 = Proxy+dn110 :: Proxy DN110; dn110 = Proxy+dn111 :: Proxy DN111; dn111 = Proxy+dn112 :: Proxy DN112; dn112 = Proxy+dn113 :: Proxy DN113; dn113 = Proxy+dn114 :: Proxy DN114; dn114 = Proxy+dn115 :: Proxy DN115; dn115 = Proxy+dn116 :: Proxy DN116; dn116 = Proxy+dn117 :: Proxy DN117; dn117 = Proxy+dn118 :: Proxy DN118; dn118 = Proxy+dn119 :: Proxy DN119; dn119 = Proxy+dn120 :: Proxy DN120; dn120 = Proxy+dn121 :: Proxy DN121; dn121 = Proxy+dn122 :: Proxy DN122; dn122 = Proxy+dn123 :: Proxy DN123; dn123 = Proxy+dn124 :: Proxy DN124; dn124 = Proxy+dn125 :: Proxy DN125; dn125 = Proxy+dn126 :: Proxy DN126; dn126 = Proxy+dn127 :: Proxy DN127; dn127 = Proxy+dn128 :: Proxy DN128; dn128 = Proxy+dn129 :: Proxy DN129; dn129 = Proxy+dn130 :: Proxy DN130; dn130 = Proxy+dn131 :: Proxy DN131; dn131 = Proxy+dn132 :: Proxy DN132; dn132 = Proxy+dn133 :: Proxy DN133; dn133 = Proxy+dn134 :: Proxy DN134; dn134 = Proxy+dn135 :: Proxy DN135; dn135 = Proxy+dn136 :: Proxy DN136; dn136 = Proxy+dn137 :: Proxy DN137; dn137 = Proxy+dn138 :: Proxy DN138; dn138 = Proxy+dn139 :: Proxy DN139; dn139 = Proxy+dn140 :: Proxy DN140; dn140 = Proxy+dn141 :: Proxy DN141; dn141 = Proxy+dn142 :: Proxy DN142; dn142 = Proxy+dn143 :: Proxy DN143; dn143 = Proxy+dn144 :: Proxy DN144; dn144 = Proxy+dn145 :: Proxy DN145; dn145 = Proxy+dn146 :: Proxy DN146; dn146 = Proxy+dn147 :: Proxy DN147; dn147 = Proxy+dn148 :: Proxy DN148; dn148 = Proxy+dn149 :: Proxy DN149; dn149 = Proxy+dn150 :: Proxy DN150; dn150 = Proxy+dn151 :: Proxy DN151; dn151 = Proxy+dn152 :: Proxy DN152; dn152 = Proxy+dn153 :: Proxy DN153; dn153 = Proxy+dn154 :: Proxy DN154; dn154 = Proxy+dn155 :: Proxy DN155; dn155 = Proxy+dn156 :: Proxy DN156; dn156 = Proxy+dn157 :: Proxy DN157; dn157 = Proxy+dn158 :: Proxy DN158; dn158 = Proxy+dn159 :: Proxy DN159; dn159 = Proxy+dn160 :: Proxy DN160; dn160 = Proxy+dn161 :: Proxy DN161; dn161 = Proxy+dn162 :: Proxy DN162; dn162 = Proxy+dn163 :: Proxy DN163; dn163 = Proxy+dn164 :: Proxy DN164; dn164 = Proxy+dn165 :: Proxy DN165; dn165 = Proxy+dn166 :: Proxy DN166; dn166 = Proxy+dn167 :: Proxy DN167; dn167 = Proxy+dn168 :: Proxy DN168; dn168 = Proxy+dn169 :: Proxy DN169; dn169 = Proxy+dn170 :: Proxy DN170; dn170 = Proxy+dn171 :: Proxy DN171; dn171 = Proxy+dn172 :: Proxy DN172; dn172 = Proxy+dn173 :: Proxy DN173; dn173 = Proxy+dn174 :: Proxy DN174; dn174 = Proxy+dn175 :: Proxy DN175; dn175 = Proxy+dn176 :: Proxy DN176; dn176 = Proxy+dn177 :: Proxy DN177; dn177 = Proxy+dn178 :: Proxy DN178; dn178 = Proxy+dn179 :: Proxy DN179; dn179 = Proxy+dn180 :: Proxy DN180; dn180 = Proxy+dn181 :: Proxy DN181; dn181 = Proxy+dn182 :: Proxy DN182; dn182 = Proxy+dn183 :: Proxy DN183; dn183 = Proxy+dn184 :: Proxy DN184; dn184 = Proxy+dn185 :: Proxy DN185; dn185 = Proxy+dn186 :: Proxy DN186; dn186 = Proxy+dn187 :: Proxy DN187; dn187 = Proxy+dn188 :: Proxy DN188; dn188 = Proxy+dn189 :: Proxy DN189; dn189 = Proxy+dn190 :: Proxy DN190; dn190 = Proxy+dn191 :: Proxy DN191; dn191 = Proxy+dn192 :: Proxy DN192; dn192 = Proxy+dn193 :: Proxy DN193; dn193 = Proxy+dn194 :: Proxy DN194; dn194 = Proxy+dn195 :: Proxy DN195; dn195 = Proxy+dn196 :: Proxy DN196; dn196 = Proxy+dn197 :: Proxy DN197; dn197 = Proxy+dn198 :: Proxy DN198; dn198 = Proxy+dn199 :: Proxy DN199; dn199 = Proxy+dn200 :: Proxy DN200; dn200 = Proxy+dn201 :: Proxy DN201; dn201 = Proxy+dn202 :: Proxy DN202; dn202 = Proxy+dn203 :: Proxy DN203; dn203 = Proxy+dn204 :: Proxy DN204; dn204 = Proxy+dn205 :: Proxy DN205; dn205 = Proxy+dn206 :: Proxy DN206; dn206 = Proxy+dn207 :: Proxy DN207; dn207 = Proxy+dn208 :: Proxy DN208; dn208 = Proxy+dn209 :: Proxy DN209; dn209 = Proxy+dn210 :: Proxy DN210; dn210 = Proxy+dn211 :: Proxy DN211; dn211 = Proxy+dn212 :: Proxy DN212; dn212 = Proxy+dn213 :: Proxy DN213; dn213 = Proxy+dn214 :: Proxy DN214; dn214 = Proxy+dn215 :: Proxy DN215; dn215 = Proxy+dn216 :: Proxy DN216; dn216 = Proxy+dn217 :: Proxy DN217; dn217 = Proxy+dn218 :: Proxy DN218; dn218 = Proxy+dn219 :: Proxy DN219; dn219 = Proxy+dn220 :: Proxy DN220; dn220 = Proxy+dn221 :: Proxy DN221; dn221 = Proxy+dn222 :: Proxy DN222; dn222 = Proxy+dn223 :: Proxy DN223; dn223 = Proxy+dn224 :: Proxy DN224; dn224 = Proxy+dn225 :: Proxy DN225; dn225 = Proxy+dn226 :: Proxy DN226; dn226 = Proxy+dn227 :: Proxy DN227; dn227 = Proxy+dn228 :: Proxy DN228; dn228 = Proxy+dn229 :: Proxy DN229; dn229 = Proxy+dn230 :: Proxy DN230; dn230 = Proxy+dn231 :: Proxy DN231; dn231 = Proxy+dn232 :: Proxy DN232; dn232 = Proxy+dn233 :: Proxy DN233; dn233 = Proxy+dn234 :: Proxy DN234; dn234 = Proxy+dn235 :: Proxy DN235; dn235 = Proxy+dn236 :: Proxy DN236; dn236 = Proxy+dn237 :: Proxy DN237; dn237 = Proxy+dn238 :: Proxy DN238; dn238 = Proxy+dn239 :: Proxy DN239; dn239 = Proxy+dn240 :: Proxy DN240; dn240 = Proxy+dn241 :: Proxy DN241; dn241 = Proxy+dn242 :: Proxy DN242; dn242 = Proxy+dn243 :: Proxy DN243; dn243 = Proxy+dn244 :: Proxy DN244; dn244 = Proxy+dn245 :: Proxy DN245; dn245 = Proxy+dn246 :: Proxy DN246; dn246 = Proxy+dn247 :: Proxy DN247; dn247 = Proxy+dn248 :: Proxy DN248; dn248 = Proxy+dn249 :: Proxy DN249; dn249 = Proxy+dn250 :: Proxy DN250; dn250 = Proxy+dn251 :: Proxy DN251; dn251 = Proxy+dn252 :: Proxy DN252; dn252 = Proxy+dn253 :: Proxy DN253; dn253 = Proxy+dn254 :: Proxy DN254; dn254 = Proxy+dn255 :: Proxy DN255; dn255 = Proxy+dn256 :: Proxy DN256; dn256 = Proxy
+ src/Type/Data/Num/Decimal/Number.hs view
@@ -0,0 +1,1516 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE Rank2Types #-}++module Type.Data.Num.Decimal.Number (+ Decimal, decimal,+ Dec, Zero, Pos, Neg, EndAsc, (:<), EndDesc, (:>),+ Singleton(..), singleton, singletonFromProxy,+ integerFromSingleton, integralFromSingleton,+ integralFromProxy,++ Integer(..), Natural(..),+ Positive(..), Negative(..),++ reifyIntegral, reifyNatural,+ reifyPositive, reifyNegative,+ reifyPos, reifyNeg,++ Digits(..),++ (:+:), (:-:), (:*:),+ Pred, Succ, Compare, IsEven, Pow2, Log2Ceil,++ (:<:), (:<=:), (:==:),+ (:>:), (:>=:), (:/=:),++ FromUnary, ToUnary,+ ToUnaryAcc, UnaryAcc, -- for Proof+ ) where++import qualified Type.Data.Num.Decimal.Digit as Digit+import qualified Type.Data.Num.Unary.Literal as UnaryLit+import qualified Type.Data.Num.Unary as Unary+import qualified Type.Data.Num as Op+import qualified Type.Data.Ord as Ord+import qualified Type.Base.Proxy as Proxy++import Type.Data.Num.Decimal.Digit+ (Dec0, Dec1, Dec2, Dec3, Dec4, Dec5, Dec6, Dec7, Dec8, Dec9)+import Type.Data.Bool (If, False, True)+import Type.Data.Ord (LT, GT, EQ)+import Type.Base.Proxy (Proxy(Proxy))++import Data.Maybe.HT (toMaybe)+import Data.Tuple.HT (swap)+import qualified Data.List as List++import Text.Printf (printf)++import qualified Prelude as P+import Prelude hiding (Integer)+++-- | Representation name for decimal type level numbers.+data Decimal++-- | The wrapper type for decimal type level numbers.+data Dec x+data Zero+data Neg x xs+data Pos x xs+++infixl 9 :<++data ds :< d+{-+instance (Show ds, Show d) => Show (ds :< d) where+ show _ = show (undefined :: ds) ++ show (undefined :: d)+-}++infixr 9 :>++data d :> ds+{-+instance (Show ds, Show d) => Show (d :> ds) where+ show _ = show (undefined :: d) ++ show (undefined :: ds)+-}+++-- | The terminator type for ascending decimal digit lists.+{-+we could add a type parameter to EndAsc+in order to assert non-empty ascending lists+-}+data EndAsc+instance Show EndAsc where+ show _ = ""++-- | The terminator type for descending decimal digit lists.+data EndDesc+instance Show EndDesc where+ show _ = ""+++instance Op.Representation Decimal where+ reifyIntegral _ i k = reifyIntegral i (k . decimal)++decimal :: Proxy n -> Proxy (Dec n)+decimal Proxy = Proxy++stripDec :: Proxy (Dec n) -> Proxy n+stripDec Proxy = Proxy+++instance Integer a => Proxy.Show (Dec a) where+ showsPrec prec =+ (\n -> showParen (prec>10) (showString (printf "decimal d%d" n)))+ . integerFromSingleton . singletonFromProxy . stripDec+++reifyIntegral :: P.Integer -> (forall s. Integer s => Proxy s -> w) -> w+reifyIntegral n f =+ if n < 0+ then+ case reverse $ digits $ negate n of+ [] -> error "negative means non-zero"+ x:xs ->+ Digit.reifyPos x (\d -> go xs (\ds -> f (negDigits d ds)))+ else+ case reverse $ digits n of+ [] -> f (Proxy :: Proxy Zero)+ x:xs ->+ Digit.reifyPos x (\d -> go xs (\ds -> f (posDigits d ds)))+ where+ go :: [P.Integer] -> (forall s. Digits s => Proxy s -> w) -> w+ go [] k = k (Proxy :: Proxy EndDesc)+ go (j:js) k = Digit.reify j (\d -> go js (\ds -> k (consDigits d ds)))+++negDigits :: Proxy d -> Proxy ds -> Proxy (Neg d ds)+negDigits Proxy Proxy = Proxy++posDigits :: Proxy d -> Proxy ds -> Proxy (Pos d ds)+posDigits Proxy Proxy = Proxy++consDigits :: Proxy d -> Proxy ds -> Proxy (d :> ds)+consDigits Proxy Proxy = Proxy+++digits :: P.Integer -> [P.Integer]+digits =+ List.unfoldr (\n -> toMaybe (n/=0) (swap $ quotRem n 10))+++reifyPos ::+ P.Integer ->+ (forall x xs. (Digit.Pos x, Digits xs) => Proxy (Pos x xs) -> a) ->+ Maybe a+reifyPos n f =+ reifyIntegral n+ (runCont $ switch reject reject (accept f))++reifyNeg ::+ P.Integer ->+ (forall x xs. (Digit.Pos x, Digits xs) => Proxy (Neg x xs) -> a) ->+ Maybe a+reifyNeg n f =+ reifyIntegral n+ (runCont $ switch reject (accept f) reject)++reifyPositive ::+ P.Integer -> (forall s. (Positive s) => Proxy s -> a) -> Maybe a+reifyPositive n f = reifyPos n f++reifyNegative ::+ P.Integer -> (forall s. (Negative s) => Proxy s -> a) -> Maybe a+reifyNegative n f = reifyNeg n f++reifyNatural ::+ P.Integer -> (forall s. (Natural s) => Proxy s -> a) -> Maybe a+reifyNatural n f =+ reifyIntegral n+ (runCont $ switch (accept f) reject (accept f))++newtype Cont a s = Cont {runCont :: Proxy s -> Maybe a}++accept :: (Proxy s -> a) -> Cont a s+accept f = Cont (Just . f)++reject :: Cont a s+reject = Cont (const Nothing)+++instance Integer x => Op.Integer (Dec x) where+ singleton = singletonToGeneric singleton+ type Repr (Dec x) = Decimal++singletonToGeneric :: Singleton x -> Op.Singleton (Dec x)+singletonToGeneric (Singleton n) = Op.Singleton n+++class Integer n where+ switch ::+ f Zero ->+ (forall x xs. (Digit.Pos x, Digits xs) => f (Neg x xs)) ->+ (forall x xs. (Digit.Pos x, Digits xs) => f (Pos x xs)) ->+ f n++instance Integer Zero where+ switch x _ _ = x+instance (Digit.Pos x, Digits xs) => Integer (Neg x xs) where+ switch _ x _ = x+instance (Digit.Pos x, Digits xs) => Integer (Pos x xs) where+ switch _ _ x = x+++class Integer n => Natural n where+ switchNat ::+ f Zero ->+ (forall x xs. (Digit.Pos x, Digits xs) => f (Pos x xs)) ->+ f n++instance Natural Zero where+ switchNat x _ = x+instance (Digit.Pos x, Digits xs) => Natural (Pos x xs) where+ switchNat _ x = x+++class Natural n => Positive n where+ switchPos ::+ (forall x xs. (Digit.Pos x, Digits xs) => f (Pos x xs)) ->+ f n++instance (Digit.Pos x, Digits xs) => Positive (Pos x xs) where+ switchPos x = x+++class Integer n => Negative n where+ switchNeg ::+ (forall x xs. (Digit.Pos x, Digits xs) => f (Neg x xs)) ->+ f n++instance (Digit.Pos x, Digits xs) => Negative (Neg x xs) where+ switchNeg x = x+++newtype Singleton x = Singleton P.Integer++singleton :: (Integer x) => Singleton x+singleton =+ switch+ (Singleton 0)+ (withProxy $ \(Digit.Singleton n) proxy ->+ negate (fromDigits (fromIntegral n) proxy))+ (withProxy $ \(Digit.Singleton n) proxy ->+ fromDigits (fromIntegral n) proxy)++withProxy ::+ (Digit.C x) =>+ (Digit.Singleton x -> Proxy xs -> P.Integer) -> Singleton (cons x xs)+withProxy f = Singleton $ f Digit.singleton Proxy++integerFromSingleton :: (Integer n) => Singleton n -> P.Integer+integerFromSingleton (Singleton n) = n++integralFromSingleton :: (Integer n, Num a) => Singleton n -> a+integralFromSingleton = fromInteger . integerFromSingleton++singletonFromProxy :: (Integer n) => Proxy n -> Singleton n+singletonFromProxy Proxy = singleton++integralFromProxy :: (Integer n, Num a) => Proxy n -> a+integralFromProxy = integralFromSingleton . singletonFromProxy+++class Digits xs where+ switchDigits ::+ f EndDesc ->+ (forall xh xl. (Digit.C xh, Digits xl) => f (xh :> xl)) ->+ f xs+instance Digits EndDesc where+ switchDigits x _ = x+instance (Digit.C xh, Digits xl) => Digits (xh :> xl) where+ switchDigits _ x = x++newtype+ FromDigits y xs =+ FromDigits {runFromDigits :: y -> Proxy xs -> y}++fromDigits :: (Num y, Digits xs) => y -> Proxy xs -> y+fromDigits =+ runFromDigits $+ switchDigits+ (FromDigits $ \acc _ -> acc)+ (FromDigits $ \acc ->+ withDigits $ \(Digit.Singleton n) xl ->+ fromDigits (10*acc + fromIntegral n) xl)++withDigits ::+ (Digit.C xh) =>+ (Digit.Singleton xh -> Proxy xl -> a) -> Proxy (xh :> xl) -> a+withDigits f Proxy = f Digit.singleton Proxy+++type Id x = x++type family NormalizePos x+type instance NormalizePos EndDesc = Zero+type instance NormalizePos (Dec0 :> xl) = NormalizePos xl+type instance NormalizePos (Dec1 :> xl) = Pos Dec1 xl+type instance NormalizePos (Dec2 :> xl) = Pos Dec2 xl+type instance NormalizePos (Dec3 :> xl) = Pos Dec3 xl+type instance NormalizePos (Dec4 :> xl) = Pos Dec4 xl+type instance NormalizePos (Dec5 :> xl) = Pos Dec5 xl+type instance NormalizePos (Dec6 :> xl) = Pos Dec6 xl+type instance NormalizePos (Dec7 :> xl) = Pos Dec7 xl+type instance NormalizePos (Dec8 :> xl) = Pos Dec8 xl+type instance NormalizePos (Dec9 :> xl) = Pos Dec9 xl++type family NormalizeNeg x+type instance NormalizeNeg EndDesc = Zero+type instance NormalizeNeg (Dec0 :> xl) = NormalizeNeg xl+type instance NormalizeNeg (Dec1 :> xl) = Neg Dec1 xl+type instance NormalizeNeg (Dec2 :> xl) = Neg Dec2 xl+type instance NormalizeNeg (Dec3 :> xl) = Neg Dec3 xl+type instance NormalizeNeg (Dec4 :> xl) = Neg Dec4 xl+type instance NormalizeNeg (Dec5 :> xl) = Neg Dec5 xl+type instance NormalizeNeg (Dec6 :> xl) = Neg Dec6 xl+type instance NormalizeNeg (Dec7 :> xl) = Neg Dec7 xl+type instance NormalizeNeg (Dec8 :> xl) = Neg Dec8 xl+type instance NormalizeNeg (Dec9 :> xl) = Neg Dec9 xl++type family Ascending x y+type instance Ascending y EndDesc = y+type instance Ascending y (xh :> xl) = Ascending (y :< xh) xl++type AscendingNonEmpty x xs = Ascending (EndAsc:<x) xs++type family Descending x y+type instance Descending EndAsc y = y+type instance Descending (xh :< xl) y = Descending xh (xl :> y)++type NormalizePosDesc xs = NormalizePos (Descending xs EndDesc)+type NormalizeNegDesc xs = NormalizeNeg (Descending xs EndDesc)+++-- type family Op.IsPositive x+type instance Op.IsPositive (Dec x) = IsPositive x+type family IsPositive x+type instance IsPositive (Neg _x _xs) = False+type instance IsPositive Zero = False+type instance IsPositive (Pos _x _xs) = True++-- type family Op.IsZero x+type instance Op.IsZero (Dec x) = IsZero x+type family IsZero x+type instance IsZero (Neg _x _xs) = False+type instance IsZero Zero = True+type instance IsZero (Pos _x _xs) = False++-- type family Op.IsNegative x+type instance Op.IsNegative (Dec x) = IsNegative x+type family IsNegative x+type instance IsNegative (Neg _x _xs) = True+type instance IsNegative Zero = False+type instance IsNegative (Pos _x _xs) = False++-- type family Op.IsNatural x+type instance Op.IsNatural (Dec x) = IsNatural x+type family IsNatural x+type instance IsNatural (Neg _x _xs) = False+type instance IsNatural Zero = True+type instance IsNatural (Pos _x _xs) = True++-- type family Op.Negate x+type instance Op.Negate (Dec x) = Dec (Negate x)++type family Negate x+type instance Negate Zero = Zero+type instance Negate (Neg x xs) = Pos x xs+type instance Negate (Pos x xs) = Neg x xs++-- type family Op.One r+type instance Op.One Decimal = Dec One+type One = Pos Dec1 EndDesc++-- type family Op.Succ x+type instance Op.Succ (Dec x) = Dec (Succ x)++type family Succ x+type instance Succ Zero = One+type instance Succ (Pos x xs) =+ NormalizePosDesc (SuccAsc (AscendingNonEmpty x xs))+type instance Succ (Neg x xs) =+ NormalizeNegDesc (PredAsc (AscendingNonEmpty x xs))++type family SuccAsc x+type instance SuccAsc EndAsc = EndAsc :< Dec1+type instance SuccAsc (x :< Dec0) = x :< Dec1+type instance SuccAsc (x :< Dec1) = x :< Dec2+type instance SuccAsc (x :< Dec2) = x :< Dec3+type instance SuccAsc (x :< Dec3) = x :< Dec4+type instance SuccAsc (x :< Dec4) = x :< Dec5+type instance SuccAsc (x :< Dec5) = x :< Dec6+type instance SuccAsc (x :< Dec6) = x :< Dec7+type instance SuccAsc (x :< Dec7) = x :< Dec8+type instance SuccAsc (x :< Dec8) = x :< Dec9+type instance SuccAsc (x :< Dec9) = SuccAsc x :< Dec0++-- type family Op.Pred x+type instance Op.Pred (Dec x) = Dec (Pred x)++type family Pred x+type instance Pred Zero = Neg Dec1 EndDesc+type instance Pred (Neg x xs) =+ NormalizeNegDesc (SuccAsc (AscendingNonEmpty x xs))+type instance Pred (Pos x xs) =+ NormalizePosDesc (PredAsc (AscendingNonEmpty x xs))++type family PredAsc x+type instance PredAsc (x :< Dec0) = PredAsc x :< Dec9+type instance PredAsc (x :< Dec1) = x :< Dec0+type instance PredAsc (x :< Dec2) = x :< Dec1+type instance PredAsc (x :< Dec3) = x :< Dec2+type instance PredAsc (x :< Dec4) = x :< Dec3+type instance PredAsc (x :< Dec5) = x :< Dec4+type instance PredAsc (x :< Dec6) = x :< Dec5+type instance PredAsc (x :< Dec7) = x :< Dec6+type instance PredAsc (x :< Dec8) = x :< Dec7+type instance PredAsc (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 @SuccAsc 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 "SuccAsc" 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 = SuccAsc 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 = SuccAsc x+type instance AddCarry Dec2 Dec9 x = SuccAsc 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 = SuccAsc x+type instance AddCarry Dec3 Dec8 x = SuccAsc x+type instance AddCarry Dec3 Dec9 x = SuccAsc 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 = SuccAsc x+type instance AddCarry Dec4 Dec7 x = SuccAsc x+type instance AddCarry Dec4 Dec8 x = SuccAsc x+type instance AddCarry Dec4 Dec9 x = SuccAsc 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 = SuccAsc x+type instance AddCarry Dec5 Dec6 x = SuccAsc x+type instance AddCarry Dec5 Dec7 x = SuccAsc x+type instance AddCarry Dec5 Dec8 x = SuccAsc x+type instance AddCarry Dec5 Dec9 x = SuccAsc 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 = SuccAsc x+type instance AddCarry Dec6 Dec5 x = SuccAsc x+type instance AddCarry Dec6 Dec6 x = SuccAsc x+type instance AddCarry Dec6 Dec7 x = SuccAsc x+type instance AddCarry Dec6 Dec8 x = SuccAsc x+type instance AddCarry Dec6 Dec9 x = SuccAsc 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 = SuccAsc x+type instance AddCarry Dec7 Dec4 x = SuccAsc x+type instance AddCarry Dec7 Dec5 x = SuccAsc x+type instance AddCarry Dec7 Dec6 x = SuccAsc x+type instance AddCarry Dec7 Dec7 x = SuccAsc x+type instance AddCarry Dec7 Dec8 x = SuccAsc x+type instance AddCarry Dec7 Dec9 x = SuccAsc x++type instance AddCarry Dec8 Dec0 x = Id x+type instance AddCarry Dec8 Dec1 x = Id x+type instance AddCarry Dec8 Dec2 x = SuccAsc x+type instance AddCarry Dec8 Dec3 x = SuccAsc x+type instance AddCarry Dec8 Dec4 x = SuccAsc x+type instance AddCarry Dec8 Dec5 x = SuccAsc x+type instance AddCarry Dec8 Dec6 x = SuccAsc x+type instance AddCarry Dec8 Dec7 x = SuccAsc x+type instance AddCarry Dec8 Dec8 x = SuccAsc x+type instance AddCarry Dec8 Dec9 x = SuccAsc x++type instance AddCarry Dec9 Dec0 x = Id x+type instance AddCarry Dec9 Dec1 x = SuccAsc x+type instance AddCarry Dec9 Dec2 x = SuccAsc x+type instance AddCarry Dec9 Dec3 x = SuccAsc x+type instance AddCarry Dec9 Dec4 x = SuccAsc x+type instance AddCarry Dec9 Dec5 x = SuccAsc x+type instance AddCarry Dec9 Dec6 x = SuccAsc x+type instance AddCarry Dec9 Dec7 x = SuccAsc x+type instance AddCarry Dec9 Dec8 x = SuccAsc x+type instance AddCarry Dec9 Dec9 x = SuccAsc x++type family AddAsc x y+type instance AddAsc EndAsc y = y+type instance AddAsc (xh :< xl) EndAsc = xh :< xl+type instance AddAsc (xh :< xl) (yh :< yl) =+ AddCarry xl yl (AddAsc xh yh) :< AddDigit xl yl++type AddPos x xs y ys =+ NormalizePosDesc+ (AddAsc (AscendingNonEmpty x xs) (AscendingNonEmpty y ys))++-- type family x Op.:+: y+type instance Dec x Op.:+: Dec y = Dec (x :+: y)++type family x :+: y+type instance (Zero ) :+: y = y+type instance (Pos x xs) :+: (Zero ) = Pos x xs+type instance (Neg x xs) :+: (Zero ) = Neg x xs+type instance (Pos x xs) :+: (Pos y ys) = AddPos x xs y ys+type instance (Neg x xs) :+: (Neg y ys) = Negate (AddPos x xs y ys)+type instance (Pos x xs) :+: (Neg y ys) = SubPos x xs y ys+type instance (Neg x xs) :+: (Pos y ys) = SubPos y ys x xs++--------------------+-- 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 @PredAsc z@+type family Borrow x y z+-- putStr $ unlines $ concat $ [ [ "type instance Borrow Dec" ++ show x ++ " Dec" ++ show y ++ " x = " ++ (if x < y then "PredAsc" else "Id") ++ " x" | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]+type instance Borrow Dec0 Dec0 x = Id x+type instance Borrow Dec0 Dec1 x = PredAsc x+type instance Borrow Dec0 Dec2 x = PredAsc x+type instance Borrow Dec0 Dec3 x = PredAsc x+type instance Borrow Dec0 Dec4 x = PredAsc x+type instance Borrow Dec0 Dec5 x = PredAsc x+type instance Borrow Dec0 Dec6 x = PredAsc x+type instance Borrow Dec0 Dec7 x = PredAsc x+type instance Borrow Dec0 Dec8 x = PredAsc x+type instance Borrow Dec0 Dec9 x = PredAsc x++type instance Borrow Dec1 Dec0 x = Id x+type instance Borrow Dec1 Dec1 x = Id x+type instance Borrow Dec1 Dec2 x = PredAsc x+type instance Borrow Dec1 Dec3 x = PredAsc x+type instance Borrow Dec1 Dec4 x = PredAsc x+type instance Borrow Dec1 Dec5 x = PredAsc x+type instance Borrow Dec1 Dec6 x = PredAsc x+type instance Borrow Dec1 Dec7 x = PredAsc x+type instance Borrow Dec1 Dec8 x = PredAsc x+type instance Borrow Dec1 Dec9 x = PredAsc 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 = PredAsc x+type instance Borrow Dec2 Dec4 x = PredAsc x+type instance Borrow Dec2 Dec5 x = PredAsc x+type instance Borrow Dec2 Dec6 x = PredAsc x+type instance Borrow Dec2 Dec7 x = PredAsc x+type instance Borrow Dec2 Dec8 x = PredAsc x+type instance Borrow Dec2 Dec9 x = PredAsc 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 = PredAsc x+type instance Borrow Dec3 Dec5 x = PredAsc x+type instance Borrow Dec3 Dec6 x = PredAsc x+type instance Borrow Dec3 Dec7 x = PredAsc x+type instance Borrow Dec3 Dec8 x = PredAsc x+type instance Borrow Dec3 Dec9 x = PredAsc 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 = PredAsc x+type instance Borrow Dec4 Dec6 x = PredAsc x+type instance Borrow Dec4 Dec7 x = PredAsc x+type instance Borrow Dec4 Dec8 x = PredAsc x+type instance Borrow Dec4 Dec9 x = PredAsc 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 = PredAsc x+type instance Borrow Dec5 Dec7 x = PredAsc x+type instance Borrow Dec5 Dec8 x = PredAsc x+type instance Borrow Dec5 Dec9 x = PredAsc 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 = PredAsc x+type instance Borrow Dec6 Dec8 x = PredAsc x+type instance Borrow Dec6 Dec9 x = PredAsc 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 = PredAsc x+type instance Borrow Dec7 Dec9 x = PredAsc 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 = PredAsc 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 SubAsc x y+type instance SubAsc x EndAsc = x+type instance SubAsc (xh :< xl) (yh :< yl) =+ SubAsc (Borrow xl yl xh) yh :< SubDigit xl yl++type family SubOrd c x y+type instance SubOrd GT x y = NormalizePosDesc (SubAsc x y)+type instance SubOrd EQ _x _y = Zero+type instance SubOrd LT x y = NormalizeNegDesc (SubAsc y x)++type SubCmp x y = SubOrd (CompareAsc x y EQ) x y++type SubPos x xs y ys =+ SubCmp (AscendingNonEmpty x xs) (AscendingNonEmpty y ys)+++-- type family x Op.:-: y+type instance Dec x Op.:-: Dec y = Dec (x :-: y)++type x :-: y = x :+: Negate y+++--------------------+-- Multiplication++-- type family Mul2 x+type instance Op.Mul2 (Dec x) = Dec (x :+: x)+type Mul2Asc x = AddAsc x x++-- type family x Op.:*: y+type instance (Dec x) Op.:*: (Dec y) = Dec (x :*: y)++type family x :*: y+type instance Zero :*: _y = Zero+type instance (Pos _x _xs) :*: Zero = Zero+type instance (Neg _x _xs) :*: Zero = Zero+type instance (Pos x xs) :*: (Pos y ys) = NormalizePosDesc (MulPos x xs y ys)+type instance (Neg x xs) :*: (Neg y ys) = NormalizePosDesc (MulPos x xs y ys)+type instance (Pos x xs) :*: (Neg y ys) = NormalizeNegDesc (MulPos x xs y ys)+type instance (Neg x xs) :*: (Pos y ys) = NormalizeNegDesc (MulPos x xs y ys)++type MulPos x xs y ys =+ MulScaleAsc (AscendingNonEmpty x xs) (AscendingNonEmpty y ys)++{-+type MulPos x xs y ys =+ MulAsc (AscendingNonEmpty x xs) (Pos y ys) EndAsc+-}++type family MulAsc x y z+type instance MulAsc _x Zero z = z+type instance MulAsc x (Pos y ys) z =+ MulAsc (Mul2Asc x) (Div2 (Pos y ys))+ (If (IsEven (Pos y ys)) z (AddAsc z x))++++-----------+-- Scale++type family MulLo x y+-- putStr $ unlines $ concat $ [ [ "type instance MulLo Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x*y) `mod` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]++type instance MulLo Dec0 Dec0 = Dec0+type instance MulLo Dec0 Dec1 = Dec0+type instance MulLo Dec0 Dec2 = Dec0+type instance MulLo Dec0 Dec3 = Dec0+type instance MulLo Dec0 Dec4 = Dec0+type instance MulLo Dec0 Dec5 = Dec0+type instance MulLo Dec0 Dec6 = Dec0+type instance MulLo Dec0 Dec7 = Dec0+type instance MulLo Dec0 Dec8 = Dec0+type instance MulLo Dec0 Dec9 = Dec0++type instance MulLo Dec1 Dec0 = Dec0+type instance MulLo Dec1 Dec1 = Dec1+type instance MulLo Dec1 Dec2 = Dec2+type instance MulLo Dec1 Dec3 = Dec3+type instance MulLo Dec1 Dec4 = Dec4+type instance MulLo Dec1 Dec5 = Dec5+type instance MulLo Dec1 Dec6 = Dec6+type instance MulLo Dec1 Dec7 = Dec7+type instance MulLo Dec1 Dec8 = Dec8+type instance MulLo Dec1 Dec9 = Dec9++type instance MulLo Dec2 Dec0 = Dec0+type instance MulLo Dec2 Dec1 = Dec2+type instance MulLo Dec2 Dec2 = Dec4+type instance MulLo Dec2 Dec3 = Dec6+type instance MulLo Dec2 Dec4 = Dec8+type instance MulLo Dec2 Dec5 = Dec0+type instance MulLo Dec2 Dec6 = Dec2+type instance MulLo Dec2 Dec7 = Dec4+type instance MulLo Dec2 Dec8 = Dec6+type instance MulLo Dec2 Dec9 = Dec8++type instance MulLo Dec3 Dec0 = Dec0+type instance MulLo Dec3 Dec1 = Dec3+type instance MulLo Dec3 Dec2 = Dec6+type instance MulLo Dec3 Dec3 = Dec9+type instance MulLo Dec3 Dec4 = Dec2+type instance MulLo Dec3 Dec5 = Dec5+type instance MulLo Dec3 Dec6 = Dec8+type instance MulLo Dec3 Dec7 = Dec1+type instance MulLo Dec3 Dec8 = Dec4+type instance MulLo Dec3 Dec9 = Dec7++type instance MulLo Dec4 Dec0 = Dec0+type instance MulLo Dec4 Dec1 = Dec4+type instance MulLo Dec4 Dec2 = Dec8+type instance MulLo Dec4 Dec3 = Dec2+type instance MulLo Dec4 Dec4 = Dec6+type instance MulLo Dec4 Dec5 = Dec0+type instance MulLo Dec4 Dec6 = Dec4+type instance MulLo Dec4 Dec7 = Dec8+type instance MulLo Dec4 Dec8 = Dec2+type instance MulLo Dec4 Dec9 = Dec6++type instance MulLo Dec5 Dec0 = Dec0+type instance MulLo Dec5 Dec1 = Dec5+type instance MulLo Dec5 Dec2 = Dec0+type instance MulLo Dec5 Dec3 = Dec5+type instance MulLo Dec5 Dec4 = Dec0+type instance MulLo Dec5 Dec5 = Dec5+type instance MulLo Dec5 Dec6 = Dec0+type instance MulLo Dec5 Dec7 = Dec5+type instance MulLo Dec5 Dec8 = Dec0+type instance MulLo Dec5 Dec9 = Dec5++type instance MulLo Dec6 Dec0 = Dec0+type instance MulLo Dec6 Dec1 = Dec6+type instance MulLo Dec6 Dec2 = Dec2+type instance MulLo Dec6 Dec3 = Dec8+type instance MulLo Dec6 Dec4 = Dec4+type instance MulLo Dec6 Dec5 = Dec0+type instance MulLo Dec6 Dec6 = Dec6+type instance MulLo Dec6 Dec7 = Dec2+type instance MulLo Dec6 Dec8 = Dec8+type instance MulLo Dec6 Dec9 = Dec4++type instance MulLo Dec7 Dec0 = Dec0+type instance MulLo Dec7 Dec1 = Dec7+type instance MulLo Dec7 Dec2 = Dec4+type instance MulLo Dec7 Dec3 = Dec1+type instance MulLo Dec7 Dec4 = Dec8+type instance MulLo Dec7 Dec5 = Dec5+type instance MulLo Dec7 Dec6 = Dec2+type instance MulLo Dec7 Dec7 = Dec9+type instance MulLo Dec7 Dec8 = Dec6+type instance MulLo Dec7 Dec9 = Dec3++type instance MulLo Dec8 Dec0 = Dec0+type instance MulLo Dec8 Dec1 = Dec8+type instance MulLo Dec8 Dec2 = Dec6+type instance MulLo Dec8 Dec3 = Dec4+type instance MulLo Dec8 Dec4 = Dec2+type instance MulLo Dec8 Dec5 = Dec0+type instance MulLo Dec8 Dec6 = Dec8+type instance MulLo Dec8 Dec7 = Dec6+type instance MulLo Dec8 Dec8 = Dec4+type instance MulLo Dec8 Dec9 = Dec2++type instance MulLo Dec9 Dec0 = Dec0+type instance MulLo Dec9 Dec1 = Dec9+type instance MulLo Dec9 Dec2 = Dec8+type instance MulLo Dec9 Dec3 = Dec7+type instance MulLo Dec9 Dec4 = Dec6+type instance MulLo Dec9 Dec5 = Dec5+type instance MulLo Dec9 Dec6 = Dec4+type instance MulLo Dec9 Dec7 = Dec3+type instance MulLo Dec9 Dec8 = Dec2+type instance MulLo Dec9 Dec9 = Dec1+++type family MulHi x y+-- putStr $ unlines $ concat $ [ [ "type instance MulHi Dec" ++ show x ++ " Dec" ++ show y ++ " = Dec" ++ show ((x*y) `div` 10) | y <- [0..9] ] ++ [ "" ] | x <- [0..9] ]++type instance MulHi Dec0 Dec0 = Dec0+type instance MulHi Dec0 Dec1 = Dec0+type instance MulHi Dec0 Dec2 = Dec0+type instance MulHi Dec0 Dec3 = Dec0+type instance MulHi Dec0 Dec4 = Dec0+type instance MulHi Dec0 Dec5 = Dec0+type instance MulHi Dec0 Dec6 = Dec0+type instance MulHi Dec0 Dec7 = Dec0+type instance MulHi Dec0 Dec8 = Dec0+type instance MulHi Dec0 Dec9 = Dec0++type instance MulHi Dec1 Dec0 = Dec0+type instance MulHi Dec1 Dec1 = Dec0+type instance MulHi Dec1 Dec2 = Dec0+type instance MulHi Dec1 Dec3 = Dec0+type instance MulHi Dec1 Dec4 = Dec0+type instance MulHi Dec1 Dec5 = Dec0+type instance MulHi Dec1 Dec6 = Dec0+type instance MulHi Dec1 Dec7 = Dec0+type instance MulHi Dec1 Dec8 = Dec0+type instance MulHi Dec1 Dec9 = Dec0++type instance MulHi Dec2 Dec0 = Dec0+type instance MulHi Dec2 Dec1 = Dec0+type instance MulHi Dec2 Dec2 = Dec0+type instance MulHi Dec2 Dec3 = Dec0+type instance MulHi Dec2 Dec4 = Dec0+type instance MulHi Dec2 Dec5 = Dec1+type instance MulHi Dec2 Dec6 = Dec1+type instance MulHi Dec2 Dec7 = Dec1+type instance MulHi Dec2 Dec8 = Dec1+type instance MulHi Dec2 Dec9 = Dec1++type instance MulHi Dec3 Dec0 = Dec0+type instance MulHi Dec3 Dec1 = Dec0+type instance MulHi Dec3 Dec2 = Dec0+type instance MulHi Dec3 Dec3 = Dec0+type instance MulHi Dec3 Dec4 = Dec1+type instance MulHi Dec3 Dec5 = Dec1+type instance MulHi Dec3 Dec6 = Dec1+type instance MulHi Dec3 Dec7 = Dec2+type instance MulHi Dec3 Dec8 = Dec2+type instance MulHi Dec3 Dec9 = Dec2++type instance MulHi Dec4 Dec0 = Dec0+type instance MulHi Dec4 Dec1 = Dec0+type instance MulHi Dec4 Dec2 = Dec0+type instance MulHi Dec4 Dec3 = Dec1+type instance MulHi Dec4 Dec4 = Dec1+type instance MulHi Dec4 Dec5 = Dec2+type instance MulHi Dec4 Dec6 = Dec2+type instance MulHi Dec4 Dec7 = Dec2+type instance MulHi Dec4 Dec8 = Dec3+type instance MulHi Dec4 Dec9 = Dec3++type instance MulHi Dec5 Dec0 = Dec0+type instance MulHi Dec5 Dec1 = Dec0+type instance MulHi Dec5 Dec2 = Dec1+type instance MulHi Dec5 Dec3 = Dec1+type instance MulHi Dec5 Dec4 = Dec2+type instance MulHi Dec5 Dec5 = Dec2+type instance MulHi Dec5 Dec6 = Dec3+type instance MulHi Dec5 Dec7 = Dec3+type instance MulHi Dec5 Dec8 = Dec4+type instance MulHi Dec5 Dec9 = Dec4++type instance MulHi Dec6 Dec0 = Dec0+type instance MulHi Dec6 Dec1 = Dec0+type instance MulHi Dec6 Dec2 = Dec1+type instance MulHi Dec6 Dec3 = Dec1+type instance MulHi Dec6 Dec4 = Dec2+type instance MulHi Dec6 Dec5 = Dec3+type instance MulHi Dec6 Dec6 = Dec3+type instance MulHi Dec6 Dec7 = Dec4+type instance MulHi Dec6 Dec8 = Dec4+type instance MulHi Dec6 Dec9 = Dec5++type instance MulHi Dec7 Dec0 = Dec0+type instance MulHi Dec7 Dec1 = Dec0+type instance MulHi Dec7 Dec2 = Dec1+type instance MulHi Dec7 Dec3 = Dec2+type instance MulHi Dec7 Dec4 = Dec2+type instance MulHi Dec7 Dec5 = Dec3+type instance MulHi Dec7 Dec6 = Dec4+type instance MulHi Dec7 Dec7 = Dec4+type instance MulHi Dec7 Dec8 = Dec5+type instance MulHi Dec7 Dec9 = Dec6++type instance MulHi Dec8 Dec0 = Dec0+type instance MulHi Dec8 Dec1 = Dec0+type instance MulHi Dec8 Dec2 = Dec1+type instance MulHi Dec8 Dec3 = Dec2+type instance MulHi Dec8 Dec4 = Dec3+type instance MulHi Dec8 Dec5 = Dec4+type instance MulHi Dec8 Dec6 = Dec4+type instance MulHi Dec8 Dec7 = Dec5+type instance MulHi Dec8 Dec8 = Dec6+type instance MulHi Dec8 Dec9 = Dec7++type instance MulHi Dec9 Dec0 = Dec0+type instance MulHi Dec9 Dec1 = Dec0+type instance MulHi Dec9 Dec2 = Dec1+type instance MulHi Dec9 Dec3 = Dec2+type instance MulHi Dec9 Dec4 = Dec3+type instance MulHi Dec9 Dec5 = Dec4+type instance MulHi Dec9 Dec6 = Dec5+type instance MulHi Dec9 Dec7 = Dec6+type instance MulHi Dec9 Dec8 = Dec7+type instance MulHi Dec9 Dec9 = Dec8+++type family ScaleLo x ys+type instance ScaleLo _x EndAsc = EndAsc+type instance ScaleLo x (yh :< yl) = ScaleLo x yh :< MulLo x yl++type family ScaleHi x ys+type instance ScaleHi _x EndAsc = EndAsc+type instance ScaleHi x (yh :< yl) = ScaleHi x yh :< MulHi x yl++type family MulScaleAsc xs ys+type instance MulScaleAsc EndAsc _ys = EndAsc+type instance MulScaleAsc (xh :< xl) ys =+ AddAsc+ (ScaleLo xl ys)+ (AddAsc (MulScaleAsc xh ys) (ScaleHi xl ys) :< Dec0)+++-----------+-- Division / Modulus++-- type family Op.IsEven x+type instance Op.IsEven (Dec x) = IsEven x++type family IsEven x+type instance IsEven Zero = True+type instance IsEven (Neg x xs) = IsEvenAsc (AscendingNonEmpty x xs)+type instance IsEven (Pos x xs) = IsEvenAsc (AscendingNonEmpty x xs)++type family IsEvenAsc x+type instance IsEvenAsc EndAsc = True+type instance IsEvenAsc (_xh :< xl) = IsEvenDigit xl++type family IsEvenDigit x+type instance IsEvenDigit Dec0 = True+type instance IsEvenDigit Dec1 = False+type instance IsEvenDigit Dec2 = True+type instance IsEvenDigit Dec3 = False+type instance IsEvenDigit Dec4 = True+type instance IsEvenDigit Dec5 = False+type instance IsEvenDigit Dec6 = True+type instance IsEvenDigit Dec7 = False+type instance IsEvenDigit Dec8 = True+type instance IsEvenDigit Dec9 = False++-- type family Op.Div2 x+type instance Op.Div2 (Dec x) = Dec (Div2 x)++type family Div2 x+type instance Div2 Zero = Zero+type instance Div2 (Neg x xs) =+ NormalizeNegDesc (Div2Asc (AscendingNonEmpty x xs))+type instance Div2 (Pos x xs) =+ NormalizePosDesc (Div2Asc (AscendingNonEmpty x xs))++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 Div2Asc x+type instance Div2Asc EndAsc = EndAsc+type instance Div2Asc (xh :< xl) =+ Div2Pos xh (Div2Digit xl) (If (IsEvenAsc xh) Dec0 Dec5)++type Div2Pos xh xl rem =+ AddCarry xl rem (Div2Asc xh) :< AddDigit xl rem++---------------+-- Exponentiation++type instance Op.Pow2 (Dec x) = Dec (Pow2 x)++type family Pow2 x+type instance Pow2 Zero = One+type instance Pow2 (Pos x xs) =+ NormalizePosDesc (Pow2Asc (Pos x xs) (EndAsc :< Dec1))++type family Pow2Asc x y+type instance Pow2Asc Zero y = y+type instance Pow2Asc (Pos x xs) y =+ Pow2Asc (Pred (Pos x xs)) (Mul2Asc y)++---------------+-- Logarithm+type instance Op.Log2Ceil (Dec x) = Dec (Log2Ceil x)++type family Log2Ceil x+type instance Log2Ceil (Pos x xs) =+ NormalizePosDesc (Log2C (Pred (Pos x xs)) EndAsc)++type family Log2C x y+type instance Log2C Zero y = y+type instance Log2C (Pos x xs) y = Log2C (Div2 (Pos x xs)) (SuccAsc y)++---------------+-- Comparison++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 Ord.Compare (Dec x) (Dec y) = Compare x y+type family Compare x y+type instance Compare (Pos x xs) (Pos y ys) = ComparePos x xs y ys+type instance Compare (Neg x xs) (Neg y ys) = ComparePos y ys x xs+type instance Compare (Pos _x _xs) (Neg _y _ys) = GT+type instance Compare (Neg _x _xs) (Pos _y _ys) = LT+type instance Compare (Pos _x _xs) (Zero ) = GT+type instance Compare (Neg _x _xs) (Zero ) = LT+type instance Compare (Zero ) (Neg _y _ys) = GT+type instance Compare (Zero ) (Pos _y _ys) = LT+type instance Compare (Zero ) (Zero ) = EQ++type ComparePos x xs y ys =+ CompareAsc (AscendingNonEmpty x xs) (AscendingNonEmpty y ys) EQ++type family CompareAsc x y c+type instance CompareAsc EndAsc EndAsc c = c+type instance CompareAsc EndAsc (_h :< _l) _c = LT+type instance CompareAsc (_h :< _l) EndAsc _c = GT+type instance CompareAsc (xh :< xl) (yh :< yl) GT =+ CompareDiff xh yh (CompareDigit xl yl) GT+type instance CompareAsc (xh :< xl) (yh :< yl) EQ =+ CompareAsc xh yh (CompareDigit xl yl)+type instance CompareAsc (xh :< xl) (yh :< yl) LT =+ CompareDiff xh yh (CompareDigit xl yl) LT++type family CompareDiff x y c l+type instance CompareDiff x y LT _c = CompareAsc x y LT+type instance CompareDiff x y EQ c = CompareAsc x y c+type instance CompareDiff x y GT _c = CompareAsc x y GT+++class x :<: y; instance (x Ord.:<: y) => Dec x :<: Dec y+class x :<=: y; instance (x Ord.:<=: y) => Dec x :<=: Dec y+class x :>=: y; instance (x Ord.:>=: y) => Dec x :>=: Dec y+class x :>: y; instance (x Ord.:>: y) => Dec x :>: Dec y+class x :==: y; instance (x Ord.:==: y) => Dec x :==: Dec y+class x :/=: y; instance (x Ord.:/=: y) => Dec x :/=: Dec y+++type GreaterPos x xs y ys = Ord.IsGT (ComparePos x xs y ys)++instance Neg x xs :<: Zero+instance Neg x xs :<: Pos y ys+instance Zero :<: Pos y ys++instance (ComparePos x xs y ys ~ GT) => Neg x xs :<: Neg y ys+instance (ComparePos x xs y ys ~ LT) => Pos x xs :<: Pos y ys+++instance Neg x xs :<=: Zero+instance Neg x xs :<=: Pos y ys+instance Zero :<=: Zero+instance Zero :<=: Pos y ys++instance (GreaterPos y ys x xs ~ False) => Neg x xs :<=: Neg y ys+instance (GreaterPos x xs y ys ~ False) => Pos x xs :<=: Pos y ys+++instance Zero :>: Neg y ys+instance Pos x xs :>: Neg y ys+instance Pos x xs :>: Zero++instance (ComparePos x xs y ys ~ LT) => Neg x xs :>: Neg y ys+instance (ComparePos x xs y ys ~ GT) => Pos x xs :>: Pos y ys+++instance Zero :>=: Neg y ys+instance Pos x xs :>=: Neg y ys+instance Zero :>=: Zero+instance Pos x xs :>=: Zero++instance (GreaterPos x xs y ys ~ False) => Neg x xs :>=: Neg y ys+instance (GreaterPos y ys x xs ~ False) => Pos x xs :>=: Pos y ys+++instance Zero :==: Zero++instance (ComparePos x xs y ys ~ EQ) => Neg x xs :==: Neg y ys+instance (ComparePos x xs y ys ~ EQ) => Pos x xs :==: Pos y ys+++instance Zero :/=: Neg y ys+instance Pos x xs :/=: Neg y ys+instance Neg x xs :/=: Zero+instance Pos x xs :/=: Zero+instance Neg x xs :/=: Pos y ys+instance Zero :/=: Pos y ys++instance (Ord.IsEQ (ComparePos x xs y ys) ~ False) => Neg x xs :/=: Neg y ys+instance (Ord.IsEQ (ComparePos x xs y ys) ~ False) => Pos x xs :/=: Pos y ys+++type family FromUnary n+type instance FromUnary Unary.Zero = Zero+type instance FromUnary (Unary.Succ n) = Succ (FromUnary n)++type family ToUnary n+type instance ToUnary Zero = Unary.Zero+type instance ToUnary (Pos x xs) = ToUnaryAcc (Digit.ToUnary x) xs++type family ToUnaryAcc m n+type instance ToUnaryAcc m EndDesc = m+type instance ToUnaryAcc m (x :> xs) =+ ToUnaryAcc (UnaryAcc m x) xs++type UnaryAcc m x = Digit.ToUnary x Unary.:+: (m Unary.:*: UnaryLit.U10)
+ src/Type/Data/Num/Decimal/Proof.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE FlexibleContexts #-}++module Type.Data.Num.Decimal.Proof (+ Digits(Digits),+ UnaryNat(UnaryNat), unaryNat,+ UnaryPos(UnaryPos), unaryPos,+ ) where++import qualified Type.Data.Num.Decimal.Digit.Proof as DigitProof+import qualified Type.Data.Num.Decimal.Digit as Digit+import qualified Type.Data.Num.Decimal.Number as Dec+import qualified Type.Data.Num.Unary.Literal as UnaryLit+import qualified Type.Data.Num.Unary.Proof as UnaryProof+import qualified Type.Data.Num.Unary as Unary++import Type.Data.Num.Decimal.Number (Pos, (:>), Natural, Positive, )+++data UnaryNat n = Unary.Natural (Dec.ToUnary n) => UnaryNat++unaryNat :: (Natural n) => UnaryNat n+unaryNat = Dec.switchNat UnaryNat (unaryUnPos unaryPosPos)++unaryUnPos :: UnaryPos n -> UnaryNat n+unaryUnPos UnaryPos = UnaryNat+++data UnaryPos n = Unary.Positive (Dec.ToUnary n) => UnaryPos++unaryPos :: (Positive n) => UnaryPos n+unaryPos = Dec.switchPos unaryPosPos++unaryPosPos :: (Digit.Pos x, Dec.Digits xs) => UnaryPos (Pos x xs)+unaryPosPos =+ withUnaryPosPos $ \x xs ->+ case toUnaryAcc (digitUnaryPos x) xs of+ UnaryProof.Pos -> UnaryPos+++withUnaryPosPos ::+ (Digit.Pos x, Dec.Digits xs) =>+ (DigitProof.UnaryPos x -> Digits xs ->+ UnaryPos (Pos x xs)) ->+ UnaryPos (Pos x xs)+withUnaryPosPos f =+ f DigitProof.unaryPos Digits++digitUnaryPos ::+ DigitProof.UnaryPos x -> UnaryProof.Pos (Digit.ToUnary x)+digitUnaryPos DigitProof.UnaryPos = UnaryProof.Pos+++data Digits xs = (Dec.Digits xs) => Digits++newtype+ ToUnaryAcc m xs =+ ToUnaryAcc {runToUnaryAcc ::+ UnaryProof.Pos m -> Digits xs ->+ UnaryProof.Pos (Dec.ToUnaryAcc m xs)}++toUnaryAcc ::+ UnaryProof.Pos m -> Digits xs ->+ UnaryProof.Pos (Dec.ToUnaryAcc m xs)+toUnaryAcc m y@Digits =+ runToUnaryAcc+ (Dec.switchDigits+ (ToUnaryAcc $ \ UnaryProof.Pos _ -> UnaryProof.Pos)+ (ToUnaryAcc $ \ acc xt ->+ toUnaryAcc+ (unaryAcc acc (DigitProof.unaryNatImpl (headDigits xt))+ UnaryProof.Pos)+ (tailDigits xt)))+ m y+++headDigits :: (Digit.C x) => Digits (x :> xs) -> DigitProof.Nat x+headDigits Digits = DigitProof.Nat++tailDigits :: Dec.Digits xs => Digits (x :> xs) -> Digits xs+tailDigits Digits = Digits+++unaryAcc ::+ UnaryProof.Pos m -> UnaryProof.Nat x -> UnaryProof.Pos UnaryLit.U10 ->+ UnaryProof.Pos (x Unary.:+: (m Unary.:*: UnaryLit.U10))+unaryAcc m x ten =+ UnaryProof.addPosR x $ UnaryProof.mulPos m ten
+ src/Type/Data/Num/Unary.hs view
@@ -0,0 +1,147 @@+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE GADTs #-}+module Type.Data.Num.Unary (+ Unary, unary, Un, Zero, Succ, zero, succ,+ HeadSingleton(Zero, Succ), headSingleton,+ Singleton(..), singleton, singletonFromProxy,+ integerFromSingleton, integralFromSingleton,+ integralFromProxy,+ Natural(..), Positive(..),+ (:+:), (:*:),+ reifyNatural,+ ) where++import qualified Type.Data.Num as Num+import qualified Type.Base.Proxy as Proxy+import Type.Base.Proxy (Proxy(Proxy))++import Text.Printf (printf)++import Prelude hiding (succ)+++-- | Representation name for unary type level numbers.+data Unary++data Un x+data Zero+data Succ x+{-+Negative numbers could be represented by Pred+but this would complicate our proofs.+We would require that a number contains only Succ or Pred.+Alternative:+Int = Zero | Neg Nat | Pos Nat+Nat = None | Succ Nat+-}++zero :: Proxy Zero+zero = Proxy++succ :: Proxy n -> Proxy (Succ n)+succ Proxy = Proxy+++class Natural n where+ switchNat ::+ f Zero ->+ (forall m. (Natural m) => f (Succ m)) ->+ f n++instance Natural Zero where switchNat x _ = x+instance Natural n => Natural (Succ n) where switchNat _ x = x+++class (Natural n) => Positive n where+ switchPos ::+ (forall m. (Natural m) => f (Succ m)) ->+ f n++instance Natural n => Positive (Succ n) where switchPos x = x+++type family x :+: y+type instance x :+: Zero = x+type instance x :+: Succ y = Succ (x :+: y)++type family x :*: y+type instance _x :*: Zero = Zero+type instance x :*: Succ y = x :+: (x :*: y)++++data HeadSingleton n where+ Zero :: HeadSingleton Zero+ Succ :: (Natural n) => HeadSingleton (Succ n)++headSingleton :: (Natural n) => HeadSingleton n+headSingleton = switchNat Zero Succ+++newtype Singleton n = Singleton Integer++instance (Natural n) => Num.Integer (Un n) where+ singleton = singletonToGeneric singleton+ type Repr (Un n) = Unary++singletonToGeneric :: Singleton n -> Num.Singleton (Un n)+singletonToGeneric (Singleton n) = Num.Singleton n++singleton :: (Natural n) => Singleton n+singleton =+ switchNat+ (Singleton 0)+ (succSingleton singleton)++succSingleton ::+ (Natural n) =>+ Singleton n -> Singleton (Succ n)+succSingleton (Singleton n) = Singleton $ n+1+++integerFromSingleton :: (Natural n) => Singleton n -> Integer+integerFromSingleton (Singleton n) = n++integralFromSingleton :: (Natural n, Num a) => Singleton n -> a+integralFromSingleton = fromInteger . integerFromSingleton++singletonFromProxy :: (Natural n) => Proxy n -> Singleton n+singletonFromProxy Proxy = singleton++integralFromProxy :: (Natural n, Num a) => Proxy n -> a+integralFromProxy = integralFromSingleton . singletonFromProxy+++instance Num.Representation Unary where+ reifyIntegral _ i k = reifyIntegral i (k . unary)++unary :: Proxy n -> Proxy (Un n)+unary Proxy = Proxy++stripUn :: Proxy (Un n) -> Proxy n+stripUn Proxy = Proxy++reifyIntegral :: Integer -> (forall s. Natural s => Proxy s -> w) -> w+reifyIntegral n f =+ if n < 0+ then error "negative unary numbers not supported so far"+ else reifyNatural n f++reifyNatural :: Integer -> (forall s. Natural s => Proxy s -> w) -> w+reifyNatural n f =+ if n>0+ then reifyNatural (n-1) (f . succ)+ else f zero+++type instance Un x Num.:+: Un y = Un (x :+: y)+type instance Un x Num.:*: Un y = Un (x :*: y)+++instance Natural a => Proxy.Show (Un a) where+ showsPrec prec =+ (\n -> showParen (prec>10) (showString (printf "unary u%d" n)))+ . integerFromSingleton . singletonFromProxy . stripUn
+ src/Type/Data/Num/Unary/Literal.hs view
@@ -0,0 +1,138 @@+module Type.Data.Num.Unary.Literal where++import Type.Data.Num.Unary (Zero, Succ)+import Type.Base.Proxy (Proxy(Proxy))+++type U0 = Zero+type U1 = Succ U0+type U2 = Succ U1+type U3 = Succ U2+type U4 = Succ U3+type U5 = Succ U4+type U6 = Succ U5+type U7 = Succ U6+type U8 = Succ U7+type U9 = Succ U8+type U10 = Succ U9+type U11 = Succ U10+type U12 = Succ U11+type U13 = Succ U12+type U14 = Succ U13+type U15 = Succ U14+type U16 = Succ U15+type U17 = Succ U16+type U18 = Succ U17+type U19 = Succ U18+type U20 = Succ U19+type U21 = Succ U20+type U22 = Succ U21+type U23 = Succ U22+type U24 = Succ U23+type U25 = Succ U24+type U26 = Succ U25+type U27 = Succ U26+type U28 = Succ U27+type U29 = Succ U28+type U30 = Succ U29+type U31 = Succ U30+type U32 = Succ U31+type U33 = Succ U32+type U34 = Succ U33+type U35 = Succ U34+type U36 = Succ U35+type U37 = Succ U36+type U38 = Succ U37+type U39 = Succ U38+type U40 = Succ U39+type U41 = Succ U40+type U42 = Succ U41+type U43 = Succ U42+type U44 = Succ U43+type U45 = Succ U44+type U46 = Succ U45+type U47 = Succ U46+type U48 = Succ U47+type U49 = Succ U48+type U50 = Succ U49+type U51 = Succ U50+type U52 = Succ U51+type U53 = Succ U52+type U54 = Succ U53+type U55 = Succ U54+type U56 = Succ U55+type U57 = Succ U56+type U58 = Succ U57+type U59 = Succ U58+type U60 = Succ U59+type U61 = Succ U60+type U62 = Succ U61+type U63 = Succ U62+type U64 = Succ U63+++u0 :: Proxy U0; u0 = Proxy+u1 :: Proxy U1; u1 = Proxy+u2 :: Proxy U2; u2 = Proxy+u3 :: Proxy U3; u3 = Proxy+u4 :: Proxy U4; u4 = Proxy+u5 :: Proxy U5; u5 = Proxy+u6 :: Proxy U6; u6 = Proxy+u7 :: Proxy U7; u7 = Proxy+u8 :: Proxy U8; u8 = Proxy+u9 :: Proxy U9; u9 = Proxy+u10 :: Proxy U10; u10 = Proxy+u11 :: Proxy U11; u11 = Proxy+u12 :: Proxy U12; u12 = Proxy+u13 :: Proxy U13; u13 = Proxy+u14 :: Proxy U14; u14 = Proxy+u15 :: Proxy U15; u15 = Proxy+u16 :: Proxy U16; u16 = Proxy+u17 :: Proxy U17; u17 = Proxy+u18 :: Proxy U18; u18 = Proxy+u19 :: Proxy U19; u19 = Proxy+u20 :: Proxy U20; u20 = Proxy+u21 :: Proxy U21; u21 = Proxy+u22 :: Proxy U22; u22 = Proxy+u23 :: Proxy U23; u23 = Proxy+u24 :: Proxy U24; u24 = Proxy+u25 :: Proxy U25; u25 = Proxy+u26 :: Proxy U26; u26 = Proxy+u27 :: Proxy U27; u27 = Proxy+u28 :: Proxy U28; u28 = Proxy+u29 :: Proxy U29; u29 = Proxy+u30 :: Proxy U30; u30 = Proxy+u31 :: Proxy U31; u31 = Proxy+u32 :: Proxy U32; u32 = Proxy+u33 :: Proxy U33; u33 = Proxy+u34 :: Proxy U34; u34 = Proxy+u35 :: Proxy U35; u35 = Proxy+u36 :: Proxy U36; u36 = Proxy+u37 :: Proxy U37; u37 = Proxy+u38 :: Proxy U38; u38 = Proxy+u39 :: Proxy U39; u39 = Proxy+u40 :: Proxy U40; u40 = Proxy+u41 :: Proxy U41; u41 = Proxy+u42 :: Proxy U42; u42 = Proxy+u43 :: Proxy U43; u43 = Proxy+u44 :: Proxy U44; u44 = Proxy+u45 :: Proxy U45; u45 = Proxy+u46 :: Proxy U46; u46 = Proxy+u47 :: Proxy U47; u47 = Proxy+u48 :: Proxy U48; u48 = Proxy+u49 :: Proxy U49; u49 = Proxy+u50 :: Proxy U50; u50 = Proxy+u51 :: Proxy U51; u51 = Proxy+u52 :: Proxy U52; u52 = Proxy+u53 :: Proxy U53; u53 = Proxy+u54 :: Proxy U54; u54 = Proxy+u55 :: Proxy U55; u55 = Proxy+u56 :: Proxy U56; u56 = Proxy+u57 :: Proxy U57; u57 = Proxy+u58 :: Proxy U58; u58 = Proxy+u59 :: Proxy U59; u59 = Proxy+u60 :: Proxy U60; u60 = Proxy+u61 :: Proxy U61; u61 = Proxy+u62 :: Proxy U62; u62 = Proxy+u63 :: Proxy U63; u63 = Proxy+u64 :: Proxy U64; u64 = Proxy
+ src/Type/Data/Num/Unary/Proof.hs view
@@ -0,0 +1,167 @@+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE FlexibleContexts #-}+module Type.Data.Num.Unary.Proof (+ Nat(..), Pos(..),+ natFromPos,+ addNat, addPosL, addPosR,+ AddZeroL(..), addZeroL,+ AddComm(..), addComm,+ AddAssoc(..), addAssoc,+ mulNat, mulPos,+ ) where++import Type.Data.Num.Unary+ (Natural, Positive, Zero, Succ, switchNat, switchPos, (:+:), (:*:))++data Nat x = Natural x => Nat+data Pos x = Positive x => Pos+++succNat :: Nat x -> Nat (Succ x)+succNat Nat = Nat++prevNat :: (Natural x) => Nat (Succ x) -> Nat x+prevNat Nat = Nat++posSucc :: Nat x -> Pos (Succ x)+posSucc Nat = Pos++prevPos :: (Natural x) => Pos (Succ x) -> Nat x+prevPos Pos = Nat+++natFromPos :: Pos x -> Nat x+natFromPos Pos = Nat+++newtype+ QuantifiedAdd condx condy prop x y =+ QuantifiedAdd {runQuantifiedAdd :: condx x -> condy y -> prop (x :+: y)}++addNat :: Nat x -> Nat y -> Nat (x :+: y)+addNat x0 y0@Nat =+ runQuantifiedAdd+ (switchNat+ (QuantifiedAdd const)+ (QuantifiedAdd $ \x -> succNat . addNat x . prevNat))+ x0 y0++addPosR :: Nat x -> Pos y -> Pos (x :+: y)+addPosR x0 y0@Pos =+ runQuantifiedAdd+ (switchPos (QuantifiedAdd $ \x -> posSucc . addNat x . prevPos))+ x0 y0++addPosL :: Pos x -> Nat y -> Pos (x :+: y)+addPosL x0 y0@Nat =+ runQuantifiedAdd+ (switchNat+ (QuantifiedAdd const)+ (QuantifiedAdd $ \x -> posSucc . addNat (natFromPos x) . prevNat))+ x0 y0+++newtype Quantified prop x = Quantified {runQuantified :: Nat x -> prop x}++induction ::+ quant Zero -> (forall x. Nat x -> quant (Succ x)) ->+ Nat y -> quant y+induction base step y@Nat =+ runQuantified+ (switchNat+ (Quantified $ const base)+ (Quantified $ step . prevNat))+ y+++data AddZeroL x = (Zero:+:x) ~ x => AddZeroL++succZeroL :: AddZeroL x -> AddZeroL (Succ x)+succZeroL AddZeroL = AddZeroL++addZeroL :: Nat x -> AddZeroL x+addZeroL = induction AddZeroL (succZeroL . addZeroL)+++{-+induction step:++Succ x :+: Succ y+Succ (x :+: Succ y)+Succ (Succ (x:+:y))+Succ (Succ x :+: y)+-}+data AddSuccL x y = (Succ x :+: y) ~ Succ (x:+:y) => AddSuccL++succSuccL :: AddSuccL x y -> AddSuccL x (Succ y)+succSuccL AddSuccL = AddSuccL++addSuccL :: Nat x -> Nat y -> AddSuccL x y+addSuccL x =+ induction+ (case addZeroL x of AddZeroL -> AddSuccL)+ (succSuccL . addSuccL x)+++{-+induction step:++y :+: Succ x+Succ (y :+: x)+Succ (x :+: y)+Succ x :+: y+-}+data AddComm x y = (x:+:y) ~ (y:+:x) => AddComm++succComm :: Nat x -> Nat y -> AddComm x y -> AddComm x (Succ y)+succComm x y AddComm = case addSuccL y x of AddSuccL -> AddComm++{- |+The proof is pretty expensive.+For proving (x:+:y ~ y:+:x) we need about @x*y@ reduction steps.+-}+addComm :: Nat x -> Nat y -> AddComm x y+addComm x =+ induction+ (case addZeroL x of AddZeroL -> AddComm)+ (\y -> succComm x y $ addComm x y)+++{-+induction step:++x :+: (y :+: Succ z)+x :+: Succ (y :+: z)+Succ (x :+: (y :+: z))+Succ ((x :+: y) :+: z)+(x :+: y) :+: Succ z+-}+data AddAssoc x y z = (x:+:(y:+:z)) ~ ((x:+:y):+:z) => AddAssoc++succAssoc :: AddAssoc x y z -> AddAssoc x y (Succ z)+succAssoc AddAssoc = AddAssoc++addAssoc :: Nat x -> Nat y -> Nat z -> AddAssoc x y z+addAssoc x y = induction AddAssoc (succAssoc . addAssoc x y)+++newtype+ QuantifiedMul condx condy prop x y =+ QuantifiedMul {runQuantifiedMul :: condx x -> condy y -> prop (x :*: y)}++mulNat :: Nat x -> Nat y -> Nat (x :*: y)+mulNat x0 y0@Nat =+ runQuantifiedMul+ (switchNat+ (QuantifiedMul $ \Nat Nat -> Nat)+ (QuantifiedMul $ \x -> addNat x . mulNat x . prevNat))+ x0 y0++mulPos :: Pos x -> Pos y -> Pos (x :*: y)+mulPos x0 y0@Pos =+ runQuantifiedMul+ (switchPos+ (QuantifiedMul $ \x -> addPosL x . mulNat (natFromPos x) . prevPos))+ x0 y0
+ src/Type/Data/Ord.hs view
@@ -0,0 +1,135 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE UndecidableInstances #-}++module Type.Data.Ord+ ( Compare+ , compare+ , LT+ , EQ+ , GT+ , IsLT+ , isLT+ , IsEQ+ , isEQ+ , IsGT+ , isGT+ , (:<:)+ , lt+ , LTT+ , (:<=:)+ , le+ , LET+ , (:==:)+ , eq+ , EQT+ , (:/=:)+ , ne+ , NET+ , (:>=:)+ , ge+ , GET+ , (:>:)+ , gt+ , GTT+ , Min+ , min+ , Max+ , max+ ) where++import Type.Data.Bool (If, Not, True, False)+import Type.Base.Proxy (Proxy(Proxy))++import Prelude ()+++type family Compare x y+data LT+data EQ+data GT+compare :: Proxy x -> Proxy y -> Proxy (Compare x y)+compare Proxy Proxy = Proxy++type family IsLT c+type instance IsLT LT = True+type instance IsLT EQ = False+type instance IsLT GT = False+isLT :: Proxy c -> Proxy (IsLT c)+isLT Proxy = Proxy++type family IsEQ c+type instance IsEQ LT = False+type instance IsEQ EQ = True+type instance IsEQ GT = False+isEQ :: Proxy c -> Proxy (IsEQ c)+isEQ Proxy = Proxy++type family IsGT c+type instance IsGT LT = False+type instance IsGT EQ = False+type instance IsGT GT = True+isGT :: Proxy c -> Proxy (IsGT c)+isGT Proxy = Proxy++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 LTT x y+type instance LTT x y = IsLT (Compare x y)+lt :: Proxy x -> Proxy y -> Proxy (LTT x y)+lt Proxy Proxy = Proxy+class x :<: y++type family LET x y+type instance LET x y = Not (GTT x y)+le :: Proxy x -> Proxy y -> Proxy (LET x y)+le Proxy Proxy = Proxy+class x :<=: y++type family EQT x y+type instance EQT x y = IsEQ (Compare x y)+eq :: Proxy x -> Proxy y -> Proxy (EQT x y)+eq Proxy Proxy = Proxy+class x :==: y++type family NET x y+type instance NET x y = Not (EQT x y)+ne :: Proxy x -> Proxy y -> Proxy (NET x y)+ne Proxy Proxy = Proxy+class x :/=: y++type family GET x y+type instance GET x y = Not (LTT x y)+ge :: Proxy x -> Proxy y -> Proxy (GET x y)+ge Proxy Proxy = Proxy+class x :>=: y++type family GTT x y+type instance GTT x y = IsGT (Compare x y)+gt :: Proxy x -> Proxy y -> Proxy (GTT x y)+gt Proxy Proxy = Proxy+class x :>: y++type family Min x y+type instance Min x y = If (LET x y) x y+min :: Proxy x -> Proxy y -> Proxy (Min x y)+min Proxy Proxy = Proxy++type family Max x y+type instance Max x y = If (GET x y) x y+max :: Proxy x -> Proxy y -> Proxy (Max x y)+max Proxy Proxy = Proxy++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,369 @@+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Main where++import qualified Type.Data.Num.Decimal.Literal as Lit+import qualified Type.Data.Num.Decimal.Number as Dec+import qualified Type.Data.Num.Unary.Literal as UnaryLit+import Type.Data.Num.Decimal.Number (Dec)+import Type.Data.Num.Decimal.Digit+import Type.Data.Num as Num+import Type.Data.Bool+import Type.Data.Ord+import Type.Base.Proxy (Proxy(Proxy))++import qualified Test.QuickCheck as Q++import Control.Monad (when)+import Data.Char (intToDigit)++import qualified Prelude+++type D0 = Dec Lit.D0+type D1 = Dec Lit.D1+type D2 = Dec Lit.D2+type D3 = Dec Lit.D3+type D4 = Dec Lit.D4+type D5 = Dec Lit.D5+type D6 = Dec Lit.D6+type D7 = Dec Lit.D7+type D8 = Dec Lit.D8+type D9 = Dec Lit.D9+type D10 = Dec Lit.D10+type D11 = Dec Lit.D11+type D16 = Dec Lit.D16+type D17 = Dec Lit.D17+type D31 = Dec Lit.D31+type D32 = Dec Lit.D32+type D49 = Dec Lit.D49+type D50 = Dec Lit.D50+type D57 = Dec Lit.D57+type D58 = Dec Lit.D58+type D90 = Dec Lit.D90+type D99 = Dec Lit.D99+type D100 = Dec Lit.D100+type D101 = Dec Lit.D101++type DN1 = Dec Lit.DN1+type DN2 = Dec Lit.DN2+type DN5 = Dec Lit.DN5+type DN6 = Dec Lit.DN6+type DN9 = Dec Lit.DN9+type DN10 = Dec Lit.DN10+type DN11 = Dec Lit.DN11+type DN50 = Dec Lit.DN50+type DN99 = Dec Lit.DN99+type DN100 = Dec Lit.DN100+type DN101 = Dec Lit.DN101++type D527 = Dec (Lit.Pos3 Dec5 Dec2 Dec7)+type D720 = Dec (Lit.Pos3 Dec7 Dec2 Dec0)+type D989 = Dec (Lit.Pos3 Dec9 Dec8 Dec9)+type D1000 = Dec (Lit.Pos4 Dec1 Dec0 Dec0 Dec0)+type D1024 = Dec (Lit.Pos4 Dec1 Dec0 Dec2 Dec4)+type D10000 = Dec (Lit.Pos5 Dec1 Dec0 Dec0 Dec0 Dec0)+type D3628800 = Dec (Lit.Pos7 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++testHalf1 :: Div2 D0 -> D0+testHalf1 = Prelude.id+testHalf2 :: Div2 D1 -> D0+testHalf2 = Prelude.id+testHalf3 :: Div2 D2 -> D1+testHalf3 = Prelude.id+testHalf4 :: Div2 D10 -> D5+testHalf4 = Prelude.id+testHalf5 :: Div2 D11 -> D5+testHalf5 = Prelude.id+testHalf6 :: Div2 D99 -> D49+testHalf6 = Prelude.id+testHalf7 :: Div2 D100 -> D50+testHalf7 = Prelude.id+testHalf8 :: Div2 D101 -> D50+testHalf8 = Prelude.id+testHalf9 :: Div2 DN1 -> D0+testHalf9 = Prelude.id+testHalf10 :: Div2 DN2 -> DN1+testHalf10 = Prelude.id+testHalf11 :: Div2 DN10 -> DN5+testHalf11 = Prelude.id+testHalf12 :: Div2 DN11 -> DN5+testHalf12 = Prelude.id+testHalf13 :: Div2 DN100 -> DN50+testHalf13 = Prelude.id++testMul1 :: D0 :*: D0 -> D0+testMul1 = Prelude.id+testMul2 :: D0 :*: D1 -> D0+testMul2 = Prelude.id+testMul3 :: D1 :*: D0 -> D0+testMul3 = Prelude.id+testMul4 :: D1 :*: D1 -> D1+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 :: EQT D0 D0 -> True+testEQ1 = Prelude.id+testEQ2 :: EQT D0 (Pred D1) -> True+testEQ2 = Prelude.id+testEQ3 :: EQT (D1 :+: D9) D10 -> True+testEQ3 = Prelude.id+testEQ4 :: EQT (D1 :+: D9) D11 -> False+testEQ4 = Prelude.id+testEQ5 :: EQT D9 D0 -> False+testEQ5 = Prelude.id+testEQ6 :: EQT D8 D0 -> False+testEQ6 = Prelude.id+testEQ7 :: EQT D7 D0 -> False+testEQ7 = Prelude.id+testEQ8 :: EQT D6 D0 -> False+testEQ8 = Prelude.id+testEQ9 :: EQT D5 D0 -> False+testEQ9 = Prelude.id+testEQ10 :: EQT D4 D0 -> False+testEQ10 = Prelude.id+testEQ11 :: EQT D3 D0 -> False+testEQ11 = Prelude.id+testEQ12 :: EQT D2 D0 -> False+testEQ12 = Prelude.id+testEQ13 :: EQT 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++testExp1 :: Pow2 D0 -> D1+testExp1 = Prelude.id+testExp2 :: Pow2 D1 -> D2+testExp2 = Prelude.id+testExp3 :: Pow2 D2 -> D4+testExp3 = Prelude.id+testExp4 :: Pow2 D3 -> D8+testExp4 = Prelude.id+testExp5 :: Pow2 D4 -> D16+testExp5 = Prelude.id+testExp6 :: Pow2 D5 -> D32+testExp6 = Prelude.id+testExp7 :: Pow2 D10 -> D1024+testExp7 = Prelude.id++testLog1 :: Log2Ceil D1 -> D0+testLog1 = Prelude.id+testLog2 :: Log2Ceil D2 -> D1+testLog2 = Prelude.id+testLog3 :: Log2Ceil D3 -> D2+testLog3 = Prelude.id+testLog4 :: Log2Ceil D4 -> D2+testLog4 = Prelude.id+testLog5 :: Log2Ceil D7 -> D3+testLog5 = Prelude.id+testLog6 :: Log2Ceil D8 -> D3+testLog6 = Prelude.id+testLog7 :: Log2Ceil D9 -> D4+testLog7 = Prelude.id++testDecToUnary :: Dec.ToUnary Lit.D42 -> UnaryLit.U42+testDecToUnary = Prelude.id++testDecFromUnary :: Dec.FromUnary UnaryLit.U42 -> Lit.D42+testDecFromUnary = Prelude.id+++class TestIter n zero where+ testIter :: Proxy n -> Proxy zero -> Prelude.String++instance ( Num.Natural n, EQT n D0 ~ True )+ => TestIter n True where+ testIter _ _ = ""++instance ( Num.Natural n, EQT n D0 ~ False+ , TestIter (Pred n) (EQT (Pred n) D0) )+ => TestIter n False where+ testIter n _ =+ intToDigit (Num.fromInteger n) :+ testIter (Proxy :: Proxy (Pred n)) (Proxy :: Proxy (EQT (Pred n) D0))++main :: Prelude.IO ()+main = do+ let testIterResult = testIter (Dec.decimal Lit.d9) (Proxy :: Proxy 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 =+ Num.reifyIntegral (Proxy :: Proxy Dec.Decimal) i Num.fromInteger Prelude.== i
tfp.cabal view
@@ -1,68 +1,74 @@ name: tfp-version: 0.3-cabal-version: >= 1.6+version: 1.0.2 build-type: Simple license: BSD3 license-file: LICENSE-copyright: Copyright (c) 2008 Peter Gavin-author: Peter Gavin-maintainer: pgavin@gmail.com-homepage: http://abt12monk.org/git/tfp.git/+copyright: Copyright (c) 2014 Henning Thielemann, 2008 Peter Gavin+author: Peter Gavin, Henning Thielemann+maintainer: haskell@henning-thielemann.de+homepage: http://www.haskell.org/haskellwiki/Type_arithmetic stability: alpha-package-url: http://abt12monk.org/git/tfp.git/-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+synopsis: Type-level integers, booleans, lists using type families+description:+ TFP is an abbreviation for Type Family Programming.+ It 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: Type System+tested-with: GHC == 7.4.2, GHC == 7.6.3, GHC == 7.8.4, GHC == 8.0.1+cabal-version: 1.14+extra-source-files:+ Changes.md -source-repository head {- type: git- location: http://abt12monk.org/git/tfp.git/-}+source-repository head+ type: darcs+ location: https://hub.darcs.net/thielema/tfp/ -flag build-test- description: Build the tfp-test test program- default: False+source-repository this+ tag: 1.0.2+ type: darcs+ location: https://hub.darcs.net/thielema/tfp/ + 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:+ utility-ht >=0.0.10 && <0.1,+ base >=4.5 && <5+ ghc-options: -Wall+ if impl(ghc>=8.0)+ ghc-options: -fno-warn-redundant-constraints+ hs-source-dirs: src 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+ Data.SizedInt+ Data.SizedWord+ Type.Base.Proxy+ Type.Data.Bool+ Type.Data.Num+ Type.Data.Num.Unary+ Type.Data.Num.Unary.Literal+ Type.Data.Num.Unary.Proof+ Type.Data.Num.Decimal+ Type.Data.Num.Decimal.Literal+ Type.Data.Num.Decimal.Digit+ Type.Data.Num.Decimal.Digit.Proof+ Type.Data.Num.Decimal.Number+ Type.Data.Num.Decimal.Proof+ Type.Data.List+ Type.Data.Ord } -executable tfp-test {- if flag(build-test) {- buildable: True- } else {- buildable: False- }- extensions: TypeFamilies, UndecidableInstances, TypeOperators,- EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables,- FlexibleInstances, TemplateHaskell, TypeSynonymInstances,- MultiParamTypeClasses, GeneralizedNewtypeDeriving,- FunctionalDependencies, Rank2Types, FlexibleContexts+test-suite tfp-test {+ type: exitcode-stdio-1.0+ build-depends:+ tfp,+ QuickCheck >= 1.2.0.0,+ base+ default-language: Haskell2010+ ghc-options: -Wall main-is: Test.hs- build-depends: base >= 3.0 && < 5, template-haskell >= 2.0, QuickCheck >= 1.2.0.0+ hs-source-dirs: test }