{-# OPTIONS_GHC  -fno-warn-orphans #-}

{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE EmptyDataDecls        #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE DeriveDataTypeable    #-}
-- |
-- Module      : TypeLevel.Number.Nat
-- Copyright   : Alexey Khudyakov
-- License     : BSD3-style (see LICENSE)
--
-- Maintainer  : Alexey Khudyakov <alexey.skladnoy@gmail.com>
-- Stability   : unstable
-- Portability : unportable (GHC only)
--
--
-- This is type level natural numbers. They are represented using
-- binary encoding which means that reasonable large numbers could be
-- represented. With default context stack depth (20) maximal number
-- is 2^18-1 (262143).
--
-- > Z           = 0
-- > I Z         = 1
-- > O (I Z)     = 2
-- > I (I Z)     = 3
-- > O (O (I Z)) = 4
-- > ...
--
-- It's easy to see that representation for each number is not
-- unique. One could add any numbers of leading zeroes:
--
-- > I Z = I (O Z) = I (O (O Z)) = 1
--
-- In order to enforce uniqueness of representation only numbers
-- without leading zeroes are members of Nat type class. This means
-- than types are equal if and only if numbers are equal.
--
-- Natural numbers support comparison and following operations: Next,
-- Prev, Add, Sub, Mul. All operations on numbers return normalized
-- numbers.
--
-- Interface type classes are reexported from TypeLevel.Number.Classes
module TypeLevel.Number.Nat ( -- * Natural numbers
                          I
                        , O
                        , Z
                        , Nat(..)
                          -- ** Lifting
                        , SomeNat(..)
                        , withNat
                          -- * Template haskell utilities
                          -- $TH
                        , natT
                        , nat
                        , module TypeLevel.Number.Classes
                        ) where

import Data.Word     (Word8,Word16,Word32,Word64)
import Data.Int      (Int8, Int16, Int32, Int64 )
import Data.Typeable (Typeable)

import TypeLevel.Number.Classes
import TypeLevel.Number.Nat.Types
import TypeLevel.Number.Nat.TH
import TypeLevel.Reify

-- $TH
-- Here is usage example for natT:
--
-- > n123 :: $(natT 123)
-- > n123 = undefined

----------------------------------------------------------------

-- | Type class for natural numbers. Only numbers without leading
-- zeroes are members of this type class.
class Nat n where
  -- | Convert natural number to integral value. It's not checked
  -- whether value could be represented.
  toInt :: Integral i => n -> i

-- | Type class for positive natural numbers. It's synonym for
-- Positive and Nat.
class Pos n

instance              Nat       Z   where toInt :: Z -> i
toInt Z
_ = i
0
instance              Nat    (I Z)  where toInt :: I Z -> i
toInt I Z
_ = i
1
instance Nat (O n) => Nat (O (O n)) where toInt :: O (O n) -> i
toInt O (O n)
_ = i
0 i -> i -> i
forall a. Num a => a -> a -> a
+ i
2 i -> i -> i
forall a. Num a => a -> a -> a
* O n -> i
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: (O n))
instance Nat (O n) => Nat (I (O n)) where toInt :: I (O n) -> i
toInt I (O n)
_ = i
1 i -> i -> i
forall a. Num a => a -> a -> a
+ i
2 i -> i -> i
forall a. Num a => a -> a -> a
* O n -> i
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: (O n))
instance Nat (I n) => Nat (O (I n)) where toInt :: O (I n) -> i
toInt O (I n)
_ = i
0 i -> i -> i
forall a. Num a => a -> a -> a
+ i
2 i -> i -> i
forall a. Num a => a -> a -> a
* I n -> i
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: (I n))
instance Nat (I n) => Nat (I (I n)) where toInt :: I (I n) -> i
toInt I (I n)
_ = i
1 i -> i -> i
forall a. Num a => a -> a -> a
+ i
2 i -> i -> i
forall a. Num a => a -> a -> a
* I n -> i
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: (I n))
-- Error reporting. Stop for denormalized numbers
class    Number_Is_Denormalized a
instance (Number_Is_Denormalized Z) => Nat (O Z) where
  toInt :: O Z -> i
toInt = [Char] -> O Z -> i
forall a. HasCallStack => [Char] -> a
error [Char]
"quench warning"

-- Synonym for positive
instance (Nat n, Positive n) => Pos n


-- | Some natural number
data SomeNat where
  SomeNat :: Nat n => n -> SomeNat
  deriving Typeable

