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