suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

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

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

svn: r18416

original commit: 78c14e434b7f6dffc6c404d090b449b097e96cfb
This commit is contained in:
Sam Tobin-Hochstadt 2010-03-01 22:31:24 +00:00
commit b0a1fde7aa
12 changed files with 182 additions and 104 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/tests/typed-scheme/fail/with-type1.ss
View File

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

7
collects/tests/typed-scheme/fail/with-type2.ss
View File

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

2
collects/tests/typed-scheme/succeed/require-procedure.ss Normal file
View File

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

13
collects/tests/typed-scheme/succeed/with-type.ss
View File

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

6
collects/typed-scheme/env/init-envs.ss vendored
View File

@ -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)))
(app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals)))
[(? Type?
(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)]))

1
collects/typed-scheme/private/base-types-new.ss
View File

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

9
collects/typed-scheme/private/type-contract.ss
View File

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

194
collects/typed-scheme/private/with-types.ss
View File

@ -9,85 +9,135 @@
"extra-procs.ss"
"prims.ss"
"base-types.ss"
scheme/contract/regions scheme/contract/base
(for-syntax "base-types-extra.ss")
(for-syntax (except-in "../utils/utils.ss" infer)
"../utils/tc-utils.ss"
(except-in (combine-in "../types/convenience.ss" "../types/abbrev.ss") ->)
"../types/utils.ss"
"../infer/infer.ss"
"../env/type-env.ss"
"../env/type-environments.ss"
"../env/type-name-env.ss"
"../env/type-alias-env.ss"
"../infer/infer-dummy.ss"
"../private/parse-type.ss"
"../private/type-contract.ss"
"../typecheck/typechecker.ss"))
scheme/contract/regions scheme/contract/base
(for-syntax
"base-types-extra.ss"
unstable/debug
(path-up "env/type-name-env.ss"
"env/type-alias-env.ss"
"infer/infer-dummy.ss"
"private/parse-type.ss"
"private/type-contract.ss"
"typecheck/typechecker.ss"
"env/type-environments.ss"
"env/type-env.ss"
"infer/infer.ss"
"utils/tc-utils.ss"
"types/utils.ss")
(except-in (path-up "utils/utils.ss" "types/convenience.ss" "types/abbrev.ss") infer ->)))
(provide with-type)
(define-for-syntax (with-type-helper stx body fvids fvtys exids extys resty expr? ctx)
(begin-with-definitions
(define old-context (unbox typed-context?))
(set-box! typed-context? #t)
(define fv-types (for/list ([t (in-list (syntax->list fvtys))])
(parse-type t)))
(define fv-cnts (for/list ([t (in-list fv-types)]
[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)))))
(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
(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
[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])
(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 fvids))])
(unregister-type i))
(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)))
(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 ([id ty] ...))]
[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
[(_ 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)))))]))
[(_ :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))]))

2
collects/typed-scheme/rep/rep-utils.ss
View File

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

33
collects/typed-scheme/scribblings/ts-reference.scrbl
View File

@ -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] ...))])]{
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
(code:line #:freevars ([id fv-type] ...))]
[result-spec (code:line #:result type)]
[export-spec ([export-id export-type] ...)])]{
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)]
}

9
collects/typed-scheme/types/convenience.ss
View File

@ -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
(-val '())
(Un (-val '())
-Number -Boolean -Symbol -String -Keyword -Char
(-pair sexp sexp)
(make-Vector sexp)
(make-Box sexp)

8
collects/typed-scheme/utils/utils.ss
View File

@ -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)))
#'pseudo-printer)
(lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))
#:inspector #f)]))