(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)
; ('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))))
(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))))]
(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)))
(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)))
(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)
; 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
,(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)])
projects / scheme.git / blobdiff