module TypeUnary.Nat
(
module TypeUnary.TyNat
, Nat(..), zero, one, two, three, four
, withIsNat, natSucc, natIsNat
, natToZ, natEq, natAdd
, IsNat(..)
, (:<:)(..), Index(..), succI, index0, index1, index2, index3
) where
import Prelude hiding (foldr,sum)
import Control.Applicative ((<$>))
import Data.Maybe (isJust)
import Data.Proof.EQ
import TypeUnary.TyNat
data Nat :: * -> * where
Zero :: Nat Z
Succ :: IsNat n => Nat n -> Nat (S n)
instance Show (Nat n) where show = show . natToZ
withIsNat :: (IsNat n => Nat n -> a) -> (Nat n -> a)
withIsNat p Zero = p Zero
withIsNat p (Succ n) = p (Succ n)
natSucc :: Nat n -> Nat (S n)
natSucc = withIsNat Succ
natIsNat :: Nat n -> (IsNat n => Nat n)
natIsNat Zero = Zero
natIsNat (Succ n) = Succ n
natToZ :: Nat n -> Integer
natToZ Zero = 0
natToZ (Succ n) = (succ . natToZ) n
natEq :: Nat m -> Nat n -> Maybe (m :=: n)
Zero `natEq` Zero = Just Refl
Succ m `natEq` Succ n = liftEq <$> (m `natEq` n)
_ `natEq` _ = Nothing
natAdd :: Nat m -> Nat n -> Nat (m :+: n)
Zero `natAdd` n = n
Succ m `natAdd` n = natSucc (m `natAdd` n)
zero :: Nat N0
zero = Zero
one :: Nat N1
one = Succ zero
two :: Nat N2
two = Succ one
three :: Nat N3
three = Succ two
four :: Nat N4
four = Succ three
infix 4 :<:
data m :<: n where
ZLess :: Z :<: S n
SLess :: m :<: n -> S m :<: S n
data Index lim = forall n. IsNat n => Index (n :<: lim) (Nat n)
instance Eq (Index lim) where
Index _ n == Index _ n' = isJust (n `natEq` n')
succI :: Index m -> Index (S m)
succI (Index p n) = Index (SLess p) (Succ n)
index0 :: Index (N1 :+: m)
index0 = Index ZLess Zero
index1 :: Index (N2 :+: m)
index1 = succI index0
index2 :: Index (N3 :+: m)
index2 = succI index1
index3 :: Index (N4 :+: m)
index3 = succI index2
class IsNat n where nat :: Nat n
instance IsNat Z where nat = Zero
instance IsNat n => IsNat (S n) where nat = Succ nat