(load "ast.scm")
+
+(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)))
+
+(define (pretty-type t)
+ (cond ((abs? t)
+ (string-append
+ (if (abs? (cadr t))
+ (string-append "(" (pretty-type (cadr t)) ")")
+ (pretty-type (cadr t)))
+ " -> "
+ (pretty-type (caddr t))))
+ (else (symbol->string t))))
+
; ('a, ('b, 'a))
(define (env-lookup env n)
(if (null? env) (error #f "empty env") ; it's a type equality
(list 'lambda (lambda-args prog) (normalize (caddr prog)))))
((app? prog)
(if (null? (cddr prog))
- (cons (normalize (car prog)) (normalize (cdr prog))) ; (f a)
- (list (list (normalize (car prog)) (normalize (cadr prog))) (normalize (caddr prog))))) ; (f a b)
+ `(,(normalize (car prog)) ,(normalize (cadr prog))) ; (f a)
+ `(,(list (normalize (car prog)) (normalize (cadr prog)))
+ ,(normalize (caddr prog))))) ; (f a b)
+ ;; (list (list (normalize (car prog))
+ ;; (normalize (cadr prog))) (normalize (caddr prog))))) ; (f a b)
((let? prog)
(append (list 'let
- (map (lambda (x) (cons (car x) (normalize (cdr x))))
+ (map (lambda (x) `(,(car x) ,(normalize (cadr x))))
(let-bindings prog)))
(map normalize (let-body prog))))
(else prog)))
+(define (builtin-type x)
+ (case x
+ ('+ '(abs int (abs int int)))
+ ('- '(abs int (abs int int)))
+ ('* '(abs int (abs int int)))
+ ('! '(abs bool bool))
+ ('bool->int '(abs bool int))
+ (else #f)))
; we typecheck the lambda calculus only (only single arg lambdas)
(define (typecheck prog)
(cond
((integer? x) (list '() 'int))
((boolean? x) (list '() 'bool))
- ((eq? x 'inc) (list '() '(abs int int)))
- ((eq? x '+) (list '() '(abs int (abs int int))))
+ ((builtin-type x) (list '() (builtin-type x)))
((symbol? x) (list '() (env-lookup env x)))
-
((let? x)
(let ((new-env (fold-left
(lambda (acc bind)
res))
(cadr (check '() (normalize prog))))
-
-(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) '())