module Data.NaturalNumber where
import Data.Typeable
import Data.Type.Equality
import TypeLevel.NaturalNumber hiding (NaturalNumber)
import qualified TypeLevel.NaturalNumber as TLN
import TypeLevel.NaturalNumber.Induction
data N a where
NZero :: N Zero
NSuccessorTo :: N n -> N (SuccessorTo n)
data UnknownN where
UnknownN :: NaturalNumber n => N n -> UnknownN
class (TLN.NaturalNumber n, Induction n) => NaturalNumber n where
asN :: N n
fromN :: N n -> n
instance NaturalNumber Zero where
asN = NZero
fromN _ = undefined
instance NaturalNumber n => NaturalNumber (SuccessorTo n) where
asN = NSuccessorTo asN
fromN _ = undefined
instance NaturalNumber n => Typeable (N n) where
typeOf n = mkTyConApp (mkTyCon $ "N#" ++ (show . naturalNumberAsInt . fromN) n) []
instance Show (N n) where
show = show . nToInt
instance Show UnknownN where
show (UnknownN n) = show n
instance Eq (N n) where
(==) _ _ = True
(/=) _ _ = False
instance EqT N where
eqT NZero NZero = Just Refl
eqT (NSuccessorTo m) (NSuccessorTo n) =
case m `eqT` n of
Just Refl -> Just Refl
Nothing -> Nothing
eqT _ _ = Nothing
nToInt :: N n -> Int
nToInt NZero = 0
nToInt (NSuccessorTo n) = 1 + nToInt n
unknownNToInt :: UnknownN -> Int
unknownNToInt (UnknownN n) = nToInt n
intToUnknownN :: Int -> UnknownN
intToUnknownN i
| i < 0 = error $ "Cannot convert negative number " ++ show i ++ " to a natural number."
| otherwise = go i
where
go 0 = UnknownN NZero
go i = case go (i1) of UnknownN n -> UnknownN (NSuccessorTo n)
intToN :: NaturalNumber n => Int -> N n
intToN i
| i == nToInt n = n
| otherwise = error $ show i ++ " /= " ++ show n
where n = asN