-
Notifications
You must be signed in to change notification settings - Fork 11
/
unify.cljc
141 lines (122 loc) · 4.67 KB
/
unify.cljc
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
;; Adapted from `https://github.com/clojure/core.unify` which was not cljs
;; compatible out of the box.
(ns hyperfiddle.rcf.unify
(:require [clojure.walk :as walk]
[clojure.set :as set]))
(defn wildcard? [x] (= '_ x))
(defn &? [form] (and (seqable? form) (= '& (first form))))
(defn lvar? [x] (and (symbol? x) (= \? (first (name x)))))
(defn failed? [env] (contains? env ::fail))
(defn unify-in-env [x y env]
(if (contains? env x)
(let [y' (get env x)]
(if (= y y')
env
(if (lvar? y')
(unify-in-env y' y env)
(assoc env ::fail {x [y' y]}))))
(assoc env x y)))
(defn wildcard-in-env [v env]
(if (contains? env '_)
(update-in env ['_] conj v)
(assoc env '_ [v])))
(defn resolve*
([env k]
(resolve* [] env k))
([path env k]
(if (= k (first path))
::cycle
(let [v (get env k)]
(if (lvar? v)
(resolve* (conj path k) env v)
v)))))
(defn ground [env]
(if (map? env)
(let [env (reduce-kv (fn [env k _v] (assoc env k (resolve* env k))) env env)]
(if (contains? env '_)
(update env '_ (fn [xs] (mapv (fn [x] (if (lvar? x) (get env x) x)) xs)))
env))
env))
(declare unify)
(defn unify-set [xs ys env]
(if (seq (set/intersection xs ys))
(unify-set (set/difference xs ys) (set/difference ys xs) env)
(let [env (unify (first xs) (first ys) env)]
(if (failed? env)
env
(unify (rest xs) (rest ys) env)))))
(defn replace-keys [m ks-map]
(reduce-kv (fn [r k v]
(-> (dissoc r k)
(assoc (if (= k '_)
(or (first (set/difference (set (get ks-map '_)) (set (keys r))))
'_)
(get ks-map k k))
v)))
m m))
(defn unify-map [xs ys env]
(let [env (unify-set (set (keys xs)) (set (keys ys)) env)
xs (replace-keys xs env)
ys (replace-keys ys env)]
(if (= xs ys)
env
(reduce (fn [env k]
(let [env (unify (find xs k) (find ys k) env)]
(if (failed? env)
(reduced env)
env)))
env (set/union (set (keys xs)) (set (keys ys)))))))
;; Javascript do not have chars. So iterating a string always produce more strings -> StackOverflow.
(defn collection? [x] (and (seqable? x) (not (string? x))))
(defn unify
([x y] (unify x y {}))
([x y env]
(let [env (cond
(failed? env) env
(wildcard? x) (wildcard-in-env y env)
(wildcard? y) (wildcard-in-env x env)
(= x y) env
(&? x) (if (seq y)
(unify (second x) (seq y) env)
env)
(&? y) (if (seq x)
(unify (second y) (seq x) env)
env)
(lvar? x) (unify-in-env x y env)
(lvar? y) (unify-in-env y x env)
(and (set? x) (set y)) (unify-set x y env)
(and (map? x) (map? y)) (unify-map x y env)
(every? collection? [x y]) (let [env (unify (first x) (first y) env)]
(if (failed? env)
env
(unify (rest x) (rest y) env)))
:else (assoc env ::fail {::root [x y]}))]
(if (failed? env)
(update env ::path (fnil conj ()) x)
env))))
(defn subst [form env]
(let [idx (volatile! -1)
get-idx! (fn [] (vswap! idx inc))]
(if (map? env)
(walk/prewalk (fn [expr] (cond
(lvar? expr) (get env expr expr)
(wildcard? expr) (get-in env ['_ (get-idx!)] '_)
:else expr))
form)
form)))
(defn unifier* [x y]
(let [env (unify x y)]
(if (failed? env)
[::fail env]
(let [env (ground env)]
[(subst y env) env]))))
(def unifier (comp first unifier*))
(defn explain [env]
(when-let [fail (::fail env)]
(str "Failed to unify "
(if-some [[a b] (::root fail)]
(str (pr-str a) " and " (pr-str b))
(let [[lvar [a b]] (first fail)]
(str (pr-str lvar) " with " (pr-str a) " and " (pr-str b))))
(when-some [path (seq (->> (::path env) (filter map-entry?) (map key)))]
(str " in " (into [] path))))))