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

don't throw internal errors for unreachable cast exprs (#386)

Browse Source 
This fills the corresponding entries in the cast table with a Dead-Code
type so that when the contract-generation pass calls the contract-def
thunk, it finds that in the table.
This commit is contained in:
Alex Knauth 2016-07-07 16:51:08 -04:00 committed by Sam Tobin-Hochstadt
parent e3f56c8a25
commit 9f3cf01d26
3 changed files with 58 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
typed-racket-lib/typed-racket/typecheck/tc-if.rkt
View File

@ -1,11 +1,13 @@
#lang racket/unit
(require "../utils/utils.rkt"
(rep prop-rep)
(types utils prop-ops)
(types abbrev utils prop-ops)
(utils tc-utils)
(typecheck signatures tc-envops tc-metafunctions)
(types type-table)
racket/match)
(private syntax-properties)
racket/match
syntax/parse)
;; if typechecking
(import tc-expr^)
@ -17,13 +19,44 @@
(define expected* (and expected (erase-props expected)))
(define results-t
(with-lexical-env/extend-props (list fs+)
#:unreachable (warn-unreachable thn)
#:unreachable (begin
(handle-unreachable-casted-exprs thn)
(warn-unreachable thn))
(test-position-add-true tst)
(tc-expr/check thn expected*)))
(define results-u
(with-lexical-env/extend-props (list fs-)
#:unreachable (warn-unreachable els)
#:unreachable (begin
(handle-unreachable-casted-exprs els)
(warn-unreachable els))
(test-position-add-false tst)
(tc-expr/check els expected*)))
(merge-tc-results (list results-t results-u))]))
;; handle-unreachable-casted-exprs : Any -> Void
;; Traverses stx looking for casted-expr properties. For each one, it
;; calls the function stored in the property, which fills an entry in
;; the cast table with the -Dead-Code type. This is so that the
;; contract-generation pass doesn't throw an internal error.
(define (handle-unreachable-casted-exprs stx)
(syntax-parse stx
[(exp:casted-expr^ e)
;; fill in this entry in the cast table with the -Dead-Code type
((attribute exp.value) -Dead-Code)
(void)]
[stx
(define e (syntax-e #'stx))
(cond
[(pair? e) (handle-unreachable-casted-exprs (car e))
(handle-unreachable-casted-exprs (cdr e))]
[(box? e) (handle-unreachable-casted-exprs (unbox e))]
[(vector? e) (for ([e (in-vector e)])
(handle-unreachable-casted-exprs e))]
[(hash? e) (for ([(k v) (in-hash e)])
(handle-unreachable-casted-exprs k)
(handle-unreachable-casted-exprs v))]
[(struct? e) (for ([e (in-vector (struct->vector e))])
(handle-unreachable-casted-exprs e))]
[else (void)])]))

4
typed-racket-lib/typed-racket/types/abbrev.rkt
View File

@ -80,6 +80,10 @@
(define (-ne-lst t) (-pair t (-lst t)))
;; For casted-exprs in unreachable code, to fill in the cast table.
;; TODO: This contract normally gets optimized away. Is there away to stop that?
(define -Dead-Code (make-Base 'Dead-Code #'(make-none/c 'dead-code/c) (λ (v) #f)))
;; Convenient constructor for Values
;; (wraps arg types with Result)
(define/cond-contract (-values args)

17
typed-racket-test/succeed/cast-mod.rkt
View File

@ -102,3 +102,20 @@
(check-equal? (f (list (list "a") (list "b") (list "c")))
(list (list "a") (list "b") (list "c"))))
(test-case "cast in dead code"
(check-equal? (if #true 1 (cast 2 Integer))
1)
(check-equal? (if #false (cast 1 Integer) 2)
2)
(check-equal? (if #true 1 (list (cast 2 Integer) (cast 3 Integer)))
1)
(check-equal? (if #true 1 `#&,(cast 2 Integer))
1)
(check-equal? (if #true 1 `#(,(cast 2 Integer) ,(cast 3 Integer)))
1)
(check-equal? (if #true 1 `#hash([,(cast 2 Integer) . ,(cast 3 Integer)]))
1)
(check-equal? (if #true 1 `#s(struct ,(cast 2 Integer) ,(cast 3 Integer)))
1)
)