Various constants are true.

Remove useless code.
`combine-filter' now handles producing the new type/object in appropriate cases.
Move student expansion later in pattern match.
Print out top-level tc-results.

svn: r14721

collects/typed-scheme/typecheck/tc-expr-unit.ss

@@ -188,9 +188,9 @@
         [(quote #t) (ret (-val #t) true-filter)]
         [(quote val)  (match expected
                         [(tc-result1: t)
-                         (ret (tc-literal #'val t))])]
+                         (ret (tc-literal #'val t) true-filter)])]
         ;; syntax
-        [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))]
+        [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) true-filter)]
         ;; mutation!
         [(set! id val)
          (match-let* ([(tc-result: id-t) (tc-expr #'id)]
@@ -273,9 +273,9 @@
       [(quote #f) (ret (-val #f) false-filter)]
       [(quote #t) (ret (-val #t) true-filter)]
       
-      [(quote val)  (ret (tc-literal #'val))]
+      [(quote val)  (ret (tc-literal #'val) true-filter)]
       ;; syntax
-      [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))]
+      [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) true-filter)]
       ;; w-c-m
       [(with-continuation-mark e1 e2 e3)
        (begin (tc-expr/check/type #'e1 Univ)
@@ -315,7 +315,6 @@
       ;; application        
       [(#%plain-app . _) (tc/app form)]
       ;; if
-      [(if tst body) (tc/if-twoarm #'tst #'body #'(#%app void))]
       [(if tst thn els) (tc/if-twoarm #'tst #'thn #'els)]                          
 
       

collects/typed-scheme/typecheck/tc-lambda-unit.ss

@@ -277,7 +277,7 @@
 (define (tc/lambda/internal form formals bodies expected)
   (if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected))
       (ret (tc/plambda form formals bodies expected))
-      (ret (tc/mono-lambda/type formals bodies expected))))
+      (ret (tc/mono-lambda/type formals bodies expected) true-filter)))
 
 ;; tc/lambda : syntax syntax-list syntax-list -> tc-result
 (define (tc/lambda form formals bodies)

collects/typed-scheme/typecheck/tc-metafunctions.ss

@@ -118,28 +118,30 @@
 (define-match-expander F-FS:
   (lambda (stx) #'(FilterSet: (list (Bot:)) _)))
 
-(d/c (combine-filter f1 f2 f3)
+(d/c (combine-filter f1 f2 f3 t2 t3 o2 o3)
-  (FilterSet? FilterSet? FilterSet? . -> . FilterSet?)
+  (FilterSet? FilterSet? FilterSet? Type? Type? Object? Object? . -> . tc-results?)
+  (define (mk f) (ret (Un t2 t3) f (make-Empty)))
   (match* (f1 f2 f3)
-    [(f (T-FS:) (F-FS:)) f] ;; the student expansion
+    [((T-FS:) f _) (ret t2 f o2)]
-    [((T-FS:) f _) f]
+    [((F-FS:) _ f) (ret t3 f o3)]
-    [((F-FS:) _ f) f]
     ;; skipping the general or/predicate rule because it's really complicated
     ;; or/predicate special case for one elem lists
     ;; note that we are relying on equal? on identifiers here
     [((FilterSet: (list (TypeFilter: t pi x)) (list (NotTypeFilter: t pi x)))
       (T-FS:)
       (FilterSet: (list (TypeFilter: s pi x)) (list (NotTypeFilter: s pi x))))
-     (make-FilterSet (list (make-TypeFilter (Un t s) pi x)) (list (make-NotTypeFilter (Un t s) pi x)))]
+     (mk (make-FilterSet (list (make-TypeFilter (Un t s) pi x)) (list (make-NotTypeFilter (Un t s) pi x))))]
     ;; or
-    [((FilterSet: f1+ f1-) (T-FS:) (FilterSet: f3+ f3-)) (combine null (append f1- f3-))]
+    [((FilterSet: f1+ f1-) (T-FS:) (FilterSet: f3+ f3-)) (mk (combine null (append f1- f3-)))]
     ;; and
     [((FilterSet: f1+ f1-) (FilterSet: f2+ f2-) (F-FS:)) 
-     (combine (append f1+ f2+) null)]
+     (mk (combine (append f1+ f2+) null))]
-    [(f f* f*) f*]
+    [(f f* f*) (mk f*)]
+    ;; the student expansion
+    [(f (T-FS:) (F-FS:)) (mk f)]
     [(_ _ _)
      ;; could intersect f2 and f3 here
-     (make-FilterSet null null)]))
+     (mk (make-FilterSet null null))]))
 
 ;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
 (define (values->tc-results tc formals)

collects/typed-scheme/typecheck/tc-new-if.ss

@@ -20,15 +20,15 @@
 
 (define (tc/if-twoarm tst thn els [expected #f])
   (define (tc e) (if expected (tc-expr/check e expected) (tc-expr e)))
-  (match (tc-expr tst)
+  (match (single-value tst)
     [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _)
-     (match-let ([(tc-results: ts fs2 _) (with-lexical-env (env+ (lexical-env) fs+) (tc thn))]
+     (match-let ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+) (tc thn))]
-                 [(tc-results: us fs3 _) (with-lexical-env (env+ (lexical-env) fs-) (tc els))])
+                 [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs-) (tc els))])
        ;; if we have the same number of values in both cases
        (cond [(= (length ts) (length us))
-              (ret (for/list ([t ts] [u us]) (Un t u))
+              (combine-results
-                   (for/list ([f2 fs2] [f3 fs3])
+               (for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3])
-                             (combine-filter f1 f2 f3)))]
+                 (combine-filter f1 f2 f3 t u o2 o3)))]
              [else
               (tc-error/expr #:return (ret Err)
                              "Expected the same number of values from both branches of if expression, but got ~a and ~a"

collects/typed-scheme/typed-scheme.ss

@@ -130,9 +130,8 @@
           body2]
          [_ (let ([ty-str (match type
                             [(tc-result1: (? (lambda (t) (type-equal? t -Void)))) #f]
-                            [(tc-result1: t)
+                            [(tc-results: t)
-                             (format "- : ~a\n" t)]
+                             (format "- : ~a\n" type)]
-                            [(tc-results: ts) (format "- : ~a\n" (cons 'values ts))]
                             [x (int-err "bad type result: ~a" x)])])
               (if #'ty-str                  
                   #`(let ([type '#,ty-str])

collects/typed-scheme/types/utils.ss

@@ -30,7 +30,8 @@
          just-Dotted?
          tc-error/expr
          lookup-fail
-         lookup-type-fail)
+         lookup-type-fail
+         combine-results)
 
 
 ;; substitute : Type Name Type -> Type
@@ -190,17 +191,15 @@
 
 ;; convenience function for returning the result of typechecking an expression
 (define ret
-  (case-lambda [(t) 
+  (case-lambda [(t)
-                (make-tc-results
+                (let ([mk (lambda (t) (make-FilterSet null null))])
-                 (cond [(Type? t)
+                  (make-tc-results
-                        (list (make-tc-result t (make-FilterSet null null) (make-Empty)))]
+                   (cond [(Type? t)
-                       [(or (Values? t) (ValuesDots? t))
+                          (list (make-tc-result t (mk t) (make-Empty)))]                       
-                        (int-err "Values in ret: ~a" t)
+                         [else
-                        #;(values->tc-results t)]
+                          (for/list ([i t])
-                       [else
+                            (make-tc-result i (mk t) (make-Empty)))])
-                        (for/list ([i t])
+                   #f))]
-                          (make-tc-result i (make-FilterSet null null) (make-Empty)))])
-                 #f)]
                [(t f)
                 (make-tc-results
                  (if (Type? t)
@@ -225,7 +224,7 @@
 
 (p/c
  [ret    
-  (->d ([t (or/c Type/c (listof Type/c) Values? ValuesDots?)])
+  (->d ([t (or/c Type/c (listof Type/c))])
        ([f (if (list? t)
                (listof FilterSet?)
                FilterSet?)]
@@ -236,6 +235,11 @@
         [dbound symbol?])
        [_ tc-results?])])
 
+(define (combine-results tcs)
+  (match tcs
+    [(list (tc-result1: t f o) ...)
+     (ret t f o)]))
+
 (define (subst v t e) (substitute t v e))