diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt index 97d4a2d8..34fe39d4 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt @@ -15,19 +15,10 @@ (define (tc/if-twoarm tst thn els [expected #f]) (define (tc expr reachable?) (unless reachable? (warn-unreachable expr)) - (cond - ;; if reachable? is #f, then we don't want to verify that this branch has the appropriate type - ;; in particular, it might be (void) - [(and expected reachable?) - (tc-expr/check expr (erase-filter expected))] - ;; this code is reachable, but we have no expected type - [reachable? (tc-expr expr)] - ;; otherwise, this code is unreachable - ;; and the resulting type should be the empty type - [(check-unreachable-code?) - (tc-expr expr) - (ret (Un))] - [else (ret (Un))])) + ;; If the code is unreachable, the resulting type should be Bottom. + (if reachable? + (tc-expr/check expr (and expected (erase-filter expected))) + (ret -Bottom))) (match (single-value tst) [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _) (define flag+ (box #t)) @@ -42,20 +33,8 @@ (tc els (unbox flag-)) fs-))) ;; record reachability - ;; since we may typecheck a given piece of code multiple times in different - ;; contexts, we need to take previous results into account - (cond [(and (not (unbox flag+)) ; maybe contradiction - ;; to be an actual contradiction, we must have either previously - ;; recorded this test as a contradiction, or have never seen it - ;; before - (not (tautology? tst)) - (not (neither? tst))) - (add-contradiction tst)] - [(and (not (unbox flag-)) ; maybe tautology - ;; mirror case - (not (contradiction? tst)) - (not (neither? tst))) - (add-tautology tst)] - [else - (add-neither tst)]) + (when (unbox flag+) + (test-position-add-true tst)) + (when (unbox flag-) + (test-position-add-false tst)) (merge-tc-results (list results-t results-u))])) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt index 8534f0ea..00ed03c8 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt @@ -347,7 +347,7 @@ (null? matching-arrs)) (warn-unreachable body) (add-dead-lambda-branch (formals-syntax formal)) - (list formal body (if (check-unreachable-code?) #f null))] + (list formal body null)] [else (list formal body matching-arrs)]) formals+bodies+arrs*) (arities-seen-add arities-seen arity))]))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/type-table.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/type-table.rkt index c7d847d3..455e9b1f 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/type-table.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/type-table.rkt @@ -16,12 +16,10 @@ [add-typeof-expr (syntax? tc-results/c . -> . any/c)] [type-of (syntax? . -> . tc-results/c)] [reset-type-table (-> any/c)] - [add-tautology (syntax? . -> . any)] - [add-contradiction (syntax? . -> . any)] - [add-neither (syntax? . -> . any)] + [test-position-add-true (syntax? . -> . any)] + [test-position-add-false (syntax? . -> . any)] [tautology? (syntax? . -> . boolean?)] [contradiction? (syntax? . -> . boolean?)] - [neither? (syntax? . -> . boolean?)] [add-dead-lambda-branch (syntax? . -> . any)] [dead-lambda-branch? (syntax? . -> . boolean?)] [;; Register that the given expression should be ignored @@ -64,22 +62,30 @@ (syntax-line e) (syntax-column e)))))) -;; keeps track of expressions that always evaluate to true or always evaluate -;; to false, so that the optimizer can eliminate dead code -;; 3 possible values: 'tautology 'contradiction 'neither -(define tautology-contradiction-table (make-hasheq)) +;; For expressions in test position keep track of if it evaluates to true/false +;; values: can be 'true, 'false, 'both. +(define test-position-table (make-hasheq)) -(define-values (add-tautology add-contradiction add-neither) +(define (test-position-add-true expr) + (hash-update! test-position-table expr + (lambda (v) + (case v + [(true) 'true] + [(false both) 'both])) + 'true)) +(define (test-position-add-false expr) + (hash-update! test-position-table expr + (lambda (v) + (case v + [(false) 'false] + [(true both) 'both])) + 'false)) + +(define-values (tautology? contradiction?) (let () (define ((mk t?) e) - (when (optimize?) - (hash-set! tautology-contradiction-table e t?))) - (values (mk 'tautology) (mk 'contradiction) (mk 'neither)))) -(define-values (tautology? contradiction? neither?) - (let () - (define ((mk t?) e) - (eq? t? (hash-ref tautology-contradiction-table e 'not-there))) - (values (mk 'tautology) (mk 'contradiction) (mk 'neither)))) + (eq? t? (hash-ref test-position-table e 'not-there))) + (values (mk 'true) (mk 'false)))) ;; keeps track of lambda branches that never get evaluated, so that the ;; optimizer can eliminate dead code. The key is the formals syntax object. diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt index d2c202f8..e0a59922 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt @@ -15,7 +15,6 @@ don't depend on any other portion of the system orig-module-stx expanded-module-stx print-syntax? - check-unreachable-code? warn-unreachable? delay-errors? current-type-names @@ -57,7 +56,6 @@ don't depend on any other portion of the system ;; do we print the fully-expanded syntax in error messages? (define print-syntax? (make-parameter #f)) -(define check-unreachable-code? (make-parameter #f)) (define warn-unreachable? (make-parameter #t))