Skip to content

Commit 49f6f29

Browse files
DamtevDamtev
authored
Implemented logic booleans, Peano and Oleg's numbers (#6)
1 parent e6fa9ec commit 49f6f29

File tree

37 files changed

+1291
-279
lines changed

37 files changed

+1291
-279
lines changed

Diff for: ‎.github/workflows/build-and-run-tests.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -35,4 +35,4 @@ jobs:
3535
if: always()
3636
with:
3737
name: klogic-tests-report
38-
path: ./**/build/reports/tests/test/
38+
path: klogic-test-results/build/reports/tests/unit-test/aggregated-results

Diff for: ‎buildSrc/build.gradle.kts

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
plugins {
2+
`kotlin-dsl`
3+
}
4+
5+
repositories {
6+
mavenCentral()
7+
gradlePluginPortal()
8+
}
9+
10+
dependencies {
11+
implementation("org.jetbrains.kotlin:kotlin-gradle-plugin:1.8.0")
12+
}

Diff for: ‎build.gradle.kts renamed to ‎buildSrc/src/main/kotlin/org.klogic.klogic-base.gradle.kts

+6-6
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
1+
import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
2+
13
plugins {
2-
kotlin("jvm") version "1.8.0"
4+
kotlin("jvm")
35
}
46

5-
repositories{
7+
repositories {
68
mavenCentral()
79
}
810

9-
dependencies{
10-
implementation("org.jetbrains.kotlin:kotlin-reflect:1.8.0")
11-
implementation("org.jetbrains.kotlinx:kotlinx-collections-immutable:0.3.5")
11+
dependencies {
1212
// https://mvnrepository.com/artifact/org.junit.jupiter/junit-jupiter-api
1313
testImplementation("org.junit.jupiter:junit-jupiter-api:5.9.2")
1414
testImplementation("org.junit.jupiter:junit-jupiter-engine:5.9.2")
@@ -19,7 +19,7 @@ java {
1919
targetCompatibility = JavaVersion.VERSION_11
2020
}
2121

22-
tasks.withType<org.jetbrains.kotlin.gradle.tasks.KotlinCompile> {
22+
tasks.withType<KotlinCompile> {
2323
kotlinOptions {
2424
freeCompilerArgs += listOf("-Xjvm-default=all", "-Xcontext-receivers")
2525
allWarningsAsErrors = true

Diff for: ‎gradle/wrapper/gradle-wrapper.properties

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
distributionBase=GRADLE_USER_HOME
22
distributionPath=wrapper/dists
3-
distributionUrl=https\://services.gradle.org/distributions/gradle-7.1.1-bin.zip
3+
distributionUrl=https\://services.gradle.org/distributions/gradle-8.0.1-bin.zip
44
zipStoreBase=GRADLE_USER_HOME
55
zipStorePath=wrapper/dists

Diff for: ‎klogic-core/build.gradle.kts

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
plugins {
2+
id("org.klogic.klogic-base")
3+
}
4+
5+
dependencies{
6+
implementation("org.jetbrains.kotlin:kotlin-reflect:1.8.0")
7+
implementation("org.jetbrains.kotlinx:kotlinx-collections-immutable:0.3.5")
8+
testImplementation(project(":klogic-utils"))
9+
testImplementation(testFixtures(project(":klogic-utils")))
10+
}

Diff for: ‎src/main/kotlin/org/klogic/core/Constraint.kt renamed to ‎klogic-core/src/main/kotlin/org/klogic/core/Constraint.kt

File renamed without changes.

Diff for: ‎src/main/kotlin/org/klogic/core/Goal.kt renamed to ‎klogic-core/src/main/kotlin/org/klogic/core/Goal.kt

+51-1
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,32 @@ infix fun Goal.and(other: Goal): Goal = { st: State -> this(st) bind other }
99
infix fun Goal.`|||`(other: Goal): Goal = this or other
1010
infix fun Goal.`&&&`(other: Goal): Goal = this and other
1111

12+
/**
13+
* Calculates g1 ||| (g2 ||| (g3 ||| ... gn)) for a non-empty list of goals.
14+
*
15+
* NOTE: right association!
16+
*/
17+
fun conde(vararg goals: Goal): Goal {
18+
require(goals.isNotEmpty()) {
19+
"Expected at least one goal for conde but got 0"
20+
}
21+
22+
return goals.reduceRight(Goal::or)
23+
}
24+
25+
/**
26+
* Calculates g1 &&& (g2 &&& (g3 &&& ... gn)) for a non-empty list of goals.
27+
*
28+
* NOTE: right association!
29+
*/
30+
fun and(vararg goals: Goal): Goal {
31+
require(goals.isNotEmpty()) {
32+
"Expected at least one goal for `and` but got 0"
33+
}
34+
35+
return goals.reduceRight(Goal::and)
36+
}
37+
1238
/**
1339
* Creates a lazy [Goal] by passed goal generator [f].
1440
*/
@@ -19,10 +45,34 @@ fun delay(f: () -> Goal): Goal = { st: State -> ThunkStream { f()(st) } }
1945
*
2046
* @see [delay], [State.freshTypedVar].
2147
*/
22-
fun <T : Term<T>> freshTypedVar(f: (Term<T>) -> Goal): Goal = delay {
48+
fun <T : Term<T>> freshTypedVars(f: (Term<T>) -> Goal): Goal = delay {
2349
{ st: State -> f(st.freshTypedVar())(st) }
2450
}
2551

52+
fun <T1 : Term<T1>, T2 : Term<T2>> freshTypedVars(f: (Term<T1>, Term<T2>) -> Goal): Goal = delay {
53+
{ st: State -> f(st.freshTypedVar(), st.freshTypedVar())(st) }
54+
}
55+
56+
fun <T1 : Term<T1>, T2 : Term<T2>, T3 : Term<T3>> freshTypedVars(f: (Term<T1>, Term<T2>, Term<T3>) -> Goal): Goal = delay {
57+
{ st: State -> f(st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar())(st) }
58+
}
59+
60+
fun <T1 : Term<T1>, T2 : Term<T2>, T3 : Term<T3>, T4 : Term<T4>> freshTypedVars(f: (Term<T1>, Term<T2>, Term<T3>, Term<T4>) -> Goal): Goal = delay {
61+
{ st: State -> f(st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar())(st) }
62+
}
63+
64+
fun <T1 : Term<T1>, T2 : Term<T2>, T3 : Term<T3>, T4 : Term<T4>, T5 : Term<T5>> freshTypedVars(f: (Term<T1>, Term<T2>, Term<T3>, Term<T4>, Term<T5>) -> Goal): Goal = delay {
65+
{ st: State -> f(st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar())(st) }
66+
}
67+
68+
fun <T1 : Term<T1>, T2 : Term<T2>, T3 : Term<T3>, T4 : Term<T4>, T5 : Term<T5>, T6: Term<T6>> freshTypedVars(f: (Term<T1>, Term<T2>, Term<T3>, Term<T4>, Term<T5>, Term<T6>) -> Goal): Goal = delay {
69+
{ st: State -> f(st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar())(st) }
70+
}
71+
72+
fun <T1 : Term<T1>, T2 : Term<T2>, T3 : Term<T3>, T4 : Term<T4>, T5 : Term<T5>, T6: Term<T6>, T7: Term<T7>> freshTypedVars(f: (Term<T1>, Term<T2>, Term<T3>, Term<T4>, Term<T5>, Term<T6>, Term<T7>) -> Goal): Goal = delay {
73+
{ st: State -> f(st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar(), st.freshTypedVar())(st) }
74+
}
75+
2676
/**
2777
* Represents an answer to evaluating the [run] expression. Contains reified [term], calculated by walking the term,
2878
* passed to [run], with corresponding to calculated [Goal]s [Substitution]s,

Diff for: ‎src/main/kotlin/org/klogic/core/State.kt renamed to ‎klogic-core/src/main/kotlin/org/klogic/core/State.kt

File renamed without changes.

Diff for: ‎src/main/kotlin/org/klogic/core/Stream.kt renamed to ‎klogic-core/src/main/kotlin/org/klogic/core/Stream.kt

File renamed without changes.

Diff for: ‎src/main/kotlin/org/klogic/core/Substitution.kt renamed to ‎klogic-core/src/main/kotlin/org/klogic/core/Substitution.kt

File renamed without changes.

Diff for: ‎src/main/kotlin/org/klogic/core/Term.kt renamed to ‎klogic-core/src/main/kotlin/org/klogic/core/Term.kt

+13-4
Original file line numberDiff line numberDiff line change
@@ -77,9 +77,17 @@ sealed interface Term<T : Term<T>> {
7777
@Suppress("UNCHECKED_CAST")
7878
fun <R : Term<R>> cast(): Term<R> = this as Term<R>
7979

80+
/**
81+
* Considers this term as already reified.
82+
*/
83+
@Suppress("UNCHECKED_CAST")
84+
fun asReified(): T = this as T
85+
8086
infix fun `===`(other: Term<T>): Goal = this unify other
8187
infix fun `!==`(other: Term<T>): Goal = this ineq other
8288

89+
fun isVar(): Boolean = this is Var<*>
90+
8391
companion object {
8492
/**
8593
* Unifies [left] with [right] by invoking non-static method.
@@ -100,8 +108,8 @@ value class Var<T : Term<T>>(val index: Int) : Term<T> {
100108
(it.walk(substitution))
101109
} ?: this
102110

103-
override fun unifyImpl(walkedOther: Term<T>, unificationState: UnificationState): UnificationState? {
104-
return if (walkedOther is Var<T>) {
111+
override fun unifyImpl(walkedOther: Term<T>, unificationState: UnificationState): UnificationState? =
112+
if (walkedOther is Var<T>) {
105113
if (this == walkedOther) {
106114
unificationState
107115
} else {
@@ -120,11 +128,12 @@ value class Var<T : Term<T>>(val index: Int) : Term<T> {
120128
unificationState.copy(substitution = unificationState.substitution + newAssociation)
121129
}
122130
}
123-
}
124131

125132
@Suppress("UNCHECKED_CAST")
126133
override fun <T2 : Term<T2>> cast(): Var<T2> = this as Var<T2>
127134

135+
override fun asReified(): T = error("Variable $this is not reified")
136+
128137
override fun toString(): String = "_.$index"
129138

130139
companion object {
@@ -164,7 +173,7 @@ interface CustomTerm<T : CustomTerm<T>> : Term<T> {
164173
override fun unifyImpl(walkedOther: Term<T>, unificationState: UnificationState): UnificationState? {
165174
if (walkedOther !is CustomTerm) {
166175
// This branch means that walkedOther is Var
167-
return walkedOther.unify(this, unificationState)
176+
return walkedOther.unifyImpl(this, unificationState)
168177
}
169178

170179
if (!(this isUnifiableWith walkedOther)) {

Diff for: ‎src/main/kotlin/org/klogic/unify/Unify.kt renamed to ‎klogic-core/src/main/kotlin/org/klogic/unify/Unify.kt

File renamed without changes.

Diff for: ‎src/test/kotlin/org/klogic/core/RunTest.kt renamed to ‎klogic-core/src/test/kotlin/org/klogic/core/RunTest.kt

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ package org.klogic.core
33
import org.junit.jupiter.api.Assertions.assertEquals
44
import org.junit.jupiter.api.Test
55
import org.klogic.core.Var.Companion.createTypedVar
6-
import org.klogic.terms.Symbol
7-
import org.klogic.terms.Symbol.Companion.toSymbol
6+
import org.klogic.utils.terms.Symbol
7+
import org.klogic.utils.terms.Symbol.Companion.toSymbol
88

99
class RunTest {
1010
@Test

Diff for: ‎src/test/kotlin/org/klogic/core/streams/BindTest.kt renamed to ‎klogic-core/src/test/kotlin/org/klogic/core/streams/BindTest.kt

-1
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@ import org.junit.jupiter.api.Assertions.assertEquals
44
import org.junit.jupiter.api.Test
55
import org.klogic.core.ConsStream
66
import org.klogic.core.RecursiveStream.Companion.nil
7-
import org.klogic.utils.ones
87

98
class BindTest {
109
@Test

Diff for: ‎src/test/kotlin/org/klogic/core/streams/MplusTest.kt renamed to ‎klogic-core/src/test/kotlin/org/klogic/core/streams/MplusTest.kt

-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@ package org.klogic.core.streams
33
import org.junit.jupiter.api.Assertions.assertEquals
44
import org.junit.jupiter.api.Test
55
import org.klogic.core.ThunkStream
6-
import org.klogic.utils.ones
7-
import org.klogic.utils.repeat
86

97
class MplusTest {
108
private fun twos(): ThunkStream<Int> = repeat(2)

Diff for: ‎klogic-core/src/test/kotlin/org/klogic/core/streams/StreamTestUtils.kt

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
package org.klogic.core.streams
2+
3+
import org.klogic.core.ConsStream
4+
import org.klogic.core.ThunkStream
5+
6+
internal fun <T> repeat(element: T): ThunkStream<T> = ThunkStream {
7+
ConsStream(element, repeat(element))
8+
}
9+
10+
internal fun ones(): ThunkStream<Int> = repeat(1)

Diff for: ‎src/test/kotlin/org/klogic/core/unify/InequalityTest.kt renamed to ‎klogic-core/src/test/kotlin/org/klogic/core/unify/InequalityTest.kt

+6-6
Original file line numberDiff line numberDiff line change
@@ -13,12 +13,12 @@ import org.klogic.core.reify
1313
import org.klogic.core.run
1414
import org.klogic.core.unreifiedRun
1515
import org.klogic.core.`|||`
16-
import org.klogic.terms.Cons.Companion.logicListOf
17-
import org.klogic.terms.LogicList
18-
import org.klogic.terms.Nil.nilLogicList
19-
import org.klogic.terms.Symbol
20-
import org.klogic.terms.plus
21-
import org.klogic.terms.toLogicList
16+
import org.klogic.utils.terms.Cons.Companion.logicListOf
17+
import org.klogic.utils.terms.LogicList
18+
import org.klogic.utils.terms.Nil.nilLogicList
19+
import org.klogic.utils.terms.Symbol
20+
import org.klogic.utils.terms.plus
21+
import org.klogic.utils.terms.toLogicList
2222
import org.klogic.utils.*
2323

2424
// Some tests are taken from faster-minikanren

Diff for: ‎src/test/kotlin/org/klogic/core/unify/UnifyTest.kt renamed to ‎klogic-core/src/test/kotlin/org/klogic/core/unify/UnifyTest.kt

+4-4
Original file line numberDiff line numberDiff line change
@@ -7,10 +7,10 @@ import org.klogic.core.Substitution
77
import org.klogic.core.reified
88
import org.klogic.core.run
99
import org.klogic.core.`|||`
10-
import org.klogic.terms.Nil.nilLogicList
11-
import org.klogic.terms.Symbol
12-
import org.klogic.terms.plus
13-
import org.klogic.terms.toLogicList
10+
import org.klogic.utils.terms.Nil.nilLogicList
11+
import org.klogic.utils.terms.Symbol
12+
import org.klogic.utils.terms.plus
13+
import org.klogic.utils.terms.toLogicList
1414
import org.klogic.unify.unifyWithConstraintsVerification
1515
import org.klogic.utils.*
1616

Diff for: ‎src/test/kotlin/org/klogic/core/unify/WalkTest.kt renamed to ‎klogic-core/src/test/kotlin/org/klogic/core/unify/WalkTest.kt

+2-2
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ package org.klogic.core.unify
33
import org.junit.jupiter.api.Assertions.assertEquals
44
import org.junit.jupiter.api.Test
55
import org.klogic.core.Substitution.Companion.of
6-
import org.klogic.terms.Nil.nilLogicList
7-
import org.klogic.terms.Symbol
6+
import org.klogic.utils.terms.Nil.nilLogicList
7+
import org.klogic.utils.terms.Symbol
88
import org.klogic.utils.x
99

1010
class WalkTest {

Diff for: ‎klogic-test-results/build.gradle.kts

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
plugins {
2+
id("org.klogic.klogic-base")
3+
id("test-report-aggregation")
4+
}
5+
6+
repositories {
7+
gradlePluginPortal()
8+
}
9+
10+
dependencies {
11+
testReportAggregation(project(":klogic-core"))
12+
testReportAggregation(project(":klogic-utils"))
13+
}
14+
15+
tasks.check {
16+
dependsOn(tasks.named<TestReport>("testAggregateTestReport"))
17+
}

Diff for: ‎klogic-utils/build.gradle.kts

+9
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
plugins {
2+
id("org.klogic.klogic-base")
3+
`java-test-fixtures`
4+
}
5+
6+
dependencies {
7+
implementation(project(":klogic-core"))
8+
testFixturesImplementation(project(":klogic-core"))
9+
}

Diff for: ‎klogic-utils/src/main/kotlin/org/klogic/utils/terms/LogicBool.kt

+66
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
@file:Suppress("ClassName", "NonAsciiCharacters", "ObjectPropertyName")
2+
3+
package org.klogic.utils.terms
4+
5+
import org.klogic.core.CustomTerm
6+
import org.klogic.core.Goal
7+
import org.klogic.core.Term
8+
import org.klogic.core.and
9+
import org.klogic.core.conde
10+
import org.klogic.utils.terms.LogicFalsᴼ.falsᴼ
11+
import org.klogic.utils.terms.LogicTruᴼ.truᴼ
12+
13+
sealed class LogicBool : CustomTerm<LogicBool> {
14+
abstract fun toBool(): Boolean
15+
16+
override fun toString(): String = toBool().toString()
17+
18+
companion object {
19+
fun Boolean.toLogicBool(): LogicBool = if (this) LogicFalsᴼ else LogicTruᴼ
20+
}
21+
}
22+
23+
object LogicFalsᴼ : LogicBool() {
24+
val falsᴼ: LogicFalsᴼ = this
25+
26+
override val subtreesToUnify: Sequence<*>
27+
get() = emptySequence<Any?>()
28+
29+
override fun constructFromSubtrees(subtrees: List<*>): CustomTerm<LogicBool> = this
30+
31+
override fun isUnifiableWith(other: CustomTerm<LogicBool>): Boolean = other is LogicFalsᴼ
32+
33+
override fun toBool(): Boolean = false
34+
}
35+
36+
object LogicTruᴼ : LogicBool() {
37+
val truᴼ: LogicTruᴼ = this
38+
39+
override val subtreesToUnify: Sequence<*>
40+
get() = emptySequence<Any?>()
41+
42+
override fun constructFromSubtrees(subtrees: List<*>): CustomTerm<LogicBool> = this
43+
44+
override fun isUnifiableWith(other: CustomTerm<LogicBool>): Boolean = other is LogicTruᴼ
45+
46+
override fun toBool(): Boolean = true
47+
}
48+
49+
fun notᴼ(x: Term<LogicBool>, y: Term<LogicBool>): Goal = conde(
50+
(x `===` falsᴼ) and (y `===` truᴼ),
51+
(y `===` falsᴼ) and (x `===` truᴼ),
52+
)
53+
54+
fun orᴼ(x: Term<LogicBool>, y: Term<LogicBool>, z: Term<LogicBool>): Goal = conde(
55+
(x `===` falsᴼ) and (y `===` falsᴼ) and (z `===` falsᴼ),
56+
(x `===` falsᴼ) and (y `===` truᴼ) and (z `===` truᴼ),
57+
(x `===` truᴼ) and (y `===` falsᴼ) and (z `===` truᴼ),
58+
(x `===` truᴼ) and (y `===` truᴼ) and (z `===` truᴼ),
59+
)
60+
61+
fun andᴼ(x: Term<LogicBool>, y: Term<LogicBool>, z: Term<LogicBool>): Goal = conde(
62+
(x `===` falsᴼ) and (y `===` falsᴼ) and (z `===` falsᴼ),
63+
(x `===` falsᴼ) and (y `===` truᴼ) and (z `===` falsᴼ),
64+
(x `===` truᴼ) and (y `===` falsᴼ) and (z `===` falsᴼ),
65+
(x `===` truᴼ) and (y `===` truᴼ) and (z `===` truᴼ),
66+
)

0 commit comments

Comments
 (0)