Make the filter actually be opened up in the AnyValues case.

original commit: 385729260faa861086a46bc54d765baa47b7cd3f
This commit is contained in:
Eric Dobson 2014-05-29 00:43:55 -07:00
parent c709f11b9b
commit f1bf4a07fd
2 changed files with 17 additions and 1 deletions

View File

@ -18,7 +18,7 @@
(define (open-Values v os ts)
(match v
[(AnyValues: f)
(tc-any-results f)]
(tc-any-results (open-Filter f os ts))]
[(Values: results)
(define-values (t-r f-r o-r)
(for/lists (t-r f-r o-r)
@ -33,6 +33,15 @@
(ret t-r f-r o-r dty dbound)]))
(define/cond-contract (open-Filter f objs ts)
(-> (Filter/c (listof Object?) (listof Type/c) Filter/c))
(for/fold ([f f])
([(o arg) (in-indexed (in-list objs))]
[arg-ty (in-list ts)])
(define key (list 0 arg))
(subst-filter f key o #t)))
;; Substitutes the given objects into the type, filters, and object
;; of a Result for function application. This matches up to the substitutions
;; in the T-App rule from the ICFP paper.

View File

@ -132,5 +132,12 @@
(list (make-Path null #'x)) (list Univ))
(ret (-opt (-> Univ -Boolean : (-FS (-filter -Symbol #'x) -top)))))
;; Substitute into filter of any values
(check-equal?
(open-Values (make-AnyValues (-filter -String '(0 0)))
(list (make-Path null #'x)) (list Univ))
(tc-any-results (-filter -String #'x)))
)
))