{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeOperators #-}
-- | Type variable.
module Language.Symantic.Lib.Data.Peano where

import Data.Type.Equality ((:~:)(Refl))

-- * Types 'Zero' and 'Succ'
-- | Type-level peano numbers of kind '*'.
data Zero
data Succ p

-- * Type 'SPeano'
-- | Singleton for peano numbers.
data SPeano p where
 SZero :: SPeano Zero
 SSucc :: SPeano p -> SPeano (Succ p)

integral_from_peano :: Integral i => SPeano p -> i
integral_from_peano SZero = 0
integral_from_peano (SSucc x) = 1 + integral_from_peano x

peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret
peano_from_integral 0 k = k SZero
peano_from_integral i k | i > 0 =
	peano_from_integral (i - 1) $ \p -> k (SSucc p)
peano_from_integral _ _ = error "peano_from_integral"

peano_eq :: forall x y. SPeano x -> SPeano y -> Maybe (x :~: y)
peano_eq SZero SZero = Just Refl
peano_eq (SSucc x) (SSucc y)
 | Just Refl <- x `peano_eq` y
 = Just Refl
peano_eq _ _ = Nothing