From 1b8d487e25101f5dd3c32ecb8ae5abf71e5c613b Mon Sep 17 00:00:00 2001
From: Jeremy Penner <jeremy@sporktania.com>
Date: Sat, 15 Jun 2024 18:44:36 -0400
Subject: [PATCH] babby's first typechecker

---
 src/main/tock/experiment.cljs | 97 +++++++++++++++++++++++++++++++++--
 1 file changed, 93 insertions(+), 4 deletions(-)

diff --git a/src/main/tock/experiment.cljs b/src/main/tock/experiment.cljs
index 73e292d..742d38c 100644
--- a/src/main/tock/experiment.cljs
+++ b/src/main/tock/experiment.cljs
@@ -5,7 +5,96 @@
             [helins.binf :as binf]
             [helins.binf.string :as binf.string]
             ;; [malli.core :as malli]
-            [malli.util]))
+            [malli.util]
+            [meander.epsilon :as m]
+            [clojure.pprint :as pp]))
+
+(defn compile-error [term message]
+  ; todo: extract location of error term
+  (js/Error. [term message]))
+
+; typechecking pass: rewrite expressions with type decorations, depth-first.
+; I can't think of any reason this shouldn't work fine, as long as we require
+; functions to have explicit type annotations
+
+; first task: decorate types for (if (= 1 2) 3 4)
+; ^i64 (if ^bool (= ^i64 (lit 1) ^i64 (lit 2)) ^i64 (lit 3) ^i64 (lit 4))
+
+(defn expr-type [expr] (:type (meta expr)))
+(defn assoc-type [expr symbol] (with-meta expr (assoc (meta expr) :type symbol)))
+(defn make-type [symbol] (fn [expr] (assoc-type expr symbol)))
+
+(def void (make-type 'void))
+(def i64 (make-type 'i64))
+(def bool (make-type 'bool))
+
+(defn coerce [expr typesym error]
+  (let [ltype (expr-type expr)]
+    (cond (= ltype typesym) expr
+          (= typesym 'void) (void `(cast ~expr))
+          :else (throw error))))
+
+(defn unify [lexpr rexpr error]
+  (let [ltype (expr-type lexpr)
+        rtype (expr-type rexpr)]
+    (cond (= ltype rtype) [lexpr rexpr]
+          (nil? error)    [(coerce lexpr 'void nil) (coerce rexpr 'void nil)]
+          :else (throw error))))
+
+(defn form-dispatch [form]
+  (if (list? form) (first form) `lit))
+
+(defmulti map-subexpressions (fn [form f] (form-dispatch form)))
+(defmethod map-subexpressions :default [form f]
+  (apply list (first form) (map f (rest form))))
+(defmethod map-subexpressions `lit [form f] form)
+
+(defmulti decorate-type (fn [form ctx] (form-dispatch form)))
+(defmethod decorate-type `if [form ctx]
+  (m/match form
+    (_ ?test ?when-true ?when-false)
+    (let [test-expr (coerce ?test 'bool (compile-error ?test "Condition must be a boolean expression"))
+          [true-expr false-expr] (unify ?when-true ?when-false nil)
+          type (expr-type true-expr)]
+      (assoc-type `(if ~test-expr ~true-expr ~false-expr) type))))
+
+(defmethod decorate-type `= [form ctx]
+  (m/match form
+    (_ ?left ?right)
+    (let [[left-expr right-expr] (unify ?left ?right (compile-error ?left "Cannot compare incompatible types"))]
+      (bool `(= ~left-expr ~right-expr)))))
+
+(defmethod decorate-type `lit [form ctx]
+  (cond (integer? form) (i64 `(lit ~form))
+        (boolean? form) (bool `(lit ~form))
+        :else           (throw (compile-error form "Not a valid literal"))))
+
+(defmulti typecheck-expr (fn [form ctx] (form-dispatch form)))
+(defmethod typecheck-expr :default [form ctx]
+  (decorate-type (map-subexpressions form #(typecheck-expr % ctx)) ctx))
+
+(binding [*print-meta* true] 
+  (pr (typecheck-expr `(if 3 3 true) nil)))
+
+; first task: compile (+ 1 2)
+; expected output: 
+; {:pretype []
+;  :posttype [:i64]
+;  :ops [[op/i64-const 1] [op/i64-const 2] [op/i64-add]]}
+
+; possible intermediate output:
+; {:pretype []
+;  :posttype [:i64]
+;  :subexprs [
+;    {:pretype [] :posttype [:i64] :ops [[op/i64-const 1]]}
+;    {:pretype [] :posttype [:i64] :ops [[op/i64-const 2]]}
+;    {:pretype [:i64 :i64] :posttype [:i64] :ops [[op/i64-add]]}
+;  ]}
+
+;; ; https://github.com/kalai-transpiler/kalai
+;; (defn compile-expr [expr scope expected-type]
+;;   (m/match expr
+;;     (+ ?l ?r)))
 
 (def test-wasm
   (-> (wasm/ctx)
@@ -22,9 +111,9 @@
                 (wasm/decompile v)))))
 
 (defn instantiate-wasm [wasm importObject]
-   (-> (wasm/compile wasm)
-       (binf/backing-buffer)
-       (js/WebAssembly.instantiate importObject)))
+  (-> (wasm/compile wasm)
+      (binf/backing-buffer)
+      (js/WebAssembly.instantiate importObject)))
 
 #_{:clj-kondo/ignore [:clojure-lsp/unused-public-var]}
 (defn main []