/* 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

2012-02-14: Orignal version developed from traditional OO version
2019-02-24: Updated to use interpolated lists, precondition for Succ,
            sealed trait Nat rather than abstract class;
            Updated comments
2019-02-27: Updated formatting and comments

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

sealed trait 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
    case Err             =>
      sys.error(s"No ordering between Zero and Err")
  }

  def toInt: Int = 0
}

case class Succ(p: Nat) extends Nat {
  // 'this' object represents value p+1

  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
    case Err     => sys.error(s"No ordering between Zero and Err")
  }

  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(s"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 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 toString
    println(s"Zero as String  ==> $Zero")
    println(s"Err as String   ==> $Err")
    println(s"three as String ==> $three")
    println(s"six as String   ==> $six")
    println(s"big as String   ==> $big")
    println(s"bad as String   ==> $bad")

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


    // Test Zero methods

    println(s"Zero + Zero      ==> ${Zero + Zero}")
    println(s"Zero + three     ==> ${Zero + three}")
    println(s"Zero + Err       ==> ${Zero + Err}")

    println(s"Zero - Zero      ==> ${Zero - Zero}")
    println(s"Zero - three     ==> ${Zero - three}")
    println(s"Zero - Err       ==> ${Zero - Err}")

    println(s"Zero == Zero     ==> ${Zero == Zero}")
    println(s"Zero == three    ==> ${Zero == three}")
    println(s"Zero == Err      ==> ${Zero == Err}")
    println(s"Zero == bad      ==> ${Zero == bad}")

    println(s"Zero < Zero      ==> ${Zero < Zero}")
    println(s"Zero < three     ==> ${Zero < three}")

    print(   "Zero < Err       ==> ")
    try   { println(Zero < Err) }
    catch { case ex: Throwable => 
              println(s"ERROR\n  ${ex.getMessage}") }

//  println(s"Zero < bad       ==> ${Zero < bad}")

    println(s"Zero <= Zero     ==> ${Zero <= Zero}")

    print(   "Zero <= Err      ==> ")
    try   { println(Zero <= Err) }
    catch { case ex: Throwable => 
              println(s"ERROR\n  ${ex.getMessage}") }

//  println(s"Zero <= bad      ==> ${Zero <= bad}")

    println(s"Zero > Zero      ==> ${Zero > Zero}")
    println(s"Zero > three     ==> ${Zero > three}")

    print(   "Zero > Err       ==> ")
    try   { println(Zero > Err) }
    catch { case ex: Throwable => 
              println(s"ERROR\n  ${ex.getMessage}") }

//  println(s"Zero > bad       ==> ${Zero > bad}")

    println(s"Zero.pred        ==> ${Zero.pred}")
    println(s"Zero.toInt       ==> ${Zero.toInt}")

    // Test Succ methods

    println(s"three + Zero     ==> ${three + Zero}")
    println(s"three + three    ==> ${three + three}")
    println(s"three + Err      ==> ${three + Err}")

    println(s"three - Zero     ==> ${three - Zero}")
    println(s"three - three    ==> ${three - three}")
    println(s"three - six      ==> ${three - six}")
    println(s"three - Err      ==> ${three - Err}")

    println(s"three == Zero    ==> ${three == Zero}")
    println(s"three == three   ==> ${three == three}") 
    println(s"three == six     ==> ${three == six}")
     println(s"three == Err     ==> ${three == Err}")
    println(s"three == bad     ==> ${three == bad}")

    println(s"three < Zero     ==> ${three < Zero}")
    println(s"three < three    ==> ${three < three}")
    println(s"three < six      ==> ${three < six}")
    println(s"six   < three    ==> ${six < three}")

    print(   "three < Err      ==> ")
    try   { println(three < Err) }
    catch { case ex: Throwable => 
              println(s"ERROR\n  ${ex.getMessage}") }

//  println(s"three < bad      ==> ${three < bad}")

    println(s"three <= Zero    ==> ${three <= Zero}")
    println(s"three <= three   ==> ${three <= three}")
    println(s"three <= six     ==> ${three <= six}")
    println(s"six   <= three   ==> ${six <= three}")

    print(   "three <= Err     ==> ")
    try   { println(three <= Err) }
    catch { case ex: Throwable => 
              println(s"ERROR\n  ${ex.getMessage}") }

//  println(s"three <= bad     ==> ${three <= bad}")

    println(s"three > Zero     ==> ${three > Zero}")
    println(s"three > three    ==> ${three > three}")
    println(s"three > six      ==> ${three > six}")
    println(s"six   > three    ==> ${six > three}")

    print(   "three > Err      ==> ")
    try   { println(three > Err) }
    catch { case ex: Throwable => 
              println(s"ERROR\n  ${ex.getMessage}") }

//  println(s"three > bad      ==> ${three > bad}")

    println(s"three.pred       ==> ${three.pred}")
    println(s"three.toInt      ==> ${three.toInt}")

    // Test Err methods

    println(s"Err + Zero       ==> ${Err + Zero}")
    println(s"Err + three      ==> ${Err + three}")
    println(s"Err + Err        ==> ${Err + Err}")

    println(s"Err - Zero       ==> ${Err - Zero}")
    println(s"Err - three      ==> ${Err - three}")
    println(s"Err - Err        ==> ${Err - Err}")

    println(s"Err == Zero      ==> ${Err == Zero}")
    println(s"Err == three     ==> ${Err == three}") 
    println(s"Err == Err       ==> ${Err == Err}") 
    println(s"Err == bad       ==> ${Err == bad}") 

    print(   "Err < three      ==> ")
    try   { println(Err < three) }
    catch { case ex: Throwable => 
              println(s"ERROR\n  ${ex.getMessage}")}

    println(s"Err.pred         ==> ${Err.pred}")
    println(s"Err.toInt        ==> ${Err.toInt}")

    // Test precondition on Succ construction
    print(    "Succ(Err)        ==> ")
    try   { println(Succ(Err)) }
    catch { case ex: Throwable => 
              println(s"ERROR\n  Succ constructor precondition fails")
	      println(s"${ex.getMessage}") 
          }
  }
}