# Natural Number Arithmetic using Peano-Inspired Structures
# H. Conrad Cunningham, Professor
# Computer and Information Science
# University of Mississippi

# Developed for CSci 556, Multiparadigm Programming, Spring 2015

#234567890123456789012345678901234567890123456789012345678901234567890

# 2015-02-15: Developed prototype from Lua version

# This program defines a representation for the "natural numbers"
# (i.e., set Nat).  It uses a structural representation inspired by
# Peano's Postulates, a well-know axiomization of the natural numbers.
# The implementation does not use any builtin number type, except for
# the functions that convert to and from numbers.  We consider 0 as
# being a natural number as is customary for many computer scientists.

# Mathematically, we can define the set Nat (of natural numbers)
# inductively as follows:

#   x in Nat if and only if 
#        (1) x = 0                                # zero
#     or (2) (Exists y : y in Nat :: x = succ(y)) # successor function

# The Nat values use a unary representation for the natural numbers;
# there is one succ object in a linear structure for each natural
# number value greater than 0.


# DATA ABSTRACTION AND MODULARITY

# Internally, this package uses a tuple {:zero} to represent the
# natural number zero and a tuple {:succ, n} represents the natural
# number successor of natural number "n".

# This implementation of Nat has two layers.

# (1) The Primitive Representation and Operations layer implements the
# core operation zero, succ, pred, is_Nat, is_zero, and is_succ. It
# encapsulates the data representation.  That is, Nat's data
# representation is a "secret" of this layer (in terms of Parnas's
# information hiding concepts).

# (2) The Nonprimitive Operations layer implements several operations
# on the natural numbers using only the primitive operations. They do
# not access the data structures implementing the functions directly.

# The data representation could be changed in the primitive layer
# without modifying the nonprimitive layer or any code that uses the
# package through the provided functions.

# Thus the code here could be given in two modules. (a) The Primitive
# Operations layer could form one module that exports the seven
# primitives.  (b) The Nonprimitive Operations layer could form a
# second module that imports the Primitive Operations module and
# exports both the primitive operations and the nonprimitive
# operations that it provides.

defmodule Nat do

  # PRIMITIVE OPERATIONS

  #  Function "is_Nat" takes an object "n" and returns true if and
  #  only if "n" has a valid Nat representation.  This recursively
  #  checks arguments of succ for validity.

  def is_Nat({:zero})    do true end
  def is_Nat({:succ, n}) do is_Nat(n) end
  def is_Nat(_)          do false end


  #  Functions "is_zero" and "is_succ" take an object "n" and return
  #  true if and only the first-level structure of "n" is a zero or
  #  succ, respectively. These functions do not recursively check the
  #  argument of succ for validity.

  def is_zero {:zero}    do true  end
  def is_zero {:succ, _} do false end
  def is_zero x          do raise "Malformed Nat #{x}." end
  
  def is_succ {:succ, _} do true end
  def is_succ {:zero}    do false end
  def is_succ x          do raise "Malformed Nat #{x}." end

  # Function "zero" constructs and returns a zero Nat. 

  def zero() do {:zero} end

  #  Function "succ" constructs and returns the successor of its Nat
  #  argument "n".  It verifies that the first level structure of "n"
  #  is valid, but it does not recursively check the argument of succ.

  def succ(n) do
    case n do
      {:zero}    -> {:succ, n}
      {:succ, _} -> {:succ, n}
      _          -> raise "Malformed Nat #{n}."
    end
  end

  
  # Function "pred" extracts and returns the predecessor of its
  # non-zero Nat argument "n".

  def pred(n) do
    case n do
      {:succ, m} -> m
      {:zero}    -> raise "Cannot take predecessor of zero." 
      _          -> raise "Malformed Nat #{n}."
    end
  end

  
  # NONPRIMITIVE OPERATIONS

  # These operations use the primitive operations zero, succ, pred,
  # is_zero, is_succ, and is_Nat or other nonprimitive operations.
  # They should not directly access the data representation of the Nat
  # data type.  It should be possible to change the data
  # representation without affecting these functions.

  # Function "add" adds its two Nat arguments and returns their sum.

  def add(m,n) do
    cond do
      is_zero(m) -> n
      is_succ(m) -> add(pred(m),succ(n))
    end
  end


  # Function "sub" subtracts its second Nat argument from its first
  # Nat argument and returns the difference.  If the first is smaller
  # than the second, then an error results.

  def sub(m,n) do
    cond do
      is_zero(n) -> m
      is_succ(n) ->
        cond do
          is_succ(m) -> sub(pred(m),pred(n))
          is_zero(m) ->
            raise "Cannot subtract larger number from smaller."
        end
    end
  end

  
  # Function "eq" returns true if and only if its two Nat arguments
  # represent the same natural number values.

  def eq(m,n) do
    cond do
      is_succ(m) -> is_succ(n) and eq(pred(m),pred(n))
      is_zero(m) -> is_zero(n)
    end
  end

  
  # Functions "lt" returns true if and only if its first Nat argument
  # is less than its second Nat argument, when compared as natural
  # number values.

  def lt(m,n) do
    cond do
      is_succ(m) -> is_succ(n) and lt(pred(m),pred(n))
      is_zero(m) -> is_succ(n)
    end
  end

  # Functions "gt" returns true if and only if its first Nat argument
  # is greater than its second Nat argument, when compared as natural
  # number values.

  def gt(m,n) do lt(n,m) end

  
  # Function "as_Nat" returns the Nat representation of the
  # nonnegative number argument "i".

  def as_Nat(i) when is_integer(i) and i >= 0 do
    cond do
      i == 0 -> zero()
      i >  0 -> succ(as_Nat(i-1))
    end
  end

  # Function "as_integer" returns the numeric value for the its Nat
  # argument "n".

  def as_integer(n) do
    cond do
      is_zero(n) -> 0
      is_succ(n) -> 1 + as_integer(pred(n))
    end
  end

  
  # Function "as_string" returns a string representation of "n".
  
  def as_string(n) do
    cond do
      is_zero(n) -> "Zero"
      is_succ(n) -> "Succ(#{as_string(pred(n))})"
    end
  end

end