From c4c203729f62958461237067354809fd8bbe5b2e Mon Sep 17 00:00:00 2001
From: Yury Kamenev <yurkam447@gmai.com>
Date: Mon, 3 Apr 2023 16:06:46 +0300
Subject: [PATCH] Refactoring

---
 .../src/main/kotlin/org/klogic/core/Goal.kt   |  8 ++--
 .../test/kotlin/org/klogic/core/ReifyTest.kt  | 45 +++++++++++++++++--
 2 files changed, 45 insertions(+), 8 deletions(-)

diff --git a/klogic-core/src/main/kotlin/org/klogic/core/Goal.kt b/klogic-core/src/main/kotlin/org/klogic/core/Goal.kt
index 6110827..ae4a100 100644
--- a/klogic-core/src/main/kotlin/org/klogic/core/Goal.kt
+++ b/klogic-core/src/main/kotlin/org/klogic/core/Goal.kt
@@ -53,13 +53,13 @@ fun delay(f: () -> Goal): Goal = { st: State -> ThunkStream { f()(st) } }
 /**
  * Reifies walked [term] using the passed [reifier] and returns a Goal from the passed [callBack].
  */
-fun <T : Term<T>, Reified : ReifiedTerm<*>> debugVar(
+fun <T : Term<T>> debugVar(
     term: Term<T>,
-    reifier: (Term<T>) -> Reified,
-    callBack: (Reified) -> Goal
+    reifier: (Term<T>, Set<Constraint<*>>) -> ReifiedTerm<*> = ::ReifiedTerm,
+    callBack: (ReifiedTerm<*>) -> Goal
 ): Goal = { st: State ->
     val walkedTerm = term.walk(st.substitution)
-    val reified = reifier(walkedTerm)
+    val reified = reifier(walkedTerm, st.constraints)
 
     callBack(reified)(st)
 }
diff --git a/klogic-core/src/test/kotlin/org/klogic/core/ReifyTest.kt b/klogic-core/src/test/kotlin/org/klogic/core/ReifyTest.kt
index f101d80..4dfd09c 100644
--- a/klogic-core/src/test/kotlin/org/klogic/core/ReifyTest.kt
+++ b/klogic-core/src/test/kotlin/org/klogic/core/ReifyTest.kt
@@ -1,21 +1,58 @@
 package org.klogic.core
 
+import org.junit.jupiter.api.AfterEach
 import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.klogic.core.Var.Companion.createTypedVar
 import org.klogic.utils.terms.PeanoLogicNumber
 import org.klogic.utils.terms.PeanoLogicNumber.Companion.succ
 import org.klogic.utils.terms.ZeroNaturalNumber.Z
+import org.klogic.utils.terms.toPeanoLogicNumber
 
 class ReifyTest {
+    private val debugValues: MutableMap<String, MutableList<ReifiedTerm<*>>> = mutableMapOf()
+
+    @AfterEach
+    fun clearDebug() {
+        debugValues.clear()
+    }
+
     @Test
     fun testDebugVar() {
-        // TODO test plus here.
+        val left = (-1).createTypedVar<PeanoLogicNumber>()
+        val right = 10.toPeanoLogicNumber()
+        val result = 13.toPeanoLogicNumber()
+
+        val run = run(10, left, plus(left, right, result))
+
+        assertEquals(3.toPeanoLogicNumber(), run.single().term)
+
+        debugValues["x"]!!.zip(debugValues["z"]!!).forEach {
+            println("x: ${it.first.term}, z: ${it.second.term}")
+        }
+
+        val expectedDebugValues = (13 downTo 1).map { it.toPeanoLogicNumber() }
+        assertEquals(expectedDebugValues, debugValues["z"]!!.map { it.term })
     }
 
-    // TODO rewrite using debugVar.
     private fun plus(x: Term<PeanoLogicNumber>, y: Term<PeanoLogicNumber>, z: Term<PeanoLogicNumber>): Goal = conde(
         (x `===` Z) and (z `===` y),
         freshTypedVars<PeanoLogicNumber, PeanoLogicNumber> { a, b ->
-            (x `===` succ(a)) and (z `===` succ(b)) and plus(a, y, b)
+            (x `===` succ(a)) and (z `===` succ(b)) and debugVar(
+                x,
+                callBack = { reifiedX ->
+                    debugValues.getOrPut("x") { mutableListOf() } += reifiedX
+
+                    debugVar(
+                        z,
+                        callBack = { reifiedZ ->
+                            debugValues.getOrPut("z") { mutableListOf() } += reifiedZ
+
+                            plus(a, y, b)
+                        }
+                    )
+                }
+            )
         }
     )
-}
\ No newline at end of file
+}