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

Correctly add scopes to incoming objects in replace-names.

Browse Source 
original commit: 1ec00bb6029a251ae0415620a5d38e43289da162
This commit is contained in:
Eric Dobson 2014-05-29 23:16:03 -07:00
parent 2b0df2f960
commit 448ada8c62
2 changed files with 22 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -83,11 +83,7 @@
#:Object (lambda (f) (subst-object f k o polarity)))
t
[#:arr dom rng rest drest kws
(let* ([st* (if (pair? k)
;; Add a scope if we are substituting an index and
;; not a free variable by name
(λ (t) (subst-type t (add-scope k) o polarity))
st)])
(let* ([st* (λ (t) (subst-type t (add-scope k) (add-scope/object o) polarity))])
(make-arr (map st dom)
(st* rng)
(and rest (st rest))
@ -95,9 +91,18 @@
(map st kws)))]))
;; add-scope : name-ref/c -> name-ref/c
;; Add a scope from an index object
;; Add a scope to an index name-ref
(define (add-scope key)
(list (+ (car key) 1) (cadr key)))
(match key
[(list fun arg) (list (add1 fun) arg)]
[(? identifier?) key]))
;; add-scope/object : Object? -> Object?
;; Add a scope to an index object
(define (add-scope/object obj)
(match obj
[(Empty:) -empty-obj]
[(Path: p nm) (make-Path p (add-scope nm))]))
;; Substitution of objects into objects
;; This is o [o'/x] from the paper

10
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/metafunction-tests.rkt
View File

@ -144,6 +144,16 @@
(list (make-Path null #'x)) (list Univ))
(ret null null null (-> Univ -Boolean : (-FS (-filter -String #'x) -top)) 'b))
)
(test-suite "replace-names"
(check-equal?
(replace-names (list (list #'x (make-Path null (list 0 0))))
(ret Univ -top-filter (make-Path null #'x)))
(ret Univ -top-filter (make-Path null (list 0 0))))
(check-equal?
(replace-names (list (list #'x (make-Path null (list 0 0))))
(ret (-> Univ Univ : -top-filter : (make-Path null #'x))))
(ret (-> Univ Univ : -top-filter : (make-Path null (list 1 0)))))
)
))