From b4d100d60cb99e714374d2db3c75a36167b109cc Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Fri, 1 May 2009 21:18:23 +0000
Subject: [PATCH] Fold tc/let-values/check into tc/let-values. Remove printfs.
 More metafunctions to handle splitting and merging filter sets. Handle
 `delay', `list', `list*' Implement tc/funapp for the simple case. Make
 `id-from' a stxclass. Shuffle code around so that it compiles. Type parsing
 now handles multiple values properly, and has a values and results entry
 point.

svn: r14680
---
 collects/typed-scheme/private/parse-type.ss   | 105 ++++++++++--------
 .../typed-scheme/private/type-annotation.ss   |   4 +-
 collects/typed-scheme/test.ss                 |  14 ++-
 collects/typed-scheme/typecheck/signatures.ss |   3 +-
 collects/typed-scheme/typecheck/tc-app.ss     |  76 ++++++++++++-
 .../typed-scheme/typecheck/tc-expr-unit.ss    |   4 +-
 .../typed-scheme/typecheck/tc-lambda-unit.ss  |   4 +-
 .../typed-scheme/typecheck/tc-let-unit.ss     |  10 +-
 .../typecheck/tc-metafunctions.ss             |  29 ++++-
 collects/typed-scheme/types/abbrev.ss         |  17 +--
 collects/typed-scheme/types/utils.ss          |  32 +++++-
 collects/typed-scheme/utils/tc-utils.ss       |  17 ++-
 12 files changed, 217 insertions(+), 98 deletions(-)

diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss
index 147a9d5ea6..509aa3a439 100644
--- a/collects/typed-scheme/private/parse-type.ss
+++ b/collects/typed-scheme/private/parse-type.ss
@@ -1,25 +1,31 @@
 #lang scheme/base
 
-(provide parse-type parse-type/id parse-type*)
+
 
 (require (except-in "../utils/utils.ss" extend))
 (require (except-in (rep type-rep) make-arr)
          (rename-in (types convenience union utils) [make-arr* make-arr])
          (utils tc-utils stxclass-util)
-         syntax/stx
+         syntax/stx (prefix-in c: scheme/contract)
          stxclass stxclass/util
          (env type-environments type-name-env type-alias-env lexical-env)
          (prefix-in t: "base-types-extra.ss")
          scheme/match 
          (for-template scheme/base "base-types-extra.ss"))
 
+(p/c [parse-type (syntax? . c:-> . Type/c)]
+     [parse-type/id (syntax? c:any/c . c:-> . Type/c)] 
+     [parse-tc-results (syntax? . c:-> . tc-results?)] 
+     [parse-tc-results/id (syntax? c:any/c . c:-> . tc-results?)] 
+     [parse-type* (syntax? . c:-> . Type/c)])
+
 (define enable-mu-parsing (make-parameter #t))
 
 
-(define (parse-type/id loc datum)
+(define ((parse/id p) loc datum)
   #;(printf "parse-type/id id : ~a~n ty: ~a~n" (syntax-object->datum loc) (syntax-object->datum stx))
   (let* ([stx* (datum->syntax loc datum loc loc)])
-    (parse-type stx*)))
+    (p stx*)))
 
 (define (stx-cadr stx) (stx-car (stx-cdr stx)))
 
@@ -322,19 +328,20 @@
       [(pred t) 
        (eq? (syntax-e #'pred) 'pred)
        (make-pred-ty (parse-type #'t))]
+      ;; function types
       [(dom -> rng : pred-ty)
        (and 
         (eq? (syntax-e #'->) '->)
         (eq? (syntax-e #':) ':))
        (begin
          (add-type-name-reference (stx-cadr stx))
-         (make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (parse-type #'pred-ty)))]
+         (make-pred-ty (list (parse-type #'dom)) (parse-values-type #'rng) (parse-type #'pred-ty)))]
       [(dom ... rest ::: -> rng)
        (and (eq? (syntax-e #'->) '->) 
             (eq? (syntax-e #':::) '*))
        (begin
          (add-type-name-reference #'->)
-         (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-type #'rng)))]
+         (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-values-type #'rng)))]
       [(dom ... rest ::: bound -> rng)
        (and (eq? (syntax-e #'->) '->) 
             (eq? (syntax-e #':::) '...)
@@ -347,7 +354,7 @@
                (make-Function
                 (list
                  (make-arr-dots (map parse-type (syntax->list #'(dom ...)))
-                                (parse-type #'rng)
+                                (parse-values-type #'rng)
                                 (parameterize ([current-tvars (extend-env (list (syntax-e #'bound)) 
                                                                           (list (make-DottedBoth (make-F (syntax-e #'bound))))
                                                                           (current-tvars))])
@@ -367,7 +374,7 @@
              (make-Function
               (list
                (make-arr-dots (map parse-type (syntax->list #'(dom ...)))
-                              (parse-type #'rng)
+                              (parse-values-type #'rng)
                               (parameterize ([current-tvars (extend-env (list var)
                                                                         (list (make-DottedBoth t))
                                                                         (current-tvars))])
@@ -378,40 +385,8 @@
        (eq? (syntax-e #'->) '->)
        (begin
          (add-type-name-reference #'->)
-         (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rng)))]
-      [(values tys ... dty dd bound)
-       (and (eq? (syntax-e #'dd) '...)
-            (identifier? #'bound)
-            (eq? (syntax-e #'values) 'values))
-       (let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))])
-         (if (not (Dotted? var))
-             (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound))             
-             (make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
-                              (parameterize ([current-tvars (extend-env (list (syntax-e #'bound)) 
-                                                                        (list (make-DottedBoth (make-F (syntax-e #'bound))))
-                                                                        (current-tvars))])
-                                (parse-type #'dty))
-                              (syntax-e #'bound))))]
-      [(values tys ... dty dd)
-       (and (eq? (syntax-e #'values) 'values) 
-            (eq? (syntax-e #'dd) '...))
-       (begin
-         (add-type-name-reference #'values)
-         (let ([bounds (filter (compose Dotted? cdr) (env-keys+vals (current-tvars)))])
-           (when (null? bounds)
-             (tc-error/stx stx "No type variable bound with ... in scope for ... type"))
-           (unless (null? (cdr bounds))
-             (tc-error/stx stx "Cannot infer bound for ... type"))
-           (match-let ([(cons var (struct Dotted (t))) (car bounds)])
-             (make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
-                              (parameterize ([current-tvars (extend-env (list var) 
-                                                                        (list (make-DottedBoth t))
-                                                                        (current-tvars))])
-                                            (parse-type #'dty))
-                              var))))]
-      [(values tys ...) 
-       (eq? (syntax-e #'values) 'values)
-       (-values (map parse-type (syntax->list #'(tys ...))))]
+         (->* (map parse-type (syntax->list #'(dom ...))) (parse-values-type #'rng)))]
+      
       [(case-lambda tys ...) 
        (eq? (syntax-e #'case-lambda) 'case-lambda)
        (make-Function 
@@ -459,7 +434,7 @@
               [tv (make-Dotted (make-F v))])
          (add-type-name-reference #'All)
          (parameterize ([current-tvars (extend-env (cons v vars) (cons tv tvars) (current-tvars))])
-           (make-PolyDots (append vars (list v)) (parse-type #'t))))]
+           (make-PolyDots (append vars (list v)) (parse-values-type #'t))))]
       [(All (vars ...) t) 
        (and (or (eq? (syntax-e #'All) 'All)
                 (eq? (syntax-e #'All) '∀))
@@ -468,7 +443,7 @@
               [tvars (map make-F vars)])
          (add-type-name-reference #'All)
          (parameterize ([current-tvars (extend-env vars tvars (current-tvars))])
-           (make-Poly vars (parse-type #'t))))]
+           (make-Poly vars (parse-values-type #'t))))]
       [(Opaque p?) 
        (eq? (syntax-e #'Opaque) 'Opaque)
        (begin
@@ -554,3 +529,45 @@
            (string? (syntax-e #'t)))
        (-val (syntax-e #'t))]
       [_ (tc-error "not a valid type: ~a" (syntax->datum stx))])))
+
+(define (parse-values-type stx)
+  (parameterize ([current-orig-stx stx])        
+    (syntax-parse stx
+      [(values tys ... dty :ddd bound:id)
+       #:when (eq? (syntax-e #'values) 'values)
+       (let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))])
+         (if (not (Dotted? var))
+             (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound))             
+             (make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
+                              (parameterize ([current-tvars (extend-env (list (syntax-e #'bound)) 
+                                                                        (list (make-DottedBoth (make-F (syntax-e #'bound))))
+                                                                        (current-tvars))])
+                                (parse-type #'dty))
+                              (syntax-e #'bound))))]
+      [(values tys ... dty :ddd)
+       #:when (and (eq? (syntax-e #'values) 'values))
+       (add-type-name-reference #'values)
+       (let ([bounds (filter (compose Dotted? cdr) (env-keys+vals (current-tvars)))])
+         (when (null? bounds)
+           (tc-error/stx stx "No type variable bound with ... in scope for ... type"))
+         (unless (null? (cdr bounds))
+           (tc-error/stx stx "Cannot infer bound for ... type"))
+         (match-let ([(cons var (struct Dotted (t))) (car bounds)])
+           (make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
+                            (parameterize ([current-tvars (extend-env (list var) 
+                                                                      (list (make-DottedBoth t))
+                                                                      (current-tvars))])
+                              (parse-type #'dty))
+                            var)))]
+      [(values tys ...) 
+       #:when (eq? (syntax-e #'values) 'values)
+       (-values (map parse-type (syntax->list #'(tys ...))))]
+      [t
+       (-values (list (parse-type #'t)))])))
+
+(define (parse-tc-results stx)
+  (values->tc-results (parse-values-type stx)))
+
+(define parse-tc-results/id (parse/id parse-tc-results))
+
+(define parse-type/id (parse/id parse-type))
\ No newline at end of file
diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss
index ec556f4d83..ae5fc69a95 100644
--- a/collects/typed-scheme/private/type-annotation.ss
+++ b/collects/typed-scheme/private/type-annotation.ss
@@ -58,8 +58,8 @@
   (define (pt prop)
     #;(print-size prop)
     (if (syntax? prop)
-        (parse-type prop)
-        (parse-type/id stx prop)))
+        (parse-tc-results prop)
+        (parse-tc-results/id stx prop)))
   (cond
     [(syntax-property stx type-ascrip-symbol) => pt]
     [else #f]))
diff --git a/collects/typed-scheme/test.ss b/collects/typed-scheme/test.ss
index c9b5d7c541..a029c11dab 100644
--- a/collects/typed-scheme/test.ss
+++ b/collects/typed-scheme/test.ss
@@ -79,6 +79,7 @@ xxx6-y
 
 (: ff (Number -> Number))
 (define (ff x) x)
+(ff 1)
 
 (lambda: ([y : String][x : Number]) (values 1 x 1))
 (lambda: ([x : Number]) (values 1 x 1))
@@ -86,4 +87,15 @@ xxx6-y
 (lambda () 1)
 #{(lambda (x) x) :: (Number -> Number)}
 ;; BUG - this should work
-{ann (values (lambda (x) x) (lambda (x) x)) (values (Number -> Number) (String -> String))}
\ No newline at end of file
+{ann (values (lambda (x) x) (lambda (x) x)) (values (Number -> Number) (String -> String))}
+
+(list 1 2 3)
+(ann (list 1 2 3) (Pair Number (Listof Integer)))
+(ann (list 1 2 3) (Listof Integer))
+(ann (list 1 2 3) (Listof Number))
+
+(list* 1 2 3)
+(ann (list* 1 2 3 (list)) (Pair Number (Listof Integer)))
+
+((lambda (x) 1) 1) 
+((lambda (x y) 1) 1 2)
diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss
index 366056c830..c5ef2012fa 100644
--- a/collects/typed-scheme/typecheck/signatures.ss
+++ b/collects/typed-scheme/typecheck/signatures.ss
@@ -39,9 +39,8 @@
    [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-results?) (or/c #f tc-results?) . -> . tc-results?)]))
 
 (define-signature tc-let^
-  ([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]
+  ([cnt tc/let-values ((syntax? syntax? syntax? syntax?) ((or/c #f tc-results?)) . ->* . tc-results?)]
    [cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-results?)]
-   [cnt tc/let-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)]
    [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)]))
 
 (define-signature tc-dots^
diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss
index 3973404bd2..155196cde6 100644
--- a/collects/typed-scheme/typecheck/tc-app.ss
+++ b/collects/typed-scheme/typecheck/tc-app.ss
@@ -1,10 +1,11 @@
 #lang scheme/unit
 
 (require (rename-in "../utils/utils.ss" [infer r:infer])
-         "signatures.ss"
+         "signatures.ss" "tc-metafunctions.ss"
          stxclass scheme/match mzlib/trace
          (for-syntax stxclass)
-         (types utils)
+         (types utils abbrev)
+         (utils tc-utils)
          (rep type-rep filter-rep object-rep)
          (for-template 
           (only-in '#%kernel [apply k:apply])
@@ -20,6 +21,7 @@
     #:literals (#%plain-app #%plain-lambda letrec-values
                 values apply k:apply not list list* call-with-values do-make-object make-object cons
                        andmap ormap)
+    ;; special case for `values'
     [(#%plain-app values arg) (single-value #'arg expected)]
     [(#%plain-app values . args)
      (match expected
@@ -35,7 +37,36 @@
        [_ (match-let ([(list (tc-result1: ts fs os) ...) 
                        (for/list ([arg (syntax->list #'args)])
                          (single-value arg))])
-            (ret ts fs os))])]))
+            (ret ts fs os))])]    
+    ;; special case for `delay'
+    [(#%plain-app 
+      mp1 
+      (#%plain-lambda () 
+        (#%plain-app mp2 (#%plain-app call-with-values (#%plain-lambda () e) list))))
+     #:declare mp1 (id-from 'make-promise 'scheme/promise)
+     #:declare mp2 (id-from 'make-promise 'scheme/promise)
+     (ret (-Promise (tc-expr/t #'e)))]
+    ;; special case for `list'
+    [(#%plain-app list . args)
+     (let ([tys (map tc-expr/t (syntax->list #'args))])
+       (ret (apply -lst* tys)))]
+    ;; special case for `list*'
+    [(#%plain-app list* . args)
+     (match-let* ([(list last tys-r ...) (reverse (map tc-expr/t (syntax->list #'args)))]
+                  [tys (reverse tys-r)])
+       (ret (foldr make-Pair last tys)))]
+    ;; inference for ((lambda
+    [(#%plain-app (#%plain-lambda (x ...) . body) args ...)
+     #:when (= (length (syntax->list #'(x ...)))
+               (length (syntax->list #'(args ...))))
+     (tc/let-values #'((x) ...) #'(args ...) #'body 
+                    #'(let-values ([(x) args] ...) . body)
+                    expected)]
+    [(#%plain-app f . args)
+     (let* ([f-ty (single-value #'f)]
+            [arg-tys (map single-value (syntax->list #'args))])
+       (tc/funapp #'f #'args f-ty arg-tys expected))]
+    [_ (int-err "tc/app NYI")]))
 
 ;(trace tc/app/internal)
 
@@ -48,6 +79,41 @@
     (check-below t expected)
     expected)
 
-;; syntax? syntax? tc-result? (listof tc-results?) (or/c #f tc-results) -> tc-results?
+(define (object-index os i)
+  (unless (number? i)
+    (int-err "object-index for keywords NYI"))
+  (list-ref os i))
+
+;; in-indexes : Listof[Type] -> Sequence[index/c]
+(define (in-indexes dom)
+  (in-range (length dom)))
+
+;; syntax? syntax? tc-results? (listof tc-results?) (or/c #f tc-results) -> tc-results?
 (define (tc/funapp f-stx args-stx ftype0 argtys expected)
-  (error "tc/funapp NYI"))
+  (match* (ftype0 argtys)
+    [((tc-result1: (Function: (list (arr: dom (Values: (list (Result: t-r lf-r lo-r) ...)) #f #f '()))))
+      (list (tc-result1: t-a phi-a o-a) ...))
+     (unless (= (length dom) (length t-a))
+       (tc-error/expr #:return (ret t-r)
+                      "Wrong number of arguments"))
+     (for ([dom-t (in-list dom)] [arg-t (in-list t-a)])
+       (check-below arg-t dom-t))
+     (let* (;; Listof[Listof[LFilterSet]]
+            [lfs-f (for/list ([lf lf-r])
+                    (for/list ([i (in-indexes dom)])
+                      (split-lfilters lf i)))]
+            ;; Listof[FilterSet]
+            [f-r (for/list ([lfs lfs-f])
+                   (merge-filter-sets (for/list ([lf lfs] [t t-a] [o o-a])
+                                    (apply-filter lf t o))))]
+            ;; Listof[Object]
+            [o-r (for/list ([lo lo-r])                     
+                   (match lo
+                     [(LPath: pi* i)
+                      (match (object-index o-a i)
+                        [(Path: pi x) (make-Path (append pi* pi) x)]
+                        [_ (make-Empty)])]
+                     [_ (make-Empty)]))])
+       (ret t-r f-r o-r))]
+    [(_ _)
+     (int-err "funapp with keyword/rest args NYI")]))
\ No newline at end of file
diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss
index 43fbcc996f..468aa19dee 100644
--- a/collects/typed-scheme/typecheck/tc-expr-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss
@@ -238,7 +238,7 @@
          (tc/send #'rcvr #'meth #'(args ...) expected)]
         ;; let
         [(let-values ([(name ...) expr] ...) . body)
-         (tc/let-values/check #'((name ...) ...) #'(expr ...) #'body form expected)]
+         (tc/let-values #'((name ...) ...) #'(expr ...) #'body form expected)]
         [(letrec-values ([(name ...) expr] ...) . body)
          (tc/letrec-values/check #'((name ...) ...) #'(expr ...) #'body form expected)]
         ;; other
@@ -340,7 +340,7 @@
       (int-err "bad form input to tc-expr: ~a" form))
     ;; typecheck form
     (let ([ty (cond [(type-ascription form) => (lambda (ann)
-                                                 (tc-expr/check/type form ann))]
+                                                 (tc-expr/check form ann))]
                     [else (internal-tc-expr form)])])
       (match ty
         [(tc-results: ts fs os)
diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss
index b0b1662938..f749365e0d 100644
--- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss
@@ -11,7 +11,7 @@
          (rename-in (types convenience utils union)
                     [make-arr* make-arr])
          (private type-annotation)
-         (types abbrev)
+         (types abbrev utils)
 	 (env type-environments lexical-env)
 	 (utils tc-utils)
          mzlib/plt-match)
@@ -68,7 +68,6 @@
        arg-list arg-types
        (make lam-result (map list arg-list arg-types) null rest-ty drest 
              (tc-exprs/check (syntax->list body) ret-ty))))
-    (printf "arg-types old new: ~a ~a~n"  arg-tys arg-types)
     (when (or (not (= arg-len tys-len))
               (and rest (and (not rest-ty)
                              (not drest))))
@@ -199,7 +198,6 @@
        (match expected          
          [(tc-result1: (Mu: _ _)) (loop (unfold expected))]
          [(tc-result1: (Function: (list (arr: argss rets rests drests '()) ...)))
-          (printf "expe: ~a~n" expected)
           (for/list ([args argss] [ret rets] [rest rests] [drest drests])
             (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args (values->tc-results ret) rest drest))]
          [_ (go (syntax->list formals) (syntax->list bodies) null null null)]))]
diff --git a/collects/typed-scheme/typecheck/tc-let-unit.ss b/collects/typed-scheme/typecheck/tc-let-unit.ss
index 06083a25cd..e1aa8fda99 100644
--- a/collects/typed-scheme/typecheck/tc-let-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-let-unit.ss
@@ -119,7 +119,7 @@
        (-> expected))]
     [_ (tc-expr/t e)]))
 
-(define (tc/let-values/internal namess exprs body form expected)
+(define (tc/let-values namess exprs body form [expected #f])
   (let* (;; a list of each name clause
          [names (map syntax->list (syntax->list namess))]
          ;; all the trailing expressions - the ones actually bound to the names
@@ -133,12 +133,4 @@
          [clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
     (do-check void names types form types body clauses expected)))
 
-(define (tc/let-values/check namess exprs body form expected)
-  (tc/let-values/internal namess exprs body form expected))
-
-(define (tc/let-values namess exprs body form)
-  (tc/let-values/internal namess exprs body form #f))
-
-;(trace tc/letrec-values/internal)
-
 
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 7bb32a4950..2314431381 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -10,7 +10,8 @@
          stxclass/util
          (for-syntax scheme/base))
 
-(provide combine-filter apply-filter abstract-filter abstract-filters)
+(provide combine-filter apply-filter abstract-filter abstract-filters
+         split-lfilters merge-filter-sets)
 
 ;; this implements the sequence invariant described on the first page relating to Bot
 (define (lcombine l1 l2)
@@ -57,7 +58,7 @@
     [(Path: p (lookup: idx)) (make-LPath p idx)]
     [_ (make-LEmpty)]))
 
-(define/contract (abstract-filter ids keys fs)
+(d/c (abstract-filter ids keys fs)
   (-> (listof identifier?) (listof index/c) FilterSet? LFilterSet?)
   (match fs
     [(FilterSet: f+ f-)
@@ -65,7 +66,7 @@
       (apply append (for/list ([f f+]) (abo ids keys f)))
       (apply append (for/list ([f f-]) (abo ids keys f))))]))
 
-(define/contract (abo xs idxs f)
+(d/c (abo xs idxs f)
   (-> (listof identifier?) (listof index/c) Filter/c (or/c '() (list/c LatentFilter/c)))
   (define (lookup y)
     (for/first ([x xs] [i idxs] #:when (free-identifier=? x y)) i)) 
@@ -78,7 +79,12 @@
     [(NotTypeFilter: t p (lookup: idx)) (list (make-LNotTypeFilter t p idx))]
     [_ null]))
 
-(define/contract (apply-filter lfs t o)
+(define (merge-filter-sets fs)
+  (match fs
+    [(list (FilterSet: f+ f-) ...)
+     (make-FilterSet (apply append f+) (apply append f-))]))
+
+(d/c (apply-filter lfs t o)
   (-> LFilterSet? Type/c Object? FilterSet?)
   (match lfs
     [(LFilterSet: lf+ lf-)
@@ -86,7 +92,7 @@
       (apply append (for/list ([lf lf+]) (apo lf t o)))
       (apply append (for/list ([lf lf-]) (apo lf t o))))]))
 
-(define/contract (apo lf s o)
+(d/c (apo lf s o)
   (-> LatentFilter/c Type/c Object? (or/c '() (list/c Filter/c)))
   (match* (lf s o)
     [((LBot:) _ _) (list (make-Bot))]
@@ -96,12 +102,23 @@
     [((LTypeFilter: t pi* _) _ (Path: pi x)) (list (make-TypeFilter t (append pi* pi) x))]
     [((LNotTypeFilter: t pi* _) _ (Path: pi x)) (list (make-NotTypeFilter t (append pi* pi) x))]))
 
+(define/contract (split-lfilters lf idx)  
+  (LFilterSet? index/c . -> . LFilterSet?)
+  (define (idx= lf)
+    (match lf
+      [(LBot:) #t]
+      [(LNotTypeFilter: _ _ idx*) (type-equal? idx* idx)]
+      [(LTypeFilter: _ _ idx*) (type-equal? idx* idx)]))
+  (match lf
+    [(LFilterSet: lf+ lf-)
+     (make-LFilterSet (filter idx= lf+) (filter idx= lf-))]))
+
 (define-match-expander T-FS:
   (lambda (stx) #'(FilterSet: _ (list (Bot:)))))
 (define-match-expander F-FS:
   (lambda (stx) #'(FilterSet: (list (Bot:)) _)))
 
-(define/contract (combine-filter f1 f2 f3)
+(d/c (combine-filter f1 f2 f3)
   (FilterSet? FilterSet? FilterSet? . -> . FilterSet?)
   (match* (f1 f2 f3)
     [(f (T-FS:) (F-FS:)) f] ;; the student expansion
diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss
index be20981216..1b785e17a2 100644
--- a/collects/typed-scheme/types/abbrev.ss
+++ b/collects/typed-scheme/types/abbrev.ss
@@ -262,19 +262,4 @@
                  (make-Function (list (make-arr* (append args (take opt-args i)) result))))))
 
 (define-syntax-rule (->opt args ... [opt ...] res)
-  (opt-fn (list args ...) (list opt ...) res))
-
-(define (tc-results->values tc)
-  (match tc
-    [(tc-results: ts fs os dty dbound)
-     (make-ValuesDots (map -result ts fs os) dty dbound)]
-    [(tc-results: ts fs os)
-     (make-Values (map -result ts fs os))]))
-
-;; FIXME - this should really be a new metafunction like abstract-filter
-(define (values->tc-results tc)
-  (match tc
-    [(ValuesDots: (list (Result: ts fs os)) dty dbound)
-     (int-err "values->tc-results NYI for Dots")]
-    [(Values: (list (Result: ts fs os)))
-     (ret ts)]))
\ No newline at end of file
+  (opt-fn (list args ...) (list opt ...) res))
\ No newline at end of file
diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss
index e37685edd5..d80088f71b 100644
--- a/collects/typed-scheme/types/utils.ss
+++ b/collects/typed-scheme/types/utils.ss
@@ -30,7 +30,9 @@
          just-Dotted?
          tc-error/expr
          lookup-fail
-         lookup-type-fail)
+         lookup-type-fail
+         values->tc-results
+         tc-results->values)
 
 
 ;; substitute : Type Name Type -> Type
@@ -192,10 +194,13 @@
 (define ret
   (case-lambda [(t) 
                 (make-tc-results
-                 (if (Type? t)
-                     (list (make-tc-result t (make-FilterSet null null) (make-Empty)))
-                     (for/list ([i t])
-                               (make-tc-result i (make-FilterSet null null) (make-Empty))))
+                 (cond [(Type? t)
+                        (list (make-tc-result t (make-FilterSet null null) (make-Empty)))]
+                       [(or (Values? t) (ValuesDots? t))
+                        (values->tc-results t)]
+                       [else
+                        (for/list ([i t])
+                          (make-tc-result i (make-FilterSet null null) (make-Empty)))])
                  #f)]
                [(t f)
                 (make-tc-results
@@ -221,7 +226,7 @@
 
 (p/c
  [ret    
-  (->d ([t (or/c Type/c (listof Type/c))])
+  (->d ([t (or/c Type/c (listof Type/c) Values? ValuesDots?)])
        ([f (if (list? t)
                (listof FilterSet?)
                FilterSet?)]
@@ -278,3 +283,18 @@
 
 (define (lookup-type-fail i)
   (tc-error/expr "~a is not bound as a type" (syntax-e i)))
+
+(define (tc-results->values tc)
+  (match tc
+    [(tc-results: ts fs os dty dbound)
+     (make-ValuesDots (map make-Result ts fs os) dty dbound)]
+    [(tc-results: ts fs os)
+     (make-Values (map make-Result ts fs os))]))
+
+;; FIXME - this should really be a new metafunction like abstract-filter
+(define (values->tc-results tc)
+  (match tc
+    [(ValuesDots: (list (Result: ts fs os)) dty dbound)
+     (int-err "values->tc-results NYI for Dots")]
+    [(Values: (list (Result: ts fs os) ...))
+     (ret ts)]))
\ No newline at end of file
diff --git a/collects/typed-scheme/utils/tc-utils.ss b/collects/typed-scheme/utils/tc-utils.ss
index 515cbef66c..b92a4bafdb 100644
--- a/collects/typed-scheme/utils/tc-utils.ss
+++ b/collects/typed-scheme/utils/tc-utils.ss
@@ -6,7 +6,7 @@ don't depend on any other portion of the system
 |#
 
 (provide (all-defined-out))
-(require "syntax-traversal.ss" (for-syntax scheme/base stxclass) scheme/match)
+(require "syntax-traversal.ss" stxclass (for-syntax scheme/base stxclass) scheme/match)
 
 ;; a parameter representing the original location of the syntax being currently checked
 (define current-orig-stx (make-parameter #'here))
@@ -168,4 +168,17 @@ don't depend on any other portion of the system
                              e))))
   (syntax-parse stx
     [(_ e:spec ...)
-     #'(list (list e.id e.ty) ...)]))
\ No newline at end of file
+     #'(list (list e.id e.ty) ...)]))
+
+;; id: identifier
+;; sym: a symbol
+;; mod: a quoted require spec like 'scheme/base
+;; is id the name sym defined in mod?
+(define (id-from? id sym mod)
+  (and (eq? (syntax-e id) sym)
+       (eq? (module-path-index-resolve (syntax-source-module id))
+            ((current-module-name-resolver) mod #f #f #f))))
+
+(define-syntax-class (id-from sym mod)
+  (pattern i:id
+           #:when (id-from? #'i sym mod)))
\ No newline at end of file