From c0e2f5891db30578b2e94c00b821093ff1dd01d2 Mon Sep 17 00:00:00 2001
From: David Nolen <david.nolen@gmail.com>
Date: Tue, 1 Nov 2011 23:26:18 -0400
Subject: [PATCH] * src/main/clojure/clojure/core/logic/arithmetic.clj:
 consolidate into clojure.core.logic

---
 .../clojure/clojure/core/logic/arithmetic.clj |    4 +-
 src/main/clojure/clojure/core/logic/bench.clj |   28 +-
 src/main/clojure/clojure/core/logic/dcg.clj   |    9 +-
 .../clojure/core/logic/disequality.clj        |  250 ----
 src/main/clojure/clojure/core/logic/match.clj |  102 --
 .../clojure/clojure/core/logic/minikanren.clj | 1008 -----------------
 .../clojure/clojure/core/logic/nonrel.clj     |  149 ---
 .../clojure/clojure/core/logic/prelude.clj    |  245 ----
 .../clojure/clojure/core/logic/tabled.clj     |  175 ---
 src/main/clojure/clojure/core/logic/unify.clj |   93 --
 src/test/clojure/clojure/core/logic/tests.clj |    8 +-
 11 files changed, 13 insertions(+), 2058 deletions(-)
 delete mode 100644 src/main/clojure/clojure/core/logic/disequality.clj
 delete mode 100644 src/main/clojure/clojure/core/logic/match.clj
 delete mode 100644 src/main/clojure/clojure/core/logic/minikanren.clj
 delete mode 100644 src/main/clojure/clojure/core/logic/nonrel.clj
 delete mode 100644 src/main/clojure/clojure/core/logic/prelude.clj
 delete mode 100644 src/main/clojure/clojure/core/logic/tabled.clj
 delete mode 100644 src/main/clojure/clojure/core/logic/unify.clj

