diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index d11d5a64db..95df2174fa 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -492,7 +492,7 @@ [identifier? (make-pred-ty (-Syntax Sym))] [syntax? (make-pred-ty (-Syntax Univ))] [syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a)) - (-> (-Syntax Univ) Univ Univ)))] + (-> (-Syntax Univ) Univ Univ)))] ))) (begin-for-syntax diff --git a/collects/typed-scheme/private/infer-unit.ss b/collects/typed-scheme/private/infer-unit.ss index b46fd0986e..4994d50e37 100644 --- a/collects/typed-scheme/private/infer-unit.ss +++ b/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 diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 5565a9d9d9..686bd2b17f 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/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 () diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss index 2390e0f519..80facd1e9d 100644 --- a/collects/typed-scheme/private/prims.ss +++ b/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)) diff --git a/collects/typed-scheme/private/syntax-traversal.ss b/collects/typed-scheme/private/syntax-traversal.ss index 247e91f258..ef0eeed44d 100644 --- a/collects/typed-scheme/private/syntax-traversal.ss +++ b/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)] - [syntax-locs (make-hash)]) - ;; find all syntax locations in original code - (let loop ([stx orig]) - (when (syntax? stx) (hash-set! syntax-locs (syntax-loc stx) stx)) - (let ([stx (if (syntax? stx) (syntax-e stx) stx)]) - (when (pair? stx) (loop (car stx)) (loop (cdr stx))))) - (or - ;; we just might get a lookfor that is already in the original - (and (eq? src (syntax-source lookfor)) - (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 - (and enclosing - (begin0 - (ormap (lambda (enc) (hash-ref syntax-locs (syntax-loc enc) #f)) - enclosing) - #;(printf "chose branch two ~a~n" enclosing)))))) + (let ([enclosing (enclosing-syntaxes-with-source expanded lookfor src)] + [syntax-locs (make-hash)]) + ;; find all syntax locations in original code + (let loop ([stx orig]) + (when (syntax? stx) (hash-set! syntax-locs (syntax-loc stx) stx)) + (let ([stx (if (syntax? stx) (syntax-e stx) stx)]) + (when (pair? stx) (loop (car stx)) (loop (cdr stx))))) + (or + ;; we just might get a lookfor that is already in the original + (and (eq? src (syntax-source lookfor)) + (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 + (and enclosing + (begin0 + (ormap (lambda (enc) (hash-ref syntax-locs (syntax-loc enc) #f)) + enclosing) + #;(printf "chose branch two ~a~n" enclosing)))))) ;(trace look-for-in-orig) diff --git a/collects/typed-scheme/private/tc-lambda-unit.ss b/collects/typed-scheme/private/tc-lambda-unit.ss index ddb2ff8e78..4f5f943e76 100644 --- a/collects/typed-scheme/private/tc-lambda-unit.ss +++ b/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)] - [rest-type (get-type #'rest)]) + [arg-types (map get-type arg-list)]) (for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) (cons #'rest arg-list)) - (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))))])) + (cond + [(dotted? #'rest) + => + (lambda (bound) + (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)]) - (map syntax-e (syntax->list p)))] - [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)))] - [_ (tc-error/expr #:return expected "Expected a value of type ~a, but got a polymorphic function." expected)])) + (match (map syntax-e (syntax->list (syntax-property form 'typechecker:plambda))) + [(list tvars ... dotted-var '...) + (let* ([literal-tvars tvars] + [new-tvars (map make-F literal-tvars)] + [ty (parameterize ([current-tvars (extend-env (cons dotted-var literal-tvars) + (cons (make-Dotted (make-F dotted-var)) new-tvars) + (current-tvars))]) + (tc/mono-lambda formals bodies #f))]) + (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)]) diff --git a/collects/typed-scheme/private/tc-toplevel.ss b/collects/typed-scheme/private/tc-toplevel.ss index a681733716..5cc6cf1302 100644 --- a/collects/typed-scheme/private/tc-toplevel.ss +++ b/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))]))] diff --git a/collects/typed-scheme/private/tc-utils.ss b/collects/typed-scheme/private/tc-utils.ss index 992bc5cdbf..c2d654ba0c 100644 --- a/collects/typed-scheme/private/tc-utils.ss +++ b/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) - (if (delay-errors?) - (set! delayed-errors (cons (make-err (apply format msg rest) (list (locate-stx stx))) delayed-errors)) - (raise-typecheck-error (apply format msg rest) (list (locate-stx stx))))) +(define (tc-error/delayed msg #:stx [stx* (current-orig-stx)] . rest) + (let ([stx (locate-stx stx*)]) + (unless (syntax? 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) diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss index d9875ef45e..ec2140682c 100644 --- a/collects/typed-scheme/private/type-annotation.ss +++ b/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-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) - => (lambda (x) - (log/ann stx x) - x)] + [(type-annotation stx #:infer #t)] [(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])) \ No newline at end of file diff --git a/collects/typed-scheme/private/type-environments.ss b/collects/typed-scheme/private/type-environments.ss index c9cc315f9c..f399bed4fa 100644 --- a/collects/typed-scheme/private/type-environments.ss +++ b/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) diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss index 621f6aabbd..21b4c5f532 100644 --- a/collects/typed-scheme/private/type-utils.ss +++ b/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) ()) \ No newline at end of file