multiplication & stuff

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

@@ -1,8 +1,22 @@
 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
 
+fun GoalScope.divModO(n: Expr, m: Expr, d: Expr, r: Expr) {
+    scope {
+        val n by bind(n)
+        val m by bind(m)
+        val d by bind(d)
+        val r by bind(r)
+        var tot by vars
+        mulO(m, d, tot)
+        plusO(tot, r, n)
+    }
+}
+
 fun main(args: Array<String>) {
 //    run {
 //        val c = (1..3).iterator().toSStream()
@@ -13,7 +27,7 @@ fun main(args: Array<String>) {
     val res1 = goal {
         var x by vars
         var r by vars
-        plusO(x, x, r)
+        divModO(x, r, nat(13), nat(1))
     }
     for (r in res1.take(50)) {
         println("---")

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

@@ -136,3 +136,127 @@ fun GoalScope.plusO(n: Expr, m: Expr, k: Expr) = scope {
 }
 
 fun GoalScope.minusO(n: Expr, m: Expr, k: Expr) = plusO(k, m, n)
+
+/*
+(define mulo
+       (\ (n m p)
+       (matche ((n m))
+               ((((()) _))  (== () p))
+               (((_ (())))  (== () p) (poso n))
+               (((((1)) _)) (== m p) (poso m))
+               (((_ ((1)))) (== n p) (>1o n))
+               (((((0 . x)) _))
+                         (exist (z)
+                                (== ((0 . z)) p)
+                                (poso x)
+                                (poso z)
+                                (>1o m)
+                                (mulo x m z)
+                        )
+                )
+               (((((1 . x)) ((0 . y)))) (poso x) (poso y)(mulo m n p))
+               (((((1 . x)) ((1 . y)))) (poso x) (poso y)(odd-mulo x n m p))
+        ))
+)
+*/
+fun GoalScope.mulO(n: Expr, m: Expr, p: Expr): Unit {
+    scope {
+        var n by bind(n)
+        var m by bind(m)
+        var p by bind(p)
+        match(n, m) { case ->
+            case(natZero, any()) { p = natZero }
+            case(any(), natZero) { p = natZero; posO(n) }
+            case(natOne, any())  { p = m; posO(m) }
+            case(any(), natOne)  { p = n; aboveOneO(n) }
+
+            val x by vars
+            case(natBits[zeroBit, x], any()) {
+                var z by vars
+                p = natBits[zeroBit, z]
+                posO(x)
+                posO(z)
+                aboveOneO(m)
+                mulO(x, m, z)
+            }
+
+            val y by vars
+            case(natBits[oneBit, x], natBits[zeroBit, y]) {
+                posO(x)
+                posO(y)
+                mulO(m, n, p)
+            }
+            case(natBits[oneBit, x], natBits[oneBit, y]) {
+                posO(x)
+                posO(y)
+                oddMulO(x, n, m, p)
+            }
+        }
+    }
+}
+
+/*
+(define odd-mulo
+        (\ (x n m p)
+        ( exist(q)
+             (bound-mulo q p n m)
+             (mulo x m q)
+             (pluso ((0 . q)) m p)
+        ))
+)
+*/
+fun GoalScope.oddMulO(x: Expr, n: Expr, m: Expr, p: Expr) {
+    scope {
+        val x by bind(x)
+        val n by bind(n)
+        val m by bind(m)
+        val p by bind(p)
+        var q by vars
+
+        boundMulO(q, p, n, m)
+        mulO(x, m, q)
+        plusO(natBits[zeroBit, q], m, p)
+    }
+}
+/*
+(define bound-mulo
+        (\ (q p n m)
+        (matche ((q p))
+                ((((()) ((_ . _)))))
+                (((((_ . x)) ((_ . y))))
+                        (exist(a z)
+                              (conde ((== (())n) (== ((a . z))m) (bound-mulo x y z (())))
+                                     ((== ((a . z))n) (bound-mulo x y z m))
+                              )
+                        )
+                )
+        ))
+)
+* */
+fun GoalScope.boundMulO(q: Expr, p: Expr, n: Expr, m: Expr) {
+    scope {
+        val q by bind(q)
+        val p by bind(p)
+        var n by bind(n)
+        var m by bind(m)
+
+        match(q, p) { case ->
+            case(natZero, natBits[any(), any()]) {}
+            val x by vars
+            val y by vars
+            case(natBits[any(), x], natBits[any(), y]) {
+                val a by vars
+                val z by vars
+                choose(
+                    {
+                        n = natZero
+                        m = natBits[a, z]
+                        boundMulO(x, y, z, natZero)
+                    }
+                )
+            }
+        }
+    }
+}
+
+

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

@@ -5,15 +5,16 @@ import kotlinx.collections.immutable.persistentListOf
 import kotlinx.collections.immutable.plus
 import ru.spbstu.logic.App
 import ru.spbstu.logic.Expr
+import java.math.BigInteger
 
 fun reify(expr: Expr): Any? = when (expr) {
-    natZero -> 0
+    natZero -> 0.toBigInteger()
     nil -> persistentListOf<Expr>()
     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
+            val base = reify(expr.args[1]) as BigInteger
+            val cc = if (expr.args[0] == oneBit) 1.toBigInteger() else 0.toBigInteger()
+            cc + base * 2.toBigInteger()
         } catch (e: Exception) {
             expr.toString()
         }