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

Substituion now works

Browse Source
This commit is contained in:
Sam Tobin-Hochstadt 2008-06-10 12:21:59 -04:00
parent 017f756c77
commit a7f81d931d
6 changed files with 54 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
collects/typed-scheme/private/free-variance.ss
View File

@ -63,7 +63,8 @@
(define (fix-bound vs bound)
(define vs* (hash-map* (lambda (k v) v) vs))
(hash-remove! vs* bound)
(hash-set! vs* bound (cons bound Dotted)))
(hash-set! vs* bound (cons bound Dotted))
vs*)
;; frees -> frees
(define (flip-variances vs)

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))

9
collects/typed-scheme/private/type-rep.ss
View File

@ -103,8 +103,8 @@
(match drest
[(cons t (? symbol? bnd))
(let ([vs (free-vars* t)])
(flip-variances (fix-bound vs bnd)))]
[(cons t bnd) (flip-variances (free-vars* t))]
(list (flip-variances (fix-bound vs bnd))))]
[(cons t bnd) (list (flip-variances (free-vars* t)))]
[_ null])
(list (free-vars* rng))
(map make-invariant
@ -113,8 +113,8 @@
(match drest
[(cons t (? number? bnd))
(let ([vs (free-idxs* t)])
(flip-variances (fix-bound vs bnd)))]
[(cons t bnd) (flip-variances (free-idxs* t))]
(list (flip-variances (fix-bound vs bnd))))]
[(cons t bnd) (list (flip-variances (free-idxs* t)))]
[_ null])
(list (free-idxs* rng))
(map make-invariant
@ -520,6 +520,7 @@
free-vars*
type-equal? type-compare type<?
remove-dups
sub-eff
(rename-out [Mu:* Mu:]
[Poly:* Poly:]
[PolyDots:* PolyDots:]

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

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

@ -99,7 +99,7 @@
[(_ val)
#'(? (lambda (x) (equal? val x)))])))
(define-for-syntax printing? #t)
(define-for-syntax printing? #f)
(define print-type* (box (lambda _ (error "print-type* not yet defined"))))
(define print-effect* (box (lambda _ (error "print-effect* not yet defined"))))