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

* Fixed variable promotion/demotion for dotted rest args

Browse Source 
* Fixed constraint generation for starred functions with
   different fixed arg lengths
This commit is contained in:
Sam Tobin-Hochstadt 2008-06-11 11:45:25 -04:00
parent 975f26b93d
commit dce8566c89
1 changed files with 62 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

97
collects/typed-scheme/private/infer.ss
View File

@ -37,16 +37,27 @@
[#:Param in out [#:Param in out
(make-Param (var-demote in V) (make-Param (var-demote in V)
(vp out))] (vp out))]
[#:arr dom rng rest #f thn els [#:arr dom rng rest drest thn els
(if (cond
(apply V-in? V (append thn els)) [(apply V-in? V (append thn els))
(make-top-arr) (make-arr null (Un) Univ #f null null)]
(make-arr (for/list ([d dom]) (var-demote d V)) [(and drest (V-in? V (cdr drest)))
(vp rng) (make-arr (for/list ([d dom]) (var-demote d V))
(and rest (var-demote rest V)) (vp rng)
#f (var-demote (car drest) V)
thn #f
els))])) thn
els)]
[else
(make-arr (for/list ([d dom]) (var-demote d V))
(vp rng)
(and rest (var-demote rest V))
(and drest
(cons (var-demote (car drest)
(cons (cdr drest) V))
(cdr drest)))
thn
els)])]))
(define (var-demote T V) (define (var-demote T V)
(define (vd t) (var-demote t V)) (define (vd t) (var-demote t V))
@ -62,15 +73,27 @@
[#:Param in out [#:Param in out
(make-Param (var-promote in V) (make-Param (var-promote in V)
(vd out))] (vd out))]
[#:arr dom rng rest #f thn els [#:arr dom rng rest drest thn els
(if (apply V-in? V (append thn els)) (cond
(make-arr null (Un) Univ null null) [(apply V-in? V (append thn els))
(make-arr (for/list ([d dom]) (var-promote d V)) (make-arr null (Un) Univ #f null null)]
(vd rng) [(and drest (V-in? V (cdr drest)))
(and rest (var-promote rest V)) (make-arr (for/list ([d dom]) (var-promote d V))
#f (vd rng)
thn (var-promote (car drest) V)
els))])) #f
thn
els)]
[else
(make-arr (for/list ([d dom]) (var-promote d V))
(vd rng)
(and rest (var-promote rest V))
(and drest
(cons (var-promote (car drest)
(cons (cdr drest) V))
(cdr drest)))
thn
els)])]))
;; a stupid impl ;; a stupid impl
(define (meet S T) (define (meet S T)
(let ([s* (restrict S T)]) (let ([s* (restrict S T)])
@ -272,22 +295,26 @@
(cset-combine (cset-combine
(filter (filter
values ;; only generate the successful csets values ;; only generate the successful csets
(for*/list ([t-arr t-arr] [s-arr s-arr]) (for*/list
(with-handlers ([exn:infer? (lambda (_) #f)]) ([t-arr t-arr] [s-arr s-arr])
(match* (t-arr s-arr) (with-handlers ([exn:infer? (lambda (_) #f)])
[((arr: ts t t-rest #f t-thn-eff t-els-eff) (arr: ss s s-rest #f s-thn-eff s-els-eff)) (match* (t-arr s-arr)
(let ([arg-mapping [((arr: ts t t-rest #f t-thn-eff t-els-eff)
(cond [(and t-rest s-rest (= (length ts) (length ss))) (arr: ss s s-rest #f s-thn-eff s-els-eff))
(cgen/list X V (cons s-rest ss) (cons t-rest ts))] (let ([arg-mapping
[(and (not t-rest) (not s-rest) (= (length ts) (length ss))) (cond [(and t-rest s-rest (<= (length ts) (length ss)))
(cgen/list X V ss ts)] (cgen/list X V (cons s-rest ss) (cons t-rest (extend ss ts t-rest)))]
[(and t-rest (not s-rest) (<= (length ts) (length ss))) [(and t-rest s-rest (>= (length ts) (length ss)))
(cgen/list X V ss (extend ss ts t-rest))] (cgen/list X V (cons s-rest (extend ts ss s-rest)) (cons t-rest ts))]
[(and s-rest (not t-rest) (>= (length ts) (length ss))) [(and (not t-rest) (not s-rest) (= (length ts) (length ss)))
(cgen/list X V (extend ts ss s-rest) ts)] (cgen/list X V ss ts)]
[else (fail! S T)])] [(and t-rest (not s-rest) (<= (length ts) (length ss)))
[ret-mapping (cgen V X t s)]) (cgen/list X V ss (extend ss ts t-rest))]
(cset-meet arg-mapping ret-mapping))])))))] [(and s-rest (not t-rest) (>= (length ts) (length ss)))
(cgen/list X V (extend ts ss s-rest) ts)]
[else (fail! S T)])]
[ret-mapping (cgen V X t s)])
(cset-meet arg-mapping ret-mapping))])))))]
[(_ _) [(_ _)
(cond [(subtype S T) empty] (cond [(subtype S T) empty]
;; or, nothing worked, and we fail ;; or, nothing worked, and we fail