Skip to content

Commit

Permalink
Rewritten debugVar with a custom reifier
Browse files Browse the repository at this point in the history
  • Loading branch information
Yury Kamenev committed Apr 3, 2023
1 parent 1768656 commit e640074
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 3 deletions.
6 changes: 3 additions & 3 deletions klogic-core/src/main/kotlin/org/klogic/core/Goal.kt
Original file line number Diff line number Diff line change
Expand Up @@ -53,10 +53,10 @@ 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>> debugVar(
fun <T : Term<T>, Reified : ReifiedTerm<*>> debugVar(
term: Term<T>,
reifier: (Term<T>) -> ReifiedTerm<T>,
callBack: (ReifiedTerm<T>) -> Goal
reifier: (Term<T>) -> Reified,
callBack: (Reified) -> Goal
): Goal = { st: State ->
val walkedTerm = term.walk(st.substitution)
val reified = reifier(walkedTerm)
Expand Down
21 changes: 21 additions & 0 deletions klogic-core/src/test/kotlin/org/klogic/core/ReifyTest.kt
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
package org.klogic.core

import org.junit.jupiter.api.Test
import org.klogic.utils.terms.PeanoLogicNumber
import org.klogic.utils.terms.PeanoLogicNumber.Companion.succ
import org.klogic.utils.terms.ZeroNaturalNumber.Z

class ReifyTest {
@Test
fun testDebugVar() {
// TODO test plus here.
}

// 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)
}
)
}

0 comments on commit e640074

Please sign in to comment.