some more naturals + some tests

pom.xml

@@ -25,7 +25,7 @@
         </dependency>
         <dependency>
             <groupId>org.jetbrains.kotlin</groupId>
-            <artifactId>kotlin-test-junit</artifactId>
+            <artifactId>kotlin-test-testng</artifactId>
             <version>${kotlin.version}</version>
             <scope>test</scope>
         </dependency>
@@ -34,12 +34,6 @@
             <artifactId>kotlin-wheels</artifactId>
             <version>0.0.0.8</version>
         </dependency>
-        <dependency>
-            <groupId>junit</groupId>
-            <artifactId>junit</artifactId>
-            <version>${junit.version}</version>
-            <scope>test</scope>
-        </dependency>
         <dependency>
             <groupId>org.jetbrains.kotlinx</groupId>
             <artifactId>kotlinx-collections-immutable-jvm</artifactId>

src/main/kotlin/ru/spbstu/logic/Dsl.kt

@@ -4,6 +4,7 @@ import kotlinx.collections.immutable.PersistentMap
 import kotlinx.collections.immutable.persistentMapOf
 import kotlinx.collections.immutable.plus
 import ru.spbstu.wheels.Stack
+import ru.spbstu.wheels.memoize
 import ru.spbstu.wheels.stack
 import kotlin.reflect.KProperty
 
@@ -49,6 +50,15 @@ class GoalScope(
         currentSolutions = fork(currentSolutions, body)
     }
 
+    @GoalDSL
+    fun exists(body: GoalScope.(Source<Expr>) -> Unit) {
+        scope {
+            var counter = 0
+            val varStream = Source { bindVariable("\$bound${++counter}") }
+            body(varStream)
+        }
+    }
+
     @GoalDSL
     inline fun choose(vararg goals: GoalScope.() -> Unit) {
         if (currentSolutions is SSNil) return
@@ -92,6 +102,8 @@ class GoalScope(
     }
 
     fun bind(e: Expr): BindingDelegate = BindingDelegate(e)
+    operator fun Expr.provideDelegate(thisRef: Any?, prop: KProperty<*>) =
+        bind(this).provideDelegate(thisRef, prop)
 
     fun any(): Expr = TempVar()
 

src/main/kotlin/ru/spbstu/logic/LazyStream.kt

@@ -57,13 +57,11 @@ infix fun <T> SStream<T>.mix(that: () -> SStream<T>): SStream<T> = when (this) {
 fun <T, U> SStream<T>.map(body: (T) -> U): SStream<U> = when (this) {
     is SSNil -> SSNil
     is SSCons -> SSCons(body(head)) {
-        tail.map(
-            body
-        )
+        tail.map(body)
     }
 }
 
-fun <T, U> SStream<T>.mapNotNull(body: (T) -> U?): SStream<U> = when (this) {
+fun <T, U: Any> SStream<T>.mapNotNull(body: (T) -> U?): SStream<U> = when (this) {
     is SSNil -> SSNil
     is SSCons -> run {
         var current: SStream<T> = this
@@ -104,4 +102,7 @@ fun <T, U> SStream<T>.mixMap(body: (T) -> SStream<U>): SStream<U> = run {
 fun <T> Iterator<T>.toSStream(): SStream<T> = when {
     !hasNext() -> SSNil
     else -> SSCons(next()) { toSStream() }
-}
+}
+
+fun <T> Iterable<T>.toSStream(): SStream<T> = iterator().toSStream()
+fun <T> Sequence<T>.toSStream(): SStream<T> = iterator().toSStream()

src/main/kotlin/ru/spbstu/logic/Main.kt

@@ -1,9 +1,6 @@
 package ru.spbstu.logic
 
-import ru.spbstu.logic.lib.mulO
-import ru.spbstu.logic.lib.nat
-import ru.spbstu.logic.lib.plusO
-import ru.spbstu.logic.lib.reify
+import ru.spbstu.logic.lib.*
 
 fun GoalScope.divModO(n: Expr, m: Expr, d: Expr, r: Expr) {
     scope {
@@ -25,9 +22,13 @@ fun main(args: Array<String>) {
 //    }
 
     val res1 = goal {
-        var x by vars
-        var r by vars
-        divModO(x, r, nat(13), nat(1))
+        var a by vars
+        var b by vars
+        var c by vars
+        var d by vars
+        eqlO(a, b)
+        //x = nat(3)
+
     }
     for (r in res1.take(50)) {
         println("---")

src/main/kotlin/ru/spbstu/logic/Util.kt

@@ -7,3 +7,34 @@ infix fun <T> List<T>.identityEquals(that: List<T>): Boolean {
     }
     return true
 }
+
+abstract class Source<out T>() {
+    abstract fun generate(): T
+
+    val storage: MutableList<@UnsafeVariance T> = mutableListOf()
+
+    fun ensureIndex(ix: Int): T {
+        while(storage.size <= ix) storage.add(generate())
+        return storage[ix]
+    }
+
+    operator fun component1(): T = ensureIndex(0)
+    operator fun component2(): T = ensureIndex(1)
+    operator fun component3(): T = ensureIndex(2)
+    operator fun component4(): T = ensureIndex(3)
+    operator fun component5(): T = ensureIndex(4)
+    operator fun component6(): T = ensureIndex(5)
+    operator fun component7(): T = ensureIndex(6)
+    operator fun component8(): T = ensureIndex(7)
+    operator fun component9(): T = ensureIndex(8)
+    operator fun component10(): T = ensureIndex(9)
+    operator fun component11(): T = ensureIndex(10)
+    operator fun component12(): T = ensureIndex(11)
+    operator fun component13(): T = ensureIndex(12)
+    operator fun component14(): T = ensureIndex(13)
+    operator fun component15(): T = ensureIndex(14)
+}
+
+inline fun <T> Source(crossinline body: () -> T): Source<T> = object: Source<T>() {
+    override fun generate(): T = body()
+}

src/main/kotlin/ru/spbstu/logic/lib/Lists.kt

@@ -113,3 +113,20 @@ fun GoalScope.lengthIO(l: Expr, out: Expr): Unit = scope {
     )
 }
 
+fun GoalScope.lengthO(l: Expr, out: Expr): Unit = scope {
+    var l by bind(l)
+    var out by bind(out)
+    choose(
+        {
+            l = nil; out = natZero
+        },
+        {
+            val t by vars
+            val tlen by vars
+            l = cons[any(), t]
+            lengthO(t, tlen)
+            plusO(tlen, natOne, out)
+        }
+    )
+}
+