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

module N where

import Base
import N0 (N0)
import qualified N0 (zero, one)

data N = Succ N0 deriving (Eq)
one = Succ N0.zero

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

n02n n = Succ $ n - N0.one
n2n0 (Succ n) = n + N0.one

instance Num N where
  a + b = n02n $ n2n0 a + n2n0 b
  a - b = n02n $ n2n0 a - n2n0 b
  a * b = n02n $ n2n0 a * n2n0 b

  negate _ = error "Cannot negate numbers of N!"
  abs    a = a
  signum _ = one

  fromInteger = n02n . fromInteger

instance Real N where
  toRational = toRational . toInteger

instance Enum N where
  succ a        = Succ $ n2n0 a
  pred (Succ a) = n02n a

  toEnum   = fromInteger . fromIntegral
  fromEnum = fromIntegral . toInteger

instance Integral N where
  a `div` b = n02n $ n2n0 a `div` n2n0 b
  a `rem` b = n02n $ n2n0 a `rem` n2n0 b
  toInteger = toInteger . n2n0

instance Ord N where
  a <= b = n2n0 a <= n2n0 b