diff --git a/collects/typed-scheme/infer/signatures.ss b/collects/typed-scheme/infer/signatures.ss index 6db02b38dc..a3b85665f3 100644 --- a/collects/typed-scheme/infer/signatures.ss +++ b/collects/typed-scheme/infer/signatures.ss @@ -1,29 +1,42 @@ #lang scheme/base -(require scheme/unit) +(require scheme/unit scheme/contract "constraint-structs.ss" "../utils/utils.ss") +(require (rep type-rep) (utils unit-utils)) (provide (all-defined-out)) (define-signature dmap^ - (dmap-meet)) + ([cnt dmap-meet (dmap? dmap? . -> . dmap?)])) (define-signature promote-demote^ - (var-promote var-demote)) + ([cnt var-promote (Type? (listof symbol?) . -> . Type?)] + [cnt var-demote (Type? (listof symbol?) . -> . Type?)])) (define-signature constraints^ - (exn:infer? - fail-sym + ([cnt exn:infer? (any/c . -> . boolean?)] + [cnt fail-sym symbol?] ;; inference failure - masked before it gets to the user program (define-syntaxes (fail!) (syntax-rules () [(_ s t) (raise fail-sym)])) - cset-meet cset-meet* + [cnt cset-meet (cset? cset? . -> . cset?)] + [cnt cset-meet* ((listof cset?) . -> . cset?)] no-constraint - empty-cset - insert - cset-combine - c-meet)) + [cnt empty-cset ((listof symbol?) . -> . cset?)] + [cnt insert (cset? symbol? Type? Type? . -> . cset?)] + [cnt cset-combine ((listof cset?) . -> . cset?)] + [cnt c-meet ((c? c?) (symbol?) . ->* . c?)])) (define-signature restrict^ - (restrict)) + ([cnt restrict (Type? Type? . -> . Type?)])) (define-signature infer^ - (infer infer/vararg infer/dots)) + ([cnt infer (((listof symbol?) (listof Type?) (listof Type?) Type? (listof symbol?)) ((or/c #f Type?)) . ->* . any)] + [cnt infer/vararg (((listof symbol?) + (listof Type?) + (listof Type?) + Type? Type? + (listof symbol?)) + ((or/c #f Type?)) . ->* . any)] + [cnt infer/dots (((listof symbol?) + symbol? + (listof Type?) (listof Type?) Type? Type? (listof symbol?)) + (#:expected (or/c #f Type?)) . ->* . any)])) diff --git a/collects/typed-scheme/private/require-contract.ss b/collects/typed-scheme/private/require-contract.ss index c718b42fc0..bcfcc2ef0f 100644 --- a/collects/typed-scheme/private/require-contract.ss +++ b/collects/typed-scheme/private/require-contract.ss @@ -12,20 +12,20 @@ (begin define-values) [(begin (define-values (n) e) e*) #`(begin (define-values (n) e) - (define name #,(syntax-property #'e* - 'inferred-name - (syntax-e #'name))))] + (define name e*))] [(begin (begin e)) - #`(define name #,(syntax-property #'e - 'inferred-name - (syntax-e #'name)))])])) + #`(define name e)])])) (define-syntax (require/contract stx) (syntax-case stx () [(require/contract nm cnt lib) (identifier? #'nm) #`(begin (require (only-in lib [nm tmp])) - (define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))] + (define-ignored nm (contract (let ([nm cnt]) nm) tmp + '#,(syntax->datum #'nm) + 'never-happen + (list (make-srcloc tmp #f #f #f #f) (symbol->string 'nm)))))] [(require/contract (orig-nm nm) cnt lib) #`(begin (require (only-in lib [orig-nm tmp])) - (define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))])) + (define-ignored nm (contract (let ([nm cnt]) nm) + tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))])) diff --git a/collects/typed-scheme/typecheck/check-subforms-unit.ss b/collects/typed-scheme/typecheck/check-subforms-unit.ss index e37c6f3719..3dd9208d83 100644 --- a/collects/typed-scheme/typecheck/check-subforms-unit.ss +++ b/collects/typed-scheme/typecheck/check-subforms-unit.ss @@ -12,7 +12,7 @@ (export check-subforms^) ;; find the subexpressions that need to be typechecked in an ignored form -;; syntax -> void +;; syntax -> any (define (check-subforms/with-handlers form) (define handler-tys '()) (define body-ty #f) @@ -48,6 +48,7 @@ [_ (void)]))) (ret (apply Un body-ty handler-tys))) +;; syntax type -> any (define (check-subforms/with-handlers/check form expected) (let loop ([form form]) (parameterize ([current-orig-stx form]) @@ -73,7 +74,7 @@ (ret expected)) ;; typecheck the expansion of a with-handlers form -;; syntax -> type +;; syntax -> any (define (check-subforms/ignore form) (let loop ([form form]) (kernel-syntax-case* form #f () diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss index 572becfda2..530ad0094c 100644 --- a/collects/typed-scheme/typecheck/signatures.ss +++ b/collects/typed-scheme/typecheck/signatures.ss @@ -1,28 +1,49 @@ #lang scheme/base -(require scheme/unit) +(require scheme/unit scheme/contract "../utils/utils.ss") +(require (rep type-rep) + (utils unit-utils) + (private type-utils)) (provide (all-defined-out)) (define-signature typechecker^ - (type-check tc-toplevel-form)) + ([cnt type-check (syntax? . -> . syntax?)] + [cnt tc-toplevel-form (syntax? . -> . any)])) (define-signature tc-expr^ - (tc-expr tc-expr/check tc-expr/check/t check-below tc-literal tc-exprs tc-exprs/check tc-expr/t)) + ([cnt tc-expr (syntax? . -> . tc-result?)] + [cnt tc-expr/check (syntax? Type? . -> . tc-result?)] + [cnt tc-expr/check/t (syntax? Type? . -> . Type?)] + [cnt check-below (->d ([s (or/c Type? tc-result?)] [t Type?]) () [_ (if (Type? s) Type? tc-result?)])] + [cnt tc-literal (any/c . -> . Type?)] + [cnt tc-exprs ((listof syntax?) . -> . tc-result?)] + [cnt tc-exprs/check ((listof syntax?) Type? . -> . tc-result?)] + [cnt tc-expr/t (syntax? . -> . Type?)])) (define-signature check-subforms^ - (check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check)) + ([cnt check-subforms/ignore (syntax? . -> . any)] + [cnt check-subforms/with-handlers (syntax? . -> . any)] + [cnt check-subforms/with-handlers/check (syntax? Type? . -> . any)])) (define-signature tc-if^ - (tc/if-onearm tc/if-twoarm tc/if-onearm/check tc/if-twoarm/check)) + ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-result?)] + [cnt tc/if-twoarm/check (syntax? syntax? syntax? Type? . -> . tc-result?)])) (define-signature tc-lambda^ - (tc/lambda tc/lambda/check tc/rec-lambda/check)) + ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)] + [cnt tc/lambda/check (syntax? syntax? syntax? Type? . -> . tc-result?)] + [cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type?) Type? . -> . Type?)])) (define-signature tc-app^ - (tc/app tc/app/check tc/funapp)) + ([cnt tc/app (syntax? . -> . tc-result?)] + [cnt tc/app/check (syntax? Type? . -> . tc-result?)] + [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type?) . -> . tc-result?)])) (define-signature tc-let^ - (tc/let-values tc/letrec-values tc/let-values/check tc/letrec-values/check)) + ([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-result?)] + [cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-result?)] + [cnt tc/let-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)] + [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)])) (define-signature tc-dots^ - (tc/dots)) + ([cnt tc/dots (syntax? . -> . (values Type? symbol?))])) diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss index a341e184c7..739025da29 100644 --- a/collects/typed-scheme/typecheck/tc-app-unit.ss +++ b/collects/typed-scheme/typecheck/tc-app-unit.ss @@ -368,8 +368,8 @@ (let ([substitution (infer vars ... rng)]) (and substitution (log-result substitution) - (or expected - (ret (subst-all substitution rng)))))) + (ret (or expected + (subst-all substitution rng)))))) (poly-fail t argtypes #:name (and (identifier? f-stx) f-stx)))))])) (define (poly-fail t argtypes #:name [name #f]) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index 9f0831ae0b..f7769e7320 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -190,7 +190,6 @@ (begin (tc-exprs/check (syntax->list #'es) Univ) (tc-expr/check #'e expected))] ;; if - [(if tst body) (tc/if-onearm/check #'tst #'body expected)] [(if tst thn els) (tc/if-twoarm/check #'tst #'thn #'els expected)] ;; lambda [(#%plain-lambda formals . body) diff --git a/collects/typed-scheme/typecheck/tc-if-unit.ss b/collects/typed-scheme/typecheck/tc-if-unit.ss index bf3a4e43bb..cc87ca8b13 100644 --- a/collects/typed-scheme/typecheck/tc-if-unit.ss +++ b/collects/typed-scheme/typecheck/tc-if-unit.ss @@ -13,9 +13,6 @@ mzlib/trace mzlib/plt-match) -;; necessary for creating (#%app void) in tc-if/onearm -(require (for-template scheme/base)) - ;; if typechecking (import tc-expr^) (export tc-if^) @@ -88,12 +85,6 @@ ;; v cannot have type (-val #f) [(Var-True-Effect: v) (check-rest *remove (-val #f) v)]))))) -;; create a dummy else branch for typechecking -(define (tc/if-onearm tst body) (tc/if-twoarm tst body (syntax/loc body (#%app void)))) - -(define (tc/if-onearm/check tst body expected) - (tc/if-twoarm/check tst body (syntax/loc body (#%app void)) expected)) - ;; the main function (define (tc/if-twoarm tst thn els) #;(printf "tc-if/twoarm~n") diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss index 962c480e05..a4159fb63f 100644 --- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss @@ -199,16 +199,18 @@ (cons (car bodies) bodies*) (cons (syntax-len (car formals)) nums-seen))])))) +;; tc/lambda : syntax syntax-list syntax-list -> tc-result (define (tc/lambda form formals bodies) (tc/lambda/internal form formals bodies #f)) ;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic -;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> Type +;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result (define (tc/lambda/internal form formals bodies 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)))) +;; tc/lambda : syntax syntax-list syntax-list Type -> tc-result (define (tc/lambda/check form formals bodies expected) (tc/lambda/internal form formals bodies expected)) diff --git a/collects/typed-scheme/utils/unit-utils.ss b/collects/typed-scheme/utils/unit-utils.ss index 728edcd193..e5f4eb0a37 100644 --- a/collects/typed-scheme/utils/unit-utils.ss +++ b/collects/typed-scheme/utils/unit-utils.ss @@ -7,7 +7,13 @@ scheme/unit-exptime scheme/match)) -(provide define-values/link-units/infer) +(provide define-values/link-units/infer cnt) + +(define-signature-form (cnt stx) + (syntax-case stx () + [(_ nm cnt) + #;(list #'nm) + (list #'[contracted nm cnt])])) (define-syntax (define-values/link-units/infer stx) ;; construct something we can put in the imports/exports clause from the datum