From 5b5a6980d5906b8af376d7dedcd5e010517031d3 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Wed, 21 Apr 2010 14:57:05 -0400
Subject: [PATCH] annotated eta works

---
 collects/typed-scheme/env/init-envs.ss        | 13 ++++++++---
 .../typed-scheme/typecheck/tc-lambda-unit.ss  |  8 ++++---
 .../typecheck/tc-metafunctions.ss             | 22 +++++--------------
 collects/typed-scheme/typecheck/tc-subst.ss   | 14 ++++++++++++
 4 files changed, 35 insertions(+), 22 deletions(-)

diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss
index 79f450907b..91a7ddef0e 100644
--- a/collects/typed-scheme/env/init-envs.ss
+++ b/collects/typed-scheme/env/init-envs.ss
@@ -42,11 +42,18 @@
     [(arr: dom rng rest drest kws)
      `(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))]
     [(TypeFilter: t p i)
-     `(make-TypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))]
+     `(make-TypeFilter ,(sub t) ,(sub p) ,(if (identifier? i)
+                                              `(quote-syntax ,i)
+                                              i))]
     [(NotTypeFilter: t p i)
-     `(make-NotTypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))]
+     `(make-NotTypeFilter ,(sub t) ,(sub p) 
+                          ,(if (identifier? i)
+                               `(quote-syntax ,i)
+                               i))]
     [(Path: p i)
-     `(make-Path ,(sub p) (quote-syntax ,i))]
+     `(make-Path ,(sub p) ,(if (identifier? i)
+                               `(quote-syntax ,i)
+                               i))]
     [(? (lambda (e) (or (Filter? e)
                         (Object? e)
                         (PathElem? e)))
diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss
index 0542519ccb..723a7fa6d5 100644
--- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss
+++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss
@@ -3,6 +3,7 @@
 (require (rename-in "../utils/utils.ss" [infer r:infer])
          "signatures.ss"
          "tc-metafunctions.ss"
+         "tc-subst.ss"
          mzlib/trace
          scheme/list
          syntax/private/util syntax/stx
@@ -201,9 +202,10 @@
        (match expected          
          [(tc-result1: (and t (Mu: _ _))) (loop (ret (unfold t)))]
          [(tc-result1: (Function: (list (arr: argss rets rests drests '()) ...)))
-          (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))]
+          (let ([fmls (car (syntax->list formals))])            
+            (for/list ([args argss] [ret rets] [rest rests] [drest drests])
+              (tc/lambda-clause/check fmls (car (syntax->list bodies))
+                                      args (values->tc-results ret (syntax->list fmls)) rest drest)))]
          [_ (go (syntax->list formals) (syntax->list bodies) null null null)]))]
     ;; otherwise
     [else (go (syntax->list formals) (syntax->list bodies) null null null)]))
diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss
index 0bf70fb680..38c971a17e 100644
--- a/collects/typed-scheme/typecheck/tc-metafunctions.ss
+++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss
@@ -72,28 +72,18 @@
   (define (rec f) (abo xs idxs f))
   (define (sb-t t) t)
   (filter-case (#:Type sb-t #:Filter rec) f
-               [#:TypeFilter t p (lookup: idx)
-                             (make-TypeFilter t p idx)]
-               [#:NotTypeFilter t p (lookup: idx)
-                                (make-NotTypeFilter t p idx)]))
+               [#:TypeFilter 
+                t p (lookup: idx)
+                (make-TypeFilter t p idx)]
+               [#:NotTypeFilter
+                t p (lookup: idx)
+                (make-NotTypeFilter t p idx)]))
 
 (define (merge-filter-sets fs)
   (match fs
     [(list (FilterSet: f+ f-) ...)
      (make-FilterSet (make-AndFilter f+) (make-AndFilter f-))]))
 
-
-
-
-;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
-(d/c/p (values->tc-results tc)
-  ((or/c Values? ValuesDots?) . -> . tc-results?)
-  (match tc
-    [(ValuesDots: (list (Result: ts fs os) ...) dty dbound)
-     (ret ts fs os dty dbound)]
-    [(Values: (list (Result: ts fs os) ...))
-     (ret ts fs os)]))
-
 (define (tc-results->values tc)
   (match tc
     [(tc-results: ts) (-values ts)]))
diff --git a/collects/typed-scheme/typecheck/tc-subst.ss b/collects/typed-scheme/typecheck/tc-subst.ss
index f6f584fc07..468328c137 100644
--- a/collects/typed-scheme/typecheck/tc-subst.ss
+++ b/collects/typed-scheme/typecheck/tc-subst.ss
@@ -129,3 +129,17 @@
                                    (and drest (cons (for-type (car drest)) (cdr drest)))
                                    (map for-type kws)))]))
    (for-type type)))
+
+;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
+(d/c/p (values->tc-results tc formals)
+  ((or/c Values? ValuesDots?) (listof identifier?) . -> . tc-results?)
+  (match tc
+    [(ValuesDots: (list rs ...) dty dbound)
+     (let-values ([(ts fs os) (for/lists (ts fs os) ([r (in-list rs)]) (open-Result r (map (lambda (i) (make-Path null i)) formals)))])
+       (ret ts fs os
+            (for/fold ([dty dty]) ([(o k) (in-indexed (in-list formals))])
+              (subst-type dty k (make-Path null o) #t))
+            dbound))]
+    [(Values: (list rs ...))
+     (let-values ([(ts fs os) (for/lists (ts fs os) ([r (in-list rs)]) (open-Result r (map (lambda (i) (make-Path null i)) formals)))])
+       (ret ts fs os))]))