From e60d7720b630609126148f5c99a5fa11dd13334a Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Fri, 1 Dec 2017 18:17:53 +0100 Subject: [PATCH 01/13] First setup --- .gitignore | 17 ++++++++--------- README.md | 15 ++++++++++++++- doc/intro.md | 3 +++ index.html | 9 +++++++++ project.clj | 15 +++++++++++++++ src/psiml/core.cljc | 26 ++++++++++++++++++++++++++ test/psiml/core_test.clj | 7 +++++++ 7 files changed, 82 insertions(+), 10 deletions(-) create mode 100644 doc/intro.md create mode 100644 index.html create mode 100644 project.clj create mode 100644 src/psiml/core.cljc create mode 100644 test/psiml/core_test.clj 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/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 @@ + +
+ + psiml +
+ + + + diff --git a/project.clj b/project.clj new file mode 100644 index 0000000..153e88f --- /dev/null +++ b/project.clj @@ -0,0 +1,15 @@ +(defproject psiml "0.1.0-SNAPSHOT" + :description "Polymorphic, Subtyped and type Infered ML" + :dependencies [[org.clojure/clojure "1.8.0"] + [org.clojure/clojurescript "1.9.521" + :exclusions [org.apache.ant/ant]]] + :plugins [[lein-cljsbuild "1.1.7"]] + :cljsbuild { :builds [{:source-paths ["src"] + :compiler {:main psiml.core + :output-to "web/main.js" + :output-dir "web/" + :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..26e9530 --- /dev/null +++ b/src/psiml/core.cljc @@ -0,0 +1,26 @@ +(ns psiml.core) + +#?(:cljs (enable-console-print!)) + +(defn -main + "I don't do a whole lot ... yet." + [& args] + (let [e :expr + abs [:abs "name" e] + var [:var "name"] + app [:app e e] + rec [:rec {"label" e}] + get [:get "label" e] + let [:let "name" e]] + ;; let-var ? can be inferred + ;; let-rec ? can be inferred + ;; then types with type variables and recursive types + (do (println "Hello, expressions!") + (println abs) + (println var) + (println app) + (println rec) + (println get) + (println let)))) + +#?(:cljs (-main)) diff --git a/test/psiml/core_test.clj b/test/psiml/core_test.clj new file mode 100644 index 0000000..b249866 --- /dev/null +++ b/test/psiml/core_test.clj @@ -0,0 +1,7 @@ +(ns psiml.core-test + (:require [clojure.test :refer :all] + [psiml.core :refer :all])) + +(deftest a-test + (testing "FIXME, I fail." + (is (= 0 1)))) From 05be4a456ede6528e116d8a908559fb1434d3e83 Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Sun, 3 Dec 2017 21:50:27 +0100 Subject: [PATCH 02/13] Simple lambda --- .travis.yml | 1 + src/psiml/core.cljc | 39 +++++++++++++++++++++------------------ src/psiml/util.cljc | 19 +++++++++++++++++++ test/psiml/core_test.clj | 8 +++++--- 4 files changed, 46 insertions(+), 21 deletions(-) create mode 100644 .travis.yml create mode 100644 src/psiml/util.cljc 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/src/psiml/core.cljc b/src/psiml/core.cljc index 26e9530..33d77ce 100644 --- a/src/psiml/core.cljc +++ b/src/psiml/core.cljc @@ -1,26 +1,29 @@ -(ns psiml.core) +(ns psiml.core + (:require [psiml.util + #?(:clj :refer + :cljs :refer-macros) [match-first]])) #?(:cljs (enable-console-print!)) +(defn eval-lambda + "Evaluates an extended lambda calculi expression" + ([expr] (eval-lambda expr {})) + ([expr env] + ((match-first + [:abs n e] [:abs n (eval-lambda e env)] + [:var n] (or (env n) [:var n]) + [:app e1 e2] (let [e2' (eval-lambda e2 env)] + (or ((match-first [:abs n e1'] (eval-lambda e1' (conj env [n e2']))) e1) + [:app (eval-lambda e1 env) e2'])) + [:rec m] [:rec (reduce (fn [m' [l e]] (assoc m' l (eval-lambda e env))) {} m)] + [:get l e] (let [e' (eval-lambda e env)] + (or ((match-first [:rec m] (m l)) e') + [:get l e']))) + expr))) + (defn -main "I don't do a whole lot ... yet." [& args] - (let [e :expr - abs [:abs "name" e] - var [:var "name"] - app [:app e e] - rec [:rec {"label" e}] - get [:get "label" e] - let [:let "name" e]] - ;; let-var ? can be inferred - ;; let-rec ? can be inferred - ;; then types with type variables and recursive types - (do (println "Hello, expressions!") - (println abs) - (println var) - (println app) - (println rec) - (println get) - (println let)))) + (println "Hello!")) #?(:cljs (-main)) diff --git a/src/psiml/util.cljc b/src/psiml/util.cljc new file mode 100644 index 0000000..e96e1c1 --- /dev/null +++ b/src/psiml/util.cljc @@ -0,0 +1,19 @@ +(ns 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))))) diff --git a/test/psiml/core_test.clj b/test/psiml/core_test.clj index b249866..b1d44ae 100644 --- a/test/psiml/core_test.clj +++ b/test/psiml/core_test.clj @@ -2,6 +2,8 @@ (:require [clojure.test :refer :all] [psiml.core :refer :all])) -(deftest a-test - (testing "FIXME, I fail." - (is (= 0 1)))) +(deftest eval-lambda-simple + (testing "Evaluate a simple expression" + (let [e [:app [:abs "x" [:get "a" [:var "x"]]] [:rec {"a" [:var "y"]}]] + r [:var "y"]] + (is (= (eval-lambda e) r))))) From 66e63b647b8ba2067c165990c8c7ce725503bb3a Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Wed, 6 Dec 2017 12:44:15 +0100 Subject: [PATCH 03/13] Core language and types --- src/psiml/core.cljc | 25 +++++++++++++++++++++++-- test/psiml/core_test.clj | 2 +- 2 files changed, 24 insertions(+), 3 deletions(-) diff --git a/src/psiml/core.cljc b/src/psiml/core.cljc index 33d77ce..8c10e91 100644 --- a/src/psiml/core.cljc +++ b/src/psiml/core.cljc @@ -11,16 +11,37 @@ ([expr env] ((match-first [:abs n e] [:abs n (eval-lambda e env)] + [:rec n e] [:rec n (eval-lambda e (conj env [n e]))] + [:cst c] [:cst c] [:var n] (or (env n) [:var n]) [:app e1 e2] (let [e2' (eval-lambda e2 env)] (or ((match-first [:abs n e1'] (eval-lambda e1' (conj env [n e2']))) e1) [:app (eval-lambda e1 env) e2'])) - [:rec m] [:rec (reduce (fn [m' [l e]] (assoc m' l (eval-lambda e env))) {} m)] + [:struct m] [:struct (reduce (fn [m' [l e]] (assoc m' l (eval-lambda e env))) {} m)] [:get l e] (let [e' (eval-lambda e env)] - (or ((match-first [:rec m] (m l)) e') + (or ((match-first [:struct m] (m l)) e') [:get l e']))) expr))) +;; [:t :int] +;; [:t :bool] +;; [:t-abs {ty -> ty}] +;; [:t-rec] +;; [:t-struct {field -> ty}] +;; [:t-var n] +;; [:t-top] +;; [:t-bot] +;; [:t-meet t t] +;; [:t-join t t] + +;; 1 --> [:t :int] +;; true --> [:t :bool] +;; (fn [n1 n2] e) --> [:abs n1 [:abs n2 r(e)]] +;; {l1 e1 l2 e2} --> [:struct {l1 r(e1) l2 r(e2)}] +;; (:l e) --> [:get l r(e)] +;; (let [n e1] e2) --> [:app [:abs n r(e2)] [:rec n r(e1)]] +;; (e1 e2) --> [:app r(e1) r(e2)] + (defn -main "I don't do a whole lot ... yet." [& args] diff --git a/test/psiml/core_test.clj b/test/psiml/core_test.clj index b1d44ae..6c2db64 100644 --- a/test/psiml/core_test.clj +++ b/test/psiml/core_test.clj @@ -4,6 +4,6 @@ (deftest eval-lambda-simple (testing "Evaluate a simple expression" - (let [e [:app [:abs "x" [:get "a" [:var "x"]]] [:rec {"a" [:var "y"]}]] + (let [e [:app [:abs "x" [:get "a" [:var "x"]]] [:struct {"a" [:var "y"]}]] r [:var "y"]] (is (= (eval-lambda e) r))))) From 63f31ff778e41e0a1db14af3c0b8b9b2a14326b0 Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Wed, 13 Dec 2017 16:02:56 +0100 Subject: [PATCH 04/13] Begin parsing and typing --- project.clj | 21 ++++--- src/psiml/core.cljc | 48 +++++++--------- src/psiml/parse.cljc | 20 +++++++ src/psiml/type.cljc | 118 +++++++++++++++++++++++++++++++++++++++ src/psiml/util.cljc | 3 +- test/psiml/core_test.clj | 8 +-- test/psiml/type_test.clj | 34 +++++++++++ 7 files changed, 209 insertions(+), 43 deletions(-) create mode 100644 src/psiml/parse.cljc create mode 100644 src/psiml/type.cljc create mode 100644 test/psiml/type_test.clj diff --git a/project.clj b/project.clj index 153e88f..3d63d11 100644 --- a/project.clj +++ b/project.clj @@ -1,15 +1,18 @@ (defproject psiml "0.1.0-SNAPSHOT" :description "Polymorphic, Subtyped and type Infered ML" - :dependencies [[org.clojure/clojure "1.8.0"] - [org.clojure/clojurescript "1.9.521" + :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"]] - :cljsbuild { :builds [{:source-paths ["src"] - :compiler {:main psiml.core - :output-to "web/main.js" - :output-dir "web/" - :optimizations :whitespace - :pretty-print true}}]} + :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 index 8c10e91..79d66e7 100644 --- a/src/psiml/core.cljc +++ b/src/psiml/core.cljc @@ -1,38 +1,27 @@ (ns psiml.core - (:require [psiml.util - #?(:clj :refer - :cljs :refer-macros) [match-first]])) + (:require [psiml.type :as t] + [psiml.parse :as p] + [clojure.core.match :refer [match]])) #?(:cljs (enable-console-print!)) -(defn eval-lambda - "Evaluates an extended lambda calculi expression" - ([expr] (eval-lambda expr {})) +(defn eval-expr + "Evaluates an expression" + ([expr] (eval-expr expr {})) ([expr env] - ((match-first - [:abs n e] [:abs n (eval-lambda e env)] - [:rec n e] [:rec n (eval-lambda e (conj env [n e]))] + (match expr + [:abs n e] [:abs n (eval-expr e env)] + [:rec n e] [:rec n (eval-expr e (conj env [n e]))] [:cst c] [:cst c] [:var n] (or (env n) [:var n]) - [:app e1 e2] (let [e2' (eval-lambda e2 env)] - (or ((match-first [:abs n e1'] (eval-lambda e1' (conj env [n e2']))) e1) - [:app (eval-lambda e1 env) e2'])) - [:struct m] [:struct (reduce (fn [m' [l e]] (assoc m' l (eval-lambda e env))) {} m)] - [:get l e] (let [e' (eval-lambda e env)] - (or ((match-first [:struct m] (m l)) e') - [:get l e']))) - expr))) - -;; [:t :int] -;; [:t :bool] -;; [:t-abs {ty -> ty}] -;; [:t-rec] -;; [:t-struct {field -> ty}] -;; [:t-var n] -;; [:t-top] -;; [:t-bot] -;; [:t-meet t t] -;; [:t-join t t] + [: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))) ;; 1 --> [:t :int] ;; true --> [:t :bool] @@ -45,6 +34,7 @@ (defn -main "I don't do a whole lot ... yet." [& args] - (println "Hello!")) + (let [e (p/string "(fn [n1] true)")] + (println e (t/expr e)))) #?(:cljs (-main)) diff --git a/src/psiml/parse.cljc b/src/psiml/parse.cljc new file mode 100644 index 0000000..3d3e8d7 --- /dev/null +++ b/src/psiml/parse.cljc @@ -0,0 +1,20 @@ +(ns psiml.parse + "Parses concrete syntax, producing abstract syntax" + (: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] + (if (seq? d) + (match d + (['fn [a] b] :seq) + (if (symbol? a) [:abs (keyword a) (data b)])) + (if (or (integer? d) (true? d) (false? d)) [:cst d]))) + +(defn string + "Parses concrete syntax from a string" + [s] + (data (read-string s))) diff --git a/src/psiml/type.cljc b/src/psiml/type.cljc new file mode 100644 index 0000000..5a3d9ab --- /dev/null +++ b/src/psiml/type.cljc @@ -0,0 +1,118 @@ +(ns psiml.type + "Types abstract syntax, producing typed abstract syntax" + #?(:cljs (:require-macros psiml.type)) + (:require [clojure.core.match :refer [match]])) + +;; typed ast {:node n :type t] +;; {:node [:abs :x {:node [:var :x] :type [:t-var]}] +;; :type [:abs [:t-var] [:t-var]]} + +;; [:t :int] +;; [:t :bool] +;; [:abs t t] +;; [:rec t] +;; {:struct {field -> e} + +;; [:top] +;; [:bot] +;; [:meet t t] +;; [:join t t] + +(defn map-env + "Returns (f t env) if t is not nil, otherwise [t env]" + [[t env] f] + (if (nil? t) [t env] (f t env))) + +(defmacro with-env + "Passes an environment through a series of operations, + binding the results and returning a final value. + + The operations are given the environment as an additional + argument and should return a value of the form [result new-env]. + The binding itself is done using map-env, thus aborting the + series of operations after an error." + ([env r] `[~r ~env]) + ([env b f & binds] + (let [senv (if (symbol? env) env (gensym))] + `(map-env (->> ~env ~f) + (fn [~b ~senv] (with-env ~senv ~@binds)))))) + +(defn env-id + "Returns `v` without affecting the environment" + [v env] + [v env]) + +(defn same-labels? + [m1 m2] + (= (into #{} (keys m1)) (into #{} (keys m2)))) + +(defn unify + [t1 t2 env] + (match [t1 t2] + [[:abs t1-in t1-out] [:abs t2-in t2-out]] + (with-env env + t-in (unify t1-in t2-in) + t-out (unify t1-out t2-out) + [:abs t-in t-out]) + [[:rec t1] [:rec t2]] + (with-env env + t (unify t1 t2) + [:rec t]) + [[:struct tm1] [:struct tm2]] + (with-env env + _ (env-id (if (same-labels? tm1 tm2) ())) + t-m ((fn [env] + (reduce (fn [[t-m env] [l t1]] + (let [t2 (tm2 l)] + (with-env env + t (unify t1 t2) + (assoc t-m l t)))) [{} env] tm1))) + [:struct t-m]) + [[:t b1] [:t b2]] (if (= b1 b2) [[:t b1] env] [nil env]) + :else [nil env])) + +(defn with-var + [n f env] + (let [shadow (env n) + [t-f env] (f (assoc env n [:t-var])) + t-n (env n)] + [[t-n t-f] (if shadow (assoc env n shadow) (dissoc env n))])) + +(defn expr + "Types an expression" + ([e] (expr e {})) + ([exp env] + (match exp + [:abs n e] + (with-env env + [t-n t-e] (with-var n #(expr e %)) + [:abs t-n t-e]) + [:rec n e] + (with-env env + [t-n t-e] (with-var n #(expr e %)) + t (unify t-n t-e) + [:rec n t]) + [:cst c] [(cond (integer? c) [:t :int] + (or (true? c) (false? c)) [:t :bool]) + env] + [:var n] [(env n) env] + [:app e1 e2] + (with-env env + t1 (expr e1) + t2 (expr e2) + [t-in t-out] (env-id (match t1 + [:abs a b] [a b] + :else nil)) + t (unify t-in t2) + t-out) + [:struct m] + (with-env env + t-m #((reduce (fn [[t-m env] [l e]] + (with-env env + t (expr e) + (assoc t-m l t))) [{} %] m)) + [:struct t-m]) + [:get l e] + (with-env env + t (expr e) + (match t [:struct t-m] (t-m l) :else nil))))) diff --git a/src/psiml/util.cljc b/src/psiml/util.cljc index e96e1c1..3fa747d 100644 --- a/src/psiml/util.cljc +++ b/src/psiml/util.cljc @@ -1,4 +1,5 @@ -(ns psiml.util) +(ns psiml.util + #?(:cljs (:require-macros psiml.util))) (defn by-two ([s] (by-two s nil)) diff --git a/test/psiml/core_test.clj b/test/psiml/core_test.clj index 6c2db64..eecbb4b 100644 --- a/test/psiml/core_test.clj +++ b/test/psiml/core_test.clj @@ -2,8 +2,8 @@ (:require [clojure.test :refer :all] [psiml.core :refer :all])) -(deftest eval-lambda-simple +(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-lambda e) r))))) + (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/type_test.clj b/test/psiml/type_test.clj new file mode 100644 index 0000000..402c492 --- /dev/null +++ b/test/psiml/type_test.clj @@ -0,0 +1,34 @@ +(ns psiml.type-test + (:require [clojure.test :refer :all] + [psiml.type :refer :all])) + +(def t-int [:t :int]) +(def t-bool [:t :bool]) + +(deftest unify-basetypes + (is (= (unify t-int t-bool {}) [nil {}])) + (is (= (unify t-int t-int {}) [t-int {}]))) + +(deftest unify-struct + (is (= (unify [:struct {:i t-int :b t-bool}] + [:struct {:b t-bool :i t-int}] {}) + [[:struct {:i t-int :b t-bool}] {}])) + (is (= (unify [:struct {:i t-int :b t-bool}] + [:struct {:b t-int :i t-bool}] {}) + [nil {}])) + (is (= (unify [:struct {:i t-int :b t-bool}] + [:struct {:a t-bool :b t-bool :i t-int}] {}) + [nil {}]))) + +(deftest expr-basetypes + (is (= (expr [:cst 1]) [t-int {}])) + (is (= (expr [:cst true]) [t-bool {}]))) + +(def id [:abs :x [:var :x]]) + +(deftest expr-id + (is (= (expr id) [[:abs [:t-var] [:t-var]] {}]))) + +;; (deftest expr-id-app +;; (is (= (expr [:app id [:var :y]] {:y [:t-var]}) +;; [[:t-var] {:y [:t-var]}]))) From 5518c115871e9c65d2f5ed7999101403d6fd3df3 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 15 Dec 2017 01:00:15 +0100 Subject: [PATCH 05/13] Parsing struct et get --- src/psiml/core.cljc | 6 +++++- src/psiml/parse.cljc | 21 ++++++++++++++++----- 2 files changed, 21 insertions(+), 6 deletions(-) diff --git a/src/psiml/core.cljc b/src/psiml/core.cljc index 79d66e7..0f02219 100644 --- a/src/psiml/core.cljc +++ b/src/psiml/core.cljc @@ -35,6 +35,10 @@ "I don't do a whole lot ... yet." [& args] (let [e (p/string "(fn [n1] true)")] - (println e (t/expr e)))) + (println e (t/expr e))) + (let [e1 (p/string "{:a 1 :b 1}")] + (println e1)) + (let [e2 (p/string "(:l 5)")] + (println e2))) #?(:cljs (-main)) diff --git a/src/psiml/parse.cljc b/src/psiml/parse.cljc index 3d3e8d7..3aabe22 100644 --- a/src/psiml/parse.cljc +++ b/src/psiml/parse.cljc @@ -8,13 +8,24 @@ (defn data "Parses concrete syntax from data" [d] - (if (seq? d) - (match d - (['fn [a] b] :seq) - (if (symbol? a) [:abs (keyword a) (data b)])) - (if (or (integer? d) (true? d) (false? d)) [:cst d]))) + (cond + (seq? d) + (match d + ;; abs + (['fn [a] b] :seq) + (if (symbol? a) [:abs (keyword a) (data b)]) + ;; get + ([a b] :seq) + (if (keyword? a) [:get (name a) (data b)])) + (or (integer? d) (true? d) (false? d)) + [:cst d] + ;; struct + (map? d) + [:struct (reduce #(conj %1 {(first %2) (data(second %2))}) {} d)])) (defn string "Parses concrete syntax from a string" [s] (data (read-string s))) + +(conj {} {(first [:a 1]) (second [:a 1])}) \ No newline at end of file From 679ff441c60a9e76684cecd04b0463fd4d0c18bf Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 15 Dec 2017 11:50:32 +0100 Subject: [PATCH 06/13] Ajout tests --- src/psiml/core.cljc | 10 ++++++---- src/psiml/parse.cljc | 9 ++------- test/psiml/parse_test.clj | 21 +++++++++++++++++++++ 3 files changed, 29 insertions(+), 11 deletions(-) create mode 100644 test/psiml/parse_test.clj diff --git a/src/psiml/core.cljc b/src/psiml/core.cljc index 0f02219..a422794 100644 --- a/src/psiml/core.cljc +++ b/src/psiml/core.cljc @@ -12,7 +12,7 @@ (match expr [:abs n e] [:abs n (eval-expr e env)] [:rec n e] [:rec n (eval-expr e (conj env [n e]))] - [:cst c] [:cst c] + [: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']))) @@ -26,7 +26,7 @@ ;; 1 --> [:t :int] ;; true --> [:t :bool] ;; (fn [n1 n2] e) --> [:abs n1 [:abs n2 r(e)]] -;; {l1 e1 l2 e2} --> [:struct {l1 r(e1) l2 r(e2)}] +;; {:l1 e1 :l2 e2} --> [:struct {:l1 r(e1) :l2 r(e2)}] ;; (:l e) --> [:get l r(e)] ;; (let [n e1] e2) --> [:app [:abs n r(e2)] [:rec n r(e1)]] ;; (e1 e2) --> [:app r(e1) r(e2)] @@ -35,10 +35,12 @@ "I don't do a whole lot ... yet." [& args] (let [e (p/string "(fn [n1] true)")] - (println e (t/expr e))) + (println e)) (let [e1 (p/string "{:a 1 :b 1}")] (println e1)) (let [e2 (p/string "(:l 5)")] - (println e2))) + (println e2)) + (let [e3 (p/string "(fn [label] {:label true})")] + (println e3))) #?(:cljs (-main)) diff --git a/src/psiml/parse.cljc b/src/psiml/parse.cljc index 3aabe22..34114d7 100644 --- a/src/psiml/parse.cljc +++ b/src/psiml/parse.cljc @@ -11,21 +11,16 @@ (cond (seq? d) (match d - ;; abs (['fn [a] b] :seq) (if (symbol? a) [:abs (keyword a) (data b)]) - ;; get ([a b] :seq) (if (keyword? a) [:get (name a) (data b)])) (or (integer? d) (true? d) (false? d)) - [:cst d] - ;; struct + [:lit d] (map? d) - [:struct (reduce #(conj %1 {(first %2) (data(second %2))}) {} d)])) + [:struct (reduce (fn [m [l v]](conj m {l (data v)})) {} d)])) (defn string "Parses concrete syntax from a string" [s] (data (read-string s))) - -(conj {} {(first [:a 1]) (second [:a 1])}) \ No newline at end of file diff --git a/test/psiml/parse_test.clj b/test/psiml/parse_test.clj new file mode 100644 index 0000000..7f0a58a --- /dev/null +++ b/test/psiml/parse_test.clj @@ -0,0 +1,21 @@ +(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" + (let [e "7" + r [:lit 7]] + (is (= (string e) r)))) + (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))))) + + + From 0792b3c44f53f1c87d2a8c9ef96a05ad611f063f Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Fri, 15 Dec 2017 13:56:23 +0100 Subject: [PATCH 07/13] First subtyping implementation --- src/psiml/type.cljc | 113 +++++++++++++++++++++++++++++++-------- test/psiml/type_test.clj | 61 +++++++++++++-------- 2 files changed, 132 insertions(+), 42 deletions(-) diff --git a/src/psiml/type.cljc b/src/psiml/type.cljc index 5a3d9ab..1ef5d3b 100644 --- a/src/psiml/type.cljc +++ b/src/psiml/type.cljc @@ -42,39 +42,110 @@ [v env] [v env]) -(defn same-labels? - [m1 m2] - (= (into #{} (keys m1)) (into #{} (keys m2)))) +(declare unify-input) +(declare unify-output) -(defn unify +(defn unify-input [t1 t2 env] (match [t1 t2] + [[:top] t] [t env] + [t [:top]] [t env] + [[:t b1] [:t b2]] + [(if (= b1 b2) [:t b1] [:meet [:t b1] [:t b2]]) env] + [[:struct tm1] [:struct tm2]] + (with-env env + t-m (#(reduce + (partial reduce (fn [[t-m env] [l t]] + (if (contains? t-m l) + (with-env env + t (unify-input (t-m l) t) + (assoc t-m l t)) + [(assoc t-m l t) env]))) + [{} %] + [tm1 tm2])) + [:struct t-m]) + [[:abs t1-out t1-in] [:abs t2-out t2-in]] + (with-env env + t-in (unify-input t1-in t2-in) + t-out (unify-output t1-out t2-out) + [:abs t-out t-in]) + [[:rec t1] [:rec t2]] + (with-env env + t (unify-input t1 t2) + [:rec t]) + :else [nil env])) + +(defn unify-output + [t1 t2 env] + (match [t1 t2] + [[:bot] t] [t env] + [t [:bot]] [t env] + [[:t b1] [:t b2]] + [(if (= b1 b2) [:t b1] [:join [:t b1] [:t b2]]) env] + [[:struct tm1] [:struct tm2]] + (with-env env + t-m (#(reduce (fn [[t-m env] [l t1]] + (if-let [t2 (tm2 l)] + (with-env env + t (unify-output t1 t2) + (assoc t-m l t)) + ([t-m env]))) + [{} %] tm1)) + [:struct t-m]) [[:abs t1-in t1-out] [:abs t2-in t2-out]] (with-env env - t-in (unify t1-in t2-in) - t-out (unify t1-out t2-out) + t-in (unify-input t1-in t2-in) + t-out (unify-output t1-out t2-out) [:abs t-in t-out]) [[:rec t1] [:rec t2]] (with-env env - t (unify t1 t2) + t (unify-output t1 t2) [:rec t]) - [[:struct tm1] [:struct tm2]] + :else [nil env])) + +(defn bi-unify + [t-in t-out env] + (match [t-in t-out] + [[:top] t] [t env] + [_ [:bot]] [[:bot] env] + [[:t a] [:t b]] + [(if (= a b) [:t a]) env] + [[:struct tm-in] [:struct tm-out]] (with-env env - _ (env-id (if (same-labels? tm1 tm2) ())) - t-m ((fn [env] - (reduce (fn [[t-m env] [l t1]] - (let [t2 (tm2 l)] - (with-env env - t (unify t1 t2) - (assoc t-m l t)))) [{} env] tm1))) + t-m (#(reduce (fn [[t-m env] [l t-in]] + (if-let [t-out (tm-out l)] + (with-env env + t (bi-unify t-in t-out) + (assoc t-m l t)) + [nil env])) + [{} %] + tm-in)) [:struct t-m]) - [[:t b1] [:t b2]] (if (= b1 b2) [[:t b1] env] [nil env]) + [[:abs t-in-out t-in-in] [:abs t-out-in t-out-out]] + (with-env env + t-a (bi-unify t-out-in t-in-out) + t-b (bi-unify t-in-in t-out-out) + [:abs t-a t-b]) + [[:rec t-in] [:rec t-out]] + [nil env] ; TODO + [[:meet t1-in t2-in] _] + (with-env env + t1 (bi-unify t1-in t-out) + t2 (bi-unify t2-in t-out) + t (unify-output t1 t2) + t) + [_ [:join t1-out t2-out]] + (with-env env + t1 (bi-unify t-in t1-out) + t2 (bi-unify t-in t2-out) + t (unify-output t1 t2) + t) :else [nil env])) (defn with-var [n f env] (let [shadow (env n) - [t-f env] (f (assoc env n [:t-var])) + [t-f env] (f (assoc env n [:top])) t-n (env n)] [[t-n t-f] (if shadow (assoc env n shadow) (dissoc env n))])) @@ -90,9 +161,9 @@ [:rec n e] (with-env env [t-n t-e] (with-var n #(expr e %)) - t (unify t-n t-e) + t (unify-output t-n t-e) [:rec n t]) - [:cst c] [(cond (integer? c) [:t :int] + [:lit c] [(cond (integer? c) [:t :int] (or (true? c) (false? c)) [:t :bool]) env] [:var n] [(env n) env] @@ -103,11 +174,11 @@ [t-in t-out] (env-id (match t1 [:abs a b] [a b] :else nil)) - t (unify t-in t2) + _ (bi-unify t-in t2) t-out) [:struct m] (with-env env - t-m #((reduce (fn [[t-m env] [l e]] + t-m (#(reduce (fn [[t-m env] [l e]] (with-env env t (expr e) (assoc t-m l t))) [{} %] m)) diff --git a/test/psiml/type_test.clj b/test/psiml/type_test.clj index 402c492..46e8a07 100644 --- a/test/psiml/type_test.clj +++ b/test/psiml/type_test.clj @@ -5,30 +5,49 @@ (def t-int [:t :int]) (def t-bool [:t :bool]) -(deftest unify-basetypes - (is (= (unify t-int t-bool {}) [nil {}])) - (is (= (unify t-int t-int {}) [t-int {}]))) - -(deftest unify-struct - (is (= (unify [:struct {:i t-int :b t-bool}] - [:struct {:b t-bool :i t-int}] {}) - [[:struct {:i t-int :b t-bool}] {}])) - (is (= (unify [:struct {:i t-int :b t-bool}] - [:struct {:b t-int :i t-bool}] {}) - [nil {}])) - (is (= (unify [:struct {:i t-int :b t-bool}] - [:struct {:a t-bool :b t-bool :i t-int}] {}) - [nil {}]))) +(defn unifications? + [t1 t2 t-input t-output t-bi] + (or (= (unify-input t1 t2 {}) [t-input {}]) + (= (unify-output t1 t2 {}) [t-output {}]) + (= (bi-unify t1 t2 {}) [t-bi {}]))) + +(deftest bi-unify-basetypes + (is (unifications? t-int t-bool + [:meet t-int t-bool] + [:join t-int t-bool] + nil)) + (is (apply unifications? (repeat 5 t-int)))) + +(deftest bi-unify-struct + (is (apply unifications? + (repeat 5 [:struct {:i t-int :b t-bool}]))) + (is (unifications? [:struct {:i t-int :b t-bool}] + [:struct {:b t-int :i t-bool}] + [:struct {:i [:meet t-int t-bool] + :b [:meet t-bool t-int]}] + [:struct {:i [:join t-int t-bool] + :b [:join t-bool t-int]}] + nil)) + (is (unifications? [:struct {:i t-int :b t-bool}] + [:struct {:a t-bool :b t-bool :i t-int}] + [:struct {:a t-bool :i t-int :b t-bool}] + [:struct {:i t-int :b t-bool}] + [:struct {:i t-int :b t-bool}]))) + +(defn type? + [e t] + (= (expr e) [t {}])) (deftest expr-basetypes - (is (= (expr [:cst 1]) [t-int {}])) - (is (= (expr [:cst true]) [t-bool {}]))) + (is (type? [:lit 1] t-int)) + (is (type? [:lit true] t-bool))) + +(deftest expr-struct + (let [s [:struct {:a [:lit 1] :b [:lit true]}]] + (is (type? s [:struct {:a t-int :b t-bool}])) + (is (type? [:get :a s] t-int)))) (def id [:abs :x [:var :x]]) (deftest expr-id - (is (= (expr id) [[:abs [:t-var] [:t-var]] {}]))) - -;; (deftest expr-id-app -;; (is (= (expr [:app id [:var :y]] {:y [:t-var]}) -;; [[:t-var] {:y [:t-var]}]))) + (is (= (expr id) [[:abs [:top] [:top]] {}]))) From 5de692d2355c5e1502429ce220abd27e45bf930e Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Sun, 17 Dec 2017 20:57:12 +0100 Subject: [PATCH 08/13] Typing for select, using simple equality unification for variables --- src/psiml/type.cljc | 299 ++++++++++++++++++++++++++++----------- test/psiml/type_test.clj | 79 +++++++++-- 2 files changed, 284 insertions(+), 94 deletions(-) diff --git a/src/psiml/type.cljc b/src/psiml/type.cljc index 1ef5d3b..f29aa3c 100644 --- a/src/psiml/type.cljc +++ b/src/psiml/type.cljc @@ -3,23 +3,17 @@ #?(:cljs (:require-macros psiml.type)) (:require [clojure.core.match :refer [match]])) -;; typed ast {:node n :type t] -;; {:node [:abs :x {:node [:var :x] :type [:t-var]}] -;; :type [:abs [:t-var] [:t-var]]} +;; TODO: typed ast {:node n :type t} -;; [:t :int] -;; [:t :bool] -;; [:abs t t] -;; [:rec t] -;; {:struct {field -> e} +;; type environment: {:vars {name -> input type} +;; :bound-t-vars #{name}} -;; [:top] -;; [:bot] -;; [:meet t t] -;; [:join t t] +(defmacro trace + [sym env] + `(do (println ~(str sym) ~sym ~env) [~sym ~env])) (defn map-env - "Returns (f t env) if t is not nil, otherwise [t env]" + "Returns (f t env) if t is not nil, otherwise [t env]." [[t env] f] (if (nil? t) [t env] (f t env))) @@ -38,14 +32,107 @@ (fn [~b ~senv] (with-env ~senv ~@binds)))))) (defn env-id - "Returns `v` without affecting the environment" + "Returns v without affecting the environment." [v env] [v env]) -(declare unify-input) -(declare unify-output) +(defn env-only + "Applies f to the environment, returning a dummy value." + [f env] + [:ok (f env)]) -(defn unify-input +(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 t1 t2] [:meet (sub-in t1) (sub-in t2)] + :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 t1 t2] [:join (sub-out t1) (sub-out t2)] + :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 %)] + (update env :vars + #(->> % + (map (fn [[n' t']] [n' (sub-in t')])) + (into {}))))) + +(defn replace-var-t + "Replaces the type of the variable n with t, + simply removes the variable if t is nil. + Returns the replaced type." + [n t env] + (let [t-n ((:vars env) n)] + [t-n (update env :vars #(if t (assoc % n t) (dissoc % n)))])) + +(defn with-var + "Introduces a new local variable n for the scope of f. + The result is of the form [[t-n t-f] env]." + [n f env] + (let [shadow (env n)] + (with-env env + t-f (#(f (assoc-in % [:vars n] [:var (gensym n)]))) + t-n (replace-var-t n shadow) + [t-n t-f]))) + +(defn new-t-var + [p f env] + (let [n (gensym p)] + (f [:var n] env))) + +(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 a b] (collect [a b]) + [:join a b] (collect [a b]))))) + +(defn abstract-types ; TODO: polymorphism + "Abstracts free type variables of t" + [t env] + (let [nb (free-vars t (:bound-t-vars env))] + [(reduce (fn [t n] [:t-abs n t]) t nb) env])) + +(declare meet) +(declare join) + +(defn meet [t1 t2 env] (match [t1 t2] [[:top] t] [t env] @@ -58,7 +145,7 @@ (partial reduce (fn [[t-m env] [l t]] (if (contains? t-m l) (with-env env - t (unify-input (t-m l) t) + t (meet (t-m l) t) (assoc t-m l t)) [(assoc t-m l t) env]))) [{} %] @@ -66,16 +153,16 @@ [:struct t-m]) [[:abs t1-out t1-in] [:abs t2-out t2-in]] (with-env env - t-in (unify-input t1-in t2-in) - t-out (unify-output t1-out t2-out) + t-in (meet t1-in t2-in) + t-out (join t1-out t2-out) [:abs t-out t-in]) - [[:rec t1] [:rec t2]] - (with-env env - t (unify-input t1 t2) - [:rec t]) - :else [nil env])) + ;; [[:rec t1'] [:rec t2']] + ;; (with-env env + ;; t (meet t1' t2') + ;; [:rec t]) + :else [[:meet t1 t2] env])) -(defn unify-output +(defn join [t1 t2 env] (match [t1 t2] [[:bot] t] [t env] @@ -87,68 +174,71 @@ t-m (#(reduce (fn [[t-m env] [l t1]] (if-let [t2 (tm2 l)] (with-env env - t (unify-output t1 t2) + t (join t1 t2) (assoc t-m l t)) ([t-m env]))) [{} %] tm1)) [:struct t-m]) [[:abs t1-in t1-out] [:abs t2-in t2-out]] (with-env env - t-in (unify-input t1-in t2-in) - t-out (unify-output t1-out t2-out) + t-in (meet t1-in t2-in) + t-out (join t1-out t2-out) [:abs t-in t-out]) - [[:rec t1] [:rec t2]] - (with-env env - t (unify-output t1 t2) - [:rec t]) - :else [nil env])) + ;; [[:rec t1'] [:rec t2']] + ;; (with-env env + ;; t (unify-output t1' t2') + ;; [:rec t]) + :else [[:join t1 t2] env])) -(defn bi-unify - [t-in t-out env] - (match [t-in t-out] - [[:top] t] [t env] - [_ [:bot]] [[:bot] env] +(defn biunify + "Biunifies t-out with t-in in the given environment. + We want the output to flow in the input. + Returns [[t-out' t-in'] env]." + [t-out t-in env] + (match [t-out t-in] + [t [:top]] [[t [:top]] env] + [[:bot] t] [[[:bot] t] env] + [_ [:var n]] ; TODO + (with-env env + _ (env-only #(bisubstitute-env n t-out t-out %)) + [t-out t-out]) + [[:var n] _] ; TODO + (with-env env + _ (env-only #(bisubstitute-env n t-in t-in %)) + [t-in t-in]) [[:t a] [:t b]] - [(if (= a b) [:t a]) env] - [[:struct tm-in] [:struct tm-out]] + [(if (= a b) [[:t a] [:t b]]) env] + [[:struct tm-out] [:struct tm-in]] (with-env env - t-m (#(reduce (fn [[t-m env] [l t-in]] - (if-let [t-out (tm-out l)] - (with-env env - t (bi-unify t-in t-out) - (assoc t-m l t)) - [nil env])) - [{} %] + [mo mi] (#(reduce (fn [[ms env] [l t-in]] + (with-env env + [mo mi] (env-id ms) + t-out (env-id (tm-out l)) + [to ti] (biunify t-out t-in) + [(assoc mo l to) (assoc mi l ti)])) + [[{} {}] %] tm-in)) - [:struct t-m]) - [[:abs t-in-out t-in-in] [:abs t-out-in t-out-out]] + [[:struct mo] [:struct mi]]) + [[:abs t-out-in t-out-out] [:abs t-in-out t-in-in]] (with-env env - t-a (bi-unify t-out-in t-in-out) - t-b (bi-unify t-in-in t-out-out) - [:abs t-a t-b]) - [[:rec t-in] [:rec t-out]] - [nil env] ; TODO - [[:meet t1-in t2-in] _] + [tio toi] (biunify t-in-out t-out-in) + [too tii] (biunify t-out-out t-in-in) + [[:abs toi too] [:abs tio tii]]) + ;; [[:rec t-in] [:rec t-out]] [nil env] + [_ [:meet t1-in t2-in]] (with-env env - t1 (bi-unify t1-in t-out) - t2 (bi-unify t2-in t-out) - t (unify-output t1 t2) - t) - [_ [:join t1-out t2-out]] + [to t1i] (biunify t-out t1-in) + [to t2i] (biunify to t2-in) + ti (meet t1i t2i) + [to ti]) + [[:join t1-out t2-out] _] (with-env env - t1 (bi-unify t-in t1-out) - t2 (bi-unify t-in t2-out) - t (unify-output t1 t2) - t) + [t1o ti] (biunify t1-out t-in) + [t2o ti] (biunify t2-out ti) + to (join t1o t2o) + [to ti]) :else [nil env])) -(defn with-var - [n f env] - (let [shadow (env n) - [t-f env] (f (assoc env n [:top])) - t-n (env n)] - [[t-n t-f] (if shadow (assoc env n shadow) (dissoc env n))])) - (defn expr "Types an expression" ([e] (expr e {})) @@ -158,23 +248,24 @@ (with-env env [t-n t-e] (with-var n #(expr e %)) [:abs t-n t-e]) - [:rec n e] - (with-env env - [t-n t-e] (with-var n #(expr e %)) - t (unify-output t-n t-e) - [:rec n t]) + ;; [: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] [(env n) env] + [:var n] [((:vars env) n) env] [:app e1 e2] (with-env env t1 (expr e1) t2 (expr e2) - [t-in t-out] (env-id (match t1 - [:abs a b] [a b] - :else nil)) - _ (bi-unify t-in t2) + [t-abs _] (new-t-var + "app" + (fn [t? env] (biunify t1 [:abs t2 t?] env))) + t-out (env-id (match t-abs + [:abs _ t-out] t-out)) t-out) [:struct m] (with-env env @@ -186,4 +277,46 @@ [:get l e] (with-env env t (expr e) - (match t [:struct t-m] (t-m l) :else nil))))) + [t-s _] (new-t-var + "get" + (fn [t? env] (biunify t [:struct {l t?}] env))) + t-out (env-id (match t-s + [:struct {l t-out}] t-out)) + t-out) + [:if e-test e-then e-else] + (with-env env + t-test (expr e-test) + t-then (expr e-then) + t-else (expr e-else) + _ (biunify t-test [:t :bool]) + t (join t-then t-else) + t) + :else [nil env]))) + +(defn eq? + ([t1 t2] (eq? t1 t2 {})) + ([t1 t2 vars] + (match [t1 t2] + [[:top] [:top]] true + [[:bot] [:bot]] true + [[:t b1] [:t b2]] (= b1 b2) + [[:var n1] [:var n2]] (= (vars n1) n2) + [[:struct tm1] [:struct tm2]] + (and (= (into #{} (keys tm1)) (into #{} (keys tm2))) + (reduce (fn [acc [l t1]] + (and acc + (let [t2 (tm2 l)] (eq? t1 t2 vars)))) + true tm1)) + [[:abs a1 b1] [:abs a2 b2]] + (and (eq? a1 a2 vars) + (eq? b1 b2 vars)) + [[:t-abs n1 t1'] [:t-abs n2 t2']] + (eq? t1' t2' (assoc vars n1 n2)) + ;; [[:rec a1] [:rec a2]] (eq? [a1 env1] [a2 env2]) + [[:meet a1 b1] [:meet a2 b2]] + (and (eq? a1 a2 vars) + (eq? b1 b2 vars)) + [[:join a1 b1] [:join a2 b2]] + (and (eq? a1 a2 vars) + (eq? b1 b2 vars)) + :else false))) diff --git a/test/psiml/type_test.clj b/test/psiml/type_test.clj index 46e8a07..3a1880e 100644 --- a/test/psiml/type_test.clj +++ b/test/psiml/type_test.clj @@ -5,11 +5,19 @@ (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}))) + (defn unifications? [t1 t2 t-input t-output t-bi] - (or (= (unify-input t1 t2 {}) [t-input {}]) - (= (unify-output t1 t2 {}) [t-output {}]) - (= (bi-unify t1 t2 {}) [t-bi {}]))) + (or (= (meet t1 t2 {}) [t-input {}]) + (= (join t1 t2 {}) [t-output {}]) + (= (biunify t1 t2 {}) [t-bi {}]))) (deftest bi-unify-basetypes (is (unifications? t-int t-bool @@ -34,20 +42,69 @@ [:struct {:i t-int :b t-bool}] [:struct {:i t-int :b t-bool}]))) -(defn type? - [e t] - (= (expr e) [t {}])) +(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' env] (expr e {:vars vars :bound-t-vars #{}})] + (is (eq? (first (abstract-types t' env)) t))))) (deftest expr-basetypes - (is (type? [:lit 1] t-int)) - (is (type? [:lit true] t-bool))) + (is-typed? [:lit 1] t-int) + (is-typed? [:lit true] t-bool)) (deftest expr-struct (let [s [:struct {:a [:lit 1] :b [:lit true]}]] - (is (type? s [:struct {:a t-int :b t-bool}])) - (is (type? [:get :a s] t-int)))) + (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 (= (expr id) [[:abs [:top] [:top]] {}]))) + (is-typed? id [:t-abs :a [: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-int t-bool]]]] + {:int-id [:abs t-int t-int] + :bool-id [:abs t-bool t-bool]})) + +(deftest select + (is-typed? [:abs :p + [:abs :v + [:abs :d + [:if [:app [:var :p] [:var :v]] + [:var :v] + [:var :d]]]]] + [:t-abs :v + [:t-abs :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]]]]])) From b5d7806d568cd38d513c627f3bdd628d95b08604 Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Tue, 19 Dec 2017 20:37:27 +0100 Subject: [PATCH 09/13] Fix tests and improve type eq? --- src/psiml/type.cljc | 49 ++++++++++++++++++++-------------------- test/psiml/type_test.clj | 45 +++++++++++++++++++----------------- 2 files changed, 48 insertions(+), 46 deletions(-) diff --git a/src/psiml/type.cljc b/src/psiml/type.cljc index f29aa3c..d2e8de9 100644 --- a/src/psiml/type.cljc +++ b/src/psiml/type.cljc @@ -176,7 +176,7 @@ (with-env env t (join t1 t2) (assoc t-m l t)) - ([t-m env]))) + [t-m env])) [{} %] tm1)) [:struct t-m]) [[:abs t1-in t1-out] [:abs t2-in t2-out]] @@ -296,27 +296,26 @@ (defn eq? ([t1 t2] (eq? t1 t2 {})) ([t1 t2 vars] - (match [t1 t2] - [[:top] [:top]] true - [[:bot] [:bot]] true - [[:t b1] [:t b2]] (= b1 b2) - [[:var n1] [:var n2]] (= (vars n1) n2) - [[:struct tm1] [:struct tm2]] - (and (= (into #{} (keys tm1)) (into #{} (keys tm2))) - (reduce (fn [acc [l t1]] - (and acc - (let [t2 (tm2 l)] (eq? t1 t2 vars)))) - true tm1)) - [[:abs a1 b1] [:abs a2 b2]] - (and (eq? a1 a2 vars) - (eq? b1 b2 vars)) - [[:t-abs n1 t1'] [:t-abs n2 t2']] - (eq? t1' t2' (assoc vars n1 n2)) - ;; [[:rec a1] [:rec a2]] (eq? [a1 env1] [a2 env2]) - [[:meet a1 b1] [:meet a2 b2]] - (and (eq? a1 a2 vars) - (eq? b1 b2 vars)) - [[:join a1 b1] [:join a2 b2]] - (and (eq? a1 a2 vars) - (eq? b1 b2 vars)) - :else false))) + (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 a1 b1] [:meet a2 b2]] + (every-eq? [[a1 a2] [b1 b2]]) + [[:join a1 b1] [:join a2 b2]] + (every-eq? [[a1 a2] [b1 b2]]) + :else false)))) diff --git a/test/psiml/type_test.clj b/test/psiml/type_test.clj index 3a1880e..8aa243f 100644 --- a/test/psiml/type_test.clj +++ b/test/psiml/type_test.clj @@ -13,34 +13,37 @@ [:t-abs :x [:abs [:var :x] [:var :y]]] #{}) #{:y}))) -(defn unifications? +(defmacro unifications? [t1 t2 t-input t-output t-bi] - (or (= (meet t1 t2 {}) [t-input {}]) - (= (join t1 t2 {}) [t-output {}]) - (= (biunify t1 t2 {}) [t-bi {}]))) + `(do (is (= (meet ~t1 ~t2 {}) [~t-input {}])) + (is (= (join ~t1 ~t2 {}) [~t-output {}])) + (is (= (first (first (biunify ~t1 ~t2 {}))) ~t-bi)))) + +(defn unified? + [t] + (unifications? t t t t t)) (deftest bi-unify-basetypes - (is (unifications? t-int t-bool + (unifications? t-int t-bool [:meet t-int t-bool] [:join t-int t-bool] - nil)) - (is (apply unifications? (repeat 5 t-int)))) + nil) + (unified? t-int)) (deftest bi-unify-struct - (is (apply unifications? - (repeat 5 [:struct {:i t-int :b t-bool}]))) - (is (unifications? [:struct {:i t-int :b t-bool}] - [:struct {:b t-int :i t-bool}] - [:struct {:i [:meet t-int t-bool] - :b [:meet t-bool t-int]}] - [:struct {:i [:join t-int t-bool] - :b [:join t-bool t-int]}] - nil)) - (is (unifications? [:struct {:i t-int :b t-bool}] - [:struct {:a t-bool :b t-bool :i t-int}] - [:struct {:a t-bool :i t-int :b t-bool}] - [:struct {:i t-int :b t-bool}] - [:struct {:i t-int :b t-bool}]))) + (unified? [:struct {:i t-int :b t-bool}]) + (unifications? [:struct {:i t-int :b t-bool}] + [:struct {:b t-int :i t-bool}] + [:struct {:i [:meet t-int t-bool] + :b [:meet t-bool t-int]}] + [:struct {:i [:join t-int t-bool] + :b [:join t-bool t-int]}] + nil) + (unifications? [:struct {:a t-bool :b t-bool :i t-int}] + [:struct {:i t-int :b t-bool}] + [:struct {:a t-bool :i t-int :b t-bool}] + [:struct {:i t-int :b t-bool}] + [:struct {:i t-int :b t-bool}])) (deftest test-eq? (is (eq? [:t-abs :a [:var :a]] From 335cb5ce6aec468fdaf6b780156f73baf1e2f129 Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Wed, 20 Dec 2017 15:24:00 +0100 Subject: [PATCH 10/13] More parsing, multiple arguments and stuff --- src/psiml/core.cljc | 18 ++-------------- src/psiml/parse.cljc | 36 ++++++++++++++++++++++++-------- test/psiml/parse_test.clj | 44 ++++++++++++++++++++++++++------------- 3 files changed, 58 insertions(+), 40 deletions(-) diff --git a/src/psiml/core.cljc b/src/psiml/core.cljc index a422794..931f6a7 100644 --- a/src/psiml/core.cljc +++ b/src/psiml/core.cljc @@ -23,24 +23,10 @@ [:get l e'])) expr))) -;; 1 --> [:t :int] -;; true --> [:t :bool] -;; (fn [n1 n2] e) --> [:abs n1 [:abs n2 r(e)]] -;; {:l1 e1 :l2 e2} --> [:struct {:l1 r(e1) :l2 r(e2)}] -;; (:l e) --> [:get l r(e)] -;; (let [n e1] e2) --> [:app [:abs n r(e2)] [:rec n r(e1)]] -;; (e1 e2) --> [:app r(e1) r(e2)] - (defn -main "I don't do a whole lot ... yet." [& args] - (let [e (p/string "(fn [n1] true)")] - (println e)) - (let [e1 (p/string "{:a 1 :b 1}")] - (println e1)) - (let [e2 (p/string "(:l 5)")] - (println e2)) - (let [e3 (p/string "(fn [label] {:label true})")] - (println e3))) + (let [e (p/string "(fn [n1 n2] true)")] + (println e))) #?(:cljs (-main)) diff --git a/src/psiml/parse.cljc b/src/psiml/parse.cljc index 34114d7..5aa58d1 100644 --- a/src/psiml/parse.cljc +++ b/src/psiml/parse.cljc @@ -1,5 +1,12 @@ (ns psiml.parse - "Parses concrete syntax, producing abstract syntax" + "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 @@ -8,17 +15,28 @@ (defn data "Parses concrete syntax from data" [d] - (cond - (seq? d) - (match d - (['fn [a] b] :seq) + (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 (name a) (data b)])) - (or (integer? d) (true? d) (false? d)) - [:lit d] + (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]](conj m {l (data v)})) {} d)])) + [:struct (reduce (fn [m [l v]] (assoc m l (data v))) {} d)])) (defn string "Parses concrete syntax from a string" diff --git a/test/psiml/parse_test.clj b/test/psiml/parse_test.clj index 7f0a58a..ff88e9f 100644 --- a/test/psiml/parse_test.clj +++ b/test/psiml/parse_test.clj @@ -4,18 +4,32 @@ [psiml.parse :refer :all])) (deftest parse-expr-simple - (testing "Parse an int" - (let [e "7" - r [:lit 7]] - (is (= (string e) r)))) - (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 "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))))) From 101df320e3231b30700978388a90d45a6f761e84 Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Fri, 12 Jan 2018 18:25:28 +0100 Subject: [PATCH 11/13] Rework biunification --- src/psiml/type.cljc | 128 +++++++++++++++++++-------------------- test/psiml/type_test.clj | 78 +++++++++++++----------- 2 files changed, 105 insertions(+), 101 deletions(-) diff --git a/src/psiml/type.cljc b/src/psiml/type.cljc index d2e8de9..9f5adc3 100644 --- a/src/psiml/type.cljc +++ b/src/psiml/type.cljc @@ -84,6 +84,13 @@ (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))) + (defn replace-var-t "Replaces the type of the variable n with t, simply removes the variable if t is nil. @@ -103,9 +110,8 @@ [t-n t-f]))) (defn new-t-var - [p f env] - (let [n (gensym p)] - (f [:var n] env))) + [p env] + [[:var (gensym p)] env]) (defn free-vars ([t bound] (free-vars t bound #{})) @@ -121,7 +127,8 @@ [:abs a b] (collect [a b]) [:t-abs n t'] (free-vars t' (conj bound n) res) [:meet a b] (collect [a b]) - [:join a b] (collect [a b]))))) + [:join a b] (collect [a b]) + :else res)))) (defn abstract-types ; TODO: polymorphism "Abstracts free type variables of t" @@ -191,53 +198,45 @@ :else [[:join t1 t2] env])) (defn biunify - "Biunifies t-out with t-in in the given environment. - We want the output to flow in the input. - Returns [[t-out' t-in'] env]." - [t-out t-in env] - (match [t-out t-in] - [t [:top]] [[t [:top]] env] - [[:bot] t] [[[:bot] t] env] - [_ [:var n]] ; TODO - (with-env env - _ (env-only #(bisubstitute-env n t-out t-out %)) - [t-out t-out]) - [[:var n] _] ; TODO - (with-env env - _ (env-only #(bisubstitute-env n t-in t-in %)) - [t-in t-in]) - [[:t a] [:t b]] - [(if (= a b) [[:t a] [:t b]]) env] - [[:struct tm-out] [:struct tm-in]] - (with-env env - [mo mi] (#(reduce (fn [[ms env] [l t-in]] - (with-env env - [mo mi] (env-id ms) - t-out (env-id (tm-out l)) - [to ti] (biunify t-out t-in) - [(assoc mo l to) (assoc mi l ti)])) - [[{} {}] %] - tm-in)) - [[:struct mo] [:struct mi]]) - [[:abs t-out-in t-out-out] [:abs t-in-out t-in-in]] - (with-env env - [tio toi] (biunify t-in-out t-out-in) - [too tii] (biunify t-out-out t-in-in) - [[:abs toi too] [:abs tio tii]]) - ;; [[:rec t-in] [:rec t-out]] [nil env] - [_ [:meet t1-in t2-in]] - (with-env env - [to t1i] (biunify t-out t1-in) - [to t2i] (biunify to t2-in) - ti (meet t1i t2i) - [to ti]) - [[:join t1-out t2-out] _] - (with-env env - [t1o ti] (biunify t1-out t-in) - [t2o ti] (biunify t2-out ti) - to (join t1o t2o) - [to ti]) - :else [nil env])) + "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 env] (meet [:var a] t-in env) + 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 env] (join [:var a] t-out env) + 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 t1 t2]] + [(into cs [[t-out t1] [t-out t2]]) t env] + [[:join t1 t2] _] + [(into cs [[t1 t-in] [t2 t-in]]) 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 expr "Types an expression" @@ -261,12 +260,9 @@ (with-env env t1 (expr e1) t2 (expr e2) - [t-abs _] (new-t-var - "app" - (fn [t? env] (biunify t1 [:abs t2 t?] env))) - t-out (env-id (match t-abs - [:abs _ t-out] t-out)) - t-out) + t? (new-t-var "app") + t? (biunify [[t1 [:abs t2 t?]]] t?) + t?) [:struct m] (with-env env t-m (#(reduce (fn [[t-m env] [l e]] @@ -277,20 +273,20 @@ [:get l e] (with-env env t (expr e) - [t-s _] (new-t-var - "get" - (fn [t? env] (biunify t [:struct {l t?}] env))) - t-out (env-id (match t-s - [:struct {l t-out}] t-out)) - t-out) + t? (new-t-var "get") + t? (biunify [[t [:struct {l t?}]]] t?) + t?) [:if e-test e-then e-else] (with-env env t-test (expr e-test) t-then (expr e-then) t-else (expr e-else) - _ (biunify t-test [:t :bool]) - t (join t-then t-else) - t) + t? (new-t-var "if") + t? (biunify [[t-test [:t :bool]] + [t-then t?] + [t-else t?]] + t?) + t?) :else [nil env]))) (defn eq? diff --git a/test/psiml/type_test.clj b/test/psiml/type_test.clj index 8aa243f..fcb7608 100644 --- a/test/psiml/type_test.clj +++ b/test/psiml/type_test.clj @@ -13,37 +13,47 @@ [:t-abs :x [:abs [:var :x] [:var :y]]] #{}) #{:y}))) -(defmacro unifications? - [t1 t2 t-input t-output t-bi] - `(do (is (= (meet ~t1 ~t2 {}) [~t-input {}])) - (is (= (join ~t1 ~t2 {}) [~t-output {}])) - (is (= (first (first (biunify ~t1 ~t2 {}))) ~t-bi)))) - -(defn unified? - [t] - (unifications? t t t t t)) - -(deftest bi-unify-basetypes - (unifications? t-int t-bool - [:meet t-int t-bool] - [:join t-int t-bool] - nil) - (unified? t-int)) - -(deftest bi-unify-struct - (unified? [:struct {:i t-int :b t-bool}]) - (unifications? [:struct {:i t-int :b t-bool}] - [:struct {:b t-int :i t-bool}] - [:struct {:i [:meet t-int t-bool] - :b [:meet t-bool t-int]}] - [:struct {:i [:join t-int t-bool] - :b [:join t-bool t-int]}] - nil) - (unifications? [:struct {:a t-bool :b t-bool :i t-int}] - [:struct {:i t-int :b t-bool}] - [:struct {:a t-bool :i t-int :b t-bool}] - [:struct {:i t-int :b t-bool}] - [:struct {:i t-int :b t-bool}])) +(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 (= (first (meet a b {})) r))) + +(deftest test-meet + (is-meet? t-int t-int t-int) + (is-meet? t-int t-bool [:meet t-int t-bool]) + (is-meet? s-iibb s-iibb s-iibb) + (is-meet? s-iibb s-ibbi + [:struct {:i [:meet t-int t-bool] + :b [:meet t-bool t-int]}]) + (is-meet? s-abiibb s-iibb s-abiibb)) + +(defn is-join? + [a b r] + (is (= (first (join a b {})) r))) + +(deftest test-join + (is-join? t-int t-int t-int) + (is-join? t-int t-bool [:join t-int t-bool]) + (is-join? s-iibb s-iibb s-iibb) + (is-join? s-iibb s-ibbi + [:struct {:i [:join t-int t-bool] + :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]] @@ -55,11 +65,9 @@ (let [[t' env] (expr e {:vars vars :bound-t-vars #{}})] (is (eq? (first (abstract-types t' env)) t))))) -(deftest expr-basetypes +(deftest test-expr (is-typed? [:lit 1] t-int) - (is-typed? [:lit true] t-bool)) - -(deftest expr-struct + (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))) From 0dc0064be6f81548e18196d4c6dee4a4e5936ba6 Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Sat, 13 Jan 2018 16:38:40 +0100 Subject: [PATCH 12/13] Type simplification, printing and isolated environments --- src/psiml/print.cljc | 52 ++++++ src/psiml/type.cljc | 341 ++++++++++++++++++--------------------- src/psiml/util.cljc | 23 +++ test/psiml/type_test.clj | 30 ++-- 4 files changed, 247 insertions(+), 199 deletions(-) create mode 100644 src/psiml/print.cljc 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 index 9f5adc3..d1cc695 100644 --- a/src/psiml/type.cljc +++ b/src/psiml/type.cljc @@ -1,45 +1,18 @@ (ns psiml.type "Types abstract syntax, producing typed abstract syntax" #?(:cljs (:require-macros psiml.type)) - (:require [clojure.core.match :refer [match]])) + (: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: {:vars {name -> input type} -;; :bound-t-vars #{name}} +;; type environment: {name -> input type} -(defmacro trace - [sym env] - `(do (println ~(str sym) ~sym ~env) [~sym ~env])) - -(defn map-env - "Returns (f t env) if t is not nil, otherwise [t env]." - [[t env] f] - (if (nil? t) [t env] (f t env))) - -(defmacro with-env - "Passes an environment through a series of operations, - binding the results and returning a final value. - - The operations are given the environment as an additional - argument and should return a value of the form [result new-env]. - The binding itself is done using map-env, thus aborting the - series of operations after an error." - ([env r] `[~r ~env]) - ([env b f & binds] - (let [senv (if (symbol? env) env (gensym))] - `(map-env (->> ~env ~f) - (fn [~b ~senv] (with-env ~senv ~@binds)))))) - -(defn env-id - "Returns v without affecting the environment." - [v env] - [v env]) - -(defn env-only - "Applies f to the environment, returning a dummy value." - [f env] - [:ok (f env)]) +(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) @@ -56,7 +29,7 @@ [: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 t1 t2] [:meet (sub-in t1) (sub-in t2)] + [:meet & ts] (into [:meet] (map sub-in ts)) :else t))) (defn bisubstitute-output @@ -71,7 +44,7 @@ [: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 t1 t2] [:join (sub-out t1) (sub-out t2)] + [:join & ts] (into [:join] (map sub-out ts)) :else t))) (defn bisubstitute-env @@ -79,10 +52,9 @@ output occurences with t-out in the environment." [n t-in t-out env] (let [sub-in #(bisubstitute-input n t-in t-out %)] - (update env :vars - #(->> % - (map (fn [[n' t']] [n' (sub-in t')])) - (into {}))))) + (->> env + (map (fn [[n' t']] [n' (sub-in t')])) + (into {})))) (defn bisubstitute-constraints [n t-in t-out constraints] @@ -91,27 +63,12 @@ (bisubstitute-input n t-in t-out ti)]) constraints))) -(defn replace-var-t - "Replaces the type of the variable n with t, - simply removes the variable if t is nil. - Returns the replaced type." - [n t env] - (let [t-n ((:vars env) n)] - [t-n (update env :vars #(if t (assoc % n t) (dissoc % n)))])) +(assoc-in {:x {:y 1}} [:x :y] 2) -(defn with-var - "Introduces a new local variable n for the scope of f. - The result is of the form [[t-n t-f] env]." - [n f env] - (let [shadow (env n)] - (with-env env - t-f (#(f (assoc-in % [:vars n] [:var (gensym n)]))) - t-n (replace-var-t n shadow) - [t-n t-f]))) - -(defn new-t-var - [p env] - [[:var (gensym p)] env]) +(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 #{})) @@ -121,81 +78,91 @@ (match t [:top] res [:bot] res - [:t _] 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 a b] (collect [a b]) - [:join a b] (collect [a b]) + [:meet & ts] (collect ts) + [:join & ts] (collect ts) :else res)))) -(defn abstract-types ; TODO: polymorphism - "Abstracts free type variables of t" - [t env] - (let [nb (free-vars t (:bound-t-vars env))] - [(reduce (fn [t n] [:t-abs n t]) t nb) env])) +(declare simplify-input) +(declare simplify-output) -(declare meet) -(declare join) +(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))])]) + not-var (concat basic abs struct)] + ;; FIXME: + ;; (or (merge-kw :meet (or (not-empty not-var) var)) [:top])) + (or (merge-kw :meet (concat not-var var)) [:top])) + :else t)) -(defn meet - [t1 t2 env] - (match [t1 t2] - [[:top] t] [t env] - [t [:top]] [t env] - [[:t b1] [:t b2]] - [(if (= b1 b2) [:t b1] [:meet [:t b1] [:t b2]]) env] - [[:struct tm1] [:struct tm2]] - (with-env env - t-m (#(reduce - (partial reduce (fn [[t-m env] [l t]] - (if (contains? t-m l) - (with-env env - t (meet (t-m l) t) - (assoc t-m l t)) - [(assoc t-m l t) env]))) - [{} %] - [tm1 tm2])) - [:struct t-m]) - [[:abs t1-out t1-in] [:abs t2-out t2-in]] - (with-env env - t-in (meet t1-in t2-in) - t-out (join t1-out t2-out) - [:abs t-out t-in]) - ;; [[:rec t1'] [:rec t2']] - ;; (with-env env - ;; t (meet t1' t2') - ;; [:rec t]) - :else [[:meet t1 t2] env])) +(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))])])) + not-var (concat basic abs struct)] + ;; FIXME + ;; (or (merge-kw :join (or (not-empty not-var) var)) [:bot])) + (or (merge-kw :join (concat not-var var)) [:bot])) + :else t)) -(defn join - [t1 t2 env] - (match [t1 t2] - [[:bot] t] [t env] - [t [:bot]] [t env] - [[:t b1] [:t b2]] - [(if (= b1 b2) [:t b1] [:join [:t b1] [:t b2]]) env] - [[:struct tm1] [:struct tm2]] - (with-env env - t-m (#(reduce (fn [[t-m env] [l t1]] - (if-let [t2 (tm2 l)] - (with-env env - t (join t1 t2) - (assoc t-m l t)) - [t-m env])) - [{} %] tm1)) - [:struct t-m]) - [[:abs t1-in t1-out] [:abs t2-in t2-out]] - (with-env env - t-in (meet t1-in t2-in) - t-out (join t1-out t2-out) - [:abs t-in t-out]) - ;; [[:rec t1'] [:rec t2']] - ;; (with-env env - ;; t (unify-output t1' t2') - ;; [:rec t]) - :else [[:join t1 t2] env])) +(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. @@ -212,21 +179,21 @@ (if (= a b) [cs t env] [[] nil env]) ;; TODO [[:var a] [:var a]] (recur cs t env) [[:var a] _] - (let [[t-in env] (meet [:var a] t-in env) + (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 env] (join [:var a] t-out env) + (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 t1 t2]] - [(into cs [[t-out t1] [t-out t2]]) t env] - [[:join t1 t2] _] - [(into cs [[t1 t-in] [t2 t-in]]) 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) @@ -238,56 +205,64 @@ (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] - (match exp - [:abs n e] - (with-env env - [t-n t-e] (with-var n #(expr e %)) - [:abs t-n t-e]) - ;; [: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] [((:vars env) n) env] - [:app e1 e2] - (with-env env - t1 (expr e1) - t2 (expr e2) - t? (new-t-var "app") - t? (biunify [[t1 [:abs t2 t?]]] t?) - t?) - [:struct m] - (with-env env - t-m (#(reduce (fn [[t-m env] [l e]] - (with-env env - t (expr e) - (assoc t-m l t))) [{} %] m)) - [:struct t-m]) - [:get l e] - (with-env env - t (expr e) - t? (new-t-var "get") - t? (biunify [[t [:struct {l t?}]]] t?) - t?) - [:if e-test e-then e-else] - (with-env env - t-test (expr e-test) - t-then (expr e-then) - t-else (expr e-else) - t? (new-t-var "if") - t? (biunify [[t-test [:t :bool]] - [t-then t?] - [t-else t?]] - t?) - t?) - :else [nil 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 {})) @@ -310,8 +285,8 @@ [[:t-abs n1 t1'] [:t-abs n2 t2']] (eq? t1' t2') ;; [[:rec a1] [:rec a2]] (eq? [a1 env1] [a2 env2]) - [[:meet a1 b1] [:meet a2 b2]] - (every-eq? [[a1 a2] [b1 b2]]) - [[:join a1 b1] [:join a2 b2]] - (every-eq? [[a1 a2] [b1 b2]]) + [[: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 index 3fa747d..9d7b9d4 100644 --- a/src/psiml/util.cljc +++ b/src/psiml/util.cljc @@ -18,3 +18,26 @@ (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/type_test.clj b/test/psiml/type_test.clj index fcb7608..62aa7d6 100644 --- a/test/psiml/type_test.clj +++ b/test/psiml/type_test.clj @@ -19,27 +19,27 @@ (defn is-meet? [a b r] - (is (= (first (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-int t-bool]) + (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-int t-bool] + [: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 (= (first (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-int t-bool]) + (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-int t-bool] + [:struct {:i [:join t-bool t-int] :b [:join t-bool t-int]}]) (is-join? s-abiibb s-iibb s-iibb)) @@ -62,8 +62,8 @@ (defn is-typed? ([e t] (is-typed? e t {})) ([e t vars] - (let [[t' env] (expr e {:vars vars :bound-t-vars #{}})] - (is (eq? (first (abstract-types t' env)) t))))) + (let [[t' _] (expr e vars)] + (is (eq? t' t))))) (deftest test-expr (is-typed? [:lit 1] t-int) @@ -75,7 +75,7 @@ (def id [:abs :x [:var :x]]) (deftest expr-id - (is-typed? id [:t-abs :a [:abs [:var :a] [:var :a]]])) + (is-typed? id [:abs [:var :a] [:var :a]])) (deftest select-int-bool (is-typed? [:abs :p @@ -87,7 +87,7 @@ [:abs [:abs t-int t-bool] [:abs t-int [:abs t-bool - [:join t-int t-bool]]]] + [:join t-bool t-int]]]] {:int-id [:abs t-int t-int] :bool-id [:abs t-bool t-bool]})) @@ -98,12 +98,10 @@ [:if [:app [:var :p] [:var :v]] [:var :v] [:var :d]]]]] - [:t-abs :v - [:t-abs :d - [:abs [:abs [:var :v] t-bool] - [:abs [:var :v] - [:abs [:var :d] - [:join [: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 From 3e4ac62eb4e973942e29c4dca1ae5ec6cf33e60a Mon Sep 17 00:00:00 2001 From: Thomas Koehler Date: Thu, 8 Feb 2018 21:56:30 +0100 Subject: [PATCH 13/13] Intermediate tests --- src/psiml/type.cljc | 15 +++++---------- test/psiml/type_test.clj | 8 ++++++++ 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/src/psiml/type.cljc b/src/psiml/type.cljc index d1cc695..a585529 100644 --- a/src/psiml/type.cljc +++ b/src/psiml/type.cljc @@ -87,6 +87,7 @@ [:join & ts] (collect ts) :else res)))) +;; FIXME: simplification (declare simplify-input) (declare simplify-output) @@ -113,11 +114,8 @@ [:struct (apply merge-with (fn [a b] [:meet a b]) - (map (fn [[_ m]] m) ss))])]) - not-var (concat basic abs struct)] - ;; FIXME: - ;; (or (merge-kw :meet (or (not-empty not-var) var)) [:top])) - (or (merge-kw :meet (concat not-var var)) [:top])) + (map (fn [[_ m]] m) ss))])])] + (or (merge-kw :meet (concat var basic abs struct)) [:top])) :else t)) (defn simplify-output @@ -150,11 +148,8 @@ (filter (fn [[l _]] (ls l)) %)) - ms))])])) - not-var (concat basic abs struct)] - ;; FIXME - ;; (or (merge-kw :join (or (not-empty not-var) var)) [:bot])) - (or (merge-kw :join (concat not-var var)) [:bot])) + ms))])]))] + (or (merge-kw :join (concat var basic abs struct)) [:bot])) :else t)) (defn simplify diff --git a/test/psiml/type_test.clj b/test/psiml/type_test.clj index 62aa7d6..f913e4d 100644 --- a/test/psiml/type_test.clj +++ b/test/psiml/type_test.clj @@ -91,6 +91,14 @@ {: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