# HG changeset patch
# User Steve Losh <steve@stevelosh.com>
# Date 1458832671 0
# Node ID c1535003a7e947e3657384f1e7091b96206405e2
# Parent  9d90efbd87878462e1bfefcbbc2121074fe16af2
More grinding through the compiled version

diff -r 9d90efbd8787 -r c1535003a7e9 src/paip-compiled.lisp
--- a/src/paip-compiled.lisp	Wed Mar 23 17:43:02 2016 +0000
+++ b/src/paip-compiled.lisp	Thu Mar 24 15:17:51 2016 +0000
@@ -17,6 +17,13 @@
            item sequence :test (complement test)
            keyword-args)))
 
+(defun find-anywhere (item tree)
+  "Does item occur anywhere in tree?"
+  (if (atom tree)
+    (if (eql item tree) tree)
+    (or (find-anywhere item (first tree))
+        (find-anywhere item (rest tree)))))
+
 (defun interned-symbol (&rest args)
   (intern (format nil "~{~A~}" args)))
 
@@ -209,27 +216,37 @@
       (nconc
         (mapcar #'make-= parameters (relation-arguments (clause-head clause)))
         (clause-body clause))
-      continuation)))
+      continuation
+      (mapcar #'self-cons parameters))))
 
-(defun compile-body (body continuation)
+(defun compile-body (body continuation bindings)
   "Compile the body of a clause."
   (if (null body)
     `(funcall ,continuation)
     (let* ((goal (first body))
            (macro (prolog-compiler-macro (predicate goal)))
            (macro-val (when macro
-                        (funcall macro goal (rest body) continuation))))
+                        (funcall macro goal (rest body) continuation bindings))))
       (if (and macro (not (eq macro-val :pass)))
         macro-val
         (compile-call
           (make-predicate (predicate goal)
                           (relation-arity goal))
-          (mapcar #'(lambda (arg) (compile-arg arg))
+          (mapcar #'(lambda (arg) (compile-arg arg bindings))
                   (relation-arguments goal))
           (if (null (rest body))
             continuation
             `#'(lambda ()
-                 ,(compile-body (rest body) continuation))))))))
+                 ,(compile-body (rest body) continuation
+                                (bind-new-variables bindings goal)))))))))
+
+(defun bind-new-variables (bindings goal)
+  "Extend bindings to include any unbound variables in goal."
+  (let ((variables (remove-if #'(lambda (v) (assoc v bindings))
+                              (variables-in goal))))
+    (nconc (mapcar #'self-cons variables) bindings)))
+
+(defun self-cons (x) (cons x x))
 
 (defun compile-call (predicate args continuation)
   `(,predicate ,@args ,continuation))
@@ -244,26 +261,87 @@
          #'(lambda ,arglist .,body)))
 
 (def-prolog-compiler-macro
-  = (goal body continuation)
+  = (goal body continuation bindings)
   (let ((args (relation-arguments goal)))
     (if (/= (length args) 2)
       :pass
-      `(when ,(compile-unify (first args) (second args))
-         ,(compile-body body continuation)))))
+      (multiple-value-bind (code1 bindings1)
+          (compile-unify (first args) (second args) bindings)
+          (compile-if code1 (compile-body body continuation bindings1))))))
+
+(defun compile-unify (x y bindings)
+  "Return 2 values: code to test if x any y unify, and a new binding list."
+  (cond
+    ((not (or (has-variable-p x) (has-variable-p y)))
+     (values (equal x y) bindings))
+    ((and (consp x) (consp y))
+     (multiple-value-bind (code1 bindings1)
+         (compile-unify (first x) (first y) bindings)
+       (multiple-value-bind (code2 bindings2)
+           (compile-unify (rest x) (rest y) bindings1)
+         (values (compile-if code1 code2) bindings2))))
+    ((variable-p x) (compile-unify-variable x y bindings))
+    (t (compile-unify-variable y x bindings))))
+
+(defun compile-if (pred then-part)
+  (case pred
+    ((t) then-part)
+    ((nil) nil)
+    (otherwise `(if ,pred ,then-part))))
 
-(defun compile-unify (x y)
-  "Return code that tests if the items unify."
-  `(unify! ,(compile-arg x) ,(compile-arg y)))
+(defun compile-unify-variable (x y bindings)
+  "X is a variable, and Y might be."
+  (let* ((xb (follow-binding x bindings))
+         (x1 (if xb (cdr xb) x))
+         (yb (if (variable-p y) (follow-binding y bindings)))
+         (y1 (if yb (cdr yb) y)))
+    (cond
+      ((or (eq x '?) (eq y '?)) (values t bindings))
+      ((not (and (equal x x1) (equal y y1)))
+       (compile-unify x1 y1 bindings))
+      ((find-anywhere x1 y1) (values nil bindings))
+      ((consp y1)
+       (values `(unify! ,x1 ,(compile-arg y1 bindings))
+               (bind-variables-in y1 bindings)))
+      ((not (null xb))
+       (if (and (variable-p y1) (null yb))
+           (values 't (extend-bindings y1 x1 bindings))
+           (values `(unify! ,x1 ,(compile-arg y1 bindings))
+                   (extend-bindings x1 y1 bindings))))
+      ((not (null yb))
+       (compile-unify-variable y1 x1 bindings))
+      (t (values 't (extend-bindings x1 y1 bindings))))))
 
+(defun bind-variables-in (exp bindings)
+  "Bind all variables in exp to themselves, and add that to bindings (except for already-bound vars)."
+  (dolist (var (variables-in exp))
+    (when (not (get-binding var bindings))
+      (setf bindings (extend-bindings var var bindings))))
+  bindings)
 
-(defun compile-arg (arg)
+(defun follow-binding (var bindings)
+  "Get the ultimate binding of var according to the bindings."
+  (let ((b (get-binding var bindings)))
+    (if (eq (car b) (cdr b))
+      b
+      (or (follow-binding (cdr b) bindings)
+          b))))
+
+(defun compile-arg (arg bindings)
   "Generate code for an argument to a goal in the body."
-  (cond ((variable-p arg) arg)
+  (cond ((eql arg '?) '(?))
+        ((variable-p arg)
+         (let ((binding (get-binding arg bindings)))
+           (if (and (not (null binding))
+                    (not (eq arg (binding-value binding))))
+             (compile-arg (binding-value binding) bindings)
+             arg)))
         ((not (has-variable-p arg)) `',arg)
         ((proper-list-p arg)
-         `(list .,(mapcar #'compile-arg arg)))
-        (t `(cons ,(compile-arg (first arg))
-                  ,(compile-arg (rest arg))))))
+         `(list .,(mapcar #'(lambda (a) (compile-arg a bindings))
+                          arg)))
+        (t `(cons ,(compile-arg (first arg) bindings)
+                  ,(compile-arg (rest arg) bindings)))))
 
 (defun has-variable-p (x)
   "Is there a variable anywhere in the expression x?"
@@ -289,6 +367,7 @@
                 :collect '(undo-bindings! old-trail)
                 :collect expression)))))
 
+
 (defun bind-unbound-vars (parameters expr)
   "Bind any variables in expr (besides the parameters) to new vars."
   (let ((expr-vars (set-difference (variables-in expr) parameters)))
@@ -297,3 +376,98 @@
                      expr-vars)
          ,expr)
       expr)))
+
+
+(defmacro <- (&rest clause)
+  "Add a clause to the database."
+  `(add-clause ',(make-anonymous clause)))
+
+
+(defun make-anonymous (exp &optional (anon-vars (anonymous-variables-in exp)))
+  "Replace variables that are only used once with ?."
+  (cond ((consp exp)
+         (cons (make-anonymous (first exp) anon-vars)
+               (make-anonymous (rest exp) anon-vars)))
+        ((member exp anon-vars) '?)
+        (t exp)))
+
+(defun anonymous-variables-in (tree)
+  "Return a list of all variables that appear only once in tree."
+  (let ((seen-once nil)
+        (seen-more nil))
+    (labels ((walk (x)
+               (cond
+                 ((variable-p x)
+                  (cond ((member x seen-once)
+                         (setf seen-once (delete x seen-once))
+                         (push x seen-more))
+                        ((member x seen-more) nil)
+                        (t (push x seen-once))))
+                 ((consp x)
+                  (walk (first x))
+                  (walk (rest x))))))
+      (walk tree)
+      seen-once)))
+
+
+
+;;;; UI -----------------------------------------------------------------------
+(defvar *uncompiled* nil "Prolog symbols that have not been compiled.")
+
+(defun add-clause (clause)
+  "Add a clause to the database, indexed by the head's predicate."
+  (let ((pred (predicate (clause-head clause))))
+    (pushnew pred *db-predicates*)
+    (pushnew pred *uncompiled*)
+    (setf (get pred clause-key)
+          (nconc (get-clauses pred) (list clause)))
+    pred))
+
+
+(defun top-level-prove (goals)
+  "Prove the list of goals by compiling and calling it."
+  (clear-predicate 'top-level-query)
+  (let ((vars (delete '? (variables-in goals))))
+    (add-clause `((top-level-query)
+                  ,@goals
+                  (show-prolog-vars ,(mapcar #'symbol-name vars)
+                                    ,vars))))
+  (run-prolog 'top-level-query/0 #'ignorelol)
+  (format t "~&No.")
+  (values))
+
+(defun run-prolog (procedure continuation)
+  "Run an 0-ary Prolog prodecure with the given continuation."
+  (prolog-compile-symbols)
+  (setf (fill-pointer *trail*) 0)
+  (setf *var-counter* 0)
+  (catch 'top-level-prove
+         (funcall procedure continuation)))
+
+(defun prolog-compile-symbols (&optional (symbols *uncompiled*))
+  (mapc #'prolog-compile symbols)
+  (setf *uncompiled* (set-difference *uncompiled* symbols)))
+
+(defun ignorelol (&rest args)
+  (declare (ignore args))
+  nil)
+
+(defun show-prolog-vars/2 (var-names vars cont)
+  (if (null vars)
+    (format t "~&Yes")
+    (loop :for name :in var-names
+          :for var :in vars :do
+          (format t "~&~A = ~A" name (deref-exp var))))
+  (if (continue-ask)
+    (funcall cont)
+    (throw 'top-level-prove nil)))
+
+(defun deref-exp (exp)
+  (if (atom (deref exp))
+    exp
+    (cons (deref-exp (first exp))
+          (deref-exp (rest exp)))))
+
+
+(defmacro ?- (&rest goals)
+  `(top-level-prove ',(replace-wildcard-variables goals)))