mk.scm

gistfile1.scm

#lang r5rs

(define-syntax var
  (syntax-rules ()
    ((_ x) (vector x))))

(define-syntax var?
  (syntax-rules ()
    ((_ x) (vector? x))))

(define empty-s '())

(define ext-s-no-check
  (lambda (x v s)
    (cons `(,x . ,v) s)))

(define rhs cdr)

(define walk
  (lambda (v s)
    (cond
      ((var? v) (let ((a (assq v s)))
                  (cond
                    (a (walk (rhs a) s))
                    (else v))))
      (else v))))

(define occurs-check
  (lambda (x v s)
    (let ((v (walk v s)))
      (cond
        ((var? v) (eq? x v))
        ((pair? v) (or (occurs-check x (car v) s)
                       (occurs-check x (cdr v) s)))
        (else #f)))))

(define ext-s
  (lambda (x v s)
    (cond
      ((occurs-check x v s) #f)
      (else (ext-s-no-check 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)
         (cond
           ((var? v) (ext-s-no-check u v s))
           (else (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))))
        ((equal? u v) s)
        (else #f)))))
          
(define reify
  (lambda (v s)
    (let ((v (walk* v s)))
      (walk* v (reify-s v empty-s)))))

(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 (length 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-syntax mzero
  (syntax-rules ()
    ((_) #f)))

(define-syntax unit
  (syntax-rules ()
    ((_ a) a)))

(define-syntax choice
  (syntax-rules ()
    ((_ a f) (cons a f))))

(define-syntax inc
  (syntax-rules ()
    ((_ e) (lambda () e))))

(define-syntax case-inf
  (syntax-rules ()
    ((_ e 
        (() e0)     ; mzero
        ((f^) e1)   ; inc
        ((a^) e2)   ; unit
        ((a f) e3)) ; choice
     (let ((a-inf e))
       (cond
         ((not a-inf) e0)
         ((procedure? a-inf) (let ((f^ a-inf)) e1))
         ((and (pair? a-inf) (procedure? (cdr a-inf)))
          (let ((a (car a-inf))
                (f (cdr a-inf)))
            e3))
         (else (let ((a^ a-inf)) e2)))))))

(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) (lambda () (bind (f) g)))))))

(define-syntax mplus*
  (syntax-rules ()
    ((_ e) e)
    ((_ e0 e ...) (mplus e0 (lambda () (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 (lambda () (mplus (f) f^)))))))

(define-syntax fresh
  (syntax-rules ()
    ((_ (x ...) g0 g ...)
     (lambda (a)
       (inc
         (let ((x (var 'x)) ...)
           (bind* (g0 a) g ...)))))))

(define-syntax run
  (syntax-rules ()
    ((_ n (x) g0 g ...)
     (take n
       (lambda ()
         ((fresh (x) g0 g ...
            (lambda (a)
              (cons (reify x a) '())))
          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-syntax ==
  (syntax-rules ()
    ((_ u v)
     (lambda (a)
       (cond
         ((unify u v a) => (lambda (a) (unit a)))
         (else (mzero)))))))

(define-syntax conde
  (syntax-rules ()
    ((_ (g0 g ...) (g1 g^ ...) ...)
     (lambda (a)
       (inc
         (mplus* (bind* (g0 a) g ...)
                 (bind* (g1 a) g^ ...)
                 ...))))))

(define nevero
  (lambda ()
    (fresh ()
      (nevero))))

(define appendo 
  (lambda (l s out)
    (conde
      ((== l '()) (== s out))
      ((fresh (a d res)
         (== `(,a . ,d) l)
         (== `(,a . ,res) out)
         (appendo d s res))))))

(define-syntax project
  (syntax-rules ()
    ((_ (x y ...) g0 g ...)
     (lambda (a)
       (let ((x (walk x a)) (y (walk y a)) ...)
         ((fresh ()
            g0 g ...) a))))))