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

Make a subst-tc-results.

Browse Source 
original commit: bdbdac3b67fa424bd3c57ec9f344c1fddf22ba56
This commit is contained in:
Eric Dobson 2014-05-22 00:38:45 -07:00
parent 209fc58db0
commit 185697e6ee
2 changed files with 18 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -244,15 +244,5 @@
;; For each name replaces all uses of it in res with the corresponding object.
;; This is used so that names do not escape the scope of their definitions
(define (replace-names names+objects res)
(define (sub proc i)
(for/fold ([s i]) ([name/object (in-list names+objects)])
(proc s (first name/object) (second name/object) #t)))
(define (subber proc lst)
(for/list ([i (in-list lst)])
(sub proc i)))
(match res
[(tc-any-results: f) (tc-any-results (sub subst-filter f))]
[(tc-results: ts fs os)
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os))]
[(tc-results: ts fs os dt db)
(ret (subber subst-type ts) (subber subst-filter-set fs) (subber subst-object os) dt db)]))
(for/fold ([res res]) ([name/object (in-list names+objects)])
(subst-tc-results res (first name/object) (second name/object) #t)))

20
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt
View File

@ -6,10 +6,7 @@
(require "../utils/utils.rkt"
racket/match
(contract-req)
(rename-in (types abbrev utils filter-ops)
[-> -->]
[->* -->*]
[one-of/c -one-of/c])
(except-in (types abbrev utils filter-ops) -> ->* one-of/c)
(rep type-rep object-rep filter-rep rep-utils))
(provide (all-defined-out))
@ -28,6 +25,21 @@
(subst-filter-set fs key o #t arg-ty)
(subst-object old-obj key o #t))))
;; Substitution of objects into a tc-results
(define/cond-contract (subst-tc-results res k o polarity)
(-> full-tc-results/c name-ref/c Object? boolean? full-tc-results/c)
(define (st t) (subst-type t k o polarity))
(define (sf f) (subst-filter f k o polarity))
(define (sfs fs) (subst-filter-set fs k o polarity))
(define (so ob) (subst-object ob k o polarity))
(match res
[(tc-any-results: f) (tc-any-results (sf f))]
[(tc-results: ts fs os)
(ret (map st ts) (map sfs fs) (map so os))]
[(tc-results: ts fs os dt db)
(ret (map st ts) (map sfs fs) (map so os) dt db)]))
;; Substitution of objects into a filter set
;; This is essentially ψ+|ψ- [o/x] from the paper
(define/cond-contract (subst-filter-set fs k o polarity [t #f])