Definition (but not use) of ... vars

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

@@ -1,7 +1,9 @@
 #lang scheme/unit
 
 (require "type-effect-convenience.ss" "type-rep.ss" "effect-rep.ss" "rep-utils.ss"
-         "free-variance.ss" "type-utils.ss" "union.ss" "tc-utils.ss" "type-name-env.ss"
+         "free-variance.ss" 
+         (except-in "type-utils.ss" Dotted)
+         "union.ss" "tc-utils.ss" "type-name-env.ss"
          "subtype.ss" "remove-intersect.ss" "signatures.ss" "utils.ss"
          "constraint-structs.ss"
          scheme/match

collects/typed-scheme/private/parse-type.ss

@@ -24,11 +24,6 @@
 
 (define (stx-cadr stx) (stx-car (stx-cdr stx)))
 
-;; t is (make-F v)
-(define-struct Dotted (t))
-(define-struct (DottedBoth Dotted) ())
-
-
 (define (parse-type stx)    
   (parameterize ([current-orig-stx stx])
     (syntax-case* stx ()

collects/typed-scheme/private/prims.ss

@@ -96,7 +96,11 @@ This file defines two sorts of primitives. All of them are provided into any mod
 (define-for-syntax (types-of-formals stx src)
   (syntax-case stx (:)
     [([var : ty] ...) (quasisyntax/loc stx (ty ...))]
-    [([var : ty] ... . [rest : rest-ty]) (syntax/loc stx (ty ... rest-ty *))]
+    [([var : ty] ... . [rest : rest-ty]) 
+     (syntax/loc stx (ty ... rest-ty *))]
+    [([var : ty] ... . [rest : rest-ty ddd bound])
+     (eq? '... (syntax-e #'ddd))
+     (syntax/loc stx (ty ... rest-ty ddd bound))]
     [_
      (let loop ([stx stx])
        (syntax-case stx ()
@@ -139,7 +143,12 @@ This file defines two sorts of primitives. All of them are provided into any mod
     [(_ arg : ty)
      (syntax-property #'arg 'type-ascription #'ty)]
     [(_ arg ty)
-     (syntax-property #'arg 'type-ascription #'ty)]))
+     (syntax-property #'arg 'type-ascription #'ty)]
+    [(_ arg ty ddd bound)
+     (eq? '... (syntax-e #'ddd))
+     (syntax-property (syntax-property #'arg 'type-ascription #'ty)
+                      'type-dotted 
+                      #'bound)]))
 
 (define-syntax (: stx)
   (let ([stx*
@@ -198,12 +207,19 @@ This file defines two sorts of primitives. All of them are provided into any mod
     (map label-one
          (syntax->list vars)
          (syntax->list tys)))
+  (define (label-dotted var ty bound)
+    (syntax-property (syntax-property var 'type-ascription ty)
+                      'type-dotted 
+                      bound))
   (syntax-case stx (:)
     [[var : ty] (label-one #'var #'ty)]
     [([var : ty] ...)
      (label #'(var ...) #'(ty ...))]
     [([var : ty] ... . [rest : rest-ty])
-     (append (label #'(var ...) #'(ty ...)) (label-one #'rest #'rest-ty))]))       
+     (append (label #'(var ...) #'(ty ...)) (label-one #'rest #'rest-ty))]
+    [([var : ty] ... . [rest : rest-ty ddd bound])
+     (eq? '... (syntax-e #'ddd))
+     (append (label #'(var ...) #'(ty ...)) (label-dotted #'rest #'rest-ty #'bound))]))
 
 (define-syntax-rule (λ: . args) (lambda: . args))
 

collects/typed-scheme/private/syntax-traversal.ss

@@ -23,6 +23,8 @@
 ;; if it can't find it.
 (define (enclosing-syntaxes-with-source enclosing lookfor src)
   (let loop ([r '()] [stx enclosing])
+    ;(printf "stx is ~a~n" (syntax->datum stx))
+    ;(printf "source is ~a~n" (syntax-source stx))
     (let* ([r (if (and (syntax? stx) (eq? src (syntax-source stx)))
                 (cons stx r)
                 r)]
@@ -44,26 +46,25 @@
   ;(printf "expanded : ~a~n" expanded)
   ;(printf "lookfor : ~a~n" lookfor)
   ;(printf "src : ~a~n" src)
-  ;; we just might get a lookfor that is already in the original
+  (let ([enclosing (enclosing-syntaxes-with-source expanded lookfor src)]
-   (let ([enclosing (enclosing-syntaxes-with-source expanded lookfor src)]
+        [syntax-locs (make-hash)])
-         [syntax-locs (make-hash)])
+    ;; find all syntax locations in original code
-     ;; find all syntax locations in original code
+    (let loop ([stx orig])
-     (let loop ([stx orig])
+      (when (syntax? stx) (hash-set! syntax-locs (syntax-loc stx) stx))
-       (when (syntax? stx) (hash-set! syntax-locs (syntax-loc stx) stx))
+      (let ([stx (if (syntax? stx) (syntax-e stx) stx)])
-       (let ([stx (if (syntax? stx) (syntax-e stx) stx)])
+        (when (pair? stx) (loop (car stx)) (loop (cdr stx)))))
-         (when (pair? stx) (loop (car stx)) (loop (cdr stx)))))
+    (or
-     (or
+     ;; we just might get a lookfor that is already in the original
-      ;; we just might get a lookfor that is already in the original
+     (and (eq? src (syntax-source lookfor))
-      (and (eq? src (syntax-source lookfor))
+          (hash-ref syntax-locs (syntax-loc lookfor) #f)
-           (hash-ref syntax-locs (syntax-loc lookfor) #f)
+          #;(printf "chose branch one: ~a~n" (hash-ref syntax-locs (syntax-loc lookfor) #f)))
-           #;(printf "chose branch one: ~a~n" (hash-ref syntax-locs (syntax-loc lookfor) #f)))
      
-      ;; look for some enclosing expression
+     ;; look for some enclosing expression
-      (and enclosing
+     (and enclosing
-           (begin0
+          (begin0
-             (ormap (lambda (enc) (hash-ref syntax-locs (syntax-loc enc) #f))
+            (ormap (lambda (enc) (hash-ref syntax-locs (syntax-loc enc) #f))
-                    enclosing)
+                   enclosing)
-             #;(printf "chose branch two ~a~n" enclosing))))))
+            #;(printf "chose branch two ~a~n" enclosing))))))
 
 ;(trace look-for-in-orig)
 

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

@@ -2,6 +2,7 @@
 
 (require "signatures.ss"
          mzlib/trace
+         scheme/list
          (except-in "type-rep.ss" make-arr) ;; doesn't need tests
          "type-effect-convenience.ss" ;; maybe needs tests
          "type-environments.ss" ;; doesn't need tests
@@ -105,14 +106,35 @@
           [t (int-err "bad match - not a tc-result: ~a no ret-ty" t)])))]
     [(args ... . rest)
      (let* ([arg-list (syntax->list #'(args ...))]
-            [arg-types (map get-type arg-list)]
+            [arg-types (map get-type arg-list)])
-            [rest-type (get-type #'rest)])
        (for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) (cons #'rest arg-list))
-       (with-lexical-env/extend 
+       (cond 
-        (cons #'rest arg-list) 
+         [(dotted? #'rest)
-        (cons (make-Listof rest-type) arg-types)
+          =>
-        (match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))])
+          (lambda (bound)
-          (make-arr arg-types t rest-type))))]))
+            (unless (Dotted? (lookup (current-tvars) bound
+                                     (lambda _ (tc-error/stx #'rest
+                                                             "Bound on ... type (~a) was not in scope" bound))))
+              (tc-error "Bound on ... type (~a) is not an appropriate type variable" bound))
+            (parameterize ([current-tvars (extend-env (list bound) 
+                                                      (list (make-DottedBoth (make-F bound)))
+                                                      (current-tvars))])
+              (let ([rest-type (get-type #'rest)])
+                (with-lexical-env/extend 
+                 arg-list
+                 arg-types
+                 (parameterize ([dotted-env (extend-env (list #'rest)
+                                                        (list (cons rest-type bound))
+                                                        (dotted-env))])
+                   (match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))])
+                     (make-arr-dots arg-types t rest-type bound)))))))]
+         [else
+          (let ([rest-type (get-type #'rest)])
+            (with-lexical-env/extend 
+             (cons #'rest arg-list) 
+             (cons (make-Listof rest-type) arg-types)
+             (match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))])
+               (make-arr arg-types t rest-type))))]))]))
 
 ;(trace tc-args)
 
@@ -164,7 +186,7 @@
 ;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic
 ;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> Type
 (define (tc/lambda/internal form formals bodies expected)
-  (if (or (syntax-property form 'typechecker:plambda) (Poly? expected))
+  (if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected))
       (tc/plambda form formals bodies expected)
       (ret (tc/mono-lambda formals bodies expected))))
 
@@ -177,6 +199,8 @@
   (match expected
     [(Poly-names: ns (and expected* (Function: _)))
      (let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
+                     (when (and (pair? p) (eq? '... (car (last p))))
+                       (tc-error "Expected a polymorphic function without ..., but given function had ..."))
                      (or (and p (map syntax-e (syntax->list p)))
                          ns))]
             [literal-tvars tvars]
@@ -185,16 +209,45 @@
                   (tc/mono-lambda formals bodies expected*))])
        ;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
        (ret expected))]
+    [(PolyDots-names: (list ns ... dvar) (and expected* (Function: _)))
+     (let-values 
+         ([(tvars dotted)
+           (let ([p (syntax-property form 'typechecker:plambda)])
+             (if p
+                 (match (map syntax-e (syntax->list p))
+                   [(list var ... dvar '...)
+                    (values var dvar)]
+                   [_ (tc-error "Expected a polymorphic function with ..., but given function had no ...")])
+                 (values ns dvar)))])
+       (let* ([literal-tvars tvars]
+              [new-tvars (map make-F literal-tvars)]
+              [ty (parameterize ([current-tvars (extend-env (cons dotted literal-tvars)
+                                                            (cons (make-Dotted (make-F dotted))
+                                                                  new-tvars)
+                                                            (current-tvars))])
+                    (tc/mono-lambda formals bodies expected*))])
+         (ret expected)))]
     [#f
-     (let* ([tvars (let ([p (syntax-property form 'typechecker:plambda)])
+     (match (map syntax-e (syntax->list (syntax-property form 'typechecker:plambda)))
-                     (map syntax-e (syntax->list p)))]
+       [(list tvars ... dotted-var '...)
-            [literal-tvars tvars]
+        (let* ([literal-tvars tvars]
-            [new-tvars (map make-F literal-tvars)]
+               [new-tvars (map make-F literal-tvars)]
-            [ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
+               [ty (parameterize ([current-tvars (extend-env (cons dotted-var literal-tvars)
-                  (tc/mono-lambda formals bodies #f))])
+                                                             (cons (make-Dotted (make-F dotted-var)) new-tvars)
-       ;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
+                                                             (current-tvars))])
-       (ret (make-Poly literal-tvars ty)))]
+                     (tc/mono-lambda formals bodies #f))])
-    [_ (tc-error/expr #:return expected "Expected a value of type ~a, but got a polymorphic function." expected)]))
+          (ret (make-PolyDots (append literal-tvars (list dotted-var)) ty)))]
+       [tvars
+        (let* ([literal-tvars tvars]
+               [new-tvars (map make-F literal-tvars)]
+               [ty (parameterize ([current-tvars (extend-env literal-tvars new-tvars (current-tvars))])
+                     (tc/mono-lambda formals bodies #f))])
+          ;(printf "plambda: ~a ~a ~a ~n" literal-tvars new-tvars ty)
+          (ret (make-Poly literal-tvars ty)))])]
+    [_ 
+     (unless (check-below (tc/plambda form formals bodies #f) expected)
+       (tc-error/expr #:return (ret expected) "Expected a value of type ~a, but got a polymorphic function." expected))
+     (ret expected)]))
     
 
 ;; form : a syntax object for error reporting
@@ -204,7 +257,6 @@
 ;; args : the types of the actual arguments to the loop
 ;; ret : the expected return type of the whole expression
 (define (tc/rec-lambda/check form formals body name args ret)
-  #;(printf "formals: ~a~n" (syntax->datum formals))
   (with-lexical-env/extend
    (syntax->list formals) args
    (let ([t (->* args ret)])

collects/typed-scheme/private/tc-toplevel.ss

@@ -94,7 +94,8 @@
             => (match-lambda 
                  [(tc-result: t)
                   (register-type (car vars) t)
-                  (list (make-def-binding (car vars) t))])]
+                  (list (make-def-binding (car vars) t))]
+                 [t (int-err "~a is not a tc-result" t)])]
            [else
             (tc-error "Untyped definition : ~a" (map syntax-e vars))]))]
       

collects/typed-scheme/private/tc-utils.ss

@@ -41,6 +41,7 @@
       stx))
 
 (define (raise-typecheck-error msg stxs)
+  (printf "msg : ~a~n" msg)
   (raise (make-exn:fail:syntax (string-append "typecheck: " msg)
                                (current-continuation-marks)
                                stxs)))
@@ -58,7 +59,7 @@
      (raise-typecheck-error msg stx)]
     [l
      (let ([stxs
-            (for/list ([e (reverse delayed-errors)])
+            (for/list ([e l])
               (sync (thread (lambda () (raise-typecheck-error (err-msg e) (err-stx e)))))
               (err-stx e))])
        (reset!)
@@ -67,10 +68,13 @@
 
 (define delay-errors? (make-parameter #t))
 
-(define (tc-error/delayed msg #:stx [stx (current-orig-stx)] . rest)
+(define (tc-error/delayed msg #:stx [stx* (current-orig-stx)] . rest)
-  (if (delay-errors?)
+  (let ([stx (locate-stx stx*)])
-      (set! delayed-errors (cons (make-err (apply format msg rest) (list (locate-stx stx))) delayed-errors))
+    (unless (syntax? stx)
-      (raise-typecheck-error (apply format msg rest) (list (locate-stx stx)))))
+      (error "syntax was not syntax" stx (syntax->datum stx*)))
+    (if (delay-errors?)
+        (set! delayed-errors (cons (make-err (apply format msg rest) (list stx)) delayed-errors))
+        (raise-typecheck-error (apply format msg rest) (list stx)))))
 
 ;; produce a type error, using the current syntax
 (define (tc-error msg . rest)  

collects/typed-scheme/private/type-annotation.ss

@@ -8,11 +8,14 @@
          get-type/infer
          type-label-symbol
          type-ascrip-symbol
+         type-dotted-symbol
          type-ascription
-         check-type)
+         check-type
+         dotted?)
 
 (define type-label-symbol 'type-label)
 (define type-ascrip-symbol 'type-ascription)
+(define type-dotted-symbol 'type-dotted)
 
 (define (print-size stx)
   (syntax-case stx ()
@@ -69,10 +72,7 @@
   (parameterize
       ([current-orig-stx stx])
     (cond
-      [(type-annotation stx #:infer #t)
+      [(type-annotation stx #:infer #t)]
-       => (lambda (x) 
-            (log/ann stx x)
-            x)]
       [(not (syntax-original? stx))
        (tc-error "untyped var: ~a" (syntax-e stx))]
       [else
@@ -121,3 +121,7 @@
       (unless (subtype e-type ty)
         ;(printf "orig-stx: ~a" (syntax->datum stx*))
         (tc-error "Body had type:~n~a~nVariable had type:~n~a~n" e-type ty)))))
+
+(define (dotted? stx)
+  (cond [(syntax-property stx type-dotted-symbol) => syntax-e]
+        [else #f]))

collects/typed-scheme/private/type-environments.ss

@@ -6,6 +6,7 @@
          make-empty-env
          extend-env
          extend/values
+         dotted-env
          initial-tvar-env)
 
 (require scheme/match
@@ -23,6 +24,10 @@
 
 (define (make-empty-env p?) (make-env p? '()))
 
+;; the environment for types of ... variables
+(define dotted-env (make-parameter (make-empty-env free-identifier=?)))
+
+
 
 ;; extend that works on single arguments
 (define (extend e k v) 

collects/typed-scheme/private/type-utils.ss

@@ -4,7 +4,7 @@
          "effect-rep.ss"
          "tc-utils.ss"
          "rep-utils.ss"
-         "free-variance.ss"
+         (only-in "free-variance.ss" combine-frees)
          mzlib/plt-match
          scheme/list
          (for-syntax scheme/base))
@@ -20,7 +20,9 @@
          tc-result-equal? 
          effects-equal?
          tc-result-t
-         unfold)
+         unfold
+         (struct-out Dotted)
+         (struct-out DottedBoth))
 
 
 ;; substitute : Type Name Type -> Type
@@ -129,3 +131,7 @@
 
 ;; fv/list : Listof[Type] -> Listof[Name]
 (define (fv/list ts) (hash-map (combine-frees (map free-vars* ts)) (lambda (k v) k)))
+
+;; t is (make-F v)
+(define-struct Dotted (t))
+(define-struct (DottedBoth Dotted) ())