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 01a88d4d47..f0b6deef2a 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 @@ -1,11 +1,10 @@ #lang racket/unit (require "../utils/utils.rkt" - "signatures.rkt" (rep type-rep filter-rep object-rep) (types abbrev union utils filter-ops) (env lexical-env type-env-structs) (utils tc-utils) - "tc-envops.rkt" + (typecheck signatures tc-envops tc-metafunctions) (types type-table) racket/match) @@ -35,10 +34,12 @@ (define flag- (box #t)) (define results-t (with-lexical-env/extend-props (list fs+) #:flag flag+ - (tc thn (unbox flag+)))) + (add-unconditional-prop + (tc thn (unbox flag+)) fs+))) (define results-u (with-lexical-env/extend-props (list fs-) #:flag flag- - (tc els (unbox flag-)))) + (add-unconditional-prop + (tc els (unbox flag-)) fs-))) ;; record reachability ;; since we may typecheck a given piece of code multiple times in different @@ -57,35 +58,4 @@ (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))])])])) + (merge-tc-results (list results-t results-u))])) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt index 49edcd36db..60e028b055 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt @@ -2,7 +2,7 @@ (require "../utils/utils.rkt" racket/match racket/list - (except-in (types abbrev union utils filter-ops) + (except-in (types abbrev union utils filter-ops tc-result) -> ->* one-of/c) (rep type-rep filter-rep object-rep rep-utils) (typecheck tc-subst) @@ -10,6 +10,7 @@ (provide abstract-results combine-props + merge-tc-results tc-results->values) @@ -234,3 +235,56 @@ [(Top:) (loop derived-formulas derived-atoms (cdr worklist))] [(Bot:) (set-box! flag #f) (values derived-formulas derived-atoms)]))))) + +(define (unconditional-prop res) + (match res + [(tc-any-results: f) f] + [(tc-results (list (tc-result: _ (FilterSet: f+ f-) _) ...) _) + (apply -and (map -or f+ f-))])) + +(define (merge-tc-results results) + (define/match (merge-tc-result r1 r2) + [((tc-result: t1 (FilterSet: f1+ f1-) o1) + (tc-result: t2 (FilterSet: f2+ f2-) o2)) + (tc-result + (Un t1 t2) + (-FS (-or f1+ f2+) (-or f1- f2-)) + (if (equal? o1 o2) o1 -empty-obj))]) + + (define/match (same-dty? r1 r2) + [(#f #f) #t] + [((cons t1 dbound) (cons t2 dbound)) #t] + [(_ _) #f]) + (define/match (merge-dty r1 r2) + [(#f #f) #f] + [((cons t1 dbound) (cons t2 dbound)) + (cons (Un t1 t2) dbound)]) + + (define/match (number-of-values res) + [((tc-results rs #f)) + (length rs)] + [((tc-results rs (cons _ dbound))) + (format "~a and ... ~a" (length rs) dbound)]) + + + (define/match (merge-two-results res1 res2) + [((tc-result1: (== -Bottom)) res2) res2] + [(res1 (tc-result1: (== -Bottom))) res1] + [((tc-any-results: f1) res2) + (tc-any-results (-or f1 (unconditional-prop res2)))] + [(res1 (tc-any-results: f2)) + (tc-any-results (-or (unconditional-prop res1) f2))] + [((tc-results results1 dty1) (tc-results results2 dty2)) + ;; if we have the same number of values in both cases + (cond + [(and (= (length results1) (length results2)) + (same-dty? dty1 dty2)) + (tc-results (map merge-tc-result results1 results2) + (merge-dty dty1 dty2))] + ;; otherwise, error + [else + (tc-error/expr "Expected the same number of values, but got ~a and ~a" + (length res1) (length res2))])]) + + (for/fold ([res (ret -Bottom)]) ([res2 (in-list results)]) + (merge-two-results res res2))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt index f096aed1e0..f87189eff8 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt @@ -149,8 +149,10 @@ (define tc-result-equal? equal?) -(provide tc-result: tc-results: tc-any-results: tc-result1: Result1: Results:) +(provide tc-result: tc-results: tc-any-results: tc-result1: Result1: Results: + tc-results) (provide/cond-contract + [tc-result (Type/c Filter/c Object? -> tc-results?)] [combine-results ((c:listof tc-results?) . c:-> . tc-results?)] [tc-any-results ((c:or/c Filter/c NoFilter?) . c:-> . tc-any-results?)] [tc-result-t (tc-result? . c:-> . Type/c)] diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt index 9394637819..a0060acad9 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt @@ -2,8 +2,9 @@ (require "test-utils.rkt" rackunit racket/format - (types abbrev union filter-ops) + (types abbrev union filter-ops tc-result) (typecheck tc-metafunctions) + (rep object-rep) (for-syntax racket/base syntax/parse)) (provide tests) @@ -41,4 +42,35 @@ ) + (test-suite "merge-tc-results" + (check-equal? + (merge-tc-results (list)) + (ret -Bottom)) + (check-equal? + (merge-tc-results (list (ret Univ))) + (ret Univ)) + (check-equal? + (merge-tc-results (list (ret Univ -top-filter (make-Path null #'x)))) + (ret Univ -top-filter (make-Path null #'x))) + (check-equal? + (merge-tc-results (list (ret -Bottom) (ret -Symbol -top-filter (make-Path null #'x)))) + (ret -Symbol -top-filter (make-Path null #'x))) + (check-equal? + (merge-tc-results (list (ret -String) (ret -Symbol))) + (ret (Un -Symbol -String))) + (check-equal? + (merge-tc-results (list (ret -String -true-filter) (ret -Symbol -true-filter))) + (ret (Un -Symbol -String) -true-filter)) + (check-equal? + (merge-tc-results (list (ret (-val #f) -false-filter) (ret -Symbol -true-filter))) + (ret (Un -Symbol (-val #f)) -top-filter)) + (check-equal? + (merge-tc-results (list (ret (list (-val 0) (-val 1))) (ret (list (-val 1) (-val 2))))) + (ret (list (Un (-val 0) (-val 1)) (Un (-val 1) (-val 2))))) + (check-equal? + (merge-tc-results (list (ret null null null -Symbol 'x) (ret null null null -String 'x))) + (ret null null null (Un -Symbol -String) 'x)) + + + ) )) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt index 62b052dccf..a3f1b32f83 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -809,7 +809,8 @@ [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (number? z))]) (lambda: ([x : Any]) (if (p? x) x 12))) - (t:-> Univ Univ : (-FS (-not-filter (-val #f) 0) (-filter (-val #f) 0)))] + (t:-> Univ Univ : (-FS (-not-filter (-val #f) 0) (-filter (-val #f) 0)) + : (make-Path null '(0 0)))] [tc-e/t (let* ([z (ann 1 : Any)] [p? (lambda: ([x : Any]) (not (number? z)))]) (lambda: ([x : Any]) (if (p? x) (ann (add1 7) Any) 12))) @@ -821,7 +822,8 @@ [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) z)]) (lambda: ([x : Any]) (if (p? x) x 12))) - (t:-> Univ Univ : (-FS (-not-filter (-val #f) 0) (-filter (-val #f) 0)))] + (t:-> Univ Univ : (-FS (-not-filter (-val #f) 0) (-filter (-val #f) 0)) + : (make-Path null '(0 0)))] [tc-e (not 1) #:ret (ret -Boolean -false-filter)]