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

Add flag for testing unreachability in env+.

Browse Source 
Use flag in if-unit.

svn: r14870
This commit is contained in:
Sam Tobin-Hochstadt 2009-05-19 15:24:55 +00:00
parent 0cd135c3bb
commit eedafc034b
2 changed files with 38 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
collects/typed-scheme/typecheck/tc-envops.ss
View File

@ -52,10 +52,15 @@
[(t* lo)
(int-err "update along ill-typed path: ~a ~a ~a" t t* lo)]))
(define/contract (env+ env fs)
(env? (listof Filter/c) . -> . env?)
;; sets the flag box to #f if anything becomes (U)
(d/c (env+ env fs flag)
(env? (listof Filter/c) (box/c #t). -> . env?)
(for/fold ([Γ env]) ([f fs])
(match f
[(Bot:) (env-map (lambda (x) (cons (car x) (Un))) Γ)]
[(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)]
[(or (TypeFilter: _ _ x) (NotTypeFilter: _ _ x))
(update-type/lexical (lambda (x t) (update t f)) x Γ)])))
(update-type/lexical (lambda (x t) (let ([new-t (update t f)])
(when (type-equal? new-t (Un))
(set-box! flag #f))
new-t))
x Γ)])))

43
collects/typed-scheme/typecheck/tc-new-if.ss
View File

@ -1,12 +1,12 @@
#lang scheme/unit
(require (rename-in "../utils/utils.ss" [infer r:infer]))
(require (rename-in "../utils/utils.ss" [infer r:infer] [extend r:extend]))
(require "signatures.ss"
(rep type-rep filter-rep object-rep)
(rename-in (types convenience subtype union utils comparison remove-intersect)
[remove *remove])
(env lexical-env)
(env lexical-env type-environments)
(r:infer infer)
(utils tc-utils mutated-vars)
(typecheck tc-envops tc-metafunctions)
@ -19,20 +19,35 @@
(export tc-if^)
(define (tc/if-twoarm tst thn els [expected #f])
(define (tc e) (if expected (tc-expr/check e expected) (tc-expr e)))
(define (tc expr reachable?)
(unless reachable? (warn-unreachable expr))
(cond
;; if reachable? is #f, then we don't want to verify that this branch has the appropriate type
;; in particular, it might be (void)
[(and expected reachable?)
(tc-expr/check expr expected)]
;; this code is reachable, but we have no expected type
[reachable? (tc-expr expr)]
;; otherwise, this code is unreachable
;; and the resulting type should be the empty type
[(check-unreachable-code?)
(tc-expr/check expr Univ)
(ret (Un))]
[else (ret (Un))]))
(match (single-value tst)
[(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _)
(match-let ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+) (tc thn))]
[(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs-) (tc els))])
;; if we have the same number of values in both cases
(cond [(= (length ts) (length us))
(combine-results
(for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3])
(combine-filter f1 f2 f3 t u o2 o3)))]
[else
(tc-error/expr #:return (ret Err)
"Expected the same number of values from both branches of if expression, but got ~a and ~a"
(length ts) (length us))]))]
(let-values ([(flag+ flag-) (values (box #t) (box #t))])
(match-let ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+ flag+) (tc thn (unbox flag+)))]
[(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs- flag-) (tc els (unbox flag-)))])
;; if we have the same number of values in both cases
(cond [(= (length ts) (length us))
(combine-results
(for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3])
(combine-filter f1 f2 f3 t u o2 o3)))]
[else
(tc-error/expr #:return (ret Err)
"Expected the same number of values from both branches of if expression, but got ~a and ~a"
(length ts) (length us))])))]
[(tc-results: t _ _)
(tc-error/expr #:return (ret (or expected Err))
"Test expression expects one value, given ~a" t)]))