Major refactoring & housekeeping

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

@@ -0,0 +1,173 @@
+package ru.spbstu.logic
+
+import kotlinx.collections.immutable.PersistentMap
+import kotlinx.collections.immutable.persistentMapOf
+import kotlinx.collections.immutable.plus
+import ru.spbstu.wheels.Stack
+import ru.spbstu.wheels.stack
+import kotlin.reflect.KProperty
+
+
+@DslMarker
+annotation class GoalDSL
+
+@GoalDSL
+class GoalScope(
+    var currentSolutions: SStream<System>,
+    var variables: PersistentMap<String, Var>,
+    val scopeStack: Stack<GoalScope>
+) {
+
+    companion object {
+        var ids = 0
+        fun freshId() = ++ids
+    }
+
+    val id = freshId()
+
+    val currentScope get() = scopeStack.top ?: this
+
+    fun equals(lhv: Expr, rhv: Expr) {
+        currentSolutions = currentSolutions.mapNotNull { it.equals(lhv, rhv) }
+    }
+
+    fun never() {
+        currentScope.currentSolutions = SSNil
+    }
+
+    inline fun <T> fork(solutions: SStream<System>, crossinline body: GoalScope.() -> T): SStream<System> {
+        if (solutions is SSNil) return SSNil
+        val freshScope = GoalScope(solutions, variables, scopeStack)
+        scopeStack.push(freshScope)
+        freshScope.body()
+        scopeStack.pop()
+        return freshScope.currentSolutions
+    }
+
+    @GoalDSL
+    inline fun scope(crossinline body: GoalScope.() -> Unit) {
+        currentSolutions = fork(currentSolutions, body)
+    }
+
+    @GoalDSL
+    inline fun choose(vararg goals: GoalScope.() -> Unit) {
+        if (currentSolutions is SSNil) return
+        val it = goals.iterator()
+        val base = currentSolutions
+
+        currentSolutions = it.toSStream().mixMap {
+            fork(base, it)
+        }
+    }
+
+    @GoalDSL
+    fun not(body: GoalScope.() -> Unit) {
+        val solutions = fork(currentSolutions, body)
+        if (solutions !is SSNil) currentSolutions = SSNil
+        TODO()
+    }
+
+    class VarsDelegate(val variable: Var)
+    inner class BindingDelegate(val expr: Expr?)
+
+    val vars = BindingDelegate(null)
+
+    private fun bindVariable(name: String): Var {
+        check(this@GoalScope === currentScope)
+        val v = ScopeVar(name, id)
+        variables += (v.name to v)
+        return v
+    }
+
+    operator fun BindingDelegate.provideDelegate(self: Any?, prop: KProperty<*>): VarsDelegate {
+        val v = bindVariable(prop.name)
+        if (expr != null) equals(v, expr)
+        return VarsDelegate(v)
+    }
+
+    operator fun VarsDelegate.getValue(self: Any?, prop: KProperty<*>): Expr = variable
+
+    operator fun VarsDelegate.setValue(self: Any?, prop: KProperty<*>, rhv: Expr) {
+        currentScope.equals(variable, rhv)
+    }
+
+    fun bind(e: Expr): BindingDelegate = BindingDelegate(e)
+
+    fun any(): Expr = TempVar()
+
+    operator fun Function1.get(arg1: Expr) =
+        App(this, arg1)
+
+    operator fun Function2.get(arg1: Expr, arg2: Expr) =
+        App(this, arg1, arg2)
+
+    operator fun Function3.get(arg1: Expr, arg2: Expr, arg3: Expr) =
+        App(this, arg1, arg2, arg3)
+
+    operator fun Function4.get(arg1: Expr, arg2: Expr, arg3: Expr, arg4: Expr) =
+        App(this, arg1, arg2, arg3, arg4)
+
+    operator fun Function1.set(arg1: Expr, value: Expr) {
+        equals(get(arg1), value)
+    }
+
+    operator fun Function2.set(arg1: Expr, arg2: Expr, value: Expr) {
+        equals(get(arg1, arg2), value)
+    }
+
+    operator fun Function3.set(arg1: Expr, arg2: Expr, arg3: Expr, value: Expr) {
+        equals(get(arg1, arg2, arg3), value)
+    }
+
+    operator fun Function4.set(arg1: Expr, arg2: Expr, arg3: Expr, arg4: Expr, value: Expr) {
+        equals(get(arg1, arg2, arg3, arg4), value)
+    }
+
+    fun asExpr(value: Any) = when (value) {
+        is Expr -> value
+        else -> Constant(value)
+    }
+
+    operator fun Function1.get(arg1: Any) =
+        App(this, asExpr(arg1))
+
+    operator fun Function2.get(arg1: Any, arg2: Any) =
+        App(this, asExpr(arg1), asExpr(arg2))
+
+    operator fun Function3.get(arg1: Any, arg2: Any, arg3: Any) =
+        App(this, asExpr(arg1), asExpr(arg2), asExpr(arg3))
+
+    operator fun Function4.get(arg1: Any, arg2: Any, arg3: Any, arg4: Any) =
+        App(this, asExpr(arg1), asExpr(arg2), asExpr(arg3), asExpr(arg4))
+
+    operator fun Function1.set(arg1: Any, value: Expr) {
+        equals(get(arg1), value)
+    }
+
+    operator fun Function2.set(arg1: Any, arg2: Any, value: Expr) {
+        equals(get(arg1, arg2), value)
+    }
+
+    operator fun Function3.set(arg1: Any, arg2: Any, arg3: Any, value: Expr) {
+        equals(get(arg1, arg2, arg3), value)
+    }
+
+    operator fun Function4.set(arg1: Any, arg2: Any, arg3: Any, arg4: Any, value: Expr) {
+        equals(get(arg1, arg2, arg3, arg4), value)
+    }
+
+    operator fun ProjectedFunction1.get(arg: Any) =
+        ProjectedApp(this, asExpr(arg))
+}
+
+@GoalDSL
+inline fun goal(
+    scope: GoalScope = GoalScope(SSCons(System()), persistentMapOf(), stack()),
+    crossinline body: GoalScope.() -> Unit
+): SStream<Solution> =
+    scope.apply(body).currentSolutions.map {
+        Solution(
+            it,
+            scope.variables.values.toSet()
+        )
+    }

