microkanren_in_felix.flx

// Jason Hemann and Dan Friedman
// microKanren, final implementation from paper

SCHEME """ (define (var c) (vector c)) """;
SCHEME """ (define (var? x) (vector? x)) """;
SCHEME """ (define (var=? x1 x2) (= (vector-ref x1 0) (vector-ref x2 0))) """;

SCHEME """
(define (assp p l)
  (cond ((null? l) #f)
        ((p (car l)) (car l))
        (else (assp p (cdr l)))))
""";

SCHEME """ 
(define (walk u s)
  (let ((pr (and (var? u) (assp (lambda (v) (var=? u v)) s))))
    (if pr (walk (cdr pr) s) u)))
""";

SCHEME """ (define (ext-s x v s) `((,x . ,v) . ,s)) """;

SCHEME """ 
(define (== u v)
  (lambda (s/c)
    (let ((s (unify u v (car s/c))))
      (if s (unit `(,s . ,(cdr s/c))) mzero))))
""";

SCHEME """ (define (unit s/c) (cons s/c mzero)) """;
SCHEME """ (define mzero '()) """;

SCHEME """ 
(define (unify u v s)
  (let ((u (walk u s)) (v (walk v s)))
    (cond
      ((and (var? u) (var? v) (var=? u v)) s)
      ((var? u) (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))))
      (else (and (eqv? u v) s)))))
""";

SCHEME """ 
(define (call/fresh f)
  (lambda (s/c)
    (let ((c (cdr s/c)))
      ((f (var c)) `(,(car s/c) . ,(+ c 1))))))
""";

SCHEME """ 
(define (disj g1 g2) (lambda (s/c) (mplus (g1 s/c) (g2 s/c))))
""";
SCHEME """ 
(define (conj g1 g2) (lambda (s/c) (bind (g1 s/c) g2)))
""";

SCHEME """ 
(define (mplus $1 $2)
  (cond
    ((null? $1) $2)
    ((procedure? $1) (lambda () (mplus $2 ($1))))
    (else (cons (car $1) (mplus (cdr $1) $2)))))
""";

SCHEME """ 
(define (bind $ g)
  (cond
    ((null? $) mzero)
    ((procedure? $) (lambda () (bind ($) g)))
    (else (mplus (g (car $)) (bind (cdr $) g)))))
""";

SCHEME """ 
(define-syntax test-check
  (syntax-rules ()
    ((_ title tested-expression expected-result)
     (begin
       (display (string-append "Testing " title "\n"))
       (let* ((expected expected-result)
              (produced tested-expression))
         (or (equal? expected produced)
             (display (string-append "test-check " 
                "Failed: " tested-expression 
                "Expected: " expected 
                "Computed: " produced
                ))))))))
""";

SCHEME """ 
(define a-and-b
  (conj 
   (call/fresh (lambda (a) (== a 7)))
   (call/fresh 
    (lambda (b) 
      (disj
       (== b 5)
       (== b 6))))))
""";

SCHEME """ 
(define fives
  (lambda (x)
    (disj
     (== x 5)      
     (lambda (a/c)
       (lambda ()
         ((fives x) a/c))))))
""";

SCHEME """ 
(define appendo
  (lambda (l s out)
    (disj
     (conj (== '() l) (== s out))
     (call/fresh
      (lambda (a)
        (call/fresh
         (lambda (d)
           (conj
            (== `(,a . ,d) l)
            (call/fresh
             (lambda (res)
               (conj
                (== `(,a . ,res) out)
                (lambda (s/c)
                  (lambda ()
                    ((appendo d s res) s/c))))))))))))))
""";

SCHEME """ 
(define appendo2
  (lambda (l s out)
    (disj
     (conj (== '() l) (== s out))
     (call/fresh
      (lambda (a)
        (call/fresh
         (lambda (d)
           (conj
            (== `(,a . ,d) l)
            (call/fresh
             (lambda (res)
               (conj
                (lambda (s/c)
                  (lambda ()
                    ((appendo2 d s res) s/c)))
                (== `(,a . ,res) out))))))))))))
""";

SCHEME """ 
(define call-appendo
  (call/fresh
   (lambda (q)
     (call/fresh
      (lambda (l)
        (call/fresh
         (lambda (s)
           (call/fresh
            (lambda (out)
              (conj
               (appendo l s out)
               (== `(,l ,s ,out) q)))))))))))
""";

SCHEME """ 
(define call-appendo2
  (call/fresh
   (lambda (q)
     (call/fresh
      (lambda (l)
        (call/fresh
         (lambda (s)
           (call/fresh
            (lambda (out)
              (conj
               (appendo2 l s out)
               (== `(,l ,s ,out) q)))))))))))
""";

