Handle ValuesDots in check-below.

Fix typo in valuesdots handling in values->tc-results
Handle ValuesDots in do-ret.
Don't try to construct silly wrappers for `apply values'
Don't use rest as list extension if it's #f
Fix tc-result handling for check-subforms/check
Add stronger contracts for Scope
Always generate substitution for infer/dots.
Fix type of `time-apply'

svn: r14815

collects/typed-scheme/env/type-alias-env.ss

@@ -31,8 +31,6 @@
   (mapping-put! id (make-unresolved stx #f)))
 
 (define (register-resolved-type-alias id ty)
-  #;(when (eq? 'Number (syntax-e id))
-    (printf "registering type ~a ~a~n~a~n" id (syntax-e id) ty))
   (mapping-put! id (make-resolved ty)))
 
 (define (lookup-type-alias id parse-type [k (lambda () (tc-error "Unknown type alias: ~a" (syntax-e id)))])

collects/typed-scheme/infer/infer-unit.ss

@@ -498,7 +498,7 @@
            [cs (cset-meet cs-short cs-dotted*)])
       (if (not expected)
           (subst-gen cs R must-vars)
-          (cset-meet cs (cgen null X R expected))))))
+          (subst-gen (cset-meet cs (cgen null X R expected)) R must-vars)))))
 
 (define (infer/simple S T R)
   (infer (fv/list T) S T R))

collects/typed-scheme/private/base-env.ss

@@ -259,10 +259,12 @@
 
 [apply        (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
 [kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))]
-[time-apply (-polydots (b a) (make-arr
+[time-apply (-polydots (b a) 
-                              (list ((list) (a a) . ->... . b)
+		       (make-Function 
-                                    (-lst a))                               
+			(list (make-arr
-                              (-values (list (-pair b (-val '())) N N N))))]
+			       (list ((list) (a a) . ->... . b)
+				     (-lst a))                               
+			       (-values (list (-pair b (-val '())) N N N))))))]
 
 [call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]
 [call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))]

collects/typed-scheme/rep/type-rep.ss

@@ -10,30 +10,31 @@
 
 (define name-table (make-weak-hasheq))
 
-(define Type/c
+(define Type/c?
-  (flat-named-contract
-   'Type
    (λ (e)
      (and (Type? e)
           (not (Scope? e))
           (not (arr? e))
           (not (Values? e))
           (not (ValuesDots? e))
-          (not (Result? e))))))
+          (not (Result? e)))))
+
+(define Type/c
+  (flat-named-contract 'Type Type/c?))
 
 ;; Name = Symbol
 
 ;; Type is defined in rep-utils.ss
 
 ;; t must be a Type
-(dt Scope ([t Type?]) [#:key (Type-key t)])
+(dt Scope ([t (or/c Type/c Scope?)]) [#:key (Type-key t)])
 
 (define (scope-depth k)
   (flat-named-contract 
    (format "Scope of depth ~a" k)
    (lambda (sc)
      (define (f k sc)
-       (cond [(= 0 k) (not (Scope? sc))]
+       (cond [(= 0 k) (Type/c? sc)]
              [(not (Scope? sc)) #f]
              [else (f (sub1 k) (Scope-t sc))]))
      (f k sc))))

collects/typed-scheme/typecheck/check-subforms-unit.ss

@@ -61,7 +61,8 @@
         [stx
          ;; this is a hander function
          (syntax-property form 'typechecker:exn-handler)
-         (tc-expr/check form (-> (Un) expected))]
+         (tc-expr/check form (match expected 
+                               [(tc-result1: e) (ret (-> (Un) e))]))]
         [stx
          ;; this is the body of the with-handlers
          (syntax-property form 'typechecker:exn-body)
@@ -71,7 +72,7 @@
            (loop #'a)
            (loop #'b))]
         [_ (void)])))
-  (ret expected))
+  expected)
 
 ;; typecheck the expansion of a with-handlers form
 ;; syntax -> any

collects/typed-scheme/typecheck/signatures.ss

@@ -23,7 +23,7 @@
 (define-signature check-subforms^
   ([cnt check-subforms/ignore (syntax? . -> . any)]
    [cnt check-subforms/with-handlers (syntax? . -> . any)]
-   [cnt check-subforms/with-handlers/check (syntax? Type/c . -> . any)]))
+   [cnt check-subforms/with-handlers/check (syntax? tc-results? . -> . any)]))
 
 (define-signature tc-if^
   ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-results?)]   

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

@@ -167,7 +167,9 @@
 
 (define (tc/apply f args)
   (define (do-ret t)
-    (match t [(Values: (list (Result: ts _ _) ...)) (ret ts)]))
+    (match t 
+      [(Values: (list (Result: ts _ _) ...)) (ret ts)]
+      [(ValuesDots: (list (Result: ts _ _) ...) dty dbound) (ret ts (for/list ([t ts]) (-FS null null)) (for/list ([t ts]) (make-Empty)) dty dbound)]))
   (define f-ty (single-value f))
   ;; produces the first n-1 elements of the list, and the last element
   (define (split l) (let-values ([(f r) (split-at l (sub1 (length l)))])
@@ -385,10 +387,10 @@
     [(#%plain-app apply values e)
      (cond [(with-handlers ([exn:fail? (lambda _ #f)])
               (untuple (tc-expr/t #'e)))
-            => (lambda (t) (ret (-values t)))]
+            => ret]
            [else (tc/apply #'values #'(e))])]
     ;; rewrite this so that it takes advantages of all the special cases
-    [(#%plain-app k:apply . args) (tc/app/internal (syntax/loc form (apply . args)) expected)]
+    [(#%plain-app k:apply . args) (tc/app/internal (syntax/loc form (#%plain-app apply . args)) expected)]
     ;; handle apply specially
     [(#%plain-app apply f . args) (tc/apply #'f #'args)]
     ;; special case for `values' with single argument - we just ignore the values, except that it forces arg to return one value
