codepad
[
create a new paste
]
login
|
about
Language:
C
C++
D
Haskell
Lua
OCaml
PHP
Perl
Plain Text
Python
Ruby
Scheme
Tcl
;;; Code that accompanies ``The Reasoned Schemer'' ;;; Daniel P. Friedman, William E. Byrd and Oleg Kiselyov ;;; MIT Press, Cambridge, MA, 2005 ;;; ;;; The implementation of the logic system used in the (2nd printing) of ;;; the book. ;;; This file was generated by writeminikanren.pl ;;; Generated at 2006-02-01 18:26:02 (define-syntax lambdag@ (syntax-rules () ((_ (s) e) (lambda (s) e)))) (define-syntax lambdaf@ (syntax-rules () ((_ () e) (lambda () e)))) (define-syntax rhs (syntax-rules () ((rhs p) (cdr p)))) (define-syntax lhs (syntax-rules () ((lhs p) (car p)))) (define-syntax var (syntax-rules () ((var w) (vector w)))) (define-syntax var? (syntax-rules () ((var? w) (vector? w)))) (define-syntax size-s (syntax-rules () ((size-s ls) (length ls)))) (define empty-s '()) (define walk (lambda (v s) (cond ((var? v) (cond ((assq v s) => (lambda (a) (let ((v^ (rhs a))) (walk v^ s)))) (else v))) (else v)))) (define ext-s (lambda (x v s) (cons `(,x . ,v) s))) (define unify (lambda (v w s) (let ((v (walk v s)) (w (walk w s))) (cond ((eq? v w) s) ((var? v) (ext-s v w s)) ((var? w) (ext-s w v s)) ((and (pair? v) (pair? w)) (cond ((unify (car v) (car w) s) => (lambda (s) (unify (cdr v) (cdr w) s))) (else #f))) ((equal? v w) 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 unify-check (lambda (v w s) (let ((v (walk v s)) (w (walk w s))) (cond ((eq? v w) s) ((var? v) (ext-s-check v w s)) ((var? w) (ext-s-check w v s)) ((and (pair? v) (pair? w)) (cond ((unify-check (car v) (car w) s) => (lambda (s) (unify-check (cdr v) (cdr w) s))) (else #f))) ((equal? v w) s) (else #f))))) (define walk* (lambda (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 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) (walk* v (reify-s v empty-s)))) (define-syntax run (syntax-rules () ((_ n^ (x) g ...) (let ((n n^) (x (var 'x))) (if (or (not n) (> n 0)) (map-inf n (lambda (s) (reify (walk* x s))) ((all g ...) empty-s)) '()))))) (define-syntax case-inf (syntax-rules () ((_ e on-zero ((a^) on-one) ((a f) on-choice)) (let ((a-inf e)) (cond ((not a-inf) on-zero) ((not (and (pair? a-inf) (procedure? (cdr a-inf)))) (let ((a^ a-inf)) on-one)) (else (let ((a (car a-inf)) (f (cdr a-inf))) on-choice))))))) (define-syntax mzero (syntax-rules () ((_) #f))) (define-syntax unit (syntax-rules () ((_ a) a))) (define-syntax choice (syntax-rules () ((_ a f) (cons a f)))) (define map-inf (lambda (n p a-inf) (case-inf a-inf '() ((a) (cons (p a) '())) ((a f) (cons (p a) (cond ((not n) (map-inf n p (f))) ((> n 1) (map-inf (- n 1) p (f))) (else '()))))))) (define == (lambda (v w) (lambdag@ (s) (cond ((unify v w s) => succeed) (else (fail s)))))) (define ==-check (lambda (v w) (lambdag@ (s) (cond ((unify-check v w s) => succeed) (else (fail s)))))) (define-syntax fresh (syntax-rules () ((_ (x ...) g ...) (lambdag@ (s) (let ((x (var 'x)) ...) ((all g ...) s)))))) (define-syntax all (syntax-rules () ((_) succeed) ((_ g) (lambdag@ (s) (g s))) ((_ g^ g ...) (lambdag@ (s) (bind (g^ s) (all g ...)))))) (define-syntax conde (syntax-rules (else) ((_) fail) ((_ (else g0 g ...)) (all g0 g ...)) ((_ (g0 g ...) c ...) (anye (all g0 g ...) (conde c ...))))) (define succeed (lambdag@ (s) (unit s))) (define fail (lambdag@ (s) (mzero))) (define bind (lambda (a-inf g) (case-inf a-inf (mzero) ((a) (g a)) ((a f) (mplus (g a) (lambdaf@ () (bind (f) g))))))) (define mplus (lambda (a-inf f) (case-inf a-inf (f) ((a) (choice a f)) ((a f0) (choice a (lambdaf@ () (mplus (f0) f))))))) (define-syntax anye (syntax-rules () ((_ g1 g2) (lambdag@ (s) (mplus (g1 s) (lambdaf@ () (g2 s))))))) (define-syntax alli (syntax-rules () ((_) succeed) ((_ g) (lambdag@ (s) (g s))) ((_ g^ g ...) (lambdag@ (s) (bindi (g^ s) (alli g ...)))))) (define-syntax condi (syntax-rules (else) ((_) fail) ((_ (else g0 g ...)) (all g0 g ...)) ((_ (g0 g ...) c ...) (anyi (all g0 g ...) (condi c ...))))) (define-syntax anyi (syntax-rules () ((_ g1 g2) (lambdag@ (s) (mplusi (g1 s) (lambdaf@ () (g2 s))))))) (define bindi (lambda (a-inf g) (case-inf a-inf (mzero) ((a) (g a)) ((a f) (mplusi (g a) (lambdaf@ () (bindi (f) g))))))) (define mplusi (lambda (a-inf f) (case-inf a-inf (f) ((a) (choice a f)) ((a f0) (choice a (lambdaf@ () (mplusi (f) f0))))))) (define-syntax conda (syntax-rules (else) ((_) fail) ((_ (else g0 g ...)) (all g0 g ...)) ((_ (g0 g ...) c ...) (ifa g0 (all g ...) (conda c ...))))) (define-syntax condu (syntax-rules (else) ((_) fail) ((_ (else g0 g ...)) (all g0 g ...)) ((_ (g0 g ...) c ...) (ifu g0 (all g ...) (condu c ...))))) (define-syntax ifa (syntax-rules () ((_ g0 g1 g2) (lambdag@ (s) (let ((s-inf (g0 s)) (g^ g1)) (case-inf s-inf (g2 s) ((s) (g^ s)) ((s f) (bind s-inf g^)))))))) (define-syntax ifu (syntax-rules () ((_ g0 g1 g2) (lambdag@ (s) (let ((s-inf (g0 s)) (g^ g1)) (case-inf s-inf (g2 s) ((s) (g^ s)) ((s f) (g^ s)))))))) (define-syntax run* (syntax-rules () ((_ (x) g ...) (run #f (x) g ...)))) (define-syntax lambda-limited (syntax-rules () ((_ n formals g) (let ((x (var 'x))) (lambda formals (ll n x g)))))) (define ll (lambda (n x g) (lambdag@ (s) (let ((v (walk x s))) (cond ((var? v) (g (ext-s x 1 s))) ((< v n) (g (ext-s x (+ v 1) s))) (else (fail s))))))) (define-syntax project (syntax-rules () ((_ (x ...) g ...) (lambdag@ (s) (let ((x (walk* x s)) ...) ((all g ...) s)))))) (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 eq-caro (lambda (l x) (caro l x))) (define pairo (lambda (p) (fresh (a d) (conso a d p)))) (define listo (lambda (l) (conde ((nullo l) succeed) ((pairo l) (fresh (d) (cdro l d) (listo d))) (else fail)))) (define membero (lambda (x l) (conde ((nullo l) fail) ((eq-caro l x) succeed) (else (fresh (d) (cdro l d) (membero x d)))))) (define rembero (lambda (x l out) (conde ((nullo l) (== '() out)) ((eq-caro l x) (cdro l out)) (else (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)) (else (fresh (a d res) (conso a d l) (conso a res out) (appendo d s res)))))) (define anyo (lambda (g) (conde (g succeed) (else (anyo g))))) (define nevero (anyo fail)) (define alwayso (anyo succeed)) (define build-num (lambda (n) (cond ((zero? n) '()) ((and (not (zero? n)) (even? n)) (cons 0 (build-num (quotient n 2)))) ((odd? n) (cons 1 (build-num (quotient (- n 1) 2))))))) (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)) (else fail)))) (define poso (lambda (n) (fresh (a d) (== `(,a . ,d) n)))) (define >1o (lambda (n) (fresh (a ad dd) (== `(,a ,ad . ,dd) n)))) (define addero (lambda (d n m r) (condi ((== 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)) (else fail)))) (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) (alli (full-addero d a b c e) (addero e x y z))))) (define +o (lambda (n m k) (addero 0 n m k))) (define -o (lambda (n m k) (+o m k n))) (define *o (lambda (n m p) (condi ((== '() 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))) (else fail)))) (define odd-*o (lambda (x n m p) (fresh (q) (bound-*o q p n m) (*o x m q) (+o `(0 . ,q) m p)))) (define bound-*o (lambda (q p n m) (conde ((nullo q) (pairo p)) (else (fresh (x y z) (cdro q x) (cdro p y) (condi ((nullo n) (cdro m z) (bound-*o x y z '())) (else (cdro n z) (bound-*o x y z m)))))))) (define =lo (lambda (n m) (conde ((== '() n) (== '() m)) ((== '(1) n) (== '(1) m)) (else (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)) (else (fresh (a x b y) (== `(,a . ,x) n) (poso x) (== `(,b . ,y) m) (poso y) (<lo x y)))))) (define <=lo (lambda (n m) (condi ((=lo n m) succeed) ((<lo n m) succeed) (else fail)))) (define <o (lambda (n m) (condi ((<lo n m) succeed) ((=lo n m) (fresh (x) (poso x) (+o n x m))) (else fail)))) (define <=o (lambda (n m) (condi ((== n m) succeed) ((<o n m) succeed) (else fail)))) (define /o (lambda (n m q r) (condi ((== r n) (== '() q) (<o n m)) ((== '(1) q) (=lo n m) (+o r m n) (<o r m)) (else (alli (<lo m n) (<o r m) (poso q) (fresh (nh nl qh ql qlm qlmr rr rh) (alli (splito n r nl nh) (splito q r ql qh) (conde ((== '() nh) (== '() qh) (-o nl r qlm) (*o ql m qlm)) (else (alli (poso nh) (*o ql m qlm) (+o qlm r qlmr) (-o qlmr nl rr) (splito rr r '() rh) (/o nh m qh rh))))))))))) (define splito (lambda (n r l h) (condi ((== '() 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))) (else fail)))) (define logo (lambda (n b q r) (condi ((== '(1) n) (poso b) (== '() q) (== '() r)) ((== '() q) (<o n b) (+o r '(1) n)) ((== '(1) q) (>1o b) (=lo n b) (+o r b n)) ((== '(1) b) (poso q) (+o 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)) (else (== `(,a ,ad ,add . ,ddd) b)))) (<lo b n) (fresh (bw1 bw nw nw1 ql1 ql s) (exp2 b '() bw1) (+o bw1 '(1) bw) (<lo q n) (fresh (q1 bwq1) (+o q '(1) q1) (*o bw q1 bwq1) (<o nw1 bwq1)) (exp2 n '() nw1) (+o nw1 '(1) nw) (/o nw bw ql1 s) (+o ql '(1) ql1) (conde ((== q ql)) (else (<lo ql q))) (fresh (bql qh s qdh qd) (repeated-mul b ql bql) (/o nw bw1 qh s) (+o ql qdh qh) (+o ql qd q) (conde ((== qd qdh)) (else (<o qd qdh))) (fresh (bqd bq1 bq) (repeated-mul b qd bqd) (*o bql bqd bq) (*o b bq bq1) (+o bq r n) (<o n bq1))))) (else fail)))) (define exp2 (lambda (n b q) (condi ((== '(1) n) (== '() q)) ((>1o n) (== '(1) q) (fresh (s) (splito n b s '(1)))) ((fresh (q1 b2) (alli (== `(0 . ,q1) q) (poso q1) (<lo b n) (appendo b `(1 . ,b) b2) (exp2 n b2 q1)))) ((fresh (q1 nh b2 s) (alli (== `(1 . ,q1) q) (poso q1) (poso nh) (splito n b s nh) (appendo b `(1 . ,b) b2) (exp2 nh b2 q1)))) (else fail)))) (define repeated-mul (lambda (n q nq) (conde ((poso n) (== '() q) (== '(1) nq)) ((== '(1) q) (== n nq)) ((>1o q) (fresh (q1 nq1) (+o q1 '(1) q) (repeated-mul n q1 nq1) (*o nq1 n nq))) (else fail)))) (define expo (lambda (b q n) (logo n b q '()))) ;;; 'trace-vars' can be used to print the values of selected variables ;;; in the substitution. (define-syntax trace-vars (syntax-rules () ((_ title x ...) (lambdag@ (s) (begin (printf "~a~n" title) (for-each (lambda (x_ t) (printf "~a = ~s~n" x_ t)) `(x ...) (reify (walk* `(,x ...) s))) (unit s)))))) (define *s (lambda (s) (unit s))) (define *u (lambda (s) (mzero))) (display (run #f (q) (== #t q))) (newline) (display (run #f (q) *s)) (newline) (display (run #f (q) *u)) (newline) (display (run* (q) (fresh (r) (== 3 q) (trace-vars "What it is!" q r))))
Private
[
?
]
Run code
Submit