 
 (extend-type ProductVar
   Unparser
-  (unparse [e] (:name e)))
+  (unparse [e] (:name e))
+  FreeVars
+  (free-vars [e kind] (if (= kind :forall)
+                        #{(:name e)}
+                        #{})))
 
 (example (unparse (mk-product-var 'my-var)) => 'my-var)
 
 (example (unparse (parse '(forall [x (univ 0)] x)))
          => '(forall [x (univ 0)] x))
+
+
+(example (free-vars (:body (parse '(forall [x (univ 0)] x))) :forall)
+         => #{'x})
+
+(example (free-vars (:body (parse '(forall [x (univ 0)] x))) :lambda)
+         => #{})
+
+;;{
+
+;; #### Open variables
+
+;; Open variables are open to substitution and/or binding
+;; in some external environment.
+
+;;}
+
+(defrecord OpenVar [name])
+
+(defn mk-open-var
+  "Make the `name` variable free and open ."
+  [name]
+  (->OpenVar name))
+
+(example (:name (mk-open-var 'my-var))
+         => 'my-var)
+
+(defn- match-open-var?
+  [expr env]
+  (match-free-var? expr env))
+
+(parser/register-term-other-parser
+ match-open-var?
+ (fn [expr env]
+   (mk-open-var expr)))
+
+(example (parse 'my-var (list))
+         => (mk-open-var 'my-var))
+
+(example (= (parse '(forall [x (univ 0)] (x y)))
+            (mk-product 'x (mk-univ 0) (mk-application
+                                        (mk-product-var 'x)
+                                        (mk-open-var 'y))))
+         => true)
+         
+(extend-type OpenVar
+  Unparser
+  (unparse [e] (:name e))
+  FreeVars
+  (free-vars [e kind] (if (= kind :open)
+                        #{(:name e)}
+                        #{})))
+
+(example (unparse (mk-open-var 'my-var)) => 'my-var)
+
+(example (unparse (parse '(forall [x (univ 0)] y)))
+         => '(forall [x (univ 0)] y))
+
+
+(example (free-vars (parse '(forall [x (univ 0)] (x y))) :open)
+         => #{'y})
+
+(example (free-vars (:body (parse '(forall [x (univ 0)] (x y)))) :lambda)
+         => #{})
+

(example (unparse (parse '(((univ 1) (univ 2)) ((univ 3) (univ 4)))))
         => '((univ 1) (univ 2) (univ 3) (univ 4)))


;;{


    [expr]
    "Produce a `parsable` clojure expression from `expr`
 in optional lexical environement `env`."))


(defprotocol FreeVars
  "A protocol for fetching the set of free variables."
  (free-vars
   [expr kind]
   "Return a set of the free variables of `expr` according 
to their kind: :product, :forall or :open."))

;;{
;;
;; ## Lambda-terms
