package scala.examples.tcpoly.calculi.lambda.simplified 

// the top-level classes are components, 
// in `class C { x: T => ... }`, the type (T) of the self variable (x) denotes C's required components
// see Odersky et al., Scalable Component Abstractions
// to avoid this "complexity" (uhm, modularity), you can just make all classes top-level
trait Syntax { self: Syntax with Binding  =>
  trait Term extends Nominal[Term] {
    def isValue: Boolean
  }

  case class Var(name: Name) extends Term {
    def isValue = false

    def swap(a: Name, b: Name) = Var(name swap(a, b))
    def fresh(a: Name) = name fresh(a)
    def alphaEq(o: AlsoNominal[Term]) = o match {
      case Var(n) => n.alphaEq(name)
      case _ => false
    }
  }

  case class Abs(abs: \\[Term]) extends Term {
    def isValue = true

    def swap(a: Name, b: Name) =  Abs(abs swap(a, b))
    def fresh(a: Name) = abs fresh(a)
    def alphaEq(o: AlsoNominal[Term]) = o match {
      case Abs(a) => a.alphaEq(abs)
      case _ => false
    }    
  }

  case class App(fun: Term, arg: Term) extends Term {
    def isValue = false

    def swap(a: Name, b: Name) = App(fun swap(a, b), arg  swap(a, b))
    def fresh(a: Name) = fun.fresh(a) && arg.fresh(a)
    def alphaEq(o: AlsoNominal[Term]) = o match {
      case App(f, a) => f.alphaEq(fun) && a.alphaEq(arg)
      case _ => false
    }    
  }

  class Literal extends Term { 
    def isValue = true 
    def swap(a: Name, b: Name) = this
    def fresh(a: Name) = true    
    def alphaEq(o: AlsoNominal[Term]) = o == this
  }
  case object t extends Literal
  case object f extends Literal
}

trait Binding { self: Binding => 
  type AlsoNominal[T] = T with Nominal[T] // avoid F-bounds
  trait Nominal[Self] { // something that contains names
    // return this entity after swapping a and b
    def swap(a: Name, b: Name): AlsoNominal[Self]

    // a is in the set of free variables of this entity
    def fresh(a: Name): Boolean
    
    def alphaEq(other: AlsoNominal[Self]): Boolean
  }
  
  object Name {
    private[Name] var nextTag: Int = -1 // only for toString
    def apply(name: String) = new Name(name)
    def apply(name: Name) = new Name(name.name)
  }
  class Name(val name: String) extends Nominal[Name] {
    def swap(a: Name, b: Name) : AlsoNominal[Name]
      = if(this.alphaEq(a)) b else if(this.alphaEq(b)) a else this

    def fresh(a: Name) = ! this.alphaEq(a)  

    def alphaEq(other: AlsoNominal[Name]) = other eq this // identity

    override def toString() = name+"$"+tag
    val tag = {Name.nextTag += 1; Name.nextTag} // only used in toString
  }
  
  case class \\[T](private val binder: Name,
              private val body: AlsoNominal[T]) extends Nominal[\\[T]] {

    def swap(a: Name, b: Name) 
      = new \\(binder swap(a, b), body swap(a, b))

    def fresh(a: Name) 
      = if(a.alphaEq(binder)) true  // implicitly alpha-convert binder
        else body.fresh(a)

    def alphaEq(o: AlsoNominal[\\[T]]): Boolean = (binder.alphaEq(o.binder) && body.alphaEq(o.body)) || 
        ((!binder.alphaEq(o.binder)) && 
         o.body.fresh(binder) && o.body.swap(o.binder, binder).alphaEq(body))

    def unabs: (Name, AlsoNominal[T]) = {
      val freshBinder = new Name(binder.name)    // Name(binder.name) would work too, this calls Name.apply(binder.name) (see object Name)
      (freshBinder, body.swap(binder, freshBinder))
    }
    
    override def toString() = {
      val (x, b) = unabs
      x+" \\ "+b
    }
    
  }  
}

trait Substitution { s: Syntax with Binding with Substitution =>
  def subst(self: Term, n: Name, to: Term): Term = self match{
    case Var(name) => if(name.alphaEq(n)) to else self
    case App(fun, arg) => App(subst(fun, n, to), 
                            subst(arg, n, to))
    case Abs(a) =>
      val (x, body) = a.unabs
      Abs(new \\(x, subst(body, n, to)))
    case _ : Literal => self
  }
}

trait Evaluation { self: Syntax with Substitution with Binding with Evaluation =>
  def eval(tm: Term): Term = tm match {
    case App(Abs(a), v) if v.isValue => 
      val (x, t) = a.unabs
      subst(t, x, v)
    case App(v, t) if v.isValue => App(v, eval(t))
    case App(t1, t2) => App(eval(t1), t2)
  }
  
  // transitive closure
  def evalX(tm: Term): Term = tm match {
    case v if v.isValue => v
    case tm => evalX(eval(tm)) // TODO: check this is tail-recursive
  }
}

object EvalTest extends Syntax with Substitution with Binding with Evaluation with Application {
  val y = Name("y")
  val x = Name("x")
  val y2 = Name("y")
  
  // (\y. (\x. \y. x) y) t
  val a = App(Abs(\\(y, App(Abs(\\(x, Abs(\\(y2, Var(x))))), Var(y)))), t)
//  val a = ('y -> (('x -> ('x -> 'x)) ~ 'y)) ~ t
//  val a = ('y -> (('x -> ('x -> 'x)) ~ 'y)) ~ t
//  val b = ('y -> ('x -> ('y -> 'x)) ~ 'y) ~ t
  
  println(evalX(a))
//  println(evalX(b))  
}