;;; 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 book

;;; This file was generated by writeminikanren.pl
;;; Generated at 2005-08-12 11:27:16

;;; Adapted for Chicken by Alex Shinn 2005-11-02 10:14:45

(define-syntax lambdag@
  (syntax-rules ()
    ((_ (s) e) (lambda (s) e))))

(define-syntax lambdaf@
  (syntax-rules ()
    ((_ () e) (lambda () e))))

(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-syntax fresh 
  (syntax-rules ()
    ((_ (x ...) g ...)
     (lambdag@ (s)
       (let ((x (var 'x)) ...)
         ((all g ...) s))))))

(define-syntax conde
  (syntax-rules ()
    ((_ c ...) (cond-aux ife c ...))))

(define-syntax all
  (syntax-rules ()
    ((_ g ...) (all-aux bind g ...))))

(define-syntax alli
  (syntax-rules ()
    ((_ g ...) (all-aux bindi g ...))))

(define-syntax condi
  (syntax-rules ()
    ((_ c ...) (cond-aux ifi c ...))))

(define-syntax conda
  (syntax-rules ()
    ((_ c ...) (cond-aux ifa c ...))))

(define-syntax condu
  (syntax-rules ()
    ((_ c ...) (cond-aux ifu c ...))))

(define-syntax all-aux
  (syntax-rules ()
    ((_ bnd) succeed)
    ((_ bnd g) g)
    ((_ bnd g0 g ...)
     (let ((g^ g0))
       (lambdag@ (s)
         (bnd (g^ s) 
           (lambdag@ (s) ((all-aux bnd g ...) s))))))))

(define-syntax cond-aux
  (syntax-rules (else)
    ((_ ifer) fail)
    ((_ ifer (else g ...)) (all g ...))
    ((_ ifer (g ...)) (all g ...))
    ((_ ifer (g0 g ...) c ...)
     (ifer g0
       (all g ...)
       (cond-aux ifer c ...)))))

(define-syntax ife
  (syntax-rules ()
    ((_ g0 g1 g2)
     (lambdag@ (s)
       (mplus ((all g0 g1) s) (lambdaf@ () (g2 s)))))))

(define-syntax ifi
  (syntax-rules ()
    ((_ g0 g1 g2)
     (lambdag@ (s)
       (mplusi ((all g0 g1) s) (lambdaf@ () (g2 s)))))))

(define-syntax ifa
  (syntax-rules ()
    ((_ g0 g1 g2)
     (lambdag@ (s)
       (let ((s-inf (g0 s)))
         (case-inf s-inf
           (g2 s)
           ((s) (g1 s))
           ((s f) (bind s-inf g1))))))))

(define-syntax ifu
  (syntax-rules ()
    ((_ g0 g1 g2)
     (lambdag@ (s)
       (let ((s-inf (g0 s)))
         (case-inf s-inf
           (g2 s)
           ((s) (g1 s))
           ((s f) (g1 s))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;; Extra forms appearing in the framenotes of the book.
;;;
;;; run* is a convenient macro (see frame 10 on page 4 of chapter 1)
;;; (run* (q) ...) is identical to (run #f (q) ...)
;;; See frame 40 on page 68 of chapter 5 for a description of 'lambda-limited'.
;;; See frame 47 on page 138 of chapter 9 for a description of 'project'.

(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-syntax project 
  (syntax-rules ()
    ((_ (x ...) g ...)  
     (lambdag@ (s)
       (let ((x (walk* x s)) ...)
         ((all g ...) s))))))

;;;  '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))))))