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

Fix TR regression and use abstraction recipe

Browse Source 
A function like (lambda (x) (lambda (y) y)) would cause TR
to fail in an internal metafunction. The fault was triggered
when the object y is abstracted to (0 0) and then the outer
lambda tries to abstract (0 0) and fails.

The problem was triggered by the new path index changes in
v6.0 because TR did not previously try to abstract objects
that occurs in the target type (now necessary for scope
lifting of path indices), which may contain non-identifier
objects.

This error didn't occur in another nearly identical (except
for one crucial identifier? check) code path, so this commit
also eliminates the duplication by abstracting.

original commit: bf47523ac92f2d3b32e6c97aa83d9d256b449a6f
This commit is contained in:
Asumu Takikawa 2014-02-14 23:24:46 -05:00
parent fae843b628
commit 08e8a6eeb1
2 changed files with 35 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -118,11 +118,7 @@
;; the given object
(define/cond-contract (abstract-object ids keys o)
(-> (listof identifier?) (listof name-ref/c) Object? Object?)
(define (lookup y)
(for/first ([x (in-list ids)] [i (in-list keys)] #:when (free-identifier=? x y)) i))
(define-match-expander lookup:
(syntax-rules ()
[(_ i) (app lookup (? values i))]))
(define-lookup: lookup: ids keys)
(match o
[(Path: p (lookup: idx)) (make-Path p idx)]
[_ -no-obj]))
@ -138,15 +134,9 @@
(define/cond-contract (abo xs idxs f)
((listof identifier?) (listof name-ref/c) Filter/c . -> . Filter/c)
(define/cond-contract (lookup y)
(identifier? . -> . (or/c #f (list/c integer? integer?)))
(for/first ([x (in-list xs)] [i (in-list idxs)] #:when (free-identifier=? x y)) i))
(define-match-expander lookup:
(syntax-rules ()
[(_ i) (or (? identifier? (app lookup (? values i)))
i)]))
(define (rec f) (abo xs idxs f))
(define (sb-t t) t)
(define-lookup: lookup: xs idxs)
(filter-case (#:Type sb-t #:Filter rec) f
[#:TypeFilter
t p (lookup: idx)
@ -155,6 +145,27 @@
t p (lookup: idx)
(-not-filter t idx p)]))
;; Look up the identifier in a mapping of a list of identifiers
;; to a list of path indices
(define/cond-contract (lookup-index target ids keys)
(-> identifier? (listof identifier?) (listof (list/c integer? integer?))
(or/c #f (list/c integer? integer?)))
(for/first ([id (in-list ids)] [index (in-list keys)]
#:when (free-identifier=? id target))
index))
;; Generates a match expander to make `lookup-index` convenient
(define-syntax-rule (define-lookup: lookup: ids keys)
(define-match-expander lookup:
(syntax-rules ()
[(_ i)
(or ;; No need to look up if it's not an identifier,
;; since that means it was already abstracted
;; into an index.
(? identifier? (app (λ (id) (lookup-index id ids keys))
(? values i)))
i)])))
(define (merge-filter-sets fs)
(match fs
[(list (FilterSet: f+ f-) ...)

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

@ -857,7 +857,8 @@
(-polydots (z x y) (t:-> (cl->*
((t:-> x z) (-pair x (-lst x)) . t:-> . (-pair z (-lst z)))
((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z)))
: (-FS (-not-filter (-val #f) #'map) (-filter (-val #f) #'map))))]
: (-FS (-not-filter (-val #f) #'map) (-filter (-val #f) #'map))
: (make-Path null #'map)))]
;; error tests
[tc-err (+ 3 #f)]
@ -1779,6 +1780,16 @@
;; type doesn't really matter, just make sure it typechecks
-Void]
;; Tests the absence of a regression with curried functions
;; (should not trigger an error with free-identifier=?)
[tc-e (lambda (x) (lambda (y) y))
#:ret
(ret (t:-> Univ (t:-> Univ Univ : (-FS (-not-filter (-val #f) (list 0 0))
(-filter (-val #f) (list 0 0)))
: (make-Path null (list 0 0)))
: (-FS -top -bot))
(-FS -top -bot))]
;; The following ensures that the correct filter can be
;; written by the user
[tc-e