Add `with-type' for defintions, add #:result keyword.

Fix contract for top-arr.
Remove static version of printing conditional.
Fix brokenness in print-converting.

svn: r18416

collects/tests/typed-scheme/fail/with-type1.ss

@@ -3,6 +3,6 @@
 #lang scheme
 (require typed/scheme)
 
-((with-type (Number -> Number)
+((with-type #:result (Number -> Number)
    (lambda: ([x : Number]) (add1 x)))
  #f)

collects/tests/typed-scheme/fail/with-type2.ss

@@ -5,6 +5,7 @@
 (require typed/scheme)
 
 (let ([x 'hello])
-  (with-type String
+  (with-type
+   #:result String
    #:freevars ([x String])
    (string-append x ", world")))

collects/tests/typed-scheme/succeed/require-procedure.ss

@@ -0,0 +1,2 @@
+#lang typed/scheme
+(require/typed scheme [procedure-arity (Procedure -> Natural)])

collects/tests/typed-scheme/succeed/with-type.ss

@@ -1,9 +1,18 @@
 #lang scheme
 (require typed/scheme)
 
-(with-type Number 3)
+(with-type #:result Number 3)
 
 (let ([x "hello"])
-  (with-type String
+  (with-type #:result String
     #:freevars ([x String])
     (string-append x ", world")))
+
+(with-type ([fun (Number -> Number)]
+            [val Number])
+  (define (fun x) x)
+  (define val 17))
+
+(fun val)
+val
+

collects/typed-scheme/env/init-envs.ss

@@ -41,10 +41,10 @@
     [(? (lambda (e) (or (LatentFilter? e)
                         (LatentObject? e)
                         (PathElem? e)))
-        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) 
+        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals)))
      `(,(gen-constructor tag) ,@(map sub vals))]
-    [(? (lambda (e) (or (Type? e)))
+    [(? Type?
-        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals))) 
+        (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx key vals)))
      `(,(gen-constructor tag) ,@(map sub vals))]
     [_ (basic v)]))
 

collects/typed-scheme/private/base-types-new.ss

@@ -49,3 +49,4 @@
 [Nothing (Un)]
 [Pairof (-poly (a b) (-pair a b))]
 [MPairof (-poly (a b) (-mpair a b))]
+

collects/typed-scheme/private/type-contract.ss

@@ -57,6 +57,7 @@
       (define (t->c/neg t #:seen [structs-seen structs-seen]) (loop t (not pos?) (not from-typed?) structs-seen))
       (define (t->c/fun f #:method [method? #f])
         (match f
+          [(Function: (list (top-arr:))) #'procedure?]
           [(Function: arrs)
            (let ()           
              (define (f a)
@@ -90,11 +91,15 @@
                      #'((dom* ...) (opt-dom* ...) #:rest (listof rst*) . ->* . rng*)
                      #'(dom* ... . -> . rng*))))
              (unless (no-duplicates (for/list ([t arrs])
-                                      (match t [(arr: dom _ _ _ _) (length dom)])))
+                                      (match t
+                                        [(arr: dom _ _ _ _) (length dom)]
+                                        ;; is there something more sensible here?
+                                        [(top-arr:) (int-err "got top-arr")])))
                (exit (fail)))
              (match (map f arrs)
                [(list e) e]
-               [l #`(case-> #,@l)]))]))
+               [l #`(case-> #,@l)]))]
+          [_ (int-err "not a function" f)]))
       (match ty
         [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
         ;; any/c doesn't provide protection in positive position

collects/typed-scheme/private/with-types.ss

@@ -10,49 +10,60 @@
          "prims.ss"
          "base-types.ss"
          scheme/contract/regions scheme/contract/base         
-         (for-syntax "base-types-extra.ss")
+         (for-syntax 
-         (for-syntax (except-in "../utils/utils.ss" infer)
+          "base-types-extra.ss"
-                     "../utils/tc-utils.ss"
+          unstable/debug
-                     (except-in (combine-in "../types/convenience.ss" "../types/abbrev.ss") ->)                     
+          (path-up "env/type-name-env.ss"
-                     "../types/utils.ss"
+                   "env/type-alias-env.ss"
-                     "../infer/infer.ss"
+                   "infer/infer-dummy.ss"
-                     "../env/type-env.ss"
+                   "private/parse-type.ss"
-                     "../env/type-environments.ss"
+                   "private/type-contract.ss"
-                     "../env/type-name-env.ss"
+                   "typecheck/typechecker.ss"
-                     "../env/type-alias-env.ss"
+                   "env/type-environments.ss" 
-                     "../infer/infer-dummy.ss"
+                   "env/type-env.ss"
-                     "../private/parse-type.ss"
+                   "infer/infer.ss"
-                     "../private/type-contract.ss"
+                   "utils/tc-utils.ss"
-                     "../typecheck/typechecker.ss"))
+                   "types/utils.ss")
+          (except-in (path-up "utils/utils.ss" "types/convenience.ss" "types/abbrev.ss") infer ->)))
 
 (provide with-type)
