X-Git-Url: http://git.lukelau.me/?p=scheme.git;a=blobdiff_plain;f=typecheck.scm;h=f6d7c86465f4869043b3d2fcb9560e42603258d7;hp=ebfd816ad62a9538839c808187d55cbeaad593db;hb=f4b0d5c1b14a1890e1b88398e256b272595346b2;hpb=d6b60d54bc90e5ebdc643d05d0b806ae7fd8aa7c diff --git a/typecheck.scm b/typecheck.scm index ebfd816..f6d7c86 100644 --- a/typecheck.scm +++ b/typecheck.scm @@ -191,18 +191,36 @@ (define (check-case dls env x) (define (check-match switch-type x) + + (define (get-bindings product-types pattern) + (define (go product-type product) + (case (ast-type product) + ['var (list (cons product product-type))] + ; an inner pattern match + ['app (let* ([inner-sum (car product)] + [inner-sums (cdr (assoc product-type dls))] + [inner-product-types (cdr (assoc inner-sum inner-sums))]) + (get-bindings inner-product-types product))] + [else '()])) + (flat-map go product-types (cdr pattern))) + + (let ([pattern (car x)] [expr (cadr x)]) - (if (eqv? (ast-type pattern) 'app) + (case (ast-type pattern) + ['app ; a pattern match with bindings (let ([sum (assoc (car pattern) (cdr (assoc switch-type dls)))]) (unless sum (error #f "can't pattern match ~a with ~a" switch-type pattern)) (let* ([names (cdr pattern)] - [types (cdr sum)] - [new-env (fold-left env-insert env names types)]) - (check dls new-env expr))) + [product-types (cdr sum)] + [new-env (append (get-bindings product-types pattern) env)]) + + (check dls new-env expr)))] + ; pattern match with binding and no constructor + ['var (check dls (env-insert env pattern switch-type) expr)] ; a pattern match without bindings - (check dls env expr)))) + [else (check dls env expr)]))) (let* ([switch-type-res (check dls env (case-switch x))] [switch-type (cadr switch-type-res)] @@ -216,9 +234,9 @@ [resolved-type (substitute case-expr-equality-cs (car case-expr-types))] - [annotated `((case (,(case-expr x) : ,switch-type) - ,(map (lambda (c e et) - `(,c (,e : ,et))) + [annotated `((case ,(caddr switch-type-res) + ,@(map (lambda (c e et) + `(,c ((,e : ,et)))) (map car (case-cases x)) (map cadr (case-cases x)) case-expr-types)) : ,resolved-type)] @@ -345,11 +363,15 @@ `((let ,(map (lambda (o n) (list (car o) (denormalize (cadr o) (cadr n)))) (let-bindings orig) (let-bindings (ann-expr normed))) - ,@(map (lambda (o n) (denormalize o n)) + ,@(map denormalize (let-body orig) (let-body (ann-expr normed)))) : ,(ann-type normed))] ['if `((if ,@(map denormalize (cdr orig) (cdr (ann-expr normed)))) - : (ann-type normed))] + : ,(ann-type normed))] + ['case `((case ,(denormalize (case-switch orig) (case-switch (ann-expr normed))) + ,@(map (lambda (o n) (cons (car o) (denormalize (cadr o) (cadr n)))) + (case-cases orig) (case-cases (ann-expr normed)))) + : ,(ann-type normed))] [else normed])) (define ann-expr car) @@ -359,7 +381,9 @@ (define (annotate-types prog) (denormalize (program-body prog) - (caddr (check (init-adts-env prog) (normalize (program-body prog)))))) + (caddr (check (program-data-layouts prog) + (init-adts-env prog) + (normalize (program-body prog)))))) ; returns a list of constraints