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

1234567890123456789012345678901234567890123456789012345678901234567890

2012-02-14: Developed from regular OO version
2016-02-10: Cleaned code and format; changed obsolete Scala usage
2019-02-24: Updated to use interpolated lists, precondition for Succ,
            sealed trait Nat rather than abstract class; Added err
            of all < comparions involving Err; Updated comments
2019-02-27: Updated formatting and comments

This version uses case classes and implements the comparison methods on
the case class/object instances. But it implements most functionality
in a module of functions. See the extensive description in the
traditional object-oriented version.

Case classes generated the needed implementations of equals and
toString and simplified construction.

*/

/* 2019-02-24 Note: Using builtin trait scala.math.Ordered would
   enable better use of Scala features.
*/

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]
sealed trait Nat extends Ord[Nat]

case object Zero extends Nat {
  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")
  }
}
    
case class Succ(p: Nat) extends Nat {
  // 'this' object represents value p+1

  require(p ne Err) // throw IllegalArgumentException if not
                    // ne and eq are reference equality operators

  def <(that: Nat): Boolean = that match {
    case Succ(q) => p < q
    case Zero    => false
    case Err     => sys.error(s"No ordering between Succ and Err")

  }
}

case object Err extends Nat {
  def <(n: Nat): Boolean = 
    sys.error(s"No ordering between Err and $n")
}

object Nat {

  def pred(n: Nat): Nat = n match {
    case Succ(p) => p
    case _       => Err
  }

  // uses pattern match on a pair of Nats
  def add(m:Nat, n:Nat): Nat = (m,n) match {
    case (Succ(_),Succ(q)) => add(Succ(m),q)
    case (_,Zero)          => m
    case (Zero,_)          => n
    case (_,Err)           => Err        
    case (Err,_)           => Err
    }

  def sub(m:Nat,n:Nat): Nat = (m,n) match {
    case (Succ(p),Succ(q)) => sub(p,q)
    case (_,Zero)          => m
    case (Zero,_)          => Err
    case (_,Err)           => Err
    case (Err,_)           => Err
  }

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

  def toInt(n:Nat): Int = n match {
    case Succ(p) => 1 + toInt(p)
    case Zero    => 0
    case Err     => -1
  }
}

import Nat._

object TestCaseExtNats {

  // 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     ==> ${add(Zero,Zero)}")
    println(s"Zero + three    ==> ${add(Zero,three)}")
    println(s"Zero + Err      ==> ${add(Zero,Err)}")

    println(s"Zero - Zero     ==> ${sub(Zero,Zero)}")
    println(s"Zero - three    ==> ${sub(Zero,three)}")
    println(s"Zero - Err      ==> ${sub(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"pred(Zero)      ==> ${pred(Zero)}")
    println(s"toInt(Zero)     ==> ${toInt(Zero)}")


    // Test Succ methods

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

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

    println(s"three - Zero    ==> ${sub(three,Zero)}")
    println(s"three - three   ==> ${sub(three,three)}")
    println(s"three - six     ==> ${sub(three,six)}")
    println(s"three - Err     ==> ${sub(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"pred(three)     ==> ${pred(three)}")
    println(s"three.toInt     ==> ${toInt(three)}")


    // Test Err methods

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

    println(s"Err - Zero      ==> ${sub(Err,Zero)}")
    println(s"Err - three     ==> ${sub(Err,three)}")
    println(s"Err - Err       ==> ${sub(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"pred(Err)       ==> ${pred(Err)}")
    println(s"toInt(Err)      ==> ${toInt(Err)}")

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