 (declare delta-step)
 
 (defn delta-step-args [def-env ts local?]
-  (loop [ts ts, ts' []]
+  (loop [ts ts, ts' [], red? false]
     (if (seq ts)
-      (let [[t' red?] (delta-step def-env (first ts) local?)]
-        (if red?
-          [(vconcat (conj ts' t')
-                    (rest ts)) true]
-          (recur (rest ts) (conj ts' t'))))
-      [ts' false])))
+      (let [[t' red-1?] (delta-step def-env (first ts) local?)]
+        (recur (rest ts) (conj ts' t') (or red? red-1?)))
+      [ts' red?])))
 
 (defn delta-step
   ([def-env t] (delta-step def-env t false))

(declare special-step)

(defn special-step-args [def-env ctx ts]
  (loop [ts ts, ts' []]
    (if (seq ts)
      (let [[t' red?] (special-step def-env ctx (first ts))]
        (if red?
          [(vconcat (conj ts' t')
                    (rest ts)) true]
          (recur (rest ts) (conj ts' t'))))
      [ts' false])))

(defn special-step [def-env ctx t]
  ;; (println "[delta-step] t=" t)

    (stx/binder? t)
    (let [[binder [x ty] body] t]
      ;; 1) try reduction in binding type
      (let [[ty' red1?] (special-step def-env ctx ty)
            ;; 2) try reduction in body
            [body' red2?] (special-step def-env ctx body)]
        [(list binder [x ty'] body') (or red1? red2?)]))
    ;; application
    (stx/app? t)
    (let [[left right] t
          ;; 1) try left reduction
          [left' lred?] (special-step def-env ctx left)
          ;; 2) try right reduction
          [right' rred?] (special-step def-env ctx right)]
      [[left' right'] (or lred? rred?)])
    ;; reference
    (stx/ref? t)
    (let [[def-name & args] t
          [args' red1?] (special-step-args def-env ctx args)
          t' (if red1? (list* def-name args') t)
          [t'' red2?] (special-reduction def-env ctx t')]
      [t'' (or red1? red2?)])
    ;; other cases
    :else [t false]))

