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

Developed for CSci 658, Software Language Engineering, Fall 2013

1234567890123456789012345678901234567890123456789012345678901234567890

2013-09-05: Developed prototype 
2013-10-06: Added constructor Zero and accessor pred to provide a
            primitive abstraction layer; modified nonprimitives to
            use only the primitive functions. 
            Replaced function treeConcat by show_data for error 
            messages and testing (to make independent of data rep)
            Changed names succ to Succ and natfields to NATFIELDS to
            follow naming convention.
            Improved comments and code format
2014-11-08: Added comments about data abstraction and modularity

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 axiomatization 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.

In this package, a table { ZERO_TYPE } represents the natural number
zero and { SUCC_TYPE, n } represents the natural number successor of
natural number "n". (The constants ZERO_TYPE and SUCC_TYPE are as
defined below.) The constructor operations Zero and Succ create the
appropriate tables.

DATA ABSTRACTION AND MODULARITY

This implementation of Nat has two layers.

(1) The Primitive Representation and Operations layer implements the
core operation Zero, Succ, pred, isNat, isZero, isSucc, and
natToString and the debugging/error utility function show_data. 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 three modules. (a) The Primitive
Operations could form one module that exports the seven primitive and
one utility function.  (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. (c) The main program could be in a third module that
imports the Nonprimitive Operations module and uses the natural number
operations exported.

--]]


-- UTILITY FUNCTIONS

