# HG changeset patch
# User Steve Losh <steve@stevelosh.com>
# Date 1458657095 0
# Node ID 3a8ee0586fdfce67df0609f6398bb75626087cc6
# Parent  2daf5fb2fe92a7e495644eac87949b8ddb7219a2
Add destructive unification

Will be used in the PAIP compiler.

diff -r 2daf5fb2fe92 -r 3a8ee0586fdf bones.asd
--- a/bones.asd	Fri Mar 18 13:50:04 2016 +0000
+++ b/bones.asd	Tue Mar 22 14:31:35 2016 +0000
@@ -19,5 +19,6 @@
                (:file "package")
                (:module "src"
                 :components ((:file "paip")
+                             (:file "paip-compiled")
                              (:file "bones")))))
 
diff -r 2daf5fb2fe92 -r 3a8ee0586fdf docs/03-reference.markdown
--- a/docs/03-reference.markdown	Fri Mar 18 13:50:04 2016 +0000
+++ b/docs/03-reference.markdown	Tue Mar 22 14:31:35 2016 +0000
@@ -16,6 +16,12 @@
 
 Whether to perform an occurs check.
 
+### BOUND-P (function)
+
+    (BOUND-P VAR)
+
+Return whether the given variable has been bound.
+
 ### CLEAR-DB (function)
 
     (CLEAR-DB)
@@ -62,9 +68,23 @@
 
     (RULE &REST CLAUSE)
 
+### UNBOUND (variable)
+
+A magic constant representing an unbound variable.
+
 ### UNIFY (function)
 
     (UNIFY X Y &OPTIONAL (BINDINGS NO-BINDINGS))
 
 Unify the two terms and return bindings necessary to do so (or FAIL).
 
+### UNIFY! (function)
+
+    (UNIFY! X Y)
+
+Destructively unify two expressions.
+
+  Any variables in `x` and `y` may have their bindings set.
+
+  
+
diff -r 2daf5fb2fe92 -r 3a8ee0586fdf package.lisp
--- a/package.lisp	Fri Mar 18 13:50:04 2016 +0000
+++ b/package.lisp	Tue Mar 22 14:31:35 2016 +0000
@@ -12,6 +12,11 @@
    #:fail #:no-bindings
    #:*check-occurs*
 
+   ;; Destructive unification
+   #:unify!
+   #:unbound
+   #:bound-p
+
    ;; Database management
    #:clear-db
    #:fact
diff -r 2daf5fb2fe92 -r 3a8ee0586fdf src/paip-compiled.lisp
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/paip-compiled.lisp	Tue Mar 22 14:31:35 2016 +0000
@@ -0,0 +1,86 @@
+(in-package #:bones.paip)
+
+;;;; Variables
+(define-constant unbound "Unbound"
+  :test #'equal
+  :documentation "A magic constant representing an unbound variable.")
+
+(defvar *var-counter* 0
+  "The number of variables created so far.")
+
+(defstruct (var (:constructor ? ())
+                (:print-function print-var))
+  (name (incf *var-counter*)) ; The variable's name (defaults to a new number)
+  (binding unbound)) ; The variable's binding (defaults to unbound)
+
+(defun* print-var ((var var) stream depth)
+  (if (or (and (numberp *print-level*)
+               (>= depth *print-level*))
+          (var-p (deref var)))
+    (format stream "?~A" (var-name var))
+    (write var :stream stream)))
+
+(defun* bound-p ((var var))
+  (:returns boolean)
+  "Return whether the given variable has been bound."
+  (not (eq (var-binding var) unbound)))
+
+(defmacro deref (expr)
+  "Chase all the bindings for the given expression in place."
+  `(progn
+    (loop :while (and (var-p ,expr) (bound-p ,expr))
+          :do (setf ,expr (var-binding ,expr)))
+    ,expr))
+
+
+;;;; Bindings
+(defvar *trail* (make-array 200 :fill-pointer 0 :adjustable t)
+  "The trail of variable bindings performed so far.")
+
+(defun* set-binding! ((var var) value)
+  (:returns (eql t))
+  "Set `var`'s binding to `value` after saving it in the trail.
+
+  Always returns `t` (success).
+
+  "
+  (when (not (eq var value))
+    (vector-push-extend var *trail*)
+    (setf (var-binding var) value))
+  t)
+
+(defun* undo-bindings! ((old-trail integer))
+  (:returns :void)
+  "Undo all bindings back to a given point in the trail.
+
+  The point is specified by giving the desired fill pointer.
+
+  "
+  (loop :until (= (fill-pointer *trail*) old-trail)
+        :do (setf (var-binding (vector-pop *trail*)) unbound))
+  (values))
+
+
+;;;; Unification
+(defun* unify! (x y)
+  (:returns boolean)
+  "Destructively unify two expressions, returning whether it was successful.
+
+  Any variables in `x` and `y` may have their bindings set.
+
+  "
+  (cond
+    ;; If they're identical objects (taking bindings into account), they unify.
+    ((eql (deref x) (deref y)) t)
+
+    ;; If they're not identical, but one is a variable, bind it to the other.
+    ((var-p x) (set-binding! x y))
+    ((var-p y) (set-binding! y x))
+
+    ;; If they're both non-empty lists, unify the cars and cdrs.
+    ((and (consp x) (consp y))
+     (and (unify! (first x) (first y))
+          (unify! (rest x) (rest y))))
+
+    ;; Otherwise they don't unify.
+    (t nil)))