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

Substitution for (List T ...)

Browse Source
This commit is contained in:
Sam Tobin-Hochstadt 2010-05-27 14:39:54 -04:00
parent 62fb6f9311
commit 310bdf3529
1 changed files with 23 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

27
collects/typed-scheme/types/utils.rkt
View File

@ -36,7 +36,8 @@
;; substitute : Type Name Type -> Type ;; substitute : Type Name Type -> Type
(define (substitute image name target #:Un [Un (get-union-maker)]) (d/c (substitute image name target #:Un [Un (get-union-maker)])
((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
(define (sb t) (substitute image name t)) (define (sb t) (substitute image name t))
(if (hash-ref (free-vars* target) name #f) (if (hash-ref (free-vars* target) name #f)
(type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb)) (type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
@ -58,14 +59,29 @@
(begin (begin
(when (eq? name dbound) (when (eq? name dbound)
(int-err "substitute used on ... variable ~a in type ~a" name target)) (int-err "substitute used on ... variable ~a in type ~a" name target))
(make-ValuesDots (map sb types) (sb dty) dbound))]) (make-ValuesDots (map sb types) (sb dty) dbound))]
[#:ListDots dty dbound
(begin
(when (eq? name dbound)
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-ListDots (sb dty) dbound))])
target)) target))
;; implements angle bracket substitution from the formalism
;; substitute-dots : Listof[Type] Option[type] Name Type -> Type ;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
(define (substitute-dots images rimage name target) (d/c (substitute-dots images rimage name target)
((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?)
(define (sb t) (substitute-dots images rimage name t)) (define (sb t) (substitute-dots images rimage name t))
(if (hash-ref (free-vars* target) name #f) (if (hash-ref (free-vars* target) name #f)
(type-case (#:Type sb #:Filter (sub-f sb)) target (type-case (#:Type sb #:Filter (sub-f sb)) target
[#:ListDots dty dbound
(if (eq? name dbound)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb dty)])
(for/fold ([t (make-Value null)])
([img images])
(make-Pair (substitute img name expanded) t)))
(make-ListDots (sb dty) dbound))]
[#:ValuesDots types dty dbound [#:ValuesDots types dty dbound
(if (eq? name dbound) (if (eq? name dbound)
(make-Values (make-Values
@ -98,7 +114,7 @@
(map sb kws)))]) (map sb kws)))])
target)) target))
;; implements sd from the formalism ;; implements curly brace substitution from the formalism
;; substitute-dotted : Type Name Name Type -> Type ;; substitute-dotted : Type Name Name Type -> Type
(define (substitute-dotted image image-bound name target) (define (substitute-dotted image image-bound name target)
(define (sb t) (substitute-dotted image image-bound name t)) (define (sb t) (substitute-dotted image image-bound name t))
@ -109,6 +125,9 @@
(make-ValuesDots (map sb types) (make-ValuesDots (map sb types)
(sb dty) (sb dty)
(if (eq? name dbound) image-bound dbound))] (if (eq? name dbound) image-bound dbound))]
[#:ListDots dty dbound
(make-ListDots (sb dty)
(if (eq? name dbound) image-bound dbound))]
[#:F name* [#:F name*
(if (eq? name* name) (if (eq? name* name)
image image