import org.scalatest._
import LambdaEvaluator._

object RenameAvoidingTest {   
  def main(args : Array[String]) {

    val test = new FunSuite {
      val x = Var("x")
      val expr1 = Lambda("x", x)

      def lambdas(expr: Expr) : Int = expr match {
        case Var(n) => 0
        case Lambda(_, b) => 1 + lambdas(b)
        case Apply(f, a) => lambdas(f) + lambdas(a)
      }

      def canonicalRename(expr: Expr, start : Int, renames : Map[String, Var]) : Expr = expr match {
        case Var(n) => if (renames contains n) renames(n) else expr
        case Lambda(x, b) => { 
          val name = "_" + start
          Lambda(name, canonicalRename(b, start + 1, renames + (x -> Var(name))))   
        } 
        case Apply(f, a) => Apply(canonicalRename(f, start, renames), canonicalRename(a, start + lambdas(f), renames))
      }
      
      def canonicalRename(expr : Expr) : Expr = canonicalRename(expr, 0, Map())
           
      test("Rename variable in simple Lambda") {
        val result = renameAvoiding(expr1, List("x")) 
        info("" + result)
        assert(result != expr1)
        assert(canonicalRename(result) === canonicalRename(expr1))
      }      
    }   
    
    test.execute()
  }
}