@@ -543,8 +545,8 @@
                      t argtys expected)]
     ;; polymorphic ... type
     [((tc-result1: (and t (PolyDots: 
-                         (and vars (list fixed-vars ... dotted-var))
+                           (and vars (list fixed-vars ... dotted-var))
-                         (Function: (list (and arrs (arr: doms rngs (and #f rests) (cons dtys dbounds) '())) ...)))))
+                           (Function: (list (and arrs (arr: doms rngs (and #f rests) (cons dtys dbounds) '())) ...)))))
       (list (tc-result1: argtys-t) ...))
      (handle-clauses (doms dtys dbounds rngs arrs) f-stx args-stx
                      (lambda (dom dty dbound rng arr) (and (<= (length dom) (length argtys))
@@ -577,8 +579,10 @@
     ;; error type is a perfectly good fcn type
     [((tc-result1: (Error:)) _) (ret (make-Error))]
     ;; otherwise fail
-    [((tc-result1: f-ty) _) (tc-error/expr #:return (ret (Un))
+    [((tc-result1: f-ty) _) 
-                                           "Cannot apply expression of type ~a, since it is not a function type" f-ty)]))
+     ;(printf "ft: ~a argt: ~a~n" ftype0 argtys)
+     (tc-error/expr #:return (ret (Un))
+                    "Cannot apply expression of type ~a, since it is not a function type" f-ty)]))
 
 
 ;; syntax? syntax? arr? (listof tc-results?) (or/c #f tc-results) [boolean?] -> tc-results?
@@ -593,7 +597,7 @@
              [(and rest (< (length t-a) (length dom)))
               (tc-error/expr #:return (ret t-r)
                              "Wrong number of arguments, expected at least ~a and got ~a" (length dom) (length t-a))])
-       (for ([dom-t (in-list-forever dom rest)] [a (syntax->list args-stx)] [arg-t (in-list t-a)])
+       (for ([dom-t (if rest (in-list-forever dom rest) (in-list dom))] [a (syntax->list args-stx)] [arg-t (in-list t-a)])
          (parameterize ([current-orig-stx a]) (check-below arg-t dom-t))))
      (let* (;; Listof[Listof[LFilterSet]]
             [lfs-f (for/list ([lf lf-r])

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

@@ -137,6 +137,10 @@
      (unless (andmap subtype t1 t2)
        (tc-error/expr "1 Expected ~a, but got ~a" t2 t1))
      expected]
+    [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound))
+     (unless (andmap subtype t1 t2)
+       (tc-error/expr "1.5 Expected ~a, but got ~a" t2 t1))
+     expected]
     [((tc-result1: t1 f o) (? Type? t2))
      (unless (subtype t1 t2)
        (tc-error/expr "1 Expected ~a, but got ~a" t2 t1))

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

@@ -146,7 +146,7 @@
 ;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results?
 (define (values->tc-results tc formals)
   (match tc
-    [(ValuesDots: (list (Result: ts lfs los)) dty dbound)
+    [(ValuesDots: (list (Result: ts lfs los) ...) dty dbound)
      (ret ts
           (for/list ([lf lfs]) 
             (merge-filter-sets

collects/typed-scheme/typed-scheme.ss

@@ -49,7 +49,7 @@
                ([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e))))
                  (lambda (e) (tc-error "Internal error: ~a" e))])]
            [parameterize (;; disable fancy printing
-                          [custom-printer #t]
+                          [custom-printer #f]
                           ;; a cheat to avoid units
                           [infer-param infer]
                           ;; do we report multiple errors