diff --git a/.gitignore b/.gitignore
index a9fe6fb..68d7462 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,13 +1,12 @@
+/target
+/classes
+/checkouts
+/web
pom.xml
pom.xml.asc
*.jar
*.class
-/lib/
-/classes/
-/target/
-/checkouts/
-.lein-deps-sum
-.lein-repl-history
-.lein-plugins/
-.lein-failures
-.nrepl-port
+/.lein-*
+/.nrepl-port
+.hgignore
+.hg/
diff --git a/.travis.yml b/.travis.yml
new file mode 100644
index 0000000..4f42080
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1 @@
+language: clojure
\ No newline at end of file
diff --git a/README.md b/README.md
index 48e06f3..ab52462 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,15 @@
# psiml
-a prototype language with subtyping polymorphism and type inference
+
+*Polymorphic, Subtyped and type Infered ML* is a prototype language inspired by Stephen Dolans' [MLsub](http://www.cl.cam.ac.uk/~sd601/mlsub/).
+
+## Usage
+
+```sh
+# On the JVM
+lein run
+lein repl
+lein test
+# On your browser
+lein cljsbuild once
+firefox index.html
+```
\ No newline at end of file
diff --git a/doc/intro.md b/doc/intro.md
new file mode 100644
index 0000000..054539c
--- /dev/null
+++ b/doc/intro.md
@@ -0,0 +1,3 @@
+# Introduction to psiml
+
+TODO: write [great documentation](http://jacobian.org/writing/what-to-write/)
diff --git a/index.html b/index.html
new file mode 100644
index 0000000..dda5c61
--- /dev/null
+++ b/index.html
@@ -0,0 +1,9 @@
+
+
+
+
+
+
diff --git a/project.clj b/project.clj
new file mode 100644
index 0000000..3d63d11
--- /dev/null
+++ b/project.clj
@@ -0,0 +1,18 @@
+(defproject psiml "0.1.0-SNAPSHOT"
+ :description "Polymorphic, Subtyped and type Infered ML"
+ :dependencies [[org.clojure/clojure "1.9.0"]
+ [org.clojure/core.match "0.3.0-alpha5"]
+ [org.clojure/clojurescript "1.9.946"
+ :exclusions [org.apache.ant/ant]]]
+ :plugins [[lein-cljsbuild "1.1.7"
+ :exclusions [[org.clojure/clojure]]]]
+ :cljsbuild {:builds [{:source-paths ["src"]
+ :compiler {:main psiml.core
+ :output-to "web/main.js"
+ :output-dir "web/"
+ :source-map "web/main.js.map"
+ :optimizations :whitespace
+ :pretty-print true}}]}
+ :main ^:skip-aot psiml.core
+ :target-path "target/%s"
+ :profiles {:uberjar {:aot :all}})
diff --git a/src/psiml/core.cljc b/src/psiml/core.cljc
new file mode 100644
index 0000000..931f6a7
--- /dev/null
+++ b/src/psiml/core.cljc
@@ -0,0 +1,32 @@
+(ns psiml.core
+ (:require [psiml.type :as t]
+ [psiml.parse :as p]
+ [clojure.core.match :refer [match]]))
+
+#?(:cljs (enable-console-print!))
+
+(defn eval-expr
+ "Evaluates an expression"
+ ([expr] (eval-expr expr {}))
+ ([expr env]
+ (match expr
+ [:abs n e] [:abs n (eval-expr e env)]
+ [:rec n e] [:rec n (eval-expr e (conj env [n e]))]
+ [:lit c] [:cst c]
+ [:var n] (or (env n) [:var n])
+ [:app e1 e2] (let [e2' (eval-expr e2 env)]
+ (or (match e1 [:abs n e1'] (eval-expr e1' (conj env [n e2'])))
+ [:app (eval-expr e1 env) e2']))
+ [:struct m] [:struct (reduce (fn [m' [l e]] (assoc m' l (eval-expr e env))) {} m)]
+ [:get l e] (let [e' (eval-expr e env)]
+ (or (match e' [:struct m] (m l))
+ [:get l e']))
+ expr)))
+
+(defn -main
+ "I don't do a whole lot ... yet."
+ [& args]
+ (let [e (p/string "(fn [n1 n2] true)")]
+ (println e)))
+
+#?(:cljs (-main))
diff --git a/src/psiml/parse.cljc b/src/psiml/parse.cljc
new file mode 100644
index 0000000..5aa58d1
--- /dev/null
+++ b/src/psiml/parse.cljc
@@ -0,0 +1,44 @@
+(ns psiml.parse
+ "Parses concrete syntax, producing abstract syntax
+ e := 1 --> [:lit 1]
+ | true --> [:lit true]
+ | (fn [a b] e) --> [:abs :a [:abs :b e']]
+ | (e1 e2 e3) --> [:app [:app e1' e2'] e3']
+ | {:l1 e1 :l2 e2} --> [:struct {:l1 e1' :l2 e2'}]
+ | (:l s) --> [:get :l s']
+ | (let [n e1] e2) --> [:app [:abs n e2'] e1']"
+ (:refer-clojure :exclude [read-string])
+ (:require [clojure.core.match :refer [match]]
+ [#?(:clj clojure.edn
+ :cljs cljs.reader) :refer [read-string]]))
+
+(defn data
+ "Parses concrete syntax from data"
+ [d]
+ (cond
+ (seq? d)
+ (match d
+ (['fn [a] b] :seq)
+ (if (symbol? a) [:abs (keyword a) (data b)])
+ (['fn [a & args] b] :seq)
+ (data (list 'fn [a] (list 'fn args b)))
+ (['let [n e] b] :seq)
+ (if (symbol? n) [:app [:abs (keyword n) (data b)] (data e)])
+ (['let [n e & r] b] :seq)
+ (data (list 'let [n e] (list 'let r b)))
+ ([a b] :seq)
+ (if (keyword? a) [:get a (data b)]
+ [:app (data a) (data b)])
+ ([a b & r] :seq)
+ (data (cons (list a b) r)))
+ (symbol? d)
+ [:var (keyword d)]
+ (or (integer? d) (true? d) (false? d))
+ [:lit d]
+ (map? d)
+ [:struct (reduce (fn [m [l v]] (assoc m l (data v))) {} d)]))
+
+(defn string
+ "Parses concrete syntax from a string"
+ [s]
+ (data (read-string s)))
diff --git a/src/psiml/print.cljc b/src/psiml/print.cljc
new file mode 100644
index 0000000..1970ebc
--- /dev/null
+++ b/src/psiml/print.cljc
@@ -0,0 +1,52 @@
+(ns psiml.print
+ (:require [clojure.core.match :refer [match]])
+ (:require [psiml.util :refer [flatten-kw interpose-fn]]))
+
+(defn expr
+ [e]
+ (match e
+ [:abs n e1] (do (print "λ") (print n) (print ".") (expr e1))
+ [:app e1 e2] (do (print "(") (expr e1)
+ (print " ") (expr e2) (print ")"))
+ [:lit l] (print l)
+ [:var n] (print n)
+ [:struct m]
+ (do (print "{")
+ (interpose-fn #(print " ")
+ (map (fn [[l e]]
+ #(do (print l)
+ (print " ")
+ (expr e))) m))
+ (print "}"))
+ [:get l e1] (do (print "(") (print l)
+ (print " ") (expr e1) (print ")"))
+ [:if test then else]
+ (do (print "(if ") (expr test)
+ (print " then ") (expr then)
+ (print " else ") (expr else) (print ")"))))
+
+(defn type
+ [t]
+ (match t
+ [:top] (print "⊤")
+ [:bot] (print "⊥")
+ [:t base] (print base)
+ [:var n] (do (print "'") (print n))
+ [:abs t1 t2] (do (print "((") (type t1) (print ")")
+ (print " → ") (type t2) (print ")"))
+ [:struct m]
+ (do (print "{")
+ (interpose-fn #(print " ")
+ (map (fn [[l t]]
+ #(do (print l)
+ (print " ")
+ (type t))) m))
+ (print "}"))
+ [:meet & ts]
+ (interpose-fn #(print " ⊓ ")
+ (map #(fn [] (type %))
+ (flatten-kw :meet ts [])))
+ [:join & ts]
+ (interpose-fn #(print " ⊔ ")
+ (map #(fn [] (type %))
+ (flatten-kw :join ts [])))))
diff --git a/src/psiml/type.cljc b/src/psiml/type.cljc
new file mode 100644
index 0000000..a585529
--- /dev/null
+++ b/src/psiml/type.cljc
@@ -0,0 +1,287 @@
+(ns psiml.type
+ "Types abstract syntax, producing typed abstract syntax"
+ #?(:cljs (:require-macros psiml.type))
+ (:require [clojure.core.match :refer [match]]
+ [psiml.util :refer [debug flatten-kw merge-kw]]
+ [psiml.print :as prt]))
+
+;; TODO: typed ast {:node n :type t}
+
+;; type environment: {name -> input type}
+
+(defn print-t-env
+ [[t env]]
+ (do (print "type: ") (prt/type t) (println)
+ (print "env: ") (prt/type [:struct env]) (println)))
+
+(declare bisubstitute-input)
+(declare bisubstitute-output)
+
+(defn bisubstitute-input
+ "Substitutes input occurences of n with t-in and
+ output occurences with t-out in the input type t."
+ [n t-in t-out t]
+ (let [sub-in #(bisubstitute-input n t-in t-out %)
+ sub-out #(bisubstitute-output n t-in t-out %)]
+ (match t
+ [:var n'] (if (= n n') t-in [:var n'])
+ [:struct t-m]
+ [:struct (into {} (map (fn [[l t]] [l (sub-in t)]) t-m))]
+ [:abs t1 t2] [:abs (sub-out t1) (sub-in t2)]
+ ;; [:rec t] [:rec (sub-in t)]
+ [:meet & ts] (into [:meet] (map sub-in ts))
+ :else t)))
+
+(defn bisubstitute-output
+ "Substitutes input occurences of n with t-in and
+ output occurences with t-out in the output type t."
+ [n t-in t-out t]
+ (let [sub-in #(bisubstitute-input n t-in t-out %)
+ sub-out #(bisubstitute-output n t-in t-out %)]
+ (match t
+ [:var n'] (if (= n n') t-out [:var n'])
+ [:struct t-m]
+ [:struct (into {} (map (fn [[l t]] [l (sub-out t)]) t-m))]
+ [:abs t1 t2] [:abs (sub-in t1) (sub-out t2)]
+ ;; [:rec t] [:rec (sub-out t)]
+ [:join & ts] (into [:join] (map sub-out ts))
+ :else t)))
+
+(defn bisubstitute-env
+ "Substitutes input occurences of n with t-in and
+ output occurences with t-out in the environment."
+ [n t-in t-out env]
+ (let [sub-in #(bisubstitute-input n t-in t-out %)]
+ (->> env
+ (map (fn [[n' t']] [n' (sub-in t')]))
+ (into {}))))
+
+(defn bisubstitute-constraints
+ [n t-in t-out constraints]
+ (into []
+ (map (fn [[to ti]] [(bisubstitute-output n t-in t-out to)
+ (bisubstitute-input n t-in t-out ti)])
+ constraints)))
+
+(assoc-in {:x {:y 1}} [:x :y] 2)
+
+(defn take-var-t
+ "Removes the type t of the variable n from env
+ and return [t env]."
+ [n env] [(or (env n) [:top]) (dissoc env n)])
+
+(defn free-vars
+ ([t bound] (free-vars t bound #{}))
+ ([t bound res]
+ (let [collect #(reduce (fn [r t] (free-vars t bound r))
+ res %)]
+ (match t
+ [:top] res
+ [:bot] res
+ [:t _] res
+ [:var n] (if (bound n) res (conj res n))
+ [:struct t-m] (collect (vals t-m))
+ [:abs a b] (collect [a b])
+ [:t-abs n t'] (free-vars t' (conj bound n) res)
+ [:meet & ts] (collect ts)
+ [:join & ts] (collect ts)
+ :else res))))
+
+;; FIXME: simplification
+(declare simplify-input)
+(declare simplify-output)
+
+(defn simplify-input
+ [t]
+ (match t
+ [:abs to ti]
+ [:abs (simplify-output to) (simplify-input ti)]
+ [:struct m]
+ [:struct
+ (into {} (map (fn [[l ti]] [l (simplify-input ti)]) m))]
+ [:meet & ts]
+ (let [meets (flatten-kw :meet ts [])
+ meets (group-by #(first %) meets)
+ var (into #{} (:var meets))
+ basic (into #{} (:t meets))
+ abs (if-let [as (:abs meets)]
+ [(simplify-input
+ [:abs
+ (merge-kw :join (map (fn [[_ to _]] to) as))
+ (merge-kw :meet (map (fn [[_ _ ti]] ti) as))])])
+ struct (if-let [ss (:struct meets)]
+ [(simplify-input
+ [:struct
+ (apply merge-with
+ (fn [a b] [:meet a b])
+ (map (fn [[_ m]] m) ss))])])]
+ (or (merge-kw :meet (concat var basic abs struct)) [:top]))
+ :else t))
+
+(defn simplify-output
+ [t]
+ (match t
+ [:abs ti to]
+ [:abs (simplify-input ti) (simplify-output to)]
+ [:struct m]
+ [:struct
+ (into {} (map (fn [[l to]] [l (simplify-output to)]) m))]
+ [:join & ts]
+ (let [joins (flatten-kw :join ts [])
+ joins (group-by #(first %) joins)
+ var (into #{} (:var joins))
+ basic (into #{} (:t joins))
+ abs (if-let [as (:abs joins)]
+ [(simplify-output
+ [:abs
+ (merge-kw :meet (map (fn [[_ ti _]] ti) as))
+ (merge-kw :join (map (fn [[_ _ to]] to) as))])])
+ struct (if-let [ss (:struct joins)]
+ (let [ms (map (fn [[_ m]] m) ss)
+ ls (apply clojure.set/intersection
+ (map #(into #{} (keys %)) ms))]
+ [(simplify-output
+ [:struct
+ (apply merge-with
+ (fn [a b] [:join a b])
+ (map #(into {}
+ (filter
+ (fn [[l _]] (ls l))
+ %))
+ ms))])]))]
+ (or (merge-kw :join (concat var basic abs struct)) [:bot]))
+ :else t))
+
+(defn simplify
+ [[t env]]
+ [(simplify-output t)
+ (->> env
+ (map (fn [[n t]] [n (simplify-input t)]))
+ (into {}))])
+
+(defn biunify
+ "Biunifies each constraint, for the output to flow in the input.
+ Applies the bisubstitutions on the output type t and
+ the negative environment env, returning [t env]."
+ [constraints t env]
+ (if-let [[t-out t-in] (peek constraints)]
+ (let [cs (pop constraints)
+ [cs t env]
+ (match [t-out t-in]
+ [_ [:top]] [cs t env]
+ [[:bot] _] [cs t env]
+ [[:t a] [:t b]]
+ (if (= a b) [cs t env] [[] nil env])
+ ;; TODO [[:var a] [:var a]] (recur cs t env)
+ [[:var a] _]
+ (let [t-in [:meet [:var a] t-in]
+ cs (bisubstitute-constraints a t-in t-out cs)
+ t (bisubstitute-output a t-in t-out t)
+ env (bisubstitute-env a t-in t-out env)]
+ [cs t env])
+ [_ [:var a]]
+ (let [t-out [:join [:var a] t-out]
+ cs (bisubstitute-constraints a t-in t-out cs)
+ t (bisubstitute-output a t-in t-out t)
+ env (bisubstitute-env a t-in t-out env)]
+ [cs t env])
+ [_ [:meet & ts]]
+ [(into cs (map (fn [t] [t-out t]) ts)) t env]
+ [[:join & ts] _]
+ [(into cs (map (fn [t] [t t-in]) ts)) t env]
+ [[:struct tm-out] [:struct tm-in]]
+ [(reduce (fn [cs [l ti]] (conj cs [(tm-out l) ti]))
+ cs tm-in)
+ t env]
+ [[:abs toi too] [:abs tio tii]]
+ [(into cs [[tio toi] [too tii]]) t env]
+ ;; [[:rec to] [:rec ti]]
+ :else [[] nil env])]
+ (recur cs t env))
+ [t env]))
+
+(defn env-meet
+ [envs]
+ (apply merge-with (fn [a b] [:meet a b]) envs))
+
+(defn expr
+ "Types an expression"
+ ([e] (expr e {}))
+ ([exp env]
+ (let [te
+ (simplify (match exp
+ [:abs n e]
+ (if-let [[t-e env] (expr e env)]
+ (if-let [[t-n env] (take-var-t n env)]
+ [[:abs t-n t-e] env]))
+ ;; [:rec n e]
+ ;; (with-env env
+ ;; [t-n t-e] (with-var n #(expr e %))
+ ;; t (biunify t-e t-n)
+ ;; [:rec n t])
+ [:lit c] [(cond (integer? c) [:t :int]
+ (or (true? c) (false? c)) [:t :bool])
+ env]
+ [:var n] (if-let [t (env n)]
+ [t env]
+ (let [t [:var (gensym "t")]]
+ [t (assoc env n t)]))
+ [:app e1 e2]
+ (if-let [[t1 env1] (expr e1 env)]
+ (if-let [[t2 env2] (expr e2 env)]
+ (let [t? [:var (gensym "a")]]
+ (biunify [[t1 [:abs t2 t?]]]
+ t? (env-meet [env1 env2])))))
+ [:struct m]
+ (if-let [t-env-m (reduce
+ (fn [t-env-m [l e]]
+ (if-let [t-env (expr e env)]
+ (assoc t-env-m l t-env)
+ (reduced nil)))
+ {} m)]
+ [[:struct (into {} (map (fn [[l [t _]]] [l t]) t-env-m))]
+ (env-meet (map #(second %) (vals t-env-m)))])
+ [:get l e]
+ (if-let [[t env] (expr e env)]
+ (let [t? [:var (gensym "g")]]
+ (biunify [[t [:struct {l t?}]]]
+ t? env)))
+ [:if e-test e-then e-else]
+ (if-let [[t-test env-test] (expr e-test env)]
+ (if-let [[t-then env-then] (expr e-then env)]
+ (if-let [[t-else env-else] (expr e-else env)]
+ (let [t? [:var (gensym "i")]]
+ (biunify [[t-test [:t :bool]]
+ [t-then t?]
+ [t-else t?]]
+ t?
+ (env-meet [env-test env-then env-else]))))))
+ :else nil))]
+ (do (prt/expr exp) (println) (print-t-env te) te))))
+
+(defn eq?
+ ([t1 t2] (eq? t1 t2 {}))
+ ([t1 t2 vars]
+ (let [every-eq? #(reduce (fn [vs [a b]]
+ (or (eq? a b vs) (reduced false)))
+ vars %)]
+ (match [t1 t2]
+ [[:top] [:top]] vars
+ [[:bot] [:bot]] vars
+ [[:t b1] [:t b2]] (if (= b1 b2) vars)
+ [[:var n1] [:var n2]] (if (contains? vars n1)
+ (if (= (vars n1) n2) vars)
+ (assoc vars n1 n2))
+ [[:struct tm1] [:struct tm2]]
+ (and (= (into #{} (keys tm1)) (into #{} (keys tm2)))
+ (every-eq? (map (fn [[l t1]] [t1 (tm2 l)]) tm1)))
+ [[:abs a1 b1] [:abs a2 b2]]
+ (every-eq? [[a1 a2] [b1 b2]])
+ [[:t-abs n1 t1'] [:t-abs n2 t2']]
+ (eq? t1' t2')
+ ;; [[:rec a1] [:rec a2]] (eq? [a1 env1] [a2 env2])
+ [[:meet & ts1] [:meet & ts2]]
+ (every-eq? (map (fn [t1 t2] [t1 t2]) ts1 ts2))
+ [[:join & ts1] [:join & ts2]]
+ (every-eq? (map (fn [t1 t2] [t1 t2]) ts1 ts2))
+ :else false))))
diff --git a/src/psiml/util.cljc b/src/psiml/util.cljc
new file mode 100644
index 0000000..9d7b9d4
--- /dev/null
+++ b/src/psiml/util.cljc
@@ -0,0 +1,43 @@
+(ns psiml.util
+ #?(:cljs (:require-macros psiml.util)))
+
+(defn by-two
+ ([s] (by-two s nil))
+ ([s e] (if-let [s (seq s)]
+ (if e
+ (lazy-seq (cons [e (first s)] (by-two (rest s) nil)))
+ (by-two (rest s) (first s)))
+ s)))
+
+(defmacro match-first
+ [& binds]
+ (let [e (gensym)
+ tests (map (fn [[p _]] `(= ~(first p) (first ~e)))
+ (by-two binds))
+ handlers (map (fn [[p b]] `(fn [~@(rest p)] ~b))
+ (by-two binds))
+ handler `(cond ~@(interleave tests handlers))]
+ `(fn [~e] (apply ~handler (rest ~e)))))
+
+(defmacro debug
+ [expr]
+ (let [r (gensym)]
+ `(let [~r ~expr]
+ (println ~(str expr) ~r) ~r)))
+
+(defn flatten-kw
+ ([kw t] (flatten-kw kw [t] []))
+ ([kw todo flat]
+ (if-let [t (peek todo)]
+ (if (= kw (first t))
+ (recur kw (into (pop todo) (rest t)) flat)
+ (recur kw (pop todo) (cons t flat)))
+ flat)))
+
+(defn merge-kw
+ [kw ts]
+ (if (second ts) (into [kw] ts) (first ts)))
+
+(defn interpose-fn
+ [f fs]
+ (reduce (fn [_ f] (f)) nil (interpose f fs)))
diff --git a/test/psiml/core_test.clj b/test/psiml/core_test.clj
new file mode 100644
index 0000000..eecbb4b
--- /dev/null
+++ b/test/psiml/core_test.clj
@@ -0,0 +1,9 @@
+(ns psiml.core-test
+ (:require [clojure.test :refer :all]
+ [psiml.core :refer :all]))
+
+(deftest eval-expr-simple
+ (testing "Evaluate a simple expression"
+ (let [e [:app [:abs :x [:get :a [:var :x]]] [:struct {:a [:var :y]}]]
+ r [:var :y]]
+ (is (= (eval-expr e) r)))))
diff --git a/test/psiml/parse_test.clj b/test/psiml/parse_test.clj
new file mode 100644
index 0000000..ff88e9f
--- /dev/null
+++ b/test/psiml/parse_test.clj
@@ -0,0 +1,35 @@
+(ns psiml.parse-test
+ (:require [clojure.test :refer :all]
+ [psiml.core :refer :all]
+ [psiml.parse :refer :all]))
+
+(deftest parse-expr-simple
+ (testing "Parse an int"
+ (is (= (string "7") [:lit 7])))
+ (testing "Parse a function with a struct"
+ (let [e "(fn [label] {:label true})"
+ r [:abs :label [:struct {:label [:lit true]}]]]
+ (is (= (string e) r))))
+ (testing "Parse a function with a nested struct"
+ (let [e "(fn [label] {:label {:hello false}})"
+ r [:abs :label [:struct {:label [:struct {:hello [:lit false]}]}]]]
+ (is (= (string e) r))))
+ (testing "Function with multiple parameters"
+ (let [e "(fn [a b c] a)"
+ r [:abs :a [:abs :b [:abs :c [:var :a]]]]]
+ (is (= (string e) r))))
+ (testing "Application with multiple arguments"
+ (let [e "(f a b 3)"
+ r [:app [:app [:app [:var :f] [:var :a]]
+ [:var :b]]
+ [:lit 3]]]
+ (is (= (string e) r))))
+ (testing "Get a label"
+ (is (= (string "(:l s)") [:get :l [:var :s]])))
+ (testing "Let some stuff"
+ (let [e "(let [a 1 b (fn [x] x)] b)"
+ r [:app [:abs :a
+ [:app [:abs :b [:var :b]]
+ [:abs :x [:var :x]]]]
+ [:lit 1]]]
+ (is (= (string e) r)))))
diff --git a/test/psiml/type_test.clj b/test/psiml/type_test.clj
new file mode 100644
index 0000000..f913e4d
--- /dev/null
+++ b/test/psiml/type_test.clj
@@ -0,0 +1,127 @@
+(ns psiml.type-test
+ (:require [clojure.test :refer :all]
+ [psiml.type :refer :all]))
+
+(def t-int [:t :int])
+(def t-bool [:t :bool])
+
+(deftest test-free-vars
+ (is (= (free-vars [:var :x] #{}) #{:x}))
+ (is (= (free-vars [:var :x] #{:x}) #{}))
+ (is (= (free-vars [:t-abs :x [:var :x]] #{}) #{}))
+ (is (= (free-vars
+ [:t-abs :x [:abs [:var :x] [:var :y]]] #{})
+ #{:y})))
+
+(def s-iibb [:struct {:i t-int :b t-bool}])
+(def s-ibbi [:struct {:i t-bool :b t-int}])
+(def s-abiibb [:struct {:a t-bool :i t-int :b t-bool}])
+
+(defn is-meet?
+ [a b r]
+ (is (= (simplify-input [:meet a b]) r)))
+
+(deftest test-meet
+ (is-meet? t-int t-int t-int)
+ (is-meet? t-int t-bool [:meet t-bool t-int])
+ (is-meet? s-iibb s-iibb s-iibb)
+ (is-meet? s-iibb s-ibbi
+ [:struct {:i [:meet t-bool t-int]
+ :b [:meet t-bool t-int]}])
+ (is-meet? s-abiibb s-iibb s-abiibb))
+
+(defn is-join?
+ [a b r]
+ (is (= (simplify-output [:join a b]) r)))
+
+(deftest test-join
+ (is-join? t-int t-int t-int)
+ (is-join? t-int t-bool [:join t-bool t-int])
+ (is-join? s-iibb s-iibb s-iibb)
+ (is-join? s-iibb s-ibbi
+ [:struct {:i [:join t-bool t-int]
+ :b [:join t-bool t-int]}])
+ (is-join? s-abiibb s-iibb s-iibb))
+
+(defn is-biunify?
+ [a b r]
+ (is (= (first (biunify [[a b]] a {})) r)))
+
+(deftest test-biunify
+ (is-biunify? t-int t-int t-int)
+ (is-biunify? t-int t-bool nil)
+ (is-biunify? s-iibb s-iibb s-iibb)
+ (is-biunify? s-iibb s-ibbi nil)
+ (is-biunify? s-abiibb s-iibb s-abiibb)
+ (is-biunify? s-iibb s-abiibb nil))
+
+(deftest test-eq?
+ (is (eq? [:t-abs :a [:var :a]]
+ [:t-abs :b [:var :b]])))
+
+(defn is-typed?
+ ([e t] (is-typed? e t {}))
+ ([e t vars]
+ (let [[t' _] (expr e vars)]
+ (is (eq? t' t)))))
+
+(deftest test-expr
+ (is-typed? [:lit 1] t-int)
+ (is-typed? [:lit true] t-bool)
+ (let [s [:struct {:a [:lit 1] :b [:lit true]}]]
+ (is-typed? s [:struct {:a t-int :b t-bool}])
+ (is-typed? [:get :a s] t-int)))
+
+(def id [:abs :x [:var :x]])
+
+(deftest expr-id
+ (is-typed? id [:abs [:var :a] [:var :a]]))
+
+(deftest select-int-bool
+ (is-typed? [:abs :p
+ [:abs :v
+ [:abs :d
+ [:if [:app [:var :p] [:var :v]]
+ [:app [:var :int-id] [:var :v]]
+ [:app [:var :bool-id] [:var :d]]]]]]
+ [:abs [:abs t-int t-bool]
+ [:abs t-int
+ [:abs t-bool
+ [:join t-bool t-int]]]]
+ {:int-id [:abs t-int t-int]
+ :bool-id [:abs t-bool t-bool]}))
+
+(deftest int-or-bool
+ (is-typed? [:if [:var :t] [:lit 1] [:lit true]]
+ [:join [:t :bool] [:t :int]]))
+
+(deftest a-or-b
+ (is-typed? [:if [:var :t] [:var :a] [:var :b]]
+ [:join [:var :a] [:var :b]]))
+
+(deftest select
+ (is-typed? [:abs :p
+ [:abs :v
+ [:abs :d
+ [:if [:app [:var :p] [:var :v]]
+ [:var :v]
+ [:var :d]]]]]
+ [:abs [:abs [:var :v] t-bool]
+ [:abs [:var :v]
+ [:abs [:var :d]
+ [:join [:var :v] [:var :d]]]]]))
+
+;; NEXT TARGET:
+;; (deftest meet-and
+;; (is-typed? [:abs :p
+;; [:abs :a
+;; [:abs :b
+;; [:if [:app [:var :p] [:var :a]]
+;; [:app [:var :p] [:var :b]]
+;; [:lit false]]]]]
+;; [:t-abs :a
+;; [:t-abs :b
+;; [:abs [:abs [:meet [:var :a] [:var :b]] t-bool]
+;; [:abs [:var :a]
+;; [:abs [:var :b]
+;; t-bool]]]]]))