source: project/kanren/mini-kanren-runtime.scm @ 7

Last change on this file since 7 was 7, checked in by felix winkelmann, 14 years ago

g.case and rss fixes, fix in post-commit script for single-file case

File size: 13.2 KB
Line 
1;;; Code that accompanies ``The Reasoned Schemer''
2;;; Daniel P. Friedman, William E. Byrd and Oleg Kiselyov
3;;; MIT Press, Cambridge, MA, 2005
4;;;
5;;; The implementation of the logic system used in the book
6
7;;; This file was generated by writeminikanren.pl
8;;; Generated at 2005-08-12 11:27:16
9
10;;; Adapted for Chicken by Alex Shinn 2005-11-02 10:14:45
11
12(require-extension syntax-case)
13(include "mini-kanren.scm")
14
15(define rhs cdr)
16(define lhs car)
17(define size-s length)
18(define var vector)
19(define var? vector?)
20 
21(define empty-s '())
22
23(define walk
24  (lambda (v s)
25    (cond
26      ((var? v)
27       (cond
28         ((assq v s) =>
29          (lambda (a)
30            (walk (rhs a) s)))
31         (else v)))
32      (else v))))
33
34(define ext-s
35  (lambda (x v s)
36    (cons `(,x . ,v) s)))
37 
38(define unify
39  (lambda (v w s)
40    (let ((v (walk v s))
41          (w (walk w s)))
42      (cond
43        ((eq? v w) s)
44        ((var? v) (ext-s v w s))
45        ((var? w) (ext-s w v s))
46        ((and (pair? v) (pair? w))
47         (cond
48           ((unify (car v) (car w) s) =>
49            (lambda (s)
50              (unify (cdr v) (cdr w) s)))
51           (else #f)))
52        ((equal? v w) s)
53        (else #f)))))
54
55(define ext-s-check
56  (lambda (x v s)
57    (cond
58      ((occurs-check x v s) #f)
59      (else (ext-s x v s)))))
60
61(define occurs-check
62  (lambda (x v s)
63    (let ((v (walk v s)))
64      (cond
65        ((var? v) (eq? v x))
66        ((pair? v) 
67         (or
68           (occurs-check x (car v) s)
69           (occurs-check x (cdr v) s)))
70        (else #f)))))
71
72(define unify-check
73  (lambda (v w s)
74    (let ((v (walk v s))
75          (w (walk w s)))
76      (cond
77        ((eq? v w) s)
78        ((var? v) (ext-s-check v w s))
79        ((var? w) (ext-s-check w v s))
80        ((and (pair? v) (pair? w))
81         (cond
82           ((unify-check (car v) (car w) s) =>
83            (lambda (s)
84              (unify-check (cdr v) (cdr w) s)))
85           (else #f)))
86        ((equal? v w) s)
87        (else #f)))))
88
89(define walk*
90  (lambda (v s)
91    (let ((v (walk v s)))
92      (cond
93        ((var? v) v)
94        ((pair? v)
95         (cons
96           (walk* (car v) s)
97           (walk* (cdr v) s)))
98        (else v)))))
99
100(define reify-s
101  (lambda (v s)
102    (let ((v (walk v s)))
103      (cond
104        ((var? v) (ext-s v (reify-name (size-s s)) s))
105        ((pair? v) (reify-s (cdr v) (reify-s (car v) s)))
106        (else s)))))
107
108(define reify-name
109  (lambda (n)
110    (string->symbol
111      (string-append "_" "." (number->string n)))))
112
113(define reify
114  (lambda (v)
115    (walk* v (reify-s v empty-s))))
116
117(define map-inf
118  (lambda (n p a-inf)
119    (case-inf a-inf
120      '()
121      ((a) 
122       (cons (p a) '()))
123      ((a f) 
124       (cons (p a)
125         (cond
126           ((not n) (map-inf n p (f)))
127           ((> n 1) (map-inf (- n 1) p (f)))
128           (else '())))))))
129
130(define succeed (lambdag@ (s) (unit s)))
131(define fail (lambdag@ (s) (mzero)))
132
133(define == 
134  (lambda (v w)
135    (lambdag@ (s)
136      (cond
137        ((unify v w s) => succeed)
138        (else (fail s))))))
139
140(define ==-check
141  (lambda (v w)
142    (lambdag@ (s)
143      (cond
144        ((unify-check v w s) => succeed)
145        (else (fail s))))))
146
147(define mplus
148  (lambda (a-inf f)
149    (case-inf a-inf
150      (f) 
151      ((a) (choice a f))
152      ((a f0) (choice a 
153                (lambdaf@ () (mplus (f0) f)))))))
154
155(define bind
156  (lambda (a-inf g)
157    (case-inf a-inf
158      (mzero) 
159      ((a) (g a))
160      ((a f) (mplus (g a)
161               (lambdaf@ () (bind (f) g)))))))
162
163(define mplusi
164  (lambda (a-inf f)
165    (case-inf a-inf
166      (f) 
167      ((a) (choice a f))
168      ((a f0) (choice a 
169                (lambdaf@ () (mplusi (f) f0)))))))
170
171(define bindi
172  (lambda (a-inf g)
173    (case-inf a-inf
174      (mzero)
175      ((a) (g a))
176      ((a f) (mplusi (g a)                                                 
177               (lambdaf@ () (bindi (f) g)))))))
178
179;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
180;;; Extra forms appearing in the framenotes of the book.
181;;;
182;;; run* is a convenient macro (see frame 10 on page 4 of chapter 1)
183;;; (run* (q) ...) is identical to (run #f (q) ...)
184;;; See frame 40 on page 68 of chapter 5 for a description of 'lambda-limited'.
185;;; See frame 47 on page 138 of chapter 9 for a description of 'project'.
186
187(define ll
188  (lambda (n x g)
189    (lambdag@ (s)
190      (let ((v (walk x s)))
191        (cond
192          ((var? v) (g (ext-s x 1 s)))
193          ((< v n) (g (ext-s x (+ v 1) s)))
194          (else (fail s)))))))
195
196;;; Useful definitions from the book
197
198(define caro
199  (lambda (p a)
200    (fresh (d)
201      (== (cons a d) p))))
202
203(define cdro
204  (lambda (p d)
205    (fresh (a)
206      (== (cons a d) p))))
207
208(define conso
209  (lambda (a d p)
210    (== (cons a d) p)))
211
212(define nullo
213  (lambda (x)
214    (== '() x)))
215
216(define eqo
217  (lambda (x y)
218    (== x y)))
219
220(define eq-caro
221  (lambda (l x)
222    (caro l x)))
223
224(define pairo
225  (lambda (p)
226    (fresh (a d)
227      (conso a d p))))
228
229(define listo
230  (lambda (l)
231    (conde
232      ((nullo l) succeed)
233      ((pairo l)
234       (fresh (d)
235         (cdro l d)
236         (listo d)))
237      (else fail))))
238
239(define membero
240  (lambda (x l)
241    (conde
242      ((nullo l) fail)
243      ((eq-caro l x) succeed)
244      (else
245        (fresh (d)
246          (cdro l d)
247          (membero x d))))))
248
249(define rembero 
250  (lambda (x l out)
251    (conde
252      ((nullo l) (== '() out))
253      ((eq-caro l x) (cdro l out))
254      (else (fresh (a d res)
255              (conso a d l)
256              (rembero x d res)
257              (conso a res out))))))
258
259(define appendo
260  (lambda (l s out)
261    (conde
262      ((nullo l) (== s out))
263      (else
264        (fresh (a d res)
265          (conso a d l)
266          (conso a res out)
267          (appendo d s res))))))
268
269(define anyo
270  (lambda (g)
271    (conde
272      (g succeed)
273      (else (anyo g)))))
274
275(define nevero (anyo fail))
276 
277(define alwayso (anyo succeed))
278
279(define build-num
280  (lambda (n)
281    (cond
282      ((zero? n) '())
283      ((and (not (zero? n)) (even? n))
284       (cons 0
285         (build-num (quotient n 2))))
286      ((odd? n)
287       (cons 1
288         (build-num (quotient (- n 1) 2)))))))
289
290(define full-addero
291  (lambda (b x y r c)
292    (conde
293      ((== 0 b) (== 0 x) (== 0 y) (== 0 r) (== 0 c))
294      ((== 1 b) (== 0 x) (== 0 y) (== 1 r) (== 0 c))
295      ((== 0 b) (== 1 x) (== 0 y) (== 1 r) (== 0 c))
296      ((== 1 b) (== 1 x) (== 0 y) (== 0 r) (== 1 c))
297      ((== 0 b) (== 0 x) (== 1 y) (== 1 r) (== 0 c))
298      ((== 1 b) (== 0 x) (== 1 y) (== 0 r) (== 1 c))
299      ((== 0 b) (== 1 x) (== 1 y) (== 0 r) (== 1 c))
300      ((== 1 b) (== 1 x) (== 1 y) (== 1 r) (== 1 c))
301      (else fail))))
302
303(define poso
304  (lambda (n)
305    (fresh (a d)
306      (== `(,a . ,d) n))))
307
308(define >1o
309  (lambda (n)
310    (fresh (a ad dd)
311      (== `(,a ,ad . ,dd) n))))
312
313(define addero
314  (lambda (d n m r)
315    (condi
316      ((== 0 d) (== '() m) (== n r))
317      ((== 0 d) (== '() n) (== m r)
318       (poso m))
319      ((== 1 d) (== '() m)
320       (addero 0 n '(1) r))
321      ((== 1 d) (== '() n) (poso m)
322       (addero 0 '(1) m r))
323      ((== '(1) n) (== '(1) m)
324       (fresh (a c)
325         (== `(,a ,c) r)
326         (full-addero d 1 1 a c)))
327      ((== '(1) n) (gen-addero d n m r))
328      ((== '(1) m) (>1o n) (>1o r)
329       (addero d '(1) n r))
330      ((>1o n) (gen-addero d n m r))
331      (else fail))))
332
333(define gen-addero
334  (lambda (d n m r)
335    (fresh (a b c e x y z)
336      (== `(,a . ,x) n)
337      (== `(,b . ,y) m) (poso y)
338      (== `(,c . ,z) r) (poso z)
339      (alli
340        (full-addero d a b c e)
341        (addero e x y z)))))
342
343(define +o
344  (lambda (n m k)
345    (addero 0 n m k)))
346
347(define -o
348  (lambda (n m k)
349    (+o m k n)))
350
351(define *o
352  (lambda (n m p)
353    (condi
354      ((== '() n) (== '() p))
355      ((poso n) (== '() m) (== '() p)) 
356      ((== '(1) n) (poso m) (== m p))   
357      ((>1o n) (== '(1) m) (== n p))
358      ((fresh (x z)
359         (== `(0 . ,x) n) (poso x)
360         (== `(0 . ,z) p) (poso z)
361         (>1o m)
362         (*o x m z)))
363      ((fresh (x y)
364         (== `(1 . ,x) n) (poso x)
365         (== `(0 . ,y) m) (poso y)
366         (*o m n p)))
367      ((fresh (x y)
368          (== `(1 . ,x) n) (poso x)     
369          (== `(1 . ,y) m) (poso y)
370          (odd-*o x n m p)))
371      (else fail))))
372
373(define odd-*o
374  (lambda (x n m p)
375    (fresh (q)
376      (bound-*o q p n m)
377      (*o x m q)
378      (+o `(0 . ,q) m p))))
379
380(define bound-*o
381  (lambda (q p n m)
382    (conde
383      ((nullo q) (pairo p))
384      (else
385        (fresh (x y z)
386          (cdro q x)
387          (cdro p y)
388          (condi
389            ((nullo n)
390             (cdro m z)
391             (bound-*o x y z '()))
392            (else
393              (cdro n z) 
394              (bound-*o x y z m))))))))
395
396(define =lo
397  (lambda (n m)
398    (conde
399      ((== '() n) (== '() m))
400      ((== '(1) n) (== '(1) m))
401      (else
402        (fresh (a x b y)
403          (== `(,a . ,x) n) (poso x)
404          (== `(,b . ,y) m) (poso y)
405          (=lo x y))))))
406
407(define <lo
408  (lambda (n m)
409    (conde
410      ((== '() n) (poso m))
411      ((== '(1) n) (>1o m))
412      (else
413        (fresh (a x b y)
414          (== `(,a . ,x) n) (poso x)
415          (== `(,b . ,y) m) (poso y)
416          (<lo x y))))))
417
418(define <=lo
419  (lambda (n m)
420    (condi
421      ((=lo n m) succeed)
422      ((<lo n m) succeed)
423      (else fail))))
424
425(define <o
426  (lambda (n m)
427    (condi
428      ((<lo n m) succeed)
429      ((=lo n m)
430       (fresh (x)
431         (poso x)
432         (+o n x m)))
433      (else fail))))
434
435(define <=o
436  (lambda (n m)
437    (condi
438      ((== n m) succeed)
439      ((<o n m) succeed)
440      (else fail))))
441
442(define /o
443  (lambda (n m q r)
444    (condi
445      ((== r n) (== '() q) (<o n m))
446      ((== '(1) q) (=lo n m) (+o r m n)
447       (<o r m))
448      (else
449        (alli
450          (<lo m n)                       
451          (<o r m)                       
452          (poso q)                 
453          (fresh (nh nl qh ql qlm qlmr rr rh)
454            (alli
455              (splito n r nl nh)
456              (splito q r ql qh)
457              (conde
458                ((== '() nh)
459                 (== '() qh)
460                 (-o nl r qlm)
461                 (*o ql m qlm))
462                (else
463                  (alli 
464                    (poso nh)
465                    (*o ql m qlm)
466                    (+o qlm r qlmr)
467                    (-o qlmr nl rr)
468                    (splito rr r '() rh)
469                    (/o nh m qh rh)))))))))))
470
471(define splito
472  (lambda (n r l h)
473    (condi
474      ((== '() n) (== '() h) (== '() l))
475      ((fresh (b n^)
476         (== `(0 ,b . ,n^) n)
477         (== '() r)
478         (== `(,b . ,n^) h)
479         (== '() l)))
480      ((fresh (n^)
481         (==  `(1 . ,n^) n)
482         (== '() r)
483         (== n^ h)
484         (== '(1) l)))
485      ((fresh (b n^ a r^)
486         (== `(0 ,b . ,n^) n)
487         (== `(,a . ,r^) r)
488         (== '() l)
489         (splito `(,b . ,n^) r^ '() h)))
490      ((fresh (n^ a r^)
491         (== `(1 . ,n^) n)
492         (== `(,a . ,r^) r)
493         (== '(1) l)
494         (splito n^ r^ '() h)))
495      ((fresh (b n^ a r^ l^)
496         (== `(,b . ,n^) n)
497         (== `(,a . ,r^) r)
498         (== `(,b . ,l^) l)
499         (poso l^)
500         (splito n^ r^ l^ h)))
501      (else fail))))
502
503(define logo
504  (lambda (n b q r)
505    (condi
506      ((== '(1) n) (poso b) (== '() q) (== '() r))
507      ((== '() q) (<o n b) (+o r '(1) n))
508      ((== '(1) q) (>1o b) (=lo n b) (+o r b n))
509      ((== '(1) b) (poso q) (+o r '(1) n))
510      ((== '() b) (poso q) (== r n))
511      ((== '(0 1) b)
512       (fresh (a ad dd)
513         (poso dd)
514         (== `(,a ,ad . ,dd) n)
515         (exp2 n '() q)
516         (fresh (s)
517           (splito n dd r s))))
518      ((fresh (a ad add ddd)
519         (conde
520           ((== '(1 1) b))
521           (else (== `(,a ,ad ,add . ,ddd) b))))
522       (<lo b n)
523       (fresh (bw1 bw nw nw1 ql1 ql s)
524         (exp2 b '() bw1)
525         (+o bw1 '(1) bw)
526         (<lo q n)
527         (fresh (q1 bwq1)
528           (+o q '(1) q1)
529           (*o bw q1 bwq1)
530           (<o nw1 bwq1))
531           (exp2 n '() nw1)
532           (+o nw1 '(1) nw)
533           (/o nw bw ql1 s)
534           (+o ql '(1) ql1)
535         (conde
536           ((== q ql))
537           (else (<lo ql q)))
538         (fresh (bql qh s qdh qd)
539           (repeated-mul b ql bql)       
540           (/o nw bw1 qh s)               
541           (+o ql qdh qh)
542           (+o ql qd q)
543           (conde
544             ((== qd qdh))
545             (else (<o qd qdh)))
546           (fresh (bqd bq1 bq)
547             (repeated-mul b qd bqd)       
548             (*o bql bqd bq)               
549             (*o b bq bq1)               
550             (+o bq r n)
551             (<o n bq1)))))
552      (else fail))))
553
554(define exp2
555  (lambda (n b q)
556    (condi
557      ((== '(1) n) (== '() q))
558      ((>1o n) (== '(1) q)
559       (fresh (s)
560         (splito n b s '(1))))
561      ((fresh (q1 b2)                       
562         (alli                 
563           (== `(0 . ,q1) q)
564           (poso q1)
565           (<lo b n)
566           (appendo b `(1 . ,b) b2)
567           (exp2 n b2 q1))))
568      ((fresh (q1 nh b2 s)               
569          (alli
570            (== `(1 . ,q1) q)
571            (poso q1)
572            (poso nh)
573            (splito n b s nh)
574            (appendo b `(1 . ,b) b2)
575            (exp2 nh b2 q1))))
576      (else fail))))
577
578(define repeated-mul
579  (lambda (n q nq)
580    (conde
581      ((poso n) (== '() q) (== '(1) nq))
582      ((== '(1) q) (== n nq))
583      ((>1o q)
584       (fresh (q1 nq1)
585         (+o q1 '(1) q)
586         (repeated-mul n q1 nq1)
587         (*o nq1 n nq)))
588      (else fail))))
589
590(define expo
591  (lambda (b q n)
592    (logo n b q '())))
Note: See TracBrowser for help on using the repository browser.