instance Show SomeNat where
  showsPrec :: Int -> SomeNat -> ShowS
showsPrec Int
d (SomeNat n
n) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    [Char] -> ShowS
showString [Char]
"withNat SomeNat " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> ShowS
forall a. Show a => a -> ShowS
shows (n -> Integer
forall n i. (Nat n, Integral i) => n -> i
toInt n
n :: Integer)



-- | Apply function which could work with any 'Nat' value only know at runtime.
withNat :: forall i a. (Integral i) => (forall n. Nat n => n -> a) -> i -> a
withNat :: (forall n. Nat n => n -> a) -> i -> a
withNat forall n. Nat n => n -> a
f i
i0
  | i
i0 i -> i -> Bool
forall a. Ord a => a -> a -> Bool
<  i
0   = [Char] -> a
forall a. HasCallStack => [Char] -> a
error [Char]
"TypeLevel.Number.Nat.withNat: negative number"
  | i
i0 i -> i -> Bool
forall a. Eq a => a -> a -> Bool
== i
0   = Z -> a
forall n. Nat n => n -> a
f (Z
forall a. HasCallStack => a
undefined :: Z)
  | Bool
otherwise = Integer
-> (forall n m. (Nat n, n ~ O m) => n -> a)
-> (forall n m. (Nat n, n ~ I m) => n -> a)
-> a
cont (i -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral i
i0) forall n. Nat n => n -> a
forall n m. (Nat n, n ~ O m) => n -> a
f forall n. Nat n => n -> a
forall n m. (Nat n, n ~ I m) => n -> a
f
  where
    cont :: Integer -> (forall n m. (Nat n, n ~ O m) => n -> a)
                    -> (forall n m. (Nat n, n ~ I m) => n -> a) -> a
    cont :: Integer
-> (forall n m. (Nat n, n ~ O m) => n -> a)
-> (forall n m. (Nat n, n ~ I m) => n -> a)
-> a
cont Integer
1 forall n m. (Nat n, n ~ O m) => n -> a
_  forall n m. (Nat n, n ~ I m) => n -> a
k1 = I Z -> a
forall n m. (Nat n, n ~ I m) => n -> a
k1 (I Z
forall a. HasCallStack => a
undefined :: I Z)
    cont Integer
i forall n m. (Nat n, n ~ O m) => n -> a
k0 forall n m. (Nat n, n ~ I m) => n -> a
k1 = Integer
-> (forall n m. (Nat n, n ~ O m) => n -> a)
-> (forall n m. (Nat n, n ~ I m) => n -> a)
-> a
cont (Integer
i Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`quot` Integer
2) forall n m. (Nat n, n ~ O m) => n -> a
k0' forall n m. (Nat n, n ~ I m) => n -> a
k1'
      where
        k0' :: forall n m. (Nat n, n ~ O m) => n -> a
        k0' :: n -> a
k0' n
_ | Integer -> Bool
forall a. Integral a => a -> Bool
odd Integer
i     = I n -> a
forall n m. (Nat n, n ~ I m) => n -> a
k1 (I n
forall a. HasCallStack => a
undefined :: I n)
              | Bool
otherwise = O n -> a
forall n m. (Nat n, n ~ O m) => n -> a
k0 (O n
forall a. HasCallStack => a
undefined :: O n)
        k1' :: forall n m. (Nat n, n ~ I m) => n -> a
        k1' :: n -> a
k1' n
_ | Integer -> Bool
forall a. Integral a => a -> Bool
odd Integer
i     = I n -> a
forall n m. (Nat n, n ~ I m) => n -> a
k1 (I n
forall a. HasCallStack => a
undefined :: I n)
              | Bool
otherwise = O n -> a
forall n m. (Nat n, n ~ O m) => n -> a
k0 (O n
forall a. HasCallStack => a
undefined :: O n)



----------------------------------------------------------------
-- Data conversion

-- To Integer
instance                Reify    Z  Integer where witness :: Witness Z Integer
witness = Integer -> Witness Z Integer
forall t a. a -> Witness t a
Witness Integer
0
instance (Nat (O n)) => Reify (O n) Integer where witness :: Witness (O n) Integer
witness = Integer -> Witness (O n) Integer
forall t a. a -> Witness t a
Witness (Integer -> Witness (O n) Integer)
-> Integer -> Witness (O n) Integer
forall a b. (a -> b) -> a -> b
$ O n -> Integer
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: O n)
instance (Nat (I n)) => Reify (I n) Integer where witness :: Witness (I n) Integer
witness = Integer -> Witness (I n) Integer
forall t a. a -> Witness t a
Witness (Integer -> Witness (I n) Integer)
-> Integer -> Witness (I n) Integer
forall a b. (a -> b) -> a -> b
$ I n -> Integer
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)

