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

Lots of unit contracts, plus some bug fixing.

Browse Source 
svn: r12820
This commit is contained in:
Sam Tobin-Hochstadt 2008-12-12 20:33:21 +00:00
parent bc62c06e1c
commit 57f1dd0c4d
9 changed files with 78 additions and 45 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
collects/typed-scheme/infer/signatures.ss
View File

@ -1,29 +1,42 @@
#lang scheme/base #lang scheme/base
(require scheme/unit) (require scheme/unit scheme/contract "constraint-structs.ss" "../utils/utils.ss")
(require (rep type-rep) (utils unit-utils))
(provide (all-defined-out)) (provide (all-defined-out))
(define-signature dmap^ (define-signature dmap^
(dmap-meet)) ([cnt dmap-meet (dmap? dmap? . -> . dmap?)]))
(define-signature promote-demote^ (define-signature promote-demote^
(var-promote var-demote)) ([cnt var-promote (Type? (listof symbol?) . -> . Type?)]
[cnt var-demote (Type? (listof symbol?) . -> . Type?)]))
(define-signature constraints^ (define-signature constraints^
(exn:infer? ([cnt exn:infer? (any/c . -> . boolean?)]
fail-sym [cnt fail-sym symbol?]
;; inference failure - masked before it gets to the user program ;; inference failure - masked before it gets to the user program
(define-syntaxes (fail!) (define-syntaxes (fail!)
(syntax-rules () (syntax-rules ()
[(_ s t) (raise fail-sym)])) [(_ s t) (raise fail-sym)]))
cset-meet cset-meet* [cnt cset-meet (cset? cset? . -> . cset?)]
[cnt cset-meet* ((listof cset?) . -> . cset?)]
no-constraint no-constraint
empty-cset [cnt empty-cset ((listof symbol?) . -> . cset?)]
insert [cnt insert (cset? symbol? Type? Type? . -> . cset?)]
cset-combine [cnt cset-combine ((listof cset?) . -> . cset?)]
c-meet)) [cnt c-meet ((c? c?) (symbol?) . ->* . c?)]))
(define-signature restrict^ (define-signature restrict^
(restrict)) ([cnt restrict (Type? Type? . -> . Type?)]))
(define-signature infer^ (define-signature infer^
(infer infer/vararg infer/dots)) ([cnt infer (((listof symbol?) (listof Type?) (listof Type?) Type? (listof symbol?)) ((or/c #f Type?)) . ->* . any)]
[cnt infer/vararg (((listof symbol?)
(listof Type?)
(listof Type?)
Type? Type?
(listof symbol?))
((or/c #f Type?)) . ->* . any)]
[cnt infer/dots (((listof symbol?)
symbol?
(listof Type?) (listof Type?) Type? Type? (listof symbol?))
(#:expected (or/c #f Type?)) . ->* . any)]))

16
collects/typed-scheme/private/require-contract.ss
View File

@ -12,20 +12,20 @@
(begin define-values) (begin define-values)
[(begin (define-values (n) e) e*) [(begin (define-values (n) e) e*)
#`(begin (define-values (n) e) #`(begin (define-values (n) e)
(define name #,(syntax-property #'e* (define name e*))]
'inferred-name
(syntax-e #'name))))]
[(begin (begin e)) [(begin (begin e))
#`(define name #,(syntax-property #'e #`(define name e)])]))
'inferred-name
(syntax-e #'name)))])]))
(define-syntax (require/contract stx) (define-syntax (require/contract stx)
(syntax-case stx () (syntax-case stx ()
[(require/contract nm cnt lib) [(require/contract nm cnt lib)
(identifier? #'nm) (identifier? #'nm)
#`(begin (require (only-in lib [nm tmp])) #`(begin (require (only-in lib [nm tmp]))
(define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))] (define-ignored nm (contract (let ([nm cnt]) nm) tmp
'#,(syntax->datum #'nm)
'never-happen
(list (make-srcloc tmp #f #f #f #f) (symbol->string 'nm)))))]
[(require/contract (orig-nm nm) cnt lib) [(require/contract (orig-nm nm) cnt lib)
#`(begin (require (only-in lib [orig-nm tmp])) #`(begin (require (only-in lib [orig-nm tmp]))
(define-ignored nm (contract cnt tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))])) (define-ignored nm (contract (let ([nm cnt]) nm)
tmp '#,(syntax->datum #'nm) 'never-happen (quote-syntax nm))))]))

5
collects/typed-scheme/typecheck/check-subforms-unit.ss
View File

@ -12,7 +12,7 @@
(export check-subforms^) (export check-subforms^)
;; find the subexpressions that need to be typechecked in an ignored form ;; find the subexpressions that need to be typechecked in an ignored form
;; syntax -> void ;; syntax -> any
(define (check-subforms/with-handlers form) (define (check-subforms/with-handlers form)
(define handler-tys '()) (define handler-tys '())
(define body-ty #f) (define body-ty #f)
@ -48,6 +48,7 @@
[_ (void)]))) [_ (void)])))
(ret (apply Un body-ty handler-tys))) (ret (apply Un body-ty handler-tys)))
;; syntax type -> any
(define (check-subforms/with-handlers/check form expected) (define (check-subforms/with-handlers/check form expected)
(let loop ([form form]) (let loop ([form form])
(parameterize ([current-orig-stx form]) (parameterize ([current-orig-stx form])
@ -73,7 +74,7 @@
(ret expected)) (ret expected))
;; typecheck the expansion of a with-handlers form ;; typecheck the expansion of a with-handlers form
;; syntax -> type ;; syntax -> any
(define (check-subforms/ignore form) (define (check-subforms/ignore form)
(let loop ([form form]) (let loop ([form form])
(kernel-syntax-case* form #f () (kernel-syntax-case* form #f ()

39
collects/typed-scheme/typecheck/signatures.ss
View File

@ -1,28 +1,49 @@
#lang scheme/base #lang scheme/base
(require scheme/unit) (require scheme/unit scheme/contract "../utils/utils.ss")
(require (rep type-rep)
(utils unit-utils)
(private type-utils))
(provide (all-defined-out)) (provide (all-defined-out))
(define-signature typechecker^ (define-signature typechecker^
(type-check tc-toplevel-form)) ([cnt type-check (syntax? . -> . syntax?)]
[cnt tc-toplevel-form (syntax? . -> . any)]))
(define-signature tc-expr^ (define-signature tc-expr^
(tc-expr tc-expr/check tc-expr/check/t check-below tc-literal tc-exprs tc-exprs/check tc-expr/t)) ([cnt tc-expr (syntax? . -> . tc-result?)]
[cnt tc-expr/check (syntax? Type? . -> . tc-result?)]
[cnt tc-expr/check/t (syntax? Type? . -> . Type?)]
[cnt check-below (->d ([s (or/c Type? tc-result?)] [t Type?]) () [_ (if (Type? s) Type? tc-result?)])]
[cnt tc-literal (any/c . -> . Type?)]
[cnt tc-exprs ((listof syntax?) . -> . tc-result?)]
[cnt tc-exprs/check ((listof syntax?) Type? . -> . tc-result?)]
[cnt tc-expr/t (syntax? . -> . Type?)]))
(define-signature check-subforms^ (define-signature check-subforms^
(check-subforms/ignore check-subforms/with-handlers check-subforms/with-handlers/check)) ([cnt check-subforms/ignore (syntax? . -> . any)]
[cnt check-subforms/with-handlers (syntax? . -> . any)]
[cnt check-subforms/with-handlers/check (syntax? Type? . -> . any)]))
(define-signature tc-if^ (define-signature tc-if^
(tc/if-onearm tc/if-twoarm tc/if-onearm/check tc/if-twoarm/check)) ([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/if-twoarm/check (syntax? syntax? syntax? Type? . -> . tc-result?)]))
(define-signature tc-lambda^ (define-signature tc-lambda^
(tc/lambda tc/lambda/check tc/rec-lambda/check)) ([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/lambda/check (syntax? syntax? syntax? Type? . -> . tc-result?)]
[cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type?) Type? . -> . Type?)]))
(define-signature tc-app^ (define-signature tc-app^
(tc/app tc/app/check tc/funapp)) ([cnt tc/app (syntax? . -> . tc-result?)]
[cnt tc/app/check (syntax? Type? . -> . tc-result?)]
[cnt tc/funapp (syntax? syntax? tc-result? (listof tc-result?) (or/c #f Type?) . -> . tc-result?)]))
(define-signature tc-let^ (define-signature tc-let^
(tc/let-values tc/letrec-values tc/let-values/check tc/letrec-values/check)) ([cnt tc/let-values (syntax? syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/letrec-values (syntax? syntax? syntax? syntax? . -> . tc-result?)]
[cnt tc/let-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)]
[cnt tc/letrec-values/check (syntax? syntax? syntax? syntax? Type? . -> . tc-result?)]))
(define-signature tc-dots^ (define-signature tc-dots^
(tc/dots)) ([cnt tc/dots (syntax? . -> . (values Type? symbol?))]))

4
collects/typed-scheme/typecheck/tc-app-unit.ss
View File

@ -368,8 +368,8 @@
(let ([substitution (infer vars ... rng)]) (let ([substitution (infer vars ... rng)])
(and substitution (and substitution
(log-result substitution) (log-result substitution)
(or expected (ret (or expected
(ret (subst-all substitution rng)))))) (subst-all substitution rng))))))
(poly-fail t argtypes #:name (and (identifier? f-stx) f-stx)))))])) (poly-fail t argtypes #:name (and (identifier? f-stx) f-stx)))))]))
(define (poly-fail t argtypes #:name [name #f]) (define (poly-fail t argtypes #:name [name #f])

1
collects/typed-scheme/typecheck/tc-expr-unit.ss
View File

@ -190,7 +190,6 @@
(begin (tc-exprs/check (syntax->list #'es) Univ) (begin (tc-exprs/check (syntax->list #'es) Univ)
(tc-expr/check #'e expected))] (tc-expr/check #'e expected))]
;; if ;; if
[(if tst body) (tc/if-onearm/check #'tst #'body expected)]
[(if tst thn els) (tc/if-twoarm/check #'tst #'thn #'els expected)] [(if tst thn els) (tc/if-twoarm/check #'tst #'thn #'els expected)]
;; lambda ;; lambda
[(#%plain-lambda formals . body) [(#%plain-lambda formals . body)

9
collects/typed-scheme/typecheck/tc-if-unit.ss
View File

@ -13,9 +13,6 @@
mzlib/trace mzlib/trace
mzlib/plt-match) mzlib/plt-match)
;; necessary for creating (#%app void) in tc-if/onearm
(require (for-template scheme/base))
;; if typechecking ;; if typechecking
(import tc-expr^) (import tc-expr^)
(export tc-if^) (export tc-if^)
@ -88,12 +85,6 @@
;; v cannot have type (-val #f) ;; v cannot have type (-val #f)
[(Var-True-Effect: v) (check-rest *remove (-val #f) v)]))))) [(Var-True-Effect: v) (check-rest *remove (-val #f) v)])))))
;; create a dummy else branch for typechecking
(define (tc/if-onearm tst body) (tc/if-twoarm tst body (syntax/loc body (#%app void))))
(define (tc/if-onearm/check tst body expected)
(tc/if-twoarm/check tst body (syntax/loc body (#%app void)) expected))
;; the main function ;; the main function
(define (tc/if-twoarm tst thn els) (define (tc/if-twoarm tst thn els)
#;(printf "tc-if/twoarm~n") #;(printf "tc-if/twoarm~n")

4
collects/typed-scheme/typecheck/tc-lambda-unit.ss
View File

@ -199,16 +199,18 @@
(cons (car bodies) bodies*) (cons (car bodies) bodies*)
(cons (syntax-len (car formals)) nums-seen))])))) (cons (syntax-len (car formals)) nums-seen))]))))
;; tc/lambda : syntax syntax-list syntax-list -> tc-result
(define (tc/lambda form formals bodies) (define (tc/lambda form formals bodies)
(tc/lambda/internal form formals bodies #f)) (tc/lambda/internal form formals bodies #f))
;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic ;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic
;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> Type ;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result
(define (tc/lambda/internal form formals bodies expected) (define (tc/lambda/internal form formals bodies expected)
(if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected)) (if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected))
(tc/plambda form formals bodies expected) (tc/plambda form formals bodies expected)
(ret (tc/mono-lambda formals bodies expected)))) (ret (tc/mono-lambda formals bodies expected))))
;; tc/lambda : syntax syntax-list syntax-list Type -> tc-result
(define (tc/lambda/check form formals bodies expected) (define (tc/lambda/check form formals bodies expected)
(tc/lambda/internal form formals bodies expected)) (tc/lambda/internal form formals bodies expected))

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

@ -7,7 +7,13 @@
scheme/unit-exptime scheme/unit-exptime
scheme/match)) scheme/match))
(provide define-values/link-units/infer) (provide define-values/link-units/infer cnt)
(define-signature-form (cnt stx)
(syntax-case stx ()
[(_ nm cnt)
#;(list #'nm)
(list #'[contracted nm cnt])]))
(define-syntax (define-values/link-units/infer stx) (define-syntax (define-values/link-units/infer stx)
;; construct something we can put in the imports/exports clause from the datum ;; construct something we can put in the imports/exports clause from the datum