{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Singleton-typed natural numbers and arithmetic.
--
--   Used for indexing into hetrogenous list types.
--
module Data.Repa.Scalar.Singleton.Nat
        ( N   (..)
        , Nat (..)
        , Add (..)
        , Mul (..)

        -- * Literals
        , nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9)
where


-- | Peano natural numbers.
data N  = Z | S N


deriving instance Show N


-- | Peano natural number singletons.
data Nat (n :: N) where
        Zero    :: Nat Z
        Succ    :: Nat n -> Nat (S n)

deriving instance Show (Nat n)


---------------------------------------------------------------------------------------------------
class Add x y where
 type AddR x y :: N
 -- | Addition of singleton typed natural numbers.
 add  :: Nat x -> Nat y -> Nat (AddR x y)

instance Add Z x where
 type AddR Z x   = x
 add :: Nat 'Z -> Nat x -> Nat (AddR 'Z x)
add Nat 'Z
Zero Nat x
y      = Nat x
Nat (AddR 'Z x)
y
 {-# INLINE add #-}

instance Add x (S y) => Add (S x) y where
 type AddR (S x) y = AddR x (S y)
 add :: Nat ('S x) -> Nat y -> Nat (AddR ('S x) y)
add (Succ Nat n
x) Nat y
y    = Nat n -> Nat ('S y) -> Nat (AddR n ('S y))
forall (x :: N) (y :: N).
Add x y =>
Nat x -> Nat y -> Nat (AddR x y)
add Nat n
x  (Nat y -> Nat ('S y)
forall (n :: N). Nat n -> Nat ('S n)
Succ Nat y
y)
 {-# INLINE add #-}


---------------------------------------------------------------------------------------------------
class Mul x y where
 type MulR x y :: N
 -- | Multiplication of singleton typed natural numbers.
 mul  :: Nat x -> Nat y -> Nat (MulR x y)

instance Mul Z x where
 type MulR  Z       x = Z
 mul :: Nat 'Z -> Nat x -> Nat (MulR 'Z x)
mul        Nat 'Z
Zero    Nat x
_ = Nat (MulR 'Z x)
Nat 'Z
Zero

instance (Mul x y, Add (MulR x y) y)
       => Mul (S x) y where
 type MulR (S x)    y = AddR (MulR x y) y
 mul :: Nat ('S x) -> Nat y -> Nat (MulR ('S x) y)
mul       (Succ Nat n
x) Nat y
y = Nat (MulR x y) -> Nat y -> Nat (AddR (MulR x y) y)
forall (x :: N) (y :: N).
Add x y =>
Nat x -> Nat y -> Nat (AddR x y)
add  (Nat n -> Nat y -> Nat (MulR n y)
forall (x :: N) (y :: N).
Mul x y =>
Nat x -> Nat y -> Nat (MulR x y)
mul  Nat n
x Nat y
y) Nat y
y


---------------------------------------------------------------------------------------------------
nat0    :: Nat Z
nat0 :: Nat 'Z
nat0    =  Nat 'Z
Zero
{-# INLINE nat0 #-}

nat1    :: Nat (S Z)
nat1 :: Nat ('S 'Z)
nat1    =  Nat 'Z -> Nat ('S 'Z)
forall (n :: N). Nat n -> Nat ('S n)
Succ Nat 'Z
Zero
{-# INLINE nat1 #-}

nat2    :: Nat (S (S Z))
nat2 :: Nat ('S ('S 'Z))
nat2    =  Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S 'Z) -> Nat ('S ('S 'Z)))
-> Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall a b. (a -> b) -> a -> b
$ Nat 'Z -> Nat ('S 'Z)
forall (n :: N). Nat n -> Nat ('S n)
Succ Nat 'Z
Zero
{-# INLINE nat2 #-}

nat3    :: Nat (S (S (S Z)))
nat3 :: Nat ('S ('S ('S 'Z)))
nat3    =  Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z))))
-> Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S 'Z) -> Nat ('S ('S 'Z)))
-> Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall a b. (a -> b) -> a -> b
$ Nat 'Z -> Nat ('S 'Z)
forall (n :: N). Nat n -> Nat ('S n)
Succ Nat 'Z
Zero
{-# INLINE nat3 #-}

nat4    :: Nat (S (S (S (S Z))))
nat4 :: Nat ('S ('S ('S ('S 'Z))))
nat4    =  Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z))))
-> Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S 'Z) -> Nat ('S ('S 'Z)))
-> Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall a b. (a -> b) -> a -> b
$ Nat 'Z -> Nat ('S 'Z)
forall (n :: N). Nat n -> Nat ('S n)
Succ Nat 'Z
Zero
{-# INLINE nat4 #-}

nat5    :: Nat (S (S (S (S (S Z)))))
nat5 :: Nat ('S ('S ('S ('S ('S 'Z)))))
nat5    =  Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z)))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z)))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z))))
-> Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S 'Z) -> Nat ('S ('S 'Z)))
-> Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall a b. (a -> b) -> a -> b
$ Nat 'Z -> Nat ('S 'Z)
forall (n :: N). Nat n -> Nat ('S n)
Succ Nat 'Z
Zero
{-# INLINE nat5 #-}

nat6    :: Nat (S (S (S (S (S (S Z))))))
nat6 :: Nat ('S ('S ('S ('S ('S ('S 'Z))))))
nat6    =  Nat ('S ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S ('S 'Z)))))
 -> Nat ('S ('S ('S ('S ('S ('S 'Z)))))))
-> Nat ('S ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z)))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z)))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z))))
-> Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S 'Z) -> Nat ('S ('S 'Z)))
-> Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall a b. (a -> b) -> a -> b
$ Nat 'Z -> Nat ('S 'Z)
forall (n :: N). Nat n -> Nat ('S n)
Succ Nat 'Z
Zero
{-# INLINE nat6 #-}

nat7    :: Nat (S (S (S (S (S (S (S Z)))))))
nat7 :: Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
nat7    =  Nat ('S ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S ('S ('S 'Z))))))
 -> Nat ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S ('S 'Z)))))
 -> Nat ('S ('S ('S ('S ('S ('S 'Z)))))))
-> Nat ('S ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z)))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z)))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z))))
-> Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S 'Z) -> Nat ('S ('S 'Z)))
-> Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall a b. (a -> b) -> a -> b
$ Nat 'Z -> Nat ('S 'Z)
forall (n :: N). Nat n -> Nat ('S n)
Succ Nat 'Z
Zero
{-# INLINE nat7 #-}

nat8    :: Nat (S (S (S (S (S (S (S (S Z))))))))
nat8 :: Nat ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
nat8    =  Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
 -> Nat ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S ('S ('S 'Z))))))
 -> Nat ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S ('S 'Z)))))
 -> Nat ('S ('S ('S ('S ('S ('S 'Z)))))))
-> Nat ('S ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z)))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z)))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z))))
-> Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S 'Z) -> Nat ('S ('S 'Z)))
-> Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall a b. (a -> b) -> a -> b
$ Nat 'Z -> Nat ('S 'Z)
forall (n :: N). Nat n -> Nat ('S n)
Succ Nat 'Z
Zero
{-# INLINE nat8 #-}

nat9    :: Nat (S (S (S (S (S (S (S (S (S Z)))))))))
nat9 :: Nat ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
nat9    =  Nat ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
 -> Nat ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
 -> Nat ('S ('S ('S ('S ('S ('S ('S ('S 'Z)))))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S ('S ('S 'Z))))))
 -> Nat ('S ('S ('S ('S ('S ('S ('S 'Z))))))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S ('S ('S ('S 'Z)))))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S ('S 'Z)))))
 -> Nat ('S ('S ('S ('S ('S ('S 'Z)))))))
-> Nat ('S ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S ('S ('S ('S 'Z))))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z)))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z))))))
-> Nat ('S ('S ('S ('S 'Z)))) -> Nat ('S ('S ('S ('S ('S 'Z)))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z)))))
-> Nat ('S ('S ('S 'Z))) -> Nat ('S ('S ('S ('S 'Z))))
forall a b. (a -> b) -> a -> b
$ Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z))))
-> Nat ('S ('S 'Z)) -> Nat ('S ('S ('S 'Z)))
forall a b. (a -> b) -> a -> b
$ Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall (n :: N). Nat n -> Nat ('S n)
Succ (Nat ('S 'Z) -> Nat ('S ('S 'Z)))
-> Nat ('S 'Z) -> Nat ('S ('S 'Z))
forall a b. (a -> b) -> a -> b
$ Nat 'Z -> Nat ('S 'Z)
forall (n :: N). Nat n -> Nat ('S n)
Succ Nat 'Z
Zero
{-# INLINE nat9 #-}