module Number.Peano.Inf
( Nat (Zero, Succ)
, infinity
, isInfinity
, (-|)
) where
import Data.Ratio ((%))
data Nat
= Zero
| Succ Nat
| Inf
infinity :: Nat
infinity = Inf
isInfinity :: Nat -> Bool
isInfinity Zero = False
isInfinity Inf = True
isInfinity (Succ n) = isInfinity n
instance Eq Nat where
Zero == Zero = True
Succ n == Succ m = n == m
Inf == Inf = error "Nat: infinity == infinity"
Succ n == Inf = n == Inf
Inf == Succ m = Inf == m
_ == _ = False
instance Ord Nat where
Zero `compare` Zero = EQ
Zero `compare` _ = LT
_ `compare` Zero = GT
Succ n `compare` Succ m = n `compare` m
Inf `compare` Inf = error "Nat: infinity `compare` infinity"
Inf `compare` Succ m = Inf `compare` m
Succ n `compare` Inf = n `compare` Inf
_ < Zero = False
Zero < _ = True
Succ n < Succ m = n < m
Inf < Inf = error "Nat: infinity < infinity"
Inf < Succ m = Inf < m
Succ n < Inf = n < Inf
x > y = y < x
x <= y = not (y < x)
x >= y = not (x < y)
Zero `max` x = x
x `max` Zero = x
Succ n `max` Succ m = Succ (n `max` m)
_ `max` _ = Inf
Zero `min` _ = Zero
_ `min` Zero = Zero
Succ n `min` Succ m = Succ (n `min` m)
Inf `min` m = m
n `min` Inf = n
instance Show Nat where
show Inf = "infinity"
show x = show $ toInteger x
infixl 6 -|
(-|) :: Nat -> Nat -> Nat
Inf -| Inf = error "Nat: infinity -| infinity"
Inf -| _ = Inf
Succ n -| Succ m = n -| m
n -| Zero = n
_ -| _ = Zero
instance Num Nat where
Inf Inf = error "Nat: infinity - infinity"
Inf _ = Inf
Succ n Succ m = n m
n Zero = n
_ Inf = error "Nat: n - inifinty"
Zero Succ _ = error "Nat: 0 - succ n"
Zero + m = m
Succ n + m = Succ (n + m)
Inf + _ = Inf
Succ n * m = m + n * m
Zero * _ = Zero
Inf * _ = Inf
fromInteger i | i < 0 = error "Nat: fromInteger on negative value."
fromInteger i = iterate Succ Zero !! fromInteger i
abs x = x
signum Zero = Zero
signum _ = Succ Zero
instance Enum Nat where
toEnum i | i < 0 = error "Nat: toEnum on negative value."
toEnum i = iterate Succ Zero !! i
fromEnum n = f 0 n where
f i Zero = i
f i (Succ m) = i' `seq` f i' m where i' = i+1
instance Real Nat where
toRational n = fromIntegral n % 1
instance Integral Nat where
toInteger n = f 0 n where
f i Zero = i
f i (Succ m) = i' `seq` f i' m where i' = i+1
quotRem _ _ = error "Nat: quotRem not implemented."