-- Function "show_data" converts raw Lua data structures to strings to
-- assist in debugging and testing. (This code was borrowed from the
-- author's Complex Number package.)

local function show_data(d)
  if type(d) == "table" then
    local res = {}
    for k,v in pairs(d) do
      res[#res+1] = "[" .. show_data(k) .. "] = " .. show_data(v)
    end
    return "(" .. table.concat(res, ", ") .. ")"
  else
    return tostring(d)
  end
end


-- PRIMITIVE REPRESENTATION AND OPERATIONS

-- Constants for operator types and their displayed names
local SUCC_TYPE, SUCC_STR = "Succ", "Succ"
local ZERO_TYPE, ZERO_STR = "Zero", "Zero"

-- Singleton constant for Zero value
local ZERO = {ZERO_TYPE}

-- Table mapping operator types to number of needed fields in rep
local NATFIELDS = { [ZERO_TYPE] = 1, [SUCC_TYPE] = 2 }

-- Function "isNatStruct" takes an object "n" and returns true if and
-- only if "n" has a valid first-level structure for a Nat
-- representation.  It does not recursively verify that an operand of
-- Succ is valid. This function is intended to be used in implementing
-- other primitive operations, not by nonprimitive operations.

local function isNatStruct(n) 
  return type(n) == "table" and #n > 0 and #n == NATFIELDS[n[1]]
end

-- Function "isNat" 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.

local function isNat(n)
  if isNatStruct(n) then
    local op = n[1]
    return op == ZERO_TYPE or (op == SUCC_TYPE and isNat(n[2]))
  else
    return false
  end
end

-- Functions "isZero" and "isSucc" 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. 

local function isZero(n)
  return isNatStruct(n) and n[1] == ZERO_TYPE
end

local function isSucc(n)
  return isNatStruct(n) and n[1] == SUCC_TYPE
end

-- Function "Zero" constructs and returns a zero Nat. (In this
-- version, it returns the singleton table constant ZERO.)

local function Zero()
  return 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.

local function Succ(n)
  if isNatStruct(n) then
    return {SUCC_TYPE,n}
  else
    error("Invalid argument to Succ: " .. show_data(n), 2)
  end
end

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

local function pred(n)
  if isSucc(n) then
    return n[2]
  else
    error("Invalid argument to pred: " .. show_data(n), 2)
  end
end

-- Function "natToString" takes a Nat "n" and returns a string
-- representation of the Nat representation.

local function natToString(n)
  if isNat(n) then
    if isZero(n) then
      return ZERO_STR
    else
      return SUCC_STR .. "(" .. natToString(pred(n)) .. ")"
    end
  else
    error("natToString called with invalid Nat: " ..
          show_data(n), 2)
  end
end


-- NONPRIMITIVE OPERATIONS

-- These operations use the primitive operations Zero, Succ, pred,
-- isZero, isSucc, and isNat 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.

-- Caveat: Function "show_data", used to format error messages and in
-- testing, violates the policy of hiding the data representation. It
-- should work with any representation, but it reveals the details of
-- that implementation.

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

local function add(m,n)
  if isZero(m) then 
    return n
  elseif isSucc(m) then
    return add(pred(m),Succ(n))
  else
    error("add called with invalid argument: " .. show_data(m), 2)
  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.

local function sub(m,n)
  if isZero(n) then 
    return m
  elseif isSucc(n)then
    if isSucc(m) then
      return sub(pred(m),pred(n))
    else
      error("sub called with first argument less than second,", 2)
    end
  else
    error("sub called with invalid second argument.", 2)
  end
end

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

local function eq(m, n)
  if isSucc(m) then
    return isSucc(n) and eq(pred(m),pred(n))
  else
    return isZero(m) and isZero(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.

local function lt(m,n)
  if isSucc(m) then
    return isSucc(n) and lt(pred(m),pred(n))
  else
    return isZero(m) and isSucc(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.

local function gt(m, n)
  if isSucc(n) then
    return isSucc(m) and gt(pred(m),pred(n))
  else
    return isZero(n) and isSucc(m)
  end
end

-- Function "toNat" returns the Nat representation of the nonnegative
-- number argument "i". 

local function toNat(i)
  if i == 0 then
    return Zero()
  elseif i > 0 then
    return Succ(toNat(i-1))
  else
    error("toNat called with negative argument: " .. show_data(i))
  end
end

-- Function "toInt" returns the numeric value for the its Nat argument
-- "n".

local function toInt(n)
  if isZero(n) then
    return 0
  elseif isSucc(n) then
    return 1 + toInt(pred(n))
  else
    error("toInt called will invalid argument: " .. show_data(i), 2)
  end
end


-- MAIN PROGRAM (partial testing)

local zero  = Zero()
local three = Succ(Succ(Succ(zero)))
local six   = Succ(Succ(Succ(three)))
local big   = 100
local bad   = -1

print("show_data(zero)      ==> " .. show_data(zero))
print("show_data(three)     ==> " .. show_data(three))
print("show_data(six)       ==> " .. show_data(six))

print("natToString(zero)    ==> " .. natToString(zero))
print("natToString(three)   ==> " .. natToString(three))
print("natToString(six)     ==> " .. natToString(six))

print("toNat(0)             ==> " .. natToString(toNat(0)))
print("toNat(3)             ==> " .. natToString(toNat(3)))
print("toNat(6)             ==> " .. natToString(toNat(6)))
print("toNat(big)           ==> " .. natToString(toNat(big)))

print("toInt(zero)          ==> " .. tostring(toInt(zero)))
print("toInt(three)         ==> " .. tostring(toInt(three)))
print("toInt(six)           ==> " .. tostring(toInt(six)))

print("add(zero,zero)       ==> " .. natToString(add(zero,zero)))
print("add(zero,three)      ==> " .. natToString(add(zero,three)))
print("add(three,zero)      ==> " .. natToString(add(three,zero)))
print("add(three,three)     ==> " .. natToString(add(three,three)))

print("sub(zero,zero)       ==> " .. natToString(sub(zero,zero)))
print("sub(three,zero)      ==> " .. natToString(sub(three,zero)))
print("sub(three,three}     ==> " .. natToString(sub(three,three)))
print("sub(six,three}       ==> " .. natToString(sub(six,three)))

print("eq(zero,zero)        ==> " .. tostring(eq(zero,zero)))
print("eq(zero,three)       ==> " .. tostring(eq(zero,three)))
print("eq(three,zero)       ==> " .. tostring(eq(three,zero)))
print("eq(three,three)      ==> " .. tostring(eq(three,three))) 
print("eq(three,six)        ==> " .. tostring(eq(three,six)))

print("lt(zero,zero)        ==> " .. tostring(lt(zero,zero)))
print("lt(zero,three)       ==> " .. tostring(lt(zero,three)))
print("lt(three,zero)       ==> " .. tostring(lt(three,zero)))
print("lt(three,three)      ==> " .. tostring(lt(three,three)))
print("lt(three,six)        ==> " .. tostring(lt(three,six)))
print("lt(six,three)        ==> " .. tostring(lt(six,three)))

print("gt(zero,zero)        ==> " .. tostring(gt(zero,zero)))
print("gt(zero,three)       ==> " .. tostring(gt(zero,three)))
print("gt(three,zero)       ==> " .. tostring(gt(three,zero)))
print("gt(three,three)      ==> " .. tostring(gt(three,three)))
print("gt(three,six)        ==> " .. tostring(gt(three,six)))
print("gt(six,three)        ==> " .. tostring(gt(six,three)))