Moved lambda special cases out of tc-app.rkt.
This commit is contained in:
parent
51671fcec4
commit
67c7e3537b
|
@ -52,6 +52,9 @@
|
||||||
(define-signature tc-app-eq^
|
(define-signature tc-app-eq^
|
||||||
([cond-contracted tc/app-eq (syntax? (or/c #f tc-results?). -> . (or/c #f tc-results?))]))
|
([cond-contracted tc/app-eq (syntax? (or/c #f tc-results?). -> . (or/c #f tc-results?))]))
|
||||||
|
|
||||||
|
(define-signature tc-app-lambda^
|
||||||
|
([cond-contracted tc/app-lambda (syntax? (or/c #f tc-results?). -> . (or/c #f tc-results?))]))
|
||||||
|
|
||||||
|
|
||||||
(define-signature tc-apply^
|
(define-signature tc-apply^
|
||||||
([cond-contracted tc/apply (syntax? syntax? . -> . tc-results?)]))
|
([cond-contracted tc/apply (syntax? syntax? . -> . tc-results?)]))
|
||||||
|
|
|
@ -28,68 +28,10 @@
|
||||||
|
|
||||||
(import tc-expr^ tc-lambda^ tc-let^ tc-apply^ tc-app-keywords^
|
(import tc-expr^ tc-lambda^ tc-let^ tc-apply^ tc-app-keywords^
|
||||||
tc-app-hetero^ tc-app-list^ tc-app-apply^ tc-app-values^
|
tc-app-hetero^ tc-app-list^ tc-app-apply^ tc-app-values^
|
||||||
tc-app-objects^ tc-app-eq^)
|
tc-app-objects^ tc-app-eq^ tc-app-lambda^)
|
||||||
(export tc-app^)
|
(export tc-app^)
|
||||||
|
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
||||||
;; let loop
|
|
||||||
|
|
||||||
(define (let-loop-check form lam lp actuals args body expected)
|
|
||||||
(syntax-parse #`(#,args #,body #,actuals)
|
|
||||||
#:literals (#%plain-app if null? pair? null)
|
|
||||||
[((val acc ...)
|
|
||||||
((~and inner-body (if (#%plain-app (~or pair? null?) val*) thn els)))
|
|
||||||
(actual actuals ...))
|
|
||||||
#:when
|
|
||||||
(and (free-identifier=? #'val #'val*)
|
|
||||||
(ormap (lambda (a) (find-annotation #'inner-body a))
|
|
||||||
(syntax->list #'(acc ...))))
|
|
||||||
(let* ([ts1 (generalize (tc-expr/t #'actual))]
|
|
||||||
[ann-ts (for/list ([a (in-syntax #'(acc ...))]
|
|
||||||
[ac (in-syntax #'(actuals ...))])
|
|
||||||
(or (find-annotation #'inner-body a)
|
|
||||||
(generalize (tc-expr/t ac))))]
|
|
||||||
[ts (cons ts1 ann-ts)])
|
|
||||||
;; check that the actual arguments are ok here
|
|
||||||
(for/list ([a (syntax->list #'(actuals ...))]
|
|
||||||
[t ann-ts])
|
|
||||||
(tc-expr/check a (ret t)))
|
|
||||||
;; then check that the function typechecks with the inferred types
|
|
||||||
(add-typeof-expr lam (tc/rec-lambda/check form args body lp ts expected))
|
|
||||||
expected)]
|
|
||||||
;; special case `for/list'
|
|
||||||
[((val acc ...)
|
|
||||||
((~and inner-body (if e1 e2 e3:id)))
|
|
||||||
(null actuals ...))
|
|
||||||
#:when (free-identifier=? #'val #'e3)
|
|
||||||
(let ([ts (for/list ([ac (syntax->list #'(actuals ...))]
|
|
||||||
[f (syntax->list #'(acc ...))])
|
|
||||||
(or
|
|
||||||
(type-annotation f #:infer #t)
|
|
||||||
(generalize (tc-expr/t ac))))]
|
|
||||||
[acc-ty (or
|
|
||||||
(type-annotation #'val #:infer #t)
|
|
||||||
(match expected
|
|
||||||
[(tc-result1: (and t (Listof: _))) t]
|
|
||||||
[_ #f])
|
|
||||||
(generalize (-val '())))])
|
|
||||||
(add-typeof-expr lam (tc/rec-lambda/check form args body lp (cons acc-ty ts) expected))
|
|
||||||
expected)]
|
|
||||||
;; special case when argument needs inference
|
|
||||||
[(_ body* _)
|
|
||||||
(let ([ts (for/list ([ac (syntax->list actuals)]
|
|
||||||
[f (syntax->list args)])
|
|
||||||
(let* ([infer-t (or (type-annotation f #:infer #t)
|
|
||||||
(find-annotation #'(begin . body*) f))])
|
|
||||||
(if infer-t
|
|
||||||
(check-below (tc-expr/t ac) infer-t)
|
|
||||||
(generalize (tc-expr/t ac)))))])
|
|
||||||
(add-typeof-expr lam (tc/rec-lambda/check form args body lp ts expected))
|
|
||||||
expected)]))
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
;; the main dispatching function
|
;; the main dispatching function
|
||||||
;; syntax tc-results? -> tc-results?
|
;; syntax tc-results? -> tc-results?
|
||||||
(define (tc/app/internal form expected)
|
(define (tc/app/internal form expected)
|
||||||
|
@ -100,6 +42,7 @@
|
||||||
(tc/app-keywords form expected)
|
(tc/app-keywords form expected)
|
||||||
(tc/app-objects form expected)
|
(tc/app-objects form expected)
|
||||||
(tc/app-eq form expected)
|
(tc/app-eq form expected)
|
||||||
|
(tc/app-lambda form expected)
|
||||||
(syntax-parse form
|
(syntax-parse form
|
||||||
#:literals (#%plain-app #%plain-lambda letrec-values quote
|
#:literals (#%plain-app #%plain-lambda letrec-values quote
|
||||||
not false? list
|
not false? list
|
||||||
|
@ -140,12 +83,6 @@
|
||||||
(match (single-value #'arg)
|
(match (single-value #'arg)
|
||||||
[(tc-result1: t (FilterSet: f+ f-) _)
|
[(tc-result1: t (FilterSet: f+ f-) _)
|
||||||
(ret -Boolean (make-FilterSet f- f+))])]
|
(ret -Boolean (make-FilterSet f- f+))])]
|
||||||
;; even more special case for match
|
|
||||||
[(#%plain-app (letrec-values ([(lp) (~and lam (#%plain-lambda args . body))]) lp*) . actuals)
|
|
||||||
#:fail-unless expected #f
|
|
||||||
#:fail-unless (not (andmap type-annotation (syntax->list #'(lp . args)))) #f
|
|
||||||
#:fail-unless (free-identifier=? #'lp #'lp*) #f
|
|
||||||
(let-loop-check form #'lam #'lp #'actuals #'args #'body expected)]
|
|
||||||
;; special case for (current-contract-region)'s default expansion
|
;; special case for (current-contract-region)'s default expansion
|
||||||
;; just let it through without any typechecking, since module-name-fixup
|
;; just let it through without any typechecking, since module-name-fixup
|
||||||
;; is a private function from syntax/location, so this must have been
|
;; is a private function from syntax/location, so this must have been
|
||||||
|
@ -160,30 +97,6 @@
|
||||||
#:declare mp1 (id-from 'make-promise 'racket/promise)
|
#:declare mp1 (id-from 'make-promise 'racket/promise)
|
||||||
#:declare mp2 (id-from 'make-promise 'racket/promise)
|
#:declare mp2 (id-from 'make-promise 'racket/promise)
|
||||||
(ret (-Promise (tc-expr/t #'e)))]
|
(ret (-Promise (tc-expr/t #'e)))]
|
||||||
;; inference for ((lambda
|
|
||||||
[(#%plain-app (#%plain-lambda (x ...) . body) args ...)
|
|
||||||
#:fail-unless (= (length (syntax->list #'(x ...)))
|
|
||||||
(length (syntax->list #'(args ...))))
|
|
||||||
#f
|
|
||||||
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
|
|
||||||
(tc/let-values #'((x) ...) #'(args ...) #'body
|
|
||||||
#'(let-values ([(x) args] ...) . body)
|
|
||||||
expected)]
|
|
||||||
;; inference for ((lambda with dotted rest
|
|
||||||
[(#%plain-app (#%plain-lambda (x ... . rst:id) . body) args ...)
|
|
||||||
#:fail-unless (<= (length (syntax->list #'(x ...)))
|
|
||||||
(length (syntax->list #'(args ...)))) #f
|
|
||||||
;; FIXME - remove this restriction - doesn't work because the annotation
|
|
||||||
;; on rst is not a normal annotation, may have * or ...
|
|
||||||
#:fail-when (type-annotation #'rst) #f
|
|
||||||
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
|
|
||||||
(let-values ([(fixed-args varargs)
|
|
||||||
(split-at (syntax->list #'(args ...)) (length (syntax->list #'(x ...))))])
|
|
||||||
(with-syntax ([(fixed-args ...) fixed-args]
|
|
||||||
[varg #`(#%plain-app list #,@varargs)])
|
|
||||||
(tc/let-values #'((x) ... (rst)) #`(fixed-args ... varg) #'body
|
|
||||||
#'(let-values ([(x) fixed-args] ... [(rst) varg]) . body)
|
|
||||||
expected)))]
|
|
||||||
[_ (tc/app/regular form expected)])))
|
[_ (tc/app/regular form expected)])))
|
||||||
|
|
||||||
(define (tc/app/regular form expected)
|
(define (tc/app/regular form expected)
|
||||||
|
|
104
collects/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
Normal file
104
collects/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
Normal file
|
@ -0,0 +1,104 @@
|
||||||
|
#lang racket/unit
|
||||||
|
|
||||||
|
(require "../../utils/utils.rkt"
|
||||||
|
syntax/parse racket/match racket/list
|
||||||
|
unstable/sequence
|
||||||
|
(typecheck signatures tc-app-helper tc-funapp check-below find-annotation )
|
||||||
|
(types abbrev utils generalize type-table)
|
||||||
|
(private type-annotation)
|
||||||
|
(rep type-rep)
|
||||||
|
|
||||||
|
(for-template racket/base))
|
||||||
|
|
||||||
|
|
||||||
|
(import tc-expr^ tc-let^ tc-lambda^)
|
||||||
|
(export tc-app-lambda^)
|
||||||
|
|
||||||
|
(define (tc/app-lambda form expected)
|
||||||
|
(syntax-parse form
|
||||||
|
#:literals (#%plain-app #%plain-lambda letrec-values)
|
||||||
|
;; let loop
|
||||||
|
[(#%plain-app (letrec-values ([(lp) (~and lam (#%plain-lambda args . body))]) lp*) . actuals)
|
||||||
|
#:fail-unless expected #f
|
||||||
|
#:fail-unless (not (andmap type-annotation (syntax->list #'(lp . args)))) #f
|
||||||
|
#:fail-unless (free-identifier=? #'lp #'lp*) #f
|
||||||
|
(let-loop-check form #'lam #'lp #'actuals #'args #'body expected)]
|
||||||
|
;; inference for ((lambda
|
||||||
|
[(#%plain-app (#%plain-lambda (x ...) . body) args ...)
|
||||||
|
#:fail-unless (= (length (syntax->list #'(x ...)))
|
||||||
|
(length (syntax->list #'(args ...))))
|
||||||
|
#f
|
||||||
|
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
|
||||||
|
(tc/let-values #'((x) ...) #'(args ...) #'body
|
||||||
|
#'(let-values ([(x) args] ...) . body)
|
||||||
|
expected)]
|
||||||
|
;; inference for ((lambda with dotted rest
|
||||||
|
[(#%plain-app (#%plain-lambda (x ... . rst:id) . body) args ...)
|
||||||
|
#:fail-unless (<= (length (syntax->list #'(x ...)))
|
||||||
|
(length (syntax->list #'(args ...)))) #f
|
||||||
|
;; FIXME - remove this restriction - doesn't work because the annotation
|
||||||
|
;; on rst is not a normal annotation, may have * or ...
|
||||||
|
#:fail-when (type-annotation #'rst) #f
|
||||||
|
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
|
||||||
|
(let-values ([(fixed-args varargs)
|
||||||
|
(split-at (syntax->list #'(args ...)) (length (syntax->list #'(x ...))))])
|
||||||
|
(with-syntax ([(fixed-args ...) fixed-args]
|
||||||
|
[varg #`(#%plain-app list #,@varargs)])
|
||||||
|
(tc/let-values #'((x) ... (rst)) #`(fixed-args ... varg) #'body
|
||||||
|
#'(let-values ([(x) fixed-args] ... [(rst) varg]) . body)
|
||||||
|
expected)))]
|
||||||
|
[_ #f]))
|
||||||
|
|
||||||
|
(define (let-loop-check form lam lp actuals args body expected)
|
||||||
|
(syntax-parse #`(#,args #,body #,actuals)
|
||||||
|
#:literals (#%plain-app if null? pair? null)
|
||||||
|
[((val acc ...)
|
||||||
|
((~and inner-body (if (#%plain-app (~or pair? null?) val*) thn els)))
|
||||||
|
(actual actuals ...))
|
||||||
|
#:when
|
||||||
|
(and (free-identifier=? #'val #'val*)
|
||||||
|
(ormap (lambda (a) (find-annotation #'inner-body a))
|
||||||
|
(syntax->list #'(acc ...))))
|
||||||
|
(let* ([ts1 (generalize (tc-expr/t #'actual))]
|
||||||
|
[ann-ts (for/list ([a (in-syntax #'(acc ...))]
|
||||||
|
[ac (in-syntax #'(actuals ...))])
|
||||||
|
(or (find-annotation #'inner-body a)
|
||||||
|
(generalize (tc-expr/t ac))))]
|
||||||
|
[ts (cons ts1 ann-ts)])
|
||||||
|
;; check that the actual arguments are ok here
|
||||||
|
(for/list ([a (syntax->list #'(actuals ...))]
|
||||||
|
[t ann-ts])
|
||||||
|
(tc-expr/check a (ret t)))
|
||||||
|
;; then check that the function typechecks with the inferred types
|
||||||
|
(add-typeof-expr lam (tc/rec-lambda/check form args body lp ts expected))
|
||||||
|
expected)]
|
||||||
|
;; special case `for/list'
|
||||||
|
[((val acc ...)
|
||||||
|
((~and inner-body (if e1 e2 e3:id)))
|
||||||
|
(null actuals ...))
|
||||||
|
#:when (free-identifier=? #'val #'e3)
|
||||||
|
(let ([ts (for/list ([ac (syntax->list #'(actuals ...))]
|
||||||
|
[f (syntax->list #'(acc ...))])
|
||||||
|
(or
|
||||||
|
(type-annotation f #:infer #t)
|
||||||
|
(generalize (tc-expr/t ac))))]
|
||||||
|
[acc-ty (or
|
||||||
|
(type-annotation #'val #:infer #t)
|
||||||
|
(match expected
|
||||||
|
[(tc-result1: (and t (Listof: _))) t]
|
||||||
|
[_ #f])
|
||||||
|
(generalize (-val '())))])
|
||||||
|
(add-typeof-expr lam (tc/rec-lambda/check form args body lp (cons acc-ty ts) expected))
|
||||||
|
expected)]
|
||||||
|
;; special case when argument needs inference
|
||||||
|
[(_ body* _)
|
||||||
|
(let ([ts (for/list ([ac (syntax->list actuals)]
|
||||||
|
[f (syntax->list args)])
|
||||||
|
(let* ([infer-t (or (type-annotation f #:infer #t)
|
||||||
|
(find-annotation #'(begin . body*) f))])
|
||||||
|
(if infer-t
|
||||||
|
(check-below (tc-expr/t ac) infer-t)
|
||||||
|
(generalize (tc-expr/t ac)))))])
|
||||||
|
(add-typeof-expr lam (tc/rec-lambda/check form args body lp ts expected))
|
||||||
|
expected)]))
|
||||||
|
|
|
@ -10,6 +10,7 @@
|
||||||
"tc-app/tc-app-eq.rkt"
|
"tc-app/tc-app-eq.rkt"
|
||||||
"tc-app/tc-app-hetero.rkt"
|
"tc-app/tc-app-hetero.rkt"
|
||||||
"tc-app/tc-app-keywords.rkt"
|
"tc-app/tc-app-keywords.rkt"
|
||||||
|
"tc-app/tc-app-lambda.rkt"
|
||||||
"tc-app/tc-app-list.rkt"
|
"tc-app/tc-app-list.rkt"
|
||||||
"tc-app/tc-app-objects.rkt"
|
"tc-app/tc-app-objects.rkt"
|
||||||
"tc-app/tc-app-values.rkt"
|
"tc-app/tc-app-values.rkt"
|
||||||
|
@ -23,4 +24,4 @@
|
||||||
(define-values/invoke-unit/infer
|
(define-values/invoke-unit/infer
|
||||||
(link tc-if@ tc-lambda@ tc-app@ tc-let@ tc-expr@ check-subforms@ tc-apply@
|
(link tc-if@ tc-lambda@ tc-app@ tc-let@ tc-expr@ check-subforms@ tc-apply@
|
||||||
tc-app-hetero@ tc-app-list@ tc-app-apply@ tc-app-values@ tc-app-keywords@
|
tc-app-hetero@ tc-app-list@ tc-app-apply@ tc-app-values@ tc-app-keywords@
|
||||||
tc-app-objects@ tc-app-eq@))
|
tc-app-objects@ tc-app-eq@ tc-app-lambda@))
|
||||||
|
|
Loading…
Reference in New Issue
Block a user