module TypeUnary.Nat
(
module TypeUnary.TyNat
, Nat(..), zero, one, two, three, four
, withIsNat, natSucc, natIsNat
, natToZ, natEq, natAdd, natMul
, IsNat(..)
, (:<:)(..), Index(..), succI, index0, index1, index2, index3
, coerceToIndex
) 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 n = show (natToZ n :: Integer)
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 :: (Enum a, Num a) => Nat n -> a
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)
natMul :: forall m n. Nat m -> Nat n -> Nat (m :*: n)
Zero `natMul` _ = Zero
Succ m `natMul` n = n `natAdd` (m `natMul` 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
coerceToIndex :: (Show i, Integral i, IsNat m) => i -> Index m
coerceToIndex = coerceToIndex' nat
coerceToIndex' :: (Show i, Integral i) => Nat m -> i -> Index m
coerceToIndex' mOrig niOrig = loop mOrig niOrig
where
loop :: (Show i, Integral i) => Nat m -> i -> Index m
loop Zero _ = error $ "coerceToIndex: out of bounds: "
++ show niOrig ++ " should be less than "
++ show mOrig
loop (Succ _) 0 = Index ZLess Zero
loop (Succ m') ni' = succI (loop m' (ni'1))
class IsNat n where nat :: Nat n
instance IsNat Z where nat = Zero
instance IsNat n => IsNat (S n) where nat = Succ nat