diff --git a/collects/tests/typed-scheme/fail/struct-provide.ss b/collects/tests/typed-scheme/fail/struct-provide.ss new file mode 100644 index 00000000..2e4f65b7 --- /dev/null +++ b/collects/tests/typed-scheme/fail/struct-provide.ss @@ -0,0 +1,11 @@ +#; +(exn-pred exn:fail:syntax? #rx".*typed module.*") +#lang scheme/load + +(module m typed-scheme + (define-struct: q ()) + (provide (all-defined-out))) + +(module n scheme + (require 'm) + q) diff --git a/collects/tests/typed-scheme/succeed/rts-prov.ss b/collects/tests/typed-scheme/succeed/rts-prov.ss new file mode 100644 index 00000000..a900b54e --- /dev/null +++ b/collects/tests/typed-scheme/succeed/rts-prov.ss @@ -0,0 +1,14 @@ +#lang scheme/load + +(module l scheme + (define-struct q ()) + (provide (all-defined-out))) + +(module m typed-scheme + (require-typed-struct q () 'l) + (provide (all-defined-out))) + +(module n typed-scheme + (require 'm) + (: f q) + (define f (make-q))) diff --git a/collects/typed-scheme/env/type-name-env.ss b/collects/typed-scheme/env/type-name-env.ss index 374a2368..4c35e9d6 100644 --- a/collects/typed-scheme/env/type-name-env.ss +++ b/collects/typed-scheme/env/type-name-env.ss @@ -3,12 +3,15 @@ (require syntax/boundmap mzlib/trace + (env type-alias-env) (utils tc-utils) + (rep type-rep) (types utils)) (provide register-type-name lookup-type-name register-type-names + add-alias type-name-env-map) ;; a mapping from id -> type (where id is the name of the type) @@ -42,3 +45,7 @@ ;; (id type -> T) -> listof[T] (define (type-name-env-map f) (module-identifier-mapping-map the-mapping f)) + +(define (add-alias from to) + (when (lookup-type-name to (lambda () #f)) + (register-resolved-type-alias from (make-Name to)))) \ No newline at end of file diff --git a/collects/typed-scheme/typecheck/provide-handling.ss b/collects/typed-scheme/typecheck/provide-handling.ss index d3fb28c9..791d6384 100644 --- a/collects/typed-scheme/typecheck/provide-handling.ss +++ b/collects/typed-scheme/typecheck/provide-handling.ss @@ -3,6 +3,7 @@ (require (except-in "../utils/utils.ss" extend)) (require (only-in srfi/1/list s:member) syntax/kerncase syntax/boundmap + (env type-name-env type-alias-env) mzlib/trace (private type-contract) (rep type-rep) @@ -73,7 +74,9 @@ #`(begin (define-syntax export-id (if (unbox typed-context?) - (make-rename-transformer #'id) + (begin + (add-alias #'export-id #'id) + (make-rename-transformer #'id)) (lambda (stx) (tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id))))) (provide (rename-out [export-id out-id]))))))] diff --git a/collects/typed-scheme/typecheck/signatures.ss b/collects/typed-scheme/typecheck/signatures.ss index 76c69b1b..c68b5e95 100644 --- a/collects/typed-scheme/typecheck/signatures.ss +++ b/collects/typed-scheme/typecheck/signatures.ss @@ -10,13 +10,13 @@ [cnt tc-toplevel-form (syntax? . -> . any)])) (define-signature tc-expr^ - ([cnt tc-expr (syntax? . -> . tc-result?)] - [cnt tc-expr/check (syntax? Type/c . -> . tc-result?)] + ([cnt tc-expr (syntax? . -> . tc-results?)] + [cnt tc-expr/check (syntax? tc-results? . -> . tc-results?)] [cnt tc-expr/check/t (syntax? Type/c . -> . Type/c)] - [cnt check-below (->d ([s (or/c Type/c tc-result?)] [t Type/c]) () [_ (if (Type/c s) Type/c tc-result?)])] - [cnt tc-literal (any/c . -> . Type/c)] - [cnt tc-exprs ((listof syntax?) . -> . tc-result?)] - [cnt tc-exprs/check ((listof syntax?) Type/c . -> . tc-result?)] + [cnt check-below (->d ([s (or/c Type/c tc-results?)] [t (or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])] + ;[cnt tc-literal (any/c . -> . Type/c)] + [cnt tc-exprs ((listof syntax?) . -> . tc-results?)] + [cnt tc-exprs/check ((listof syntax?) Type/c . -> . tc-results?)] [cnt tc-expr/t (syntax? . -> . Type/c)])) (define-signature check-subforms^ @@ -25,24 +25,24 @@ [cnt check-subforms/with-handlers/check (syntax? Type/c . -> . any)])) (define-signature tc-if^ - ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-result?)] - [cnt tc/if-twoarm/check (syntax? syntax? syntax? Type/c . -> . tc-result?)])) + ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-results?)] + [cnt tc/if-twoarm/check (syntax? syntax? syntax? Type/c . -> . tc-results?)])) (define-signature tc-lambda^ - ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)] - [cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-result?)] + ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-results?)] + [cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-results?)] [cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type/c) Type/c . -> . Type/c)])) (define-signature tc-app^ - ([cnt tc/app (syntax? . -> . tc-result?)] - [cnt tc/app/check (syntax? Type/c . -> . tc-result?)] - [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type/c) . -> . tc-result?)])) + ([cnt tc/app (syntax? . -> . tc-results?)] + [cnt tc/app/check (syntax? tc-results? . -> . tc-results?)] + [cnt tc/funapp (syntax? syntax? tc-result? (listof tc-results?) (or/c #f Type/c) . -> . tc-results?)])) (define-signature tc-let^ - ([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/c . -> . tc-result?)] - [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type/c . -> . tc-result?)])) + ([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-results?)] + [cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-results?)] + [cnt tc/let-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)] + [cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? tc-results? . -> . tc-results?)])) (define-signature tc-dots^ ([cnt tc/dots (syntax? . -> . (values Type/c symbol?))])) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index d83daf0d..ae1ebf76 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -3,7 +3,7 @@ (require (rename-in "../utils/utils.ss" [private private-in])) (require syntax/kerncase - scheme/match + scheme/match (prefix-in - scheme/contract) "signatures.ss" (types utils convenience union subtype) (private-in parse-type type-annotation) @@ -23,7 +23,8 @@ ;; return the type of a literal value ;; scheme-value -> type -(define (tc-literal v-stx [expected #f]) +(d/c (tc-literal v-stx [expected #f]) + (-->* (syntax?) ((-or/c #f Type/c)) Type/c) (define-syntax-class exp (pattern i #:when expected @@ -45,7 +46,7 @@ [(i ...) (-Tuple (map tc-literal (syntax->list #'(i ...))))] [i #:declare i (3d vector?) - (make-Vector (apply Un (map tc-literal (vector->list #'i.datum))))] + (make-Vector (apply Un (map tc-literal (vector->list #'i.datum))))] [_ Univ])) @@ -120,15 +121,20 @@ (match (tc-expr/check e t) [(tc-result: t) t])) -;; check-below : (/\ (Result Type -> Result) +;; check-below : (/\ (Results Type -> Result) +;; (Results Results -> Result) ;; (Type Type -> Type)) (define (check-below tr1 expected) - (match (list tr1 expected) - [(list (tc-result: t1 te1 ee1) t2) + (match* (tr1 expected) + [((tc-results: t1) (tc-results: t2)) + (unless (andmap subtype t1 t2) + (tc-error/expr "Expected ~a, but got ~a" t2 t1)) + (ret expected)] + [((tc-result1: t1) (? Type? t2)) (unless (subtype t1 t2) (tc-error/expr "Expected ~a, but got ~a" t2 t1)) (ret expected)] - [(list t1 t2) + [((? Type? t1) (? Type? t2)) (unless (subtype t1 t2) (tc-error/expr"Expected ~a, but got ~a" t2 t1)) expected])) @@ -159,7 +165,9 @@ ;; data [(quote #f) (ret (-val #f) false-filter)] [(quote #t) (ret (-val #t) true-filter)] - [(quote val) (ret (tc-literal #'val expected))] + [(quote val) (match expected + [(tc-result1: t) + (ret (tc-literal #'val t))])] ;; syntax [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))] ;; mutation! @@ -314,9 +322,9 @@ (tc-expr/check form ann))] [else (internal-tc-expr form)])]) (match ty - [(tc-result: t eff1 eff2) - (let ([ty* (do-inst form t)]) - (ret ty* eff1 eff2))])))) + [(tc-results: ts fs os) + (let ([ts* (do-inst form ts)]) + (ret ts fs os))])))) (define (tc/send rcvr method args [expected #f]) (match (tc-expr rcvr) diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss index d443fd77..c6dbd984 100644 --- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss @@ -19,10 +19,10 @@ (import tc-expr^) (export tc-lambda^) -(d-s/c lam-result ([args (listof (list identifier? Type/c))] - [kws (listof (list keyword? identifier? Type/c boolean?))] +(d-s/c lam-result ([args (listof (list/c identifier? Type/c))] + [kws (listof (list/c keyword? identifier? Type/c boolean?))] [rest (or/c #f Type/c)] - [drest (or/c #f (cons symbol? Type/c))] + [drest (or/c #f (cons/c symbol? Type/c))] [body tc-results?]) #:transparent) diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss index 08bd1e87..4c6b019b 100644 --- a/collects/typed-scheme/typecheck/tc-structs.ss +++ b/collects/typed-scheme/typecheck/tc-structs.ss @@ -131,11 +131,13 @@ (map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent) null))) (register-type-name nm (wrapper sty)) - (for/list ([e bindings]) - (let ([nm (car e)] - [t (cdr e)]) - (register-type nm t) - (make-def-binding nm t)))) + (cons + (make-def-stx-binding nm) + (for/list ([e bindings]) + (let ([nm (car e)] + [t (cdr e)]) + (register-type nm t) + (make-def-binding nm t))))) ;; check and register types for a polymorphic define struct ;; tc/poly-struct : Listof[identifier] (U identifier (list identifier identifier)) Listof[identifier] Listof[syntax] -> void diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss index 937568aa..fce1a1a3 100644 --- a/collects/typed-scheme/typecheck/tc-toplevel.ss +++ b/collects/typed-scheme/typecheck/tc-toplevel.ss @@ -161,7 +161,7 @@ [(define-values (var ...) expr) (let* ([vars (syntax->list #'(var ...))] [ts (map lookup-type vars)]) - (tc-expr/check #'expr (-values ts))) + (tc-expr/check #'expr (ret ts))) (void)] ;; to handle the top-level, we have to recur into begins diff --git a/collects/typed-scheme/typecheck/typechecker.ss b/collects/typed-scheme/typecheck/typechecker.ss index ed935ff9..2f41a66a 100644 --- a/collects/typed-scheme/typecheck/typechecker.ss +++ b/collects/typed-scheme/typecheck/typechecker.ss @@ -5,11 +5,11 @@ mzlib/trace (only-in scheme/unit provide-signature-elements) "signatures.ss" "tc-toplevel.ss" - "tc-if-unit.ss" "tc-lambda-unit.ss" "tc-app-unit.ss" + "tc-new-if.ss" "tc-lambda-unit.ss" "tc-new-app-unit.ss" "tc-let-unit.ss" "tc-dots-unit.ss" "tc-expr-unit.ss" "check-subforms-unit.ss") (provide-signature-elements typechecker^ tc-expr^) (define-values/link-units/infer - tc-toplevel@ tc-if@ tc-lambda@ tc-dots@ tc-app@ tc-let@ tc-expr@ check-subforms@) + tc-toplevel@ tc-new-if@ tc-lambda@ tc-dots@ tc-new-app@ tc-let@ tc-expr@ check-subforms@) diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss index 0c4af4ee..facbcf88 100644 --- a/collects/typed-scheme/types/utils.ss +++ b/collects/typed-scheme/types/utils.ss @@ -180,7 +180,12 @@ [(_ tp fp op dty dbound) #'(struct tc-results ((list (struct tc-result (tp fp op)) (... ...)) (cons dty dbound)))] [(_ tp) #'(struct tc-results ((list (struct tc-result (tp _ _)) (... ...)) #f))])) -(provide tc-result: tc-results: tc-result? tc-results?) +(define-match-expander tc-result1: + (syntax-parser + [(_ tp fp op) #'(struct tc-results ((list (struct tc-result (tp fp op))) #f))] + [(_ tp) #'(struct tc-results ((list (struct tc-result (tp _ _))) #f))])) + +(provide tc-result: tc-results: tc-result1: tc-result? tc-results?) ;; convenience function for returning the result of typechecking an expression (define ret @@ -214,7 +219,7 @@ [o (if (list? t) (listof Object?) Object?)]) - [_ (listof tc-result?)])]) + [_ tc-results?])]) (define (subst v t e) (substitute t v e))