From 378daf06b97f991fcdbb80299105cedcf0906d9b Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Mon, 3 Sep 2012 19:00:08 -0700 Subject: [PATCH] Made tc/exprs check its non final terms with the correct type. Closes PR12974. original commit: 5a43a5c73078b71dbe4d8b170a88b55812dcb383 --- .../tests/typed-racket/succeed/pr12974.rkt | 18 +++++ .../typed-racket/typecheck/tc-expr-unit.rkt | 4 +- collects/typed-racket/typecheck/tc-if.rkt | 74 +++++++++++-------- .../typed-racket/typecheck/tc-let-unit.rkt | 3 +- .../typecheck/tc-metafunctions.rkt | 1 + .../typed-racket/typecheck/tc-toplevel.rkt | 2 +- 6 files changed, 66 insertions(+), 36 deletions(-) create mode 100644 collects/tests/typed-racket/succeed/pr12974.rkt diff --git a/collects/tests/typed-racket/succeed/pr12974.rkt b/collects/tests/typed-racket/succeed/pr12974.rkt new file mode 100644 index 00000000..513a3a6a --- /dev/null +++ b/collects/tests/typed-racket/succeed/pr12974.rkt @@ -0,0 +1,18 @@ +#lang typed/racket + +(define (f) + (let loop ((i 5)) + (if (zero? i) + (void) + (loop (sub1 i)))) + 2) + +(let loop ((i 5)) + (if (zero? i) + (void) + (loop (sub1 i)))) + + +(define (g) + (values 1 2) + 2) diff --git a/collects/typed-racket/typecheck/tc-expr-unit.rkt b/collects/typed-racket/typecheck/tc-expr-unit.rkt index fd64206d..b59ccd9d 100644 --- a/collects/typed-racket/typecheck/tc-expr-unit.rkt +++ b/collects/typed-racket/typecheck/tc-expr-unit.rkt @@ -550,11 +550,11 @@ (define (tc-exprs exprs) (cond [(null? exprs) (ret -Void)] [(null? (cdr exprs)) (tc-expr (car exprs))] - [else (tc-expr/check/type (car exprs) Univ) + [else (tc-expr/check (car exprs) tc-any-results) (tc-exprs (cdr exprs))])) (define (tc-exprs/check exprs expected) (cond [(null? exprs) (check-below (ret -Void) expected)] [(null? (cdr exprs)) (tc-expr/check (car exprs) expected)] - [else (tc-expr/check/type (car exprs) Univ) + [else (tc-expr/check (car exprs) tc-any-results) (tc-exprs/check (cdr exprs) expected)])) diff --git a/collects/typed-racket/typecheck/tc-if.rkt b/collects/typed-racket/typecheck/tc-if.rkt index 4e385cb7..3e7a634f 100644 --- a/collects/typed-racket/typecheck/tc-if.rkt +++ b/collects/typed-racket/typecheck/tc-if.rkt @@ -17,6 +17,7 @@ (define (erase-filter tc) (match tc + [(tc-any-results:) tc] [(tc-results: ts _ _) (ret ts (for/list ([f ts]) (make-NoFilter)) (for/list ([f ts]) (make-NoObject)))])) @@ -44,9 +45,11 @@ [new-thn-props (filter (λ (e) (and (atomic-filter? e) (not (memq e (env-props (lexical-env)))))) (env-props env-thn))] [new-els-props (filter (λ (e) (and (atomic-filter? e) (not (memq e (env-props (lexical-env)))))) - (env-props env-els))] - [(tc-results: ts fs2 os2) (with-lexical-env env-thn (tc thn (unbox flag+)))] - [(tc-results: us fs3 os3) (with-lexical-env env-els (tc els (unbox flag-)))]) + (env-props env-els))]) + + + (define results-t (with-lexical-env env-thn (tc thn (unbox flag+)))) + (define results-u (with-lexical-env env-els (tc els (unbox flag-)))) ;(printf "old props: ~a\n" (env-props (lexical-env))) ;(printf "fs+: ~a\n" fs+) ;(printf "fs-: ~a\n" fs-) @@ -72,36 +75,43 @@ (add-tautology tst)] [else (add-neither tst)]) - - ;; if we have the same number of values in both cases - (cond [(= (length ts) (length us)) - (let ([r (combine-results - (for/list ([f2 fs2] [f3 fs3] [t2 ts] [t3 us] [o2 os2] [o3 os3]) - (let ([filter - (match* (f2 f3) - [((NoFilter:) _) - (-FS -top -top)] - [(_ (NoFilter:)) - (-FS -top -top)] - [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-)) - ;(printf "f2- ~a f+ ~a\n" f2- fs+) - (-FS (-or (apply -and fs+ f2+ new-thn-props) (apply -and fs- f3+ new-els-props)) - (-or (apply -and fs+ f2- new-thn-props) (apply -and fs- f3- new-els-props)))])] - [type (Un t2 t3)] - [object (if (object-equal? o2 o3) o2 (make-Empty))]) - ;(printf "result filter is: ~a\n" filter) - (ret type filter object))))]) - (cond-check-below r expected))] - ;; special case if one of the branches is unreachable - [(and (= 1 (length us)) (type-equal? (car us) (Un))) - (cond-check-below (ret ts fs2 os2) expected)] - [(and (= 1 (length ts)) (type-equal? (car ts) (Un))) - (cond-check-below (ret us fs3 os3) expected)] - ;; otherwise, error + (match* (results-t results-u) + [((tc-any-results:) _) (cond-check-below tc-any-results expected)] + [(_ (tc-any-results:)) (cond-check-below tc-any-results expected)] + [((tc-results: ts fs2 os2) + (tc-results: us fs3 os3)) + ;; if we have the same number of values in both cases + (cond [(= (length ts) (length us)) + (let ([r (combine-results + (for/list ([f2 fs2] [f3 fs3] [t2 ts] [t3 us] [o2 os2] [o3 os3]) + (let ([filter + (match* (f2 f3) + [((NoFilter:) _) + (-FS -top -top)] + [(_ (NoFilter:)) + (-FS -top -top)] + [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-)) + ;(printf "f2- ~a f+ ~a\n" f2- fs+) + (-FS (-or (apply -and fs+ f2+ new-thn-props) (apply -and fs- f3+ new-els-props)) + (-or (apply -and fs+ f2- new-thn-props) (apply -and fs- f3- new-els-props)))])] + [type (Un t2 t3)] + [object (if (object-equal? o2 o3) o2 (make-Empty))]) + ;(printf "result filter is: ~a\n" filter) + (ret type filter object))))]) + (cond-check-below r expected))] + ;; special case if one of the branches is unreachable + [(and (= 1 (length us)) (type-equal? (car us) (Un))) + (cond-check-below (ret ts fs2 os2) expected)] + [(and (= 1 (length ts)) (type-equal? (car ts) (Un))) + (cond-check-below (ret us fs3 os3) expected)] + ;; otherwise, error [else - (tc-error/expr #:return (ret (or expected Err)) + (tc-error/expr #:return (or expected (ret Err)) "Expected the same number of values from both branches of `if' expression, but got ~a and ~a" - (length ts) (length us))])))] + (length ts) (length us))])])))] + [(tc-any-results:) + (tc-error/expr #:return (or expected (ret Err)) + "Test expression expects one value, given unknown amount")] [(tc-results: t _ _) - (tc-error/expr #:return (ret (or expected Err)) + (tc-error/expr #:return (or expected (ret Err)) "Test expression expects one value, given ~a" t)])) diff --git a/collects/typed-racket/typecheck/tc-let-unit.rkt b/collects/typed-racket/typecheck/tc-let-unit.rkt index 48f743e1..0f300178 100644 --- a/collects/typed-racket/typecheck/tc-let-unit.rkt +++ b/collects/typed-racket/typecheck/tc-let-unit.rkt @@ -23,12 +23,13 @@ (define (erase-filter tc) (match tc + [(tc-any-results:) tc] [(tc-results: ts _ _) (ret ts (for/list ([f ts]) (make-NoFilter)) (for/list ([f ts]) (make-NoObject)))])) (define/cond-contract (do-check expr->type namess results expected-results form exprs body clauses expected #:abstract [abstract null]) (((syntax? syntax? tc-results/c . c:-> . any/c) - (listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c) + (listof (listof identifier?)) (listof tc-results?) (listof tc-results?) syntax? (listof syntax?) syntax? (listof syntax?) (or/c #f tc-results/c)) (#:abstract any/c) . c:->* . diff --git a/collects/typed-racket/typecheck/tc-metafunctions.rkt b/collects/typed-racket/typecheck/tc-metafunctions.rkt index 8e59d3d0..9fcdd03d 100644 --- a/collects/typed-racket/typecheck/tc-metafunctions.rkt +++ b/collects/typed-racket/typecheck/tc-metafunctions.rkt @@ -73,6 +73,7 @@ (define (tc-results->values tc) (match tc + [(tc-any-results:) ManyUniv] [(tc-results: ts) (-values ts)])) (provide combine-props tc-results->values) diff --git a/collects/typed-racket/typecheck/tc-toplevel.rkt b/collects/typed-racket/typecheck/tc-toplevel.rkt index 52af2f50..9fe88b6b 100644 --- a/collects/typed-racket/typecheck/tc-toplevel.rkt +++ b/collects/typed-racket/typecheck/tc-toplevel.rkt @@ -255,7 +255,7 @@ (loop (cdr l)))))] ;; otherwise, the form was just an expression - [_ (tc-expr form)]))) + [_ (tc-expr/check form tc-any-results)])))