Skip to content
Browse files

prototype of speed

  • Loading branch information...
1 parent f0ce96e commit 7ddee45594e566fc11d9813fb7db82d1db3fad96 @fogus fogus committed Aug 8, 2012
Showing with 1,014 additions and 0 deletions.
  1. +1,006 −0 src/main/clojure/clojure/core/unify/core.clj
  2. +8 −0 src/test/clojure/clojure/core/unify/core_tests.clj
View
1,006 src/main/clojure/clojure/core/unify/core.clj
@@ -0,0 +1,1006 @@
+(ns clojure.core.unify.core
+ (:use [clojure.walk :only [postwalk]])
+ (:import [java.io Writer]))
+
+(def ^{:dynamic true} *occurs-check* true)
+(def ^{:dynamic true} *reify-vars* 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.))
+
+(defprotocol ILVar
+ (constraints [this])
+ (add-constraint [this c])
+ (add-constraints [this ds])
+ (remove-constraint [this c])
+ (remove-constraints [this]))
+
+;; =============================================================================
+;; 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 choice)
+(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)))))
+ (toString [_]
+ (prn-str [s l verify cs]))
+
+ 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
+
+(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]
+ (if *reify-vars*
+ (ext s v (reify-lvar-name s))
+ (ext s v (:name meta))))
+ 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 {:name name})))
+ ([name]
+ (let [oname name
+ name (str name "_" (. clojure.lang.RT (nextID)))]
+ (LVar. name (.hashCode name) nil {:name oname})))
+ ([name cs]
+ (let [oname name
+ name (str name "_" (. clojure.lang.RT (nextID)))]
+ (LVar. name (.hashCode name) cs {:name oname}))))
+
+(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)
+ 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
+ "Constructs a sequence a with an improper tail d if d is a logic variable."
+ [a d]
+ (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))
+
+;; -----------------------------------------------------------------------------
+;; 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)))
+
+;; -----------------------------------------------------------------------------
+;; 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)))
+
+;; -----------------------------------------------------------------------------
+;; 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)))))
+
+;; -----------------------------------------------------------------------------
+;; 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.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.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))))))
+
+;; -----------------------------------------------------------------------------
+;; 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))
+
+;; 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]
+ (with-meta
+ (map #(walk* s %) v)
+ (meta v))))
+
+(extend-protocol IWalkTerm
+ clojure.lang.IPersistentVector
+ (walk-term [v s]
+ (with-meta
+ (loop [v v r (transient [])]
+ (if (seq v)
+ (recur (next v) (conj! r (walk* s (first v))))
+ (persistent! r)))
+ (meta v))))
+
+(extend-protocol IWalkTerm
+ clojure.lang.IPersistentMap
+ (walk-term [v s]
+ (with-meta
+ (loop [v v r (transient {})]
+ (if (seq v)
+ (let [[vfk vfv] (first v)]
+ (recur (next v) (assoc! r vfk (walk* s vfv))))
+ (persistent! r)))
+ (meta v))))
+
+(extend-protocol IWalkTerm
+ clojure.lang.IPersistentSet
+ (walk-term [v s]
+ (with-meta
+ (loop [v v r #{}]
+ (if (seq v)
+ (recur (next v) (conj r (walk* s (first v))))
+ r))
+ (meta v))))
+
+;; =============================================================================
+;; 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)))))
+
+
+;; =============================================================================
+;; Easy Unification
+
+(defn- lvarq-sym? [s]
+ (and (symbol? s) (= (first (str s)) \?)))
+
+(defn- proc-lvar [lvar-expr store]
+ (let [v (if-let [u (@store lvar-expr)]
+ u
+ (lvar 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))))
+
+(defmacro --unify--
+ "A goal that attempts to unify terms u and v."
+ [u v]
+ `(fn [a#]
+ (if-let [b# (unify a# ~u ~v)]
+ b# nil)))
+
+(defn- lvar-bind [sym]
+ ((juxt identity
+ (fn [s] `(lvar '~s))) sym))
+
+(defn- lvar-binds [syms]
+ (mapcat lvar-bind syms))
+
+(defmacro fresh
+ "Creates fresh variables. Goals occuring within form a logical
+ conjunction."
+ [[& lvars] & goals]
+ `(fn [a#]
+ (-inc
+ (let [~@(lvar-binds lvars)]
+ (bind* a# ~@goals)))))
+
+(defmacro solve [& [n [x :as bindings] & goals]]
+ (if (> (count bindings) 1)
+ `(solve ~n [q#] (fresh ~bindings ~@goals (== q# ~bindings)))
+ `(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
+ "Executes goals until a maximum of n results are found."
+ [n & goals]
+ `(doall (solve ~n ~@goals)))
+
+(defmacro run*
+ "Executes goals until results are exhausted."
+ [& goals]
+ `(run false ~@goals))
+
+(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
+ (lcons (prep* f store) tail)))
+ (postwalk (replace-lvar store) expr))
+ :else expr))))
+
+(defn prep
+ "Prep a quoted expression. All symbols preceded by ? will
+ be replaced with logic vars."
+ [expr]
+ (let [lvars (atom {})
+ prepped (if (lcons-expr? expr)
+ (prep* expr lvars true)
+ (postwalk (replace-lvar lvars) expr))]
+ (with-meta prepped {:lvars @lvars})))
+
+(defn unifier*
+ "Unify the terms u and w."
+ ([u w]
+ (first
+ (run* [q]
+ (--unify-- u w)
+ (--unify-- u q))))
+ ([u w & ts]
+ (apply unifier* (unifier* u w) ts)))
+
+(defn binding-map*
+ "Return the binding map that unifies terms u and w.
+ u and w should prepped terms."
+ ([u w]
+ (let [lvars (merge (-> u meta :lvars)
+ (-> w meta :lvars))
+ s (unify empty-s u w)]
+ (when s
+ (into {} (map (fn [[k v]]
+ [k (-reify s v)])
+ lvars)))))
+ ([u w & ts]
+ (apply binding-map* (binding-map* u w) ts)))
+
+(defn unifier
+ "Unify the terms u and w. Will prep the terms."
+ ([u w]
+ {:pre [(not (lcons? u))
+ (not (lcons? w))]}
+ (let [up (prep u)
+ wp (prep w)]
+ (unifier* up wp)))
+ ([u w & ts]
+ (apply unifier (unifier u w) ts)))
+
+(defn binding-map
+ "Return the binding map that unifies terms u and w.
+ Will prep the terms."
+ ([u w]
+ {:pre [(not (lcons? u))
+ (not (lcons? w))]}
+ (let [up (prep u)
+ wp (prep w)]
+ (binding-map* up wp)))
+ ([u w & ts]
+ (apply binding-map (binding-map u w) ts)))
+
+
+(comment
+
+ (binding-map '(1 2 3) '(1 2 ?x))
+ (binding-map [1 2 3] [1 2 '?x])
+ (unifier [1 2 3] [1 2 '?x])
+ (prep '[1 2 ?x])
+
+
+ (def tmpl "http://foo.com/foo/?a/?b")
+
+ (def T (map symbol (-> tmpl
+ (.replace "http://foo.com/foo/" "")
+ (.split "/"))))
+
+
+ (defn match [req]
+ (-> req
+ :url
+ (.replace "http://foo.com/foo/" "")
+ (.split "/")
+ seq
+ (binding-map T)))
+
+ (match {:url "http://foo.com/foo/1/2"})
+ ;=> {?a 1, ?b 2}
+
+ (match {:url "http://foo.com/foo/1/fred"})
+
+ (unifier T [1 2])
+
+ )
View
8 src/test/clojure/clojure/core/unify/core_tests.clj
@@ -0,0 +1,8 @@
+(ns ^{:doc "A unification library for Clojure."
+ :author "Michael Fogus"}
+ clojure.core.unify.core
+ (:use [clojure.core.unify.core] :reload-all)
+ (:use [clojure.test]))
+
+(deftest test-unify
+ (is (= 1 1)))

0 comments on commit 7ddee45

Please sign in to comment.
Something went wrong with that request. Please try again.