 (example
  (mk-fresh 'x '#{x x' x''}) => 'x''')
 
-(s/def ::subst (s/map-of ::var ::term))
-
-(defn subst- [[tag t] sub forbid]
-  (case tag
-    :var [(get sub t t) forbid]
-    :bind (let [{binder :binder [x ty] :binding body :body} t
-                [x' sub' forbid']
-                (if (contains? forbid x)
-                  (let [x' (mk-fresh x forbid)]
-                    [x' (assoc sub x x') (conj forbid x')])
-                  [x sub forbid])
-                [ty' forbid''] (subst- ty sub forbid')
-                [body' forbid'''] (subst- body sub' forbid'')]
-            [(list binder [x' ty'] body')
-             forbid'''])
-    :app (let [[rator forbid'] (subst- (:rator t) sub forbid)
-               [rand forbid''] (subst- (:rand t) sub forbid')]
-           [(list rator rand) forbid''])
-    [t forbid]))
-
-(defn subst
-  ([t sub] (let [t (validate ::term t)]
-             (first (subst- t sub (free-vars- t)))))
-  ([t k v & kvs] (subst t (apply hash-map (cons k (cons v kvs)))))) 
+(defn subst-
+  ([t sub] (subst- t sub #{}))
+  ([t sub forbid]
+   (cond
+     (var? t) [(get sub t t) (conj forbid t)]
+     (binder? t) (let [[binder [x ty] body] t
+                       [x' sub' forbid']
+                       (if (contains? forbid x)
+                         (let [x' (mk-fresh x forbid)]
+                           [x' (assoc sub x x') (conj forbid x')])
+                         [x (dissoc sub x) forbid])
+                       [ty' forbid''] (subst- ty sub forbid')
+                       [body' forbid'''] (subst- body sub' forbid'')]
+                   ;; (println "term=" (list binder [x' ty'] body') "sub=" sub')
+                   [(list binder [x' ty'] body')
+                    forbid'''])
+     (app? t) (let [[rator forbid'] (subst- (first t) sub forbid)
+                    [rand forbid''] (subst- (second t) sub forbid')]
+                [[rator rand] forbid''])
+     (ref? t) (let [[args forbid'] (reduce (fn [[ts forbid] t]
+                                             (let [[t' forbid'] (subst- t sub forbid)]
+                                               [(conj ts t') forbid'])) ['() forbid] (rest t))]
+                [(conj (into '() args) (first t)) forbid'])
+     :else [t forbid])))
+
+(defn subst [t sub]
+  (let [[t' _] (subst- t sub #{})]
+    t'))
 
 (example
  (subst 'x {'x :type}) => :type)


(ns typetheory.syntax
  (:require [clj-by.example :refer [example do-for-example]])
  (:require [clojure.spec :as s])
  (:require [clojure.test.check :as tc])
  (:require [clojure.test.check.generators :as gen])
  (:require [clojure.test.check.properties :as prop])
  )

;;{

 (subst 'y {'x :type}) => 'y)

(example
 (subst '[y x] {'x :type}) => '[y :type])

(example
 (subst '[x (lambda [x :type] (test x y z))] {'x :type, 'y :kind})
 => '[:type (lambda [x' :type] (test x' :kind z))])
q
(example
 (subst '[x (prod [x :type] [y x])] {'x :type, 'y 'x})
 => '[:type (prod [x' :type] [x x'])])
;; and not: '(:type (prod [x :type] (x x)))


