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

Change tc-app-lambda to not return bad filters.

Browse Source 
Makes tc/rec-lambda/check return the actual results, and erase the names of
the values bound by the let.

original commit: 8cf1246fb1d32e1ea4cf1d1df4bfc6c70ae30f46
This commit is contained in:
Eric Dobson 2014-03-19 20:19:25 -07:00
parent 2f3ec59680
commit b518da29d3
5 changed files with 64 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
View File

@ -3,6 +3,7 @@
(require "../../utils/utils.rkt"
"signatures.rkt"
"utils.rkt"
(prefix-in - (contract-req))
syntax/parse racket/match racket/list
unstable/sequence unstable/syntax
(typecheck signatures find-annotation)
@ -53,7 +54,9 @@
expected)))))
(define (let-loop-check lam lp actuals args body expected)
(define/cond-contract
(let-loop-check lam lp actuals args body expected)
(syntax? syntax? syntax? syntax? syntax? tc-results/c . --> . tc-results/c)
(syntax-parse #`(#,args #,body #,actuals)
#:literal-sets (kernel-literals lambda-literals)
[((val acc ...)
@ -76,8 +79,10 @@
[t (in-list 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 args body lp ts expected))
expected)]
(define-values (fun-results body-results)
(tc/rec-lambda/check args body lp ts expected))
(add-typeof-expr lam fun-results)
body-results)]
;; special case `for/list'
[((val acc ...)
((~and inner-body (if e1 e2 e3:id)))
@ -95,8 +100,10 @@
[(tc-result1: (and t (Listof: _))) t]
[_ #f])
(generalize (-val '())))])
(add-typeof-expr lam (tc/rec-lambda/check args body lp (cons acc-ty ts) expected))
expected)]
(define-values (fun-results body-results)
(tc/rec-lambda/check args body lp (cons acc-ty ts) expected))
(add-typeof-expr lam fun-results)
body-results)]
;; special case when argument needs inference
[(_ body* _)
(let ([ts (for/list ([ac (in-syntax actuals)]
@ -106,6 +113,8 @@
(if infer-t
(tc-expr/check/t ac (ret infer-t))
(generalize (tc-expr/t ac)))))])
(add-typeof-expr lam (tc/rec-lambda/check args body lp ts expected))
expected)]))
(define-values (fun-results body-results)
(tc/rec-lambda/check args body lp ts expected))
(add-typeof-expr lam fun-results)
body-results)]))

10
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
View File

@ -520,12 +520,16 @@
;; name : the name of the loop
;; args : the types of the actual arguments to the loop
;; ret : the expected return type of the whole expression
(define (tc/rec-lambda/check formals body name args return)
;; Returns both the tc-results of the function and of the body
(define (tc/rec-lambda/check formals* body name args return)
(define formals (syntax->list formals*))
(with-lexical-env/extend
(syntax->list formals) args
formals args
(let* ([r (tc-results->values return)]
[t (make-arr args r)]
[ft (make-Function (list t))])
(with-lexical-env/extend
(list name) (list ft)
(begin (tc-body/check body return) (ret ft))))))
(values
(erase-names/results formals (ret ft))
(erase-names/results formals (tc-body/check body return)))))))

40
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
View File

@ -8,7 +8,7 @@
global-env type-env-structs scoped-tvar-env)
(rep type-rep filter-rep)
syntax/free-vars
(typecheck signatures tc-metafunctions tc-subst internal-forms)
(typecheck signatures tc-metafunctions internal-forms)
(utils tarjan)
racket/match (contract-req)
syntax/parse syntax/stx
@ -64,31 +64,19 @@
clauses
exprs
expected-results)
(let ([subber (lambda (proc lst)
(for/list ([i (in-list lst)])
(for/fold ([s i])
([nm (in-list (apply append abstract namess))])
(proc s nm -empty-obj #t))))])
(define (run res)
(match res
[(tc-any-results:) res]
[(tc-results: ts fs os)
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
[(tc-results: ts fs os dt db)
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)]))
(with-lexical-env/extend/props
;; we typechecked the rhss with the lhss having types that potentially contain undefined
;; if undefined can actually show up, a type error will have been triggered
;; it is therefore safe to typecheck the body with the original types the user gave us
;; any undefined-related problems have been caught already
namess
expected-types ; types w/o undefined
(append p1 p2)
;; typecheck the body
(run
(if expected
(tc-body/check body (erase-filter expected))
(tc-body body)))))))
(with-lexical-env/extend/props
;; we typechecked the rhss with the lhss having types that potentially contain undefined
;; if undefined can actually show up, a type error will have been triggered
;; it is therefore safe to typecheck the body with the original types the user gave us
;; any undefined-related problems have been caught already
namess
expected-types ; types w/o undefined
(append p1 p2)
;; typecheck the body
(erase-names/results (apply append abstract namess)
(if expected
(tc-body/check body (erase-filter expected))
(tc-body body))))))
(define (tc-expr/maybe-expected/t e names)
(syntax-parse names

27
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt
View File

@ -5,9 +5,11 @@
(except-in (types abbrev union utils filter-ops)
-> ->* one-of/c)
(rep type-rep filter-rep object-rep rep-utils)
(typecheck tc-subst)
(contract-req))
(provide abstract-results
erase-names/results
combine-props
tc-results->values)
@ -100,20 +102,13 @@
;; the scope count in the keys so that names are
;; substituted with the correct level of nesting
(λ (type)
(abstract-type ids (add-scope keys) type))])
(abstract-type ids (map add-scope keys) type))])
(make-arr (map at dom)
(at* rng) ; only increase scope in range
(and rest (at rest))
(and drest (cons (at (car drest)) (cdr drest)))
(map at kws)))]))
;; add-scope : Listof<name-ref/c> -> Listof<name-ref/c>
;; Add a scope to the index object
(define (add-scope keys)
(for/list ([depth+arg keys])
(match-define (list depth arg) depth+arg)
(list (+ 1 depth) arg)))
;; Abstract all given id objects into index objects (keys) in
;; the given object
(define/cond-contract (abstract-object ids keys o)
@ -246,3 +241,19 @@
[(Bot:) (set-box! flag #f) (values derived-props derived-atoms)]
[_ (loop (cons p derived-props) derived-atoms (cdr worklist))])))))
;; erase-names/results: (listof identifier?) tc-results? -> tc-results?
;; Maps all of the given names in the results to the empty object.
;; This is used so that names do not escape the scope of their definitions
;; TODO support mapping names to other objects.
(define (erase-names/results names res)
(define (subber proc lst)
(for/list ([i (in-list lst)])
(for/fold ([s i])
([nm (in-list names)])
(proc s nm -empty-obj #t))))
(match res
[(tc-any-results:) res]
[(tc-results: ts fs os)
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
[(tc-results: ts fs os dt db)
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)]))

16
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -933,7 +933,7 @@
(do: : Number ((x : (Listof Number) x (cdr x))
(sum : Number 0 (+ sum (car x))))
((null? x) sum)))
#:ret (ret -Number -top-filter -no-obj)]
#:ret (ret -Number -top-filter -empty-obj)]
[tc-e/t (if #f 1 'foo) (-val 'foo)]
@ -1179,7 +1179,7 @@
([j : Natural (+ i 'a) (+ j i)])
((>= j 10))
#f)
#:ret (ret -Void -no-filter -no-obj)]
#:ret (ret -Void -top-filter -empty-obj)]
[tc-err (apply +)]
[tc-e/t
(let ([x eof])
@ -1748,7 +1748,7 @@
[tc-e (let ([my-pred (λ () #f)])
(for/and: : Any ([i (in-range 4)])
(my-pred)))
#:ret (ret Univ -top-filter -no-obj)]
#:ret (ret Univ -top-filter -empty-obj)]
[tc-e
(let ()
(define: long : (List 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 Integer)
@ -1864,7 +1864,7 @@
(ann
((letrec ((x (lambda (acc #{ v : Symbol}) (if v (list v) acc)))) x) null (list 'bad 'prog))
(Listof Symbol))
#:ret (ret (-lst -Symbol) -no-filter -no-obj)]
#:ret (ret (-lst -Symbol) -top-filter -empty-obj)]
[tc-e (filter values empty)
(-lst -Bottom)]
[tc-e (lambda lst (map (plambda: (b) ([x : b]) x) lst))
@ -2150,7 +2150,7 @@
(values x y))
#:ret (ret (-HT -Symbol -String)
(-FS -top -top)
-no-obj)]
-empty-obj)]
[tc-e (for*/hash: : (HashTable Symbol String)
([k (in-list '(x y z))]
[v (in-list '("a" "b"))]
@ -2158,7 +2158,7 @@
(values k v))
#:ret (ret (-HT -Symbol -String)
(-FS -top -top)
-no-obj)]
-empty-obj)]
;; PR 13937
[tc-e (let ()
@ -2399,9 +2399,9 @@
[tc-e (let/ec k : String (k "foo")) -String]
[tc-e (ann (do ([x : Integer 0 (add1 x)]) ((> x 10) x) (displayln x))
Integer)
#:ret (ret -Integer -no-filter -no-obj)]
#:ret (ret -Integer -top-filter -empty-obj)]
[tc-e (do : Integer ([x : Integer 0 (add1 x)]) ((> x 10) x) (displayln x))
#:ret (ret -Integer -no-filter -no-obj)]
#:ret (ret -Integer -top-filter -empty-obj)]
[tc-e (tr:case-lambda [(x [y : String]) x])
#:ret (ret (t:-> Univ -String Univ
: (-FS (-not-filter (-val #f) (list 0 0))