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