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

Make tc-if not manage raw prop-envs.

Browse Source 
original commit: daf087c8013bcba465fe0f0662529edda7fef1cf
This commit is contained in:
Eric Dobson 2014-05-24 09:16:38 -07:00
parent eabe5a6a33
commit 22f507dc18
2 changed files with 65 additions and 61 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -3,6 +3,7 @@
(require (rename-in "../utils/utils.rkt" [infer infer-in]))
(require racket/match
(only-in unstable/list list-update)
(for-syntax racket/base syntax/parse)
(contract-req)
(infer-in infer)
(rep type-rep filter-rep object-rep rep-utils)
@ -78,5 +79,10 @@
[_ Γ])))
;; run code in an extended env and with replaced props
(define-syntax-rule (with-lexical-env/extend-props ps . b)
(with-lexical-env (env+ (lexical-env) ps (box #t)) . b))
(define-syntax (with-lexical-env/extend-props stx)
(define-splicing-syntax-class flag
[pattern (~seq #:flag v:expr)]
[pattern (~seq) #:with v #'(box #t)])
(syntax-parse stx
[(_ ps flag:flag . b)
#'(with-lexical-env (env+ (lexical-env) ps flag.v) . b)]))

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

@ -31,63 +31,61 @@
[else (ret (Un))]))
(match (single-value tst)
[(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _)
(let*-values ([(flag+ flag-) (values (box #t) (box #t))])
(match-let* ([env-thn (env+ (lexical-env) (list fs+) flag+)]
[env-els (env+ (lexical-env) (list fs-) flag-)])
(define results-t
(with-lexical-env env-thn
(add-unconditional-prop (tc thn (unbox flag+)) (apply -and (env-props env-thn)))))
(define results-u
(with-lexical-env env-els
(add-unconditional-prop (tc els (unbox flag-)) (apply -and (env-props env-els)))))
(define flag+ (box #t))
(define flag- (box #t))
(define results-t
(with-lexical-env/extend-props (list fs+) #:flag flag+
(add-unconditional-prop (tc thn (unbox flag+)) (apply -and (env-props (lexical-env))))))
(define results-u
(with-lexical-env/extend-props (list fs-) #:flag flag-
(add-unconditional-prop (tc els (unbox flag-)) (apply -and (env-props (lexical-env))))))
;; record reachability
;; since we may typecheck a given piece of code multiple times in different
;; contexts, we need to take previous results into account
(cond [(and (not (unbox flag+)) ; maybe contradiction
;; to be an actual contradiction, we must have either previously
;; recorded this test as a contradiction, or have never seen it
;; before
(not (tautology? tst))
(not (neither? tst)))
(add-contradiction tst)]
[(and (not (unbox flag-)) ; maybe tautology
;; mirror case
(not (contradiction? tst))
(not (neither? tst)))
(add-tautology tst)]
[else
(add-neither tst)])
(match* (results-t results-u)
[((tc-any-results: f1) (tc-any-results: f2))
(tc-any-results (-or (-and fs+ f1) (-and fs- f2)))]
;; Not do awful things here
[((tc-results: ts (list (FilterSet: f+ f-) ...) os) (tc-any-results: f2))
(tc-any-results (-or (apply -and (map -or f+ f-)) f2))]
[((tc-any-results: f2) (tc-results: ts (list (FilterSet: f+ f-) ...) os))
(tc-any-results (-or (apply -and (map -or f+ f-)) f2))]
[((tc-results: ts fs2 os2)
(tc-results: us fs3 os3))
;; if we have the same number of values in both cases
(cond [(= (length ts) (length us))
(combine-results
(for/list ([f2 (in-list fs2)] [f3 (in-list fs3)]
[t2 (in-list ts)] [t3 (in-list us)]
[o2 (in-list os2)] [o3 (in-list os3)])
(let ([filter
(match* (f2 f3)
[((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
(-FS (-or f2+ f3+) (-or f2- f3-))])]
[type (Un t2 t3)]
[object (if (object-equal? o2 o3) o2 -empty-obj)])
(ret type filter object))))]
;; special case if one of the branches is unreachable
[(and (= 1 (length us)) (type-equal? (car us) (Un)))
(ret ts fs2 os2)]
[(and (= 1 (length ts)) (type-equal? (car ts) (Un)))
(ret us fs3 os3)]
;; otherwise, error
[else
(tc-error/expr "Expected the same number of values from both branches of `if' expression, but got ~a and ~a"
(length ts) (length us))])])))]))
;; record reachability
;; since we may typecheck a given piece of code multiple times in different
;; contexts, we need to take previous results into account
(cond [(and (not (unbox flag+)) ; maybe contradiction
;; to be an actual contradiction, we must have either previously
;; recorded this test as a contradiction, or have never seen it
;; before
(not (tautology? tst))
(not (neither? tst)))
(add-contradiction tst)]
[(and (not (unbox flag-)) ; maybe tautology
;; mirror case
(not (contradiction? tst))
(not (neither? tst)))
(add-tautology tst)]
[else
(add-neither tst)])
(match* (results-t results-u)
[((tc-any-results: f1) (tc-any-results: f2))
(tc-any-results (-or (-and fs+ f1) (-and fs- f2)))]
;; Not do awful things here
[((tc-results: ts (list (FilterSet: f+ f-) ...) os) (tc-any-results: f2))
(tc-any-results (-or (apply -and (map -or f+ f-)) f2))]
[((tc-any-results: f2) (tc-results: ts (list (FilterSet: f+ f-) ...) os))
(tc-any-results (-or (apply -and (map -or f+ f-)) f2))]
[((tc-results: ts fs2 os2)
(tc-results: us fs3 os3))
;; if we have the same number of values in both cases
(cond [(= (length ts) (length us))
(combine-results
(for/list ([f2 (in-list fs2)] [f3 (in-list fs3)]
[t2 (in-list ts)] [t3 (in-list us)]
[o2 (in-list os2)] [o3 (in-list os3)])
(let ([filter
(match* (f2 f3)
[((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
(-FS (-or f2+ f3+) (-or f2- f3-))])]
[type (Un t2 t3)]
[object (if (object-equal? o2 o3) o2 -empty-obj)])
(ret type filter object))))]
;; special case if one of the branches is unreachable
[(and (= 1 (length us)) (type-equal? (car us) (Un)))
(ret ts fs2 os2)]
[(and (= 1 (length ts)) (type-equal? (car ts) (Un)))
(ret us fs3 os3)]
;; otherwise, error
[else
(tc-error/expr "Expected the same number of values from both branches of `if' expression, but got ~a and ~a"
(length ts) (length us))])])]))