# HG changeset patch
# User Steve Losh <steve@stevelosh.com>
# Date 1467759753 0
# Node ID 410acaae0c1434ccdfdf55482aea0ded81b8a36b
# Parent  6a93a2d2ed609427d34b52c7744203d2ef07a37e
Implement logic frames for assertion/retraction

diff -r 6a93a2d2ed60 -r 410acaae0c14 .lispwords
--- a/.lispwords	Tue Jul 05 16:53:58 2016 +0000
+++ b/.lispwords	Tue Jul 05 23:02:33 2016 +0000
@@ -7,3 +7,4 @@
 (1 recursively)
 (1 when-let)
 (1 rule)
+(0 push-logic-frame-with)
diff -r 6a93a2d2ed60 -r 410acaae0c14 examples/bench.lisp
--- a/examples/bench.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/examples/bench.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -22,11 +22,11 @@
   ; (format t "PAIP (Compiled) --------------------~%")
   ; (time (paiprolog-test::dfs-exhaust))
 
-  ; (format t "PAIP (Interpreted) -----------------~%")
-  ; (time (bones.paip::dfs-exhaust))
+  (format t "PAIP (Interpreted) -----------------~%")
+  (time (bones.paip::depth-first-search :exhaust t))
 
   (format t "WAM --------------------------------~%")
-  (time (bones.wam::dfs-exhaust)))
+  (time (bones.wam::depth-first-search :exhaust t)))
 
 (defmacro run-test (&rest settings)
   `(progn
diff -r 6a93a2d2ed60 -r 410acaae0c14 examples/ggp-paip-interpreted.lisp
--- a/examples/ggp-paip-interpreted.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/examples/ggp-paip-interpreted.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -1,17 +1,61 @@
 (in-package #:bones.paip)
 
+;;;; Queues
+(deftype queue () '(cons list list))
+(declaim (inline queue-contents make-queue
+                 enqueue dequeue
+                 queue-empty-p queue-append))
+
+
+(defun* queue-contents ((q queue))
+  (:returns list)
+  (cdr q))
+
+(defun* make-queue ()
+  (:returns queue)
+  (let ((q (cons nil nil)))
+    (setf (car q) q)))
+
+(defun* enqueue ((item t) (q queue))
+  (:returns queue)
+  (setf (car q)
+        (setf (rest (car q))
+              (cons item nil)))
+  q)
+
+(defun* dequeue ((q queue))
+  (:returns t)
+  (prog1
+      (pop (cdr q))
+    (if (null (cdr q))
+      (setf (car q) q))))
+
+(defun* queue-empty-p ((q queue))
+  (:returns boolean)
+  (null (queue-contents q)))
+
+(defun* queue-append ((q queue) (l list))
+  (:returns queue)
+  (when l
+    (setf (car q)
+          (last (setf (rest (car q))
+                      l))))
+  q)
+
+
+;;;; Rules
 (clear-db)
 
 (rule (member ?thing (cons ?thing ?rest)))
 
 (rule (member ?thing (cons ?other ?rest))
-      (member ?thing ?rest))
+  (member ?thing ?rest))
 
 (rule (true ?state ?thing)
-      (member ?thing ?state))
+  (member ?thing ?state))
 
 (rule (does ?performed ?role ?move)
-      (member (does ?role ?move) ?performed))
+  (member (does ?role ?move) ?performed))
 
 (rule (role robot))
 
@@ -22,111 +66,111 @@
 (rule (init (step num1)))
 
 (rule (next ?state ?performed (on p))
-      (does ?performed robot a)
-      (true ?state (off p)))
+  (does ?performed robot a)
+  (true ?state (off p)))
 (rule (next ?state ?performed (on q))
-      (does ?performed robot a)
-      (true ?state (on q)))
+  (does ?performed robot a)
+  (true ?state (on q)))
 (rule (next ?state ?performed (on r))
-      (does ?performed robot a)
-      (true ?state (on r)))
+  (does ?performed robot a)
+  (true ?state (on r)))
 (rule (next ?state ?performed (off p))
-      (does ?performed robot a)
-      (true ?state (on p)))
+  (does ?performed robot a)
+  (true ?state (on p)))
 (rule (next ?state ?performed (off q))
-      (does ?performed robot a)
-      (true ?state (off q)))
+  (does ?performed robot a)
+  (true ?state (off q)))
 (rule (next ?state ?performed (off r))
-      (does ?performed robot a)
-      (true ?state (off r)))
+  (does ?performed robot a)
+  (true ?state (off r)))
 
 (rule (next ?state ?performed (on p))
-      (does ?performed robot b)
-      (true ?state (on q)))
+  (does ?performed robot b)
+  (true ?state (on q)))
 (rule (next ?state ?performed (on q))
-      (does ?performed robot b)
-      (true ?state (on p)))
+  (does ?performed robot b)
+  (true ?state (on p)))
 (rule (next ?state ?performed (on r))
-      (does ?performed robot b)
-      (true ?state (on r)))
+  (does ?performed robot b)
+  (true ?state (on r)))
 (rule (next ?state ?performed (off p))
-      (does ?performed robot b)
-      (true ?state (off q)))
+  (does ?performed robot b)
+  (true ?state (off q)))
 (rule (next ?state ?performed (off q))
-      (does ?performed robot b)
-      (true ?state (off p)))
+  (does ?performed robot b)
+  (true ?state (off p)))
 (rule (next ?state ?performed (off r))
-      (does ?performed robot b)
-      (true ?state (off r)))
+  (does ?performed robot b)
+  (true ?state (off r)))
 
 (rule (next ?state ?performed (on p))
-      (does ?performed robot c)
-      (true ?state (on p)))
+  (does ?performed robot c)
+  (true ?state (on p)))
 (rule (next ?state ?performed (on q))
-      (does ?performed robot c)
-      (true ?state (on r)))
+  (does ?performed robot c)
+  (true ?state (on r)))
 (rule (next ?state ?performed (on r))
-      (does ?performed robot c)
-      (true ?state (on q)))
+  (does ?performed robot c)
+  (true ?state (on q)))
 (rule (next ?state ?performed (off p))
-      (does ?performed robot c)
-      (true ?state (off p)))
+  (does ?performed robot c)
+  (true ?state (off p)))
 (rule (next ?state ?performed (off q))
-      (does ?performed robot c)
-      (true ?state (off r)))
+  (does ?performed robot c)
+  (true ?state (off r)))
 (rule (next ?state ?performed (off r))
-      (does ?performed robot c)
-      (true ?state (off q)))
+  (does ?performed robot c)
+  (true ?state (off q)))
 
 (rule (next ?state ?performed (off s))
-      (does ?performed robot a)
-      (true ?state (off s)))
+  (does ?performed robot a)
+  (true ?state (off s)))
 (rule (next ?state ?performed (off s))
-      (does ?performed robot b)
-      (true ?state (off s)))
+  (does ?performed robot b)
+  (true ?state (off s)))
 (rule (next ?state ?performed (off s))
-      (does ?performed robot c)
-      (true ?state (off s)))
+  (does ?performed robot c)
+  (true ?state (off s)))
 (rule (next ?state ?performed (on s))
-      (does ?performed robot a)
-      (true ?state (on s)))
+  (does ?performed robot a)
+  (true ?state (on s)))
 (rule (next ?state ?performed (on s))
-      (does ?performed robot b)
-      (true ?state (on s)))
+  (does ?performed robot b)
+  (true ?state (on s)))
 (rule (next ?state ?performed (on s))
-      (does ?performed robot c)
-      (true ?state (on s)))
+  (does ?performed robot c)
+  (true ?state (on s)))
 (rule (next ?state ?performed (off s))
-      (does ?performed robot d)
-      (true ?state (on s)))
+  (does ?performed robot d)
+  (true ?state (on s)))
 (rule (next ?state ?performed (on s))
-      (does ?performed robot d)
-      (true ?state (off s)))
+  (does ?performed robot d)
+  (true ?state (off s)))
 
 (rule (next ?state ?performed (on p))
-      (does ?performed robot d)
-      (true ?state (on p)))
+  (does ?performed robot d)
+  (true ?state (on p)))
 (rule (next ?state ?performed (off p))
-      (does ?performed robot d)
-      (true ?state (off p)))
+  (does ?performed robot d)
+  (true ?state (off p)))
 
 (rule (next ?state ?performed (on q))
-      (does ?performed robot d)
-      (true ?state (on q)))
+  (does ?performed robot d)
+  (true ?state (on q)))
 (rule (next ?state ?performed (off q))
-      (does ?performed robot d)
-      (true ?state (off q)))
+  (does ?performed robot d)
+  (true ?state (off q)))
 
 (rule (next ?state ?performed (on r))
-      (does ?performed robot d)
-      (true ?state (on r)))
+  (does ?performed robot d)
+  (true ?state (on r)))
 (rule (next ?state ?performed (off r))
-      (does ?performed robot d)
-      (true ?state (off r)))
+  (does ?performed robot d)
+  (true ?state (off r)))
 
 (rule (next ?state ?performed (step ?y))
-      (true ?state (step ?x))
-      (succ ?x ?y))
+  (true ?state (step ?x))
+  (succ ?x ?y))
 
 (rule (succ num1 num2))
 (rule (succ num2 num3))
@@ -142,26 +186,26 @@
 (rule (legal robot d))
 
 (rule (goal ?state robot num100)
-      (true ?state (on p))
-      (true ?state (on q))
-      (true ?state (on r))
-      (true ?state (on s)))
+  (true ?state (on p))
+  (true ?state (on q))
+  (true ?state (on r))
+  (true ?state (on s)))
 (rule (goal ?state robot num0)
-      (true ?state (off p)))
+  (true ?state (off p)))
 (rule (goal ?state robot num0)
-      (true ?state (off q)))
+  (true ?state (off q)))
 (rule (goal ?state robot num0)
-      (true ?state (off r)))
+  (true ?state (off r)))
 (rule (goal ?state robot num0)
-      (true ?state (off s)))
+  (true ?state (off s)))
 
 (rule (terminal ?state)
-      (true ?state (step num8)))
+  (true ?state (step num8)))
 (rule (terminal ?state)
-      (true ?state (on p))
-      (true ?state (on q))
-      (true ?state (on r))
-      (true ?state (on s)))
+  (true ?state (on p))
+  (true ?state (on q))
+  (true ?state (on r))
+  (true ?state (on s)))
 
 
 (defvar *count* 0)
@@ -182,9 +226,21 @@
 (defun terminalp (state)
   (raw-provable-p `(terminal ,state)))
 
