Add `unregister-type'

Add type regions.
Untyped lexical vars not an internal error.

svn: r18374

original commit: 8e3a67936eeb14fc08279a075966f93e35209f23
This commit is contained in:
Stevie Strickland 2010-02-27 01:26:16 +00:00
parent cdb7b62f5e
commit a92cd6cdce
10 changed files with 173 additions and 19 deletions

View File

@ -0,0 +1,8 @@
#;
(exn-pred exn:fail:contract?)
#lang scheme
(require typed/scheme)
((with-type (Number -> Number)
(lambda: ([x : Number]) (add1 x)))
#f)

View File

@ -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")))

View File

@ -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")))

View File

@ -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))

View File

@ -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)

View File

@ -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)))))]))

View File

@ -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")))]
}

View File

@ -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)

View File

@ -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)])

View File

@ -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)))