typecheck.scm

   1 (load "ast.scm")
   2
   3 (define (abs? t)
   4   (and (list? t) (eq? (car t) 'abs)))
   5
   6 (define (tvar? t)
   7   (and (not (list? t))
   8        (not (concrete? t))
   9        (symbol? t)))
  10
  11 (define (concrete? t)
  12   (and (symbol? t)
  13        (char-upper-case? (string-ref (symbol->string t) 0))))
  14
  15 (define (pretty-type t)
  16   (cond ((abs? t)
  17          (string-append
  18           (if (abs? (cadr t))
  19               (string-append "(" (pretty-type (cadr t)) ")")
  20               (pretty-type (cadr t)))
  21           " -> "
  22           (pretty-type (caddr t))))
  23         (else (symbol->string t))))
  24
  25 (define (pretty-constraints cs)
  26   (string-append "{"
  27                  (fold-left string-append
  28                             ""
  29                             (map (lambda (c)
  30                                    (string-append
  31                                     (pretty-type (car c))
  32                                     ": "
  33                                     (pretty-type (cdr c))
  34                                     ", "))
  35                                  cs))
  36                  "}"))
  37
  38                                         ; ('a, ('b, 'a))
  39 (define (env-lookup env n)
  40   (if (null? env) (error #f "empty env" env n)                  ; it's a type equality
  41       (if (eq? (caar env) n)
  42           (cdar env)
  43           (env-lookup (cdr env) n))))
  44
  45 (define (env-insert env n t)
  46   (cons (cons n t) env))
  47
  48 (define abs-arg cadr)
  49
  50 (define cur-tvar 0)
  51 (define (fresh-tvar)
  52   (begin
  53     (set! cur-tvar (+ cur-tvar 1))
  54     (string->symbol
  55      (string-append "t" (number->string (- cur-tvar 1))))))
  56
  57 (define (last xs)
  58   (if (null? (cdr xs))
  59       (car xs)
  60       (last (cdr xs))))
  61
  62 (define (normalize prog) ; (+ a b) -> ((+ a) b)
  63   (case (ast-type prog)
  64     ('lambda
  65                                         ; (lambda (x y) (+ x y)) -> (lambda (x) (lambda (y) (+ x y)))
  66         (if (> (length (lambda-args prog)) 1)
  67             (list 'lambda (list (car (lambda-args prog)))
  68                   (normalize (list 'lambda (cdr (lambda-args prog)) (caddr prog))))
  69             (list 'lambda (lambda-args prog) (normalize (caddr prog)))))
  70     ('app
  71      (if (null? (cddr prog))
  72          `(,(normalize (car prog)) ,(normalize (cadr prog))) ; (f a)
  73          (normalize `(,(list (normalize (car prog)) (normalize (cadr prog)))
  74                       ,@(cddr prog))))) ; (f a b)
  75     ('let
  76         (append (list 'let
  77                       (map (lambda (x) `(,(car x) ,(normalize (cadr x))))
  78                            (let-bindings prog)))
  79                 (map normalize (let-body prog))))
  80     (else (ast-traverse normalize prog))))
  81
  82 (define (builtin-type x)
  83   (case x
  84     ('+ '(abs Int (abs Int Int)))
  85     ('- '(abs Int (abs Int Int)))
  86     ('* '(abs Int (abs Int Int)))
  87     ('! '(abs Bool Bool))
  88     ('= '(abs Int (abs Int Bool)))
  89     ('bool->int '(abs Bool Int))
  90     ('print '(abs String Void))
  91     (else (error #f "Couldn't find type for builtin" x))))
  92
  93 (define (check-let env x)
  94
  95   ; acc is a pair of (env . annotated bindings)
  96   (define (process-component acc comps)
  97     (let*
  98                                         ; create a new env with tvars for each component
  99                                         ; e.g. scc of (x y)
 100                                         ; scc-env = ((x . t0) (y . t1))
 101         ([scc-env
 102           (fold-left
 103            (lambda (acc c)
 104              (env-insert acc c (fresh-tvar)))
 105            (car acc) comps)]
 106                                         ; typecheck each component
 107          [type-results
 108           (map
 109            (lambda (c)
 110              (let ([body (cadr (assoc c (let-bindings x)))])
 111                (check scc-env body)))
 112            comps)]
 113                                         ; collect all the constraints in the scc
 114          [cs
 115           (fold-left
 116            (lambda (acc res c)
 117              (constraint-merge
 118               (constraint-merge
 119                                         ; unify with tvars from scc-env
 120                                         ; result ~ tvar
 121                (~ (env-lookup scc-env c) (cadr res))
 122                (car res))
 123               acc))
 124            '() type-results comps)]
 125                                         ; substitute *only* the bindings in this scc
 126          [new-env
 127           (map (lambda (x)
 128                  (if (memv (car x) comps)
 129                      (cons (car x) (substitute cs (cdr x)))
 130                      x))
 131                scc-env)]
 132
 133          [annotated-bindings (append (cdr acc) ; the previous annotated bindings
 134                                      (map list
 135                                           comps
 136                                           (map caddr type-results)))])
 137       (cons new-env annotated-bindings)))
 138                                         ; takes in the current environment and a scc
 139                                         ; returns new environment with scc's types added in
 140   (let* ([components (reverse (sccs (graph (let-bindings x))))]
 141          [results (fold-left process-component (cons env '()) components)]
 142          [new-env (car results)]
 143          [annotated-bindings (cdr results)]
 144
 145          [body-results (map (lambda (body) (check new-env body)) (let-body x))]
 146          [let-type (cadr (last body-results))]
 147          [cs (fold-left (lambda (acc cs) (constraint-merge acc cs)) '() (map car body-results))]
 148
 149          [annotated `((let ,annotated-bindings ,@(map caddr body-results)) : ,let-type)])
 150     (list cs let-type annotated)))
 151
 152 (define (check-app env x)
 153   (if (eqv? (car x) (cadr x))
 154                                         ; recursive function (f f)
 155                                         ; TODO: what about ((f a) f)????
 156       (let* ([func-type (env-lookup env (car x))]
 157              [return-type (fresh-tvar)]
 158              [other-func-type `(abs ,func-type ,return-type)]
 159              [cs (~ func-type other-func-type)]
 160              [resolved-return-type (substitute cs return-type)]
 161
 162              [annotated `(((,(car x) : ,func-type)
 163                            (,(cadr x) : ,func-type)) : ,resolved-return-type)])
 164         (list cs resolved-return-type annotated)))
 165
 166                                         ; regular function
 167   (let* ([arg-type-res (check env (cadr x))]
 168          [arg-type (cadr arg-type-res)]
 169          [func-type-res (check env (car x))]
 170          [func-type (cadr func-type-res)]
 171
 172                                         ; f ~ a -> t0
 173          [func-c (~
 174                   (substitute (car arg-type-res) func-type)
 175                   `(abs ,arg-type ,(fresh-tvar)))]
 176          [cs (constraint-merge
 177               (constraint-merge func-c (car arg-type-res))
 178               (car func-type-res))]
 179
 180          [resolved-func-type (substitute cs func-type)]
 181          [resolved-return-type (caddr resolved-func-type)]
 182
 183          [annotated `((,(caddr func-type-res)
 184                        ,(caddr arg-type-res)) : ,resolved-return-type)])
 185
 186     (if (abs? resolved-func-type)
 187         (let ((return-type (substitute cs (caddr resolved-func-type))))
 188           (list cs return-type annotated))
 189         (error #f "not a function"))))
 190
 191 ; returns a list (constraints type annotated)
 192 (define (check env x)
 193   (define (make-result cs type)
 194     (list cs type `(,x : ,type)))
 195   ;; (display "check: ")
 196   ;; (display x)
 197   ;; (display "\n\t")
 198   ;; (display env)
 199   ;; (newline)
 200   (let
 201       ((res
 202         (case (ast-type x)
 203           ('int-literal (make-result '() 'Int))
 204           ('bool-literal (make-result '() 'Bool))
 205           ('string-literal (make-result '() 'String))
 206           ('builtin (make-result '() (builtin-type x)))
 207
 208           ('if
 209            (let* ((cond-type-res (check env (cadr x)))
 210                   (then-type-res (check env (caddr x)))
 211                   (else-type-res (check env (cadddr x)))
 212                   (then-eq-else-cs (~ (cadr then-type-res)
 213                                       (cadr else-type-res)))
 214                   (cs (constraint-merge
 215                        (car then-type-res)
 216                        (constraint-merge (~ (cadr cond-type-res) 'Bool)
 217                                          (constraint-merge (car else-type-res)
 218                                                            then-eq-else-cs))))
 219                   (return-type (substitute cs (cadr then-type-res)))
 220                   [annotated `((if ,(caddr cond-type-res)
 221                                    ,(caddr then-type-res)
 222                                    ,(caddr else-type-res)) : ,return-type)])
 223              (list cs return-type annotated)))
 224
 225           ('var (make-result '() (env-lookup env x)))
 226           ('let (check-let env x))
 227
 228
 229           ('lambda
 230               (let* ([new-env (env-insert env (lambda-arg x) (fresh-tvar))]
 231
 232                      [body-type-res (check new-env (lambda-body x))]
 233                      [cs (car body-type-res)]
 234                      [subd-env (substitute-env (car body-type-res) new-env)]
 235                      [arg-type (env-lookup subd-env (lambda-arg x))]
 236                      [resolved-arg-type (substitute cs arg-type)]
 237
 238                      [lambda-type `(abs ,resolved-arg-type ,(cadr body-type-res))]
 239
 240                      [annotated `((lambda (,(lambda-arg x)) ,(caddr body-type-res)) : ,lambda-type)])
 241
 242                 (list (car body-type-res) ; constraints
 243                       lambda-type  ; type
 244                       annotated)))
 245
 246
 247           ('app (check-app env x))
 248           ['case
 249               (let* ([expr-type-res (check env (case-expr x))]
 250                      [expr-type (cadr env)]
 251                      [case-match-type-res (map (lambda (x) (check env x))
 252                                                (map car (case-cases x)))]
 253                      [case-match-types (map cadr case-match-type-res)]
 254
 255                      [case-expr-type-res (map (lambda (x) (check env x))
 256                                               (map cadr (case-cases x)))]
 257                      [case-expr-types (map cadr case-expr-types-res)]
 258
 259                      [case-match-equality-cs (fold-left constraint-merge '()
 260                                                         (map (lambda (t) (~ t expr-type)) case-match-types))]
 261
 262                      [case-expr-equality-cs (fold-left constraint-merge '()
 263                                                        (map (lambda (t) (~ t (car case-expr-type-res)))
 264                                                             (cdr case-expr-type-res)))]
 265
 266                      [resolved-type (substitute case-expr-eqaulity-cs (car case-expr-type-res))]
 267
 268                      [annotated `((case (,(case-expr x) : ,expr-type)
 269                                     ,(map (lambda (c e et)
 270                                             `(,c (,e : ,et)))
 271                                           (map car (case-cases x))
 272                                           (map cadr (case-cases x))
 273                                           case-expr-types)) : ,resolved-type)]
 274
 275                      [cs (fold-left constraint-merge '()
 276                                     (append case-match-equality-cs
 277                                             case-expr-equality-cs
 278                                             (cadr expr-type-res)))])
 279                 (list cs resolved-type annotated))])))
 280
 281     ;; (display "result of ")
 282     ;; (display x)
 283     ;; (display ":\n\t")
 284     ;; (display (pretty-type (cadr res)))
 285     ;; (display "\n\t[")
 286     ;; (display (pretty-constraints (car res)))
 287     ;; (display "]\n")
 288     res))
 289
 290 (define (init-adts-env prog)
 291   (flat-map data-tors-type-env (program-data-layouts prog)))
 292
 293                                         ; we typecheck the lambda calculus only (only single arg lambdas)
 294 (define (typecheck prog)
 295   (let ([expanded (expand-pattern-matches prog)])
 296     (cadr (check (init-adts-env expanded) (normalize (program-body expanded))))))
 297
 298
 299                                         ; before passing annotated types onto codegen
 300                                         ; we need to restore the pre-normalization structure
 301                                         ; (this is important for function arity etc)
 302 (define (denormalize orig normed)
 303
 304   (define (collapse-lambdas n x)
 305     (case n
 306       [0 x]
 307       [else
 308        (let* ([inner-lambda (lambda-body (ann-expr x))]
 309               [arg (lambda-arg (ann-expr x))]
 310               [inner-collapsed (ann-expr (collapse-lambdas (- n 1) inner-lambda))])
 311          `((lambda ,(cons arg (lambda-args inner-collapsed))
 312              ,(lambda-body inner-collapsed)) : ,(ann-type x)))]))
 313
 314   (define (collapse-apps n x)
 315     (case n
 316       [-1 (error #f "nullary functions not handled yet")]
 317       [0 x]
 318       [else
 319        (let* ([inner-app (car (ann-expr x))]
 320               [inner-collapsed (collapse-apps (- n 1) inner-app)])
 321          `(,(append (ann-expr inner-collapsed) (cdr (ann-expr x))) : ,(ann-type x)))]))
 322
 323   (case (ast-type orig)
 324     ['lambda
 325         (let ([collapsed (collapse-lambdas (- (length (lambda-args orig)) 1) normed)])
 326           `((lambda ,(lambda-args (ann-expr collapsed))
 327               ,(denormalize (lambda-body orig)
 328                             (lambda-body (ann-expr collapsed)))) : ,(ann-type collapsed)))]
 329     ['app
 330      (let ([collapsed (collapse-apps (- (length orig) 2) normed)])
 331        `(,(map (lambda (o n) (denormalize o n)) orig (ann-expr collapsed))
 332          : ,(ann-type collapsed)))]
 333     ['let
 334         `((let ,(map (lambda (o n) (list (car o) (denormalize (cadr o) (cadr n))))
 335                      (let-bindings orig)
 336                      (let-bindings (ann-expr normed)))
 337             ,@(map (lambda (o n) (denormalize o n))
 338                    (let-body orig)
 339                    (let-body (ann-expr normed)))) : ,(ann-type normed))]
 340     ['if `((if ,@(map denormalize (cdr orig) (cdr (ann-expr normed))))
 341            : (ann-type normed))]
 342     [else normed]))
 343
 344 (define ann-expr car)
 345 (define ann-type caddr)
 346
 347                                         ; prerequisites: expand-pattern-matches
 348 (define (annotate-types prog)
 349   (denormalize
 350    (program-body prog)
 351    (caddr (check (init-adts-env prog) (normalize (program-body prog))))))
 352
 353
 354                                         ; returns a list of constraints
 355 (define (~ a b)
 356   (let ([res (unify? a b)])
 357     (if res
 358         res
 359         (error #f
 360                (format "couldn't unify ~a ~~ ~a" a b)))))
 361
 362 (define (unify? a b)
 363   (cond [(eq? a b) '()]
 364         [(tvar? a) (list (cons a b))]
 365         [(tvar? b) (list (cons b a))]
 366         [(and (abs? a) (abs? b))
 367          (let* [(arg-cs (unify? (cadr a) (cadr b)))
 368                 (body-cs (unify? (substitute arg-cs (caddr a))
 369                                  (substitute arg-cs (caddr b))))]
 370            (constraint-merge body-cs arg-cs))]
 371         [else #f]))
 372
 373 (define (substitute cs t)
 374   (cond
 375    [(tvar? t)
 376     (if (assoc t cs)
 377         (cdr (assoc t cs))
 378         t)]
 379    [(abs? t) `(abs ,(substitute cs (cadr t))
 380                    ,(substitute cs (caddr t)))]
 381    [else t]))
 382
 383                                         ; applies substitutions to all variables in environment
 384 (define (substitute-env cs env)
 385   (map (lambda (x) (cons (car x) (substitute cs (cdr x)))) env))
 386
 387                                         ; composes constraints a onto b and merges, i.e. applies a to b
 388                                         ; a should be the "more important" constraints
 389 (define (constraint-merge a b)
 390   (define (f cs constraint)
 391     (cons (car constraint)
 392           (substitute cs (cdr constraint))))
 393
 394   (define (most-concrete a b)
 395     (cond
 396      [(tvar? a) b]
 397      [(tvar? b) a]
 398      [(and (abs? a) (abs? b))
 399       `(abs ,(most-concrete (cadr a) (cadr b))
 400             ,(most-concrete (caddr a) (caddr b)))]
 401      [(abs? a) b]
 402      [(abs? b) a]
 403      [else a]))
 404
 405                                         ; for any two constraints that clash, e.g. t1 ~ abs t2 t3
 406                                         ; and t1 ~ abs int t3
 407                                         ; prepend the most concrete version of the type to the
 408                                         ; list of constraints
 409   (define (clashes)
 410     (define (gen acc x)
 411       (if (assoc (car x) a)
 412           (cons (cons (car x) (most-concrete (cdr (assoc (car x) a))
 413                                              (cdr x)))
 414                 acc)
 415           acc))
 416     (fold-left gen '() b))
 417
 418   (define (union p q)
 419     (append (filter (lambda (x) (not (assoc (car x) p)))
 420                     q)
 421             p))
 422   (append (clashes) (union a (map (lambda (z) (f a z)) b))))
 423
 424
 425 ;;                                      ; a1 -> a2 ~ a3 -> a4;
 426 ;;                                      ; a1 -> a2 !~ Bool -> Bool
 427 ;;                                      ; basically can the tvars be renamed
 428 (define (types-equal? x y)
 429   (let ([cs (unify? x y)])
 430     (if (not cs) #f
 431         (let*
 432             ([test (lambda (acc c)
 433                      (and acc
 434                           (tvar? (car c)) ; the only substitutions allowed are tvar -> tvar
 435                           (tvar? (cdr c))))])
 436           (fold-left test #t cs)))))
 437
 438                                         ; input: a list of binds ((x . y) (y . 3))
 439                                         ; returns: pair of verts, edges ((x y) . (x . y))
 440