From c6f2b2d5178b85e0f961f37f2ae4f0e650c7fb3c Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 6 May 2008 00:42:28 +0000 Subject: [PATCH] Remove unneccessary requires. Fix let checking to use annotations as the expected type for the RHS. Fix bug in use of expected types in inference. svn: r9674 --- collects/typed-scheme/private/base-env.ss | 2 +- collects/typed-scheme/private/infer-ops.ss | 14 +++---- collects/typed-scheme/private/signatures.ss | 2 +- collects/typed-scheme/private/tc-app-unit.ss | 11 +---- collects/typed-scheme/private/tc-expr-unit.ss | 4 ++ collects/typed-scheme/private/tc-let-unit.ss | 21 ++++------ collects/typed-scheme/private/tc-toplevel.ss | 5 +-- collects/typed-scheme/private/tc-utils.ss | 7 ++++ .../typed-scheme/private/type-annotation.ss | 42 ++++++++++++------- collects/typed-scheme/typed-reader.ss | 2 - 10 files changed, 58 insertions(+), 52 deletions(-) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index a9ba1625cd..21ee9fd206 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -483,7 +483,7 @@ ))) (begin-for-syntax - ;(printf "running base-env~n") + #;(printf "running base-env~n") (initialize-type-env initial-env) (initialize-others)) diff --git a/collects/typed-scheme/private/infer-ops.ss b/collects/typed-scheme/private/infer-ops.ss index 69a3268987..5e9dbffe69 100644 --- a/collects/typed-scheme/private/infer-ops.ss +++ b/collects/typed-scheme/private/infer-ops.ss @@ -271,18 +271,18 @@ ;; returns a substitution ;; if R is #f, we don't care about the substituion ;; just return a boolean result -(define (infer X S T R) - (with-handlers ([exn:infer? (lambda _ #f)]) +(define (infer X S T R [expected #f]) + (with-handlers ([exn:infer? (lambda _ #f)]) (let ([cs (cgen/list X null S T)]) - (if R - (subst-gen cs R) - #t)))) + (if (not expected) + (subst-gen cs R) + (cset-meet cs (cgen null X R expected)))))) ;; like infer, but T-var is the vararg type: -(define (infer/vararg X S T T-var R) +(define (infer/vararg X S T T-var R [expected #f]) (define new-T (extend S T T-var)) (and ((length S) . >= . (length T)) - (infer X S new-T R))) + (infer X S new-T R expected))) ;; Listof[A] Listof[B] B -> Listof[B] ;; pads out t to be as long as s diff --git a/collects/typed-scheme/private/signatures.ss b/collects/typed-scheme/private/signatures.ss index d2c72d75ad..d028b717a7 100644 --- a/collects/typed-scheme/private/signatures.ss +++ b/collects/typed-scheme/private/signatures.ss @@ -22,7 +22,7 @@ (type-check tc-toplevel-form)) (define-signature tc-expr^ - (tc-expr tc-expr/check check-below tc-literal tc-exprs tc-exprs/check tc-expr/t #;check-expr)) + (tc-expr tc-expr/check tc-expr/check/t check-below tc-literal tc-exprs tc-exprs/check tc-expr/t #;check-expr)) (define-signature check-subforms^ (check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check)) diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss index 1f19cd4d6d..a3c8bf2313 100644 --- a/collects/typed-scheme/private/tc-app-unit.ss +++ b/collects/typed-scheme/private/tc-app-unit.ss @@ -195,12 +195,6 @@ [f-ty (tc-error/expr #:return (ret (Un)) "Type of argument to apply is not a function type: ~n~a" f-ty)])))) -(define (stringify l [between " "]) - (define (intersperse v l) - (cond [(null? l) null] - [(null? (cdr l)) l] - [else (cons (car l) (cons v (intersperse v (cdr l))))])) - (apply string-append (intersperse between (map (lambda (s) (format "~a" s)) l)))) (define (tc/funapp f-stx args-stx ftype0 argtys expected) (match-let* ([(list (tc-result: argtypes arg-thn-effs arg-els-effs) ...) argtys]) @@ -267,8 +261,7 @@ (stringify (map stringify msg-doms) "\n") (stringify argtypes))))] [(and (= (length (car doms*)) (length argtypes)) - (infer (fv/list (car doms*)) argtypes (car doms*) (if expected #f (car rngs*))) - #;(infer/list (car doms*) argtypes vars)) + (infer (fv/list (cons (car rngs*) (car doms*))) argtypes (car doms*) (car rngs*) expected)) => (lambda (substitution) (or expected (let* ([s (lambda (t) (subst-all substitution t))] @@ -298,7 +291,7 @@ (unless (<= (length dom) (length argtypes)) (tc-error "incorrect number of arguments to function: ~a ~a" dom argtypes)) (let ([substitution - (infer/vararg vars argtypes dom rest (if expected #f rng))]) + (infer/vararg vars argtypes dom rest rng expected)]) (cond [(and expected substitution) expected] [substitution diff --git a/collects/typed-scheme/private/tc-expr-unit.ss b/collects/typed-scheme/private/tc-expr-unit.ss index c68b0e2f02..b9a48725c7 100644 --- a/collects/typed-scheme/private/tc-expr-unit.ss +++ b/collects/typed-scheme/private/tc-expr-unit.ss @@ -87,6 +87,10 @@ (define (tc-expr/t e) (match (tc-expr e) [(tc-result: t) t])) +(define (tc-expr/check/t e t) + (match (tc-expr/check e t) + [(tc-result: t) t])) + (define (check-below tr1 expected) (match (list tr1 expected) [(list (tc-result: t1 te1 ee1) t2) diff --git a/collects/typed-scheme/private/tc-let-unit.ss b/collects/typed-scheme/private/tc-let-unit.ss index aec3ad4175..953eebfd52 100644 --- a/collects/typed-scheme/private/tc-let-unit.ss +++ b/collects/typed-scheme/private/tc-let-unit.ss @@ -24,8 +24,6 @@ (export tc-let^) (define (do-check expr->type namess types form exprs body clauses expected) - ;; just for error reporting - #;(define clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])) ;; extend the lexical environment for checking the body (with-lexical-env/extend ;; the list of lists of name @@ -104,16 +102,13 @@ ;; if none of the names bound in the letrec are free vars of this rhs [(not (ormap (lambda (n) (s:member n flat-names bound-identifier=?)) (free-vars (car exprs)))) ;; then check this expression separately - (let ([t (tc-expr/maybe-expected/t (car exprs) (car names))]) - (with-lexical-env/extend - (list (car names)) - (list (get-type/infer (car names) t)) - (loop (cdr names) (cdr exprs) (apply append (cdr names)) (cdr clauses))))] + (with-lexical-env/extend + (list (car names)) + (list (get-type/infer (car names) (car exprs) (lambda (e) (tc-expr/maybe-expected/t e (car names))) tc-expr/check/t)) + (loop (cdr names) (cdr exprs) (apply append (cdr names)) (cdr clauses)))] [else ;(for-each (lambda (vs) (for-each (lambda (v) (printf/log "Letrec Var: ~a~n" (syntax-e v))) vs)) names) - (do-check (lambda (stx e t) - (match (tc-expr/check e t) - [(tc-result: t) t])) + (do-check (lambda (stx e t) (tc-expr/check/t e t)) names (map (lambda (l) (map get-type l)) names) form exprs body clauses expected)])))) ;; this is so match can provide us with a syntax property to @@ -133,12 +128,12 @@ ;; all the trailing expressions - the ones actually bound to the names [exprs (syntax->list exprs)] ;; the types of the exprs - [inferred-types (map (tc-expr-t/maybe-expected expected) exprs)] + #;[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)] ;; the annotated types of the name (possibly using the inferred types) - [types (map get-type/infer names inferred-types)] + [types (for/list ([name names] [e exprs]) (get-type/infer name e (tc-expr-t/maybe-expected expected) tc-expr/check/t))] ;; the clauses for error reporting [clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])]) - (do-check check-type names types form inferred-types body clauses expected))) + (do-check void names types form types body clauses expected))) (define (tc/let-values/check namess exprs body form expected) (tc/let-values/internal namess exprs body form expected)) diff --git a/collects/typed-scheme/private/tc-toplevel.ss b/collects/typed-scheme/private/tc-toplevel.ss index 20ae12e9df..917f7532f3 100644 --- a/collects/typed-scheme/private/tc-toplevel.ss +++ b/collects/typed-scheme/private/tc-toplevel.ss @@ -3,7 +3,7 @@ (require syntax/kerncase mzlib/etc - mzlib/plt-match + scheme/match "signatures.ss" "tc-structs.ss" "type-utils.ss" @@ -21,11 +21,8 @@ "provide-handling.ss" "type-alias-env.ss" "type-contract.ss" - ;(only-in "prims.ss" :) (for-template - ;(only-in "prims.ss" :) "internal-forms.ss" - "tc-utils.ss" (lib "contract.ss") scheme/base)) diff --git a/collects/typed-scheme/private/tc-utils.ss b/collects/typed-scheme/private/tc-utils.ss index 5a01f647ac..7ac1390e78 100644 --- a/collects/typed-scheme/private/tc-utils.ss +++ b/collects/typed-scheme/private/tc-utils.ss @@ -7,6 +7,13 @@ (define orig-module-stx (make-parameter #f)) (define expanded-module-stx (make-parameter #f)) +(define (stringify l [between " "]) + (define (intersperse v l) + (cond [(null? l) null] + [(null? (cdr l)) l] + [else (cons (car l) (cons v (intersperse v (cdr l))))])) + (apply string-append (intersperse between (map (lambda (s) (format "~a" s)) l)))) + ;; helper function, not currently used (define (find-origin stx) (cond [(syntax-property stx 'origin) => (lambda (orig) diff --git a/collects/typed-scheme/private/type-annotation.ss b/collects/typed-scheme/private/type-annotation.ss index a30d4ff091..f18d107f5e 100644 --- a/collects/typed-scheme/private/type-annotation.ss +++ b/collects/typed-scheme/private/type-annotation.ss @@ -1,7 +1,7 @@ #lang scheme/base (require "type-rep.ss" "parse-type.ss" "tc-utils.ss" "subtype.ss" "utils.ss" "union.ss" "resolve-type.ss" - "type-env.ss") + "type-env.ss" "type-effect-convenience.ss") (require (lib "plt-match.ss") mzlib/trace) (provide type-annotation @@ -76,22 +76,34 @@ ;; get the type annotations on this list of identifiers ;; if not all identifiers have annotations, return the supplied inferred type ;; list[identifier] type -> list[type] -(define (get-type/infer stxs e-type) - (match (list stxs e-type) - [(list '() (Values: '())) (list)] - [(list (list stx ...) (Values: (list ty ...))) - (map (lambda (stx ty) - (cond [(type-annotation stx) => (lambda (ann) (check-type stx ty ann) (log/extra stx ty ann) ann)] - [else (log/noann stx ty) ty])) - stx ty)] - [(list (list stx) ty) +(define (get-type/infer stxs expr tc-expr tc-expr/check) + (match stxs + ['() + (tc-expr/check expr (-values null)) + (list)] + [(list stx) (cond [(type-annotation stx #:infer #t) => (lambda (ann) - (check-type stx ty ann) - (log/extra stx ty ann) - (list ann))] - [else (log/noann stx ty) (list ty)])] - [else (int-err "wrong type arity - get-type/infer ~a ~a" stxs e-type)])) + (list (tc-expr/check expr ann)))] + [else (list (tc-expr expr))])] + [(list stx ...) + (let ([anns (for/list ([s stxs]) (type-annotation s #:infer #t))]) + (if (for/and ([a anns]) a) + (begin (tc-expr/check expr (-values anns)) anns) + (let ([ty (tc-expr expr)]) + (match ty + [(Values: tys) + (if (not (= (length stxs) (length tys))) + (tc-error/delayed #:ret (map (lambda _ (Un)) stxs) + "Expression should produce ~a values, but produces ~a values of types ~a" + (length stxs) (length tys) (stringify tys)) + (map (lambda (stx ty) + (cond [(type-annotation stx #:infer #t) => (lambda (ann) (check-type stx ty ann) (log/extra stx ty ann) ann)] + [else (log/noann stx ty) ty])) + stxs tys))] + [ty (tc-error/delayed #:ret (map (lambda _ (Un)) stxs) + "Expression should produce ~a values, but produces one values of type " + (length stxs) ty)]))))])) ;; check that e-type is compatible with ty in context of stx diff --git a/collects/typed-scheme/typed-reader.ss b/collects/typed-scheme/typed-reader.ss index 7a14a18b61..ebce71356a 100644 --- a/collects/typed-scheme/typed-reader.ss +++ b/collects/typed-scheme/typed-reader.ss @@ -1,7 +1,5 @@ #lang scheme/base -(require (for-template "private/prims.ss")) - ;; Provides raise-read-error and raise-read-eof-error (require syntax/readerr)