module Number.Peano.Inf
( Nat
, infinity
, inductive_infinity
, diff
, zeroDiff
, infDiff
, (-|)
) where
import Test.LazySmallCheck (Serial(..), cons0, cons1, (\/))
data Nat
= Zero
| Succ Nat
| Inf
instance Serial Nat where
series = cons0 Zero \/ cons1 Succ \/ cons0 Inf
infinity :: Nat
infinity = Inf
inductive_infinity :: Nat
inductive_infinity = let n = Succ n in n
instance Eq Nat where
Zero == Zero = True
Succ n == Succ m = n == m
Inf == Inf = True
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 = EQ
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 = False
Inf < Succ m = Inf < m
Succ n < Inf = n < Inf
n > m = m < n
n <= m = not (m < n)
n >= m = not (n < m)
Zero `max` m = m
n `max` Zero = n
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
toInteger' :: Nat -> Maybe Integer
toInteger' n = f 0 n where
f i Zero = Just i
f i (Succ m) = i' `seq` f i' m where i' = i+1
f _ Inf = Nothing
instance Show Nat where
show n = case toInteger' n of
Just i -> show i
Nothing -> "infinity"
infix 6 `diff`
diff
:: Nat
-> Nat
-> Either Nat Nat
n `diff` Zero = Left n
Zero `diff` m = Right m
Succ n `diff` Succ m = n `diff` m
Inf `diff` Inf = error "Number.Peano.Inf: infinity - infinity."
Inf `diff` Succ m = Inf `diff` m
Succ n `diff` Inf = n `diff` Inf
infixl 6 `infDiff`
infDiff :: Nat -> Nat -> Either Nat Nat
Inf `infDiff` _ = Left Inf
Succ n `infDiff` Succ m = n `infDiff` m
Succ n `infDiff` Inf = n `infDiff` Inf
n `infDiff` Zero = Left n
Zero `infDiff` m = Right m
infixl 6 `zeroDiff`
zeroDiff :: Nat -> Nat -> Either Nat Nat
n `zeroDiff` Zero = Left n
Zero `zeroDiff` m = Right m
Succ n `zeroDiff` Succ m = n `zeroDiff` m
Inf `zeroDiff` Inf = Left Zero
Inf `zeroDiff` Succ m = Inf `zeroDiff` m
Succ n `zeroDiff` Inf = n `zeroDiff` Inf
infixl 6 -|
(-|) :: Nat -> Nat -> Nat
n -| m = case n `diff` m of
Left k -> k
Right _ -> Zero
instance Num Nat where
n m = case n `diff` m of
Left k -> k
Right _ -> error "Number.Peano.Inf: 0 - succ n."
Zero + m = m
Succ n + m = Succ (n + m)
Inf + _ = Inf
Succ n * m = m + n * m
Zero * _ = Zero
_ * Zero = Zero
Inf * _ = Inf
fromInteger i | i < 0 = error "Number.Peano.Inf: fromInteger on negative value."
fromInteger i = iterate Succ Zero !! fromInteger i
abs n = n
signum Zero = Zero
signum _ = Succ Zero
instance Enum Nat where
succ = Succ
pred Inf = Inf
pred (Succ n) = n
pred Zero = error "Number.Peano.Inf: pred 0."
toEnum i | i < 0 = error "Number.Peano.Inf: 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
f _ Inf = error "Number.Peano.Inf: fromEnum infinity."
enumFrom = iterate Succ
enumFromTo n m = case m `infDiff` n of
Right _ -> []
Left k -> f k n where
f Zero l = [l]
f (Succ j) l = l: f j (Succ l)
f Inf l = iterate Succ l
enumFromThen n n' = case n `zeroDiff` n' of
Left Zero -> n: repeat n'
Left d -> n: n': f (n' `zeroDiff` d) where
f (Right _) = []
f (Left j) = j: f (j `zeroDiff` d)
Right d -> n: iterate (d +) n'
enumFromThenTo n n' m = case n `zeroDiff` n' of
Left Zero -> n: repeat n'
Left d -> case m `compare` n of
EQ -> [n]
GT -> []
LT -> n: f (n' `zeroDiff` m) n' where
f (Right _) _ = []
f (Left j) l = l: f (j `zeroDiff` d) (l d)
Right d -> case m `infDiff` n of
Right _ -> []
Left k -> n: f (k `infDiff` d) n' where
f (Right _) _ = []
f (Left j) l = l: f (j `infDiff` d) (d + l)
instance Real Nat where
toRational n = toRational (fromIntegral n :: Integer)
instance Integral Nat where
toInteger n = case toInteger' n of
Just i -> i
Nothing -> error "Number.Peano.Inf: toInteger infinity."
quotRem _ _ = error "Number.Peano.Inf: quotRem not implemented."
instance Bounded Nat where
minBound = Zero
maxBound = Inf