Skip to content

Commit

Permalink
Introduced template terms, refactored some signatures of public API (#9)
Browse files Browse the repository at this point in the history
  • Loading branch information
Damtev authored Mar 21, 2023
1 parent 3a6732e commit 1768656
Show file tree
Hide file tree
Showing 15 changed files with 106 additions and 96 deletions.
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/org.klogic.klogic-base.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ plugins {
}

group = "org.klogic"
version = "0.1.2"
version = "0.1.3"

repositories {
mavenCentral()
Expand Down
24 changes: 6 additions & 18 deletions klogic-core/src/main/kotlin/org/klogic/core/Goal.kt
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package org.klogic.core

import org.klogic.core.RecursiveStream.Companion.nil
import org.klogic.core.RecursiveStream.Companion.nilStream
import org.klogic.core.RecursiveStream.Companion.single

typealias Goal = (State) -> RecursiveStream<State>
Expand All @@ -19,20 +19,14 @@ val success: Goal = { st: State -> single(st) }
/**
* Represents a [Goal] that always fails.
*/
val failure: Goal = { _: State -> nil() }
val failure: Goal = { _: State -> nilStream() }

/**
* Calculates g1 ||| (g2 ||| (g3 ||| ... gn)) for a non-empty list of goals.
* Calculates g1 ||| (g2 ||| (g3 ||| ... gn)) for a sequence of goals.
*
* NOTE: right association!
*/
fun conde(vararg goals: Goal): Goal {
require(goals.isNotEmpty()) {
"Expected at least one goal for conde but got 0"
}

return goals.reduceRight(Goal::or)
}
fun conde(goal: Goal, vararg goals: Goal): Goal = goal or goals.reduceRight(Goal::or)

/**
* Invokes [this] [Goal]. If it succeeds, returns a [RecursiveStream] with its result.
Expand All @@ -45,17 +39,11 @@ infix fun Goal.condo2(second: Goal): Goal = { st: State ->
}

/**
* Calculates g1 &&& (g2 &&& (g3 &&& ... gn)) for a non-empty list of goals.
* Calculates g1 &&& (g2 &&& (g3 &&& ... gn)) for a sequence of goals.
*
* NOTE: right association!
*/
fun and(vararg goals: Goal): Goal {
require(goals.isNotEmpty()) {
"Expected at least one goal for `and` but got 0"
}

return goals.reduceRight(Goal::and)
}
fun and(goal: Goal, vararg goals: Goal): Goal = goal and goals.reduceRight(Goal::and)

/**
* Creates a lazy [Goal] by passed goal generator [f].
Expand Down
7 changes: 4 additions & 3 deletions klogic-core/src/main/kotlin/org/klogic/core/Stream.kt
Original file line number Diff line number Diff line change
Expand Up @@ -53,14 +53,15 @@ sealed class RecursiveStream<out T> {
operator fun plus(head: @UnsafeVariance T): RecursiveStream<T> = ConsStream(head, this)

companion object {
fun <T> nil(): RecursiveStream<T> = NilStream
fun <T> nilStream(): RecursiveStream<T> = NilStream
fun <T> emptyStream(): RecursiveStream<T> = nilStream()

fun <T> of(vararg elements: T): RecursiveStream<T> {
fun <T> streamOf(vararg elements: T): RecursiveStream<T> {
if (elements.isEmpty()) {
return NilStream
}

return elements.fold(nil()) { acc, e ->
return elements.fold(nilStream()) { acc, e ->
ConsStream(e, acc)
}
}
Expand Down
10 changes: 5 additions & 5 deletions klogic-core/src/main/kotlin/org/klogic/core/Term.kt
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
package org.klogic.core

import org.klogic.core.RecursiveStream.Companion.nil
import org.klogic.core.RecursiveStream.Companion.nilStream
import org.klogic.core.RecursiveStream.Companion.single
import org.klogic.unify.UnificationState

Expand Down Expand Up @@ -35,14 +35,14 @@ sealed interface Term<T : Term<T>> {
/**
* Tries to unify this term to [other] term of the same type.
* If succeeds, returns a [Goal] with [RecursiveStream] containing single [State] with a corresponding [Substitution],
* and a goal with the [nil] stream otherwise.
* and a goal with the [nilStream] stream otherwise.
*
* @see [State.unifyWithConstraintsVerification] for details.
*/
infix fun unify(other: Term<T>): Goal = { st: State ->
st.unifyWithConstraintsVerification(this, other)?.let {
single(it)
} ?: nil()
} ?: nilStream()
}

/**
Expand All @@ -57,7 +57,7 @@ sealed interface Term<T : Term<T>> {
infix fun ineq(other: Term<T>): Goal = { st: State ->
st.substitution.ineq(this, other).let {
when (it) {
ViolatedConstraintResult -> nil()
ViolatedConstraintResult -> nilStream()
RedundantConstraintResult -> single(st)
is SatisfiableConstraintResult -> {
val newConstraint = it.simplifiedConstraint
Expand Down Expand Up @@ -200,5 +200,5 @@ interface CustomTerm<T : CustomTerm<T>> : Term<T> {
* Checks whether this term can be unified with [other] term. For example, different branches of the same sealed term
* often cannot be unified - for instance, a not empty list cannot be unified with an empty list.
*/
infix fun isUnifiableWith(other: CustomTerm<T>): Boolean = true
infix fun isUnifiableWith(other: CustomTerm<T>): Boolean = javaClass == other.javaClass
}
Original file line number Diff line number Diff line change
Expand Up @@ -3,12 +3,12 @@ package org.klogic.core.streams
import org.junit.jupiter.api.Assertions.assertEquals
import org.junit.jupiter.api.Test
import org.klogic.core.ConsStream
import org.klogic.core.RecursiveStream.Companion.nil
import org.klogic.core.RecursiveStream.Companion.nilStream

