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

Make tc-expr the same implementation as tc-expr/check.

Browse Source
This commit is contained in:
Eric Dobson 2014-05-26 12:05:39 -07:00
parent 5431ddb6c1
commit a8bc079c4b
2 changed files with 53 additions and 138 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/signatures.rkt
View File

@ -7,7 +7,7 @@
(define-signature tc-expr^ (define-signature tc-expr^
([cond-contracted tc-expr (syntax? . -> . full-tc-results/c)] ([cond-contracted tc-expr (syntax? . -> . full-tc-results/c)]
[cond-contracted tc-expr/check (syntax? tc-results/c . -> . full-tc-results/c)] [cond-contracted tc-expr/check (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]
[cond-contracted tc-expr/check/t (syntax? tc-results/c . -> . Type/c)] [cond-contracted tc-expr/check/t (syntax? tc-results/c . -> . Type/c)]
[cond-contracted tc-body (syntax? . -> . full-tc-results/c)] [cond-contracted tc-body (syntax? . -> . full-tc-results/c)]
[cond-contracted tc-body/check (syntax? tc-results/c . -> . full-tc-results/c)] [cond-contracted tc-body/check (syntax? tc-results/c . -> . full-tc-results/c)]
@ -23,7 +23,7 @@
([cond-contracted check-class (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)])) ([cond-contracted check-class (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]))
(define-signature tc-if^ (define-signature tc-if^
([cond-contracted tc/if-twoarm ((syntax? syntax? syntax?) (tc-results/c) . ->* . full-tc-results/c)])) ([cond-contracted tc/if-twoarm ((syntax? syntax? syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]))
(define-signature tc-literal^ (define-signature tc-literal^
([cond-contracted tc-literal (->* (syntax?) ((or/c Type/c #f)) Type/c)])) ([cond-contracted tc-literal (->* (syntax?) ((or/c Type/c #f)) Type/c)]))

187
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
View File

@ -64,7 +64,7 @@
;; typecheck form ;; typecheck form
(define t (tc-expr/check/internal form expected)) (define t (tc-expr/check/internal form expected))
(add-typeof-expr form t) (add-typeof-expr form t)
(check-below t expected))) (cond-check-below t expected)))
(define (explicit-fail stx msg var) (define (explicit-fail stx msg var)
(cond [(and (identifier? var) (lookup-type/lexical var #:fail (λ _ #f))) (cond [(and (identifier? var) (lookup-type/lexical var #:fail (λ _ #f)))
@ -75,9 +75,9 @@
t))] t))]
[else (tc-error/expr #:stx stx (syntax-e msg))])) [else (tc-error/expr #:stx stx (syntax-e msg))]))
;; tc-expr/check : syntax tc-results -> tc-results ;; tc-expr/check : syntax maybe[tc-results] -> tc-results
(define/cond-contract (tc-expr/check/internal form expected) (define/cond-contract (tc-expr/check/internal form expected)
(--> syntax? tc-results/c full-tc-results/c) (--> syntax? (-or/c tc-results/c #f) full-tc-results/c)
(parameterize ([current-orig-stx form]) (parameterize ([current-orig-stx form])
;(printf "form: ~a\n" (syntax-object->datum form)) ;(printf "form: ~a\n" (syntax-object->datum form))
;; the argument must be syntax ;; the argument must be syntax
@ -90,7 +90,9 @@
(check-class form expected)] (check-class form expected)]
[stx:exn-handlers^ [stx:exn-handlers^
(register-ignored! form) (register-ignored! form)
(check-subforms/with-handlers/check form expected)] (if expected
(check-subforms/with-handlers/check form expected)
(check-subforms/with-handlers form))]
;; explicit failure ;; explicit failure
[t:typecheck-failure [t:typecheck-failure
(explicit-fail #'t.stx #'t.message #'t.var)] (explicit-fail #'t.stx #'t.message #'t.var)]
@ -102,7 +104,7 @@
[(tc-result1: t) [(tc-result1: t)
(ret (tc-literal #'val t) -true-filter)] (ret (tc-literal #'val t) -true-filter)]
[_ [_
(ret (tc-literal #'val #f))])] (ret (tc-literal #'val) -true-filter)])]
;; syntax ;; syntax
[(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) -true-filter)] [(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) -true-filter)]
;; mutation! ;; mutation!
@ -124,12 +126,16 @@
(match key-t (match key-t
[(tc-result1: (Continuation-Mark-Keyof: rhs)) [(tc-result1: (Continuation-Mark-Keyof: rhs))
(tc-expr/check/type #'e2 rhs) (tc-expr/check/type #'e2 rhs)
(tc-expr/check #'e3 expected)] (if expected
(tc-expr/check #'e3 expected)
(tc-expr #'e3))]
[(? (λ (result) [(? (λ (result)
(and (identifier? #'e1) (and (identifier? #'e1)
(free-identifier=? #'pz:pk #'e1 #f (syntax-local-phase-level))))) (free-identifier=? #'pz:pk #'e1 #f (syntax-local-phase-level)))))
(tc-expr/check/type #'e2 Univ) (tc-expr/check/type #'e2 Univ)
(tc-expr/check #'e3 expected)] (if expected
(tc-expr/check #'e3 expected)
(tc-expr #'e3))]
[(tc-result1: key-t) [(tc-result1: key-t)
;(check-below key-t -Symbol) ;(check-below key-t -Symbol)
;; FIXME -- would need to protect `e2` with any-wrap/c contract ;; FIXME -- would need to protect `e2` with any-wrap/c contract
@ -139,7 +145,10 @@
;(tc-expr/check #'e3 expected) ;(tc-expr/check #'e3 expected)
(tc-error/expr "with-continuation-mark requires a continuation-mark-key, but got ~a" key-t)])] (tc-error/expr "with-continuation-mark requires a continuation-mark-key, but got ~a" key-t)])]
;; application ;; application
[(#%plain-app . _) (tc/app/check form expected)] [(#%plain-app . _)
(if expected
(tc/app/check form expected)
(tc/app form))]
;; #%expression ;; #%expression
[(#%expression e) (tc/#%expression form expected)] [(#%expression e) (tc/#%expression form expected)]
;; syntax ;; syntax
@ -147,18 +156,25 @@
[(letrec-syntaxes+values stxs vals . body) [(letrec-syntaxes+values stxs vals . body)
(tc-expr/check (syntax/loc form (letrec-values vals . body)) expected)] (tc-expr/check (syntax/loc form (letrec-values vals . body)) expected)]
;; begin ;; begin
[(begin . es) (tc-body/check #'es expected)] [(begin . es)
(if expected
(tc-body/check #'es expected)
(tc-body #'es))]
[(begin0 e . es) [(begin0 e . es)
(begin0 (begin0
(tc-expr/check #'e expected) (if expected (tc-expr/check #'e expected) (tc-expr #'e))
(tc-body/check #'es (tc-any-results -top)))] (tc-body/check #'es (tc-any-results -top)))]
;; if ;; if
[(if tst thn els) (tc/if-twoarm #'tst #'thn #'els expected)] [(if tst thn els) (tc/if-twoarm #'tst #'thn #'els expected)]
;; lambda ;; lambda
[(#%plain-lambda formals . body) [(#%plain-lambda formals . body)
(tc/lambda/check form #'(formals) #'(body) expected)] (if expected
(tc/lambda/check form #'(formals) #'(body) expected)
(tc/lambda form #'(formals) #'(body)))]
[(case-lambda [formals . body] ...) [(case-lambda [formals . body] ...)
(tc/lambda/check form #'(formals ...) #'(body ...) expected)] (if expected
(tc/lambda/check form #'(formals ...) #'(body ...) expected)
(tc/lambda form #'(formals ...) #'(body ...)))]
;; send ;; send
[(let-values (((_) meth)) [(let-values (((_) meth))
(let-values (((_) rcvr)) (let-values (((_) rcvr))
@ -170,7 +186,9 @@
(register-ignored! form) (register-ignored! form)
(tc/send #'find-app #'rcvr #'meth #'(args ...) expected)] (tc/send #'find-app #'rcvr #'meth #'(args ...) expected)]
;; kw function def ;; kw function def
;; TODO simplify this case
[(~and (let-values ([(f) fun]) . body) _:kw-lambda^) [(~and (let-values ([(f) fun]) . body) _:kw-lambda^)
#:when expected
(match expected (match expected
[(tc-result1: (and f (or (Function: _) [(tc-result1: (and f (or (Function: _)
(Poly: _ (Function: _))))) (Poly: _ (Function: _)))))
@ -180,6 +198,7 @@
(tc-expr form)])] (tc-expr form)])]
;; opt function def ;; opt function def
[(~and (let-values ([(f) fun]) . body) opt:opt-lambda^) [(~and (let-values ([(f) fun]) . body) opt:opt-lambda^)
#:when expected
(define conv-type (define conv-type
(match expected (match expected
[(tc-result1: fun-type) [(tc-result1: fun-type)
@ -190,89 +209,22 @@
(if conv-type (if conv-type
(begin (tc-expr/check/type #'fun conv-type) expected) (begin (tc-expr/check/type #'fun conv-type) expected)
(tc-expr form))] (tc-expr form))]
;; let
[(let-values ([(name ...) expr] ...) . body)
(tc/let-values #'((name ...) ...) #'(expr ...) #'body expected)]
[(letrec-values ([(name ...) expr] ...) . body)
(tc/letrec-values #'((name ...) ...) #'(expr ...) #'body expected)]
;; other
[_ (int-err "cannot typecheck unknown form : ~s" (syntax->datum form))]
)))
;; type check form in the current type environment
;; if there is a type error in form, or if it has the wrong annotation, error
;; otherwise, produce the type of form
;; syntax[expr] -> type
(define (tc-expr form)
;; do the actual typechecking of form
;; internal-tc-expr : syntax -> Type
(define (internal-tc-expr form)
(syntax-parse form
#:literal-sets (kernel-literals tc-expr-literals)
[stx:tr:class^
(check-class form #f)]
;;
[stx:exn-handlers^
(register-ignored! form)
(check-subforms/with-handlers form) ]
;; explicit failure
[t:typecheck-failure
(explicit-fail #'t.stx #'t.message #'t.var)]
;; data
[(quote #f) (ret (-val #f) -false-filter)]
[(quote #t) (ret (-val #t) -true-filter)]
[(quote val) (ret (tc-literal #'val) -true-filter)]
;; syntax
[(quote-syntax datum) (ret (-Syntax (tc-literal #'datum)) -true-filter)]
;; w-c-m
[(with-continuation-mark e1 e2 e3)
(define key-t (single-value #'e1))
(match key-t
[(tc-result1: (Continuation-Mark-Keyof: rhs))
(tc-expr/check/type #'e2 rhs)
(tc-expr #'e3)]
[(? (λ (result)
(and (identifier? #'e1)
(free-identifier=? #'pz:pk #'e1 #f (syntax-local-phase-level)))))
(tc-expr/check/type #'e2 Univ)
(tc-expr #'e3)]
[(tc-result1: key-t)
;; see comments in the /check variant
(tc-error/expr "with-continuation-mark requires a continuation-mark-key, but got ~a" key-t)])]
;; lambda
[(#%plain-lambda formals . body)
(tc/lambda form #'(formals) #'(body))]
[(case-lambda [formals . body] ...)
(tc/lambda form #'(formals ...) #'(body ...))]
;; send
[(let-values (((_) meth))
(let-values (((_) rcvr))
(let-values (((_) (~and find-app (#%plain-app find-method/who _ _ _))))
(let-values ([_arg-var args] ...)
(if wrapped-object-check
ignore-this-case
(#%plain-app _ _ _arg-var2 ...))))))
(register-ignored! form)
(tc/send #'find-app #'rcvr #'meth #'(args ...))]
;; kw function def
[(~and _:kw-lambda^ [(~and _:kw-lambda^
(let-values ([(f) fun]) (let-values ([(f) fun])
(let-values _ (let-values _
(#%plain-app (#%plain-app
maker maker
lambda-for-kws lambda-for-kws
(case-lambda ; wrapper function (case-lambda ; wrapper function
(formals . cl-body) ...) (formals . cl-body) ...)
(~or (quote (mand-kw:keyword ...)) (~or (quote (mand-kw:keyword ...))
(~and _ (~bind [(mand-kw 1) '()]))) (~and _ (~bind [(mand-kw 1) '()])))
(quote (all-kw:keyword ...)) (quote (all-kw:keyword ...))
. rst)))) . rst))))
(ret (kw-unconvert (tc-expr/t #'fun) (ret (kw-unconvert (tc-expr/t #'fun)
(syntax->list #'(formals ...)) (syntax->list #'(formals ...))
(syntax->datum #'(mand-kw ...)) (syntax->datum #'(mand-kw ...))
(syntax->datum #'(all-kw ...))))] (syntax->datum #'(all-kw ...))))]
;; opt function def
[(~and opt:opt-lambda^ [(~and opt:opt-lambda^
(let-values ([(f) fun]) (let-values ([(f) fun])
(case-lambda (formals . cl-body) ...))) (case-lambda (formals . cl-body) ...)))
@ -280,55 +232,18 @@
(syntax->list #'(formals ...))))] (syntax->list #'(formals ...))))]
;; let ;; let
[(let-values ([(name ...) expr] ...) . body) [(let-values ([(name ...) expr] ...) . body)
(tc/let-values #'((name ...) ...) #'(expr ...) #'body)] (tc/let-values #'((name ...) ...) #'(expr ...) #'body expected)]
[(letrec-values ([(name ...) expr] ...) . body) [(letrec-values ([(name ...) expr] ...) . body)
(tc/letrec-values #'((name ...) ...) #'(expr ...) #'body)] (tc/letrec-values #'((name ...) ...) #'(expr ...) #'body expected)]
;; mutation!
[(set! id val)
(match-let* ([(tc-result1: id-t) (tc-expr #'id)]
[(tc-result1: val-t) (tc-expr #'val)])
(unless (subtype val-t id-t)
(type-mismatch id-t val-t "mutation only allowed with compatible types"))
(ret -Void))]
;; top-level variable reference - occurs at top level
[(#%top . id) (tc-id #'id)]
;; #%expression
[(#%expression e) (tc/#%expression form #f)]
;; #%variable-reference
[(#%variable-reference . _)
(ret -Variable-Reference)]
;; identifiers
[x:identifier (tc-id #'x)]
;; application
[(#%plain-app . _) (tc/app form)]
;; if
[(if tst thn els) (tc/if-twoarm #'tst #'thn #'els)]
;; syntax
;; for now, we ignore the rhs of macros
[(letrec-syntaxes+values stxs vals . body)
(tc-expr (syntax/loc form (letrec-values vals . body)))]
;; begin
[(begin . es) (tc-body #'es)]
[(begin0 e . es)
(begin0
(tc-expr #'e)
(tc-body #'es))]
;; other ;; other
[_ (int-err "cannot typecheck unknown form : ~s" (syntax->datum form))])) [_ (int-err "cannot typecheck unknown form : ~s" (syntax->datum form))])))
(parameterize ([current-orig-stx form]) ;; type check form in the current type environment
;(printf "form: ~a\n" (syntax->datum form)) ;; if there is a type error in form, or if it has the wrong annotation, error
;; the argument must be syntax ;; otherwise, produce the type of form
(unless (syntax? form) ;; syntax[expr] -> type
(int-err "bad form input to tc-expr: ~a" form)) (define (tc-expr form)
;; typecheck form (tc-expr/check form #f))
(let ([ty (internal-tc-expr form)])
(add-typeof-expr form ty)
ty)))
(define (single-value form [expected #f]) (define (single-value form [expected #f])
(define t (if expected (tc-expr/check form expected) (tc-expr form))) (define t (if expected (tc-expr/check form expected) (tc-expr form)))