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

lots of let improvements

Browse Source 
and check rationalization

svn: r14635

original commit: 5a49e92de7e48a52482a3287846a8a37b8d42de4
This commit is contained in:
Sam Tobin-Hochstadt 2009-04-27 23:25:34 +00:00
parent b0634cd6af
commit 33ec27925d
4 changed files with 29 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
collects/typed-scheme/test.ss
View File

@ -9,3 +9,14 @@
(plambda: (a) ([y : a]) y)
(plambda: (a) ([y : a]) y)
(plambda: () ([y : Boolean]) (if y #t #f))
#{(if #t #t #t) :: Boolean}
(let () 3)
(let ([x 1] [y 2]) x)
#{(let ([x 1] [y 2]) x) :: Number}
(let: ([x : Number 1] [y : Integer 2]) x)
#{(let: ([x : Integer 1] [y : Integer 2]) x) :: Integer}
#{(let*: ([x : Number 1] [x : Integer 2]) x) :: Integer}

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

@ -12,11 +12,11 @@
(define-signature tc-expr^
([cnt tc-expr (syntax? . -> . tc-results?)]
[cnt tc-expr/check (syntax? tc-results? . -> . tc-results?)]
[cnt tc-expr/check/t (syntax? Type/c . -> . Type/c)]
[cnt tc-expr/check/t (syntax? tc-results? . -> . Type/c)]
[cnt check-below (->d ([s (or/c Type/c tc-results?)] [t (or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])]
;[cnt tc-literal (any/c . -> . Type/c)]
[cnt tc-exprs ((listof syntax?) . -> . tc-results?)]
[cnt tc-exprs/check ((listof syntax?) Type/c . -> . tc-results?)]
[cnt tc-exprs/check ((listof syntax?) tc-results? . -> . tc-results?)]
[cnt tc-expr/t (syntax? . -> . Type/c)]))
(define-signature check-subforms^
@ -26,11 +26,11 @@
(define-signature tc-if^
([cnt tc/if-twoarm (syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/if-twoarm/check (syntax? syntax? syntax? Type/c . -> . tc-results?)]))
[cnt tc/if-twoarm/check (syntax? syntax? syntax? tc-results? . -> . tc-results?)]))
(define-signature tc-lambda^
([cnt tc/lambda (syntax? syntax? syntax? . -> . tc-results?)]
[cnt tc/lambda/check (syntax? syntax? syntax? Type/c . -> . tc-results?)]
[cnt tc/lambda/check (syntax? syntax? syntax? tc-results? . -> . tc-results?)]
[cnt tc/rec-lambda/check (syntax? syntax? syntax? syntax? (listof Type/c) Type/c . -> . Type/c)]))
(define-signature tc-app^

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

@ -126,7 +126,7 @@
(define (tc-expr/check/t e t)
(match (tc-expr/check e t)
[(tc-result: t) t]))
[(tc-result1: t) t]))
;; check-below : (/\ (Results Type -> Result)
;; (Results Results -> Result)
@ -146,6 +146,10 @@
(tc-error/expr "Expected ~a, but got ~a" t2 t1))
expected]))
(define (tc-expr/check/type form expected)
#;(syntax? Type/c . -> . tc-results?)
(tc-expr/check form (ret expected)))
;; tc-expr/check : syntax tc-results -> tc-results
(define (tc-expr/check form expected)
(parameterize ([current-orig-stx form])
@ -194,8 +198,8 @@
(check-below (tc-id #'x) expected)]
;; w-c-m
[(with-continuation-mark e1 e2 e3)
(begin (tc-expr/check #'e1 Univ)
(tc-expr/check #'e2 Univ)
(begin (tc-expr/check/type #'e1 Univ)
(tc-expr/check/type #'e2 Univ)
(tc-expr/check #'e3 expected))]
;; application
[(#%plain-app . _) (tc/app/check form expected)]
@ -264,8 +268,8 @@
[(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)))]
;; w-c-m
[(with-continuation-mark e1 e2 e3)
(begin (tc-expr/check #'e1 Univ)
(tc-expr/check #'e2 Univ)
(begin (tc-expr/check/type #'e1 Univ)
(tc-expr/check/type #'e2 Univ)
(tc-expr #'e3))]
;; lambda
[(#%plain-lambda formals . body)
@ -326,7 +330,7 @@
(int-err "bad form input to tc-expr: ~a" form))
;; typecheck form
(let ([ty (cond [(type-ascription form) => (lambda (ann)
(tc-expr/check form ann))]
(tc-expr/check/type form ann))]
[else (internal-tc-expr form)])])
(match ty
[(tc-results: ts fs os)
@ -353,11 +357,11 @@
(define (tc-exprs exprs)
(cond [(null? exprs) (ret -Void)]
[(null? (cdr exprs)) (tc-expr (car exprs))]
[else (tc-expr/check (car exprs) Univ)
[else (tc-expr/check/type (car exprs) Univ)
(tc-exprs (cdr exprs))]))
(define (tc-exprs/check exprs expected)
(cond [(null? exprs) (check-below (ret -Void) expected)]
[(null? (cdr exprs)) (tc-expr/check (car exprs) expected)]
[else (tc-expr/check (car exprs) Univ)
[else (tc-expr/check/type (car exprs) Univ)
(tc-exprs/check (cdr exprs) expected)]))

3
collects/typed-scheme/typecheck/tc-let-unit.ss
View File

@ -126,7 +126,8 @@
;; the types of the exprs
#;[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)]
;; the annotated types of the name (possibly using the inferred types)
[types (for/list ([name names] [e exprs]) (get-type/infer name e (tc-expr-t/maybe-expected expected) tc-expr/check/t))]
[types (for/list ([name names] [e exprs]) (get-type/infer name e (tc-expr-t/maybe-expected expected)
(lambda (e t) (tc-expr/check/t e (ret t)))))]
;; the clauses for error reporting
[clauses (syntax-case form () [(lv cl . b) (syntax->list #'cl)])])
(do-check void names types form types body clauses expected)))