SCHEME """ 
(define call-appendo3
  (call/fresh
   (lambda (q)
     (call/fresh
      (lambda (l)
        (call/fresh
         (lambda (s)
           (call/fresh
            (lambda (out)
              (conj
               (== `(,l ,s ,out) q)
               (appendo l s out)))))))))))
""";

SCHEME """ (define ground-appendo (appendo '(a) '(b) '(a b))) """;
SCHEME """ (define ground-appendo2  (appendo2 '(a) '(b) '(a b))) """;

SCHEME """ 
(define relo
  (lambda (x)
    (call/fresh
     (lambda (x1)
       (call/fresh
        (lambda (x2)
          (conj
           (== x `(,x1 . ,x2))
           (disj
            (== x1 x2)
            (lambda (s/c)
              (lambda () ((relo x) s/c)))))))))))
""";

SCHEME """ 
(define many-non-ans
  (call/fresh
   (lambda (x)
     (disj
      (relo `(5 . 6))
      (== x 3)))))
""";

SCHEME """ 
(define-syntax Zzz
  (syntax-rules ()
    ((_ g) (lambda (s/c) (lambda () (g s/c))))))
""";

SCHEME """ 
(define-syntax conj+
  (syntax-rules ()
    ((_ g) (Zzz g))
    ((_ g0 g ...) (conj (Zzz g0) (conj+ g ...)))))
""";

SCHEME """ 
(define-syntax disj+
  (syntax-rules ()
    ((_ g) (Zzz g))
    ((_ g0 g ...) (disj (Zzz g0) (disj+ g ...)))))
""";

SCHEME """ 
(define-syntax fresh
  (syntax-rules ()
    ((_ () g0 g ...) (conj+ g0 g ...))
    ((_ (x0 x ...) g0 g ...)
     (call/fresh
      (lambda (x0)
        (fresh (x ...) g0 g ...))))))
""";

SCHEME """ 
(define-syntax conde
  (syntax-rules ()
    ((_ (g0 g ...) ...) (disj+ (conj+ g0 g ...) ...))))
""";

SCHEME """ 
(define-syntax run
  (syntax-rules ()
    ((_ n (x ...) g0 g ...)
     (map reify-1st (take n (call/goal (fresh (x ...) g0 g ...)))))))
""";

SCHEME """ 
(define-syntax run*
  (syntax-rules ()
    ((_ (x ...) g0 g ...)
     (map reify-1st (take-all (call/goal (fresh (x ...) g0 g ...)))))))
""";

SCHEME """ 
(define empty-state '(() . 0))
""";

SCHEME """ 
(define (call/goal g) (g empty-state))
""";

SCHEME """ 
(define (pull $)
  (if (procedure? $) (pull ($)) $))
""";

SCHEME """ 
(define (take-all $)
  (let (($ (pull $)))
    (if (null? $) '() (cons (car $) (take-all (cdr $))))))
""";

SCHEME """ 
(define (take n $)
  (if (zero? n) '()
    (let (($ (pull $)))
      (if (null? $) '() (cons (car $) (take (- n 1) (cdr $)))))))
""";

SCHEME """ 
(define (reify-1st s/c)
  (let ((v (walk* (var 0) (car s/c))))
    (walk* v (reify-s v '()))))
""";

SCHEME """ 
(define (walk* v s)
  (let ((v (walk v s)))
    (cond
      ((var? v) v)
      ((pair? v) (cons (walk* (car v) s)
                   (walk* (cdr v) s)))
      (else  v))))
""";

SCHEME """ 
(define (reify-s v s)
  (let ((v (walk v s)))
    (cond
      ((var? v)
       (let  ((n (reify-name (length s))))
         (cons `(,v . ,n) s)))
      ((pair? v) (reify-s (cdr v) (reify-s (car v) s)))
      (else s))))
""";

SCHEME """ 
(define (reify-name n)
  (string->symbol
    (string-append "_" "." (number->string n))))
""";

SCHEME """ 
(define (fresh/nf n f)
  (letrec
    ((app-f/v*
       (lambda (n v*)
         (cond
           ((zero? n) (apply f (reverse v*)))
           (else (call/fresh
                   (lambda (x)
                     (app-f/v* (- n 1) (cons x v*)))))))))
     (app-f/v* n '())))
""";

SCHEME """ 
(test-check "second-set t1"
  (let (($ ((call/fresh (lambda (q) (== q 5))) empty-state)))
    (car $))
  '(((#(0) . 5)) . 1))
""";

SCHEME """ 
  (display
  (let (($ ((call/fresh (lambda (q) (== q 7))) empty-state)))
    (car $)))
""";

println$ "done";