object Lambda {

  def main(args: Array[String]): Unit = {
    // λ. 0 0
    val omega = Abstraction(Application(Variable(0), Variable(0)))
    //(λ. λ. 1 1) ((λ. (0 0)) (λ. (0 0)))
    val test = Application(
      Application(Abstraction(Abstraction(Variable(1))), Variable(1)),
      Application(omega, omega)
    )
    println(test)
    println("Normale Reduktion: " + test.evalNormal)
    //Applikative Reduktion führt hier zu einem Endlosloop
  }

  sealed trait LambdaTerm {

    /**
      * Prüft ob der Term eine Normalform ist
      */
    def isNormal: Boolean

    /**
      * Substituiert alle Vorkommen von der Variable index mit der gegebenen Substitution
      */
    def substitute(index: Int, substitution: LambdaTerm): LambdaTerm

    /**
      * Führt einen Reduktionsschritt nach der normalen Auswertungsstrategie durch
      */
    def reduceNormal: LambdaTerm

    /**
      * Führt einen Reduktionsschritt nach der applikativen Auswertungsstrategie durch
      */
    def reduceApplicative: LambdaTerm

    /**
      * Reduziert einen Term zu einer Normalform mittels der normalen Auswertungsstrategie
      */
    def evalNormal: LambdaTerm = ??? //TODO:

    /**
      * Reduziert einen Term zu einer Normalform mittels der applikativen Auswertungsstrategie
      */
    def evalApplicative: LambdaTerm = ??? //TODO:
  }

  case class Variable(index: Int) extends LambdaTerm {
    override def isNormal: Boolean = ??? //TODO:

    override def substitute(index: Int, substitution: LambdaTerm): LambdaTerm = ??? //TODO:

    override def reduceNormal: LambdaTerm = ??? //TODO:

    override def reduceApplicative: LambdaTerm = ??? //TODO:

    override def toString: String = index.toString
  }

  case class Application(left: LambdaTerm, right: LambdaTerm) extends LambdaTerm {
    override def isNormal: Boolean = ??? //TODO:

    override def reduceNormal: LambdaTerm = ??? //TODO:

    override def reduceApplicative: LambdaTerm = ??? //TODO:

    override def substitute(index: Int, substitution: LambdaTerm): LambdaTerm = ??? //TODO:

    override def toString: String = s"($left $right)"
  }

  case class Abstraction(term: LambdaTerm) extends LambdaTerm {
    override def isNormal: Boolean = ??? //TODO:

    override def reduceNormal: LambdaTerm = ??? //TODO:

    override def reduceApplicative: LambdaTerm = ??? //TODO:

    override def substitute(index: Int, substitution: LambdaTerm): LambdaTerm = ??? //TODO:

    /**
     * Führt einen Beta Reduktionsschritt durch, bei dem die an diesem Term gebundene Variable
     * durch den gegebenen Term ersetzt wird.
     */
    def beta(substituteTerm: LambdaTerm): LambdaTerm = ??? //TODO:

    override def toString: String = s"(λ. $term)"
  }
}