+
+(defun equiv-roles (move1 move2)
+  (eq (car move1) (car move2)))
+
 (defun legal-moves (state)
   (declare (ignore state))
-  (return-all (legal ?role ?move)))
+  (let* ((individual-moves
+           (loop :for move :in (return-all (legal ?role ?action))
+                 :collect (cons (cdr (assoc '?role move))
+                                (cdr (assoc '?action move)))))
+         (joint-moves
+           (apply #'map-product #'list
+                  (equivalence-classes #'equiv-roles individual-moves))))
+    joint-moves))
+
 
 (defun roles ()
   (extract '?role (return-all (role ?role))))
@@ -196,79 +252,34 @@
 (defun goal-values (state)
   (raw-return-all `(goal ,state ?role ?goal)))
 
-(defun next-state (current-state move)
-  (let ((does (to-fake-list `((does
-                                ,(cdr (assoc '?role move))
-                                ,(cdr (assoc '?move move)))))))
+(defun next-state (current-state joint-move)
+  (let ((does (to-fake-list
+                (loop :for (role . action) :in joint-move
+                      :collect `(does ,role ,action)))))
     (to-fake-list
       (extract
         '?what
         (raw-return-all `(next ,current-state ,does ?what))))))
 
 
-(defstruct search-path state (path nil) (previous nil))
-
-(defun tree-search (states goal-p children combine)
-  (labels
-      ((recur (states)
-         (if (null states)
-           nil
-           (destructuring-bind (state . remaining) states
-             (incf *count*)
-             ; (format t "Searching: ~S (~D remaining)~%" state (length remaining))
-             (if (funcall goal-p state)
-               state
-               (recur (funcall combine
-                               (funcall children state)
-                               remaining)))))))
-    (let ((result (recur states)))
-      (when result
-        (reverse (search-path-path result))))))
-
-
-(defun buttons-goal-p (search-path)
-  (let ((state (search-path-state search-path)))
-    (and (terminalp state)
-         (eql (goal-value state 'robot) 'num100))))
+(defun depth-first-search (&key exhaust)
+  (let ((*count* 0)
+        (nodes (make-queue)))
+    (enqueue (cons (initial-state) nil) nodes)
+    (pprint
+      (while (not (queue-empty-p nodes))
+        (incf *count*)
+        (destructuring-bind (state . path)
+            (dequeue nodes)
+          ; (format t "Searching: ~S (~D remaining)~%" state (length remaining))
+          (if (and (not exhaust)
+                   (eql 'num100 (goal-value state 'robot)))
+            (return (list state (reverse path)))
+            (let ((children
+                    (when (not (terminalp state))
+                      (loop :for joint-move :in (legal-moves state)
+                            :collect (cons (next-state state joint-move)
+                                           (cons joint-move path))))))
+              (queue-append nodes children))))))
+    (format t "~%Searched ~D nodes.~%" *count*)))
 
-(defun buttons-children (search-path)
-  (let ((state (search-path-state search-path))
-        (path (search-path-path search-path)))
-    (when (not (terminalp state))
-      (loop :for move :in (legal-moves state)
-            :collect (make-search-path :state (next-state state move)
-                                       :path (cons move path)
-                                       :previous search-path)))))
-
-(defun never (&rest args)
-  (declare (ignore args))
-  nil)
-
-(defun dfs ()
-  (tree-search (list (make-search-path :state (initial-state)))
-               #'buttons-goal-p
-               #'buttons-children
-               #'append))
-
-(defun dfs-exhaust ()
-  (let ((*count* 0))
-    (prog1
-        (tree-search (list (make-search-path :state (initial-state)))
-                     #'never
-                     #'buttons-children
-                     #'append)
-        (format t "Searched ~D nodes.~%" *count*))))
-
-(defun bfs ()
-  (tree-search (list (make-search-path :state (initial-state)))
-               #'buttons-goal-p
-               #'buttons-children
-               (lambda (x y)
-                 (append y x))))
-
-; (sb-sprof:with-profiling
-;     (:report :flat
-;      :sample-interval 0.001
-;      :loop nil)
-;   (dfs-exhaust)
-;   )
diff -r 6a93a2d2ed60 -r 410acaae0c14 examples/ggp-wam.lisp
--- a/examples/ggp-wam.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/examples/ggp-wam.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -1,284 +1,256 @@
 (in-package #:bones.wam)
 
-(defparameter *d* (make-database))
+;;;; Rules
+(setf *database* (make-database))
+
+(push-logic-frame)
+
+(fact (role robot))
 
-(with-database *d*
-  (rules ((member ?thing (list* ?thing ?rest)))
-         ((member ?thing (list* ?other ?rest))
-          (member ?thing ?rest)))
+(facts (init (off p))
+       (init (off q))
+       (init (off r))
+       (init (off s))
+       (init (step num1)))
 
-  (rule (true ?state ?thing)
-        (member ?thing ?state))
 
-  (rule (does ?performed ?role ?move)
-        (member (does ?role ?move) ?performed))
-
-  (fact (role robot))
-
-  (facts (init (off p))
-         (init (off q))
-         (init (off r))
-         (init (off s))
-         (init (step num1))))
+(rule (next (on p))
+  (does robot a)
+  (true (off p)))
+(rule (next (on q))
+  (does robot a)
+  (true (on q)))
+(rule (next (on r))
+  (does robot a)
+  (true (on r)))
+(rule (next (off p))
+  (does robot a)
+  (true (on p)))
+(rule (next (off q))
+  (does robot a)
+  (true (off q)))
+(rule (next (off r))
+  (does robot a)
+  (true (off r)))
 
-(with-database *d*
-  (rules ((next ?state ?performed (on p))
-          (does ?performed robot a)
-          (true ?state (off p)))
-         ((next ?state ?performed (on q))
-          (does ?performed robot a)
-          (true ?state (on q)))
-         ((next ?state ?performed (on r))
-          (does ?performed robot a)
-          (true ?state (on r)))
-         ((next ?state ?performed (off p))
-          (does ?performed robot a)
-          (true ?state (on p)))
-         ((next ?state ?performed (off q))
-          (does ?performed robot a)
-          (true ?state (off q)))
-         ((next ?state ?performed (off r))
-          (does ?performed robot a)
-          (true ?state (off r)))
+(rule (next (on p))
+  (does robot b)
+  (true (on q)))
+(rule (next (on q))
+  (does robot b)
+  (true (on p)))
+(rule (next (on r))
+  (does robot b)
+  (true (on r)))
+(rule (next (off p))
+  (does robot b)
+  (true (off q)))
+(rule (next (off q))
+  (does robot b)
+  (true (off p)))
+(rule (next (off r))
+  (does robot b)
+  (true (off r)))
 
-         ((next ?state ?performed (on p))
-          (does ?performed robot b)
-          (true ?state (on q)))
-         ((next ?state ?performed (on q))
-          (does ?performed robot b)
-          (true ?state (on p)))
-         ((next ?state ?performed (on r))
-          (does ?performed robot b)
-          (true ?state (on r)))
-         ((next ?state ?performed (off p))
-          (does ?performed robot b)
-          (true ?state (off q)))
-         ((next ?state ?performed (off q))
-          (does ?performed robot b)
-          (true ?state (off p)))
-         ((next ?state ?performed (off r))
-          (does ?performed robot b)
-          (true ?state (off r)))
-
-         ((next ?state ?performed (on p))
-          (does ?performed robot c)
-          (true ?state (on p)))
-         ((next ?state ?performed (on q))
-          (does ?performed robot c)
-          (true ?state (on r)))
-         ((next ?state ?performed (on r))
-          (does ?performed robot c)
-          (true ?state (on q)))
-         ((next ?state ?performed (off p))
-          (does ?performed robot c)
-          (true ?state (off p)))
-         ((next ?state ?performed (off q))
-          (does ?performed robot c)
-          (true ?state (off r)))
-         ((next ?state ?performed (off r))
-          (does ?performed robot c)
-          (true ?state (off q)))
+(rule (next (on p))
+  (does robot c)
+  (true (on p)))
+(rule (next (on q))
+  (does robot c)
+  (true (on r)))
+(rule (next (on r))
+  (does robot c)
+  (true (on q)))
+(rule (next (off p))
+  (does robot c)
+  (true (off p)))
+(rule (next (off q))
+  (does robot c)
+  (true (off r)))
+(rule (next (off r))
+  (does robot c)
+  (true (off q)))
 
-         ((next ?state ?performed (off s))
-          (does ?performed robot a)
-          (true ?state (off s)))
-         ((next ?state ?performed (off s))
-          (does ?performed robot b)
-          (true ?state (off s)))
-         ((next ?state ?performed (off s))
-          (does ?performed robot c)
-          (true ?state (off s)))
-         ((next ?state ?performed (on s))
-          (does ?performed robot a)
-          (true ?state (on s)))
-         ((next ?state ?performed (on s))
-          (does ?performed robot b)
-          (true ?state (on s)))
-         ((next ?state ?performed (on s))
-          (does ?performed robot c)
-          (true ?state (on s)))
-         ((next ?state ?performed (off s))
-          (does ?performed robot d)
-          (true ?state (on s)))
-         ((next ?state ?performed (on s))
-          (does ?performed robot d)
-          (true ?state (off s)))
+(rule (next (off s))
+  (does robot a)
+  (true (off s)))
+(rule (next (off s))
+  (does robot b)
+  (true (off s)))
+(rule (next (off s))
+  (does robot c)
+  (true (off s)))
+(rule (next (on s))
+  (does robot a)
+  (true (on s)))
+(rule (next (on s))
+  (does robot b)
+  (true (on s)))
+(rule (next (on s))
+  (does robot c)
+  (true (on s)))
+(rule (next (off s))
+  (does robot d)
+  (true (on s)))
+(rule (next (on s))
+  (does robot d)
+  (true (off s)))
 
-         ((next ?state ?performed (on p))
-          (does ?performed robot d)
-          (true ?state (on p)))
-         ((next ?state ?performed (off p))
-          (does ?performed robot d)
-          (true ?state (off p)))
+(rule (next (on p))
+  (does robot d)
+  (true (on p)))
+(rule (next (off p))
+  (does robot d)
+  (true (off p)))
 
-         ((next ?state ?performed (on q))
-          (does ?performed robot d)
-          (true ?state (on q)))
-         ((next ?state ?performed (off q))
-          (does ?performed robot d)
-          (true ?state (off q)))
+(rule (next (on q))
+  (does robot d)
+  (true (on q)))
+(rule (next (off q))
+  (does robot d)
+  (true (off q)))
 
-         ((next ?state ?performed (on r))
-          (does ?performed robot d)
-          (true ?state (on r)))
-         ((next ?state ?performed (off r))
-          (does ?performed robot d)
-          (true ?state (off r)))
+(rule (next (on r))
+  (does robot d)
+  (true (on r)))
+(rule (next (off r))
+  (does robot d)
+  (true (off r)))
 
-         ((next ?state ?performed (step ?y))
-          (true ?state (step ?x))
-          (succ ?x ?y))))
+(rule (next (step ?y))
+  (true (step ?x))
+  (succ ?x ?y))
+
 
-(with-database *d*
-  (facts (succ num1 num2)
-         (succ num2 num3)
-         (succ num3 num4)
-         (succ num4 num5)
-         (succ num5 num6)
-         (succ num6 num7)
-         (succ num7 num8))
+(facts (succ num1 num2)
+       (succ num2 num3)
+       (succ num3 num4)
+       (succ num4 num5)
+       (succ num5 num6)
+       (succ num6 num7)
+       (succ num7 num8))
 
-  (facts (legal robot a)
-         (legal robot b)
-         (legal robot c)
-         (legal robot d)))
+(facts (legal robot a)
+       (legal robot b)
+       (legal robot c)
+       (legal robot d))
 
-(with-database *d*
-  (rules ((goal ?state robot num100)
-          (true ?state (on p))
-          (true ?state (on q))
-          (true ?state (on r))
-          (true ?state (on s))
-          )
-         ((goal ?state robot num0)
-          (true ?state (off p)))
-         ((goal ?state robot num0)
-          (true ?state (off q)))
-         ((goal ?state robot num0)
-          (true ?state (off r)))
-         ((goal ?state robot num0)
-          (true ?state (off s)))
-         )
 
-  (rules ((terminal ?state)
-          (true ?state (step num8)))
-         ((terminal ?state)
-          (true ?state (on p))
-          (true ?state (on q))
-          (true ?state (on r))
-          (true ?state (on s))
-          )))
+(rule (goal robot num100)
+  (true (on p))
+  (true (on q))
+  (true (on r))
+  (true (on s)))
+(rule (goal robot num0)
+  (true (off p)))
+(rule (goal robot num0)
+  (true (off q)))
+(rule (goal robot num0)
+  (true (off r)))
+(rule (goal robot num0)
+  (true (off s)))
+
+
+(rule (terminal)
+  (true (step num8)))
+(rule (terminal)
+  (true (on p))
+  (true (on q))
+  (true (on r))
+  (true (on s)))
+
+(finalize-logic-frame)
 
 
 (defun extract (key results)
   (mapcar (lambda (result) (getf result key)) results))
 
-(defun to-prolog-list (l)
-  (if (null l)
-    nil
-    (list* 'list l)))
 
 (defun initial-state ()
-  (to-prolog-list
-    (with-database *d*
-      (extract '?what (return-all (init ?what))))))
+  (extract '?what (return-all (init ?what))))
+
+(defun terminalp ()
+  (prove (terminal)))
+
+
+(defun equiv-roles (move1 move2)
+  (eq (car move1) (car move2)))
 
-(defun terminalp (state)
-  (with-database *d*
-    (perform-prove `((terminal ,state)))))
-
-(defun legal-moves (state)
-  (declare (ignore state))
-  (with-database *d*
-    (return-all (legal ?role ?move))))
+(defun legal-moves ()
+  (let* ((individual-moves
+           (loop :for move :in (return-all (legal ?role ?action))
+                 :collect (cons (getf move '?role)
+                                (getf move '?action))))
+         (joint-moves
+           (apply #'map-product #'list
+                  (equivalence-classes #'equiv-roles individual-moves))))
+    joint-moves))
 
 (defun roles ()
-  (with-database *d*
-    (extract '?role (return-all (role ?role)))))
+  (extract '?role (return-all (role ?role))))
+
+(defun goal-value (role)
+  (getf (perform-return `((goal ,role ?goal))
+                        :one)
+        '?goal))
 
-(defun goal-value (state role)
-  (with-database *d*
-    (getf (perform-return `((goal ,state ,role ?goal)) :one) '?goal)))
+(defun goal-values ()
+  (perform-return `((goal ?role ?goal))
+                  :all))
+
+(defun next-state ()
+  (extract '?what (return-all (next ?what))))
+
 
-(defun goal-values (state)
-  (with-database *d*
-    (perform-return `((goal ,state ?role ?goal)) :all)))
+(defun apply-state (state)
+  (push-logic-frame)
+  (loop :for fact :in state
+        :do (add-fact `(true ,fact)))
+  (finalize-logic-frame))
 
-(defun next-state (current-state move)
-  (let ((does `(list (does
-                       ,(getf move '?role)
-                       ,(getf move '?move)))))
-    (with-database *d*
-      (to-prolog-list
-        (extract '?what
-                 (perform-return `((next ,current-state ,does ?what)) :all))))))
+(defun apply-moves (moves)
+  (push-logic-frame)
+  (loop :for (role . action) :in moves
+        :do (add-fact `(does ,role ,action)))
+  (finalize-logic-frame))
+
+
+(defun clear-state ()
+  (pop-logic-frame))
+
+(defun clear-moves ()
+  (pop-logic-frame))
 
 
 (defvar *count* 0)
 
-(defstruct search-path state (path nil) (previous nil))
-
-(defun tree-search (states goal-p children combine)
-  (labels
-      ((recur (states)
-         (if (null states)
-           nil
-           (destructuring-bind (state . remaining) states
-             (incf *count*)
-             ; (format t "Searching: ~S (~D remaining)~%" state (length remaining))
-             (if (funcall goal-p state)
-               state
-               (recur (funcall combine
-                               (funcall children state)
-                               remaining)))))))
-    (let ((result (recur states)))
-      (when result
-        (reverse (search-path-path result))))))
-
-
-(defun buttons-goal-p (search-path)
-  (let ((state (search-path-state search-path)))
-    (and (terminalp state)
-         (eql (goal-value state 'robot) 'num100))))
 
-(defun buttons-children (search-path)
-  (let ((state (search-path-state search-path))
-        (path (search-path-path search-path)))
-    (when (not (terminalp state))
-      (loop :for move :in (legal-moves state)
-            :collect (make-search-path :state (next-state state move)
-                                       :path (cons move path)
-                                       :previous search-path)))))
-
-(defun never (&rest args)
-  (declare (ignore args))
-  nil)
-
-(defun dfs ()
-  (tree-search (list (make-search-path :state (initial-state)))
-               #'buttons-goal-p
-               #'buttons-children
-               #'append))
+; (declaim (optimize (speed 0) (debug 3)))
+;; nodes: (state . path)
+(defun depth-first-search (&key exhaust)
+  (let ((*count* 0)
+        (nodes (make-queue)))
+    (enqueue (cons (initial-state) nil) nodes)
+    (pprint
+      (while (not (queue-empty-p nodes))
+        (incf *count*)
+        (destructuring-bind (state . path)
+            (dequeue nodes)
+          (apply-state state)
+          ; (format t "Searching: ~S (~D remaining)~%" state (length remaining))
+          (if (and (not exhaust) (eql 'num100 (goal-value 'robot)))
+            (progn
+              (clear-state)
+              (return (list state (reverse path))))
+            (let ((children
+                    (when (not (terminalp))
+                      (loop :for joint-move :in (legal-moves)
+                            :collect (prog2
+                                       (apply-moves joint-move)
+                                       (cons (next-state)
+                                             (cons joint-move path))
+                                       (clear-moves))))))
+              (clear-state)
+              (queue-append nodes children))))))
+    (format t "~%Searched ~D nodes.~%" *count*)))
 
-(defun dfs-exhaust ()
-  (let ((*count* 0))
-    (prog1
-        (tree-search (list (make-search-path :state (initial-state)))
-                     #'never
-                     #'buttons-children
-                     #'append)
-      (format t "Searched ~D nodes.~%" *count*))))
-
-(defun bfs ()
-  (tree-search (list (make-search-path :state (initial-state)))
-               #'buttons-goal-p
-               #'buttons-children
-               (lambda (x y)
-                 (append y x))))
-
-; (sb-sprof:with-profiling
-;     (:report :flat
-;      :sample-interval 0.001
-;      :loop nil)
-;   (dfs-exhaust)
-;   )
diff -r 6a93a2d2ed60 -r 410acaae0c14 examples/profile.lisp
--- a/examples/profile.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/examples/profile.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -1,17 +1,17 @@
 (ql:quickload 'bones)
+(load "examples/ggp-wam.lisp")
 
 (require :sb-sprof)
 
-(load "examples/ggp-wam.lisp")
-
-(in-package :bones)
+(in-package :bones.wam)
 
 (defun reload ()
   (let ((*standard-output* (make-broadcast-stream))
         (*debug-io* (make-broadcast-stream))
         (*terminal-io* (make-broadcast-stream))
         (*error-output* (make-broadcast-stream)))
-    (asdf:load-system 'bones :force t)))
+    (asdf:load-system 'bones :force t)
+    (load "examples/ggp-wam.lisp")))
 
 
 (defun run-profile ()
@@ -19,12 +19,14 @@
 
   (format t "PROFILING -------------------------------~%")
 
+  ; (sb-sprof:profile-call-counts "COMMON-LISP")
   (sb-sprof:profile-call-counts "BONES.WAM")
+  (sb-sprof:profile-call-counts "BONES.QUICKUTILS")
 
   (sb-sprof:with-profiling (:max-samples 5000
-                            :sample-interval 0.001
+                            :sample-interval 0.0005
                             :loop nil)
-    (bones.wam::dfs-exhaust))
+    (bones.wam::depth-first-search :exhaust t))
 
   (sb-sprof:report :type :flat)
   )
@@ -36,10 +38,10 @@
 
 ; (format t "~%~%====================================~%")
 ; (format t "(speed 3) (safety 1) (debug 0)~%")
-; (declaim (optimize (speed 3) (safety 1) (debug 0)))
-; (run-test)
+; (declaim (optimize (speed 3) (safety 3) (debug 3)))
+; (run-profile)
 
-(format t "~%~%====================================~%")
-(format t "(speed 3) (safety 0) (debug 0)~%")
+; (format t "~%~%====================================~%")
+; (format t "(speed 3) (safety 0) (debug 0)~%")
 (declaim (optimize (speed 3) (safety 0) (debug 0)))
 (run-profile)
diff -r 6a93a2d2ed60 -r 410acaae0c14 package-test.lisp
--- a/package-test.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/package-test.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -24,8 +24,8 @@
     #:with-database
     #:make-database
     #:with-fresh-database
+    #:push-logic-frame-with
     #:rule
-    #:rules
     #:fact
     #:facts
     #:call
diff -r 6a93a2d2ed60 -r 410acaae0c14 package.lisp
--- a/package.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/package.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -16,7 +16,14 @@
     #:recur
     #:when-let
     #:unique-items
-    #:dis))
+    #:dis
+    #:make-queue
+    #:enqueue
+    #:dequeue
+    #:queue-empty-p
+    #:queue-append)
+  (:shadowing-import-from #:cl-arrows
+    #:->))
 
 (defpackage #:bones.circle
   (:use #:cl #:defstar)
@@ -49,9 +56,7 @@
     #:circle-backward-splice
     #:circle-forward-splice
     #:circle-insert-beginning
-    #:circle-insert-end
-    )
-  )
+    #:circle-insert-end))
 
 (defpackage #:bones.wam
   (:use
@@ -101,6 +106,5 @@
     ;; Interactive queries
     #:query
     #:query-one
-    #:query-all
-    ))
+    #:query-all))
 
diff -r 6a93a2d2ed60 -r 410acaae0c14 src/make-quickutils.lisp
--- a/src/make-quickutils.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/src/make-quickutils.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -19,5 +19,6 @@
                :weave
                :range
                :alist-plist
-               )
+               :equivalence-classes
+               :map-product)
   :package "BONES.QUICKUTILS")
diff -r 6a93a2d2ed60 -r 410acaae0c14 src/quickutils.lisp
--- a/src/quickutils.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/src/quickutils.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -2,7 +2,7 @@
 ;;;; See http://quickutil.org for details.
 
 ;;;; To regenerate:
-;;;; (qtlc:save-utils-as "quickutils.lisp" :utilities '(:DEFINE-CONSTANT :SET-EQUAL :CURRY :SWITCH :ENSURE-BOOLEAN :WHILE :UNTIL :TREE-MEMBER-P :TREE-COLLECT :WITH-GENSYMS :ONCE-ONLY :ZIP :ALIST-TO-HASH-TABLE :MAP-TREE :WEAVE :RANGE :ALIST-PLIST) :ensure-package T :package "BONES.QUICKUTILS")
+;;;; (qtlc:save-utils-as "quickutils.lisp" :utilities '(:DEFINE-CONSTANT :SET-EQUAL :CURRY :SWITCH :ENSURE-BOOLEAN :WHILE :UNTIL :TREE-MEMBER-P :TREE-COLLECT :WITH-GENSYMS :ONCE-ONLY :ZIP :ALIST-TO-HASH-TABLE :MAP-TREE :WEAVE :RANGE :ALIST-PLIST :EQUIVALENCE-CLASSES :MAP-PRODUCT) :ensure-package T :package "BONES.QUICKUTILS")
 
 (eval-when (:compile-toplevel :load-toplevel :execute)
   (unless (find-package "BONES.QUICKUTILS")
@@ -21,7 +21,9 @@
                                          :TREE-MEMBER-P :TREE-COLLECT
                                          :ONCE-ONLY :TRANSPOSE :ZIP
                                          :ALIST-TO-HASH-TABLE :MAP-TREE :WEAVE
-                                         :RANGE :SAFE-ENDP :ALIST-PLIST))))
+                                         :RANGE :SAFE-ENDP :ALIST-PLIST
+                                         :EQUIVALENCE-CLASSES :MAPPEND
+                                         :MAP-PRODUCT))))
 
   (defun %reevaluate-constant (name value test)
     (if (not (boundp name))
@@ -366,10 +368,64 @@
           ((safe-endp tail) (nreverse alist))
         (push (cons (car tail) (cadr tail)) alist))))
   
+
+  (defun equivalence-classes (equiv seq)
+    "Partition the sequence `seq` into a list of equivalence classes
+defined by the equivalence relation `equiv`."
+    (let ((classes nil))
+      (labels ((find-equivalence-class (x)
+                 (member-if (lambda (class)
+                              (funcall equiv x (car class)))
+                            classes))
+               
+               (add-to-class (x)
+                 (let ((class (find-equivalence-class x)))
+                   (if class
+                       (push x (car class))
+                       (push (list x) classes)))))
+        (declare (dynamic-extent (function find-equivalence-class)
+                                 (function add-to-class))
+                 (inline find-equivalence-class
+                         add-to-class))
+        
+        ;; Partition into equivalence classes.
+        (map nil #'add-to-class seq)
+        
+        ;; Return the classes.
+        classes)))
+  
+
+  (defun mappend (function &rest lists)
+    "Applies `function` to respective element(s) of each `list`, appending all the
+all the result list to a single list. `function` must return a list."
+    (loop for results in (apply #'mapcar function lists)
+          append results))
+  
+
+  (defun map-product (function list &rest more-lists)
+    "Returns a list containing the results of calling `function` with one argument
+from `list`, and one from each of `more-lists` for each combination of arguments.
+In other words, returns the product of `list` and `more-lists` using `function`.
+
+Example:
+
+    (map-product 'list '(1 2) '(3 4) '(5 6))
+     => ((1 3 5) (1 3 6) (1 4 5) (1 4 6)
+         (2 3 5) (2 3 6) (2 4 5) (2 4 6))"
+    (labels ((%map-product (f lists)
+               (let ((more (cdr lists))
+                     (one (car lists)))
+                 (if (not more)
+                     (mapcar f one)
+                     (mappend (lambda (x)
+                                (%map-product (curry f x) more))
+                              one)))))
+      (%map-product (ensure-function function) (cons list more-lists))))
+  
 (eval-when (:compile-toplevel :load-toplevel :execute)
   (export '(define-constant set-equal curry switch eswitch cswitch
             ensure-boolean while until tree-member-p tree-collect with-gensyms
             with-unique-names once-only zip alist-to-hash-table map-tree weave
-            range alist-plist plist-alist)))
+            range alist-plist plist-alist equivalence-classes map-product)))
 
 ;;;; END OF quickutils.lisp ;;;;
diff -r 6a93a2d2ed60 -r 410acaae0c14 src/utils.lisp
--- a/src/utils.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/src/utils.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -92,3 +92,51 @@
     `(labels ((recur ,(mapcar #'extract-var bindings)
                 ,@body))
       (recur ,@(mapcar #'extract-val bindings)))))
+
+
+;;;; Queues
+;;; Thanks, Norvig.
+
+(deftype queue () '(cons list list))
+(declaim (inline queue-contents make-queue
+                 enqueue dequeue
+                 queue-empty-p queue-append))
+
+
+(defun* queue-contents ((q queue))
+  (:returns list)
+  (cdr q))
+
+(defun* make-queue ()
+  (:returns queue)
+  (let ((q (cons nil nil)))
+    (setf (car q) q)))
+
+(defun* enqueue ((item t) (q queue))
+  (:returns queue)
+  (setf (car q)
+        (setf (rest (car q))
+              (cons item nil)))
+  q)
+
+(defun* dequeue ((q queue))
+  (:returns t)
+  (prog1
+      (pop (cdr q))
+    (if (null (cdr q))
+      (setf (car q) q))))
+
+(defun* queue-empty-p ((q queue))
+  (:returns boolean)
+  (null (queue-contents q)))
+
+(defun* queue-append ((q queue) (l list))
+  (:returns queue)
+  (when l
+    (setf (car q)
+          (last (setf (rest (car q))
+                      l))))
+  q)
+
+
+
diff -r 6a93a2d2ed60 -r 410acaae0c14 src/wam/compiler.lisp
--- a/src/wam/compiler.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/src/wam/compiler.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -1187,22 +1187,35 @@
             (clause-permanent-vars clause-props))))
 
 
-(defun find-arity (rule)
-  (let ((head (first rule)))
+(defun find-predicate (clause)
+  "Return a pair of the functor and arity of `clause`
+
+  A functor and an arity together specify a particular Prolog predicate.
+
+  "
+  ;; ( (f ?x ?y)   | head   ||| clause
+  ;;   (foo ?x)    || body  |||
+  ;;   (bar ?y) )  ||       |||
+  (destructuring-bind (head . body) clause
+    (declare (ignore body))
     (cond
-      ((null head) (error "Rule ~S has a NIL head." rule))
-      ((atom head) 0) ; constants are 0-arity
-      (t (1- (length head))))))
+      ((null head)
+       (error "Clause ~S has a NIL head." clause))
+      ((atom head) ; constants are 0-arity
+       (cons head 0))
+      (t
+       (cons (car head)
+             (1- (length head)))))))
 
 (defun check-rules (rules)
-  ;; TODO: fix constant handling here...
-  (let* ((predicates (mapcar #'caar rules))
-         (arities (mapcar #'find-arity rules))
-         (functors (zip predicates arities)))
-    (assert (= 1 (length (remove-duplicates functors :test #'equal))) ()
-      "Must add exactly 1 predicate at a time (got: ~S)."
-      functors)
-    (values (first predicates) (first arities))))
+  (let ((predicates (-<> rules
+                      (mapcar #'find-predicate <>)
+                      (remove-duplicates <> :test #'equal))))
+    (assert (= 1 (length predicates)) ()
+      "Must add exactly one predicate at a time (got: ~S)."
+      predicates)
+    (values (car (first predicates))
+            (cdr (first predicates)))))
 
 (defun precompile-rules (wam rules)
   "Compile `rules` into a list of instructions.
diff -r 6a93a2d2ed60 -r 410acaae0c14 src/wam/dump.lisp
--- a/src/wam/dump.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/src/wam/dump.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -307,7 +307,9 @@
                 0)) ; this
      (to (min (+ (wam-program-counter wam) 8) ; is
               (length (wam-code wam))))) ; bad
-  (format t "CODE~%")
+  (format t "CODE (size: ~D frame(s) / ~:[OPEN~;CLOSED~])~%"
+          (length (wam-code-stack wam))
+          (wam-code-closed-p wam))
   (dump-code-store wam (wam-code wam) from to))
 
 
diff -r 6a93a2d2ed60 -r 410acaae0c14 src/wam/ui.lisp
--- a/src/wam/ui.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/src/wam/ui.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -1,6 +1,7 @@
 (in-package #:bones.wam)
 
 
+;;;; Database
 (defparameter *database* nil)
 (defvar *results* nil)
 
@@ -16,23 +17,49 @@
   `(with-database (make-database) ,@body))
 
 
-(defun add-rules (rules)
-  (compile-rules *database* rules))
+;;;; Assertion
+(defun add-rule (clause)
+  (wam-code-add-clause! *database* clause)
+  (values))
+
+(defun add-fact (fact)
+  (add-rule (list fact))
+  (values))
+
+(defun add-facts (facts)
+  (mapc #'add-fact facts)
+  (values))
 
 
 (defmacro rule (&body body)
-  `(add-rules '(,body)))
-
-(defmacro fact (&body body)
-  `(add-rules '(,body)))
+  `(add-rule ',body))
 
-(defmacro rules (&body rules)
-  `(add-rules ',rules))
+(defmacro fact (fact)
+  `(add-fact ',fact))
 
-(defmacro facts (&body rules)
-  `(add-rules ',(mapcar #'list rules)))
+(defmacro facts (&body facts)
+  `(progn
+     ,@(loop :for f :in facts :collect `(fact ,f))))
 
 
+;;;; Logic Frames
+(defun push-logic-frame ()
+  (wam-code-push-frame! *database*))
+
+(defun pop-logic-frame ()
+  (wam-code-pop-frame! *database*))
+
+(defun finalize-logic-frame ()
+  (wam-code-finalize-frame! *database*))
+
+(defmacro push-logic-frame-with (&body body)
+  `(prog2
+     (push-logic-frame)
+     (progn ,@body)
+     (finalize-logic-frame)))
+
+
+;;;; Querying
 (defun display-results (results)
   (format t "~%")
   (loop :for (var result . more) :on results :by #'cddr :do
diff -r 6a93a2d2ed60 -r 410acaae0c14 src/wam/wam.lisp
--- a/src/wam/wam.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/src/wam/wam.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -5,8 +5,9 @@
   ;; Inline all these struct accessors, otherwise things get REAL slow.
   (inline wam-store
           wam-code
+          wam-code-stack
+          wam-code-labels
           wam-functors
-          wam-code-labels
           wam-fail
           wam-backtracked
           wam-unification-stack
@@ -58,6 +59,12 @@
       :element-type 'code-word)
     :type (vector code-word)
     :read-only t)
+  (code-labels
+    (make-hash-table)
+    :read-only t)
+  (code-stack
+    nil
+    :type list)
   (functors
     (make-array 64
       :fill-pointer 0
@@ -65,9 +72,6 @@
       :element-type 'functor)
     :type (vector functor)
     :read-only t)
-  (code-labels
-    (make-hash-table)
-    :read-only t)
   (unification-stack
     (make-array 16
       :fill-pointer 0
@@ -585,8 +589,8 @@
   (:returns (or null code-index))
   (gethash functor (wam-code-labels wam)))
 
-;; Note that this takes a functor/arity and not a cons.
 (defun (setf wam-code-label) (new-value wam functor arity)
+  ;; Note that this takes a functor/arity and not a cons.
   (setf (gethash (wam-ensure-functor-index wam (cons functor arity))
                  (wam-code-labels wam))
         new-value))
@@ -604,6 +608,88 @@
   (values))
 
 
+;;;; Code Stack
+(defstruct code-stack-frame
+  (start 0 :type code-index)
+  (final nil :type boolean)
+  (predicates (make-hash-table) :type hash-table))
+
+
+(defun* wam-code-stack-current-frame ((wam wam))
+  (:returns (or null code-stack-frame))
+  (first (wam-code-stack wam)))
+
+(defun* wam-code-stack-empty-p ((wam wam))
+  (:returns boolean)
+  (not (wam-code-stack-current-frame wam)))
+
+
+(defun* wam-code-open-p ((wam wam))
+  (:returns boolean)
+  (let ((frame (wam-code-stack-current-frame wam)))
+    (and frame (not (code-stack-frame-final frame)))))
+
+(defun* wam-code-closed-p ((wam wam))
+  (:returns boolean)
+  (not (wam-code-open-p wam)))
+
+
+(defun* wam-code-push-frame! ((wam wam))
+  (:returns :void)
+  (assert (wam-code-closed-p wam) ()
+    "Cannot push code frame unless the code stack is closed.")
+  (push (make-code-stack-frame
+          :start (fill-pointer (wam-code wam))
+          :final nil
+          :predicates (make-hash-table))
+        (wam-code-stack wam))
+  (values))
+
+(defun* wam-code-pop-frame! ((wam wam))
+  (:returns :void)
+  (with-slots (code-stack) wam
+    (assert code-stack ()
+      "Cannot pop code frame from an empty code stack.")
+    (assert (code-stack-frame-final (first code-stack)) ()
+      "Cannot pop unfinalized code frame.")
+    (with-slots (start predicates)
+        (pop code-stack)
+      (setf (fill-pointer (wam-code wam)) start)
+      (loop :for label :being :the hash-keys :of predicates
+            :do (remhash label (wam-code-labels wam)))))
+  (values))
+
+
+(defun* assert-label-not-already-compiled ((wam wam) clause label)
+  (assert (not (wam-code-label wam label))
+      ()
+    "Cannot add clause ~S because its predicate has preexisting compiled code."
+    clause))
+
+
+(defun* wam-code-add-clause! ((wam wam) clause)
+  (assert (wam-code-open-p wam) ()
+    "Cannot add clause ~S without an open code stack frame."
+    clause)
+  (let ((label (wam-ensure-functor-index wam (find-predicate clause))))
+    (assert-label-not-already-compiled wam clause label)
+    (with-slots (predicates)
+        (wam-code-stack-current-frame wam)
+      (push clause (gethash label predicates))))
+  (values))
+
+
+(defun* wam-code-finalize-frame! ((wam wam))
+  (assert (wam-code-open-p wam) ()
+    "There is no code frame waiting to be finalized.")
+  (with-slots (predicates final)
+      (wam-code-stack-current-frame wam)
+    (loop :for clauses :being :the hash-values :of predicates
+          :do (compile-rules wam (reverse clauses))) ; circular dep here, ugh.
+    (setf final t))
+  (values))
+
+
 ;;;; Registers
 ;;; The WAM has two types of registers:
 ;;;
diff -r 6a93a2d2ed60 -r 410acaae0c14 test/wam.lisp
--- a/test/wam.lisp	Tue Jul 05 16:53:58 2016 +0000
+++ b/test/wam.lisp	Tue Jul 05 23:02:33 2016 +0000
@@ -8,49 +8,50 @@
 (defun make-test-database ()
   (let ((db (make-database)))
     (with-database db
+      (push-logic-frame-with
 
-      (facts (always))
+        (facts (always)
 
-      (facts (drinks tom ?anything)
-             (drinks kim water)
-             (drinks alice bourbon)
-             (drinks bob genny-cream)
-             (drinks candace birch-beer))
+               (drinks tom ?anything)
+               (drinks kim water)
+               (drinks alice bourbon)
+               (drinks bob genny-cream)
+               (drinks candace birch-beer)
 
-      (facts (listens alice blues)
-             (listens alice jazz)
-             (listens bob blues)
-             (listens bob rock)
-             (listens candace blues))
+               (listens alice blues)
+               (listens alice jazz)
+               (listens bob blues)
+               (listens bob rock)
+               (listens candace blues)
 
-      (facts (fuzzy cats))
+               (fuzzy cats)
 
-      (facts (cute cats)
-             (cute snakes))
+               (cute cats)
+               (cute snakes))
 
-      (rules ((pets alice ?what)
-              (cute ?what))
+        (rule (pets alice ?what)
+          (cute ?what))
 
-             ((pets bob ?what)
-              (cute ?what)
-              (fuzzy ?what))
+        (rule (pets bob ?what)
+          (cute ?what)
+          (fuzzy ?what))
 
-             ((pets candace ?bird)
-              (flies ?bird)))
+        (rule (pets candace ?bird)
+          (flies ?bird))
 
-      (rules ((likes sally ?who)
-              (likes ?who cats)
-              (drinks ?who beer))
+        (rule (likes sally ?who)
+          (likes ?who cats)
+          (drinks ?who beer))
 
-             ((likes tom cats))
-             ((likes alice cats))
-             ((likes kim cats))
+        (facts (likes tom cats)
+               (likes alice cats)
+               (likes kim cats))
 
-             ((likes kim ?who)
-              (likes ?who cats)))
+        (rule (likes kim ?who)
+          (likes ?who cats))
 
-      (rules ((narcissist ?person)
-              (likes ?person ?person)))
+        (rule (narcissist ?person)
+          (likes ?person ?person)))
 
       )
     db))
@@ -126,7 +127,8 @@
 
 (test simple-unification
   (with-fresh-database
-    (rule (= ?x ?x))
+    (push-logic-frame-with
+      (rule (= ?x ?x)))
     (should-return
       ((= x x) empty)
       ((= x y) fail)
@@ -139,12 +141,13 @@
 
 (test dynamic-call
   (with-fresh-database
-    (facts (g cats)
-           (g (f dogs)))
-    (rule (normal ?x)
-      (g ?x))
-    (rule (dynamic ?struct)
-      (call ?struct))
+    (push-logic-frame-with
+      (facts (g cats)
+             (g (f dogs)))
+      (rule (normal ?x)
+        (g ?x))
+      (rule (dynamic ?struct)
+        (call ?struct)))
     (should-return
       ((normal foo) fail)
       ((normal cats) empty)
@@ -164,9 +167,11 @@
 
 (test not
   (with-fresh-database
-    (facts (yes ?anything))
-    (rules ((not ?x) (call ?x) ! fail)
-           ((not ?x)))
+    (push-logic-frame-with
+      (fact (yes ?anything))
+
+      (rule (not ?x) (call ?x) ! fail)
+      (rule (not ?x)))
     (should-return
       ((yes x) empty)
       ((no x) fail)
@@ -175,53 +180,57 @@
 
 (test backtracking
   (with-fresh-database
-    (facts (a))
-    (facts (b))
-    (facts (c))
-    (facts (d))
-    (rules ((f ?x) (a))
-           ((f ?x) (b) (c))
-           ((f ?x) (d)))
+    (push-logic-frame-with
+      (facts (b))
+      (facts (c))
+      (facts (d))
+      (rule (f ?x) (a))
+      (rule (f ?x) (b) (c))
+      (rule (f ?x) (d)))
     (should-return
       ((f foo) empty)))
   (with-fresh-database
-    ; (facts (a))
-    (facts (b))
-    (facts (c))
-    (facts (d))
-    (rules ((f ?x) (a))
-           ((f ?x) (b) (c))
-           ((f ?x) (d)))
+    (push-logic-frame-with
+      ; (facts (a))
+      (facts (b))
+      (facts (c))
+      (facts (d))
+      (rule (f ?x) (a))
+      (rule (f ?x) (b) (c))
+      (rule (f ?x) (d)))
     (should-return
       ((f foo) empty)))
   (with-fresh-database
-    ; (facts (a))
-    (facts (b))
-    (facts (c))
-    ; (facts (d))
-    (rules ((f ?x) (a))
-           ((f ?x) (b) (c))
-           ((f ?x) (d)))
+    (push-logic-frame-with
+      ; (facts (a))
+      (facts (b))
+      (facts (c))
+      ; (facts (d))
+      (rule (f ?x) (a))
+      (rule (f ?x) (b) (c))
+      (rule (f ?x) (d)))
     (should-return
       ((f foo) empty)))
   (with-fresh-database
-    ; (facts (a))
-    ; (facts (b))
-    (facts (c))
-    ; (facts (d))
-    (rules ((f ?x) (a))
-           ((f ?x) (b) (c))
-           ((f ?x) (d)))
+    (push-logic-frame-with
+      ; (facts (a))
+      ; (facts (b))
+      (facts (c))
+      ; (facts (d))
+      (rule (f ?x) (a))
+      (rule (f ?x) (b) (c))
+      (rule (f ?x) (d)))
     (should-return
       ((f foo) fail)))
   (with-fresh-database
-    ; (facts (a))
-    (facts (b))
-    ; (facts (c))
-    ; (facts (d))
-    (rules ((f ?x) (a))
-           ((f ?x) (b) (c))
-           ((f ?x) (d)))
+    (push-logic-frame-with
+      ; (facts (a))
+      (facts (b))
+      ; (facts (c))
+      ; (facts (d))
+      (rule (f ?x) (a))
+      (rule (f ?x) (b) (c))
+      (rule (f ?x) (d)))
     (should-return
       ((f foo) fail))))
 
@@ -256,23 +265,25 @@
 (test register-allocation
   ;; test for tricky register allocation bullshit
   (with-fresh-database
-    (fact (a fact-a fact-a))
-    (fact (b fact-b fact-b))
-    (fact (c fact-c fact-c))
+    (push-logic-frame-with
+      (fact (a fact-a fact-a))
+      (fact (b fact-b fact-b))
+      (fact (c fact-c fact-c))
 
-    (rule (foo ?x)
-          (a ?a ?a)
-          (b ?b ?b)
-          (c ?c ?c))
+      (rule (foo ?x)
+        (a ?a ?a)
+        (b ?b ?b)
+        (c ?c ?c)))
 
     (should-return
       ((foo dogs) empty))))
 
 (test lists
   (with-fresh-database
-    (rules ((member ?x (list* ?x ?)))
-           ((member ?x (list* ? ?rest))
-            (member ?x ?rest)))
+    (push-logic-frame-with
+      (rule (member ?x (list* ?x ?)))
+      (rule (member ?x (list* ?y ?rest))
+        (member ?x ?rest)))
 
     (should-fail
       (member ?anything nil)
@@ -300,15 +311,18 @@
 
 (test cut
   (with-fresh-database
-    (facts (a))
-    (facts (b))
-    (facts (c))
-    (facts (d))
-    (rules ((f a) (a))
-           ((f bc) (b) ! (c))
-           ((f d) (d)))
-    (rules ((g ?what) (never))
-           ((g ?what) (f ?what)))
+    (push-logic-frame-with
+      (facts (a))
+      (facts (b))
+      (facts (c))
+      (facts (d))
+
+      (rule (f a) (a))
+      (rule (f bc) (b) ! (c))
+      (rule (f d) (d))
+
+      (rule (g ?what) (never))
+      (rule (g ?what) (f ?what)))
     (should-return
       ((f ?what)
        (?what a)
@@ -318,15 +332,18 @@
        (?what bc))))
 
   (with-fresh-database
-    ; (facts (a))
-    (facts (b))
-    (facts (c))
-    (facts (d))
-    (rules ((f a) (a))
-           ((f bc) (b) ! (c))
-           ((f d) (d)))
-    (rules ((g ?what) (never))
-           ((g ?what) (f ?what)))
+    (push-logic-frame-with
+      ; (facts (a))
+      (facts (b))
+      (facts (c))
+      (facts (d))
+
+      (rule (f a) (a))
+      (rule (f bc) (b) ! (c))
+      (rule (f d) (d))
+
+      (rule (g ?what) (never))
+      (rule (g ?what) (f ?what)))
     (should-return
       ((f ?what)
        (?what bc))
@@ -334,15 +351,18 @@
        (?what bc))))
 
   (with-fresh-database
-    ; (facts (a))
-    ; (facts (b))
-    (facts (c))
-    (facts (d))
-    (rules ((f a) (a))
-           ((f bc) (b) ! (c))
-           ((f d) (d)))
-    (rules ((g ?what) (never))
-           ((g ?what) (f ?what)))
+    (push-logic-frame-with
+      ; (facts (a))
+      ; (facts (b))
+      (facts (c))
+      (facts (d))
+
+      (rule (f a) (a))
+      (rule (f bc) (b) ! (c))
+      (rule (f d) (d))
+
+      (rule (g ?what) (never))
+      (rule (g ?what) (f ?what)))
     (should-return
       ((f ?what)
        (?what d))
@@ -350,39 +370,46 @@
        (?what d))))
 
   (with-fresh-database
-    ; (facts (a))
-    (facts (b))
-    ; (facts (c))
-    (facts (d))
-    (rules ((f a) (a))
-           ((f bc) (b) ! (c))
-           ((f d) (d)))
-    (rules ((g ?what) (never))
-           ((g ?what) (f ?what)))
+    (push-logic-frame-with
+      ; (facts (a))
+      (facts (b))
+      ; (facts (c))
+      (facts (d))
+
+      (rule (f a) (a))
+      (rule (f bc) (b) ! (c))
+      (rule (f d) (d))
+
+      (rule (g ?what) (never))
+      (rule (g ?what) (f ?what)))
     (should-fail
       (f ?what)
       (g ?what)))
 
   (with-fresh-database
-    ; (facts (a))
-    ; (facts (b))
-    (facts (c))
-    ; (facts (d))
-    (rules ((f a) (a))
-           ((f bc) (b) ! (c))
-           ((f d) (d)))
-    (rules ((g ?what) (never))
-           ((g ?what) (f ?what)))
+    (push-logic-frame-with
+      ; (facts (a))
+      ; (facts (b))
+      (facts (c))
+      ; (facts (d))
+
+      (rule (f a) (a))
+      (rule (f bc) (b) ! (c))
+      (rule (f d) (d))
+
+      (rule (g ?what) (never))
+      (rule (g ?what) (f ?what)))
     (should-fail
       (f ?what)
       (g ?what))))
 
 (test anonymous-variables
   (with-fresh-database
-    (fact (foo x))
-    (rule (bar (baz ?x ?y ?z ?thing))
-          (foo ?thing))
-    (fact (wild ? ? ?))
+    (push-logic-frame-with
+      (fact (foo x))
+      (rule (bar (baz ?x ?y ?z ?thing))
+        (foo ?thing))
+      (fact (wild ? ? ?)))
     (should-return
       ((bar (baz a b c no)) fail)
       ((bar (baz a b c ?what)) (?what x))