Don't produce extra errors for top-level defines.

Lots more error message improvements for application.
Work on polydots apply.
Extend environment only in the proper place in plambda.
Don't let a variable unify with a dotted variable.
This commit is contained in:
Sam Tobin-Hochstadt 2008-06-17 16:28:34 -04:00
parent ddbb045a3e
commit c8a2810742
7 changed files with 76 additions and 38 deletions

View File

@ -6,6 +6,7 @@
"union.ss" "tc-utils.ss" "type-name-env.ss"
"subtype.ss" "remove-intersect.ss" "signatures.ss" "utils.ss"
"constraint-structs.ss"
(only-in "type-environments.ss" lookup current-tvars)
scheme/match
mzlib/etc
mzlib/trace
@ -185,8 +186,18 @@
[(_ (Univ:)) empty]
[((F: (? (lambda (e) (memq e X)) v)) S)
(when (match S
[(F: v*)
(just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
[_ #f])
(fail! S T))
(singleton (Un) v (var-demote S V))]
[(S (F: (? (lambda (e) (memq e X)) v)))
(when (match S
[(F: v*)
(just-Dotted? (lookup (current-tvars) v* (lambda _ #f)))]
[_ #f])
(fail! S T))
(singleton (var-promote S V) v Univ)]

View File

@ -126,14 +126,18 @@
(let loop ([l l] [acc '()])
(if (null? (cdr l))
(values (reverse acc) (car l))
(loop (cdr l) (cons (car l) acc)))))
(define (printable dom rst drst)
(loop (cdr l) (cons (car l) acc)))))
(define (printable-h dom r-ty r-bound)
(let ([doms-string (if (null? dom) "" (string-append (stringify dom) " "))])
(cond [rst
(format "~a~a *" doms-string rst)]
[drst
(format "~a~a ... ~a" doms-string (car drst) (cdr drst))]
(cond [r-bound
(format "~a~a ... ~a" doms-string r-ty r-bound)]
[r-ty
(format "~a~a *" doms-string r-ty)]
[else (stringify dom)])))
(define (printable dom rst drst)
(cond [rst (printable-h dom rst #f)]
[drst (printable-h dom (car drst) (cdr drst))]
[else (printable-h dom #f #f)]))
(define-values (fixed-args tail) (split (syntax->list args)))
(define (apply-error doms rests drests arg-tys tail-ty tail-bound)
(if (and (not (null? doms)) (null? (cdr doms)))
@ -172,11 +176,9 @@
(let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests])
(cond [(null? doms*)
(let-values ([(tail-ty tail-bound)
(with-handlers ([exn:fail? (lambda _ (values #f #f))])
(with-handlers ([exn:fail? (lambda _ (values (tc-expr/t tail) #f))])
(tc/dots tail))])
(if tail-ty
(apply-error doms rests drests arg-tys tail-ty tail-bound)
(apply-error doms rests drests arg-tys (tc-expr/t tail) #f)))]
(apply-error doms rests drests arg-tys tail-ty tail-bound))]
[(and (car rests*)
(let-values ([(tail-ty tail-bound)
(with-handlers ([exn:fail? (lambda _ (values #f #f))])
@ -203,9 +205,9 @@
(ret (car rngs*))]
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1))))
(let*-values ([(arg-tys tail-ty) (values (map tc-expr/t fixed-args)
(tc-expr/t tail))]
[(arg-tys0) (append arg-tys (list tail-ty))])
(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))])
(tc/dots tail))])
(for-each (lambda (x) (unless (not (Poly? x))
(tc-error "Polymorphic argument ~a to polymorphic function in apply not allowed" x)))
(cons tail-ty arg-tys))
@ -220,11 +222,11 @@
(tc-error/expr
#:return (ret (Un))
"polymorphic function domain did not match -~ndomain was: ~a~nrest argument was: ~a~narguments were ~a~n"
(car doms) (car rests) (stringify arg-tys0))
(car doms) (car rests) (printable-h arg-tys tail-ty tail-bound))
(tc-error/expr
#:return (ret (Un))
"polymorphic function domain did not match -~ndomain was: ~a~narguments were ~a~n"
(car doms) (stringify arg-tys0)))]
(car doms) (printable-h arg-tys tail-ty tail-bound)))]
[else
(tc-error/expr
#:return (ret (Un))
@ -235,8 +237,11 @@
(format "~a rest argument: " (stringify dom) rest)
(stringify dom)))
"\n")
(stringify arg-tys0))])])]
[(and (<= (length (car doms*))
(printable-h arg-tys tail-ty tail-bound))])])]
;; the actual work, when we have a * function and a list final argument
[(and (car rests*)
(not tail-bound)
(<= (length (car doms*))
(length arg-tys))
(infer/vararg vars
(cons tail-ty arg-tys)
@ -244,12 +249,18 @@
(car doms*))
(car rests*)
(car rngs*)))
=> (lambda (substitution)
#;(let* ([s (lambda (t) (subst-all substitution t))]
[new-doms* (append (map s (car doms*)) (list (make-Listof (s (car rests*)))))])
(unless (andmap subtype arg-tys0 new-doms*)
(int-err "Inconsistent substitution - arguments not subtypes: ~n~a~n~a~n" arg-tys0 new-doms*)))
(ret (subst-all substitution (car rngs*))))]
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
[(and (car rests*)
tail-bound
(<= (length (car doms*))
(length arg-tys))
(infer/vararg vars
(cons (make-Listof tail-ty) arg-tys)
(cons (make-Listof (car rests*))
(car doms*))
(car rests*)
(car rngs*)))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*))])))]
[(tc-result: (Poly: vars (Function: '())))
(tc-error/expr #:return (ret (Un))

View File

@ -25,6 +25,8 @@
(values dty dbound)])]
[(#%plain-app map f l)
(let-values ([(lty lbound) (tc/dots #'l)])
(unless (Dotted? (lookup (current-tvars) lbound (lambda _ #f)))
(int-err "tc/dots: ~a was not dotted" lbound))
(parameterize ([current-tvars (extend-env (list lbound)
(list (make-DottedBoth (make-F lbound)))
(current-tvars))])

View File

@ -116,18 +116,19 @@
(lambda _ (tc-error/stx #'rest
"Bound on ... type (~a) was not in scope" bound))))
(tc-error "Bound on ... type (~a) is not an appropriate type variable" bound))
(parameterize ([current-tvars (extend-env (list bound)
(list (make-DottedBoth (make-F bound)))
(current-tvars))])
(let ([rest-type (get-type #'rest)])
(with-lexical-env/extend
arg-list
arg-types
(parameterize ([dotted-env (extend-env (list #'rest)
(list (cons rest-type bound))
(dotted-env))])
(match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))])
(make-arr-dots arg-types t rest-type bound)))))))]
(let ([rest-type (parameterize ([current-tvars
(extend-env (list bound)
(list (make-DottedBoth (make-F bound)))
(current-tvars))])
(get-type #'rest))])
(with-lexical-env/extend
arg-list
arg-types
(parameterize ([dotted-env (extend-env (list #'rest)
(list (cons rest-type bound))
(dotted-env))])
(match-let ([(tc-result: t thn els) (tc-exprs (syntax->list body))])
(make-arr-dots arg-types t rest-type bound))))))]
[else
(let ([rest-type (get-type #'rest)])
(with-lexical-env/extend

View File

@ -90,7 +90,10 @@
(map (lambda (s) (make-def-binding s (lookup-type s))) vars)]
;; special case to infer types for top level defines - should handle the multiple values case here
[(and (= 1 (length vars))
(with-handlers ([exn:fail? (lambda _ #f)]) (tc-expr #'expr)))
(with-handlers ([exn:fail? (lambda _ #f)])
(save-errors!)
(begin0 (tc-expr #'expr)
(restore-errors!))))
=> (match-lambda
[(tc-result: t)
(register-type (car vars) t)

View File

@ -49,6 +49,11 @@
(define-struct err (msg stx) #:prefab)
(define-values (save-errors! restore-errors!)
(let ([v (box #f)])
(values (lambda () (set-box! v delayed-errors))
(lambda () (set! delayed-errors (unbox v))))))
(define (report-all-errors)
(define (reset!) (set! delayed-errors null))
(match (reverse delayed-errors)

View File

@ -22,7 +22,8 @@
tc-result-t
unfold
(struct-out Dotted)
(struct-out DottedBoth))
(struct-out DottedBoth)
just-Dotted?)
;; substitute : Type Name Type -> Type
@ -134,4 +135,8 @@
;; t is (make-F v)
(define-struct Dotted (t))
(define-struct (DottedBoth Dotted) ())
(define-struct (DottedBoth Dotted) ())
(define (just-Dotted? S)
(and (Dotted? S)
(not (DottedBoth? S))))