// ! The 'App' trait is the new version of 'Application'
// ! (The 'Application' trait is deprecated in Scala 2.9)
object BoolExpTest extends App {

//  import BoolExp._ // Make members of BoolExp immediately available
  import BoolExp._
  import java.io._
  
  /** Check if expected result and actual result match */
  def checkEq[T](desc : String, expected : T, actual : T) {
    if (actual != expected) {
      println("\tTEST FAILED: " + desc);
      println("\t  Found:    " + actual);
      println("\t  Expected: " + expected);
      System.exit(-1)
    } else println("\tTest Passed: " + desc)
  }

  // Implicit conversions used for easier building of test cases
  // ! Since some variable "x" could be a Var or an IVar depending
  // ! on context, and likewise a boolean could be a Val or an IVal,
  // ! it's easier to use these implicit conversions when building tests.
  implicit def bool2Val(bool : Boolean) = Val(bool)
  implicit def bool2IVal(bool : Boolean) = IVal(bool)
  implicit def sym2Var(sym : Symbol) = Var(sym.name)
  implicit def sym2IVar(sym : Symbol) = IVar(sym.name)

  // Overloaded eval with 1 arg for convenience
  def eval(exp : IfExp) = BoolExp.eval(exp, Map.empty)

  // Convenience method for full BoolExp => IfExp => BoolExp conversion
  def rawReduce(exp : BoolExp) = convertToBool(eval(normalize(convertToIf(exp))))

  // Convenience declarations for tests
  val v = 'v
  val w = 'w
  val x = 'x
  val y = 'y
  val z = 'z
  val f1 = And(x,y)
  val if1 = IIf(x, y, false)
  val f2 = Or(x,y)
  val if2 = IIf(x, true, y)
  val f3 = Implies(x,y)
  val if3 = IIf(x, y, true)
  val f4 = Not(z)
  val if4 = IIf(z, false, true)
  val f5 = If(x, y, z)
  val if5 = IIf(x, y, z)
  val f6 = Or(And(x,y), Or(y,z))
  val if6 = IIf(IIf(x, y, false), true, IIf(y, true, z))
  val f7 = And(Or(x,y), And(y,z))
  val if7 = IIf(IIf(x, true, y), IIf(y, z, false), false)
  val f8 = Implies(Implies(x,y), And(y,z))
  val if8 = IIf(IIf(x, y, true), IIf(y, z, false), true)
  val nif8 = IIf(x, IIf(y, IIf(y, z, false), true), IIf(true, IIf(y, z, false), true))
  val enif8 = IIf(x, IIf(y, z, true), IIf(y, z, false))
  val if9 = IIf(if8, x, y)
  val nif9 = IIf(x, IIf(y, IIf(y, IIf(z, x, y), IIf(false, x, y)), IIf(true, x, y)),
               IIf(true, IIf(y, IIf(z, x, y), IIf(false, x, y)), IIf(true, x, y)))
  val enif9 = IIf(x, true, IIf(y, IIf(z, false, true), false))
  val nif10 = IIf(x, y, y)
  val enif10 = y
  val nif11 = IIf(x, true, false)
  val enif11 = x
  
  // Tests
  println(">> Basic Tests")
  checkEq[Boolean]("Variable x not equals Variable y", true, x != y)
  checkEq[BoolExp]("Variable equals", x, Var("x"))
  checkEq[BoolExp]("And equals", f1, And(x,y))
  checkEq[BoolExp]("Or equals", f2, Or(x,y))
  checkEq[BoolExp]("Implies equals", f3, Implies(x,y))
  checkEq[BoolExp]("Not equals", f4, Not(z))
  checkEq[BoolExp]("If equals", f5, If(x, y, z))
  println(">> If-Conversion Tests")
  checkEq[IfExp]("Variable Conversion", x, convertToIf(x));
  checkEq[IfExp]("And Conversion", if1, convertToIf(f1));
  checkEq[IfExp]("Or Conversion", if2, convertToIf(f2));
  checkEq[IfExp]("Implies Conversion", if3, convertToIf(f3));
  checkEq[IfExp]("Not Conversion", if4, convertToIf(f4));
  checkEq[IfExp]("If Conversion", if5, convertToIf(f5));
  checkEq[IfExp]("Compound Or Conversion", if6, convertToIf(f6));
  checkEq[IfExp]("Compound And Conversion", if7, convertToIf(f7));
  checkEq[IfExp]("Compound Implies Conversion", if8, convertToIf(f8));
  println(">> Normalization Tests")
  checkEq[IfExp]("Normalize Variable", x, normalize(x))
  checkEq[IfExp]("Normalize true", true, normalize(true))
  checkEq[IfExp]("Normalize false", false, normalize(false))
  checkEq[IfExp]("Normalize Trivial If", if5, normalize(if5))
  checkEq[IfExp]("One-step Normalize", nif8, normalize(if8))
  checkEq[IfExp]("Nested Normalize", nif9, normalize(if9))
  println(">> Symbolic Evaluation Tests")
  checkEq[IfExp]("Eval Variable", x, eval(x))
  checkEq[IfExp]("Eval If Sub", IIf(x, y, IIf(y, false, z)), eval(IIf(x, IIf(x, y, z), IIf(y, x, z))))
  checkEq[IfExp]("Eval Trivial If", if5, eval(if5))
  checkEq[IfExp]("Eval nif8", enif8, eval(nif8))
  checkEq[IfExp]("Eval nif9", enif9, eval(nif9))
  checkEq[IfExp]("Check (? x alpha alpha) => alpha", enif10, eval(nif10))
  checkEq[IfExp]("Check (? x T F) => x", enif11, eval(nif11)) 
  println(">> Convert To Bool Tests")
  checkEq[BoolExp]("Convert True", true, convertToBool(true))
  checkEq[BoolExp]("Convert False", false, convertToBool(false))
  checkEq[BoolExp]("Convert Not", Not(x), convertToBool(IIf(x, false, true)))
  checkEq[BoolExp]("Convert And", And(x, y), convertToBool(IIf(x, y, false)))
  checkEq[BoolExp]("Convert Or", Or(x, y), convertToBool(IIf(x, true, y)))
  checkEq[BoolExp]("Convert Implies", Implies(x, y), convertToBool(IIf(x, y, true)))
  checkEq[BoolExp]("Convert If", If(x, y, z), convertToBool(IIf(x, y, z)))
  checkEq[BoolExp]("Convert Compound", And(v, If(w, x, Or(y, z))),
    convertToBool(IIf(v, IIf(w, x, IIf(y, true, z)), false)))
  println(">> Full Tests")
  checkEq[BoolExp]("Full 1", true,
    rawReduce(Or(And(x, y), Or(And(x, Not(y)), Or(And(Not(x), y), And(Not(x), Not(y)))))))
  checkEq[BoolExp]("Full 2", Implies(x, Not(y)),
    rawReduce(Or(And(x, Not(y)), Or(And(Not(x), y), And(Not(x), Not(y))))))
  /* Test that confirms the file "bigData0.txt" is located in the project directory. */
//  checkEq[Boolean]("bigData0 exists", true, new File("bigData0.txt").isFile())
  /* Test that reduce correctly processes the Boolean expression in file "bigData0.txt" */
//  checkEq[String]("bigData0 runs", "T", new Parser(new File("bigData0.txt")).reduce)
}