diff options
| -rw-r--r-- | readme.md | 7 | ||||
| -rwxr-xr-x | scheme/houses-mk.sh | 6 | ||||
| -rwxr-xr-x | scheme/houses-uk.sh | 6 | ||||
| -rw-r--r-- | scheme/houses.scm | 42 | ||||
| -rwxr-xr-x | scheme/logo-mk.sh | 6 | ||||
| -rwxr-xr-x | scheme/logo-uk.sh | 6 | ||||
| -rw-r--r-- | scheme/logo.scm | 52 | ||||
| -rw-r--r-- | scheme/mk.scm | 269 | ||||
| -rw-r--r-- | scheme/mkdefs.scm | 418 | ||||
| -rwxr-xr-x | scheme/refresh.sh | 16 | ||||
| -rw-r--r-- | scheme/uk.scm | 140 | ||||
| -rwxr-xr-x | scheme/zebra-mk.sh | 6 | ||||
| -rwxr-xr-x | scheme/zebra-uk.sh | 6 | ||||
| -rw-r--r-- | scheme/zebra.scm | 22 |
14 files changed, 74 insertions, 928 deletions
@@ -110,12 +110,7 @@ bindings are easy to do when backtracking during the depth-first search. #### Credits and Licensing -The `mk.scm` and `mkdefs.scm` files in the `scheme` benchmarking comparison -subdirectory are taken from [simple-miniKanren](https://github.com/miniKanren/simple-miniKanren). -The `uk.scm` file is collected code snippets from the -[2013 microKanren paper](http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf). - -Everything else written by Jedidiah Barber. +Written by Jedidiah Barber. Licensed under the Sunset License v1.0. For details see `license.txt`. diff --git a/scheme/houses-mk.sh b/scheme/houses-mk.sh deleted file mode 100755 index c2045d6..0000000 --- a/scheme/houses-mk.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/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 deleted file mode 100755 index d17893b..0000000 --- a/scheme/houses-uk.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/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 index 8178bf5..40dadc5 100644 --- a/scheme/houses.scm +++ b/scheme/houses.scm @@ -2,6 +2,16 @@ ; Equivalent to example/houses.adb + +; Place contents of mk.scm from simple-miniKanren here. +; An equivalent microKanren implementation such as from the 2013 paper will also work. + + +; Place contents of mkdefs.scm from simple-miniKanren here. +; Be sure to leave out the (load "mk.scm") line. + + + (define (value bin) (cond ((null? bin) 0) @@ -64,21 +74,21 @@ (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)))) +; Main program +(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 deleted file mode 100755 index f53f976..0000000 --- a/scheme/logo-mk.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/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 deleted file mode 100755 index cda4aa7..0000000 --- a/scheme/logo-uk.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/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 index 18fc9ed..fee72f7 100644 --- a/scheme/logo.scm +++ b/scheme/logo.scm @@ -2,6 +2,16 @@ ; Equivalent to test/logo.adb + +; Place contents of mk.scm from simple-miniKanren here. +; An equivalent microKanren implementation such as from the 2013 paper will also work. + + +; Place contents of mkdefs.scm from simple-miniKanren here. +; Be sure to leave out the (load "mk.scm") line. + + + (define (value bin) (cond ((null? bin) 0) @@ -24,26 +34,26 @@ (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))) +; Main program +(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 deleted file mode 100644 index 9917284..0000000 --- a/scheme/mk.scm +++ /dev/null @@ -1,269 +0,0 @@ - -; 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 deleted file mode 100644 index 10ee052..0000000 --- a/scheme/mkdefs.scm +++ /dev/null @@ -1,418 +0,0 @@ - -; 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 deleted file mode 100755 index e38b99f..0000000 --- a/scheme/refresh.sh +++ /dev/null @@ -1,16 +0,0 @@ -#!/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 deleted file mode 100644 index 6d2a0f4..0000000 --- a/scheme/uk.scm +++ /dev/null @@ -1,140 +0,0 @@ - -; 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 deleted file mode 100755 index 24e1b4b..0000000 --- a/scheme/zebra-mk.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/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 deleted file mode 100755 index 6a891ad..0000000 --- a/scheme/zebra-uk.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/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 index 9ba0fea..f33eba8 100644 --- a/scheme/zebra.scm +++ b/scheme/zebra.scm @@ -2,6 +2,16 @@ ; Equivalent to example/zebra.adb + +; Place contents of mk.scm from simple-miniKanren here. +; An equivalent microKanren implementation such as from the 2013 paper will also work. + + +; Place contents of mkdefs.scm from simple-miniKanren here. +; Be sure to leave out the (load "mk.scm") line. + + + (define (on-right l r li) (conde ((fresh (z) @@ -44,11 +54,11 @@ (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)))) +; Main program +(let* ((s (run 1 (h) (zebra h)))) + (for-each + (lambda (x) + (begin (display x) (newline))) + (car s))) |