Make search for implication assumption recursive

src/main/scala/com/melvic/chi/ast/Proof.scala

@@ -18,5 +18,10 @@ object Proof {
   final case class Disjunction(name: String, left: (String, Proof), right: (String, Proof)) extends Proof
 
   final case class Abstraction(domain: Proof, codomain: Proof) extends Proof
-  final case class Application(functionName: String, params: List[Proof]) extends Proof
+
+  /**
+    * Function application. The first parameter is a proof by itself, rather than a function
+    * name as a string, in order to support invokations of curried functions (e.g `f(a)(b)`)
+    */
+  final case class Application(function: Proof, params: List[Proof]) extends Proof
 }

src/main/scala/com/melvic/chi/ast/Proposition.scala

@@ -3,6 +3,8 @@ package com.melvic.chi.ast
 import com.melvic.chi.out.Display
 import com.melvic.chi.parsers.Language
 
+import scala.annotation.tailrec
+
 sealed trait Proposition
 
 object Proposition {
@@ -60,4 +62,11 @@ object Proposition {
 
   def exists(proposition: Proposition)(f: Atom => Boolean): Boolean =
     filter(proposition)(f).nonEmpty
+
+  @tailrec
+  def rightMostOf(implication: Implication): Proposition =
+    implication match {
+      case Implication(_, consequent: Implication) => rightMostOf(consequent)
+      case Implication(_, consequent) => consequent
+    }
 }

src/main/scala/com/melvic/chi/env/Env.scala

@@ -25,7 +25,7 @@ object Env {
     env.proofs.filter(predicate.orElse(_ => false))
 
   def filterByConsequent(consequent: Proposition)(implicit env: Env): List[Proof] =
-    filter { case Variable(_, Implication(_, `consequent`)) => true }
+    filter { case Variable(_, impl: Implication) if Proposition.rightMostOf(impl) == consequent => true }
 
   def without(proof: Proof)(implicit env: Env): Env =
     fromList(env.proofs.filterNot(_ == proof))

src/main/scala/com/melvic/chi/eval/Evaluate.scala

@@ -1,6 +1,6 @@
 package com.melvic.chi.eval
 
-import com.melvic.chi.ast.Proof.{PLeft, PRight, TUnit, Variable}
+import com.melvic.chi.ast.Proof.{Application, PLeft, PRight, TUnit, Variable}
 import com.melvic.chi.ast.Proposition._
 import com.melvic.chi.ast.{Definition, Proof, Proposition, Signature}
 import com.melvic.chi.env.Env
@@ -59,12 +59,20 @@ object Evaluate {
     implicationOpt
       .toRight(Fault.cannotProve(atom))
       .flatMap {
-        case variable @ Variable(functionName, Implication(antecedent, _)) =>
+        case variable @ Variable(_, Implication(antecedent, consequent)) =>
           val newEnv = Env.without(variable)
-          Evaluate
-            .fromProposition(antecedent)(newEnv)
-            .map(Rule.implicationElimination(functionName, _))
-            .orElse(deduce(atom)(newEnv))
+
+          def recurse(function: Proof, in: Proposition, out: Proposition): Result[Proof] =
+            Evaluate.fromProposition(in)(newEnv)
+              .map(Rule.implicationElimination(function, _))
+              .flatMap { application =>
+                out match {
+                  case `atom` => Result.success(application)
+                  case Implication(newIn, newOut) => recurse(application, newIn, newOut)
+                }
+              }
+
+          recurse(variable, antecedent, consequent).orElse(deduce(atom)(newEnv))
       }
   }
 

src/main/scala/com/melvic/chi/eval/Rule.scala

@@ -68,11 +68,11 @@ object Rule {
     *     B
     * In programming, it means applying the function to the argument.
     */
-  def implicationElimination(functionName: String, argument: Proof): Proof =
+  def implicationElimination(function: Proof, argument: Proof): Proof =
     argument match {
-      case TUnit                    => Application(functionName, Nil)
-      case Proof.Conjunction(terms) => Application(functionName, terms)
-      case param                    => Application(functionName, List(param))
+      case TUnit                    => Application(function, Nil)
+      case Proof.Conjunction(terms) => Application(function, terms)
+      case param                    => Application(function, List(param))
     }
 
   /**

src/test/scala/com/melvic/chi/tests/ScalaDefSpec.scala

@@ -175,4 +175,15 @@ class ScalaDefSpec extends AnyFlatSpec with should.Matchers {
         |  }""".stripMargin
     )
   }
+
+  "search for implication assumption" should "be recursive" in {
+    generateAndShow("def foo[A, B, C]: (A => (B => C)) => ((A, B) => C)") should be(
+      """Detected language: Scala
+        |Generated code:
+        |def foo[A, B, C]: ((A => (B => C)) => ((A, B) => C)) =
+        |  f => { case (a, b) =>
+        |    f(a)(b)
+        |  }""".stripMargin
+    )
+  }
 }