class BindTest {
@Test
fun testBind() {
val simpleBind = ones().bind { ConsStream(2, ConsStream(3, nil())) }
val simpleBind = ones().bind { ConsStream(2, ConsStream(3, nilStream())) }
val firstTen = simpleBind.take(10)

val expected = listOf(2, 2, 3, 2, 3, 2, 3, 2, 3, 2)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ import org.klogic.core.reify
import org.klogic.core.run
import org.klogic.core.unreifiedRun
import org.klogic.core.`|||`
import org.klogic.utils.terms.Cons.Companion.logicListOf
import org.klogic.utils.terms.LogicList.Companion.logicListOf
import org.klogic.utils.terms.LogicList
import org.klogic.utils.terms.Nil.nilLogicList
import org.klogic.utils.terms.Symbol
Expand Down
15 changes: 1 addition & 14 deletions klogic-utils/src/main/kotlin/org/klogic/utils/terms/LogicBool.kt
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,14 @@

package org.klogic.utils.terms

import org.klogic.core.CustomTerm
import org.klogic.core.Goal
import org.klogic.core.Term
import org.klogic.core.and
import org.klogic.core.conde
import org.klogic.utils.terms.LogicFalsᴼ.falsᴼ
import org.klogic.utils.terms.LogicTruᴼ.truᴼ

sealed class LogicBool : CustomTerm<LogicBool> {
sealed class LogicBool : EmptyTerm<LogicBool>() {
abstract fun toBool(): Boolean

override fun toString(): String = toBool().toString()
Expand All @@ -23,24 +22,12 @@ sealed class LogicBool : CustomTerm<LogicBool> {
object LogicFalsᴼ : LogicBool() {
val falsᴼ: LogicFals= this

override val subtreesToUnify: Sequence<*> = emptySequence<Any?>()

override fun constructFromSubtrees(subtrees: Iterable<*>): CustomTerm<LogicBool> = this

override fun isUnifiableWith(other: CustomTerm<LogicBool>): Boolean = other is LogicFals

override fun toBool(): Boolean = false
}

object LogicTruᴼ : LogicBool() {
val truᴼ: LogicTru= this

override val subtreesToUnify: Sequence<*> = emptySequence<Any?>()

override fun constructFromSubtrees(subtrees: Iterable<*>): CustomTerm<LogicBool> = this

override fun isUnifiableWith(other: CustomTerm<LogicBool>): Boolean = other is LogicTru

override fun toBool(): Boolean = true
}

Expand Down
33 changes: 14 additions & 19 deletions klogic-utils/src/main/kotlin/org/klogic/utils/terms/LogicList.kt
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,20 @@ sealed class LogicList<T : Term<T>> : CustomTerm<LogicList<T>> {
abstract fun isEmpty(): Boolean
abstract operator fun get(index: Int): Term<T>
abstract fun toList(): List<Term<T>>


companion object {
/**
* Constructs [LogicList] of the specified type from passed [terms].
*/
fun <T : Term<T>> logicListOf(vararg terms: Term<T>): LogicList<T> {
if (terms.isEmpty()) {
return nilLogicList()
}

return Cons(terms.first(), logicListOf(*terms.drop(1).toTypedArray()))
}
}
}

/**
Expand All @@ -39,9 +53,6 @@ object Nil : LogicList<Nothing>() {

override fun constructFromSubtrees(subtrees: Iterable<*>): CustomTerm<LogicList<Nothing>> = this

// Nil cannot be unified with a not empty list
override fun isUnifiableWith(other: CustomTerm<LogicList<Nothing>>): Boolean = other is Nil

override fun get(index: Int): Nothing = throw IndexOutOfBoundsException("This list is empty")

override fun toList(): List<Term<Nothing>> = emptyList()
Expand Down Expand Up @@ -75,9 +86,6 @@ data class Cons<T : Term<T>>(val head: Term<T>, val tail: Term<LogicList<T>>) :
return Cons(head as Term<T>, tail as Term<LogicList<T>>)
}

// A not empty list cannot be unified with an empty list
override fun isUnifiableWith(other: CustomTerm<LogicList<T>>): Boolean = other is Cons

@Suppress("UNCHECKED_CAST")
override fun get(index: Int): Term<T> {
require(index >= 0) {
Expand Down Expand Up @@ -117,19 +125,6 @@ data class Cons<T : Term<T>>(val head: Term<T>, val tail: Term<LogicList<T>>) :

return mapToString().joinToString(", ", prefix = "(", postfix = ")")
}

companion object {
/**
* Constructs [LogicList] of the specified type from passed [terms].
*/
fun <T : Term<T>> logicListOf(vararg terms: Term<T>): LogicList<T> {
if (terms.isEmpty()) {
return nilLogicList()
}

return Cons(terms.first(), logicListOf(*terms.drop(1).toTypedArray()))
}
}
}

/**
Expand Down
22 changes: 5 additions & 17 deletions klogic-utils/src/main/kotlin/org/klogic/utils/terms/LogicPair.kt
Original file line number Diff line number Diff line change
@@ -1,27 +1,15 @@
package org.klogic.utils.terms

import org.klogic.core.CustomTerm
import org.klogic.core.Term

/**
* Represents a logic type for simple [Pair].
*/
data class LogicPair<A : Term<A>, B : Term<B>>(val first: Term<A>, val second: Term<B>) : CustomTerm<LogicPair<A, B>> {
override val subtreesToUnify: Sequence<*> = sequenceOf(first, second)

override fun constructFromSubtrees(subtrees: Iterable<*>): CustomTerm<LogicPair<A, B>> {
// We use by-hand iteration here to avoid losing performance.
val iterator = subtrees.iterator()
val first = iterator.next()
val second = iterator.next()

require(!iterator.hasNext()) {
"Expected only 2 elements for constructing LogicPair but got more elements"
}

@Suppress("UNCHECKED_CAST")
return LogicPair(first as Term<A>, second as Term<B>)
}
data class LogicPair<A : Term<A>, B : Term<B>>(
override val first: Term<A>,
override val second: Term<B>
) : BinaryTerm<LogicPair<A, B>, Term<A>, Term<B>>() {
override val constructor: (Term<A>, Term<B>) -> LogicPair<A, B> = ::LogicPair
}

/**
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,13 @@

package org.klogic.utils.terms

import org.klogic.core.CustomTerm
import org.klogic.core.Goal
import org.klogic.core.Term
import org.klogic.core.and
import org.klogic.core.conde
import org.klogic.core.delay
import org.klogic.core.freshTypedVars
import org.klogic.utils.terms.Cons.Companion.logicListOf
import org.klogic.utils.terms.LogicList.Companion.logicListOf
import org.klogic.utils.terms.Nil.nilLogicList
import org.klogic.utils.terms.OlegLogicNumber.Companion.digitOne
import org.klogic.utils.terms.OlegLogicNumber.Companion.digitZero
Expand All @@ -22,12 +21,9 @@ typealias Digit = Symbol
/**
* Logic number represented by list of [Digit]s, from the last digit to the first.
*/
data class OlegLogicNumber(val digits: Term<LogicList<Digit>>) : CustomTerm<OlegLogicNumber> {
override val subtreesToUnify: Sequence<*> = sequenceOf(digits)

@Suppress("UNCHECKED_CAST")
override fun constructFromSubtrees(subtrees: Iterable<*>): CustomTerm<OlegLogicNumber> =
OlegLogicNumber(subtrees.single() as Term<LogicList<Digit>>)
data class OlegLogicNumber(val digits: Term<LogicList<Digit>>) : UnaryTerm<OlegLogicNumber, Term<LogicList<Digit>>>() {
override val value: Term<LogicList<Digit>> = digits
override val constructor: (Term<LogicList<Digit>>) -> OlegLogicNumber = ::OlegLogicNumber

operator fun get(index: Int): Term<Digit> = (digits as LogicList<Digit>)[index]

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ import org.klogic.core.Var
import org.klogic.core.and
import org.klogic.core.conde
import org.klogic.core.freshTypedVars
import org.klogic.utils.terms.Cons.Companion.logicListOf
import org.klogic.utils.terms.LogicList.Companion.logicListOf
import org.klogic.utils.terms.LogicFalsᴼ.falsᴼ
import org.klogic.utils.terms.LogicTruᴼ.truᴼ
import org.klogic.utils.terms.Nil.nilLogicList
Expand All @@ -34,8 +34,6 @@ object ZeroNaturalNumber : PeanoLogicNumber() {

override fun constructFromSubtrees(subtrees: Iterable<*>): CustomTerm<PeanoLogicNumber> = this

override fun isUnifiableWith(other: CustomTerm<PeanoLogicNumber>): Boolean = other is ZeroNaturalNumber

override fun toInt(): Int = 0

override fun toString(): String = "0"
Expand All @@ -48,8 +46,6 @@ data class PositiveNaturalNumber(val previous: Term<PeanoLogicNumber>) : PeanoLo
override fun constructFromSubtrees(subtrees: Iterable<*>): CustomTerm<PeanoLogicNumber> =
PositiveNaturalNumber(subtrees.single() as Term<PeanoLogicNumber>)

override fun isUnifiableWith(other: CustomTerm<PeanoLogicNumber>): Boolean = other is PositiveNaturalNumber

override fun toInt(): Int {
require(previous !is Var) {
"$this number is not reified"
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
package org.klogic.utils.terms

import org.klogic.core.CustomTerm

/**
* A template for any [CustomTerm] that does not store any values - e.g., objects like [LogicBool].
*/
@Suppress("RedundantModalityModifier")
abstract class EmptyTerm<Term : CustomTerm<Term>> : CustomTerm<Term> {
override val subtreesToUnify: Sequence<*> = emptySequence<Any?>()

override fun constructFromSubtrees(subtrees: Iterable<*>): CustomTerm<Term> = this
}

/**
* A template fpr any [CustomTerm] that stores one value of an arbitrary type.
*/
abstract class UnaryTerm<Term : CustomTerm<Term>, Value> : CustomTerm<Term> {
abstract val value: Value
abstract val constructor: (Value) -> UnaryTerm<Term, Value>

override val subtreesToUnify: Sequence<*>
get() = sequenceOf(value)

override fun constructFromSubtrees(subtrees: Iterable<*>): CustomTerm<Term> {
val value = subtrees.iterator().next()
// Do not check other values for better performance

@Suppress("UNCHECKED_CAST")
return constructor(value as Value)
}
}

/**
* A template fpr any [CustomTerm] that stores two values of arbitrary types.
*/
abstract class BinaryTerm<Term : CustomTerm<Term>, FirstValue, SecondValue> : CustomTerm<Term> {
abstract val first: FirstValue
abstract val second: SecondValue
abstract val constructor: (FirstValue, SecondValue) -> BinaryTerm<Term, FirstValue, SecondValue>

override val subtreesToUnify: Sequence<*>
get() = sequenceOf(first, second)

override fun constructFromSubtrees(subtrees: Iterable<*>): CustomTerm<Term> {
val (first, second) = subtrees.takeFirstAndSecondElements()
// Do not check other values for better performance

@Suppress("UNCHECKED_CAST")
return constructor(first as FirstValue, second as SecondValue)
}

private fun <T> Iterable<T>.takeFirstAndSecondElements(): Pair<T, T> {
val iterator = iterator()

// We use by-hand iteration here to avoid losing performance.
return iterator.next() to iterator.next()
}
}
Loading

0 comments on commit 1768656

Please sign in to comment.