«K12/K13» N0.hs «PDF», «POD»

module N0 where

import Base

data N0 = Zero | Succ N0 deriving (Eq)
zero = Zero
one  = Succ Zero

instance Show N0 where
  show a = "N0[" ++ (show . toInteger $ a) ++ "]"

instance Num N0 where
  a + b | b == Zero = a
  a + b | b /= one  = a + (b - one) + one
  a + b | b == one  = Succ a

  a - b | a == b = Zero
  a - b | a /= b = one + (a - (b + one))

  a * b | b == Zero = Zero
  a * b | b /= Zero = a * (b - one) + a
  
  negate _ = error "Cannot negate numbers of N0!"
  abs    a = a

  signum Zero = Zero
  signum _    = one

  fromInteger 0 = Zero
  fromInteger n = Succ $ fromInteger (n - 1)

instance Real N0 where
  toRational = toRational . toInteger

instance Enum N0 where
  succ a = Succ a
  pred Zero     = error "No predecessor of 0 of N0!"
  pred (Succ a) = a

  toEnum   = fromInteger . fromIntegral
  fromEnum = fromIntegral . toInteger

instance Integral N0 where
  a `div` b | b == Zero = error "Division by N0[0]!"
  a `div` b | a == b    = one
  a `div` b | otherwise = one + (a - b) `div` b

  a `rem` b | a < b = a
  a `rem` b | otherwise = (a - b) `rem` b

  toInteger Zero     = 0
  toInteger (Succ a) = 1 + toInteger a

instance Ord N0 where
  a <= b | a == b    = True
  a <= b | b == Zero = False
  a <= b | otherwise = a <= (b - one)