Some equivalent test programs in Scheme running on microKanren and miniKanren for benchmark comparisonsHEADmaster

13 files changed, 1066 insertions, 0 deletions

diff --git a/scheme/houses-mk.sh b/scheme/houses-mk.sh
new file mode 100755
index 0000000..c2045d6
--- /dev/null
+++ b/scheme/houses-mk.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+
+/usr/bin/env -S guile -e run-houses -l "mk.scm" -l "mkdefs.scm" -s "houses.scm"
+
+
diff --git a/scheme/houses-uk.sh b/scheme/houses-uk.sh
new file mode 100755
index 0000000..d17893b
--- /dev/null
+++ b/scheme/houses-uk.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+
+/usr/bin/env -S guile -e run-houses -l "uk.scm" -l "mkdefs.scm" -s "houses.scm"
+
+
diff --git a/scheme/houses.scm b/scheme/houses.scm
new file mode 100644
index 0000000..8178bf5
--- /dev/null
+++ b/scheme/houses.scm
@@ -0,0 +1,84 @@
+
+; Equivalent to example/houses.adb
+
+
+(define (value bin)
+  (cond
+    ((null? bin) 0)
+    ((zero? (car bin)) (* 2 (value (cdr bin))))
+    (#t (+ 1 (* 2 (value (cdr bin)))))))
+
+
+(define (do-unique x li)
+  (fresh (h t)
+    (caro li h)
+    (cdro li t)
+    (conde
+      ((<o x h))
+      ((<o h x)))
+    (conde
+      ((== t '()))
+      ((do-unique x t)))))
+
+
+(define (unique li)
+  (fresh (h t)
+    (caro li h)
+    (cdro li t)
+    (conde
+      ((== t '()))
+      ((do-unique h t) (unique t)))))
+
+
+(define (within-range v l h)
+  (conde
+    ((<=o l v) (<=o v h))
+    (fail)))
+
+
+(define (doors-from a d b)
+  (conde
+    ((pluso a d b))
+    ((minuso a d b))))
+
+
+(define (houses a1 a2 b1 b2 c1 c2 d1 d2)
+  (conde
+    ((within-range a1 (build-num 3) (build-num 8))
+     (within-range a2 (build-num 2) (build-num 8))
+     (within-range b1 (build-num 6) (build-num 8))
+     (within-range b2 (build-num 4) (build-num 7))
+     (within-range c1 (build-num 5) (build-num 8))
+     (within-range c2 (build-num 2) (build-num 8))
+     (within-range d1 (build-num 1) (build-num 3))
+     (within-range d2 (build-num 5) (build-num 7))
+
+     (unique `(,a1 ,a2 ,b1 ,b2 ,c1 ,c2 ,d1 ,d2))
+
+     (doors-from a1 (build-num 1) a2)
+     (doors-from b1 (build-num 2) b2)
+     (doors-from c1 (build-num 3) c2)
+     (doors-from d1 (build-num 4) d2)
+
+     (<o b2 c1))
+    (fail)))
+
+
+(define (run-houses args)
+  (let*
+      ((s (run 1 (h)
+          (fresh (s t u v w x y z)
+            (== h `(,s ,t ,u ,v ,w ,x ,y ,z))
+            (houses s t u v w x y z))))
+       (r (car s)))
+    (begin
+      (display (string-append "Allison: "  (number->string (value (list-ref r 0))))) (newline)
+      (display (string-append "Adrienne: " (number->string (value (list-ref r 1))))) (newline)
+      (display (string-append "Belinda: "  (number->string (value (list-ref r 2))))) (newline)
+      (display (string-append "Benito: "   (number->string (value (list-ref r 3))))) (newline)
+      (display (string-append "Cheri: "    (number->string (value (list-ref r 4))))) (newline)
+      (display (string-append "Crawford: " (number->string (value (list-ref r 5))))) (newline)
+      (display (string-append "Daryl: "    (number->string (value (list-ref r 6))))) (newline)
+      (display (string-append "Don: "      (number->string (value (list-ref r 7))))) (newline))))
+
+
diff --git a/scheme/logo-mk.sh b/scheme/logo-mk.sh
new file mode 100755
index 0000000..f53f976
--- /dev/null
+++ b/scheme/logo-mk.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+
+/usr/bin/env -S guile -e run-logo -l "mk.scm" -l "mkdefs.scm" -s "logo.scm"
+
+
diff --git a/scheme/logo-uk.sh b/scheme/logo-uk.sh
new file mode 100755
index 0000000..cda4aa7
--- /dev/null
+++ b/scheme/logo-uk.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+
+/usr/bin/env -S guile -e run-logo -l "uk.scm" -l "mkdefs.scm" -s "logo.scm"
+
+
diff --git a/scheme/logo.scm b/scheme/logo.scm
new file mode 100644
index 0000000..18fc9ed
--- /dev/null
+++ b/scheme/logo.scm
@@ -0,0 +1,49 @@
+
+; Equivalent to test/logo.adb
+
+
+(define (value bin)
+  (cond
+    ((null? bin) 0)
+    ((zero? (car bin)) (* 2 (value (cdr bin))))
+    (#t (+ 1 (* 2 (value (cdr bin)))))))
+
+
+(define (test pow base)
+  (begin
+    (display (string-append "log_" (number->string base) " (" (number->string pow) ") = "))
+    (let* ((n (build-num pow))
+           (b (build-num base))
+           (s (run 1 (d) (fresh (q r) (== d `(,q ,r)) (logo n b q r))))
+           (q (car (car s)))
+           (r (car (cdr (car s)))))
+      (begin
+        (display (value q))
+        (display " r ")
+        (display (value r))
+        (newline)))))
+
+
+(define (run-logo args)
+  (begin
+    (display "Logarithm")
+    (newline)
+    (test 1 1)
+    (test 68 2)
+    (test 68 3)
+    (test 68 4)
+    (test 68 5)
+    (test 68 6)
+    (test 68 7)
+    (test 68 8)
+    (newline)
+    (display "Expected Failure")
+    (newline)
+    (display (run 1 (d) (fresh (q r) (== d `(,q ,r)) (logo 68 1 q r))))
+    (newline)
+    (display (run 1 (d) (fresh (q r) (== d `(,q ,r)) (logo 68 0 q r))))
+    (newline)
+    (display (run 1 (d) (fresh (q r) (== d `(,q ,r)) (logo 0 0 q r))))
+    (newline)))
+
+
diff --git a/scheme/mk.scm b/scheme/mk.scm
new file mode 100644
index 0000000..9917284
--- /dev/null
+++ b/scheme/mk.scm
@@ -0,0 +1,269 @@
+
+; miniKanren core from simple-miniKanren
+
+; https://minikanren.org
+; https://github.com/miniKanren/simple-miniKanren
+
+
+;;; This file was generated by writeminikanren.pl
+;;; Generated at 2007-10-25 15:24:42
+
+(define-syntax lambdag@
+  (syntax-rules ()
+    ((_ (p) e) (lambda (p) e))))
+
+(define-syntax lambdaf@
+  (syntax-rules ()
+    ((_ () e) (lambda () e))))
+
+(define-syntax run*
+  (syntax-rules ()
+    ((_ (x) g ...) (run #f (x) g ...))))
+
+(define-syntax rhs
+  (syntax-rules ()
+    ((_ x) (cdr x))))
+
+(define-syntax lhs
+  (syntax-rules ()
+    ((_ x) (car x))))
+
+(define-syntax size-s
+  (syntax-rules ()
+    ((_ x) (length x))))
+
+(define-syntax var
+  (syntax-rules ()
+    ((_ x) (vector x))))
+
+(define-syntax var?
+  (syntax-rules ()
+    ((_ x) (vector? x))))
+
+(define empty-s '())
+
+(define walk
+  (lambda (u S)
+    (cond
+      ((and (var? u) (assq u S)) =>
+       (lambda (pr) (walk (rhs pr) S)))
+      (else u))))
+
+(define ext-s
+  (lambda (x v s)
+    (cons `(,x . ,v) s)))
+
+(define unify
+  (lambda (u v s)
+    (let ((u (walk u s))
+          (v (walk v s)))
+      (cond
+        ((eq? u v) s)
+        ((var? u) (ext-s-check u v s))
+        ((var? v) (ext-s-check v u s))
+        ((and (pair? u) (pair? v))
+         (let ((s (unify 
+                    (car u) (car v) s)))
+           (and s (unify 
+                    (cdr u) (cdr v) s))))
+        ((equal? u v) s)
+        (else #f)))))
+
+(define ext-s-check
+  (lambda (x v s)
+    (cond
+      ((occurs-check x v s) #f)
+      (else (ext-s x v s)))))
+
+(define occurs-check
+  (lambda (x v s)
+    (let ((v (walk v s)))
+      (cond
+        ((var? v) (eq? v x))
+        ((pair? v) 
+         (or 
+           (occurs-check x (car v) s)
+           (occurs-check x (cdr v) s)))
+        (else #f)))))
+
+(define walk*
+  (lambda (w s)
+    (let ((v (walk w s)))
+      (cond
+        ((var? v) v)
+        ((pair? v)
+         (cons
+           (walk* (car v) s)
+           (walk* (cdr v) s)))
+        (else v)))))
+
+(define reify-s
+  (lambda (v s)
+    (let ((v (walk v s)))
+      (cond
+        ((var? v)
+         (ext-s v (reify-name (size-s s)) s))
+        ((pair? v) (reify-s (cdr v)
+                     (reify-s (car v) s)))
+        (else s)))))
+
+(define reify-name
+  (lambda (n)
+    (string->symbol
+      (string-append "_" "." (number->string n)))))
+
+(define reify
+  (lambda (v s)
+    (let ((v (walk* v s)))
+      (walk* v (reify-s v empty-s)))))
+
+(define-syntax mzero 
+  (syntax-rules () ((_) #f)))
+
+(define-syntax inc 
+  (syntax-rules () ((_ e) (lambdaf@ () e))))
+
+(define-syntax unit 
+  (syntax-rules () ((_ a) a)))
+
+(define-syntax choice 
+  (syntax-rules () ((_ a f) (cons a f))))
+ 
+(define-syntax case-inf
+  (syntax-rules ()
+    ((_ e (() e0) ((f^) e1) ((a^) e2) ((a f) e3))
+     (let ((a-inf e))
+       (cond
+         ((not a-inf) e0)
+         ((procedure? a-inf)  (let ((f^ a-inf)) e1))
+         ((not (and (pair? a-inf)
+                    (procedure? (cdr a-inf))))
+          (let ((a^ a-inf)) e2))
+         (else (let ((a (car a-inf)) (f (cdr a-inf))) 
+                 e3)))))))
+
+(define-syntax run
+  (syntax-rules ()
+    ((_ n (x) g0 g ...)
+     (take n
+       (lambdaf@ ()
+         ((fresh (x) g0 g ... 
+            (lambdag@ (s)
+              (cons (reify x s) '())))
+          empty-s))))))
+ 
+(define take
+  (lambda (n f)
+    (if (and n (zero? n)) 
+      '()
+      (case-inf (f)
+        (() '())
+        ((f) (take n f))
+        ((a) a)
+        ((a f)
+         (cons (car a)
+           (take (and n (- n 1)) f)))))))
+
+(define ==
+  (lambda (u v)
+    (lambdag@ (s)
+      (unify u v s))))
+ 
+(define-syntax fresh
+  (syntax-rules ()
+    ((_ (x ...) g0 g ...)
+     (lambdag@ (s)
+       (inc
+         (let ((x (var 'x)) ...)
+           (bind* (g0 s) g ...)))))))
+ 
+(define-syntax bind*
+  (syntax-rules ()
+    ((_ e) e)
+    ((_ e g0 g ...) (bind* (bind e g0) g ...))))
+ 
+(define bind
+  (lambda (a-inf g)
+    (case-inf a-inf
+      (() (mzero))
+      ((f) (inc (bind (f) g)))
+      ((a) (g a))
+      ((a f) (mplus (g a) (lambdaf@ () (bind (f) g)))))))
+
+(define-syntax conde
+  (syntax-rules ()
+    ((_ (g0 g ...) (g1 g^ ...) ...)
+     (lambdag@ (s) 
+       (inc 
+         (mplus* 
+           (bind* (g0 s) g ...)
+           (bind* (g1 s) g^ ...) ...))))))
+ 
+(define-syntax mplus*
+  (syntax-rules ()
+    ((_ e) e)
+    ((_ e0 e ...) (mplus e0 
+                    (lambdaf@ () (mplus* e ...))))))
+ 
+(define mplus
+  (lambda (a-inf f)
+    (case-inf a-inf
+      (() (f))
+      ((f^) (inc (mplus (f) f^)))
+      ((a) (choice a f))
+      ((a f^) (choice a (lambdaf@ () (mplus (f) f^)))))))
+
+(define-syntax conda
+  (syntax-rules ()
+    ((_ (g0 g ...) (g1 g^ ...) ...)
+     (lambdag@ (s)
+       (inc
+         (ifa ((g0 s) g ...)
+              ((g1 s) g^ ...) ...))))))
+ 
+(define-syntax ifa
+  (syntax-rules ()
+    ((_) (mzero))
+    ((_ (e g ...) b ...)
+     (let loop ((a-inf e))
+       (case-inf a-inf
+         (() (ifa b ...))
+         ((f) (inc (loop (f))))
+         ((a) (bind* a-inf g ...))
+         ((a f) (bind* a-inf g ...)))))))
+
+(define-syntax condu
+  (syntax-rules ()
+    ((_ (g0 g ...) (g1 g^ ...) ...)
+     (lambdag@ (s)
+       (inc
+         (ifu ((g0 s) g ...)
+              ((g1 s) g^ ...) ...))))))
+ 
+(define-syntax ifu
+  (syntax-rules ()
+    ((_) (mzero))
+    ((_ (e g ...) b ...)
+     (let loop ((a-inf e))
+       (case-inf a-inf
+         (() (ifu b ...))
+         ((f) (inc (loop (f))))
+         ((a) (bind* a-inf g ...))
+         ((a f) (bind* (unit a) g ...)))))))
+
+(define-syntax project
+  (syntax-rules ()
+    ((_ (x ...) g g* ...)
+     (lambdag@ (s)
+       (let ((x (walk* x s)) ...)
+         ((fresh () g g* ...) s))))))
+
+(define succeed (== #f #f))
+
+(define fail (== #f #t))
+
+(define onceo
+  (lambda (g)
+    (condu
+      (g succeed)
+      ((== #f #f) fail))))
diff --git a/scheme/mkdefs.scm b/scheme/mkdefs.scm
new file mode 100644
index 0000000..10ee052
--- /dev/null
+++ b/scheme/mkdefs.scm
@@ -0,0 +1,418 @@
+
+; miniKanren prelude from simple-miniKanren
+
+; https://minikanren.org
+; https://github.com/miniKanren/simple-miniKanren
+
+
+(define-syntax run1 (syntax-rules () ((_ (x) g0 g ...) (run 1 (x) g0 g ...))))
+(define-syntax run2 (syntax-rules () ((_ (x) g0 g ...) (run 2 (x) g0 g ...))))
+(define-syntax run3 (syntax-rules () ((_ (x) g0 g ...) (run 3 (x) g0 g ...))))
+(define-syntax run4 (syntax-rules () ((_ (x) g0 g ...) (run 4 (x) g0 g ...))))
+(define-syntax run5 (syntax-rules () ((_ (x) g0 g ...) (run 5 (x) g0 g ...))))
+(define-syntax run6 (syntax-rules () ((_ (x) g0 g ...) (run 6 (x) g0 g ...))))
+(define-syntax run7 (syntax-rules () ((_ (x) g0 g ...) (run 7 (x) g0 g ...))))
+(define-syntax run8 (syntax-rules () ((_ (x) g0 g ...) (run 8 (x) g0 g ...))))
+(define-syntax run9 (syntax-rules () ((_ (x) g0 g ...) (run 9 (x) g0 g ...))))
+(define-syntax run10 (syntax-rules () ((_ (x) g0 g ...) (run 10 (x) g0 g ...))))
+
+(define-syntax run11 (syntax-rules () ((_ (x) g0 g ...) (run 11 (x) g0 g ...))))
+(define-syntax run12 (syntax-rules () ((_ (x) g0 g ...) (run 12 (x) g0 g ...))))
+(define-syntax run13 (syntax-rules () ((_ (x) g0 g ...) (run 13 (x) g0 g ...))))
+(define-syntax run14 (syntax-rules () ((_ (x) g0 g ...) (run 14 (x) g0 g ...))))
+(define-syntax run15 (syntax-rules () ((_ (x) g0 g ...) (run 15 (x) g0 g ...))))
+(define-syntax run16 (syntax-rules () ((_ (x) g0 g ...) (run 16 (x) g0 g ...))))
+(define-syntax run17 (syntax-rules () ((_ (x) g0 g ...) (run 17 (x) g0 g ...))))
+(define-syntax run18 (syntax-rules () ((_ (x) g0 g ...) (run 18 (x) g0 g ...))))
+(define-syntax run19 (syntax-rules () ((_ (x) g0 g ...) (run 19 (x) g0 g ...))))
+(define-syntax run20 (syntax-rules () ((_ (x) g0 g ...) (run 20 (x) g0 g ...))))
+
+(define-syntax run21 (syntax-rules () ((_ (x) g0 g ...) (run 21 (x) g0 g ...))))
+(define-syntax run22 (syntax-rules () ((_ (x) g0 g ...) (run 22 (x) g0 g ...))))
+(define-syntax run23 (syntax-rules () ((_ (x) g0 g ...) (run 23 (x) g0 g ...))))
+(define-syntax run24 (syntax-rules () ((_ (x) g0 g ...) (run 24 (x) g0 g ...))))
+(define-syntax run25 (syntax-rules () ((_ (x) g0 g ...) (run 25 (x) g0 g ...))))
+(define-syntax run26 (syntax-rules () ((_ (x) g0 g ...) (run 26 (x) g0 g ...))))
+(define-syntax run27 (syntax-rules () ((_ (x) g0 g ...) (run 27 (x) g0 g ...))))
+(define-syntax run28 (syntax-rules () ((_ (x) g0 g ...) (run 28 (x) g0 g ...))))
+(define-syntax run29 (syntax-rules () ((_ (x) g0 g ...) (run 29 (x) g0 g ...))))
+(define-syntax run30 (syntax-rules () ((_ (x) g0 g ...) (run 30 (x) g0 g ...))))
+
+(define-syntax run31 (syntax-rules () ((_ (x) g0 g ...) (run 31 (x) g0 g ...))))
+(define-syntax run32 (syntax-rules () ((_ (x) g0 g ...) (run 32 (x) g0 g ...))))
+(define-syntax run33 (syntax-rules () ((_ (x) g0 g ...) (run 33 (x) g0 g ...))))
+(define-syntax run34 (syntax-rules () ((_ (x) g0 g ...) (run 34 (x) g0 g ...))))
+(define-syntax run35 (syntax-rules () ((_ (x) g0 g ...) (run 35 (x) g0 g ...))))
+(define-syntax run36 (syntax-rules () ((_ (x) g0 g ...) (run 36 (x) g0 g ...))))
+(define-syntax run37 (syntax-rules () ((_ (x) g0 g ...) (run 37 (x) g0 g ...))))
+(define-syntax run38 (syntax-rules () ((_ (x) g0 g ...) (run 38 (x) g0 g ...))))
+(define-syntax run39 (syntax-rules () ((_ (x) g0 g ...) (run 39 (x) g0 g ...))))
+(define-syntax run40 (syntax-rules () ((_ (x) g0 g ...) (run 40 (x) g0 g ...))))
+
+(define caro
+  (lambda (p a)
+    (fresh (d)
+      (== (cons a d) p))))
+
+(define cdro
+  (lambda (p d)
+    (fresh (a)
+      (== (cons a d) p))))
+
+(define conso
+  (lambda (a d p)
+    (== (cons a d) p)))
+
+(define nullo
+  (lambda (x)
+    (== '() x)))
+
+(define eqo
+  (lambda (x y)
+    (== x y)))
+
+(define pairo
+  (lambda (p)
+    (fresh (a d)
+      (conso a d p))))
+
+(define membero
+  (lambda (x l)
+    (conde      
+      ((fresh (a)
+         (caro l a)
+         (== a x)))
+      ((fresh (d)
+         (cdro l d)
+         (membero x d))))))
+
+(define rembero
+  (lambda (x l out)
+    (conde
+      ((nullo l) (== '() out))
+      ((caro l x) (cdro l out))
+      ((fresh (a d res)
+         (conso a d l)
+         (rembero x d res)
+         (conso a res out))))))
+
+(define appendo
+  (lambda (l s out)
+    (conde
+      ((nullo l) (== s out))
+      ((fresh (a d res)
+         (conso a d l)
+         (conso a res out)
+         (appendo d s res))))))
+
+(define flatteno
+  (lambda (s out)
+    (conde
+      ((nullo s) (== '() out))
+      ((pairo s)
+       (fresh (a d res-a res-d)
+         (conso a d s)
+         (flatteno a res-a)
+         (flatteno d res-d)
+         (appendo res-a res-d out)))
+      ((conso s '() out)))))
+
+(define anyo
+  (lambda (g)
+    (conde
+      (g)
+      ((anyo g)))))
+
+(define nevero (anyo fail))
+(define alwayso (anyo succeed))
+
+
+
+(define build-num
+  (lambda (n)
+    (cond
+      ((odd? n)
+       (cons 1
+         (build-num (quotient (- n 1) 2))))    
+      ((and (not (zero? n)) (even? n))
+       (cons 0
+         (build-num (quotient n 2))))
+      ((zero? n) '()))))
+
+(define poso
+  (lambda (n)
+    (fresh (a d)
+      (== `(,a . ,d) n))))
+
+(define >1o
+  (lambda (n)
+    (fresh (a ad dd)
+      (== `(,a ,ad . ,dd) n))))
+
+(define full-addero
+  (lambda (b x y r c)
+    (conde
+      ((== 0 b) (== 0 x) (== 0 y) (== 0 r) (== 0 c))
+      ((== 1 b) (== 0 x) (== 0 y) (== 1 r) (== 0 c))
+      ((== 0 b) (== 1 x) (== 0 y) (== 1 r) (== 0 c))
+      ((== 1 b) (== 1 x) (== 0 y) (== 0 r) (== 1 c))
+      ((== 0 b) (== 0 x) (== 1 y) (== 1 r) (== 0 c))
+      ((== 1 b) (== 0 x) (== 1 y) (== 0 r) (== 1 c))
+      ((== 0 b) (== 1 x) (== 1 y) (== 0 r) (== 1 c))
+      ((== 1 b) (== 1 x) (== 1 y) (== 1 r) (== 1 c)))))
+
+(define addero
+  (lambda (d n m r)
+    (conde
+      ((== 0 d) (== '() m) (== n r))
+      ((== 0 d) (== '() n) (== m r)
+       (poso m))
+      ((== 1 d) (== '() m)
+       (addero 0 n '(1) r))
+      ((== 1 d) (== '() n) (poso m)
+       (addero 0 '(1) m r))
+      ((== '(1) n) (== '(1) m)
+       (fresh (a c)
+         (== `(,a ,c) r)
+         (full-addero d 1 1 a c)))
+      ((== '(1) n) (gen-addero d n m r))
+      ((== '(1) m) (>1o n) (>1o r)
+       (addero d '(1) n r))
+      ((>1o n) (gen-addero d n m r)))))
+
+(define gen-addero
+  (lambda (d n m r)
+    (fresh (a b c e x y z)
+      (== `(,a . ,x) n)
+      (== `(,b . ,y) m) (poso y)
+      (== `(,c . ,z) r) (poso z)
+      (full-addero d a b c e)
+      (addero e x y z))))
+
+(define pluso
+  (lambda (n m k)
+    (addero 0 n m k)))
+
+(define minuso
+  (lambda (n m k)
+    (pluso m k n)))
+
+(define *o
+  (lambda (n m p)
+    (conde
+      ((== '() n) (== '() p))
+      ((poso n) (== '() m) (== '() p))  
+      ((== '(1) n) (poso m) (== m p))   
+      ((>1o n) (== '(1) m) (== n p))
+      ((fresh (x z)
+         (== `(0 . ,x) n) (poso x)
+         (== `(0 . ,z) p) (poso z)
+         (>1o m)
+         (*o x m z)))
+      ((fresh (x y)
+         (== `(1 . ,x) n) (poso x)
+         (== `(0 . ,y) m) (poso y)
+         (*o m n p)))
+      ((fresh (x y)
+         (== `(1 . ,x) n) (poso x)      
+         (== `(1 . ,y) m) (poso y)
+         (odd-*o x n m p))))))
+
+(define odd-*o
+  (lambda (x n m p)
+    (fresh (q)
+      (bound-*o q p n m)
+      (*o x m q)
+      (pluso `(0 . ,q) m p))))
+
+(define bound-*o
+  (lambda (q p n m)
+    (conde
+      ((nullo q) (pairo p))
+      ((fresh (x y z)
+         (cdro q x)
+         (cdro p y)
+         (conde
+           ((nullo n)
+            (cdro m z)
+            (bound-*o x y z '()))
+           ((cdro n z) 
+            (bound-*o x y z m))))))))
+
+(define =lo
+  (lambda (n m)
+    (conde
+      ((== '() n) (== '() m))
+      ((== '(1) n) (== '(1) m))
+      ((fresh (a x b y)
+         (== `(,a . ,x) n) (poso x)
+         (== `(,b . ,y) m) (poso y)
+         (=lo x y))))))
+
+(define <lo
+  (lambda (n m)
+    (conde
+      ((== '() n) (poso m))
+      ((== '(1) n) (>1o m))
+      ((fresh (a x b y)
+         (== `(,a . ,x) n) (poso x)
+         (== `(,b . ,y) m) (poso y)
+         (<lo x y))))))
+
+(define <=lo
+  (lambda (n m)
+    (conde
+      ((=lo n m))
+      ((<lo n m)))))
+
+(define <o
+  (lambda (n m)
+    (conde
+      ((<lo n m))
+      ((=lo n m)
+       (fresh (x)
+         (poso x)
+         (pluso n x m))))))
+
+(define <=o
+  (lambda (n m)
+    (conde
+      ((== n m))
+      ((<o n m)))))
+
+(define /o
+  (lambda (n m q r)
+    (conde
+      ((== r n) (== '() q) (<o n m))
+      ((== '(1) q) (=lo n m) (pluso r m n)
+       (<o r m))
+      ((<lo m n)                        
+       (<o r m)                        
+       (poso q)                 
+       (fresh (nh nl qh ql qlm qlmr rr rh)
+         (splito n r nl nh)
+         (splito q r ql qh)
+         (conde
+           ((== '() nh)
+            (== '() qh)
+            (minuso nl r qlm)
+            (*o ql m qlm))
+           ((poso nh)
+            (*o ql m qlm)
+            (pluso qlm r qlmr)
+            (minuso qlmr nl rr)
+            (splito rr r '() rh)
+            (/o nh m qh rh))))))))
+
+(define splito
+  (lambda (n r l h)
+    (conde
+      ((== '() n) (== '() h) (== '() l))
+      ((fresh (b n^)
+         (== `(0 ,b . ,n^) n)
+         (== '() r)
+         (== `(,b . ,n^) h)
+         (== '() l)))
+      ((fresh (n^)
+         (==  `(1 . ,n^) n)
+         (== '() r)
+         (== n^ h)
+         (== '(1) l)))
+      ((fresh (b n^ a r^)
+         (== `(0 ,b . ,n^) n)
+         (== `(,a . ,r^) r)
+         (== '() l)
+         (splito `(,b . ,n^) r^ '() h)))
+      ((fresh (n^ a r^)
+         (== `(1 . ,n^) n)
+         (== `(,a . ,r^) r)
+         (== '(1) l)
+         (splito n^ r^ '() h)))
+      ((fresh (b n^ a r^ l^)
+         (== `(,b . ,n^) n)
+         (== `(,a . ,r^) r)
+         (== `(,b . ,l^) l)
+         (poso l^)
+         (splito n^ r^ l^ h))))))
+
+(define logo
+ (lambda (n b q r)
+   (conde
+     ((== '(1) n) (poso b) (== '() q) (== '() r))
+     ((== '() q) (<o n b) (pluso r '(1) n))
+     ((== '(1) q) (>1o b) (=lo n b) (pluso r b n))
+     ((== '(1) b) (poso q) (pluso r '(1) n))
+     ((== '() b) (poso q) (== r n))
+     ((== '(0 1) b)
+      (fresh (a ad dd)
+        (poso dd)
+        (== `(,a ,ad . ,dd) n)
+        (exp2 n '() q)
+        (fresh (s)
+          (splito n dd r s))))
+     ((fresh (a ad add ddd)
+        (conde
+          ((== '(1 1) b))
+          ((== `(,a ,ad ,add . ,ddd) b))))
+      (<lo b n)
+      (fresh (bw1 bw nw nw1 ql1 ql s)
+        (exp2 b '() bw1)
+        (pluso bw1 '(1) bw)
+        (<lo q n)
+        (fresh (q1 bwq1)
+          (pluso q '(1) q1)
+          (*o bw q1 bwq1)
+          (<o nw1 bwq1))
+          (exp2 n '() nw1)
+          (pluso nw1 '(1) nw)
+          (/o nw bw ql1 s)
+          (pluso ql '(1) ql1)
+          (<=lo ql q)
+          (fresh (bql qh s qdh qd)
+            (repeated-mul b ql bql)
+            (/o nw bw1 qh s)
+            (pluso ql qdh qh)
+            (pluso ql qd q)
+            (<=o qd qdh)
+            (fresh (bqd bq1 bq)
+              (repeated-mul b qd bqd)
+              (*o bql bqd bq)
+              (*o b bq bq1)
+              (pluso bq r n)
+              (<o n bq1))))))))
+
+(define exp2
+  (lambda (n b q)
+    (conde
+      ((== '(1) n) (== '() q))
+      ((>1o n) (== '(1) q)
+       (fresh (s)
+         (splito n b s '(1))))
+      ((fresh (q1 b2)
+         (== `(0 . ,q1) q)
+         (poso q1)
+         (<lo b n)
+         (appendo b `(1 . ,b) b2)
+         (exp2 n b2 q1)))
+      ((fresh (q1 nh b2 s)
+         (== `(1 . ,q1) q)
+         (poso q1)
+         (poso nh)
+         (splito n b s nh)
+         (appendo b `(1 . ,b) b2)
+         (exp2 nh b2 q1))))))
+
+(define repeated-mul
+  (lambda (n q nq)
+    (conde
+      ((poso n) (== '() q) (== '(1) nq))
+      ((== '(1) q) (== n nq))
+      ((>1o q)
+       (fresh (q1 nq1)
+         (pluso q1 '(1) q)
+         (repeated-mul n q1 nq1)
+         (*o nq1 n nq))))))
+
+(define expo
+  (lambda (b q n)
+    (logo n b q '())))
diff --git a/scheme/refresh.sh b/scheme/refresh.sh
new file mode 100755
index 0000000..e38b99f
--- /dev/null
+++ b/scheme/refresh.sh
@@ -0,0 +1,16 @@
+#!/bin/bash
+
+
+# Script that resets Scheme compilation to facilitate switching between mini and micro.
+# Don't need to recompile mk.scm and uk.scm since they don't depend on anything.
+
+#touch mk.scm
+touch mkdefs.scm
+
+#touch uk.scm
+
+touch houses.scm
+touch logo.scm
+touch zebra.scm
+
+
diff --git a/scheme/uk.scm b/scheme/uk.scm
new file mode 100644
index 0000000..6d2a0f4
--- /dev/null
+++ b/scheme/uk.scm
@@ -0,0 +1,140 @@
+
+; microKanren core from 2013 microKanren paper
+
+; http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf
+
+
+(import (rnrs lists))
+
+
+(define (var c) (vector c))
+(define (var? x) (vector? x))
+(define (var=? x1 x2) (= (vector-ref x1 0) (vector-ref x2 0)))
+
+(define (walk u s)
+  (let ((pr (and (var? u) (assp (lambda (v) (var=? u v)) s))))
+    (if pr (walk (cdr pr) s) u)))
+
+(define (ext-s x v s) `((,x . ,v) . ,s))
+
+(define (== u v)
+  (lambda (sc)
+    (let ((s (unify u v (car sc))))
+      (if s (unit `(,s . ,(cdr sc))) mzero))))
+
+(define (unit sc) (cons sc mzero))
+(define mzero '())
+
+(define (unify u v s)
+  (let ((u (walk u s))
+        (v (walk v s)))
+    (cond
+      ((and (var? u) (var? v) (var=? u v)) s)
+      ((var? u) (ext-s u v s))
+      ((var? v) (ext-s v u s))
+      ((and (pair? u) (pair? v))
+        (let ((s (unify (car u) (car v) s)))
+          (and s (unify (cdr u) (cdr v) s))))
+      (else (and (eqv? u v) s)))))
+
+(define (call/fresh f)
+  (lambda (sc)
+    (let ((c (cdr sc)))
+      ((f (var c)) `(,(car sc) . ,(+ c 1))))))
+
+(define (disj g1 g2) (lambda (sc) (mplus (g1 sc) (g2 sc))))
+(define (conj g1 g2) (lambda (sc) (bind (g1 sc) g2)))
+
+(define (mplus s1 s2)
+  (cond
+    ((null? s1) s2)
+    ((procedure? s1) (lambda () (mplus s2 (s1))))
+    (else (cons (car s1) (mplus (cdr s1) s2)))))
+
+(define (bind s g)
+  (cond
+    ((null? s) mzero)
+    ((procedure? s) (lambda () (bind (s) g)))
+    (else (mplus (g (car s)) (bind (cdr s) g)))))
+
+(define-syntax zzz
+  (syntax-rules ()
+    ((_ g) (lambda (sc) (lambda () (g sc))))))
+
+(define-syntax conj+
+  (syntax-rules ()
+    ((_ g) (zzz g))
+    ((_ g0 g ...) (conj (zzz g0) (conj+ g ...)))))
+
+(define-syntax disj+
+  (syntax-rules ()
+    ((_ g) (zzz g))
+    ((_ g0 g ...) (disj (zzz g0) (disj+ g ...)))))
+
+(define-syntax conde
+  (syntax-rules ()
+    ((_ (g0 g ...) ...) (disj+ (conj+ g0 g ...) ...))))
+
+(define-syntax fresh
+  (syntax-rules ()
+    ((_ () g0 g ...) (conj+ g0 g ...))
+    ((_ (x0 x ...) g0 g ...)
+      (call/fresh (lambda (x0) (fresh (x ...) g0 g ...))))))
+
+(define (pull s) (if (procedure? s) (pull (s)) s))
+
+(define (take-all s)
+  (let ((s (pull s)))
+    (if (null? s) '() (cons (car s) (take-all (cdr s))))))
+
+(define (take n s)
+  (if (zero? n) '()
+    (let ((s (pull s)))
+      (cond
+        ((null? s) '())
+        (else (cons (car s) (take (- n 1) (cdr s))))))))
+
+(define (mk-reify sc*)
+  (map reify-state/1st-var sc*))
+
+(define (reify-state/1st-var sc)
+  (let ((v (walk* (var 0) (car sc))))
+    (walk* v (reify-s v '()))))
+
+(define (reify-s v s)
+  (let ((v (walk v s)))
+    (cond
+      ((var? v)
+        (let ((n (reify-name (length s))))
+          (cons `(,v . ,n) s)))
+      ((pair? v) (reify-s (cdr v) (reify-s (car v) s)))
+      (else s))))
+
+(define (reify-name n)
+  (string->symbol
+    (string-append "_" "." (number->string n))))
+
+(define (walk* v s)
+  (let ((v (walk v s)))
+    (cond
+      ((var? v) v)
+      ((pair? v) (cons (walk* (car v) s) (walk* (cdr v) s)))
+      (else v))))
+
+(define empty-state '(() . 0))
+(define (call/empty-state g) (g empty-state))
+
+(define-syntax run
+  (syntax-rules ()
+    ((_ n (x ...) g0 g ...)
+      (mk-reify (take n (call/empty-state (fresh (x ...) g0 g ...)))))))
+
+(define-syntax run*
+  (syntax-rules ()
+    ((_ (x ...) g0 g ...)
+      (mk-reify (take-all (call/empty-state (fresh (x ...) g0 g ...)))))))
+
+(define succeed (== #f #f))
+(define fail (== #f #t))
+
+
diff --git a/scheme/zebra-mk.sh b/scheme/zebra-mk.sh
new file mode 100755
index 0000000..24e1b4b
--- /dev/null
+++ b/scheme/zebra-mk.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+
+/usr/bin/env -S guile -e run-zebra -l "mk.scm" -l "mkdefs.scm" -s "zebra.scm"
+
+
diff --git a/scheme/zebra-uk.sh b/scheme/zebra-uk.sh
new file mode 100755
index 0000000..6a891ad
--- /dev/null
+++ b/scheme/zebra-uk.sh
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+
+/usr/bin/env -S guile -e run-zebra -l "uk.scm" -l "mkdefs.scm" -s "zebra.scm"
+
+
diff --git a/scheme/zebra.scm b/scheme/zebra.scm
new file mode 100644
index 0000000..9ba0fea
--- /dev/null
+++ b/scheme/zebra.scm
@@ -0,0 +1,54 @@
+
+; Equivalent to example/zebra.adb
+
+
+(define (on-right l r li)
+  (conde
+    ((fresh (z)
+      (caro li l)
+      (cdro li z)
+      (caro z r)))
+    ((fresh (z)
+      (cdro li z)
+      (on-right l r z)))))
+
+
+(define (next-to l r li)
+  (conde
+    ((on-right l r li))
+    ((on-right r l li))))
+
+
+(define (zebra h)
+  (fresh (a b c d e)
+    (== h `(,a ,b ,c ,d ,e))
+    (fresh (w x y z) (== a `(norwegian ,w ,x ,y ,z)))
+    (fresh (w x y z) (== c `(,w ,x milk ,y ,z)))
+
+    (fresh (x y z) (membero `(englishman ,x ,y ,z red) h))
+    (fresh (x y z) (membero `(,x kools ,y ,z yellow) h))
+    (fresh (x y z) (membero `(spaniard ,x ,y dog ,z) h))
+    (fresh (x y z) (membero `(,x ,y coffee ,z green) h))
+    (fresh (x y z) (membero `(ukrainian ,x tea ,y ,z) h))
+    (fresh (x y z) (membero `(,x luckystrikes oj ,y ,z) h))
+    (fresh (x y z) (membero `(japanese parliaments ,x ,y ,z) h))
+    (fresh (x y z) (membero `(,x oldgolds ,y snails ,z) h))
+
+    (fresh (s t u v w x y z) (on-right `(,s ,t ,u ,v ivory) `(,w ,x ,y ,z green) h))
+
+    (fresh (s t u v w x y z) (next-to `(norwegian ,s ,t ,u ,v) `(,w ,x ,y ,z blue) h))
+    (fresh (s t u v w x y z) (next-to `(,s ,t ,u horse ,v) `(,w kools ,x ,y ,z) h))
+    (fresh (s t u v w x y z) (next-to `(,s ,t ,u fox ,v) `(,w chesterfields ,x ,y ,z) h))
+
+    (fresh (w x y z) (membero `(,w ,x water ,y ,z) h))
+    (fresh (w x y z) (membero `(,w ,x ,y zebra ,z) h))))
+
+
+(define (run-zebra args)
+  (let* ((s (run 1 (h) (zebra h))))
+    (for-each
+      (lambda (x)
+        (begin (display x) (newline)))
+      (car s))))
+
+