-- To Int
instance                Reify    Z  Int where witness :: Witness Z Int
witness = Int -> Witness Z Int
forall t a. a -> Witness t a
Witness Int
0
instance (Nat (O n)) => Reify (O n) Int where witness :: Witness (O n) Int
witness = Int -> Witness (O n) Int
forall t a. a -> Witness t a
Witness (Int -> Witness (O n) Int) -> Int -> Witness (O n) Int
forall a b. (a -> b) -> a -> b
$ O n -> Int
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: O n)
instance (Nat (I n)) => Reify (I n) Int where witness :: Witness (I n) Int
witness = Int -> Witness (I n) Int
forall t a. a -> Witness t a
Witness (Int -> Witness (I n) Int) -> Int -> Witness (I n) Int
forall a b. (a -> b) -> a -> b
$ I n -> Int
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)

-- To Word8
instance                                              Reify    Z  Word8 where witness :: Witness Z Word8
witness = Word8 -> Witness Z Word8
forall t a. a -> Witness t a
Witness Word8
0
instance (Nat (O n), (O n) `Lesser` $(natT 0x100)) => Reify (O n) Word8 where witness :: Witness (O n) Word8
witness = Word8 -> Witness (O n) Word8
forall t a. a -> Witness t a
Witness (Word8 -> Witness (O n) Word8) -> Word8 -> Witness (O n) Word8
forall a b. (a -> b) -> a -> b
$ O n -> Word8
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: O n)
instance (Nat (I n), (I n) `Lesser` $(natT 0x100)) => Reify (I n) Word8 where witness :: Witness (I n) Word8
witness = Word8 -> Witness (I n) Word8
forall t a. a -> Witness t a
Witness (Word8 -> Witness (I n) Word8) -> Word8 -> Witness (I n) Word8
forall a b. (a -> b) -> a -> b
$ I n -> Word8
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)

-- To Word16
instance                                                Reify    Z  Word16 where witness :: Witness Z Word16
witness = Word16 -> Witness Z Word16
forall t a. a -> Witness t a
Witness Word16
0
instance (Nat (O n), (O n) `Lesser` $(natT 0x10000)) => Reify (O n) Word16 where witness :: Witness (O n) Word16
witness = Word16 -> Witness (O n) Word16
forall t a. a -> Witness t a
Witness (Word16 -> Witness (O n) Word16) -> Word16 -> Witness (O n) Word16
forall a b. (a -> b) -> a -> b
$ O n -> Word16
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: O n)
instance (Nat (I n), (I n) `Lesser` $(natT 0x10000)) => Reify (I n) Word16 where witness :: Witness (I n) Word16
witness = Word16 -> Witness (I n) Word16
forall t a. a -> Witness t a
Witness (Word16 -> Witness (I n) Word16) -> Word16 -> Witness (I n) Word16
forall a b. (a -> b) -> a -> b
$ I n -> Word16
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)

-- To Word32 (No checks. Won't to default centext stack length)
instance                Reify    Z  Word32 where witness :: Witness Z Word32
witness = Word32 -> Witness Z Word32
forall t a. a -> Witness t a
Witness Word32
0
instance (Nat (O n)) => Reify (O n) Word32 where witness :: Witness (O n) Word32
witness = Word32 -> Witness (O n) Word32
forall t a. a -> Witness t a
Witness (Word32 -> Witness (O n) Word32) -> Word32 -> Witness (O n) Word32
forall a b. (a -> b) -> a -> b
$ O n -> Word32
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: O n)
instance (Nat (I n)) => Reify (I n) Word32 where witness :: Witness (I n) Word32
witness = Word32 -> Witness (I n) Word32
forall t a. a -> Witness t a
Witness (Word32 -> Witness (I n) Word32) -> Word32 -> Witness (I n) Word32
forall a b. (a -> b) -> a -> b
$ I n -> Word32
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)

