 
   "
   [term & {:as env}]
-  (ev term env))
+  (ev term #{} env))
 
 (defn ?
   "funcall, the counit of product-exponential adjunction"
   ([& terms]
-   (as-> (ev (Beta. terms) {}) term
-     (if (beta? term)
-       (ev (Form. term (apply clojure.set/union (map fv terms))) {})
-       term)))
+   (let [terms (for [t terms] (if (var? t) (Form. t #{t}) t))
+         vars (apply clojure.set/union (map :vars (filter form? terms)))]
+     (ev (Beta. terms) vars {})))
   ([]))
 
 (defn %
   "forall"
   ([term & args] ; currently args can only be vars
-   (-> (Forall. term (vec args))
-       (ev {})
-       (Form. (reduce disj (if (form? term) (:vars term) #{}) args))
-       (ev {})))
+   (ev (Forall. term (vec args))
+       (reduce disj (if (form? term) (:vars term) #{}) args)
+       {}))
   ([term] term))
 
 (defn !

;; vars = set var
;; args = vec var

;; term = form | var | val
;; form = expr & vars
;; expr = beta | forall
;;
;; expr are always wrapped in form
;; vars only reduces during evaluation
;;
;; val    => val
;; var    => val | var
;; form   => form | var | val
;; beta   => form | beta | var | val
;; forall => forall

(defrecord Var    [name])         (defn var?    [x] (instance?  Var    x))
(defrecord Form   [expr vars])    (defn form?   [x] (instance?  Form   x))
(defrecord Beta   [sexp])         (defn beta?   [x] (instance?  Beta   x))
(defrecord Forall [term args])    (defn forall? [x] (instance?  Forall x))
(defprotocol Expr)                (defn expr?   [x] (satisfies? Expr   x))
(extend-protocol Expr Beta Forall)

(defprotocol Term
  "

  fv

  ev

  - substitutes all keys in expr to vals in env (: map var val)
  - beta reduces a term whose expr has a Forall as head

  "
  (fv [this])
  (ev [this env]))

(extend-protocol Term

  Var
  (fv [this] #{this})
  (ev [this env] (env this this))

  Form
  (fv [this] (:vars this))
  (ev [{:keys [expr vars]} env]
    (let [;; evaluates expr if necessary
          term (if (some vars (keys env)) (ev expr env) expr)
          vars (if (form? term) (:vars term) (reduce disj vars (keys env)))
          term (if (form? term) (:expr term) term)
          ;; now term is not a form
          term (if (and (beta? term) (empty? vars))
                 (as-> (:sexp term) [head & body]
                   (apply head body))
                 term)]
      (if (expr? term)
        (Form. term vars)
        term)))

  Beta
  (ev [this env]
    (as-> (:sexp this) [head & body :as sexp]
      ;; evalutes sexp if necessary
      (cond->> sexp (seq env) (map #(ev % env)))
      (if (and (form? head) (forall? (:expr head)))
        (let [{:keys [expr vars]} head
              {:keys [term args]} expr

  )

;; todo
;; - fix (keys env)
;; - test how to replace var using env
