Move tc-if merging results logic to tc-metafunctions for reuse.

2014-05-28 08:47:55 -07:00 · 2014-05-28 08:47:55 -07:00 · 447b52855f
commit 447b52855f
parent 5fa263b232
5 changed files with 101 additions and 41 deletions
--- 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))]))
--- 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)))
--- 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)]
--- 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))
+
+
+    )
  ))
--- 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)]