------------------------------------------------------------------------------
--- Library defining natural numbers in Peano representation and
--- some operations on this representation.
---
--- @author Michael Hanus
--- @version May 2017
--- @category general
------------------------------------------------------------------------------

module Nat
  ( Nat(..), fromNat, toNat, add, sub, mul, leq
  ) where

--- Natural numbers defined in Peano representation.
data Nat = Z | S Nat
 deriving (Eq,Show)

--- Transforms a natural number into a standard integer.
fromNat :: Nat -> Int
fromNat Z     = 0
fromNat (S n) = 1 + fromNat n

--- Transforms a standard integer into a natural number.
toNat :: Int -> Nat
toNat n | n == 0 = Z
        | n > 0  = S (toNat (n-1))

--- Addition on natural numbers.
add :: Nat -> Nat -> Nat
add Z     n = n
add (S m) n = S(add m n)

--- Subtraction defined by reversing addition.
sub :: Nat -> Nat -> Nat
sub x y | add y z == x  = z where z free

--- Multiplication on natural numbers.
mul :: Nat -> Nat -> Nat
mul Z     _ = Z
mul (S m) n = add n (mul m n)

-- less-or-equal predicated on natural numbers:
leq :: Nat -> Nat -> Bool
leq Z     _     = True
leq (S _) Z     = False
leq (S x) (S y) = leq x y