bsdfk

temp.ss

#lang r5rs
;;;;
; From the paper:
;     Relational Programming in miniKanren:
;     Techniques, Applications, And Implementations
;     William E. Byrd
;;;;

;;
;; Conventions:
;; s = association list
;; v = value
;; x = logic variable
;;


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

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

;empty association list
(define empty-s '())

;insert into the assoc list without checking if it is already present
(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))))

;like ext-s-no-check, but first checks to see if it is already in the assoc list
(define ext-s
  (lambda (x v s)
    (cond
      ((occurs-check x v s) #f)
      (else (ext-s-no-check x v s)))))

;checks if 
(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 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)))))

;monadic zero
(define-syntax mzero
  (syntax-rules ()
    ((_) #f)))

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

;choose one of (zero, unit, thunk, choice), thunk
(define-syntax choice
  (syntax-rules ()
    ((_ a f) (cons a f))))

;lazily unit
(define-syntax inc
  (syntax-rules ()
    ((_ e) (lambda () e))))

;poor man's pattern matching
(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 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 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 bind*
  (syntax-rules ()
    ((_ e) e)
    ((_ e g0 g ...) (bind* (bind e g0) g ...))))