# HG changeset patch
# User Steve Losh <steve@stevelosh.com>
# Date 1457634176 0
# Node ID 5bb73a585f2ca63398827bfef4e0512b040f5d76
# Parent  1340243d4843c1879248e5e9035127e3a7a6f917
Finish basic proving

I gave up on making the renameless unification work because I'm just too dumb to
understand it.  Gonna throw this all away when I hit the WAM book anyhow, so
it's not worth wasting time on.  Maybe I'll come back to it later if I have
time.

diff -r 1340243d4843 -r 5bb73a585f2c package.lisp
--- a/package.lisp	Thu Mar 10 15:14:48 2016 +0000
+++ b/package.lisp	Thu Mar 10 18:22:56 2016 +0000
@@ -6,5 +6,8 @@
   (:use #:cl #:defstar #:bones.utils)
   (:export #:unify
            #:fail #:no-bindings
-           #:*check-occurs*))
+           #:*check-occurs*
+           #:clear-db
+           #:fact #:rule
+           #:find-all #:query))
 
diff -r 1340243d4843 -r 5bb73a585f2c src/paip.lisp
--- a/src/paip.lisp	Thu Mar 10 15:14:48 2016 +0000
+++ b/src/paip.lisp	Thu Mar 10 18:22:56 2016 +0000
@@ -2,7 +2,7 @@
 
 ;;;; Types
 (deftype logic-variable ()
-  'keyword)
+  'symbol)
 
 (deftype binding ()
   '(cons logic-variable t))
@@ -27,7 +27,10 @@
 (defun* variable-p (term)
   (:returns boolean)
   "Return whether the given term is a logic variable."
-  (keywordp term))
+  (and (symbolp term)
+       (equal (char (symbol-name term) 0)
+              #\?)))
+
 
 (defun* get-binding ((variable logic-variable)
                      (bindings binding-list))
@@ -35,6 +38,12 @@
   "Return the binding (var . val) for the given variable, or nil."
   (assoc variable bindings))
 
+(defun* has-binding ((variable logic-variable)
+                     (bindings binding-list))
+  (:returns boolean)
+  (not (null (get-binding variable bindings))))
+
+
 (defun* binding-variable ((binding binding))
   (:returns logic-variable)
   "Return the variable part of a binding."
@@ -44,6 +53,7 @@
   "Return the value part of a binding."
   (cdr binding))
 
+
 (defun* lookup ((variable logic-variable)
                 (bindings binding-list))
   "Return the value the given variable is bound to."
@@ -55,10 +65,11 @@
   (:returns binding-list)
   "Add a binding (var . val) to the binding list (nondestructively)."
   (cons (cons variable value)
-        (if (and (eq bindings no-bindings))
+        (if (and (equal bindings no-bindings))
           nil
           bindings)))
 
+
 (defun* check-occurs ((variable logic-variable)
                       (target t)
                       (bindings binding-list))
@@ -228,65 +239,97 @@
   (mapc #'clear-predicate *db-predicates*))
 
 
+(defun unique-find-anywhere-if (predicate tree &optional acc)
+  (if (atom tree)
+    (if (funcall predicate tree)
+      (adjoin tree acc)
+      acc)
+    (unique-find-anywhere-if predicate
+                             (first tree)
+                             (unique-find-anywhere-if predicate (rest tree) acc))))
+
+(defun variables-in (expr)
+  (unique-find-anywhere-if #'variable-p expr))
+
 (defun rename-variables (form)
   "Replace all variables in the form with new (unique) ones."
-  (sublis (mapcar #'(lambda (variable) (cons variable (gensym (string var))))
+  (sublis (mapcar #'(lambda (variable)
+                      (cons variable (gensym (string variable))))
                   (variables-in form))
           form))
 
+(defun prove-single-clause (goal bindings clause)
+  (let ((new-clause (rename-variables clause)))
+    (prove-all (clause-body new-clause)
+               (unify goal (clause-head new-clause) bindings))))
+
+(defun prove (goal bindings)
+  ;; We look up all the possible clauses for the goal and try proving
+  ;; each individually.  Each one will give us back a list of possible
+  ;; solutions.
+  ;;
+  ;; Then we concatenate the results to return all the possible
+  ;; solutions.
+  (mapcan (curry #'prove-single-clause goal bindings)
+          (get-clauses (predicate goal))))
+
 (defun prove-all (goals bindings)
   "Returns a list of solutions to the conjunction of goals."
-  ;; strap in, here we go.
-  (labels ((prove-single-clause
-            (goal clause bindings)
-            "Try to prove a goal against a single clause using the given bindings.
+  (cond
+   ;; If something failed further up the pipeline, bail here.
+   ((eq bindings fail) fail)
 
-            Return all possible solutions as a list of binding-lists.
+   ;; If there's nothing to prove, it's vacuously true.  Return a list of the
+   ;; bindings as the result.
+   ((null goals) (list bindings))
 
-            "
-            ;; Try to prove a goal against a specific clause:
-            ;;
-            ;;     (likes sally kim)
-            ;;     ((likes sally :x) (likes :x cats))
-            ;;
-            ;; To do this, we try to unify the goal with the head of the clause,
-            ;; and then use the resulting bindings to prove the rest of the
-            ;; items in the clause.
-            ;;
-            ;; First rename the variables in the clause, because they stand on
-            ;; their own and shouldn't be confused with ones in the bindings.
-            (let ((new-clause (rename-variables clause)))
-              (prove-all (clause-body new-clause)
-                         (unify goal (clause-head new-clause) bindings))))
-           (prove
-            (goal bindings)
-            "Try to prove a goal, using the given bindings.
+   ;; Otherwise we try to prove the first thing in the list.  This gives us
+   ;; back a list of possible bindings we could use.
+   ;;
+   ;; For each possible solution to the head, we try using it to prove the
+   ;; rest of the goals and concatenate all the results.  Failed attempts are
+   ;; represented as FAIL which is nil, so will collapse in the concatenation.
+   (t (mapcan #'(lambda (possible-solution)
+                 (prove-all (rest goals) possible-solution))
+              (prove (first goals) bindings)))))
+
+(defun show-variables (variables solution)
+  (if (null variables)
+    (format t "~&Yes")
+    (dolist (var variables)
+      (format t "~&~A = ~A"
+              var (substitute-bindings solution var))))
+  (princ ";"))
 
-            Return all possible solutions as a list of binding-lists.
+(defun clean-variables (variables solution)
+  (mapcar #'(lambda (var)
+             (cons var (substitute-bindings solution var)))
+    variables))
 
-            "
-            ;; We look up all the possible clauses for the goal and try proving
-            ;; each individually.  Each one will give us back a list of possible
-            ;; solutions.
-            ;;
-            ;; Then we concatenate the results to return all the possible
-            ;; solutions.
-            (mapcan #'prove-single-clause (get-clauses (predicate goal)))))
-    (cond
-     ;; If something failed further up the pipeline, bail here.
-     ((eq bindings fail) fail)
+(defun show-solutions (variables solutions)
+  (if (null solutions)
+    (format t "~&No.")
+    (mapc (curry #'show-variables variables)
+          solutions))
+  (values))
+
+(defun clean-solutions (variables solutions)
+  (mapcar (curry #'clean-variables variables)
+          solutions))
 
-     ;; If there's nothing to prove, it's vacuously true.  Return a list of the
-     ;; bindings as the result.
-     ((null goals) (list bindings))
+(defun top-level-prove (goals)
+  (show-solutions
+    (variables-in goals)
+    (prove-all goals no-bindings)))
 
-     ;; Otherwise we try to prove the first thing in the list.  This gives us
-     ;; back a list of possible bindings we could use.
-     ;;
-     ;; For each possible solution to the head, we try using it to prove the
-     ;; rest of the goals and concatenate all the results.  Failed attempts are
-     ;; represented as FAIL which is nil, so will collapse in the concatenation.
-     (t (mapcan #'(lambda (possible-solution)
-                   (prove-all (rest goals) possible-solution))
-                (prove (first goals) bindings))))))
+(defun top-level-find (goals)
+  (clean-solutions
+    (variables-in goals)
+    (prove-all goals no-bindings)))
 
+(defmacro query (&rest goals)
+  `(top-level-prove ',goals))
+
+(defmacro find-all (&rest goals)
+  `(top-level-find ',goals))
+
diff -r 1340243d4843 -r 5bb73a585f2c test/paip.lisp
--- a/test/paip.lisp	Thu Mar 10 15:14:48 2016 +0000
+++ b/test/paip.lisp	Thu Mar 10 18:22:56 2016 +0000
@@ -17,6 +17,24 @@
   `(is (eql bones.paip:fail (unify ',x ',y))))
 
 
+(defmacro with-db (rules &rest body)
+  `(progn
+     (clear-db)
+     ,@(mapcar #'(lambda (rule) `(rule ,@rule))
+               rules)
+     ,@body))
+
+
+(defmacro proves (query)
+  `(is-true (find-all ,query)))
+
+(defmacro not-proves (query)
+  `(is-false (find-all ,query)))
+
+(defmacro proves-with (query results)
+  `(is (set-equal ',results (find-all ,query)
+                  :test #'alist-equal)))
+
 ;;;; Unification
 (test constant-unification
   (unifies 1 1 no-bindings)
@@ -30,33 +48,81 @@
   (not-unifies () (a)))
 
 (test variable-unification
-  (unifies :x 1 ((:x . 1)))
-  (unifies :x a ((:x . a)))
-  (unifies :x :y ((:x . :y)))
-  (unifies (:x (f :x)) (2 (f 2)) ((:x . 2)))
-  (unifies (likes sally :thing)
-           (likes :person cats)
-           ((:thing . cats)
-            (:person . sally)))
-  (unifies (:x + :y)
+  (unifies ?x 1 ((?x . 1)))
+  (unifies ?x a ((?x . a)))
+  (unifies ?x ?y ((?x . ?y)))
+  (unifies (?x (f ?x)) (2 (f 2)) ((?x . 2)))
+  (unifies (likes sally ?thing)
+           (likes ?person cats)
+           ((?thing . cats)
+            (?person . sally)))
+  (unifies (?x + ?y)
            (10 + (1 + 2))
-           ((:x . 10)
-            (:y . (1 + 2))))
-  (unifies (:x + (:y + :z))
+           ((?x . 10)
+            (?y . (1 + 2))))
+  (unifies (?x + (?y + ?z))
            (10 + (1 + 2))
-           ((:x . 10)
-            (:y . 1)
-            (:z . 2)))
-  (not-unifies (:x :x) (1 2))
-  (not-unifies (:x :y :x) (1 1 3)))
+           ((?x . 10)
+            (?y . 1)
+            (?z . 2)))
+  (not-unifies (?x ?x) (1 2))
+  (not-unifies (?x ?y ?x) (1 1 3)))
 
 (test occurs-unification
-  (not-unifies :x (f :x))
-  (not-unifies :x (f (:x 1)))
-  (not-unifies :x (:x :x))
-  (not-unifies :x (:x :y))
+  (not-unifies ?x (f ?x))
+  (not-unifies ?x (f (?x 1)))
+  (not-unifies ?x (?x ?x))
+  (not-unifies ?x (?x ?y))
   (let ((*check-occurs* nil))
-    (unifies :x (f :x)     ((:x . (f :x))))
-    (unifies :x (f (:x 1)) ((:x . (f (:x 1)))))
-    (unifies :x (:x :x)    ((:x . (:x :x))))
-    (unifies :x (:x :y)    ((:x . (:x :y))))))
+    (unifies ?x (f ?x)     ((?x . (f ?x))))
+    (unifies ?x (f (?x 1)) ((?x . (f (?x 1)))))
+    (unifies ?x (?x ?x)    ((?x . (?x ?x))))
+    (unifies ?x (?x ?y)    ((?x . (?x ?y))))))
+
+
+;;;; Basic Proving
+(test prove-facts
+  (with-db (((likes kim cats))
+            ((likes tom cats)))
+    (proves (likes kim cats))
+    (proves (likes tom cats))
+    (not-proves (likes kim tom))
+    (not-proves (likes kim))))
+
+(test prove-rules-simple
+  (with-db (((likes kim cats))
+            ((likes sally ?x) (likes ?x cats)))
+    (proves (likes sally kim))
+    (not-proves (likes sally sally))))
+
+(test prove-member
+  (with-db (((member ?x (?x . ?tail)))
+            ((member ?x (?y . ?tail)) (member ?x ?tail)))
+    (proves (member 1 (1 2)))
+    (proves (member 2 (1 2)))
+    (proves (member (x) (1 (x) 2)))
+    (not-proves (member 1 ()))
+    (not-proves (member ?x ()))
+    (not-proves (member 1 (a b c)))
+    (proves-with (member ?x (1 2 3))
+                 (((?x . 1))
+                  ((?x . 2))
+                  ((?x . 3))))
+    (proves-with (member ?x (1 1 1))
+                 (((?x . 1))))
+    (proves-with (member (?x ?y) ((a b) (c d) 1))
+                 (((?x . a) (?y . b))
+                  ((?x . c) (?y . d))))))
+
+(test prove-last
+  (with-db (((last ?x (?x)))
+            ((last ?x (?y . ?tail)) (last ?x ?tail)))
+    (proves (last 1 (1)))
+    (proves (last 2 (1 2)))
+    (not-proves (last 1 ()))
+    (not-proves (last 1 ((1))))
+    (not-proves (last 1 (1 2)))
+    (proves-with (last ?x (1 2 3))
+                 (((?x . 3))))
+    (proves-with (last ?x (1 (2 3)))
+                 (((?x . (2 3)))))))