 ;; form = expr | term
 ;; term = expr & vars
 ;; vars = set var
+;; args = vec var
 
 (defrecord Term   [expr vars])
 (defrecord Forall [expr args])
+
+(defn term?   [x] (instance? Term   x))
+(defn forall? [x] (instance? Forall x))
 
 (defn forms->term
   "merges multiple forms into a single term"
   [forms]
   (loop [forms (seq forms)  expr []  vars #{}]
     (if-let [[form & forms] forms]
-      (if (instance? Term form) ; build expr & collect vars
+      (if (term? form)
         (recur forms (conj expr (:expr form)) (into vars (:vars form)))
         (recur forms (conj expr        form)        vars))
       (Term. (seq expr) vars))))

(defn subst
  "substitutes all keys in expr to vals in env"
  [env expr]
  (cond ; todo use a better data structure (lens?) for this
    (seq? expr)             (map (partial subst env) expr)
    (instance? Forall expr) (assoc expr :expr (subst (reduce dissoc env (:args expr)) (:expr expr)))
    :else                   (env expr expr)))

(defn beta
  "beta-reduces a term whose expr has a Forall as head"
  [{[{:keys [expr args]} & vals] :expr vars :vars}]
  (loop [rgs (seq args)  als (seq vals)  env {}]
    (match [rgs als]
           [nil nil] (Term. (subst env expr) (reduce disj vars (keys env)))
           [_   nil] (Term. (Forall. (subst env expr) rgs) (reduce disj vars (keys env)))
           [nil   _] (throw (ex-info "arity error" {:args args :vals vals}))
           :else (let [[a & rgs] rgs
                       [v & als] als]
                   (recur rgs als (assoc env a v))))))

(defn ?
  "funcall, the counit of product-exponential adjunction"
  ([& forms]
   (as-> (forms->term forms) {:keys [expr vars] :as term}
     (cond-> term (instance? Forall (first expr)) beta)
     (if (seq vars) term (eval expr))))
  ([]))

(defn %
  "forall"
  [form & args] ; currently args can only be var terms
  (let [term (if (instance? Term form) form (Term. form #{}))
        expr (:expr term)
        args (map :expr args)]
    (Term.
     (if (instance? Forall expr)
       (Forall. (:expr expr) (concat args (:args expr)))
       (Forall.        expr          args))
     (reduce disj (:vars term) args))))

(defn !


  )

(comment ; todo goal 1

  ;; let
  ;; - A B C be types
