From 4432a2c44d76e70258f4b1d38114745726ffd1fc Mon Sep 17 00:00:00 2001
From: Luke Lau <luke.lau@intel.com>
Date: Wed, 17 Jul 2019 15:07:58 +0100
Subject: [PATCH] Start typechecker

---
 typecheck.scm | 126 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 126 insertions(+)
 create mode 100644 typecheck.scm

diff --git a/typecheck.scm b/typecheck.scm
new file mode 100644
index 0000000..a396a24
--- /dev/null
+++ b/typecheck.scm
@@ -0,0 +1,126 @@
+(define (is-app? x)
+  (and (list? x) (not (eq? (car x) 'lambda))))
+
+
+(define (is-lambda? x)
+  (and (list? x) (eq? (car x) 'lambda)))
+
+(define lambda-arg cadr)
+(define lambda-body caddr)
+
+; ('a, ('b, 'a))
+(define (env-lookup env x)
+  (if (null? env) (error #f "empty env")			; it's a type equality
+      (if (eq? (caar env) x)
+	  (cdar env)
+	  (env-lookup (cdr env) x))))
+
+(define abs-arg cadr)
+
+(define cur-tvar 0)
+(define (fresh-tvar)
+  (begin
+    (set! cur-tvar (+ cur-tvar 1))
+    (string->symbol
+     (string-append "t" (number->string (- cur-tvar 1))))))
+
+(define (typecheck env x)
+  (display "typechecking:\n\t")
+  (display x)
+  (display "\t")
+  (display env)
+  (display "\n")
+  (let
+      ((res
+	(cond
+	 ((integer? x) (list '() 'int))
+	 ((boolean? x) (list '() 'bool))
+	 ((eq? x 'inc) (list '() '(abs int int)))
+	 ((symbol? x) (list '() (env-lookup env x)))
+
+	 ((is-lambda? x)
+	  (let* ((new-env (cons (cons (lambda-arg x) (fresh-tvar)) env))
+		 (body-type-res (typecheck new-env (lambda-body x)))
+		 (subd-env (substitute (car body-type-res) new-env)))
+	    (display "lambda: ")
+	    (display body-type-res)
+	    (display "\n")
+	    (list (car body-type-res)
+	          (list 'abs
+			(env-lookup subd-env (lambda-arg x))
+			(cadr body-type-res)))))
+	 
+	 ((is-app? x) ; (f a)
+	  (let* ((arg-type-res (typecheck env (cadr x)))
+					; typecheck f with the knowledge that f : a -> x
+		 (func-type-res (typecheck env (car x)))
+		 (func-type (cadr func-type-res))
+		 (c (unify func-type
+			   (list 'abs
+				 (cadr arg-type-res)
+				 (fresh-tvar)))) 
+		 (new-env (substitute c env))
+		 (resolved-func-type (env-lookup new-env (car x))))
+	    (display "is-app:\n")
+	    (display c)
+	    (display "\n")
+	    (display new-env)
+	    (display "\n")
+	    (display resolved-func-type)
+	    (display "\n")
+	    (display arg-type-res)
+	    (display "\n")
+	    (if (abs? resolved-func-type)
+		(list (append c
+			      (unify (cadr arg-type-res)
+				     (cadr resolved-func-type)))
+		      (caddr resolved-func-type))
+		(error #f "wah")))))))
+    (display "result of ")
+    (display x)
+    (display ":\n\t")
+    (display (cadr res))
+    (display "[")
+    (display (car res))
+    (display "]\n")
+    res))
+
+
+(define (abs? t)
+  (and (list? t) (eq? (car t) 'abs)))
+
+(define (tvar? t)
+  (and (not (list? t)) (not (concrete? t)) (symbol? t)))
+
+(define (concrete? t)
+  (case t
+    ('int #t)
+    ('bool #t)
+    (else #f)))
+
+					; returns a list of pairs of constraints
+(define (unify a b)
+  (cond ((eq? a b) '())
+	((or (tvar? a) (tvar? b)) (list (cons a b)))
+	((and (abs? a) (abs? b))
+	 (append (unify (cadr a) (cadr b))
+		 (unify (caddr a) (caddr b))))
+	(else (error #f "could not unify"))))
+
+					; takes a list of constraints and a type environment, and makes it work
+(define (substitute c env)
+  (let ((go (lambda (x) (let ((tv (cdr x))
+			      (n (car x)))
+			  ;; (display tv)
+			  ;; (display "\n")
+			  ;; (display n)
+			  (cons n (fold-left
+				   (lambda (a y)
+				     ;; (display y)
+				     ;; (display ":")
+				     ;; (display a)
+				     (cond ((eq? a (car y)) (cdr y))
+					   ((eq? a (cdr y)) (car y))
+					   (else a)))
+				   tv c))))))
+  (map go env)))
-- 
2.30.2