X-Git-Url: https://git.lukelau.me/?a=blobdiff_plain;f=typecheck.scm;h=6aca2c1161ab5506189da5fdea2a0675d4761567;hb=7bcc8cc8aa41849a6f6e0615a1309b7ac3b3956f;hp=a526620e7139665fd72273394914462419cb45d0;hpb=c4a5f8ab1efce20f0e1181ffe34639facb19594a;p=scheme.git diff --git a/typecheck.scm b/typecheck.scm index a526620..6aca2c1 100644 --- a/typecheck.scm +++ b/typecheck.scm @@ -244,7 +244,40 @@ annotated))) - ('app (check-app env x))))) + ('app (check-app env x)) + ['case + (let* ([expr-type-res (check env (case-expr x))] + [expr-type (cadr env)] + [case-match-type-res (map (lambda (x) (check env x)) + (map car (case-cases x)))] + [case-match-types (map cadr case-match-type-res)] + + [case-expr-type-res (map (lambda (x) (check env x)) + (map cadr (case-cases x)))] + [case-expr-types (map cadr case-expr-types-res)] + + [case-match-equality-cs (fold-left constraint-merge '() + (map (lambda (t) (~ t expr-type)) case-match-types))] + + [case-expr-equality-cs (fold-left constraint-merge '() + (map (lambda (t) (~ t (car case-expr-type-res))) + (cdr case-expr-type-res)))] + + [resolved-type (substitute case-expr-eqaulity-cs (car case-expr-type-res))] + + [annotated `((case (,(case-expr x) : ,expr-type) + ,(map (lambda (c e et) + `(,c (,e : ,et))) + (map car (case-cases x)) + (map cadr (case-cases x)) + case-expr-types)) : ,resolved-type)] + + [cs (fold-left constraint-merge '() + (append case-match-equality-cs + case-expr-equality-cs + (cadr expr-type-res)))]) + (list cs resolved-type annotated))]))) + ;; (display "result of ") ;; (display x) ;; (display ":\n\t") @@ -259,7 +292,7 @@ ; we typecheck the lambda calculus only (only single arg lambdas) (define (typecheck prog) - (let ([expanded (program-map-exprs expand-pattern-matches prog)]) + (let ([expanded (expand-pattern-matches prog)]) (cadr (check (init-adts-env expanded) (normalize (program-body expanded))))))