Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

file 162 lines (139 sloc) 4.792 kb
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
(ns clojure.core.logic.unifier
  (:refer-clojure :exclude [==])
  (:use [clojure.core.logic.protocols]
        [clojure.core.logic :exclude [unify] :as l]))

;; =============================================================================
;; 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 false))]
    (swap! store assoc 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
               (lcons (prep* f store) tail)))
           (walk-term expr (replace-lvar store)))
         
        :else expr))))

(defn prep
  "Prep a quoted expression. All symbols preceded by ? will
be replaced with logic vars."
  [expr]
  (let [lvars (atom {})
        prepped (cond
                  (lvarq-sym? expr) (proc-lvar expr lvars)

                  (lcons-expr? expr)
                  (prep* expr lvars true)

                  :else (walk-term expr (replace-lvar lvars)))]
    (if (instance? clojure.lang.IMeta prepped)
      (with-meta prepped {::lvars (keys @lvars)})
      prepped)))

(defn queue-constraint [s c vs]
  (cond
    (vector? vs)
    (queue s (-unwrap (apply c (map #(lvar % false) vs))))

    (set? vs)
    (reduce (fn [s v] (queue s (-unwrap (c (lvar v false))))) s vs)

    (symbol? vs)
    (queue s (-unwrap (apply c (map #(lvar % false) (list vs)))))

    :else
    (throw
     (Exception.
      (str "Only symbol, set of symbols, or vector of symbols allowed "
           "on left hand side")))))

(defn queue-constraints [s [vs cs]]
  (let [cs (if-not (sequential? cs) [cs] cs)]
    (reduce (fn [s c] (queue-constraint s c vs)) s cs)))

(defn -unify* [init-s u w]
  (first
    (take*
      (fn []
        ((fresh [q]
           (== u w) (== q u)
           (fn [a]
             (fix-constraints a))
           (reifyg q))
         init-s)))))

(defn init-s [opts s]
  (let [s (reduce (fn [s [k v]] ((== k v) s)) s (:as opts))]
    (reduce queue-constraints
      (with-meta s {:reify-vars (fn [v rs] rs)})
      (:when opts))))

(defn unify*
  "Unify the terms ts."
  ([ts] (unify* {} ts))
  ([opts ts]
     (let [init-s (init-s opts empty-s)]
       (-unify*
         (vary-meta init-s assoc :reify-vars false)
         (reduce #(-unify* init-s %1 %2) (butlast ts))
         (last ts)))))

(defn unifier*
  "Return the unifier that unifies terms ts.
All terms in ts should prepped terms."
  ([ts] (unifier* {} ts))
  ([opts ts]
     (letfn [(-unifier* [s u w]
               (let [s (fix-constraints (l/unify (with-meta s {:reify-vars false}) u w))]
                 (when s
                   (->> (:lvars opts)
                     (map (fn [sym] [sym (lvar sym false)]))
                     (filter (fn [[sym var]] (not= (walk s var) var)))
                     (map (fn [[sym var]] [sym (-reify s var)]))
                     (into {})))))]
       (let [init-s (init-s opts empty-s)]
         (reduce #(-unifier* init-s %1 %2) ts)))))

(defn unify
  "Unify the terms ts returning a the value that represents their
unificaiton. Will prep the terms."
  ([ts] (unify {} ts))
  ([opts ts]
     (let [opts (if (contains? opts :as)
                  (assoc opts :as
                    (->> (:as opts)
                      (map (fn [[k v]] [(lvar k false) (prep v)]))
                      (into {})))
                  opts)]
       (unify* opts (map prep ts)))))

(defn unifier
  "Return the unifier for terms ts. Will prep the terms."
  ([ts] (unifier {} ts))
  ([opts ts]
     (let [opts (if (contains? opts :as)
                  (assoc opts :as
                    (->> (:as opts)
                      (map (fn [[k v]] [(lvar k false) (prep v)]))
                      (into {})))
                  opts)
           ts' (map prep ts)
           lvars (->> (concat ts' (map val (:as opts)))
                   (map #(-> % meta ::lvars))
                   (reduce into))]
       (unifier* (assoc opts :lvars lvars) (map prep ts)))))
Something went wrong with that request. Please try again.