{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Repa.Scalar.Singleton.Nat
( N (..)
, Nat (..)
, Add (..)
, Mul (..)
, nat0, nat1, nat2, nat3, nat4, nat5, nat6, nat7, nat8, nat9)
where
data N = Z | S N
deriving instance Show N
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
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
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 #-}