diff --git a/src/main/clojure/clojure/core/logic/arithmetic.clj b/src/main/clojure/clojure/core/logic/arithmetic.clj
index 27dd871d..69506e29 100644
--- a/src/main/clojure/clojure/core/logic/arithmetic.clj
+++ b/src/main/clojure/clojure/core/logic/arithmetic.clj
@@ -1,8 +1,6 @@
 (ns clojure.core.logic.arithmetic
   (:refer-clojure :exclude [reify == inc = > < >= <=])
-  (:use clojure.core.logic.minikanren
-        [clojure.core.logic.nonrel :only [project]])
-  (:import [clojure.core.logic.minikanren Substitutions]))
+  (:use clojure.core.logic))
 
 (defmacro = [x y]
   "Goal for testing whether x and y are equal. Non-relational."
diff --git a/src/main/clojure/clojure/core/logic/bench.clj b/src/main/clojure/clojure/core/logic/bench.clj
index 6a54428a..97f3f1da 100644
--- a/src/main/clojure/clojure/core/logic/bench.clj
+++ b/src/main/clojure/clojure/core/logic/bench.clj
@@ -1,10 +1,7 @@
 (ns clojure.core.logic.bench
   (:refer-clojure :exclude [reify inc ==])
-  (:use clojure.core.logic.minikanren
-        [clojure.core.logic.prelude :only [defne membero appendo]]
-        [clojure.core.logic.disequality :only [!=]])
-  (:require [clojure.core.logic.nonrel :as nonrel]
-            [clojure.core.logic.arithmetic :as a]))
+  (:use clojure.core.logic)
+  (:require [clojure.core.logic.arithmetic :as a]))
 
 (comment
   (run* [q]
@@ -63,17 +60,6 @@
 ;; zebra
 ;; =============================================================================
 
-(defn conso [a d l]
-  (== (lcons a d) l))
-
-(defn firsto [l a]
-  (fresh [d]
-    (conso a d l)))
-
-(defn resto [l d]
-  (fresh [a]
-    (== (lcons a d) l)))
-
 (defne righto [x y l]
   ([_ _ [x y . ?r]])
   ([_ _ [_ . ?r]] (righto x y ?r)))
@@ -134,7 +120,7 @@
   ([_ ()])
   ([[?x ?y] [[?x1 ?y1] . ?others]]
      (!= ?y ?y1)
-     (nonrel/project [?y ?y1 ?x ?x1]
+     (project [?y ?y1 ?x ?x1]
        (!= (- ?y1 ?y) (- ?x1 ?x))
        (!= (- ?y1 ?y) (- ?x ?x1)))
      (noattacko [?x ?y] ?others)))
@@ -204,11 +190,11 @@
        (digito o l5 l6)
        (digito r l6 l7)
        (digito y l7 l8)
-       (nonrel/project [s e n d m o r y]
+       (project [s e n d m o r y]
          (== ?send (+ (* s 1000) (* e 100) (* n 10) d))
          (== ?more (+ (* m 1000) (* o 100) (* r 10) e))
          (== ?money (+ (* m 10000) (* o 1000) (* n 100) (* e 10) y))
-         (nonrel/project [?send ?more]
+         (project [?send ?more]
            (== ?money (+ ?send ?more)))))))
 
 (defn send-money-quicklyo [send more money]
@@ -243,8 +229,8 @@
 
 (defne partitiono [a b c d]
   ([[?x . ?l] _ [?x . ?l1] _]
-     (nonrel/conda
-      ((nonrel/project [?x b]
+     (conda
+      ((project [?x b]
          (== (<= ?x b) true))
        (partition ?l b ?l1 d))
       (partition ?l b c d))))
\ No newline at end of file
diff --git a/src/main/clojure/clojure/core/logic/dcg.clj b/src/main/clojure/clojure/core/logic/dcg.clj
index 741cbdd7..f40395ac 100644
--- a/src/main/clojure/clojure/core/logic/dcg.clj
+++ b/src/main/clojure/clojure/core/logic/dcg.clj
@@ -1,7 +1,6 @@
 (ns clojure.core.logic.dcg
   (:refer-clojure :exclude [reify == inc])
-  (:use [clojure.core.logic minikanren prelude])
-  (:require [clojure.core.logic.nonrel :as nonrel]))
+  (:use [clojure.core.logic]))
 
 ;; TODO: think about indexing
 ;; TODO: note that rest args are problematic since we add two invisible args
@@ -198,7 +197,7 @@
   (def-->e digito [x]
     ([_] [x]
        (!dcg
-        (nonrel/project [x]
+        (project [x]
           (== (contains? digits x) true)))))
 
   (def-->e numo [x]
@@ -210,7 +209,7 @@
   (def-->e symo [x]
     ([[?a . ?as]] [?a]
        (!dcg
-        (nonrel/project [?a]
+        (project [?a]
           (conde
             ((== (contains? alpha ?a) true))
             ((== (contains? nonalnum ?a) true)))))
@@ -219,7 +218,7 @@
   (def-->e symro [x]
     ([[?a . ?as]] [?a]
        (!dcg
-        (nonrel/project [?a]
+        (project [?a]
           (conde
             ((== (contains? alnum ?a) true))
             ((== (contains? nonalnum ?a) true)))))
diff --git a/src/main/clojure/clojure/core/logic/disequality.clj b/src/main/clojure/clojure/core/logic/disequality.clj
deleted file mode 100644
index 1e99a303..00000000
--- a/src/main/clojure/clojure/core/logic/disequality.clj
+++ /dev/null
@@ -1,250 +0,0 @@
-(ns clojure.core.logic.disequality
-  (:refer-clojure :exclude [reify == inc])
-  (:use clojure.core.logic.minikanren
-        clojure.core.logic.match)
-  (:import [clojure.core.logic.minikanren Substitutions Pair]
-           [java.io Writer]))
-
-;; =============================================================================
-;; Utilities
-
-;; TODO: change to lazy-seq
-(defn prefix [s <s]
-  (if (= s <s)
-    ()
-    (cons (first s) (prefix (rest s) <s))))
-
-;; =============================================================================
-;; Verification
-
-(declare make-store)
-(declare merge-constraint)
-(declare make-c)
-(declare propagate)
-(declare get-simplified)
-(declare discard-simplified)
-(declare constraint-verify)
-
-(defn ^Substitutions constraint-verify-simple [^Substitutions s u v]
-  (let [uc (set (map #(walk s %) (constraints u)))]
-    (if (contains? uc v)
-      nil
-      (let [u (remove-constraints u)
-            v (if (lvar? v) (add-constraints v uc) v)]
-        (make-s (-> (.s s) (dissoc u) (assoc u v))
-                (cons (pair u v) (.l s))
-                constraint-verify
-                (.cs s))))))
-
-(defn ^Substitutions constraint-verify [^Substitutions s u v]
-  (when-let [s (constraint-verify-simple s u v)]
-    (if-let [cs (.cs s)]
-      (let [cs (propagate cs s u v)
-            ^Substitutions s (reduce (fn [s [u c]]
-                                       (constrain s u c))
-                                     s (get-simplified cs))
-            s (make-s (.s s) (.l s)
-                      constraint-verify (discard-simplified cs))]
-        (constraint-verify-simple s (get-var s u) v))
-      s)))
-
-(defprotocol IDisequality
-  (!=-verify [this sp]))
-
-(defn unify* [^Substitutions s m]
-  (loop [[[u v :as p] & r] (seq m) result {}]
-    (let [^Substitutions sp (unify s u v)]
-      (cond
-       (nil? p) result
-       (not sp) nil
-       (identical? s sp) (recur r result)
-       :else (recur r
-                    (conj result
-                          (first (prefix (.l sp) (.l s)))))))))
-
-(extend-type Substitutions
-  IDisequality
-  (!=-verify [this sp]
-             (let [^Substitutions sp sp]
-               (cond
-                (not sp) this
-                (= this sp) nil
-                :else (let [[[u v] :as c] (prefix (.l sp) (.l this))
-                            simple (= (count c) 1)]
-                        (if simple
-                          (let [u (walk this u)
-                                v (walk this v)]
-                            (if (= u v)
-                              nil
-                              (let [s (.s this)
-                                    u (add-constraint u v)
-                                    s (if (contains? s u)
-                                        (let [uv (s u)]
-                                          (-> s (dissoc u) (assoc u uv)))
-                                        (assoc s u unbound))
-                                    v (if (lvar? v) (add-constraint v u) v)
-                                    s (if (contains? s v)
-                                        (let [vv (s v)]
-                                          (-> s (dissoc v) (assoc v vv)))
-                                        (assoc s v unbound))]
-                                (make-s s (.l this) constraint-verify (.cs this)))))
-                          (let [r (unify* this c)]
-                            (cond
-                             (nil? r) this
-                             (empty? r) nil
-                             :else (make-s (.s this) (.l this) constraint-verify
-                                           (-> (or (.cs this) (make-store))
-                                               (merge-constraint
-                                                (make-c r))))))))))))
-
-;; =============================================================================
-;; Constraint
-
-;; need hashCode and equals for propagation bit
-(deftype Constraint [^String name ^clojure.lang.Associative m okeys hash]
-  Object
-  (equals [this o]
-          (and (.. this getClass (isInstance o))
-               (let [^Constraint o o]
-                 (identical? name (.name o)))))
-  (hashCode [_] hash)
-  clojure.lang.Associative
-  (containsKey [this key]
-               (contains? m key))
-  (entryAt [this key]
-           (.entryAt m key))
-  clojure.lang.IPersistentMap
-  (without [this key]
-           (Constraint. name (dissoc m key) okeys hash))
-  clojure.lang.ISeq
-  (first [_] (first m))
-  (seq [_] (seq m))
-  (count [_] (count m))
-  clojure.lang.ILookup
-  (valAt [this key]
-         (m key)))
-
-;; NOTE: gensym is slow don't use it directly
-(defn ^Constraint make-c [m]
-  (let [name (str "constraint-" (. clojure.lang.RT (nextID)))]
-    (Constraint. name m (keys m) (.hashCode name))))
-
-(defn constraint? [x]
-  (instance? Constraint x))
-
-(defmethod print-method Constraint [x ^Writer writer]
-           (.write writer (str "<constraint:" (.m ^Constraint x) ">")))
-
-;; =============================================================================
-;; Constraint Store
-
-(defprotocol IConstraintStore
-  (merge-constraint [this c])
-  (refine-constraint [this c u])
-  (discard-constraint [this c])
-  (propagate [this s u v])
-  (get-simplified [this])
-  (discard-simplified [this]))
-
-(deftype ConstraintStore [vmap cmap simple]
-  IConstraintStore
-  (merge-constraint [this c]
-                    (let [ks (keys c)]
-                      (reduce (fn [cs k] (assoc cs k c)) this ks))) ;; NOTE: switch to loop/recur?
-
-  (refine-constraint [this c u]
-                     (let [^Constraint c c
-                           name (.name c)
-                           ^Constraint c (dissoc (get cmap name) u)
-                           vmap (update-in vmap [u] #(disj % name))
-                           vmap (if (empty? (vmap u))
-                                  (dissoc vmap u)
-                                  vmap)]
-                       (if (= (count c) 1)
-                         (let [okeys (.okeys c)
-                               cmap (dissoc cmap name)
-                               vmap (reduce (fn [m v]
-                                              (update-in m [v] #(disj % name)))
-                                            vmap okeys)] ;; NOTE: hmm not all these keys exist
-                           ;; TODO: clear out empty vars like below
-                           (ConstraintStore. vmap cmap
-                                             (conj (or simple [])
-                                                   (first c))))
-                         (let [cmap (assoc cmap name c)]
-                           (ConstraintStore. vmap cmap simple)))))
-
-  (discard-constraint [this c]
-                      (let [^Constraint c c
-                            name (.name c)
-                            ^Constraint c (get cmap name)
-                            okeys (.okeys c)
-                            cmap (dissoc cmap name)
-                            vmap (reduce (fn [m v] ;; TODO: combine
-                                           (update-in m [v] #(disj % name)))
-                                         vmap okeys)
-                            vmap (reduce (fn [m v]
-                                           (if (empty? (m v))
-                                             (dissoc m v)
-                                             m))
-                                         vmap okeys)]
-                        (ConstraintStore. vmap cmap simple)))
-
-  (propagate [this s u v]
-             (if (contains? vmap u)
-               (let [cs (get this u)]
-                 (loop [[c & cr] cs me this]
-                   (if (nil? c)
-                     me
-                     (let [vp (walk s (get c u))]
-                       (cond
-                        (= vp v) (recur cr (refine-constraint me c u))
-                        (or (lvar? vp)
-                            (lvar? v)) (recur cr me)
-                            :else (recur cr (discard-constraint me c)))))))
-               this))
-
-  (get-simplified [this] simple)
-
-  (discard-simplified [this] (ConstraintStore. vmap cmap nil))
-
-  clojure.lang.Associative
-  (assoc [this u c]
-    (if (constraint? c)
-      (let [name (.name ^Constraint c)]
-        (ConstraintStore. (update-in vmap [u] (fnil #(conj % name) #{}))
-                          (assoc cmap name c) simple))
-      (throw (Exception. "Adding something which is not a constraint"))))
-
-  (containsKey [this key]
-               (contains? vmap key))
-
-  (entryAt [this key]
-           (when (contains? vmap key)
-             (let [val (when-let [s (seq (map #(cmap %) (vmap key)))]
-                         (vec s))]
-               (clojure.core/reify
-                clojure.lang.IMapEntry
-                (key [_] key)
-                (val [_] val)
-                Object
-                (toString [_] (.toString [key val]))))))
-
-  clojure.lang.ILookup
-  (valAt [this key]
-         (when (contains? vmap key)
-           (when-let [s (seq (map #(cmap %) (vmap key)))]
-             (vec s)))))
-
-(defn ^ConstraintStore make-store []
-  (ConstraintStore. {} {} nil))
-
-;; =============================================================================
-;; Syntax
-
-(defmacro != [u v]
-  "Impose a disequality constraint on u and v. If the two
-  terms ever unify will result in failure. u and v can be
-  compound terms allowing complex conditions to require
-  failure."
-  `(fn [a#]
-     (!=-verify a# (unify a# ~u ~v))))
diff --git a/src/main/clojure/clojure/core/logic/match.clj b/src/main/clojure/clojure/core/logic/match.clj
deleted file mode 100644
index 03decf14..00000000
--- a/src/main/clojure/clojure/core/logic/match.clj
+++ /dev/null
@@ -1,102 +0,0 @@
-(ns clojure.core.logic.match
-  (:refer-clojure :exclude [reify == inc])
-  (:use clojure.core.logic.minikanren)
-  (:require [clojure.set :as set])
-  (:import [clojure.core.logic.minikanren Substitutions]))
-
-(defn warn [& msg]
-  (binding [*out* *err*]
-    (apply println "WARNING:" msg)))
-
-(declare p->term)
-
-(defn lcons-p? [p]
-  (and (coll? p)
-       (not (nil? (some '#{.} p)))))
-
-(defn p->llist [p]
-  `(llist
-    ~@(map p->term
-           (remove #(contains? '#{.} %) p))))
-
-(defn p->term [p]
-  (cond
-   (= p '_) `(lvar)
-   (lcons-p? p) (p->llist p)
-   (and (coll? p)
-        (not= (first p) 'quote)) (cond
-                                  (list? p) p
-                                  :else `[~@(map p->term p)])
-   :else p))
-
-(defn lvar-sym? [s]
-  (= (first (str s)) \?))
-
-(defn extract-vars
-  ([p]
-     (set (cond
-           (lvar-sym? p) [p]
-           (coll? p) (filter lvar-sym? (flatten p))
-           :else nil)))
-  ([p seen]
-     (set/difference (extract-vars p) (set seen))))
-
-(defn fresh-expr? [cs]
-  (= (first cs) `fresh))
-
-(defn ex
-  ([vs t a]
-     `(fresh [~@vs]
-        (== ~t ~a)))
-  ([vs t a exprs]
-     (if (fresh-expr? exprs)
-       `(fresh [~@vs]
-          (== ~t ~a)
-          ~exprs)
-       `(fresh [~@vs]
-          (== ~t ~a)
-          ~@exprs))))
-
-(defn ex* [[[p a :as pa] & par] exprs seen]
-  (let [t (p->term p)
-        vs (extract-vars p seen)
-        seen (reduce conj seen vs)]
-    (cond
-     (nil? pa) exprs
-     (= p '_) (ex* par exprs seen)
-     (empty? par) (if exprs
-                    (ex vs t a exprs)
-                    (ex vs t a))
-     :else (let [r (ex* par exprs seen)]
-             (if r
-               (ex vs t a r)
-               (ex vs t a))))))
-
-(defn all-blank? [p]
-  (every? #(= % '_) p))
-
-(defn handle-clause [as]
-  (when-not (vector? as)
-    (throw (Exception. (str "Expecting vector of arguments, instead " as))))
-  (fn [[p & exprs]]
-    (when-not (vector? p)
-      (throw (Exception. (str "Expecting vector of matches, instead " p))))
-    (when-not (= (count p) (count as))
-      (warn "Differing number of matches. Matching" p "against" as))
-    (let [pas (partition 2 (interleave p as))
-          r (ex* pas exprs #{})]
-      (if (all-blank? p)
-        r
-        (list r)))))
-
-(defn handle-clauses [t as cs]
-  `(~t
-    ~@(map (handle-clause as) cs)))
-
-(defn defnm [t n as & cs]
-  (if-let [tabled? (-> n meta :tabled)]
-    `(def ~n
-          (clojure.core.logic.tabled/tabled [~@as]
-                               ~(handle-clauses t as cs)))
-    `(defn ~n [~@as]
-       ~(handle-clauses t as cs))))
diff --git a/src/main/clojure/clojure/core/logic/minikanren.clj b/src/main/clojure/clojure/core/logic/minikanren.clj
deleted file mode 100644
index 4d298593..00000000
--- a/src/main/clojure/clojure/core/logic/minikanren.clj
+++ /dev/null
@@ -1,1008 +0,0 @@
-(ns clojure.core.logic.minikanren
-  (:refer-clojure :exclude [reify == inc])
-  (:import [java.io Writer]))
-
-(def ^{:dynamic true} *occurs-check* true)
-
-(defprotocol IUnifyTerms
-  (unify-terms [u v s]))
-
-(defprotocol IUnifyWithNil
-  (unify-with-nil [v u s]))
-
-(defprotocol IUnifyWithObject
-  (unify-with-object [v u s]))
-
-(defprotocol IUnifyWithLVar
-  (unify-with-lvar [v u s]))
-
-(defprotocol IUnifyWithLSeq
-  (unify-with-lseq [v u s]))
-
-(defprotocol IUnifyWithSequential
-  (unify-with-seq [v u s]))
-
-(defprotocol IUnifyWithMap
-  (unify-with-map [v u s]))
-
-(defprotocol IUnifyWithSet
-  (unify-with-set [v u s]))
-
-(defprotocol IReifyTerm
-  (reify-term [v s]))
-
-(defprotocol IWalkTerm
-  (walk-term [v s]))
-
-(defprotocol IOccursCheckTerm
-  (occurs-check-term [v x s]))
-
-(defprotocol IBuildTerm
-  (build-term [u s]))
-
-(defprotocol IBind
-  (bind [this g]))
-
-(defprotocol IMPlus
-  (mplus [a f]))
-
-(defprotocol ITake
-  (take* [a]))
-
-(deftype Unbound [])
-(def ^Unbound unbound (Unbound.))
-
-;; =============================================================================
-;; Pair
-
-(defprotocol IPair
-  (lhs [this])
-  (rhs [this]))
-
-(deftype Pair [lhs rhs]
-  clojure.lang.Counted
-  (count [_] 2)
-  clojure.lang.Indexed
-  (nth [_ i] (case i
-                   0 lhs
-                   1 rhs
-                   (throw (IndexOutOfBoundsException.))))
-  (nth [_ i not-found] (case i
-                             0 lhs
-                             1 rhs
-                             not-found))
-  IPair
-  (lhs [_] lhs)
-  (rhs [_] rhs)
-  java.util.Map$Entry
-  (getKey [_] lhs)
-  (getValue [_] rhs)
-  Object
-  (toString [_]
-    (str "(" lhs " . " rhs ")")))
-
-(defn ^Pair pair [lhs rhs]
-  (Pair. lhs rhs))
-
-;; =============================================================================
-;; Substitutions
-
-(defprotocol ISubstitutions
-  (length [this])
-  (occurs-check [this u v])
-  (ext [this u v])
-  (ext-no-check [this u v])
-  (swap [this cu])
-  (constrain [this u c])
-  (get-var [this v])
-  (use-verify [this f])
-  (walk [this v])
-  (walk-var [this v])
-  (walk* [this v])
-  (unify [this u v])
-  (reify-lvar-name [_])
-  (-reify [this v])
-  (reify [this v])
-  (build [this u]))
-
-(declare empty-s)
-(declare unify-terms)
-(declare occurs-check-term)
-(declare reify-term)
-(declare walk-term)
-(declare build-term)
-(declare choice)
-(declare add-constraint)
-(declare lvar)
-(declare lvar?)
-(declare pair)
-(declare lcons)
-
-(deftype Substitutions [s l verify cs]
-  Object
-  (equals [this o]
-    (or (identical? this o)
-        (and (.. this getClass (isInstance o))
-             (= s ^clojure.lang.PersistentHashMap (.s ^Substitutions o)))))
-
-  ISubstitutions
-  (length [this] (count s))
-
-  (occurs-check [this u v]
-    (let [v (walk this v)]
-      (occurs-check-term v u this)))
-  
-  (ext [this u v]
-    (if (and *occurs-check* (occurs-check this u v))
-      nil
-      (ext-no-check this u v)))
-
-  (ext-no-check [this u v]
-    (verify this u v))
-
-  (swap [this cu]
-    (if (contains? s cu)
-      (let [v (s cu)]
-        (Substitutions. (-> s (dissoc cu) (assoc cu v)) l verify cs))
-      (Substitutions. (assoc s cu unbound) l verify cs)))
-
-  (constrain [this u c]
-    (let [u (walk this u)]
-      (swap this (add-constraint u c))))
-
-  (get-var [this v]
-    (first (find s v)))
-
-  (use-verify [this f]
-    (Substitutions. s l f cs))
-  
-  (walk [this v]
-    (loop [lv v [v vp] (find s v)]
-      (cond
-       (nil? v) lv
-       (identical? vp unbound) v
-       (not (lvar? vp)) vp
-       :else (recur vp (find s vp)))))
-  
-  (walk-var [this v]
-    (loop [lv v [v vp] (find s v)]
-      (cond
-       (nil? v) lv
-       (identical? vp unbound) v
-       (not (lvar? vp)) v
-       :else (recur vp (find s vp)))))
-  
-  (walk* [this v]
-    (let [v (walk this v)]
-      (walk-term v this)))
-
-  (unify [this u v]
-    (if (identical? u v)
-      this
-      (let [u (walk this u)
-            v (walk this v)]
-        (if (identical? u v)
-          this
-          (unify-terms u v this)))))
-
-  (reify-lvar-name [this]
-    (symbol (str "_." (count s))))
-
-  (-reify [this v]
-    (let [v (walk this v)]
-      (reify-term v this)))
-
-  (reify [this v]
-    (let [v (walk* this v)]
-      (walk* (-reify empty-s v) v)))
-
-  (build [this u]
-    (build-term u this))
-
-  IBind
-  (bind [this g]
-    (g this))
-  IMPlus
-  (mplus [this f]
-    (choice this f))
-  ITake
-  (take* [this] this))
-
-(defn ^Substitutions pass-verify [^Substitutions s u v]
-  (Substitutions. (assoc (.s s) u v)
-                  (cons (pair u v) (.l s))
-                  (.verify s)
-                  (.cs s)))
-
-(defn ^Substitutions make-s
-  ([m l] (Substitutions. m l pass-verify nil))
-  ([m l f] (Substitutions. m l f nil))
-  ([m l f cs] (Substitutions. m l f cs)))
-
-(def ^Substitutions empty-s (make-s {} '()))
-
-(defn subst? [x]
-  (instance? Substitutions x))
-
-(defn ^Substitutions to-s [v]
-  (let [s (reduce (fn [m [k v]] (assoc m k v)) {} v)
-        l (reduce (fn [l [k v]] (cons (Pair. k v) l)) '() v)]
-    (make-s s l)))
-
-;; =============================================================================
-;; Logic Variables
-
-(defprotocol ILVar
-  (constraints [this])
-  (add-constraint [this c])
-  (add-constraints [this ds])
-  (remove-constraint [this c])
-  (remove-constraints [this]))
-
-(deftype LVar [name hash cs meta]
-  clojure.lang.IObj
-  (meta [this]
-    meta)
-  (withMeta [this new-meta]
-    (LVar. name hash cs meta))
-  Object
-  (toString [_] (str "<lvar:" name ">"))
-  (equals [this o]
-    (and (.. this getClass (isInstance o))
-         (let [^LVar o o]
-           (identical? name (.name o)))))
-  (hashCode [_] hash)
-  ILVar
-  (constraints [_] cs)
-  (add-constraint [_ c] (LVar. name hash (conj (or cs #{}) c) meta))
-  (add-constraints [_ ds] (LVar. name hash (reduce conj (or cs #{}) ds) meta))
-  (remove-constraint [_ c] (LVar. name hash (disj cs c) meta))
-  (remove-constraints [_] (LVar. name hash nil meta))
-  IUnifyTerms
-  (unify-terms [u v s]
-    (unify-with-lvar v u s))
-  IUnifyWithNil
-  (unify-with-nil [v u s]
-    (ext-no-check s v u))
-  IUnifyWithObject
-  (unify-with-object [v u s]
-    (ext s v u))
-  IUnifyWithLVar
-  (unify-with-lvar [v u s]
-    (ext-no-check s u v))
-  IUnifyWithLSeq
-  (unify-with-lseq [v u s]
-    (ext s v u))
-  IUnifyWithSequential
-  (unify-with-seq [v u s]
-    (ext s v u))
-  IUnifyWithMap
-  (unify-with-map [v u s]
-    (ext s v u))
-  IUnifyWithSet
-  (unify-with-set [v u s]
-    (ext s v u))
-  IReifyTerm
-  (reify-term [v s]
-    (ext s v (reify-lvar-name s)))
-  IWalkTerm
-  (walk-term [v s] v)
-  IOccursCheckTerm
-  (occurs-check-term [v x s] (= (walk s v) x))
-  IBuildTerm
-  (build-term [u s]
-    (let [m (.s ^Substitutions s)
-          l (.l ^Substitutions s)
-          lv (lvar 'ignore) ]
-      (if (contains? m u)
-        s
-        (make-s (assoc m u lv)
-                (cons (Pair. u lv) l))))))
-
-(defn ^LVar lvar
-  ([]
-     (let [name (str (. clojure.lang.RT (nextID)))]
-       (LVar. name (.hashCode name) nil nil)))
-  ([name]
-     (let [name (str name "_" (. clojure.lang.RT (nextID)))]
-       (LVar. name (.hashCode name) nil nil)))
-  ([name cs]
-     (let [name (str name "_" (. clojure.lang.RT (nextID)))]
-       (LVar. name (.hashCode name) cs nil))))
-
-(defmethod print-method LVar [x ^Writer writer]
-  (.write writer (str "<lvar:" (.name ^LVar x) ">")))
-
-(defn lvar? [x]
-  (instance? LVar x))
-
-;; =============================================================================
-;; LCons
-
-(defmacro umi
-  [& args]
-  (if (resolve 'unchecked-multiply-int)
-    `(unchecked-multiply-int ~@args)
-    `(unchecked-multiply ~@args)))
-
-(defmacro uai
-  [& args]
-  (if (resolve 'unchecked-add-int)
-    `(unchecked-add-int ~@args)
-    `(unchecked-add ~@args)))
-
-(defprotocol LConsSeq
-  (lfirst [this])
-  (lnext [this]))
-
-;; TODO: clean up the printing code
-
-(defprotocol LConsPrint
-  (toShortString [this]))
-
-(declare lcons?)
-
-(deftype LCons [a d ^{:unsynchronized-mutable true :tag int} cache meta]
-  clojure.lang.IObj
-  (meta [this]
-    meta)
-  (withMeta [this new-meta]
-    (LCons. a d cache new-meta))
-  LConsSeq
-  (lfirst [_] a)
-  (lnext [_] d)
-  LConsPrint
-  (toShortString [this]
-    (cond
-     (.. this getClass (isInstance d)) (str a " " (toShortString d))
-     :else (str a " . " d )))
-  Object
-  (toString [this] (cond
-                    (.. this getClass (isInstance d)) (str "(" a " " (toShortString d) ")")
-                    :else (str "(" a " . " d ")")))
-  (equals [this o]
-    (or (identical? this o)
-        (and (.. this getClass (isInstance o))
-             (loop [me this
-                    you o]
-               (cond
-                (nil? me) (nil? you)
-                (lvar? me) true
-                (lvar? you) true
-                (and (lcons? me) (lcons? you))
-                  (let [mef  (lfirst me)
-                        youf (lfirst you)]
-                    (and (or (= mef youf)
-                             (lvar? mef)
-                             (lvar? youf))
-                         (recur (lnext me) (lnext you))))
-                :else (= me you))))))
-
-  (hashCode [this]
-    (if (= cache -1)
-      (do
-        (set! cache (uai (umi (int 31) (clojure.lang.Util/hash d))
-                         (clojure.lang.Util/hash a)))
-        cache)
-      cache))
-  IUnifyTerms
-  (unify-terms [u v s]
-    (unify-with-lseq v u s))
-  IUnifyWithNil
-  (unify-with-nil [v u s] false)
-  IUnifyWithObject
-  (unify-with-object [v u s] false)
-  IUnifyWithLVar
-  (unify-with-lvar [v u s]
-    (ext s u v))
-  IUnifyWithLSeq
-  (unify-with-lseq [v u s]
-    (loop [u u v v s s]
-      (if (lvar? u)
-        (unify s u v)
-        (cond
-         (lvar? v) (unify s v u)
-         (and (lcons? u) (lcons? v))
-           (if-let [s (unify s (lfirst u) (lfirst v))]
-             (recur (lnext u) (lnext v) s)
-             false)
-         :else (unify s u v)))))
-  IUnifyWithSequential
-  (unify-with-seq [v u s]
-    (unify-with-lseq u v s))
-  IUnifyWithMap
-  (unify-with-map [v u s] false)
-  IUnifyWithSet
-  (unify-with-set [v u s] false)
-  IReifyTerm
-  (reify-term [v s]
-    (loop [v v s s]
-      (if (lcons? v)
-        (recur (lnext v) (-reify s (lfirst v)))
-        (-reify s v))))
-  ;; TODO: no way to make this non-stack consuming w/o a lot more thinking
-  ;; we could use continuation passing style and trampoline
-  IWalkTerm
-  (walk-term [v s]
-    (lcons (walk* s (lfirst v))
-           (walk* s (lnext v))))
-  IOccursCheckTerm
-  (occurs-check-term [v x s]
-    (loop [v v x x s s]
-      (if (lcons? v)
-        (or (occurs-check s x (lfirst v))
-            (recur (lnext v) x s))
-        (occurs-check s x v))))
-  IBuildTerm
-  (build-term [u s]
-    (loop [u u s s]
-      (if (lcons? u)
-        (recur (lnext u) (build s (lfirst u)))
-        (build s u)))))
-
-(defmethod print-method LCons [x ^Writer writer]
-  (.write writer (str x)))
-
-(defn lcons [a d]
-  "Constructs a sequence a with an improper tail d if d is a logic variable."
-  (if (or (coll? d) (nil? d))
-    (cons a (seq d))
-    (LCons. a d -1 nil)))
-
-(defn lcons? [x]
-  (instance? LCons x))
-
-(defmacro llist
-  "Constructs a sequence from 2 or more arguments, with the last argument as the tail.
-  The tail is improper if the last argument is a logic variable."
-  ([f s] `(lcons ~f ~s))
-  ([f s & rest] `(lcons ~f (llist ~s ~@rest))))
-
-;; =============================================================================
-;; Unification
-
-;; TODO : a lot of cascading ifs need to be converted to cond
-
-(extend-protocol IUnifyTerms
-  nil
-  (unify-terms [u v s]
-    (unify-with-nil v u s)))
-
-(extend-type Object
-  IUnifyTerms
-  (unify-terms [u v s]
-    (unify-with-object v u s)))
-
-(extend-protocol IUnifyTerms
-  clojure.lang.Sequential
-  (unify-terms [u v s]
-    (unify-with-seq v u s)))
-
-(extend-protocol IUnifyTerms
-  clojure.lang.IPersistentMap
-  (unify-terms [u v s]
-    (unify-with-map v u s)))
-
-(extend-protocol IUnifyTerms
-  clojure.lang.IPersistentSet
-  (unify-terms [u v s]
-    (unify-with-set v u s)))
-
-;; -----------------------------------------------------------------------------
-;; Unify nil with X
-
-(extend-protocol IUnifyWithNil
-  nil
-  (unify-with-nil [v u s] s))
-
-(extend-type Object
-  IUnifyWithNil
-  (unify-with-nil [v u s] false))
-
-(extend-protocol IUnifyWithNil
-  clojure.lang.Sequential
-  (unify-with-nil [v u s] false))
-
-(extend-protocol IUnifyWithNil
-  clojure.lang.IPersistentMap
-  (unify-with-nil [v u s] false))
-
-(extend-protocol IUnifyWithNil
-  clojure.lang.IPersistentSet
-  (unify-with-nil [v u s] false))
-
-;; -----------------------------------------------------------------------------
-;; Unify Object with X
-
-(extend-protocol IUnifyWithObject
-  nil
-  (unify-with-object [v u s] false))
-
-(extend-type Object
-  IUnifyWithObject
-  (unify-with-object [v u s]
-    (if (= u v) s false)))
-
-(extend-protocol IUnifyWithObject
-  clojure.lang.Sequential
-  (unify-with-object [v u s] false))
-
-(extend-protocol IUnifyWithObject
-  clojure.lang.IPersistentMap
-  (unify-with-object [v u s] false))
-
-(extend-protocol IUnifyWithObject
-  clojure.lang.IPersistentSet
-  (unify-with-object [v u s] false))
-
-;; -----------------------------------------------------------------------------
-;; Unify LVar with X
-
-(extend-protocol IUnifyWithLVar
-  nil
-  (unify-with-lvar [v u s] (ext-no-check s u v)))
-
-(extend-type Object
-  IUnifyWithLVar
-  (unify-with-lvar [v u s]
-    (ext s u v)))
-
-(extend-protocol IUnifyWithLVar
-  clojure.lang.Sequential
-  (unify-with-lvar [v u s]
-    (ext s u v)))
-
-(extend-protocol IUnifyWithLVar
-  clojure.lang.IPersistentMap
-  (unify-with-lvar [v u s]
-    (ext s u v)))
-
-(extend-protocol IUnifyWithLVar
-  clojure.lang.IPersistentSet
-  (unify-with-lvar [v u s]
-    (ext s u v)))
-
-;; -----------------------------------------------------------------------------
-;; Unify LCons with X
-
-(extend-protocol IUnifyWithLSeq
-  nil
-  (unify-with-lseq [v u s] false))
-
-(extend-type Object
-  IUnifyWithLSeq
-  (unify-with-lseq [v u s] false))
-
-(extend-protocol IUnifyWithLSeq
-  clojure.lang.Sequential
-  (unify-with-lseq [v u s]
-    (loop [u u v v s s]
-      (if (seq v)
-        (if (lcons? u)
-          (if-let [s (unify s (lfirst u) (first v))]
-            (recur (lnext u) (next v) s)
-            false)
-          (unify s u v))
-        (if (lvar? u)
-          (unify s u '())
-          false)))))
-
-(extend-protocol IUnifyWithLSeq
-  clojure.lang.IPersistentMap
-  (unify-with-lseq [v u s] false))
-
-(extend-protocol IUnifyWithLSeq
-  clojure.lang.IPersistentSet
-  (unify-with-lseq [v u s] false))
-
-;; -----------------------------------------------------------------------------
-;; Unify Sequential with X
-
-(extend-protocol IUnifyWithSequential
-  nil
-  (unify-with-seq [v u s] false))
-
-(extend-type Object
-  IUnifyWithSequential
-  (unify-with-seq [v u s] false))
-
-(extend-protocol IUnifyWithSequential
-  clojure.lang.IPersistentMap
-  (unify-with-seq [v u s] false))
-
-(extend-protocol IUnifyWithSequential
-  clojure.lang.IPersistentSet
-  (unify-with-seq [v u s] false))
-
-(extend-protocol IUnifyWithSequential
-  clojure.lang.Sequential
-  (unify-with-seq [v u s]
-    (loop [u u v v s s]
-      (if (seq u)
-        (if (seq v)
-          (if-let [s (unify s (first u) (first v))]
-            (recur (next u) (next v) s)
-            false)
-          false)
-        (if (seq v) false s)))))
-
-;; -----------------------------------------------------------------------------
-;; Unify IPersistentMap with X
-
-(extend-protocol IUnifyWithMap
-  nil
-  (unify-with-map [v u s] false))
-
-(extend-type Object
-  IUnifyWithMap
-  (unify-with-map [v u s] false))
-
-(extend-protocol IUnifyWithMap
-  clojure.lang.Sequential
-  (unify-with-map [v u s] false))
-
-(extend-protocol IUnifyWithMap
-  clojure.lang.IPersistentMap
-  (unify-with-map [v u s]
-    (let [ks (keys u)]
-      (loop [ks ks u u v v s s]
-        (if (seq ks)
-          (let [kf (first ks)
-                vf (get v kf ::not-found)]
-            (if (= vf ::not-found)
-              false
-              (if-let [s (unify s (get u kf) vf)]
-                (recur (next ks) (dissoc u kf) (dissoc v kf) s)
-                false)))
-          (if (seq v)
-            false
-            s))))))
-
-(extend-protocol IUnifyWithMap
-  clojure.lang.IPersistentSet
-  (unify-with-map [v u s] false))
-
-;; -----------------------------------------------------------------------------
-;; Unify IPersistentSet with X
-
-(extend-protocol IUnifyWithSet
-  nil
-  (unify-with-set [v u s] false))
-
-(extend-type Object
-  IUnifyWithSet
-  (unify-with-set [v u s] false))
-
-(extend-protocol IUnifyWithSet
-  clojure.lang.Sequential
-  (unify-with-set [v u s] false))
-
-(extend-protocol IUnifyWithSet
-  clojure.lang.IPersistentMap
-  (unify-with-set [v u s] false))
-
-;; TODO : improve speed, the following takes 890ms
-;; 
-;; (let [a (lvar 'a)
-;;       b (lvar 'b)
-;;       c (lvar 'c)
-;;       d (lvar 'd)
-;;       s1 #{a b 3 4 5}
-;;       s2 #{1 2 3 c d}]
-;;     (dotimes [_ 10]
-;;       (time
-;;        (dotimes [_ 1e5]
-;;          (.s (unify empty-s s1 s2))))))
-
-(extend-protocol IUnifyWithSet
-  clojure.lang.IPersistentSet
-  (unify-with-set [v u s]
-    (loop [u u v v ulvars [] umissing []]
-      (if (seq u)
-        (if (seq v)
-          (let [uf (first u)]
-            (if (lvar? uf)
-              (recur (disj u uf) v (conj ulvars uf) umissing)
-              (if (contains? v uf)
-                (recur (disj u uf) (disj v uf) ulvars umissing)
-                (recur (disj u uf) v ulvars (conj umissing uf)))))
-          false)
-        (if (seq v)
-          (if (seq ulvars)
-            (loop [v v vlvars [] vmissing []]
-              (if (seq v)
-                (let [vf (first v)]
-                  (if (lvar? vf)
-                    (recur (disj v vf) (conj vlvars vf) vmissing)
-                    (recur (disj v vf) vlvars (conj vmissing vf))))
-                (unify s (concat ulvars umissing)
-                       (concat vmissing vlvars))))
-            false)
-          s)))))
-
-;; =============================================================================
-;; Reification
-
-(extend-protocol IReifyTerm
-  nil
-  (reify-term [v s] s))
-
-(extend-type Object
-  IReifyTerm
-  (reify-term [v s] s))
-
-(extend-protocol IReifyTerm
-  clojure.lang.IPersistentCollection
-  (reify-term [v s]
-    (loop [v v s s]
-      (if (seq v)
-        (recur (next v) (-reify s (first v)))
-        s))))
-
-;; =============================================================================
-;; Walk Term
-
-(extend-protocol IWalkTerm
-  nil
-  (walk-term [v s] nil))
-
-(extend-type Object
-  IWalkTerm
-  (walk-term [v s] v))
-
-(extend-protocol IWalkTerm
-  clojure.lang.ISeq
-  (walk-term [v s]
-    (map #(walk* s %) v)))
-
-(extend-protocol IWalkTerm
-  clojure.lang.IPersistentVector
-  (walk-term [v s]
-    (loop [v v r (transient [])]
-      (if (seq v)
-        (recur (next v) (conj! r (walk* s (first v))))
-        (persistent! r)))))
-
-(extend-protocol IWalkTerm
-  clojure.lang.IPersistentMap
-  (walk-term [v s]
-    (loop [v v r (transient {})]
-      (if (seq v)
-        (let [[vfk vfv] (first v)]
-          (recur (next v) (assoc! r vfk (walk* s vfv))))
-        (persistent! r)))))
-
-(extend-protocol IWalkTerm
-  clojure.lang.IPersistentSet
-  (walk-term [v s]
-    (loop [v v r {}]
-      (if (seq v)
-        (recur (next v) (conj r (walk* s (first v))))
-        r))))
-
-;; =============================================================================
-;; Occurs Check Term
-
-(extend-protocol IOccursCheckTerm
-  nil
-  (occurs-check-term [v x s] false))
-
-(extend-type Object
-  IOccursCheckTerm
-  (occurs-check-term [v x s] false))
-
-(extend-protocol IOccursCheckTerm
-  clojure.lang.IPersistentCollection
-  (occurs-check-term [v x s]
-    (loop [v v x x s s]
-      (if (seq v)
-        (or (occurs-check s x (first v))
-            (recur (next v) x s))
-        false))))
-
-;; =============================================================================
-;; Build Term
-
-(extend-protocol IBuildTerm
-  nil
-  (build-term [u s] s))
-
-(extend-type Object
-  IBuildTerm
-  (build-term [u s] s))
-
-(extend-protocol IBuildTerm
-  clojure.lang.ISeq
-  (build-term [u s]
-    (reduce build s u)))
-
-;; =============================================================================
-;; Goals and Goal Constructors
-
-(defmacro bind*
-  ([a g] `(bind ~a ~g))
-  ([a g & g-rest]
-     `(bind* (bind ~a ~g) ~@g-rest)))
-
-(defmacro mplus*
-  ([e] e)
-  ([e & e-rest]
-     `(mplus ~e (fn [] (mplus* ~@e-rest)))))
-
-(defmacro inc [& rest]
-  `(fn inc [] ~@rest))
-
-(extend-type Object
-  ITake
-  (take* [this] this))
-
-;; TODO: Choice always holds a as a list, can we just remove that?
-
-(deftype Choice [a f]
-  IBind
-  (bind [this g]
-    (mplus (g a) (inc (bind f g))))
-  IMPlus
-  (mplus [this fp]
-    (Choice. a (fn [] (mplus (fp) f))))
-  ITake
-  (take* [this]
-    (lazy-seq (cons (first a) (lazy-seq (take* f))))))
-
-(defn ^Choice choice [a f]
-  (Choice. a f))
-
-;; -----------------------------------------------------------------------------
-;; MZero
-
-(extend-protocol IBind
-  nil
-  (bind [_ g] nil))
-
-(extend-protocol IMPlus
-  nil
-  (mplus [_ b] b))
-
-(extend-protocol ITake
-  nil
-  (take* [_] '()))
-
-;; -----------------------------------------------------------------------------
-;; Unit
-
-(extend-type Object
-  IMPlus
-  (mplus [this f]
-    (Choice. this f)))
-
-;; -----------------------------------------------------------------------------
-;; Inc
-
-(extend-type clojure.lang.Fn
-  IBind
-  (bind [this g]
-    (inc (bind (this) g)))
-  IMPlus
-  (mplus [this f]
-    (inc (mplus (f) this)))
-  ITake
-  (take* [this] (lazy-seq (take* (this)))))
-
-;; =============================================================================
-;; Syntax
-
-(defn succeed [a]
-  "A goal that always succeeds."
-  a)
-
-(defn fail [a] 
-  "A goal that always fails."
-  nil)
-
-(def s# succeed)
-
-(def u# fail)
-
-(defmacro == [u v]
-  "A goal that attempts to unify terms u and v."
-  `(fn [a#]
-     (if-let [b# (unify a# ~u ~v)]
-       b# nil)))
-
-(defn bind-conde-clause [a]
-  (fn [g-rest]
-    `(bind* ~a ~@g-rest)))
-
-(defn bind-conde-clauses [a clauses]
-  (map (bind-conde-clause a) clauses))
-
-(defmacro conde [& clauses]
-  "Logical disjunction of the clauses. The first goal in
-  a clause is considered the head of that clause. Interleaves the
-  execution of the clauses."
-  (let [a (gensym "a")]
-    `(fn [~a]
-       (inc
-        (mplus* ~@(bind-conde-clauses a clauses))))))
-
-(defn lvar-bind [sym]
-  ((juxt identity
-         (fn [s] `(lvar '~s))) sym))
-
-(defn lvar-binds [syms]
-  (mapcat lvar-bind syms))
-
-(defmacro fresh [[& lvars] & goals]
-  "Creates fresh variables. Goals occuring within form a logical 
-  conjunction."
-  `(fn [a#]
-     (inc
-      (let [~@(lvar-binds lvars)]
-        (bind* a# ~@goals)))))
-
-(defmacro solve [& [n [x] & goals]]
-  `(let [xs# (take* (fn []
-                      ((fresh [~x] ~@goals
-                         (fn [a#]
-                           (cons (reify a# ~x) '()))) ;; TODO: do we need this?
-                       empty-s)))]
-     (if ~n
-       (take ~n xs#)
-       xs#)))
-
-(defmacro run [n & goals]
-  "Executes goals until a maximum of n results are found."
-  `(doall (solve ~n ~@goals)))
-
-(defmacro run* [& goals]
-  "Executes goals until results are exhausted."
-  `(run false ~@goals))
-
-(defmacro run-nc [& [n & goals]]
-  "Executes goals until a maximum of n results are found. Does not occurs-check."
-  `(binding [*occurs-check* false]
-     (run ~n ~@goals)))
-
-(defmacro run-nc* [& goals]
-  "Executes goals until results are exhausted. Does not occurs-check."
-  `(run-nc false ~@goals))
-
-(defmacro lazy-run [& [n & goals]]
-  "Lazily executes goals until a maximum of n results are found."
-  `(solve ~n ~@goals))
-
-(defmacro lazy-run* [& goals]
-  "Lazily executes goals until results are exhausted."
-  `(solve false ~@goals))
-
-(defn sym->lvar [sym]
-  `(lvar '~sym))
-
-(defmacro all
-  "Like fresh but does does not create logic variables."
-  ([] `clojure.core.logic.minikanren/s#)
-  ([& goals] `(fn [a#] (bind* a# ~@goals))))
-
-;; =============================================================================
-;; Debugging
-
-(defmacro log [s]
-  `(fn [a#]
-     (println ~s)
-     a#))
-
-(defmacro trace-s []
-  `(fn [a#]
-     (println (str a#))
-     a#))
-
-(defn trace-lvar [a lvar]
-  `(println (format "%5s = %s" (str '~lvar) (reify ~a ~lvar))))
-
-(defmacro trace-lvars [title & lvars]
-  "Goal for tracing the values of logic variables."
-  (let [a (gensym "a")]
-    `(fn [~a]
-       (println ~title)
-       ~@(map (partial trace-lvar a) lvars)
-       ~a)))
\ No newline at end of file
diff --git a/src/main/clojure/clojure/core/logic/nonrel.clj b/src/main/clojure/clojure/core/logic/nonrel.clj
deleted file mode 100644
index 53acbef2..00000000
--- a/src/main/clojure/clojure/core/logic/nonrel.clj
+++ /dev/null
@@ -1,149 +0,0 @@
-(ns clojure.core.logic.nonrel
-  (:refer-clojure :exclude [reify == inc])
-  (:use [clojure.core.logic.minikanren :exclude [lvar]]
-        clojure.core.logic.match)
-  (:import [clojure.core.logic.minikanren Substitutions Choice]))
-
-;; =============================================================================
-;; project
-
-(defn project-binding [s]
-  (fn [var]
-    `(~var (walk* ~s ~var))))
-
-(defn project-bindings [vars s]
-  (reduce concat (map (project-binding s) vars)))
-
-(defmacro project [[& vars] & goals]
-  "Extract the values bound to the specified logic vars. Non-relational."
-  (let [a (gensym "a")]
-    `(fn [~a]
-       (let [~@(project-bindings vars a)]
-         ((fresh []
-            ~@goals) ~a)))))
-
-;; =============================================================================
-;; conda (soft-cut), condu (committed-choice)
-;;
-;; conda once a line succeeds no others are tried
-;; condu a line can succeed only one time
-
-;; TODO : conda and condu should probably understanding logging
-
-(defprotocol IIfA
-  (ifa [b gs c]))
-
-(defprotocol IIfU
-  (ifu [b gs c]))
-
-;; TODO : if -> when
-
-(defmacro ifa*
-  ([])
-  ([[e & gs] & grest]
-     `(ifa ~e [~@gs]
-           ~(if (seq grest)
-              `(delay (ifa* ~@grest))
-              nil))))
-
-(defmacro ifu*
-  ([])
-  ([[e & gs] & grest]
-     `(ifu ~e [~@gs]
-           ~(if (seq grest)
-              `(delay (ifu* ~@grest))
-              nil))))
-
-(extend-protocol IIfA
-  nil
-  (ifa [b gs c]
-       (when c
-         (force c))))
-
-(extend-protocol IIfU
-  nil
-  (ifu [b gs c]
-       (when c
-         (force c))))
-
-(extend-type Substitutions
-  IIfA
-  (ifa [b gs c]
-       (loop [b b [g0 & gr] gs]
-         (if g0
-           (when-let [b (g0 b)]
-             (recur b gr))
-           b))))
-
-(extend-type Substitutions
-  IIfU
-  (ifu [b gs c]
-       (loop [b b [g0 & gr] gs]
-         (if g0
-           (when-let [b (g0 b)]
-             (recur b gr))
-           b))))
-
-(extend-type clojure.lang.Fn
-  IIfA
-  (ifa [b gs c]
-       (inc (ifa (b) gs c))))
-
-(extend-type clojure.lang.Fn
-  IIfU
-  (ifu [b gs c]
-       (inc (ifu (b) gs c))))
-
-(extend-protocol IIfA
-  Choice
-  (ifa [b gs c]
-       (reduce bind b gs)))
-
-;; TODO: Choice always holds a as a list, can we just remove that?
-(extend-protocol IIfU
-  Choice
-  (ifu [b gs c]
-       (reduce bind (.a ^Choice b) gs)))
-
-(defn cond-clauses [a]
-  (fn [goals]
-    `((~(first goals) ~a) ~@(rest goals))))
-
-(defmacro conda
-  [& clauses]
-  "Soft cut. Once the head of a clause has succeeded
-  all other clauses will be ignored. Non-relational."
-  (let [a (gensym "a")]
-    `(fn [~a]
-       (ifa* ~@(map (cond-clauses a) clauses)))))
-
-(defmacro condu [& clauses]
-  "Committed choice. Once the head (first goal) of a clause 
-  has succeeded, remaining goals of the clause will only
-  be run once. Non-relational."
-  (let [a (gensym "a")]
-    `(fn [~a]
-       (ifu* ~@(map (cond-clauses a) clauses)))))
-
-;; =============================================================================
-;; copy-term
-
-(defn copy-term [u v]
-  "Copies a term u into v. Non-relational."
-  (project [u]
-    (== (walk* (build empty-s u) u) v)))
-
-;; =============================================================================
-;; lvar nonlvar
-
-(defmacro lvaro [v]
-  "Goal to test whether a logic var is ground. Non-relational."
-  `(fn [a#]
-     (if (lvar? (walk a# ~v))
-       a# nil)))
-
-(defmacro nonlvaro [v]
-  "Goal to test whether a logic var is ground. Non-relational."
-  `(fn [a#]
-     (if (not (lvar? (walk a# ~v)))
-       a# nil)))
\ No newline at end of file
diff --git a/src/main/clojure/clojure/core/logic/prelude.clj b/src/main/clojure/clojure/core/logic/prelude.clj
deleted file mode 100644
index 34fbe2bb..00000000
--- a/src/main/clojure/clojure/core/logic/prelude.clj
+++ /dev/null
@@ -1,245 +0,0 @@
-(ns clojure.core.logic.prelude
-  (:refer-clojure :exclude [reify == inc])
-  (:use clojure.core.logic.minikanren)
-  (:require [clojure.set :as set]
-            [clojure.core.logic.nonrel :as nonrel]
-            [clojure.core.logic.tabled :as tabled]
-            [clojure.core.logic.match :as match]))
-
-;; =============================================================================
-;; Useful goals
-
-(defn nilo [a]
-  "Goal that unifies its argument with nil."
-  (== nil a))
-
-(defn emptyo [a]
-  "Goal that unifies its argument with the empty list."
-  (== '() a))
-
-(defn conso [a d l]
-  "The cons operation as a relation. Can be used to
-  construct a list or destructure one."
-  (== (lcons a d) l))
-
-(defn firsto [l a]
-  "first as a relation."
-  (fresh [d]
-    (conso a d l)))
-
-(defn resto [l d]
-  "rest as a relation."
-  (fresh [a]
-    (== (lcons a d) l)))
-
-;; =============================================================================
-;; Goal sugar syntax
-
-(defmacro defne [& rest]
-  "Define a goal fn. Supports pattern matching. All
-   patterns will be tried. See conde."
-  (apply match/defnm `conde rest))
-
-(defmacro matche [xs & cs]
-  "Pattern matching macro. All patterns will be tried.
-  See conde."
-  (match/handle-clauses `conde xs cs))
-
-;; -----------------------------------------------------------------------------
-;; defnu, defna, matcha, matchu
-
-;; TODO: we need to rethink defna and defnu, the unification comes first
-;; the *question* should come first
-
-(defmacro defna [& rest]
-  "Define a soft cut goal. See conda."
-  (apply match/defnm 'clojure.core.logic.nonrel/conda rest))
-
-(defmacro defnu [& rest]
-  "Define a committed choice goal. See condu."
-  (apply match/defnm 'clojure.core.logic.nonrel/condu rest))
-
-(defmacro matcha [xs & cs]
-  "Define a soft cut pattern match. See conda."
-  (match/handle-clauses 'clojure.core.logic.nonrel/conda xs cs))
-
-(defmacro matchu [xs & cs]
-  "Define a committed choice goal. See condu."
-  (match/handle-clauses 'clojure.core.logic.nonrel/condu xs cs))
-
-;; ==============================================================================
-;; More convenient goals
-
-(defne membero [x l]
-  ([_ [x . ?tail]])
-  ([_ [?head . ?tail]]
-     (membero x ?tail)))
-
-(defne appendo [x y z]
-  ([() _ y])
-  ([[?a . ?d] _ [?a . ?r]] (appendo ?d y ?r)))
-
-;; =============================================================================
-;; Rel
-
-(defn to-stream [aseq]
-  (when (seq aseq)
-    (choice (first aseq)
-            (fn [] (to-stream (next aseq))))))
-
-(defmacro def-arity-exc-helper []
-  (try
-    (Class/forName "clojure.lang.ArityException")
-    `(defn arity-exc-helper [~'name ~'n]
-       (fn [~'& ~'args]
-         (throw (clojure.lang.ArityException. ~'n (str ~'name)))))
-    (catch java.lang.ClassNotFoundException e
-     `(defn ~'arity-exc-helper [~'name ~'n]
-        (fn [~'& ~'args]
-          (throw (java.lang.IllegalArgumentException.
-                  (str "Wrong number of args (" ~'n ") passed to:" ~'name))))))))
-
-(def-arity-exc-helper)
-
-(defn sym-helper [prefix n]
-  (symbol (str prefix n)))
-
-(def f-sym (partial sym-helper "f"))
-(def a-sym (partial sym-helper "a"))
-
-(defn ->sym [& args]
-  (symbol (apply str args)))
-
-(defn defrel-helper [name arity args]
-  (let [r (range 1 (+ arity 2))
-        arity-excs (fn [n] `(arity-exc-helper '~name ~n))]
-    (if (seq args)
-      `(do
-         (def ~name (~'clojure.core.logic.prelude.Rel. '~name (atom {}) nil ~@(map arity-excs r)))
-         (extend-rel ~name ~@args))
-      `(def ~name (~'clojure.core.logic.prelude.Rel. '~name (atom {}) nil ~@(map arity-excs r))))))
-
-(defmacro def-apply-to-helper [n]
-  (let [r (range 1 (clojure.core/inc n))
-        args (map a-sym r)
-        arg-binds (fn [n]
-                    (mapcat (fn [a]
-                              `(~a (first ~'arglist) ~'arglist (next ~'arglist)))
-                            (take n args)))
-        case-clause (fn [n]
-                      `(~n (let [~@(arg-binds (dec n))]
-                            (.invoke ~'ifn ~@(take (dec n) args)
-                                     (clojure.lang.Util/ret1 (first ~'arglist) nil)))))]
-   `(defn ~'apply-to-helper [~(with-meta 'ifn {:tag clojure.lang.IFn}) ~'arglist]
-      (case (clojure.lang.RT/boundedLength ~'arglist 20)
-            ~@(mapcat case-clause r)))))
-
-(def-apply-to-helper 20)
-
-(defprotocol IRel
-  (setfn [this arity f])
-  (indexes-for [this arity])
-  (add-indexes [this arity index]))
-
-;; TODO: consider moving the set/indexes inside Rel, perf implications?
-
-(defmacro RelHelper [arity]
-  (let [r (range 1 (+ arity 2))
-        fs (map f-sym r)
-        mfs (map #(with-meta % {:volatile-mutable true :tag clojure.lang.IFn})
-                 fs)
-        create-sig (fn [n]
-                     (let [args (map a-sym (range 1 (clojure.core/inc n)))]
-                       `(~'invoke [~'_ ~@args]
-                                  (~(f-sym n) ~@args))))
-        set-case (fn [[f arity]]
-                   `(~arity (set! ~f ~'f)))]
-    `(do
-       (deftype ~'Rel [~'name ~'indexes ~'meta
-                       ~@mfs]
-         clojure.lang.IObj
-         (~'withMeta [~'_ ~'meta]
-           (~'Rel. ~'name ~'indexes ~'meta ~@fs))
-         (~'meta [~'_]
-           ~'meta)
-         clojure.lang.IFn
-         ~@(map create-sig r)
-         (~'applyTo [~'this ~'arglist]
-            (~'apply-to-helper ~'this ~'arglist))
-         ~'IRel
-         (~'setfn [~'_ ~'arity ~'f]
-           (case ~'arity
-                 ~@(mapcat set-case (map vector fs r))))
-         (~'indexes-for [~'_ ~'arity]
-           ((deref ~'indexes) ~'arity))
-         (~'add-indexes [~'_ ~'arity ~'index]
-           (swap! ~'indexes assoc ~'arity ~'index)))
-       (defmacro ~'defrel [~'name ~'& ~'rest]
-         (defrel-helper ~'name ~arity ~'rest)))))
-
-(RelHelper 20)
-
-(defn index-sym [name arity o]
-  (->sym name "_" arity "-" o "-index"))
-
-(defn set-sym [name arity]
-  (->sym name "_" arity "-set"))
-
-;; TODO: for arity greater than 20, we need to use rest args
-
-(defmacro extend-rel [name & args]
-  (let [arity (count args)
-        r (range 1 (clojure.core/inc arity))
-        as (map a-sym r)
-        indexed (vec (filter (fn [[a i]]
-                               (-> a meta :index))
-                             (map vector
-                                  args
-                                  (range 1 (clojure.core/inc arity)))))
-        check-lvar (fn [[o i]]
-                     (let [a (a-sym i)]
-                       `((not (~'lvar? (~'walk* ~'a ~a)))
-                         ((deref ~(index-sym name arity o)) (~'walk* ~'a ~a)))))
-        indexed-set (fn [[o i]]
-                      `(def ~(index-sym name arity o) (atom {})))]
-    (if (<= arity 20)
-     `(do
-        (def ~(set-sym name arity) (atom #{}))
-        ~@(map indexed-set indexed)
-        (add-indexes ~name ~arity '~indexed)
-        (setfn ~name ~arity
-               (fn [~@as]
-                 (fn [~'a]
-                   (let [set# (cond
-                               ~@(mapcat check-lvar indexed)
-                               :else (deref ~(set-sym name arity)))]
-                     (~'to-stream
-                      (->> set#
-                           (map (fn [cand#]
-                                  (when-let [~'a (~'unify ~'a [~@as] cand#)]
-                                    ~'a)))
-                           (remove nil?)))))))))))
-
-;; TODO: Should probably happen in a transaction
-
-(defn facts
-  "Define a series of facts. Takes a vector of vectors where each vector
-   represents a fact tuple, all with the same number of elements."
-  ([rel [f :as tuples]] (facts rel (count f) tuples))
-  ([^Rel rel arity tuples]
-     (let [rel-set (var-get (resolve (set-sym (.name rel) arity)))
-           tuples (map vec tuples)]
-       (swap! rel-set (fn [s] (into s tuples)))
-       (let [indexes (indexes-for rel arity)]
-         (doseq [[o i] indexes]
-           (let [index (var-get (resolve (index-sym (.name rel) arity o)))]
-             (let [indexed-tuples (map (fn [t]
-                                         {(nth t (dec i)) #{t}})
-                                       tuples)]
-               (swap! index
-                      (fn [i]
-                        (apply merge-with set/union i indexed-tuples))))))))))
-
-(defn fact [rel & tuple]
-  "Add a fact to a relation defined with defrel."
-  (facts rel [(vec tuple)]))
diff --git a/src/main/clojure/clojure/core/logic/tabled.clj b/src/main/clojure/clojure/core/logic/tabled.clj
deleted file mode 100644
index 10ac5d8f..00000000
--- a/src/main/clojure/clojure/core/logic/tabled.clj
+++ /dev/null
@@ -1,175 +0,0 @@
-;; See - William Byrd “Relational Programming in miniKanren:
-;; Techniques, Applications, and Implementations”
-
-(ns clojure.core.logic.tabled
-  (:refer-clojure :exclude [reify == inc])
-  (:use clojure.core.logic.minikanren)
-  (:import [clojure.core.logic.minikanren Substitutions Choice]))
-
-;; =============================================================================
-;; Data Structures
-;; (atom []) is cache, waiting streams are PersistentVectors
-
-(defprotocol ISuspendedStream
-  (ready? [this]))
-
-(deftype SuspendedStream [cache ansv* f]
-  ISuspendedStream
-  (ready? [this]
-          (not= @cache ansv*)))
-
-(defn ^SuspendedStream make-ss [cache ansv* f]
-  {:pre [(instance? clojure.lang.Atom cache)
-         (list? ansv*)
-         (fn? f)]}
-  (SuspendedStream. cache ansv* f))
-
-(defn ss? [x]
-  (instance? SuspendedStream x))
-
-(defn to-w [s]
-  (into [] s))
-
-(defn w? [x]
-  (vector? x))
-
-(defn w-check [w sk fk]
-  (loop [w w a []]
-    (cond
-     (nil? w) (fk)
-     (ready? (first w)) (sk
-                         (fn []
-                           (let [^SuspendedStream ss (first w)
-                                 f (.f ss)
-                                 w (to-w (concat a (next w)))]
-                             (if (empty? w)
-                               (f)
-                               (mplus (f) (fn [] w))))))
-     :else (recur (next w) (conj a (first w))))))
-
-;; -----------------------------------------------------------------------------
-;; Extend Substitutions to support tabling
-
-(defprotocol ITabled
-  (-reify-tabled [this v])
-  (reify-tabled [this v])
-  (alpha-equiv? [this x y])
-  (reuse [this argv cache start end])
-  (subunify [this arg ans]))
-
-;; CONSIDER: subunify, reify-term-tabled, extending all the necessary types to them
-
-(extend-type Substitutions
-  ITabled
-
-  (-reify-tabled [this v]
-                 (let [v (walk this v)]
-                   (cond
-                    (lvar? v) (ext-no-check this v (lvar (count (.s this))))
-                    (coll? v) (-reify-tabled
-                               (-reify-tabled this (first v))
-                               (next v))
-                    :else this)))
-
-  (reify-tabled [this v]
-                (let [v (walk* this v)]
-                  (walk* (-reify-tabled empty-s v) v)))
-
-  (alpha-equiv? [this x y]
-                (= (reify this x) (reify this y)))
-
-  (reuse [this argv cache start end]
-         (let [start (or start @cache)
-               end   (or end [])]
-           (letfn [(reuse-loop [ansv*]
-                     (if (= ansv* end)
-                       [(make-ss cache start
-                                 (fn [] (reuse this argv cache @cache start)))]
-                       (Choice. (subunify this argv (reify-tabled this (first ansv*)))
-                                (fn [] (reuse-loop (rest ansv*))))))]
-             (reuse-loop start))))
-
-  (subunify [this arg ans]
-            (let [arg (walk this arg)]
-              (cond
-               (= arg ans) this
-               (lvar? arg) (ext-no-check this arg ans)
-               (coll? arg) (subunify
-                            (subunify this (next arg) (next ans))
-                            (first arg) (first ans))
-               :else this))))
-
-;; -----------------------------------------------------------------------------
-;; Waiting Stream
-
-(extend-type clojure.lang.IPersistentVector
-  IBind
-  (bind [this g]
-        (w-check this
-                 (fn [f] (bind f g))
-                 (fn [] (to-w
-                         (map (fn [^SuspendedStream ss]
-                                (make-ss (.cache ss) (.ansv* ss)
-                                         (fn [] (bind ((.f ss)) g))))
-                              this)))))
-  IMPlus
-  (mplus [this f]
-         (w-check this
-                  (fn [fp] (mplus fp f))
-                  (fn []
-                    (let [a-inf (f)]
-                      (if (w? a-inf)
-                        (to-w (concat a-inf this))
-                        (mplus a-inf (fn [] this)))))))
-  ITake
-  (take* [this]
-         (w-check this
-                  (fn [f] (take* f))
-                  (fn [] ()))))
-
-(defn master [argv cache]
-  (fn [a]
-    (when (every? (fn [ansv]
-                    (not (alpha-equiv? a argv ansv)))
-                  @cache)
-      (do (swap! cache conj (reify-tabled a argv))
-          a))))
-
-;; -----------------------------------------------------------------------------
-;; Syntax
-
-;; TODO: consider the concurrency implications much more closely
-
-(defn table [goal]
-  "Function to table a goal. Useful when tabling should only persist
-  for the duration of a run."
-  (let [table (atom {})]
-    (fn [& args]
-      (let [argv args]
-        (fn [a]
-          (let [key (reify a argv)
-                cache (get @table key)]
-            (if (nil? cache)
-              (let [cache (atom ())]
-                (swap! table assoc key cache)
-                ((fresh []
-                   (apply goal args)
-                   (master argv cache)) a))
-              (reuse a argv cache nil nil))))))))
-
-(defmacro tabled [args & grest]
-  "Macro for defining a tabled goal. Prefer ^:tabled with the 
-  defne/a/u forms over using this directly."
-  `(let [table# (atom {})]
-     (fn [~@args]
-       (let [argv# ~args]
-         (fn [a#]
-           (let [key# (reify a# argv#)
-                 cache# (get @table# key#)]
-             (if (nil? cache#)
-               (let [cache# (atom ())]
-                 (swap! table# assoc key# cache#)
-                 ((fresh []
-                    ~@grest
-                    (master argv# cache#)) a#))
-               (reuse a# argv# cache# nil nil))))))))
\ No newline at end of file
diff --git a/src/main/clojure/clojure/core/logic/unify.clj b/src/main/clojure/clojure/core/logic/unify.clj
deleted file mode 100644
index 3010aadf..00000000
--- a/src/main/clojure/clojure/core/logic/unify.clj
+++ /dev/null
@@ -1,93 +0,0 @@
-(ns clojure.core.logic.unify
-  (:use [clojure.walk :only [postwalk]]
-        clojure.set)
-  (:require [clojure.core.logic.minikanren :as mk]))
-
-(defn lvarq-sym? [s]
-  (and (symbol? s) (= (first (str s)) \?)))
-
-(defn rem-? [s]
-  (symbol (apply str (drop 1 (str s)))))
-
-(defn proc-lvar [lvar-expr store]
-  (let [v (if-let [u (@store lvar-expr)]
-            u
-            (mk/lvar (rem-? lvar-expr)))]
-    (swap! store conj [lvar-expr v])
-    v))
-
-(defn lcons-expr? [expr]
-  (and (seq? expr) (some '#{.} (set expr))))
-
-(declare prep*)
-
-(defn replace-lvar [store]
-  (fn [expr]
-    (if (lvarq-sym? expr)
-      (proc-lvar expr store)
-      (if (lcons-expr? expr)
-        (prep* expr store)
-        expr))))
-
-(defn prep*
-  ([expr store] (prep* expr store false false))
-  ([expr store lcons?] (prep* expr store lcons? false))
-  ([expr store lcons? last?]
-     (let [expr (if (and last? (seq expr))
-                  (first expr)
-                  expr)]
-       (cond
-        (lvarq-sym? expr) (proc-lvar expr store)
-        (seq? expr) (if (or lcons? (lcons-expr? expr))
-                      (let [[f & n] expr
-                            skip (= f '.)
-                            tail (prep* n store lcons? skip)]
-                        (if skip
-                          tail
-                          (mk/lcons (prep* f store) tail)))
-                      (postwalk (replace-lvar store) expr))
-        :else expr))))
-
-(defn prep [expr]
-  "Prep a quoted expression. All symbols preceded by ? will
-  be replaced with logic vars."
-  (let [lvars (atom {})
-        prepped (if (lcons-expr? expr)
-                  (prep* expr lvars true)
-                  (postwalk (replace-lvar lvars) expr))]
-    (with-meta prepped {:lvars @lvars})))
-
-(defn unifier* [u w]
-  "Unify the terms u and w."
-  (first
-    (mk/run* [q]
-      (mk/== u w)
-      (mk/== u q))))
-
-(defn binding-map* [u w]
-  "Return the binding map that unifies terms u and w.
-  u and w should prepped terms."
-  (let [lvars (merge (-> u meta :lvars)
-                     (-> w meta :lvars))
-        s (mk/unify mk/empty-s u w)]
-    (when s
-      (into {} (map (fn [[k v]]
-                      [k (mk/reify s v)])
-                    lvars)))))
-
-(defn unifier [u w]
-  "Unify the terms u and w. Will prep the terms."
-  {:pre [(not (mk/lcons? u))
-         (not (mk/lcons? w))]}
-  (let [up (prep u)
-        wp (prep w)]
-    (unifier* up wp)))
-
-(defn binding-map [u w]
-  "Return the binding map that unifies terms u and w.
-  Will prep the terms."
-  {:pre [(not (mk/lcons? u))
-         (not (mk/lcons? w))]}
-  (let [up (prep u)
-        wp (prep w)]
-    (binding-map* up wp)))
\ No newline at end of file
diff --git a/src/test/clojure/clojure/core/logic/tests.clj b/src/test/clojure/clojure/core/logic/tests.clj
index 89a8c868..e5a0a81c 100644
--- a/src/test/clojure/clojure/core/logic/tests.clj
+++ b/src/test/clojure/clojure/core/logic/tests.clj
@@ -1,12 +1,6 @@
 (ns clojure.core.logic.tests
   (:refer-clojure :exclude [reify == inc intern])
-  (:use [clojure.core.logic.minikanren] :reload)
-  (:use [clojure.core.logic.prelude] :reload)
-  (:use [clojure.core.logic.match] :reload)
-  (:use [clojure.core.logic.nonrel :exclude [lvar]] :reload)
-  (:use [clojure.core.logic.disequality] :reload)
-  (:use [clojure.core.logic.tabled] :reload)
-  (:use [clojure.core.logic.unify] :reload)
+  (:use [clojure.core.logic] :reload)
   (:use clojure.test))
 
 ;; =============================================================================