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")
; we typecheck the lambda calculus only (only single arg lambdas)
(define (typecheck prog)
- (cadr (check (init-adts-env prog) (normalize (program-body prog)))))
+ (let ([expanded (expand-pattern-matches prog)])
+ (cadr (check (init-adts-env expanded) (normalize (program-body expanded))))))
; before passing annotated types onto codegen
(define ann-expr car)
(define ann-type caddr)
+
+ ; prerequisites: expand-pattern-matches
(define (annotate-types prog)
- (denormalize (program-body prog)
+ (denormalize
+ (program-body prog)
(caddr (check (init-adts-env prog) (normalize (program-body prog))))))