/* Natural Number Arithmetic using Peano-Inspired Structures
   Using Functional Object-Oriented Style with Case Classes
   H. Conrad Cunningham, Professor
   Computer and Information Science
   University of Mississippi

1234567890123456789012345678901234567890123456789012345678901234567890

14 Feb 2012: Orignal version developed from traditional OO version

This version puts all the functionality into the case classes/object
methods.

*/

trait Ord[T] {
  def < (that: T): Boolean
  def <=(that: T): Boolean = (this < that) || (this == that)
  def > (that: T): Boolean = !(this <= that)
  def >=(that: T): Boolean = !(this < that)
}

abstract class Nat extends Ord[Nat] {
  def pred: Nat
  def +(that:Nat): Nat
  def -(that:Nat): Nat
  def toInt: Int
}

case object Zero extends Nat {

  def pred: Nat = Err

  def +(that:Nat): Nat = that

  def -(that:Nat): Nat = that match {
    case Zero => Zero
    case _    => Err
  }

  def <(that:Nat): Boolean = that match {
    case Succ(pred:Nat) => true
    case Zero           => false
  }

  def toInt: Int = 0
}

case class Succ(p:Nat) extends Nat {
  require(p ne Err)

  def pred: Nat = p

  def +(that: Nat): Nat = that match { 
    case Succ(q) => Succ(this) + q
    case Zero    => this
    case Err     => Err
  }

  def -(that:Nat): Nat = that match {
    case Succ(q)  => p - q
    case Zero     => this
    case Err      => Err
  }

  def <(that:Nat): Boolean = that match {
    case Succ(q) => p < q
    case Zero    => false
  }

  def toInt: Int = 1 + p.toInt
}

case object Err extends Nat {

  def +(that:Nat): Nat = Err 

  def -(that:Nat): Nat = Err 

  def pred: Nat = Err

  def <(n: Nat): Boolean = 
    sys.error("No ordering between Err and " + n)

  def toInt: Int = -1
}

object Nat {
  def toNat(n:Int): Nat = 
    if (n > 0)
      Succ(toNat(n-1)) 
    else if (n == 0)
      Zero 
    else
      Err
}

// Allow companion object method access without "Nat."  qualification

import Nat._

object TestCaseObjNats {

  // Main method for testing
  def main(args: Array[String]) {

    // Constants to use in tests
    val three = Succ(Succ(Succ(Zero)))
    val six   = Succ(Succ(Succ(three)))
    val big   = 100
    val bad   = -1

    // Test conversion from Int to Nat and testing toString
    println("toNat(0)             ==> " + toNat(0))
    println("toNat(5)             ==> " + toNat(5))
    println("toNat(big)           ==> " + toNat(big))
    println("toNat(bad)           ==> " + toNat(bad))

    // Test Zero methods

    println("Zero + Zero          ==> " + (Zero + Zero))
    println("Zero + three         ==> " + (Zero + three))
    println("Zero + Err           ==> " + (Zero + Err))

    println("Zero - Zero          ==> " + (Zero - Zero))
    println("Zero - three         ==> " + (Zero - three))
    println("Zero - Err           ==> " + (Zero - Err))

    println("Zero == Zero         ==> " + (Zero == Zero))
    println("Zero == three        ==> " + (Zero == three))
    println("Zero == Err          ==> " + (Zero == Err))
    println("Zero == bad          ==> " + (Zero == bad))

    println("Zero < Zero          ==> " + (Zero < Zero))
    println("Zero < three         ==> " + (Zero < three))

    print(  "Zero < Err           ==> ")
    try   { println((Zero < Err)) }
    catch { case ex: Throwable => println("Error:  " + ex.getMessage)}

//  println("Zero < bad           ==> " + (Zero < bad))

    println("Zero <= Zero         ==> " + (Zero <= Zero))

    print(  "Zero <= Err          ==> ")
    try   { println((Zero <= Err)) }
    catch { case ex: Throwable => println("Error:  " + ex.getMessage)}

//  println("Zero <= bad          ==> " + (Zero <= bad))

    println("Zero > Zero          ==> " + (Zero > Zero))
    println("Zero > three         ==> " + (Zero > three))

    print(  "Zero > Err           ==> ")
    try   { println((Zero > Err)) }
    catch { case ex: Throwable => println("Error:  " + ex.getMessage)}

//  println("Zero > bad           ==> " + (Zero > bad))

    println("Zero.pred            ==> " + Zero.pred)
    println("Zero.toInt           ==> " + Zero.toInt)

    // Test Succ methods

    println("three + Zero         ==> " + (three + Zero))
    println("three + three        ==> " + (three + three))
    println("three + Err          ==> " + (three + Err))

    println("three - Zero         ==> " + (three - Zero))
    println("three - three        ==> " + (three - three))
    println("three - six          ==> " + (three - six))
    println("three - Err          ==> " + (three - Err))

    println("three == Zero        ==> " + (three == Zero))
    println("three == three       ==> " + (three == three)) 
    println("three == six         ==> " + (three == six))
    println("three == Err         ==> " + (three == Err))
    println("three == bad         ==> " + (three == bad))

    println("three < Zero         ==> " + (three < Zero))
    println("three < three        ==> " + (three < three))
    println("three < six          ==> " + (three < six))
    println("six   < three        ==> " + (six < three))

    print(  "three < Err          ==> ")
    try   { println((three < Err)) }
    catch { case ex: Throwable => println("Error:  " + ex.getMessage)}

//  println("three < bad          ==> " + (three < bad))

    println("three <= Zero        ==> " + (three <= Zero))
    println("three <= three       ==> " + (three <= three))
    println("three <= six         ==> " + (three <= six))
    println("six   <= three       ==> " + (six <= three))

    print(  "three <= Err         ==> ")
    try   { println((three <= Err)) }
    catch { case ex: Throwable => println("Error:  " + ex.getMessage)}

//  println("three <= bad         ==> " + (three <= bad))

    println("three > Zero         ==> " + (three > Zero))
    println("three > three        ==> " + (three > three))
    println("three > six          ==> " + (three > six))
    println("six   > three        ==> " + (six > three))

    print(  "three > Err          ==> ")
    try   { println((three > Err)) }
    catch { case ex: Throwable => println("Error:  " + ex.getMessage)}

//  println("three > bad          ==> " + (three > bad))

    println("three.pred           ==> " + three.pred)
    println("three.toInt          ==> " + three.toInt)

    // Test Err methods

    println("Err + Zero           ==> " + (Err + Zero))
    println("Err + three          ==> " + (Err + three))
    println("Err + Err            ==> " + (Err + Err))

    println("Err - Zero           ==> " + (Err - Zero))
    println("Err - three          ==> " + (Err - three))
    println("Err - Err            ==> " + (Err - Err))

    println("Err == Zero          ==> " + (Err == Zero))
    println("Err == three         ==> " + (Err == three)) 
    println("Err == Err           ==> " + (Err == Err)) 
    println("Err == bad           ==> " + (Err == bad)) 

    print(  "Err < three          ==> ")
    try   { println((Err < three)) }
    catch { case ex: Throwable => println("Error:  " + ex.getMessage)}

    println("Err.pred             ==> " + Err.pred)
    println("Err.toInt            ==> " + Err.toInt)

    // Test precondition on Succ construction
    print(  "Succ(Err)            ==> ")
    try   { println(Succ(Err)) }
    catch { case ex: Throwable => 
              println("Error on Succ constructor precondition check: "
	              + ex.getMessage) 
          }
  }
}