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

polymorphic lambdas are true values.

Browse Source 
Use correct pattern.
Return the appropriate types from apply, not the Values struct in the rng.

svn: r14756
This commit is contained in:
Sam Tobin-Hochstadt 2009-05-08 23:11:57 +00:00
parent c2da52d661
commit 1444c07c0a
3 changed files with 26 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

43
collects/typed-scheme/typecheck/tc-app.ss
View File

@ -166,6 +166,8 @@
(ret expected))])) (ret expected))]))
(define (tc/apply f args) (define (tc/apply f args)
(define (do-ret t)
(match t [(Values: (list (Result: ts _ _) ...)) (ret ts)]))
(define f-ty (single-value f)) (define f-ty (single-value f))
;; produces the first n-1 elements of the list, and the last element ;; produces the first n-1 elements of the list, and the last element
(define (split l) (let-values ([(f r) (split-at l (sub1 (length l)))]) (define (split l) (let-values ([(f r) (split-at l (sub1 (length l)))])
@ -195,7 +197,7 @@
(subtype (apply -lst* arg-tys #:tail (make-Listof tail-ty)) (subtype (apply -lst* arg-tys #:tail (make-Listof tail-ty))
(apply -lst* (car doms*) #:tail (make-Listof (car rests*))))))) (apply -lst* (car doms*) #:tail (make-Listof (car rests*)))))))
(printf/log "Non-poly apply, ... arg\n") (printf/log "Non-poly apply, ... arg\n")
(ret (car rngs*))] (do-ret (car rngs*))]
[(and (car rests*) [(and (car rests*)
(let ([tail-ty (with-handlers ([exn:fail? (lambda _ #f)]) (let ([tail-ty (with-handlers ([exn:fail? (lambda _ #f)])
(tc-expr/t tail))]) (tc-expr/t tail))])
@ -206,7 +208,7 @@
(printf/log (if (memq (syntax->datum f) '(+ - * / max min)) (printf/log (if (memq (syntax->datum f) '(+ - * / max min))
"Simple arithmetic non-poly apply\n" "Simple arithmetic non-poly apply\n"
"Simple non-poly apply\n")) "Simple non-poly apply\n"))
(ret (car rngs*))] (do-ret (car rngs*))]
[(and (car drests*) [(and (car drests*)
(let-values ([(tail-ty tail-bound) (let-values ([(tail-ty tail-bound)
(with-handlers ([exn:fail? (lambda _ (values #f #f))]) (with-handlers ([exn:fail? (lambda _ (values #f #f))])
@ -216,9 +218,9 @@
(subtypes arg-tys (car doms*)) (subtypes arg-tys (car doms*))
(subtype tail-ty (car (car drests*)))))) (subtype tail-ty (car (car drests*))))))
(printf/log "Non-poly apply, ... arg\n") (printf/log "Non-poly apply, ... arg\n")
(ret (car rngs*))] (do-ret (car rngs*))]
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests drests '()) ..1)))) [(tc-result1: (Poly: vars (Function: (list (arr: doms rngs rests drests '()) ..1))))
(let*-values ([(arg-tys) (map tc-expr/t fixed-args)] (let*-values ([(arg-tys) (map tc-expr/t fixed-args)]
[(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))]) [(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))])
(tc/dots tail))]) (tc/dots tail))])
@ -242,7 +244,7 @@
(car rests*) (car rests*)
(car rngs*) (car rngs*)
(fv (car rngs*)))) (fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; actual work, when we have a * function and ... final arg ;; actual work, when we have a * function and ... final arg
[(and (car rests*) [(and (car rests*)
tail-bound tail-bound
@ -255,7 +257,7 @@
(car rests*) (car rests*)
(car rngs*) (car rngs*)
(fv (car rngs*)))) (fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg ;; ... function, ... arg
[(and (car drests*) [(and (car drests*)
tail-bound tail-bound
@ -263,7 +265,7 @@
(= (length (car doms*)) (= (length (car doms*))
(length arg-tys)) (length arg-tys))
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*)))) (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; if nothing matches, around the loop again ;; if nothing matches, around the loop again
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result1: (Poly: vars (Function: '()))) [(tc-result1: (Poly: vars (Function: '())))
@ -294,7 +296,7 @@
(car rests*) (car rests*)
(car rngs*) (car rngs*)
(fv (car rngs*)))) (fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; actual work, when we have a * function and ... final arg ;; actual work, when we have a * function and ... final arg
[(and (car rests*) [(and (car rests*)
tail-bound tail-bound
@ -308,7 +310,7 @@
(car rngs*) (car rngs*)
(fv (car rngs*)))) (fv (car rngs*))))
=> (lambda (substitution) => (lambda (substitution)
(ret (subst-all substitution (car rngs*))))] (do-ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg, same bound on ... ;; ... function, ... arg, same bound on ...
[(and (car drests*) [(and (car drests*)
tail-bound tail-bound
@ -317,7 +319,7 @@
(length arg-tys)) (length arg-tys))
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*)))) (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))
=> (lambda (substitution) => (lambda (substitution)
(ret (subst-all substitution (car rngs*))))] (do-ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg, different bound on ... ;; ... function, ... arg, different bound on ...
[(and (car drests*) [(and (car drests*)
tail-bound tail-bound
@ -331,11 +333,11 @@
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))) (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*)))))
=> (lambda (substitution) => (lambda (substitution)
(define drest-bound (cdr (car drests*))) (define drest-bound (cdr (car drests*)))
(ret (substitute-dotted (cadr (assq drest-bound substitution)) (do-ret (substitute-dotted (cadr (assq drest-bound substitution))
tail-bound tail-bound
drest-bound drest-bound
(subst-all (alist-delete drest-bound substitution eq?) (subst-all (alist-delete drest-bound substitution eq?)
(car rngs*)))))] (car rngs*)))))]
;; ... function, (List A B C etc) arg ;; ... function, (List A B C etc) arg
[(and (car drests*) [(and (car drests*)
(not tail-bound) (not tail-bound)
@ -347,7 +349,7 @@
(car (car drests*)) (car rngs*) (fv (car rngs*)))) (car (car drests*)) (car rngs*) (fv (car rngs*))))
=> (lambda (substitution) => (lambda (substitution)
(define drest-bound (cdr (car drests*))) (define drest-bound (cdr (car drests*)))
(ret (subst-all substitution (car rngs*))))] (do-ret (subst-all substitution (car rngs*))))]
;; if nothing matches, around the loop again ;; if nothing matches, around the loop again
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result1: (PolyDots: vars (Function: '()))) [(tc-result1: (PolyDots: vars (Function: '())))
@ -373,7 +375,7 @@
[(#%plain-app not arg) [(#%plain-app not arg)
(match (single-value #'arg) (match (single-value #'arg)
[(tc-result1: t (FilterSet: f+ f-) _) [(tc-result1: t (FilterSet: f+ f-) _)
(ret t (make-FilterSet f- f+))])] (ret -Boolean (make-FilterSet f- f+))])]
;; (apply values l) gets special handling ;; (apply values l) gets special handling
[(#%plain-app apply values e) [(#%plain-app apply values e)
(cond [(with-handlers ([exn:fail? (lambda _ #f)]) (cond [(with-handlers ([exn:fail? (lambda _ #f)])
@ -382,6 +384,8 @@
[else (tc/apply #'values #'(e))])] [else (tc/apply #'values #'(e))])]
;; rewrite this so that it takes advantages of all the special cases ;; rewrite this so that it takes advantages of all the special cases
[(#%plain-app k:apply . args) (tc/app/internal (syntax/loc form (apply . args)) expected)] [(#%plain-app k:apply . args) (tc/app/internal (syntax/loc form (apply . args)) expected)]
;; handle apply specially
[(#%plain-app apply f . args) (tc/apply #'f #'args)]
;; special case for `values' with single argument - we just ignore the values, except that it forces arg to return one value ;; special case for `values' with single argument - we just ignore the values, except that it forces arg to return one value
[(#%plain-app values arg) (single-value #'arg expected)] [(#%plain-app values arg) (single-value #'arg expected)]
;; handle `values' specially ;; handle `values' specially
@ -400,8 +404,6 @@
(for/list ([arg (syntax->list #'args)]) (for/list ([arg (syntax->list #'args)])
(single-value arg))]) (single-value arg))])
(ret ts fs os))])] (ret ts fs os))])]
;; rewrite this so that it takes advantages of all the special cases
[(#%plain-app k:apply . args) (tc/app/internal (syntax/loc form (apply . args)) expected)]
;; special case for keywords ;; special case for keywords
[(#%plain-app [(#%plain-app
(#%plain-app kpe kws num fn) (#%plain-app kpe kws num fn)
@ -449,7 +451,10 @@
(tc/let-values #'((x) ...) #'(args ...) #'body (tc/let-values #'((x) ...) #'(args ...) #'body
#'(let-values ([(x) args] ...) . body) #'(let-values ([(x) args] ...) . body)
expected)] expected)]
;; FIXME - make this work - doesn't work because the annotation
;; on rst is not a normal annotation, may have * or ...
;; inference for ((lambda with dotted rest ;; inference for ((lambda with dotted rest
#;
[(#%plain-app (#%plain-lambda (x ... . rst:id) . body) args ...) [(#%plain-app (#%plain-lambda (x ... . rst:id) . body) args ...)
#:when (<= (length (syntax->list #'(x ...))) #:when (<= (length (syntax->list #'(x ...)))
(length (syntax->list #'(args ...)))) (length (syntax->list #'(args ...))))

2
collects/typed-scheme/typecheck/tc-expr-unit.ss
View File

@ -121,7 +121,7 @@
;; tc-expr/t : Expr -> Type ;; tc-expr/t : Expr -> Type
(define (tc-expr/t e) (match (tc-expr e) (define (tc-expr/t e) (match (tc-expr e)
[(tc-result1: t _ _) t] [(tc-result1: t _ _) t]
[t (int-err "tc-expr returned ~a, not a single tc-result, for ~a" t (syntax->datum e))])) [t (int-err "tc-expr returned ~a, not a single tc-result, for ~a" t (syntax->datum e))]))
(define (tc-expr/check/t e t) (define (tc-expr/check/t e t)
(match (tc-expr/check e t) (match (tc-expr/check e t)

2
collects/typed-scheme/typecheck/tc-lambda-unit.ss
View File

@ -277,7 +277,7 @@
;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result ;; tc/lambda/internal syntax syntax-list syntax-list option[type] -> tc-result
(define (tc/lambda/internal form formals bodies expected) (define (tc/lambda/internal form formals bodies expected)
(if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected)) (if (or (syntax-property form 'typechecker:plambda) (Poly? expected) (PolyDots? expected))
(ret (tc/plambda form formals bodies expected)) (ret (tc/plambda form formals bodies expected) true-filter)
(ret (tc/mono-lambda/type formals bodies expected) true-filter))) (ret (tc/mono-lambda/type formals bodies expected) true-filter)))
;; tc/lambda : syntax syntax-list syntax-list -> tc-result ;; tc/lambda : syntax syntax-list syntax-list -> tc-result