packages feed

tfp 0.8 → 1.0

raw patch · 30 files changed

+4017/−2816 lines, 30 filesdep +utility-htdep ~base

Dependencies added: utility-ht

Dependency ranges changed: base

Files

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