--[[ 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

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.

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.

--]]

-- 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 "treeConcat" takes a recursive list of lists in argument
-- "t" and returns the corresponding parenthesized traversal string.
-- A list is stored in the low positive integer indices of an
-- list-style Lua table. This package uses this function mostly for
-- error messages and in dbugging. (This was borrowed from the
-- author's KILT Utilities Module.)

local function treeConcat(t)
  if type(t) ~= "table" then return tostring(t) end
  local res = {}
  for i = 1, #t do
    res[i] = treeConcat(t[i])
  end
  return "(" .. table.concat(res," ") .. ")"
end

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

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 "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: " .. treeConcat(n), 2)
  end
end

-- 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(m[2],succ(n))
  else
    error("add called with invalid argument: " .. treeConcat(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(m[2],n[2])
    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(m[2],n[2])
  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(m[2],n[2])
  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(m[2],n[2])
  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: " .. treeConcat(i)
-- 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(n[2])
  else
    error("toInt called will invalid argument: " .. treeConcat(i), 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(n[2]) .. ")"
    end
  else
    error("natToString called with invalid Nat: " ..
          treeConcat(n), 2)
  end
end

-- MAIN PROGRAM (partial testing)

local three = succ(succ(succ(ZERO)))
local six   = succ(succ(succ(three)))
local big   = 100
local bad   = -1

print("treeConcat(ZERO)    ==> " .. treeConcat(ZERO))
print("treeConcat(three)   ==> " .. treeConcat(three))
print("treeConcat(six)     ==> " .. treeConcat(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)))