(ns nal.deriver.substitution
(:require [nal.deriver.utils :refer [walk]]
[clojure.core.unify :as u]
[clojure.string :as s])) | |
Defn replaces var-elements from statemts by placeholders for unification. | (defn replace-vars
[var-type statement]
(walk statement
(and (coll? :el) (= var-type (first :el)))
(->> :el second (str "?") symbol))) |
Returns map of inified elements from both collections. | (defn unification-map
[var-symbol p2 p3]
(let [var-type (if (= var-symbol "$")
'ind-var
'dep-var)]
((u/make-occurs-unify-fn #(and (coll? %) (= var-type (first %)))) p2 p3))) |
(def munification-map (memoize unification-map)) | |
(defn placeholder->symbol [pl] (->> pl str (drop 1) s/join symbol)) | |
Updates keys in unification map from placeholders like ?X to vectors like ['dep-var X] | (defn replace-placeholders
[var-type u-map]
(->> u-map
(map (fn [[k v]] [[var-type (placeholder->symbol k)] v]))
(into {}))) |
Unifies p2 and p3, then replaces elements from the unification map inside the conclusion. | (defn substitute
[var-symbol p2 p3 conclusion]
(let [u-map (munification-map var-symbol p2 p3)]
(walk conclusion (u-map el) (u-map el)))) |