X-Git-Url: http://git.lukelau.me/?p=scheme.git;a=blobdiff_plain;f=typecheck.scm;h=821035230affddf4d813074316f5aecaeaa2efc5;hp=6a99869c0697302f361a9e28ac216013f5d018d6;hb=844dcd052c6f551d9936693c2b4c49cf920c7051;hpb=9d93b066cfd6505849dff12146159bedeadf96b9 diff --git a/typecheck.scm b/typecheck.scm index 6a99869..8210352 100644 --- a/typecheck.scm +++ b/typecheck.scm @@ -4,14 +4,13 @@ (and (list? t) (eq? (car t) 'abs))) (define (tvar? t) - (and (not (list? t)) (not (concrete? t)) (symbol? t))) + (and (not (list? t)) + (not (concrete? t)) + (symbol? t))) (define (concrete? t) - (case t - ('int #t) - ('bool #t) - ('void #t) - (else #f))) + (and (symbol? t) + (char-upper-case? (string-ref (symbol->string t) 0)))) (define (pretty-type t) (cond ((abs? t) @@ -38,7 +37,7 @@ ; ('a, ('b, 'a)) (define (env-lookup env n) - (if (null? env) (error #f "empty env") ; it's a type equality + (if (null? env) (error #f "empty env" env n) ; it's a type equality (if (eq? (caar env) n) (cdar env) (env-lookup (cdr env) n)))) @@ -82,46 +81,16 @@ (define (builtin-type x) (case x - ('+ '(abs int (abs int int))) - ('- '(abs int (abs int int))) - ('* '(abs int (abs int int))) - ('! '(abs bool bool)) - ('= '(abs int (abs int bool))) - ('bool->int '(abs bool int)) - ('print '(abs string void)) - (else #f))) - -(define (check env x) - (display "check: ") - (display x) - (display "\n\t") - (display env) - (newline) - (let - ((res - (case (ast-type x) - ('int-literal (list '() 'int)) - ('bool-literal (list '() 'bool)) - ('string-literal (list '() 'string)) - ('builtin (list '() (builtin-type x))) - - ('if - (let* ((cond-type-res (check env (cadr x))) - (then-type-res (check env (caddr x))) - (else-type-res (check env (cadddr x))) - (then-eq-else-cs (~ (cadr then-type-res) - (cadr else-type-res))) - (cs (constraint-merge - (car then-type-res) - (constraint-merge (car else-type-res) - then-eq-else-cs))) - (return-type (substitute cs (cadr then-type-res)))) - (when (not (eqv? (cadr cond-type-res) 'bool)) - (error #f "if condition isn't bool")) - (list cs return-type))) - - ('var (list '() (env-lookup env x))) - ('let + ('+ '(abs Int (abs Int Int))) + ('- '(abs Int (abs Int Int))) + ('* '(abs Int (abs Int Int))) + ('! '(abs Bool Bool)) + ('= '(abs Int (abs Int Bool))) + ('bool->int '(abs Bool Int)) + ('print '(abs String Void)) + (else (error #f "Couldn't find type for builtin" x)))) + +(define (check-let env x) ; takes in the current environment and a scc ; returns new environment with scc's types added in (let* ([components (reverse (sccs (graph (let-bindings x))))] @@ -162,13 +131,42 @@ (cons (car x) (substitute cs (cdr x))) x)) scc-env)]) - (display "cs:") - (display cs) - (newline) new-env))] [new-env (fold-left process-component env components)]) (check new-env (last (let-body x))))) +(define (check env x) + ;; (display "check: ") + ;; (display x) + ;; (display "\n\t") + ;; (display env) + ;; (newline) + (let + ((res + (case (ast-type x) + ('int-literal (list '() 'Int)) + ('bool-literal (list '() 'Bool)) + ('string-literal (list '() 'String)) + ('builtin (list '() (builtin-type x))) + + ('if + (let* ((cond-type-res (check env (cadr x))) + (then-type-res (check env (caddr x))) + (else-type-res (check env (cadddr x))) + (then-eq-else-cs (~ (cadr then-type-res) + (cadr else-type-res))) + (cs (constraint-merge + (car then-type-res) + (constraint-merge (~ (cadr cond-type-res) 'Bool) + (constraint-merge (car else-type-res) + then-eq-else-cs)))) + (return-type (substitute cs (cadr then-type-res)))) + (list cs return-type))) + + ('var (list '() (env-lookup env x))) + ('let (check-let env x)) + + ('lambda (let* [(new-env (env-insert env (lambda-arg x) (fresh-tvar))) @@ -198,7 +196,7 @@ (other-func-type `(abs ,func-type ,return-type)) (cs (~ func-type other-func-type)) (resolved-return-type (substitute cs return-type))] - (list cs resolved-return-type)) + (list cs resolved-return-type))) ; regular function (let* ((arg-type-res (check env (cadr x))) @@ -228,19 +226,24 @@ (if (abs? resolved-func-type) (let ((return-type (substitute cs (caddr resolved-func-type)))) (list cs return-type)) - (error #f "not a function")))))))) - (display "result of ") - (display x) - (display ":\n\t") - (display (pretty-type (cadr res))) - (display "\n\t[") - (display (pretty-constraints (car res))) - (display "]\n") + (error #f "not a function"))))))) + ;; (display "result of ") + ;; (display x) + ;; (display ":\n\t") + ;; (display (pretty-type (cadr res))) + ;; (display "\n\t[") + ;; (display (pretty-constraints (car res))) + ;; (display "]\n") res)) ; we typecheck the lambda calculus only (only single arg lambdas) (define (typecheck prog) - (cadr (check '() (normalize prog)))) + + (let ([init-env (flat-map data-tors (program-datas prog))]) + (display init-env) + (newline) + (cadr (check init-env (normalize (program-body prog)))))) + ; returns a list of constraints (define (~ a b) @@ -278,9 +281,9 @@ ; composes constraints a onto b and merges, i.e. applies a to b ; a should be the "more important" constraints (define (constraint-merge a b) - (define (f constraint) + (define (f cs constraint) (cons (car constraint) - (substitute a (cdr constraint)))) + (substitute cs (cdr constraint)))) (define (most-concrete a b) (cond @@ -291,30 +294,30 @@ ,(most-concrete (caddr a) (caddr b)))] [(abs? a) b] [(abs? b) a] - [else (error #f "impossible! most-concrete")])) - - (define (union p q) - (cond - [(null? p) q] - [(null? q) p] - [else - (let ([x (car q)]) - (if (assoc (car x) p) - (if (eqv? (most-concrete (cddr (assoc (car x) p)) - (cdr x)) - (cdr x)) - (cons x (union (filter (p) (not (eqv? - + [else a])) + + ; for any two constraints that clash, e.g. t1 ~ abs t2 t3 + ; and t1 ~ abs int t3 + ; prepend the most concrete version of the type to the + ; list of constraints + (define (clashes) + (define (gen acc x) + (if (assoc (car x) a) + (cons (cons (car x) (most-concrete (cdr (assoc (car x) a)) + (cdr x))) + acc) + acc)) + (fold-left gen '() b)) (define (union p q) (append (filter (lambda (x) (not (assoc (car x) p))) q) p)) - (union a (map f b))) + (append (clashes) (union a (map (lambda (z) (f a z)) b)))) ;; ; a1 -> a2 ~ a3 -> a4; -;; ; a1 -> a2 !~ bool -> bool +;; ; a1 -> a2 !~ Bool -> Bool ;; ; basically can the tvars be renamed (define (types-equal? x y) (let ([cs (unify? x y)])