Created

Embed URL

HTTPS clone URL

SSH clone URL

You can clone with HTTPS or SSH.

Download Gist

Peter Norvig's unifier in Clojure, take 2

View gist:374764
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
(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 defalias)]
[core :only (seqable?)]])
(:require [clojure
[walk :as walk]
[zip :as zip]]))
 
(defn variable?
"Is x a variable (a symbol beginning with '?')?"
[x]
(and (symbol? x) (= (first (name x)) \?)))
 
(defalias compound? seqable?)
 
(defvar *occurs-check* true "Perform the occurs check?")
 
(declare unify-variable occurs?)
 
(defn unify
"Attempt to unify x and y with the given bindings (if any)."
([x y] (unify x y {}))
([x y bs]
(cond
(not bs) nil
(= 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)))
 
(defmacro cond-let
[& clauses]
(when clauses
`(~(if (vector? (first clauses))
'if-let
'if)
~(first clauses)
~(if (next clauses)
(second clauses)
(throw (IllegalArgumentException.
"cond-let requires an even number of forms")))
(cond-let ~@(nnext clauses)))))
 
(defn unify-variable
"Unify the variable v with x."
[v x bs]
(cond-let
[vb (bs v)] (unify vb x bs)
[vx (and (variable? x) (bs x))] (unify v vx bs)
(and *occurs-check* (occurs? v x bs)) nil
:else (assoc bs v x)))
 
(defn resolve-steps
[v bs]
(loop [v v steps [v]]
(if-let [vv (bs v)]
(if (variable? vv)
(recur vv (conj steps vv))
(conj steps vv))
(conj steps (bs v)))))
 
(defn resolve-variable
"Resolve v to its value in bs (nil if none)."
[v bs]
(loop [v v]
(if-let [vv (bs v)]
(if (variable? vv)
(recur vv)
vv))))
 
(defn resolve-variable*
"Resolve v to its value in bs (last var in the chain if none)."
[v bs]
(loop [v v]
(if-let [vv (bs v)]
(if (and (variable? vv)
(find bs vv))
(recur vv)
vv))))
 
(defn resolves-to?
"Does v resolve to x with the given bindings?"
[v x bs]
(let [vv (resolve-variable v bs)]
(= vv x)))
 
#_
(defn occurs?
"Does v occur anywhere inside x?"
([v x bs] (occurs? v x bs []))
([v x bs to-do]
(cond
(= v x) true
(and (variable? x) (find bs x)) (recur v (bs x) bs to-do)
(compound? x) (recur v (first x) bs (conj to-do (rest x)))
(empty? to-do) false
:else (recur v (peek to-do) bs (pop to-do)))))
 
(defn compound-zip
[root]
(zip/zipper seqable? seq (fn [_ cs] cs) root))
 
(defn occurs?
"Does v occur anywhere inside x?"
[v x bs]
(loop [z (compound-zip [x])]
(let [current (zip/node z)]
(cond (zip/end? z) false
(= v current) true
(and (variable? current)
(find bs current))
(recur (zip/next (zip/insert-right z (bs current))))
(zip/end? z) false
:else (recur (zip/next z))))))
 
(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)]
(walk/prewalk #(if (variable? %) (bs %) %) x)))
 
(defn subst*
[x bs]
(walk/prewalk #(if (variable? %) (resolve-variable % bs) %) x))
 
(defn subst-memo
[x bs]
(let [memo (atom {})]
(walk/prewalk
(fn [item]
(if (variable? item)
(cond (find @memo item) (@memo item)
(find bs item) (let [v (resolve-variable* item bs)]
(swap! memo assoc item v)
v)
:else item)
item))
x)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.