-(define-syntax (with-type stx)
+
-  (define-splicing-syntax-class free-vars
+(define-for-syntax (with-type-helper stx body fvids fvtys exids extys resty expr? ctx)
-    #: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 fv-types (for/list ([t (in-list (syntax->list fvtys))])
-       (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 ...)))])
+                               [stx (in-list (syntax->list fvtys))])
                       (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 ...)))]
+    (define ex-types (for/list ([t (syntax->list extys)])
+                       (parse-type t)))
+    (define ex-cnts (for/list ([t (in-list ex-types)]
+                               [stx (in-list (syntax->list extys))])
+                      (type->contract t #:typed-side #t
+                                      (lambda () (tc-error/stx stx "Type ~a could not be converted to a contract." t)))))
+    (define region-tc-result 
+      (and expr? (parse-tc-results resty)))
+    (define region-cnt 
+      (and region-tc-result
+           (match region-tc-result 
+             [(tc-result1: t) (type->contract 
+                               t 
+                               #:typed-side #t
+                               (lambda () (tc-error/stx #'region-ty-stx "Type ~a could not be converted to a contract." t)))])))
+    (for ([i (in-list (syntax->list fvids))]
           [ty (in-list fv-types)])
       (register-type i ty))
-       (define expanded-body (local-expand #'(let () . body) 'expression null))
+    (define expanded-body 
+      (if expr?
+          (with-syntax ([body body])
+            (local-expand #'(let () . body) ctx null))
+          (with-syntax ([(body ...) body]
+                        [(id ...) exids]
+                        [(ty ...) extys])
+            (local-expand #'(let () (begin (: id ty) ... body ... (values id ...))) ctx null))))
     (parameterize (;; disable fancy printing?
                    [custom-printer #t]
                    ;; a cheat to avoid units
@@ -75,19 +86,58 @@
                    ;; for error reporting
                    [orig-module-stx stx]
                    [expanded-module-stx expanded-body])
-         (tc-expr/check expanded-body region-tc-result))
+      (if expr?
+          (tc-expr/check expanded-body region-tc-result)
+          (tc-expr/check expanded-body (ret ex-types))))
     (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 ...)))])
+    (for ([i (in-list (syntax->list fvids))])
       (unregister-type i))
-       (with-syntax ([(cnt ...) fv-cnts]
+    (with-syntax ([(fv.id ...) fvids]
+                  [(cnt ...) fv-cnts]
+                  [(ex-id ...) exids]
+                  [(ex-cnt ...) ex-cnts]
                   [region-cnt region-cnt]
+                  [body expanded-body]
                   [check-syntax-help (syntax-property #'(void) 'disappeared-use (type-name-references))])
+      (if expr?
           (quasisyntax/loc stx
             (begin check-syntax-help
                    (with-contract typed-region
                      #:result region-cnt
                      #:freevars ([fv.id cnt] ...)                                
-                                 . body)))))]))
+                     body)))
+          (syntax/loc stx
+            (begin
+              (define-values () (begin check-syntax-help (values)))
+              (with-contract typed-region
+                ([ex-id ex-cnt] ...)
+                (define-values (ex-id ...) body))))))))
+
+(define-syntax (with-type stx)
+  (define-syntax-class typed-id
+    #:description "[id type]"
+    [pattern (id ty)])
+  (define-splicing-syntax-class free-vars
+    #:description "free variable specification"
+    #:attributes ((id 1) (ty 1))
+    [pattern (~seq #:freevars (:typed-id ...))]
+    [pattern (~seq)
+             #:with (id ...) null
+             #:with (ty ...) null])
+  (define-syntax-class typed-ids
+    #:description "sequence of typed identifiers"
+    #:attributes ((id 1) (ty 1))
+    [pattern (t:typed-id ...)
+             #:with (id ...) #'(t.id ...)
+             #:with (ty ...) #'(t.ty ...)])
+  (define-splicing-syntax-class result-ty
+    #:description "result specification"
+    [pattern (~seq #:result ty:expr)])
+  (syntax-parse stx
+    [(_ :typed-ids fv:free-vars . body)
+     (with-type-helper stx #'body #'(fv.id ...) #'(fv.ty ...) #'(id ...) #'(ty ...) #f #f (syntax-local-context))]
+    [(_ :result-ty fv:free-vars . body)
+     (with-type-helper stx #'body #'(fv.id ...) #'(fv.ty ...) #'() #'() #'ty #t (syntax-local-context))]))
  

collects/typed-scheme/rep/rep-utils.ss

@@ -25,7 +25,7 @@
 
 (provide == defintern hash-id (for-syntax fold-target))
 
-(define-struct Rep (seq free-vars free-idxs stx))
+(define-struct Rep (seq free-vars free-idxs stx) #:transparent)
 
 (define-for-syntax fold-target #'fold-target)
 (define-for-syntax default-fields (list #'seq #'free-vars #'free-idxs #'stx))

collects/typed-scheme/scribblings/ts-reference.scrbl

@@ -337,28 +337,43 @@ Examples:
 
 The @scheme[with-type] for allows for localized Typed Scheme regions in otherwise untyped code.
 
-@defform/subs[(with-type type fv-clause body ...+)
+@defform*/subs[[(with-type result-spec fv-clause body ...+)
+                (with-type export-spec fv-clause body ...+)]
               ([fv-clause code:blank
-                          (code:line #:freevars ([id fv-type] ...))])]{
+                          (code:line #:freevars ([id fv-type] ...))]
-Checks that @scheme[body ...+] has the type @scheme[type].  The @scheme[id]s are assumed to 
+               [result-spec (code:line #:result type)]
-have the types ascribed to them; these types are converted to contracts and checked dynamically.
+               [export-spec ([export-id export-type] ...)])]{
-Uses of the result value are also appropriately checked by a contract generated from 
+The first form, an expression, checks that @scheme[body ...+] has the type @scheme[type].  
+Uses of the result value are appropriately checked by a contract generated from 
 @scheme[type].
 
+The second form, which can be used as a definition, checks that each of the @scheme[export-id]s 
+has the specified type.  These types are also enforced in the surrounding code with contracts.
+
+The @scheme[id]s are assumed to 
+have the types ascribed to them; these types are converted to contracts and checked dynamically.
+
 @examples[#:eval the-eval
 (with-type Number 3)
 
-((with-type (Number -> Number)
+((with-type #:result (Number -> Number)
    (lambda: ([x : Number]) (add1 x)))
  #f)
 
 (let ([x "hello"])
-  (with-type String
+  (with-type #:result String
     #:freevars ([x String])
     (string-append x ", world")))
 
 (let ([x 'hello])
-  (with-type String
+  (with-type #:result String
     #:freevars ([x String])
-    (string-append x ", world")))]
+    (string-append x ", world")))
+
+(with-type ([fun (Number -> Number)]
+            [val Number])
+  (define (fun x) x)
+  (define val 17))
+
+(fun val)]
 }

collects/typed-scheme/types/convenience.ss

@@ -2,7 +2,7 @@
 (require "../utils/utils.ss"
          (rep type-rep filter-rep object-rep)
          (utils tc-utils)
-         "abbrev.ss"
+         "abbrev.ss" (only-in scheme/contract current-blame-format)
 	 (types comparison printer union subtype utils)
          scheme/list scheme/match scheme/promise
          (for-syntax syntax/parse scheme/base)
@@ -14,7 +14,6 @@
          make-Name make-ValuesDots make-Function
          (rep-out filter-rep object-rep))
 
-
 (define (one-of/c . args)
   (apply Un (map -val args)))
 
@@ -47,7 +46,7 @@
 
 (define In-Syntax
   (-mu e
-       (*Un -Boolean -Symbol -String -Keyword -Char -Number (-val null)
+       (*Un (-val null) -Boolean -Symbol -String -Keyword -Char -Number 
             (make-Vector (-Syntax e))
             (make-Box (-Syntax e))
             (-lst (-Syntax e))
@@ -57,8 +56,8 @@
 
 (define (-Sexpof t)
   (-mu sexp
-       (Un -Number -Boolean -Symbol -String -Keyword -Char
+       (Un (-val '())
-           (-val '())
+           -Number -Boolean -Symbol -String -Keyword -Char           
            (-pair sexp sexp)
            (make-Vector sexp)
            (make-Box sexp)

collects/typed-scheme/utils/utils.ss

@@ -126,8 +126,6 @@ at least theoretically.
 ;; - 1 printers have to be defined at the same time as the structs
 ;; - 2 we want to support things printing corectly even when the custom printer is off
 
-(define-for-syntax printing? #t)
-
 (define-syntax-rule (defprinter t ...)
   (begin
     (define t (box (lambda _ (error (format "~a not yet defined" 't))))) ...
@@ -147,16 +145,14 @@ at least theoretically.
       (pretty-print (print-convert s))
       (newline))))
 
-(define custom-printer (make-parameter #t))
+(define custom-printer (make-parameter #f))
   
 (define-syntax (define-struct/printer stx)
   (syntax-parse stx
     [(form name (flds ...) printer:expr)
      #`(define-struct name (flds ...) 
          #:property prop:custom-write 
-         #,(if printing? 
+         (lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))
-               #'(lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))
-               #'pseudo-printer)
          #:inspector #f)]))