src/main/kotlin/ru/spbstu/Expr.kt → src/main/kotlin/ru/spbstu/logic/Expr.kt

@@ -1,4 +1,4 @@
-package ru.spbstu
+package ru.spbstu.logic
 
 import ru.spbstu.wheels.hashCombine
 import kotlin.reflect.KProperty
@@ -10,6 +10,12 @@ sealed class Expr {
     abstract fun subst(map: Map<Var, Expr>): Expr
 }
 
+object Invalid: Expr() {
+    override fun <C : MutableCollection<Var>> vars(collector: C): C = collector
+    override fun subst(map: Map<Var, Expr>): Expr = this
+    override fun toString(): String = "<INVALID>"
+}
+
 sealed class Atom : Expr()
 sealed class Var : Atom() {
     abstract val name: String
@@ -42,6 +48,10 @@ data class Constant<T>(val value: T) : Atom() {
     override fun subst(map: Map<Var, Expr>) = this
 
     override fun toString(): String = "$value"
+
+    companion object {
+        fun Symbol(name: String): Constant<Symbol> = Symbol.get(name)
+    }
 }
 
 data class MuExpr(val base: Var, val body: Expr) : Expr() {
@@ -68,31 +78,35 @@ sealed class Function {
 
 data class Function1(override val name: String) : Function() {
     companion object {
-        operator fun getValue(self: Any?, prop: KProperty<*>): Function1 = Function1(prop.name)
+        operator fun getValue(self: Any?, prop: KProperty<*>): Function1 =
+            Function1(prop.name)
     }
 
     override fun toString(): String = super.toString()
 }
 
 data class Function2(override val name: String) : Function() {
     companion object {
-        operator fun getValue(self: Any?, prop: KProperty<*>): Function2 = Function2(prop.name)
+        operator fun getValue(self: Any?, prop: KProperty<*>): Function2 =
+            Function2(prop.name)
     }
 
     override fun toString(): String = super.toString()
 }
 
 data class Function3(override val name: String) : Function() {
     companion object {
-        operator fun getValue(self: Any?, prop: KProperty<*>): Function3 = Function3(prop.name)
+        operator fun getValue(self: Any?, prop: KProperty<*>): Function3 =
+            Function3(prop.name)
     }
 
     override fun toString(): String = super.toString()
 }
 
 data class Function4(override val name: String) : Function() {
     companion object {
-        operator fun getValue(self: Any?, prop: KProperty<*>): Function4 = Function4(prop.name)
+        operator fun getValue(self: Any?, prop: KProperty<*>): Function4 =
+            Function4(prop.name)
     }
 
     override fun toString(): String = super.toString()
@@ -165,16 +179,19 @@ operator fun ProjectedFunction1.plus(rhv: ProjectedFunction1): ProjectedFunction
     }
 }
 
-fun ProjectedApp(f: ProjectedFunction1, arg: Expr): Expr? {
+fun ProjectedApp(f: ProjectedFunction1, arg: Expr): Expr {
     return when (arg) {
         is Var -> ProjectedApp(f = f, v = arg)
         is Constant<*> -> try {
             Constant(f.invoke(arg.value))
         } catch (ex: IllegalArgumentException) {
-            null
+            Invalid
         }
-        is ProjectedApp -> ProjectedApp(f + arg.f, arg.v)
-        else -> null
+        is ProjectedApp -> ProjectedApp(
+            f + arg.f,
+            arg.v
+        )
+        else -> Invalid
     }
 }
 
@@ -192,8 +209,21 @@ data class ProjectedApp constructor(val f: ProjectedFunction1, val v: Var) : App
         return collector
     }
 
-    override fun subst(map: Map<Var, Expr>) = ProjectedApp(f = f, arg = v.subst(map)) ?: Constant(null)
+    override fun subst(map: Map<Var, Expr>) = ProjectedApp(
+        f = f,
+        arg = v.subst(map)
+    ) ?: Constant(null)
 
     override fun toString(): String = "$f[$v]"
 }
 
+class Symbol private constructor(val name: String) {
+    override fun equals(other: Any?): Boolean = other is Symbol && name == other.name
+    override fun hashCode(): Int = name.hashCode()
+    override fun toString(): String = name
+
+    companion object {
+        fun get(name: String): Constant<Symbol> = Constant(Symbol(name))
+        operator fun getValue(thisRef: Any?, prop: KProperty<*>): Expr = get(prop.name)
+    }
+}

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

@@ -1,4 +1,4 @@
-package ru.spbstu
+package ru.spbstu.logic
 
 sealed class SStream<out T> : Sequence<T>
 object SSNil : SStream<Nothing>() {
@@ -56,7 +56,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) }
+    is SSCons -> SSCons(body(head)) {
+        tail.map(
+            body
+        )
+    }
 }
 
 fun <T, U> SStream<T>.mapNotNull(body: (T) -> U?): SStream<U> = when (this) {
@@ -66,7 +70,8 @@ fun <T, U> SStream<T>.mapNotNull(body: (T) -> U?): SStream<U> = when (this) {
         while (current is SSCons) {
             val bhead = body(current.head)
             if (bhead != null) {
-                return@run SSCons(bhead) { tail.mapNotNull(body) }
+                val ctail = current.tail
+                return@run SSCons(bhead) { ctail.mapNotNull(body) }
             }
             current = current.tail
         }

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

@@ -0,0 +1,25 @@
+package ru.spbstu.logic
+
+import ru.spbstu.logic.lib.plusO
+import ru.spbstu.logic.lib.reify
+
+fun main(args: Array<String>) {
+//    run {
+//        val c = (1..3).iterator().toSStream()
+//        val mu = c.mixMap { (0..it).iterator().toSStream() }
+//        println(mu.toList())
+//    }
+
+    val res1 = goal {
+        var x by vars
+        var r by vars
+        plusO(x, x, r)
+    }
+    for (r in res1.take(50)) {
+        println("---")
+        for ((k, v) in r) {
+            println("$k = ${reify(v)}")
+        }
+    }
+}
+