autokanren.scm

autokanren.scm

;; This runs in veneer http://tca.github.io/veneer/editor.html
;; (developed inside veneer!)

;; Questions
;; A. How to shuffle all the recursive calls to the end, or just bubble unifications to the top?
;; B. How to optimize away simple things? seems very "one way" I do a tiny bit of optimization already..

;; it can generate kanren versions of four scheme functions (append, mem, rember, unwrap)

(define (nullo e)
  (== e '()))
(define (pairo e)
  (fresh (u v)
   (== e `(,u . ,v))))

(define (eq-caro l x)
  (fresh (t)
     (== l `(,x . ,t))))

(define (not-membero e l)
  (conde
   ((== l '()))
   ((fresh (x y)
      (== l `(,x . ,y))
      (=/= e x)
      (not-membero e y)))))

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

(define (replace-nodeo s p q s^)
  (conde
   ((== s p) (== q s^))
   ((symbolo s) (=/= s p) (== s s^))
   ((== s '()) (== s^ '()))
   ((fresh (x y x^ y^)
      (=/= s p)
      (== s `(,x . ,y))
      (== s^ `(,x^ . ,y^))
      (replace-nodeo x p q x^)
      (replace-nodeo y p q y^)))))

;;;

(define (t1 q r)
  (fresh ()
    (== q '(define (append x y)
             (cond ((null? x) y)
                   ((pair? x) (cons (car x) (append (cdr x) y))))))
    (translate-definition q r)))

(define (t1b a b)
  (fresh (m)
   (== a '(cons (car x) (append (cdr x) y)))
   (replace-nodeo a '(car x) 'u m)
   (replace-nodeo m '(cdr x) 'v b)))

(define (t2 q r) ;; pg 47
  (fresh ()
    (== q '(define (mem x l)
             (cond ((null? l) l)
                   ((eq-car? l x) l)
                   ((pair? l) (mem x (cdr l))))))
    (translate-definition q r)))

(define (t3 q r) ;; pg 51
  (fresh ()
    (== q '(define (rember x l)
             (cond ((null? l) l)
                   ((eq-car? l x) (cdr l))
                   ((pair? l);; changed from else to pair?
                    (cons (car l) (rember x (cdr l))))
                   
                   )))
    (translate-definition q r)))

(define (t4 q r) ;; pg 68
  (fresh ()
    (== q '(define (unwrap x)
             (cond ((pair? x)(unwrap (car x)))
                   (else x))))
    (translate-definition q r)))

;;;

(define (name-mangleo n n^)
  (conde
   ((== n 'append) (== n^ 'appendo))
   ((== n 'mem) (== n^ 'memo))
   ((== n 'rember) (== n^ 'rembero))
   ((== n 'unwrap) (== n^ 'unwrapo))
   
   ((== n 'null?) (== n^ 'nullo))
   ((== n 'pair?) (== n^ 'pairo))
   ((== n 'eq-car?) (== n^ 'eq-caro))
   ((== n 'cons) (== n^ 'conso))))

(define (unpack-def d name args body)
  (== d `(define (,name . ,args) ,body)))

(define (translate-definition i o)
  (fresh (n a b n^ a^ b^ r)
    (symbolo r)
    (unpack-def i n a b)
    (unpack-def o n^ a^ b^)
    ;;n
    (name-mangleo n n^)
    ;;a
    (not-membero r a)
    (appendo a `(,r)  a^)
    ;;b
    (translate-expression b b^ r)
    ))

(define (translate-expression b b^ r)
  (conde
   ((symbolo b)
    (== b^ `(== ,r ,b)))
   ((fresh (f f^ args)
     (== b `(,f . ,args))
     (=/= f 'cond)
     (name-mangleo f f^)
     (translate-function-callo f^ args b^ r)))
   ((fresh (clauses clauses^)
      (== b `(cond . ,clauses))
      (== b^ `(conde . ,clauses^))
      (translate-clauses clauses clauses^ r)))))

(define (translate-function-callo f^ args b^ r)
  (fresh (call args^)
   (translate-function-call-argumentso args args^ b^ call)
   (appendo `(,f^ . ,args^) `(,r) call)
         ))

(define (translate-predicate-callo po args b^)
  (fresh (call args^)
   (translate-function-call-argumentso args args^ b^ call)
   (== `(,po . ,args^) call)))

(define (translate-function-call-argumentso args args^ b^ call)
  (conde
   ((== args '()) (== args^ '()) (== b^ call))
   ((fresh (x y x^ y^ b^^ r)
      (== args `(,x . ,y))
      (== args^ `(,r . ,y^))
      (symbolo r)
      (conde
       ((symbolo x) (== x r) ;; this is a tiny bit dangerous in case
         ;; both of then happen to be symbols, then we really do
         ;; not to insert an == into the code, but hopefully that
         ;; wont happen.. if it does you can easily fix it by
         ;; make all the parameters the relation being defined to be
         ;; logic variables
                    (== b^ b^^))
       ((pairo x) (translate-expression x x^ r)
                  (== b^ `(fresh (,r) ,x^ ,b^^))))
      (translate-function-call-argumentso y y^ b^^ call)))))

(define (translate-clauses clauses clauses^ r)
  (conde
   ((== clauses '())
    (== clauses^ '()))
   ((fresh (rest rest^ condition body clause^)
     (== clauses `((,condition ,body) . ,rest))
     (== clauses^ `(,clause^ . ,rest^))
     (conde
      ((fresh (e body^)
         (== condition `(null? ,e))
         (symbolo e)
         (== clause^ `((== ,e '()) ,body^))
         (translate-expression body body^ r)
         ))
      ((fresh (e e2 f1 f2 bodym bodymm body^)
         (conde
          ((== condition `(pair? ,e))
           (symbolo e)
           (== clause^ `((fresh (,f1 ,f2)
                          (== ,e `(,,f1 . ,,f2))
                          ,body^))))
          ((== condition `(eq-car? ,e ,e2))
           (symbolo e) (symbolo e2)
           (== clause^ `((fresh (,f2)
                          (== ,e `(,,e2 . ,,f2))
                          ,body^)))))
         (symbolo f1)
         (symbolo f2)
         
         (replace-nodeo body `(car ,e) f1 bodym)
         (replace-nodeo bodym `(cdr ,e) f2 bodymm)
         (translate-expression bodymm body^ r)))
      ((fresh (p po b^ ergs body^)
         (== condition `(,p . ,ergs))
         (=/= p 'null?)
         (=/= p 'pair?)
         (=/= p 'eq-car?)
         (name-mangleo p po)
         (translate-predicate-callo po ergs b^)
         (== clause^ `(,b^ ,body^))
         (translate-expression body body^ r)
         ))
   	  ((fresh (e body^)
         (== condition 'else)
         (== clause^ `(,body^))
         (translate-expression body body^ r))))
     (translate-clauses rest rest^ r)))))

;;

(t4 q r)

output.scm

(define (conso x y z) (== z `(,x . ,y)))

;; Here is the output of the program, formatted/indented by me

(define (appendo x y _.0)
  (conde ((== x (quote ())) (== _.0 y))
         ((fresh (_.1 _.2)
            (== x (quasiquote ((unquote _.1) . (unquote _.2))))
            (fresh (_.3)
              (appendo _.2 y _.3)
              (conso _.1 _.3 _.0))))))


(define (memo x l _.0)
  (conde ((== l (quote ())) (== _.0 l))
         ((fresh (_.1)
            (== l (quasiquote ((unquote x) . (unquote _.1))))
            (== _.0 l)))
         ((fresh (_.2 _.3)
            (== l (quasiquote ((unquote _.2) . (unquote _.3))))
            (memo x _.3 _.0)))))


(define (rembero x l _.0)
  (conde ((== l (quote ())) (== _.0 l))
         ((fresh (_.1)
            (== l (quasiquote ((unquote x) . (unquote _.1))))
            (== _.0 _.1)))
         ((fresh (_.2 _.3)
            (== l (quasiquote ((unquote _.2) . (unquote _.3))))
            (fresh (_.4)
              (rembero x _.3 _.4)
              (conso _.2 _.4 _.0))))))

(define (unwrapo x _.0)
  (conde ((fresh (_.1 _.2)
            (== x (quasiquote ((unquote _.1) . (unquote _.2))))
            (unwrapo _.1 _.0)))
         ((== _.0 x))))