-- To Word64 (No checks. Won't to default centext stack length)
instance                Reify    Z  Word64 where witness :: Witness Z Word64
witness = Word64 -> Witness Z Word64
forall t a. a -> Witness t a
Witness Word64
0
instance (Nat (O n)) => Reify (O n) Word64 where witness :: Witness (O n) Word64
witness = Word64 -> Witness (O n) Word64
forall t a. a -> Witness t a
Witness (Word64 -> Witness (O n) Word64) -> Word64 -> Witness (O n) Word64
forall a b. (a -> b) -> a -> b
$ O n -> Word64
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: O n)
instance (Nat (I n)) => Reify (I n) Word64 where witness :: Witness (I n) Word64
witness = Word64 -> Witness (I n) Word64
forall t a. a -> Witness t a
Witness (Word64 -> Witness (I n) Word64) -> Word64 -> Witness (I n) Word64
forall a b. (a -> b) -> a -> b
$ I n -> Word64
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)

-- To Int8
instance                                             Reify    Z  Int8 where witness :: Witness Z Int8
witness = Int8 -> Witness Z Int8
forall t a. a -> Witness t a
Witness Int8
0
instance (Nat (O n), (O n) `Lesser` $(natT 0x80)) => Reify (O n) Int8 where witness :: Witness (O n) Int8
witness = Int8 -> Witness (O n) Int8
forall t a. a -> Witness t a
Witness (Int8 -> Witness (O n) Int8) -> Int8 -> Witness (O n) Int8
forall a b. (a -> b) -> a -> b
$ O n -> Int8
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: O n)
instance (Nat (I n), (I n) `Lesser` $(natT 0x80)) => Reify (I n) Int8 where witness :: Witness (I n) Int8
witness = Int8 -> Witness (I n) Int8
forall t a. a -> Witness t a
Witness (Int8 -> Witness (I n) Int8) -> Int8 -> Witness (I n) Int8
forall a b. (a -> b) -> a -> b
$ I n -> Int8
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)

-- To Int16
instance                                               Reify    Z  Int16 where witness :: Witness Z Int16
witness = Int16 -> Witness Z Int16
forall t a. a -> Witness t a
Witness Int16
0
instance (Nat (O n), (O n) `Lesser` $(natT 0x8000)) => Reify (O n) Int16 where witness :: Witness (O n) Int16
witness = Int16 -> Witness (O n) Int16
forall t a. a -> Witness t a
Witness (Int16 -> Witness (O n) Int16) -> Int16 -> Witness (O n) Int16
forall a b. (a -> b) -> a -> b
$ O n -> Int16
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: O n)
instance (Nat (I n), (I n) `Lesser` $(natT 0x8000)) => Reify (I n) Int16 where witness :: Witness (I n) Int16
witness = Int16 -> Witness (I n) Int16
forall t a. a -> Witness t a
Witness (Int16 -> Witness (I n) Int16) -> Int16 -> Witness (I n) Int16
forall a b. (a -> b) -> a -> b
$ I n -> Int16
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)

-- To Int32 (No checks. Won't to default centext stack length)
instance                Reify    Z  Int32 where witness :: Witness Z Int32
witness = Int32 -> Witness Z Int32
forall t a. a -> Witness t a
Witness Int32
0
instance (Nat (O n)) => Reify (O n) Int32 where witness :: Witness (O n) Int32
witness = Int32 -> Witness (O n) Int32
forall t a. a -> Witness t a
Witness (Int32 -> Witness (O n) Int32) -> Int32 -> Witness (O n) Int32
forall a b. (a -> b) -> a -> b
$ O n -> Int32
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: O n)
instance (Nat (I n)) => Reify (I n) Int32 where witness :: Witness (I n) Int32
witness = Int32 -> Witness (I n) Int32
forall t a. a -> Witness t a
Witness (Int32 -> Witness (I n) Int32) -> Int32 -> Witness (I n) Int32
forall a b. (a -> b) -> a -> b
$ I n -> Int32
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)

