minikanren break

gistfile1.txt

#lang r5rs

;; chapter 3 minikanren

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

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

(define empty-s '())

;; unsafe version, lvar in lvar blow-up
(define ext-s-no-check
  (lambda (x v s) ;; lvar val and subs 'map'
    (cons `(,x . ,v) s)))

;; triangulation substitution
;; never seen vals on left hand side, lvar.lvar, lvar.val, but never val.lvar

;; (assq 1 (cons (cons 1 2) (cons 3 4)))) => (mcons 1 2), finds kv pair

(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)))))

;; safe version
(define ext-s
  (lambda (x v s)
    (cond
      ((occurs-check x v s) #f)
      (else (ext-s-no-check x v s)))))

;; unify, big idea
;; recursive walk, lvar unify them and their info
;; find subs-map that make the two lvars eq

(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)) ;; nb. v u order, value nocanbe lefty
        ((and (pair? u) (pair? v))
         (let ((s (unify (car u) (car v) s)))
           (and s (unify (cdr u) (cdr u) 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)))))

;; takes empty smap, returns smap with names
(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)))))