 (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])
  )

;;{

;; ## Lambda terms
;;}

(defn kind? [t]
  (= t :kind))

(defn type? [t]
  (= t :type))

(defn sort? [t]
  (or (kind? t)
      (type? t)))

(defn var? [t]
  (symbol? t))

(defn binder? [t]
  (and (list? t)
       (contains? '#{lambda prod} (first t))))

(defn app? [t]
  (and (vector? t)
       (= (count t) 2)))

(defn ref? [t]
  (and (list? t)
       (not (contains? '#{lambda prod} (first t)))))

;;{
;; ## Free and bound variables
;;}

(defn free-vars [t]
  (cond
    (var? t) #{t}
    (binder? t) (let [[_ [x ty] body] t]
                  (clojure.set/union (free-vars ty)
                                     (disj (free-vars body) x)))
    (app? t) (clojure.set/union (free-vars (first t))
                                (free-vars (second t)))
    (ref? t) (apply clojure.set/union (map free-vars (rest t)))
    :else #{}))

(example
 (free-vars 'x) => #{'x})

(example
 (free-vars '[x y]) => #{'x 'y})

(example
 (free-vars '(lambda [x t] [x [y z]])) => #{'t 'y 'z})

(example
 (free-vars '(prod [x t] [x [y z]])) => #{'t 'y 'z})

(example
 (free-vars '(lambda [x t] (test x y z))) => '#{t y z})

(defn vars [t]
  (cond
    (var? t) #{t}
    (binder? t) (let [[_ [x ty] body] t]
                  (clojure.set/union (vars ty) (vars body)))
    (app? t) (clojure.set/union (vars (first t))
                                (vars (second t)))
    (ref? t) (apply clojure.set/union (map vars (rest t)))
    :else #{}))

(example
 (vars 'x) => #{'x})

(example
 (vars '[x y]) => #{'x 'y})

(example
 (vars '(lambda [x t] (test x [y z]))) => #{'t 'x 'y 'z})

(example
 (vars '(prod [x t] (test x [y z]))) => #{'t 'x 'y 'z})

(defn bound-vars [t]
  (clojure.set/difference (vars t) (free-vars t)))

(example
 (bound-vars 'x) => #{})

(example
 (bound-vars '[x y]) => #{})

(example
 (bound-vars '(lambda [x t] (test x [y z]))) => #{'x})

(example
 (bound-vars '(lambda [x t] (test t [y z]))) => #{})

(example
 (bound-vars '(prod [x t] (test x [y z]))) => #{'x})

;;{
;; ## Substitution
