diff --git a/collects/tests/typed-scheme/fail/with-type1.ss b/collects/tests/typed-scheme/fail/with-type1.ss new file mode 100644 index 00000000..4acf56ae --- /dev/null +++ b/collects/tests/typed-scheme/fail/with-type1.ss @@ -0,0 +1,8 @@ +#; +(exn-pred exn:fail:contract?) +#lang scheme +(require typed/scheme) + +((with-type (Number -> Number) + (lambda: ([x : Number]) (add1 x))) + #f) diff --git a/collects/tests/typed-scheme/fail/with-type2.ss b/collects/tests/typed-scheme/fail/with-type2.ss new file mode 100644 index 00000000..75824a07 --- /dev/null +++ b/collects/tests/typed-scheme/fail/with-type2.ss @@ -0,0 +1,10 @@ +#; +(exn-pred exn:fail:contract?) +#lang scheme + +(require typed/scheme) + +(let ([x 'hello]) + (with-type String + #:freevars ([x String]) + (string-append x ", world"))) \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/with-type.ss b/collects/tests/typed-scheme/succeed/with-type.ss new file mode 100644 index 00000000..2ce8853d --- /dev/null +++ b/collects/tests/typed-scheme/succeed/with-type.ss @@ -0,0 +1,9 @@ +#lang scheme +(require typed/scheme) + +(with-type Number 3) + +(let ([x "hello"]) + (with-type String + #:freevars ([x String]) + (string-append x ", world"))) diff --git a/collects/typed-scheme/env/type-env.ss b/collects/typed-scheme/env/type-env.ss index 7aaf08ac..8521f8ec 100644 --- a/collects/typed-scheme/env/type-env.ss +++ b/collects/typed-scheme/env/type-env.ss @@ -1,7 +1,7 @@ #lang scheme/base (require "../utils/utils.ss" - syntax/boundmap + syntax/id-table (utils tc-utils) (types utils)) @@ -11,21 +11,22 @@ register-type/undefined lookup-type register-types + unregister-type check-all-registered-types type-env-map) -;; module-identifier-mapping from id -> type or Box[type] +;; free-id-table from id -> type or Box[type] ;; where id is a variable, and type is the type of the variable ;; if the result is a box, then the type has not actually been defined, just registered -(define the-mapping (make-module-identifier-mapping)) +(define the-mapping (make-free-id-table)) ;; add a single type to the mapping ;; identifier type -> void (define (register-type id type) - (module-identifier-mapping-put! the-mapping id type)) + (free-id-table-set! the-mapping id type)) (define (register-type-if-undefined id type) - (if (module-identifier-mapping-get the-mapping id (lambda _ #f)) + (if (free-id-table-ref the-mapping id (lambda _ #f)) (tc-error/stx id "Duplicate type annotation for ~a" (syntax-e id)) (register-type id type))) @@ -33,9 +34,9 @@ ;; identifier type -> void (define (register-type/undefined id type) ;(printf "register-type/undef ~a~n" (syntax-e id)) - (if (module-identifier-mapping-get the-mapping id (lambda _ #f)) + (if (free-id-table-ref the-mapping id (lambda _ #f)) (tc-error/stx id "Duplicate type annotation for ~a" (syntax-e id)) - (module-identifier-mapping-put! the-mapping id (box type)))) + (free-id-table-set! the-mapping id (box type)))) ;; add a bunch of types to the mapping ;; listof[id] listof[type] -> void @@ -46,21 +47,24 @@ ;; if none found, calls lookup-fail ;; identifier -> type (define (lookup-type id [fail-handler (lambda () (lookup-type-fail id))]) - (let ([v (module-identifier-mapping-get the-mapping id fail-handler)]) + (let ([v (free-id-table-ref the-mapping id fail-handler)]) (if (box? v) (unbox v) v))) (define (maybe-finish-register-type id) - (let ([v (module-identifier-mapping-get the-mapping id)]) + (let ([v (free-id-table-ref the-mapping id)]) (if (box? v) (register-type id (unbox v)) #f))) +(define (unregister-type id) + (free-id-table-remove! the-mapping id)) + (define (finish-register-type id) (unless (maybe-finish-register-type id) (tc-error/stx id "Duplicate defintion for ~a" (syntax-e id)))) (define (check-all-registered-types) - (module-identifier-mapping-for-each + (free-id-table-for-each the-mapping (lambda (id e) (when (box? e) @@ -74,4 +78,4 @@ ;; map over the-mapping, producing a list ;; (id type -> T) -> listof[T] (define (type-env-map f) - (module-identifier-mapping-map the-mapping f)) + (free-id-table-map the-mapping f)) diff --git a/collects/typed-scheme/main.ss b/collects/typed-scheme/main.ss index a072bfdb..1ce6926e 100644 --- a/collects/typed-scheme/main.ss +++ b/collects/typed-scheme/main.ss @@ -18,4 +18,4 @@ (for-syntax "private/base-types-extra.ss")) (provide (rename-out [with-handlers: with-handlers] [real? number?]) (for-syntax (all-from-out "private/base-types-extra.ss")) - assert) + assert with-type) diff --git a/collects/typed-scheme/private/with-types.ss b/collects/typed-scheme/private/with-types.ss new file mode 100644 index 00000000..dfaf470f --- /dev/null +++ b/collects/typed-scheme/private/with-types.ss @@ -0,0 +1,93 @@ +#lang scheme/base + +(require (for-syntax scheme/base syntax/parse mzlib/etc scheme/match) + scheme/require + "base-env.ss" + "base-special-env.ss" + "base-env-numeric.ss" + "base-env-indexing-old.ss" + "extra-procs.ss" + "prims.ss" + "base-types.ss" + scheme/contract/regions scheme/contract/base + (for-syntax "base-types-extra.ss") + (for-syntax (except-in (path-up "utils/utils.ss") infer) + (path-up "utils/tc-utils.ss") + (except-in (combine-in (path-up "types/convenience.ss") (path-up "types/abbrev.ss")) ->) + (path-up "types/utils.ss") + (path-up "infer/infer.ss") + (path-up "env/type-env.ss") + (path-up "env/type-environments.ss") + (path-up "env/type-name-env.ss") + (path-up "env/type-alias-env.ss") + (path-up "infer/infer-dummy.ss") + (path-up "private/parse-type.ss") + (path-up "private/type-contract.ss") + (path-up "typecheck/typechecker.ss"))) + +(provide with-type) +(define-syntax (with-type stx) + (define-splicing-syntax-class free-vars + #:attributes ((id 1) (ty 1)) + [pattern (~seq #:freevars ([id ty] ...))] + [pattern (~seq) + #:with (id ...) null + #:with (ty ...) null]) + (syntax-parse stx + [(_ region-ty-stx fv:free-vars . body) + (begin-with-definitions + (define old-context (unbox typed-context?)) + (set-box! typed-context? #t) + (define region-tc-result (parse-tc-results #'region-ty-stx)) + (define region-cnt (match region-tc-result + [(tc-result1: t) (type->contract + t + (lambda () (tc-error/stx #'region-ty-stx "Type ~a could not be converted to a contract." t)))])) + (define fv-types (for/list ([t (syntax->list #'(fv.ty ...))]) + (parse-type t))) + (define fv-cnts (for/list ([t (in-list fv-types)] + [stx (in-list (syntax->list #'(fv.ty ...)))]) + (type->contract t #:typed-side #f + (lambda () (tc-error/stx stx "Type ~a could not be converted to a contract." t))))) + (for ([i (in-list (syntax->list #'(fv.id ...)))] + [ty (in-list fv-types)]) + (register-type i ty)) + (define expanded-body (local-expand #'(let () . body) 'expression null)) + (parameterize (;; disable fancy printing? + [custom-printer #t] + ;; a cheat to avoid units + [infer-param infer] + ;; do we report multiple errors + [delay-errors? #t] + ;; this parameter is for parsing types + [current-tvars initial-tvar-env] + ;; this parameter is just for printing types + ;; this is a parameter to avoid dependency issues + [current-type-names + (lambda () + (append + (type-name-env-map (lambda (id ty) + (cons (syntax-e id) ty))) + (type-alias-env-map (lambda (id ty) + (cons (syntax-e id) ty)))))] + ;; reinitialize seen type variables + [type-name-references null] + ;; for error reporting + [orig-module-stx stx] + [expanded-module-stx expanded-body]) + (tc-expr/check expanded-body region-tc-result)) + (report-all-errors) + (set-box! typed-context? old-context) + ;; then clear the new entries from the env ht + (for ([i (in-list (syntax->list #'(fv.id ...)))]) + (unregister-type i)) + (with-syntax ([(cnt ...) fv-cnts] + [region-cnt region-cnt] + [check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))]) + (quasisyntax/loc stx + (begin check-syntax-help + (with-contract typed-region + #:result region-cnt + #:freevars ([fv.id cnt] ...) + . body)))))])) + \ No newline at end of file diff --git a/collects/typed-scheme/scribblings/ts-reference.scrbl b/collects/typed-scheme/scribblings/ts-reference.scrbl index 6387cf56..5b7bd3d2 100644 --- a/collects/typed-scheme/scribblings/ts-reference.scrbl +++ b/collects/typed-scheme/scribblings/ts-reference.scrbl @@ -6,6 +6,8 @@ scheme/list srfi/14 version/check))] +@(define the-eval (make-base-eval)) +@(the-eval '(require (except-in typed/scheme #%top-interaction #%module-begin))) @title[#:tag "top"]{The Typed Scheme Reference} @@ -330,3 +332,33 @@ Examples: @schememod[typed-scheme/no-check (: x Number) (define x "not-a-number")] + +@section{Typed Regions} + +The @scheme[with-type] for allows for localized Typed Scheme regions in otherwise untyped code. + +@defform/subs[(with-type type fv-clause body ...+) + ([fv-clause code:blank + (code:line #:freevars ([id fv-type] ...))])]{ +Checks that @scheme[body ...+] has the type @scheme[type]. The @scheme[id]s are assumed to +have the types ascribed to them; these types are converted to contracts and checked dynamically. +Uses of the result value are also appropriately checked by a contract generated from +@scheme[type]. + +@examples[#:eval the-eval +(with-type Number 3) + +((with-type (Number -> Number) + (lambda: ([x : Number]) (add1 x))) + #f) + +(let ([x "hello"]) + (with-type String + #:freevars ([x String]) + (string-append x ", world"))) + +(let ([x 'hello]) + (with-type String + #:freevars ([x String]) + (string-append x ", world")))] +} diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss index 0e1b5832..9dc8e20e 100644 --- a/collects/typed-scheme/typed-scheme.ss +++ b/collects/typed-scheme/typed-scheme.ss @@ -2,7 +2,7 @@ (require (rename-in "utils/utils.ss" [infer r:infer])) -(require (private base-types) +(require (private base-types with-types) (for-syntax (except-in syntax/parse id) scheme/base @@ -19,14 +19,12 @@ syntax/kerncase scheme/match)) - - - (provide (rename-out [module-begin #%module-begin] [top-interaction #%top-interaction] [#%plain-lambda lambda] [#%app #%app] - [require require])) + [require require]) + with-type) (define-for-syntax catch-errors? #f) diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss index 85d4aa5b..03a52627 100644 --- a/collects/typed-scheme/types/utils.ss +++ b/collects/typed-scheme/types/utils.ss @@ -295,7 +295,7 @@ ;; error for unbound variables (define (lookup-fail e) (match (identifier-binding e) - ['lexical (int-err "untyped lexical variable ~a" (syntax-e e))] + ['lexical (tc-error/expr "untyped lexical variable ~a" (syntax-e e))] [#f (tc-error/expr "untyped top-level identifier ~a" (syntax-e e))] [(list _ _ nominal-source-mod nominal-source-id _ _ _) (let-values ([(x y) (module-path-index-split nominal-source-mod)]) diff --git a/collects/typed/scheme/base.ss b/collects/typed/scheme/base.ss index be070611..c37fa0e4 100644 --- a/collects/typed/scheme/base.ss +++ b/collects/typed/scheme/base.ss @@ -17,5 +17,5 @@ typed-scheme/private/extra-procs (for-syntax typed-scheme/private/base-types-extra)) (provide (rename-out [with-handlers: with-handlers]) - assert + assert with-type (for-syntax (all-from-out typed-scheme/private/base-types-extra)))