diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt index 3c74d461..3332e47c 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt @@ -3,6 +3,7 @@ (require (rename-in "../utils/utils.rkt" [infer infer-in])) (require racket/match (only-in unstable/list list-update) + (for-syntax racket/base syntax/parse) (contract-req) (infer-in infer) (rep type-rep filter-rep object-rep rep-utils) @@ -78,5 +79,10 @@ [_ Γ]))) ;; run code in an extended env and with replaced props -(define-syntax-rule (with-lexical-env/extend-props ps . b) - (with-lexical-env (env+ (lexical-env) ps (box #t)) . b)) +(define-syntax (with-lexical-env/extend-props stx) + (define-splicing-syntax-class flag + [pattern (~seq #:flag v:expr)] + [pattern (~seq) #:with v #'(box #t)]) + (syntax-parse stx + [(_ ps flag:flag . b) + #'(with-lexical-env (env+ (lexical-env) ps flag.v) . b)])) 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 d1b2f722..f4ef73be 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 @@ -31,63 +31,61 @@ [else (ret (Un))])) (match (single-value tst) [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _) - (let*-values ([(flag+ flag-) (values (box #t) (box #t))]) - (match-let* ([env-thn (env+ (lexical-env) (list fs+) flag+)] - [env-els (env+ (lexical-env) (list fs-) flag-)]) - (define results-t - (with-lexical-env env-thn - (add-unconditional-prop (tc thn (unbox flag+)) (apply -and (env-props env-thn))))) - (define results-u - (with-lexical-env env-els - (add-unconditional-prop (tc els (unbox flag-)) (apply -and (env-props env-els))))) + (define flag+ (box #t)) + (define flag- (box #t)) + (define results-t + (with-lexical-env/extend-props (list fs+) #:flag flag+ + (add-unconditional-prop (tc thn (unbox flag+)) (apply -and (env-props (lexical-env)))))) + (define results-u + (with-lexical-env/extend-props (list fs-) #:flag flag- + (add-unconditional-prop (tc els (unbox flag-)) (apply -and (env-props (lexical-env)))))) - ;; 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)]) - (match* (results-t results-u) - - [((tc-any-results: f1) (tc-any-results: f2)) - (tc-any-results (-or (-and fs+ f1) (-and fs- f2)))] - ;; Not do awful things here - [((tc-results: ts (list (FilterSet: f+ f-) ...) os) (tc-any-results: f2)) - (tc-any-results (-or (apply -and (map -or f+ f-)) f2))] - [((tc-any-results: f2) (tc-results: ts (list (FilterSet: f+ f-) ...) os)) - (tc-any-results (-or (apply -and (map -or f+ f-)) f2))] - [((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)) - (combine-results - (for/list ([f2 (in-list fs2)] [f3 (in-list fs3)] - [t2 (in-list ts)] [t3 (in-list us)] - [o2 (in-list os2)] [o3 (in-list os3)]) - (let ([filter - (match* (f2 f3) - [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-)) - (-FS (-or f2+ f3+) (-or f2- f3-))])] - [type (Un t2 t3)] - [object (if (object-equal? o2 o3) o2 -empty-obj)]) - (ret type filter object))))] - ;; special case if one of the branches is unreachable - [(and (= 1 (length us)) (type-equal? (car us) (Un))) - (ret ts fs2 os2)] - [(and (= 1 (length ts)) (type-equal? (car ts) (Un))) - (ret us fs3 os3)] - ;; otherwise, error - [else - (tc-error/expr "Expected the same number of values from both branches of `if' expression, but got ~a and ~a" - (length ts) (length us))])])))])) + ;; 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)]) + (match* (results-t results-u) + [((tc-any-results: f1) (tc-any-results: f2)) + (tc-any-results (-or (-and fs+ f1) (-and fs- f2)))] + ;; Not do awful things here + [((tc-results: ts (list (FilterSet: f+ f-) ...) os) (tc-any-results: f2)) + (tc-any-results (-or (apply -and (map -or f+ f-)) f2))] + [((tc-any-results: f2) (tc-results: ts (list (FilterSet: f+ f-) ...) os)) + (tc-any-results (-or (apply -and (map -or f+ f-)) f2))] + [((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)) + (combine-results + (for/list ([f2 (in-list fs2)] [f3 (in-list fs3)] + [t2 (in-list ts)] [t3 (in-list us)] + [o2 (in-list os2)] [o3 (in-list os3)]) + (let ([filter + (match* (f2 f3) + [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-)) + (-FS (-or f2+ f3+) (-or f2- f3-))])] + [type (Un t2 t3)] + [object (if (object-equal? o2 o3) o2 -empty-obj)]) + (ret type filter object))))] + ;; special case if one of the branches is unreachable + [(and (= 1 (length us)) (type-equal? (car us) (Un))) + (ret ts fs2 os2)] + [(and (= 1 (length ts)) (type-equal? (car ts) (Un))) + (ret us fs3 os3)] + ;; otherwise, error + [else + (tc-error/expr "Expected the same number of values from both branches of `if' expression, but got ~a and ~a" + (length ts) (length us))])])]))