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

Substituion now works

Browse Source 
original commit: a7f81d931d9bef247b9215cb1e6fdd3e616dd6a2
This commit is contained in:
Sam Tobin-Hochstadt 2008-06-10 12:21:59 -04:00
parent 583b640833
commit a93289aedd
3 changed files with 46 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/typed-scheme/private/subtype.ss
View File

@ -1,6 +1,6 @@
#lang scheme/base
(require "type-rep.ss" "unify.ss" "type-utils.ss"
(require (except-in "type-rep.ss" sub-eff) "unify.ss" "type-utils.ss"
"tc-utils.ss"
"effect-rep.ss"
"type-comparison.ss"

6
collects/typed-scheme/private/type-effect-convenience.ss
View File

@ -69,7 +69,11 @@
(define make-arr*
(case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))]
[(dom rng rest) (make-arr dom rng rest #f (list) (list))]
[(dom rng rest eff1 eff2) (make-arr dom rng rest #f eff1 eff2)]))
[(dom rng rest eff1 eff2) (make-arr dom rng rest #f eff1 eff2)]
[(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest eff1 eff2)]))
(define (make-arr-dots dom rng dty dbound)
(make-arr* dom rng #f (cons dty dbound) null null))
(define (make-promise-ty t)
(make-Struct (string->uninterned-symbol "Promise") #f (list t) #f #f #'promise? values))

41
collects/typed-scheme/private/type-utils.ss
View File

@ -10,6 +10,7 @@
(provide fv fv/list
substitute
substitute-dots
subst-all
subst
ret
@ -26,7 +27,45 @@
(define (sb t) (substitute image name t))
(if (hash-ref (free-vars* target) name #f)
(type-case sb target
[#:F name* (if (eq? name* name) image target)])
[#:F name* (if (eq? name* name) image target)]
[#:arr dom rng rest drest thn-eff els-eff
(begin
(when (and (pair? drest)
(eq? name (cdr drest)))
(int-err "substitute used on ... variable ~a" name))
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff)))])
target))
;; substitute-dots : Listof[Type] Name Type -> Type
(define (substitute-dots images name target)
(define (sb t) (substitute-dots images name t))
(if (hash-ref (free-vars* target) name #f)
(type-case sb target
[#:F name* (if (eq? name* name)
(int-err "substitute-dots: got single variable ~a" name*)
target)]
[#:arr dom rng rest drest thn-eff els-eff
(if (and (pair? drest)
(eq? name (cdr drest)))
(make-arr (append
(map sb dom)
(map (lambda (img) (substitute img name (car drest))) images))
(sb rng)
#f
#f
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff))
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(map (lambda (e) (sub-eff sb e)) thn-eff)
(map (lambda (e) (sub-eff sb e)) els-eff)))])
target))
;; substitute many variables