diff options
Diffstat (limited to 'scheme/mk.scm')
| -rw-r--r-- | scheme/mk.scm | 269 |
1 files changed, 269 insertions, 0 deletions
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)))) |