Correctly add scopes to incoming objects in replace-names.
This commit is contained in:
parent
2ba070c6b3
commit
1ec00bb602
|
@ -83,11 +83,7 @@
|
||||||
#:Object (lambda (f) (subst-object f k o polarity)))
|
#:Object (lambda (f) (subst-object f k o polarity)))
|
||||||
t
|
t
|
||||||
[#:arr dom rng rest drest kws
|
[#:arr dom rng rest drest kws
|
||||||
(let* ([st* (if (pair? k)
|
(let* ([st* (λ (t) (subst-type t (add-scope k) (add-scope/object o) polarity))])
|
||||||
;; 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)])
|
|
||||||
(make-arr (map st dom)
|
(make-arr (map st dom)
|
||||||
(st* rng)
|
(st* rng)
|
||||||
(and rest (st rest))
|
(and rest (st rest))
|
||||||
|
@ -95,9 +91,18 @@
|
||||||
(map st kws)))]))
|
(map st kws)))]))
|
||||||
|
|
||||||
;; add-scope : name-ref/c -> name-ref/c
|
;; 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)
|
(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
|
;; Substitution of objects into objects
|
||||||
;; This is o [o'/x] from the paper
|
;; This is o [o'/x] from the paper
|
||||||
|
|
|
@ -144,6 +144,16 @@
|
||||||
(list (make-Path null #'x)) (list Univ))
|
(list (make-Path null #'x)) (list Univ))
|
||||||
(ret null null null (-> Univ -Boolean : (-FS (-filter -String #'x) -top)) 'b))
|
(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)))))
|
||||||
)
|
)
|
||||||
))
|
))
|
||||||
|
|
Loading…
Reference in New Issue
Block a user