-- To Int64 (No checks. Won't to default centext stack length)
instance                Reify    Z  Int64 where witness :: Witness Z Int64
witness = Int64 -> Witness Z Int64
forall t a. a -> Witness t a
Witness Int64
0
instance (Nat (O n)) => Reify (O n) Int64 where witness :: Witness (O n) Int64
witness = Int64 -> Witness (O n) Int64
forall t a. a -> Witness t a
Witness (Int64 -> Witness (O n) Int64) -> Int64 -> Witness (O n) Int64
forall a b. (a -> b) -> a -> b
$ O n -> Int64
forall n i. (Nat n, Integral i) => n -> i
toInt (O n
forall a. HasCallStack => a
undefined :: O n)
instance (Nat (I n)) => Reify (I n) Int64 where witness :: Witness (I n) Int64
witness = Int64 -> Witness (I n) Int64
forall t a. a -> Witness t a
Witness (Int64 -> Witness (I n) Int64) -> Int64 -> Witness (I n) Int64
forall a b. (a -> b) -> a -> b
$ I n -> Int64
forall n i. (Nat n, Integral i) => n -> i
toInt (I n
forall a. HasCallStack => a
undefined :: I n)

----------------------------------------------------------------
-- Number normalization

-- Add trailing zero bit to number. It's added only if number is not
-- equal to zero. Actual normalization is done here.
type family   Add0Bit n :: *
type instance Add0Bit    Z  = Z
type instance Add0Bit (O n) = (O (O n))
type instance Add0Bit (I n) = (O (I n))

type instance Normalized    Z  = Z
type instance Normalized (I n) = I (Normalized n)
type instance Normalized (O n) = Add0Bit (Normalized n)

----------------------------------------------------------------
-- Show instances.
-- Nat contexts are used to ensure correctness of numbers.
instance              Show    Z  where show :: Z -> [Char]
show Z
_ = [Char]
"[0:N]"
instance Nat (O n) => Show (O n) where show :: O n -> [Char]
show O n
n = [Char]
"["[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++Integer -> [Char]
forall a. Show a => a -> [Char]
show (O n -> Integer
forall n i. (Nat n, Integral i) => n -> i
toInt O n
n :: Integer)[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
":N]"
instance Nat (I n) => Show (I n) where show :: I n -> [Char]
show I n
n = [Char]
"["[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++Integer -> [Char]
forall a. Show a => a -> [Char]
show (I n -> Integer
forall n i. (Nat n, Integral i) => n -> i
toInt I n
n :: Integer)[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
":N]"

----------------------------------------------------------------
-- Next number.
-- Number normalization is not required.
type instance Next    Z  = I Z
type instance Next (I n) = O (Next n)
type instance Next (O n) = I n

----------------------------------------------------------------
-- Previous number.
-- Normalization isn't requred too. It's done manually in (I Z) case.
type instance Prev    (I Z)   = Z
type instance Prev (O (O n))  = I (Prev (O n))
type instance Prev (I (O n))  = O (O n)
type instance Prev (O (I n))  = I (Prev (I n))
type instance Prev (I (I n))  = O (I n)


----------------------------------------------------------------
-- Comparison

-- Join compare results. a is result of comparison of low digits b is
-- result of comparion of higher digits.
type family Join a b :: *

type instance Join IsLesser  IsEqual   = IsLesser
type instance Join IsEqual   IsEqual   = IsEqual
type instance Join IsGreater IsEqual   = IsGreater
type instance Join a         IsLesser  = IsLesser
type instance Join a         IsGreater = IsGreater

-- Instances for comparison
type instance Compare    Z     Z  = IsEqual
type instance Compare (O n)    Z  = IsGreater
type instance Compare (I n)    Z  = IsGreater
type instance Compare    Z  (O n) = IsLesser
type instance Compare    Z  (I n) = IsLesser

type instance Compare (O n) (O m) = Compare n m
type instance Compare (O n) (I m) = Join IsLesser  (Compare n m)
type instance Compare (I n) (O m) = Join IsGreater (Compare n m)
type instance Compare (I n) (I m) = Compare n m

----------------------------------------------------------------
-- Positive and Non-zero numbers

instance Nat (I n) => Positive (I n)
instance Nat (O n) => Positive (O n)

instance Nat (I n) => NonZero (I n)
instance Nat (O n) => NonZero (O n)

----------------------------------------------------------------
-- Addition
data Carry      -- Designate carry bit
data NoCarry    -- No carry bit in addition

-- Type family which actually implement addtition of natural numbers
type family Add' n m c :: *

-- Recursion termination without carry bit. Full enumeration is
-- required to avoid overlapping instances
type instance Add'    Z     Z  NoCarry = Z
type instance Add' (O n)    Z  NoCarry = O n
type instance Add' (I n)    Z  NoCarry = I n
type instance Add'    Z  (O n) NoCarry = O n
type instance Add'    Z  (I n) NoCarry = I n
-- Recursion termination with carry bit
type instance Add'    Z   Z      Carry = I Z
type instance Add' (O n)  Z      Carry = I n
type instance Add' (I n)  Z      Carry = Add' (I n) (I Z) NoCarry
type instance Add'    Z  (O n)   Carry = I n
type instance Add'    Z  (I n)   Carry = Add' (I n) (I Z) NoCarry
-- Generic recursion (No carry)
type instance Add' (O n) (O m) NoCarry = O (Add' n m NoCarry)
type instance Add' (I n) (O m) NoCarry = I (Add' n m NoCarry)
type instance Add' (O n) (I m) NoCarry = I (Add' n m NoCarry)
type instance Add' (I n) (I m) NoCarry = O (Add' n m   Carry)
-- Generic recursion (with carry)
type instance Add' (O n) (O m)   Carry = I (Add' n m NoCarry)
type instance Add' (I n) (O m)   Carry = O (Add' n m   Carry)
type instance Add' (O n) (I m)   Carry = O (Add' n m   Carry)
type instance Add' (I n) (I m)   Carry = I (Add' n m   Carry)

