Add `unregister-type'

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

svn: r18374

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)

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

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

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

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)

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

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

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)
 

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

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