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

Typecheck (lambda args body) as (arg1 -> result).

Browse Source 
original commit: 0e42a791a75a30bb2bf45bf968d053dfdf567d40
This commit is contained in:
Eric Dobson 2013-02-03 17:40:25 -08:00
parent 22672f99e8
commit 54d6d3ffec
2 changed files with 22 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
collects/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -341,6 +341,12 @@
[tc-e/t (lambda: ([x : Number] . [y : Boolean *]) (car y)) (->* (list N) B B)]
[tc-e ((lambda: ([x : Number] . [y : Boolean *]) (car y)) 3) B]
[tc-e (apply (lambda: ([x : Number] . [y : Boolean *]) (car y)) 3 '(#f)) B]
[tc-e (lambda args (void)) #:ret (ret (t:-> -String -Void) (-FS -top -bot))
#:expected (ret (t:-> -String -Void) (-FS -top -bot))]
[tc-e (lambda (x y . z)
(+ x y (+ (length z))))
#:ret (ret (t:-> -Byte -Index N) (-FS -top -bot))
#:expected (ret (t:-> -Byte -Index N) (-FS -top -bot))]
[tc-e/t (let: ([x : Number 3])
(when (number? x) #t))

23
collects/typed-racket/typecheck/tc-lambda-unit.rkt
View File

@ -72,7 +72,7 @@
[(> arg-len tys-len) (append arg-tys
(map (lambda _ (or rest-ty (Un)))
(drop arg-list tys-len)))]))])
(define (check-body)
(define (check-body [rest-ty rest-ty])
(with-lexical-env/extend
arg-list arg-types
(make-lam-result (for/list ([al arg-list] [at arg-types] [a-ty arg-tys]) (list al at)) null
@ -80,7 +80,15 @@
;; make up a fake name if none exists, this is an error case anyway
(and drest (cons (or rest (generate-temporary)) drest))
(tc-exprs/check (syntax->list body) ret-ty))))
(when (or (not (= arg-len tys-len))
;; Check that the number of formal arguments is valid for the expected type.
;; Thus it must be able to accept the number of arguments that the expected
;; type has. So we check for three cases, if the function doesn't accept
;; enough arguments, if it requires too many arguments, or if it doesn't
;; support rest arguments if needed.
;; This allows a form like (lambda args body) to have the type (-> Symbol
;; Number) with out a rest arg.
(when (or (and (< arg-len tys-len) (not rest))
(> arg-len tys-len)
(and (or rest-ty drest) (not rest)))
(tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest)))
(cond
@ -101,11 +109,10 @@
(let ([rest-type (cond
[rest-ty rest-ty]
[(type-annotation rest) (get-type rest #:default Univ)]
[(< arg-len tys-len) (list-ref arg-tys arg-len)]
[else (Un)])])
[else Univ])])
(with-lexical-env/extend
(list rest) (list (-lst rest-type))
(check-body)))])))
(check-body rest-type)))])))
;; typecheck a single lambda, with argument list and body
;; drest-ty and drest-bound are both false or not false
@ -230,8 +237,10 @@
#:when (and (not r) (not dr) (= (length a) (length (syntax->list fml)))))
f)]
[else
;; fml is an improper list, thus the function has a rest argument, and so valid
;; types must have at least as many positional arguments as it does.
(for/list ([a argss] [f fs] [r rests] [dr drests]
#:when (and (or r dr) (= (length a) (sub1 (syntax-len fml)))))
#:when (>= (length a) (sub1 (syntax-len fml))))
f)])]
[_ null]))
(define (go expected formals bodies formals* bodies* nums-seen)
@ -241,7 +250,7 @@
(for/list ([f* formals*] [b* bodies*])
(match (find-expected expected f*)
;; very conservative -- only do anything interesting if we get exactly one thing that matches
[(list)
[(list)
(if (and (= 1 (length formals*)) (match expected ((tc-results: _) #t) (_ #f)))
(tc-error/expr #:return (list (lam-result null null (list #'here Univ) #f (ret (Un))))
"Expected a function of type ~a, but got a function with the wrong arity"