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 24b2ca5..ae4a100 100644 --- a/klogic-core/src/main/kotlin/org/klogic/core/Goal.kt +++ b/klogic-core/src/main/kotlin/org/klogic/core/Goal.kt @@ -55,11 +55,11 @@ fun delay(f: () -> Goal): Goal = { st: State -> ThunkStream { f()(st) } } */ fun > debugVar( term: Term, - reifier: (Term) -> ReifiedTerm, - callBack: (ReifiedTerm) -> Goal + reifier: (Term, Set>) -> 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 new file mode 100644 index 0000000..4dfd09c --- /dev/null +++ b/klogic-core/src/test/kotlin/org/klogic/core/ReifyTest.kt @@ -0,0 +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>> = mutableMapOf() + + @AfterEach + fun clearDebug() { + debugValues.clear() + } + + @Test + fun testDebugVar() { + val left = (-1).createTypedVar() + 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 }) + } + + private fun plus(x: Term, y: Term, z: Term): Goal = conde( + (x `===` Z) and (z `===` y), + freshTypedVars { a, 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) + } + ) + } + ) + } + ) +}