Make with-lexical-env/extend-props not execute its body if its dead.

original commit: 203311e9933df681799c0399a6889a98c1b8f9c0
This commit is contained in:
Eric Dobson 2014-05-24 14:55:07 -07:00
parent 0cef9a0625
commit 8d2615131f
4 changed files with 46 additions and 51 deletions

View File

@ -8,7 +8,7 @@
(infer-in infer)
(rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
(types resolve subtype remove-intersect union filter-ops)
(types tc-result resolve subtype remove-intersect union filter-ops)
(env type-env-structs lexical-env)
(rename-in (types abbrev)
[-> -->]
@ -18,9 +18,6 @@
(provide
with-lexical-env/extend-props)
(provide/cond-contract
[env+ (([e env?] [fs (listof Filter/c)] [bx (box/c boolean?)])
#:pre (bx) (unbox bx) . ->i . [_ env?])])
(define/cond-contract (update t ft pos? lo)
(Type/c Type/c boolean? (listof PathElem?) . -> . Type/c)
@ -63,29 +60,35 @@
(int-err "update along ill-typed path: ~a ~a ~a" t t* lo)
t]))
;; sets the flag box to #f if anything becomes (U)
(define (env+ env fs flag)
(define-values (props atoms) (combine-props fs (env-props env) flag))
(for/fold ([Γ (replace-props env (append atoms props))]) ([f (in-list atoms)])
(match f
[(Bot:) (set-box! flag #f) (env-map (lambda (k v) (Un)) Γ)]
[(or (TypeFilter: ft (Path: lo x)) (NotTypeFilter: ft (Path: lo x)))
(update-type/lexical
(lambda (x t) (let ([new-t (update t ft (TypeFilter? f) lo)])
(when (type-equal? new-t -Bottom)
(set-box! flag #f))
new-t))
x Γ)]
[_ Γ])))
;; Returns #f if anything becomes (U)
(define (env+ env fs)
(let/ec exit
(define-values (props atoms) (combine-props fs (env-props env) exit))
(for/fold ([Γ (replace-props env (append atoms props))]) ([f (in-list atoms)])
(match f
[(or (TypeFilter: ft (Path: lo x)) (NotTypeFilter: ft (Path: lo x)))
(update-type/lexical
(lambda (x t)
(define new-t (update t ft (TypeFilter? f) lo))
(when (type-equal? new-t -Bottom)
(exit #f))
new-t)
x Γ)]
[_ Γ]))))
;; run code in an extended env and with replaced props. Requires the body to return a tc-results.
;; TODO make this only add the new prop instead of the entire environment once tc-id is fixed to
;; include the interesting props in its filter.
(define-syntax (with-lexical-env/extend-props stx)
(define-splicing-syntax-class flag
[pattern (~seq #:flag v:expr)]
[pattern (~seq) #:with v #'(box #t)])
(define-splicing-syntax-class unreachable?
(pattern (~seq #:unreachable form:expr))
(pattern (~seq) #:with form #'(begin)))
(syntax-parse stx
[(_ ps flag:flag . b)
#'(with-lexical-env (env+ (lexical-env) ps flag.v)
(add-unconditional-prop (let () . b) (apply -and (env-props (lexical-env)))))]))
[(_ ps:expr u:unreachable? . b)
#'(let ([new-env (env+ (lexical-env) ps)])
(if new-env
(with-lexical-env new-env
(add-unconditional-prop (let () . b) (apply -and (env-props new-env))))
(let ()
u.form
(ret -Bottom))))]))

View File

@ -13,28 +13,18 @@
(export tc-if^)
(define (tc/if-twoarm tst thn els [expected #f])
(define (tc expr reachable?)
(unless reachable? (warn-unreachable expr))
;; If the code is unreachable, the resulting type should be Bottom.
(if reachable?
(tc-expr/check expr (and expected (erase-filter expected)))
(ret -Bottom)))
(match (single-value tst)
[(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _)
(define flag+ (box #t))
(define flag- (box #t))
[(tc-result1: _ (FilterSet: fs+ fs-) _)
(define expected* (and expected (erase-filter expected)))
(define results-t
(with-lexical-env/extend-props (list fs+) #:flag flag+
(add-unconditional-prop
(tc thn (unbox flag+)) fs+)))
(with-lexical-env/extend-props (list fs+)
#:unreachable (warn-unreachable thn)
(test-position-add-true tst)
(tc-expr/check thn expected*)))
(define results-u
(with-lexical-env/extend-props (list fs-) #:flag flag-
(add-unconditional-prop
(tc els (unbox flag-)) fs-)))
(with-lexical-env/extend-props (list fs-)
#:unreachable (warn-unreachable els)
(test-position-add-false tst)
(tc-expr/check els expected*)))
;; record reachability
(when (unbox flag+)
(test-position-add-true tst))
(when (unbox flag-)
(test-position-add-false tst))
(merge-tc-results (list results-t results-u))]))

View File

@ -55,8 +55,8 @@
[(cons (AndFilter: ps*) ps) (loop (append ps* ps))]
[(cons p ps) (cons p (loop ps))])))
(define/cond-contract (combine-props new-props old-props flag)
((listof Filter/c) (listof Filter/c) (box/c boolean?)
(define/cond-contract (combine-props new-props old-props exit)
((listof Filter/c) (listof Filter/c) (-> #f none/c)
. -> .
(values (listof (or/c ImpFilter? OrFilter?)) (listof (or/c TypeFilter? NotTypeFilter?))))
(define (atomic-prop? p) (or (TypeFilter? p) (NotTypeFilter? p)))
@ -93,7 +93,7 @@
[(AndFilter: ps) (loop derived-formulas derived-atoms (append ps (cdr worklist)))]
[(Top:) (loop derived-formulas derived-atoms (cdr worklist))]
[(Bot:) (set-box! flag #f) (values derived-formulas derived-atoms)])))))
[(Bot:) (exit #f)])))))
(define (unconditional-prop res)

View File

@ -15,10 +15,12 @@
[(_ new:expr existing:expr expected:expr box-v:expr)
(quasisyntax/loc stx
(test-case (~a '(new + existing = expected))
(define b (box #t))
(define-values (res-formulas res-props) (combine-props new existing b))
#,(syntax/loc stx (check-equal? (append res-formulas res-props) expected))
#,(syntax/loc stx (check-equal? (unbox b) box-v))))]))
(define success
(let/ec exit
(define-values (res-formulas res-props) (combine-props new existing exit))
#,(syntax/loc stx (check-equal? (append res-formulas res-props) expected))
#t))
#,(syntax/loc stx (check-equal? success box-v))))]))
(define tests