Peter Norvig's unifier in Clojure

unifier.clj

(ns
  #^{:doc "CL original by Peter Norvig, initial version in Clojure by Kevin Livingston. See http://groups.google.com/group/clojure/browse_thread/thread/996ecadf98328c6b#"}
  unifier.core
  (:use [clojure.contrib.def :only (defvar)]))

(defn variable?
  "Is x a variable (a symbol beginning with '?')?"
  [x]
  (and (symbol? x) (= (first (name x)) \?)))

(defn compound?
  "Is x a compound form (a non-empty seq)?"
  [x]
  (and (seq? x) (seq x)))

(defvar *occurs-check* true "Perform the occurs check?")

(declare unify-variable occurs-check)

(defn unify
  "Attempt to unify x and y with the given bindings (if any)."
  ([x y] (unify x y {}))
  ([x y bs]
     (when bs
       (cond
        (= x y)       bs
        (variable? x) (unify-variable x y bs)
        (variable? y) (unify-variable y x bs)
        (every? compound? [x y])
        (unify (rest x) (rest y)
               (unify (first x) (first y) bs))
        :else nil))))

(defn unify-variable
  "Unify the variable v with x."
  [v x bs]
  (if-let [vb (bs v)]
    (unify vb x bs)
    (if-let [vx (and (variable? x) (bs x))]
      (unify v vx bs)
      (if (and *occurs-check* (occurs-check v x bs))
        nil
        (assoc bs v x)))))

(defn occurs-check
  "Does v occur anywhere inside x?"
  [v x bs]
  (some identity
        [(= v x)
         (and (variable? x)
              (if-let [vx (bs x)]
                (= v vx)))
         (and (compound? x)
              (or (occurs-check v (first x) bs)
                  (occurs-check v (rest x) bs)))]))

(defn simplify-bindings
  [bs]
  (into {} (map (fn [[k v]]
                  [k (loop [v v]
                       (if (variable? v)
                         (recur (bs v))
                         v))])
                bs)))

(defn subst
  [x bs]
  (let [bs (simplify-bindings bs)]
    (map #(cond (variable? %) (bs %)
                (compound? %) (subst % bs)
                :else         %)
         x)))