-- Enumeration of all possible instances heads is required to avoid
-- overlapping.
type instance Add (O n) (O m) = Normalized (Add' (O n) (O m) NoCarry)
type instance Add (I n) (O m) = Normalized (Add' (I n) (O m) NoCarry)
type instance Add (O n) (I m) = Normalized (Add' (O n) (I m) NoCarry)
type instance Add (I n) (I m) = Normalized (Add' (I n) (I m) NoCarry)
type instance Add (O n)    Z  = Normalized (Add' (O n)    Z  NoCarry)
type instance Add (I n)    Z  = Normalized (Add' (I n)    Z  NoCarry)
type instance Add    Z  (O n) = Normalized (Add'    Z  (O n) NoCarry)
type instance Add    Z  (I n) = Normalized (Add'    Z  (I n) NoCarry)
type instance Add    Z     Z  = Normalized (Add'    Z     Z  NoCarry)

----------------------------------------------------------------
-- Subtraction
data Borrow     -- Borrow bit
data NoBorrow   -- Do not borrow bit

-- Type class which actually implement addtition of natural numbers
type family Sub' n m c :: *

-- Recursion termination without carry bit. Full enumeration is
-- required to avoid overlapping instances
type instance Sub'    Z     Z  NoBorrow = Z
type instance Sub' (O n)    Z  NoBorrow = O n
type instance Sub' (I n)    Z  NoBorrow = I n
-- Recursion termination with carry bit
type instance Sub' (O n)  Z      Borrow = I (Sub' n Z Borrow)
type instance Sub' (I n)  Z      Borrow = O n
-- Generic recursion (No carry)
type instance Sub' (O n) (O m) NoBorrow = O (Sub' n m NoBorrow)
type instance Sub' (I n) (O m) NoBorrow = I (Sub' n m NoBorrow)
type instance Sub' (O n) (I m) NoBorrow = I (Sub' n m   Borrow)
type instance Sub' (I n) (I m) NoBorrow = O (Sub' n m NoBorrow)
-- -- Generic recursion (with carry)
type instance Sub' (O n) (O m)   Borrow = I (Sub' n m   Borrow)
type instance Sub' (I n) (O m)   Borrow = O (Sub' n m NoBorrow)
type instance Sub' (O n) (I m)   Borrow = O (Sub' n m   Borrow)
type instance Sub' (I n) (I m)   Borrow = I (Sub' n m   Borrow)

-- Enumeration of all possible instances heads is required to avoid
-- overlapping.
type instance Sub (O n) (O m) = Normalized (Sub' (O n) (O m) NoBorrow)
type instance Sub (I n) (O m) = Normalized (Sub' (I n) (O m) NoBorrow)
type instance Sub (O n) (I m) = Normalized (Sub' (O n) (I m) NoBorrow)
type instance Sub (I n) (I m) = Normalized (Sub' (I n) (I m) NoBorrow)
type instance Sub (O n)    Z  = Normalized (Sub' (O n)    Z  NoBorrow)
type instance Sub (I n)    Z  = Normalized (Sub' (I n)    Z  NoBorrow)
type instance Sub    Z     Z  = Normalized (Sub'    Z     Z  NoBorrow)

----------------------------------------------------------------
-- Multiplication
----------------------------------------------------------------

type instance Mul n    Z  = Z
type instance Mul n (O m) = Normalized (O (Mul n m))
type instance Mul n (I m) = Normalized (Add' n (O (Mul n m)) NoCarry)