class BoolExpTest extends junit.framework.TestCase {
  
  /* import the JUnit test framework */
  import java.io._
  import junit.framework._
  import junit.framework.Assert._
 
  /* import the members of the object BoolExp */
  import BoolExp._

  /* This implicit conversions slighly simplify the notation for some conditional
   * exprssions.  Such expressions often contain the boolean constants Val(true) or 
   * Val(false), which are more conveniently written as simple true or false. */
  implicit def bool2Val(bool : Boolean) = Val(bool)

  /* This def overloads eval with 1 arg for convenience */
  def eval(exp : NormExp) = BoolExp.eval(exp, Map.empty)

  /* This method composes the methods defined in BoolExp to create a simplifier that reduces BoolExp 
   * => IfExp => NormExp => BoolExp. */
  def rawReduce(exp : BoolExp) = convertToBool(eval(normalize(convertToIf(exp))))

  /* Constants used in tests */
  val v = Var("v")
  val w = Var("w")
  val x = Var("x")
  val y = Var("y")
  val z = Var("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 nif5 = NIf(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 = NIf(x, NIf(y, NIf(y, z, false), true), NIf(true, NIf(y, z, false), true))
  val enif8 = NIf(x, NIf(y, z, true), NIf(y, z, false))
  val if9 = IIf(if8, x, y)
  val nif9 = NIf(x, NIf(y, NIf(y, NIf(z, x, y), NIf(false, x, y)), NIf(true, x, y)),
               NIf(true, NIf(y, NIf(z, x, y), NIf(false, x, y)), NIf(true, x, y)))
  val enif9 = NIf(x, true, NIf(y, NIf(z, false, true), false))
  val nif10 = NIf(x, y, y)
  val enif10 = y
  val nif11 = NIf(x, true, false)
  val enif11 = x

  def testBoolExp() {
    // Tests
//    println(">> Basic Tests")
    assertEquals("Variable x not equals Variable y", true, x != y)
    assertEquals("Variable equals", Var("x"), Var("x"))
    assertEquals("And equals", f1, And(x, y))
    assertEquals("Or equals", f2, Or(x, y))
    assertEquals("Implies equals", f3, Implies(x, y))
    assertEquals("Not equals", f4, Not(z))
    assertEquals("If equals", f5, If(x, y, z))
    println(">> If-Conversion Tests")
    assertEquals("Variable Conversion", x, convertToIf(x));
    assertEquals("And Conversion", if1, convertToIf(f1));
    assertEquals("Or Conversion", if2, convertToIf(f2));
    assertEquals("Implies Conversion", if3, convertToIf(f3));
    assertEquals("Not Conversion", if4, convertToIf(f4));
    assertEquals("If Conversion", if5, convertToIf(f5));
    assertEquals("Compound Or Conversion", if6, convertToIf(f6));
    assertEquals("Compound And Conversion", if7, convertToIf(f7));
    assertEquals("Compound Implies Conversion", if8, convertToIf(f8));
    println(">> Normalization Tests")
    assertEquals("Normalize Variable", x, normalize(x))
    assertEquals("Normalize true", True, normalize(true))
    assertEquals("Normalize false", False, normalize(false))
    assertEquals("Normalize Trivial If", nif5, normalize(if5))
    assertEquals("One-step Normalize", nif8, normalize(if8))
    assertEquals("Nested Normalize", nif9, normalize(if9))
    println(">> Symbolic Evaluation Tests")
    assertEquals("Eval Variable", x, eval(x))
//    assertEquals("Eval If Sub", NIf(x, y, NIf(y, false, z)), eval(IIf(x, IIf(x, y, z), IIf(y, x, z))))
    assertEquals("Eval Trivial If", nif5, eval(nif5))
    assertEquals("Eval nif8", enif8, eval(nif8))
    assertEquals("Eval nif9", enif9, eval(nif9))
    assertEquals("Check (? x alpha alpha) => alpha", enif10, eval(nif10))
    assertEquals("Check (? x T F) => x", enif11, eval(nif11))
    println(">> Convert To Bool Tests")
    assertEquals("Convert True", Val(true), convertToBool(true))
    assertEquals("Convert False", Val(false), convertToBool(false))
    assertEquals("Convert Not", Not(x), convertToBool(NIf(x, false, true)))
    assertEquals("Convert And", And(x, y), convertToBool(NIf(x, y, false)))
    assertEquals("Convert Or", Or(x, y), convertToBool(NIf(x, true, y)))
    assertEquals("Convert Implies", Implies(x, y), convertToBool(NIf(x, y, true)))
    assertEquals("Convert If", If(x, y, z), convertToBool(NIf(x, y, z)))
    assertEquals("Convert Compound", And(v, If(w, x, Or(y, z))),
      convertToBool(NIf(v, NIf(w, x, NIf(y, true, z)), false)))
    println(">> Full Tests")
    assertEquals("Full 1", Val(true),
      rawReduce(Or(And(x, y), Or(And(x, Not(y)), Or(And(Not(x), y), And(Not(x), Not(y)))))))
    val computedValue: BoolExp = rawReduce(Or(And(x, Not(y)), Or(And(Not(x), y), And(Not(x), Not(y)))))
    assertEquals("Full 2", Implies(x, Not(y)), computedValue)
    assertEquals("littleData1 exists", true, new File("littleData1.txt").isFile())
    assertEquals("littleData1", "T", new Parser(new File("littleData1.txt")).reduce)
  }
}