--- 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)
--- 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")))))
--- 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))
--- 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))
--- /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")
--- 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))))
+
+
--- /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 ;;;;
--- 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)))))
--- 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)))
+ )
+
+