# HG changeset patch
# User Steve Losh <steve@stevelosh.com>
# Date 1457450867 0
# Node ID d08be78928164703a81ac4396074a6de4a28da0b
# Parent  b22eb7fe2faafdbad0d2ea8dfb9bb67617251f3a
Get some basic unification up and running

diff -r b22eb7fe2faa -r d08be7892816 Makefile
--- a/Makefile	Tue Mar 08 12:31:44 2016 +0000
+++ b/Makefile	Tue Mar 08 15:27:47 2016 +0000
@@ -5,6 +5,9 @@
 test:
 	sbcl --noinform --load test/run.lisp  --eval '(quit)'
 
+src/utils.lisp: src/make-utilities.lisp
+	cd src && sbcl --noinform --load make-utilities.lisp  --eval '(quit)'
+
 docs: docs/build/index.html
 
 docs/build/index.html: $(docfiles)
diff -r b22eb7fe2faa -r d08be7892816 bones.asd
--- a/bones.asd	Tue Mar 08 12:31:44 2016 +0000
+++ b/bones.asd	Tue Mar 08 15:27:47 2016 +0000
@@ -10,11 +10,13 @@
 
   :depends-on (#:defstar
                #:optima
+               #:trivial-types
                #:fare-quasiquote-optima
                #:fare-quasiquote-readtable)
 
   :serial t
-  :components ((:file "package")
+  :components ((:file "src/utils") ; quickutils package ordering crap
+               (:file "package")
                (:module "src"
                 :components ((:file "paip")
                              (:file "bones")))))
diff -r b22eb7fe2faa -r d08be7892816 package-test.lisp
--- a/package-test.lisp	Tue Mar 08 12:31:44 2016 +0000
+++ b/package-test.lisp	Tue Mar 08 15:27:47 2016 +0000
@@ -1,5 +1,11 @@
 (defpackage #:bones-test
-  (:use #:cl #:5am #:bones))
+  (:use #:cl #:5am
+        #:bones))
 
 (defpackage #:bones-test.paip
-  (:use #:cl #:5am #:bones.paip))
+  (:use #:cl #:5am
+        #:bones.utils
+        #:bones.paip)
+  (:import-from #:bones.paip)
+  ; kill me
+  (:shadowing-import-from #:5am #:fail))
diff -r b22eb7fe2faa -r d08be7892816 package.lisp
--- a/package.lisp	Tue Mar 08 12:31:44 2016 +0000
+++ b/package.lisp	Tue Mar 08 15:27:47 2016 +0000
@@ -3,6 +3,7 @@
   (:export #:hello))
 
 (defpackage #:bones.paip
-  (:use #:cl)
-  (:export #:foo))
+  (:use #:cl #:defstar #:bones.utils)
+  (:export #:unify
+           #:fail #:no-bindings))
 
diff -r b22eb7fe2faa -r d08be7892816 src/make-utilities.lisp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/make-utilities.lisp	Tue Mar 08 15:27:47 2016 +0000
@@ -0,0 +1,6 @@
+(ql:quickload 'quickutil)
+
+(qtlc:save-utils-as "utils.lisp"
+                    :utilities '(:define-constant
+                                 :set-equal)
+                    :package "BONES.UTILS")
diff -r b22eb7fe2faa -r d08be7892816 src/paip.lisp
--- a/src/paip.lisp	Tue Mar 08 12:31:44 2016 +0000
+++ b/src/paip.lisp	Tue Mar 08 15:27:47 2016 +0000
@@ -1,4 +1,153 @@
 (in-package #:bones.paip)
 
-(defun foo ()
-  1)
+;;;; Types
+(deftype logic-variable ()
+  'keyword)
+
+(deftype binding ()
+  '(cons logic-variable t))
+
+(deftype binding-list ()
+  '(trivial-types:association-list keyword t))
+
+
+;;;; Constants
+(define-constant fail nil
+  :documentation "Failure to unify")
+
+(define-constant no-bindings '((:bones-empty-bindings . t))
+  :test 'equal
+  :documentation "A succesful unification, with no bindings.")
+
+(defparameter *check-occurs* t
+  "Whether to perform an occurs check.")
+
+
+;;;; Unification
+(defun* variable-p (term)
+  (:returns boolean)
+  "Return whether the given term is a logic variable."
+  (keywordp term))
+
+(defun* get-binding ((variable logic-variable)
+                     (bindings binding-list))
+  (:returns (or binding null))
+  "Return the binding (var . val) for the given variable, or nil."
+  (assoc variable bindings))
+
+(defun* binding-variable ((binding binding))
+  (:returns logic-variable)
+  "Return the variable part of a binding."
+  (car binding))
+
+(defun* binding-value ((binding binding))
+  "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."
+  (binding-value (get-binding variable bindings)))
+
+(defun* extend-bindings ((variable logic-variable)
+                         (value t)
+                         (bindings binding-list))
+  (:returns binding-list)
+  "Add a binding (var . val) to the binding list (nondestructively)."
+  (cons (cons variable value)
+        (if (and (eq bindings no-bindings))
+          nil
+          bindings)))
+
+(defun* match-variable ((variable logic-variable)
+                        (input t)
+                        (bindings binding-list))
+  "Match the var with input, using (possibly updating) and returning bindings."
+  (let ((binding (get-binding variable bindings)))
+    (cond ((not binding)
+           (extend-bindings variable input bindings))
+          ((equal input (binding-value binding))
+           bindings)
+          (t fail))))
+
+(defun* check-occurs ((variable logic-variable)
+                      (target t)
+                      (bindings binding-list))
+  (:returns boolean)
+  "Check whether the variable occurs somewhere in the target.
+
+  Takes the bindings into account.  This is expensive.
+
+  "
+  (cond
+   ;; If the target is this variable, then yep.
+   ((eql variable target) t)
+
+   ;; The empty list doesn't contain anything.
+   ((null target) nil)
+
+   ;; The the target is a (different) variable that has a binding, we need to
+   ;; check if the variable occurs in its bindings.
+   ((and (variable-p target)
+         (get-binding target bindings))
+    (check-occurs variable (lookup target bindings) bindings))
+
+   ;; If the target is a list, check if any of the elements contain the variable.
+   ((listp target)
+    (or (check-occurs variable (first target) bindings)
+        (check-occurs variable (rest target) bindings)))
+
+   ;; Otherwise we're safe.
+   (t nil)))
+
+(defun unify (x y &optional (bindings no-bindings))
+  "Unify the two terms and return bindings necessary to do so (or FAIL)."
+  (flet ((unify-variable
+          (variable target bindings)
+          (cond
+           ;; If we've already got a binding for this variable, we can try to
+           ;; unify its value with the target.
+           ((get-binding variable bindings)
+            (unify (lookup variable bindings) target bindings))
+
+           ;; If the target is ALSO a variable, and it has a binding, then we
+           ;; can unify this variable with the target's value.
+           ((and (variable-p target) (get-binding target bindings))
+            (unify variable (lookup target bindings) bindings))
+
+           ;; If this variable occurs in the target (including in something
+           ;; in its bindings) and we're checking occurrence, bail.
+           ((and *check-occurs* (check-occurs variable target bindings))
+            fail)
+
+           ;; Otherwise we can just bind this variable to the target.
+           (t (extend-bindings variable target bindings)))))
+    (cond
+     ;; Pass failures through.
+     ((eq bindings fail) fail)
+
+     ;; Trying to unify two identical objects (constants or variables) can just
+     ;; return the bindings as-is.
+     ;;
+     ;; ex: (unify :y :y) or (unify 'foo 'foo)
+     ((eql x y) bindings)
+
+     ;; Unifying a variable with something.
+     ((variable-p x) (unify-variable x y bindings))
+     ((variable-p y) (unify-variable y x bindings))
+
+     ;; Unifying a non-variable with nil should fail, except for nil itself.
+     ;; But that was handled with (eql x y).
+     ((or (null x) (null y)) fail)
+
+     ;; Unifying non-empty compound terms such as
+     ;; (likes :x cats) with (likes sally :y).
+     ((and (listp x) (listp y))
+      (unify (rest x) (rest y) ; Unify the tails with the bindings gotten from...
+             (unify (first x) (first y) bindings))) ; unifying the heads.
+
+     ;; Otherwise we're looking at different constants, or a constant and a
+     ;; compound term, so just give up.
+     (t fail))))
+
+
diff -r b22eb7fe2faa -r d08be7892816 src/utils.lisp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/utils.lisp	Tue Mar 08 15:27:47 2016 +0000
@@ -0,0 +1,70 @@
+;;;; This file was automatically generated by Quickutil.
+;;;; See http://quickutil.org for details.
+
+;;;; To regenerate:
+;;;; (qtlc:save-utils-as "utils.lisp" :utilities '(:DEFINE-CONSTANT :SET-EQUAL) :ensure-package T :package "BONES.UTILS")
+
+(eval-when (:compile-toplevel :load-toplevel :execute)
+  (unless (find-package "BONES.UTILS")
+    (defpackage "BONES.UTILS"
+      (:documentation "Package that contains Quickutil utility functions.")
+      (:use #:cl))))
+
+(in-package "BONES.UTILS")
+
+(when (boundp '*utilities*)
+  (setf *utilities* (union *utilities* '(:DEFINE-CONSTANT :SET-EQUAL))))
+
+  (defun %reevaluate-constant (name value test)
+    (if (not (boundp name))
+        value
+        (let ((old (symbol-value name))
+              (new value))
+          (if (not (constantp name))
+              (prog1 new
+                (cerror "Try to redefine the variable as a constant."
+                        "~@<~S is an already bound non-constant variable ~
+                       whose value is ~S.~:@>" name old))
+              (if (funcall test old new)
+                  old
+                  (restart-case
+                      (error "~@<~S is an already defined constant whose value ~
+                              ~S is not equal to the provided initial value ~S ~
+                              under ~S.~:@>" name old new test)
+                    (ignore ()
+                      :report "Retain the current value."
+                      old)
+                    (continue ()
+                      :report "Try to redefine the constant."
+                      new)))))))
+
+  (defmacro define-constant (name initial-value &key (test ''eql) documentation)
+    "Ensures that the global variable named by `name` is a constant with a value
+that is equal under `test` to the result of evaluating `initial-value`. `test` is a
+function designator that defaults to `eql`. If `documentation` is given, it
+becomes the documentation string of the constant.
+
+Signals an error if `name` is already a bound non-constant variable.
+
+Signals an error if `name` is already a constant variable whose value is not
+equal under `test` to result of evaluating `initial-value`."
+    `(defconstant ,name (%reevaluate-constant ',name ,initial-value ,test)
+       ,@(when documentation `(,documentation))))
+  
+
+  (defun set-equal (list1 list2 &key (test #'eql) (key nil keyp))
+    "Returns true if every element of `list1` matches some element of `list2` and
+every element of `list2` matches some element of `list1`. Otherwise returns false."
+    (let ((keylist1 (if keyp (mapcar key list1) list1))
+          (keylist2 (if keyp (mapcar key list2) list2)))
+      (and (dolist (elt keylist1 t)
+             (or (member elt keylist2 :test test)
+                 (return nil)))
+           (dolist (elt keylist2 t)
+             (or (member elt keylist1 :test test)
+                 (return nil))))))
+  
+(eval-when (:compile-toplevel :load-toplevel :execute)
+  (export '(define-constant set-equal)))
+
+;;;; END OF utils.lisp ;;;;
diff -r b22eb7fe2faa -r d08be7892816 test/bones.lisp
--- a/test/bones.lisp	Tue Mar 08 12:31:44 2016 +0000
+++ b/test/bones.lisp	Tue Mar 08 15:27:47 2016 +0000
@@ -3,5 +3,3 @@
 (def-suite :bones)
 (in-suite :bones)
 
-(test hello-works
-  (is (equal 0 (1- (hello)))))
diff -r b22eb7fe2faa -r d08be7892816 test/paip.lisp
--- a/test/paip.lisp	Tue Mar 08 12:31:44 2016 +0000
+++ b/test/paip.lisp	Tue Mar 08 15:27:47 2016 +0000
@@ -3,5 +3,48 @@
 (def-suite :bones.paip)
 (in-suite :bones.paip)
 
-(test foo-works
-  (is (equal 0 (1- (foo)))))
+(defun alist-equal (x y)
+  (set-equal x y :test #'equal))
+
+(defmacro unifies (x y bindings)
+  `(is (alist-equal ,(if (eql bindings 'no-bindings)
+                       'no-bindings
+                       `',bindings)
+                    (unify ',x ',y))))
+
+(defmacro not-unifies (x y)
+  `(is (eql bones.paip:fail (unify ',x ',y))))
+
+(test constant-unification
+  (unifies 1 1 no-bindings)
+  (unifies foo foo no-bindings)
+  (unifies (a) (a) no-bindings)
+  (unifies (a b c) (a b c) no-bindings)
+  (not-unifies 1 2)
+  (not-unifies foo bar)
+  (not-unifies a (a))
+  (not-unifies (a) (a b))
+  (not-unifies () (a))
+  )
+
+(test variable-unification
+  (unifies :x 1 ((:x . 1)))
+  (unifies :x 2 ((:x . 2)))
+  (unifies :x a ((:x . a)))
+  (unifies :x :y ((:x . :y)))
+  (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))
+           (10 + (1 + 2))
+           ((:x . 10)
+            (:y . 1)
+            (:z . 2)))
+  )
+
+