Fixes & stuff

vorpal-research · Aug 18, 2020 · 1515ab4 · 1515ab4
1 parent 80fc7e1
commit 1515ab4
Show file tree

Hide file tree

Showing 3 changed files with 92 additions and 39 deletions.
diff --git a/src/main/kotlin/ru/spbstu/Hello.kt b/src/main/kotlin/ru/spbstu/Hello.kt
@@ -3,6 +3,7 @@ package ru.spbstu
 import kotlinx.collections.immutable.*
 import ru.spbstu.wheels.Stack
 import ru.spbstu.wheels.stack
+import java.lang.Exception
 import kotlin.reflect.KProperty
 
 class System(
@@ -78,13 +79,15 @@ class System(
             is AppBase -> {
                 val maybeAlpha = BoundVar(nesting + 1)
                 substitutions[value] = maybeAlpha
-                val maybeNewArgs = value.args.map { expand(it, substitutions, renaming, marked, cache, nesting + 1) }
+                val freshCache = cache.toMutableMap()
+                val maybeNewArgs = value.args.map { expand(it, substitutions, renaming, marked, freshCache, nesting + 1) }
                 var res = value
                 if (!(maybeNewArgs identityEquals value.args)) res = res.copy(args = maybeNewArgs) ?: Constant(null)
                 if (maybeAlpha in marked) {
                     res = MuExpr(maybeAlpha, res)
-                    cache.clear()
+                    freshCache.clear()
                 }
+                cache.putAll(freshCache)
                 marked.remove(maybeAlpha)
                 substitutions.remove(value)
                 res
@@ -395,8 +398,9 @@ fun GoalScope.match(
 ) {
     val choices: MutableList<GoalScope.() -> Unit> = mutableListOf()
     tabler { arg, body ->
-        choices += {
+        choices += choice@{
             equals(arg1, asExpr(arg))
+            if (currentScope.currentSolutions == SSNil) return@choice
             body()
         }
     }
@@ -411,9 +415,10 @@ fun GoalScope.match(
 ) {
     val choices: MutableList<GoalScope.() -> Unit> = mutableListOf()
     tabler { g1, g2, body ->
-        choices += {
+        choices += choice@{
             equals(arg1, asExpr(g1))
             equals(arg2, asExpr(g2))
+            if (currentScope.currentSolutions == SSNil) return@choice
             body()
         }
     }
@@ -429,10 +434,11 @@ fun GoalScope.match(
 ) {
     val choices: MutableList<GoalScope.() -> Unit> = mutableListOf()
     tabler { g1, g2, g3, body ->
-        choices += {
+        choices += choice@{
             equals(arg1, asExpr(g1))
             equals(arg2, asExpr(g2))
             equals(arg3, asExpr(g3))
+            if (currentScope.currentSolutions == SSNil) return@choice
             body()
         }
     }
@@ -449,11 +455,12 @@ fun GoalScope.match(
 ) {
     val choices: MutableList<GoalScope.() -> Unit> = mutableListOf()
     tabler { g1, g2, g3, g4, body ->
-        choices += {
+        choices += choice@{
             equals(arg1, asExpr(g1))
             equals(arg2, asExpr(g2))
             equals(arg3, asExpr(g3))
             equals(arg4, asExpr(g4))
+            if (currentScope.currentSolutions == SSNil) return@choice
             body()
         }
     }
@@ -471,12 +478,13 @@ fun GoalScope.match(
 ) {
     val choices: MutableList<GoalScope.() -> Unit> = mutableListOf()
     tabler { g1, g2, g3, g4, g5, body ->
-        choices += {
+        choices += choice@{
             equals(arg1, asExpr(g1))
             equals(arg2, asExpr(g2))
             equals(arg3, asExpr(g3))
             equals(arg4, asExpr(g4))
             equals(arg5, asExpr(g5))
+            if (currentScope.currentSolutions == SSNil) return@choice
             body()
         }
     }
@@ -491,6 +499,14 @@ data class Solution(val system: System, val variables: Set<Var>) {
             "$it = " + system.expand(it, renaming = renaming, cache = cache)
         }
     }
+
+    operator fun iterator(): Iterator<Pair<Var, Expr>> = iterator {
+        val renaming = mutableMapOf<Var, Var>()
+        val cache = mutableMapOf<Expr, Expr>()
+        for (v in variables) {
+            yield(v to system.expand(v, renaming = renaming, cache = cache))
+        }
+    }
 }
 
 inline fun goal(
@@ -506,7 +522,7 @@ val natZero = Constant("zero")
 val natBits by Function2
 val zeroBit = Constant('0')
 val oneBit = Constant('1')
-val GoalScope.natOne: Expr get() = natBits[1, natZero]
+val GoalScope.natOne: Expr get() = natBits['1', natZero]
 
 val inc by ProjectedFunction1(
     forward = { require(it is Int); it + 1 },
@@ -747,18 +763,33 @@ fun GoalScope.bitAndO(x: Expr, y: Expr, r: Expr) = table(x, y, r) { row ->
     row('1', '1', '1')
 }
 
+fun reify(expr: Expr): Any? = when(expr) {
+    natZero -> 0
+    is App -> when(expr.f) {
+        natBits -> try {
+            val base = reify(expr.args[1]) as Int
+            val cc = if(expr.args[0] == oneBit) 1 else 0
+            cc + base * 2
+        } catch (e: Exception) { expr.toString() }
+        else -> expr.toString()
+    }
+    else -> expr.toString()
+}
+
 fun main(args: Array<String>) {
     val res1 = goal {
-        val n by vars
-        val m by vars
+        var n by vars
+        var m by vars
         var r by vars
-        r = nat(14)
+        //r = nat(13)
         plusO(n, m, r)
 
     }
-    for(r in res1.take(50)) {
+    for (r in res1.take(50)) {
         println("---")
-        println(r)
+        for((k, v) in r) {
+            println("$k = ${reify(v)}")
+        }
     }
 }
 
diff --git a/src/main/kotlin/ru/spbstu/LazyStream.kt b/src/main/kotlin/ru/spbstu/LazyStream.kt
@@ -1,24 +1,25 @@
 package ru.spbstu
 
-sealed class SStream<out T>: Sequence<T>
-object SSNil: SStream<Nothing>() {
-    object NilIterator: Iterator<Nothing> {
+sealed class SStream<out T> : Sequence<T>
+object SSNil : SStream<Nothing>() {
+    object NilIterator : Iterator<Nothing> {
         override fun hasNext(): Boolean = false
         override fun next(): Nothing = throw NoSuchElementException()
     }
+
     override fun iterator(): Iterator<Nothing> = NilIterator
 
     override fun toString(): String = "[]"
 }
 
-data class SSCons<out T>(val head: T, val lazyTail: Lazy<SStream<T>>? = null): SStream<T>() {
-    constructor(head: T, fTail: () -> SStream<T>): this(head, lazy(fTail))
+data class SSCons<out T>(val head: T, val lazyTail: Lazy<SStream<T>>? = null) : SStream<T>() {
+    constructor(head: T, fTail: () -> SStream<T>) : this(head, lazy(fTail))
 
     val tail get() = lazyTail?.value ?: SSNil
     override fun iterator(): Iterator<T> = iterator {
         var current: SStream<T> = this@SSCons
-        loop@while(true) {
-            when(current) {
+        loop@ while (true) {
+            when (current) {
                 is SSCons -> {
                     yield(current.head)
                     current = current.tail
@@ -31,19 +32,15 @@ data class SSCons<out T>(val head: T, val lazyTail: Lazy<SStream<T>>? = null): S
     override fun toString(): String = buildString {
         append('[')
         var current: SStream<T> = this@SSCons
-        while(current is SSCons) {
+        while (current is SSCons) {
             append(current.head)
-            val lazyTail = current.lazyTail
-            if(lazyTail != null) {
-                append(", ")
-
-                if(lazyTail.isInitialized()) {
-                    current = lazyTail.value
-                } else {
-                    append("...")
-                    break
-                }
-            } else break
+            val lazyTail = current.lazyTail ?: break
+            if (!lazyTail.isInitialized()) {
+                append(", ...")
+                break
+            }
+            current = lazyTail.value
+            if(current is SSCons) append(", ")
         }
 
         append(']')
@@ -57,18 +54,18 @@ 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) {
+fun <T, U> SStream<T>.map(body: (T) -> U): SStream<U> = when (this) {
     is SSNil -> SSNil
     is SSCons -> SSCons(body(head)) { tail.map(body) }
 }
 
-fun <T, U> SStream<T>.mapNotNull(body: (T) -> U?): SStream<U> = when(this) {
+fun <T, U> SStream<T>.mapNotNull(body: (T) -> U?): SStream<U> = when (this) {
     is SSNil -> SSNil
     is SSCons -> run {
         var current: SStream<T> = this
-        while(current is SSCons) {
+        while (current is SSCons) {
             val bhead = body(current.head)
-            if(bhead != null) {
+            if (bhead != null) {
                 return@run SSCons(bhead) { tail.mapNotNull(body) }
             }
             current = current.tail
@@ -77,9 +74,26 @@ fun <T, U> SStream<T>.mapNotNull(body: (T) -> U?): SStream<U> = when(this) {
     }
 }
 
-fun <T, U> SStream<T>.mixMap(body: (T) -> SStream<U>): SStream<U> = when(this) {
-    is SSNil -> SSNil
-    is SSCons -> body(head) mix { tail.mixMap(body) }
+fun <T, U> SStream<T>.mixMap(body: (T) -> SStream<U>): SStream<U> = run {
+    when (this) {
+        is SSNil -> SSNil
+        is SSCons -> /* oh, it looked so much better recursion-style =( */
+            when (val bhead = body(head)) {
+                !is SSNil -> bhead mix { tail.mixMap(body) }
+                else -> {
+                    var current = tail
+                    while (current is SSCons) {
+                        val bhead = body(current.head)
+                        if (bhead !is SSNil) {
+                            val current = current
+                            return@run bhead mix { current.tail.mixMap(body) }
+                        }
+                        current = current.tail
+                    }
+                    SSNil
+                }
+            }
+    }
 }
 
 fun <T> Iterator<T>.toSStream(): SStream<T> = when {

diff --git a/src/test/kotlin/ru/spbstu/HelloTest.kt b/src/test/kotlin/ru/spbstu/HelloTest.kt
@@ -0,0 +1,8 @@
+package ru.spbstu
+
+import org.junit.Test
+import kotlin.test.assertEquals
+
+class HelloTest {
+
+}