From 1047f7625d2dfa53d2896fa44fde732873d86ba4 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Thu, 14 May 2009 18:57:02 +0000 Subject: [PATCH] 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 | 2 -- collects/typed-scheme/infer/infer-unit.ss | 2 +- collects/typed-scheme/private/base-env.ss | 10 ++++++---- collects/typed-scheme/rep/type-rep.ss | 13 ++++++------ .../typecheck/check-subforms-unit.ss | 5 +++-- collects/typed-scheme/typecheck/signatures.ss | 2 +- collects/typed-scheme/typecheck/tc-app.ss | 20 +++++++++++-------- .../typed-scheme/typecheck/tc-expr-unit.ss | 4 ++++ .../typecheck/tc-metafunctions.ss | 2 +- collects/typed-scheme/typed-scheme.ss | 2 +- 10 files changed, 36 insertions(+), 26 deletions(-) diff --git a/collects/typed-scheme/env/type-alias-env.ss b/collects/typed-scheme/env/type-alias-env.ss index dd9183d32c..f8506de824 100644 --- a/collects/typed-scheme/env/type-alias-env.ss +++ b/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)))]) diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss index 340550ef42..ee36c67cb5 100644 --- a/collects/typed-scheme/infer/infer-unit.ss +++ b/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)) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 2c30681288..c70355ae16 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/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 - (list ((list) (a a) . ->... . b) - (-lst a)) - (-values (list (-pair b (-val '())) N N N))))] +[time-apply (-polydots (b a) + (make-Function + (list (make-arr + (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)))] diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index 76c0144302..bcebb693da 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -10,30 +10,31 @@ (define name-table (make-weak-hasheq)) -(define Type/c - (flat-named-contract - 'Type +(define Type/c? (λ (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)))) diff --git a/collects/typed-scheme/typecheck/check-subforms-unit.ss b/collects/typed-scheme/typecheck/check-subforms-unit.ss index 3e93d5eaa3..3ab084dc2e 100644 --- a/collects/typed-scheme/typecheck/check-subforms-unit.ss +++ b/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 diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss index f50e5f923e..c8a5eeb528 100644 --- a/collects/typed-scheme/typecheck/signatures.ss +++ b/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?)] diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index 1accdc8f71..6f92e70b1a 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/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)) - (Function: (list (and arrs (arr: doms rngs (and #f rests) (cons dtys dbounds) '())) ...))))) + (and vars (list fixed-vars ... dotted-var)) + (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)) - "Cannot apply expression of type ~a, since it is not a function type" f-ty)])) + [((tc-result1: 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]) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index cb55d1abaf..6661dd7f49 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/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)) diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss index 6487fb093b..1a1d17c22a 100644 --- a/collects/typed-scheme/typecheck/tc-metafunctions.ss +++ b/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 diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss index 5646b76a53..e9249d8723 100644 --- a/collects/typed-scheme/typed-scheme.ss +++ b/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