From 8307bf835b23160b58b52c50815997f5fd8e11e8 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 29 Apr 2008 21:42:37 +0000 Subject: [PATCH] Fix new inference algorithm to handle all test cases. svn: r9538 --- collects/typed-scheme/private/infer-ops.ss | 42 +++++++++++++---- collects/typed-scheme/private/tc-app-unit.ss | 48 ++++++++++---------- collects/typed-scheme/typed-scheme.ss | 3 +- 3 files changed, 59 insertions(+), 34 deletions(-) diff --git a/collects/typed-scheme/private/infer-ops.ss b/collects/typed-scheme/private/infer-ops.ss index 3841c4abe8..b328a08285 100644 --- a/collects/typed-scheme/private/infer-ops.ss +++ b/collects/typed-scheme/private/infer-ops.ss @@ -139,6 +139,15 @@ (singleton (Un) v (var-demote S V))] [(S (F: (? (lambda (e) (memq e X)) v))) (singleton (var-promote S V) v Univ)] + [((Struct: nm p flds proc) (Struct: nm p flds* proc*)) + (let-values ([(flds flds*) + (cond [(and proc proc*) + (values (cons proc flds) (cons proc* flds*))] + [(or proc proc*) + (fail! S T)] + [else (values flds flds*)])]) + (cset-meet* X (for/list ([f flds] [f* flds*]) + (cgen V X f f*))))] [((Pair: a b) (Pair: a* b*)) (cset-meet (cgen V X a a*) (cgen V X b b*))] ;; if we have two mu's, we rename them to have the same variable @@ -148,6 +157,14 @@ ;; other mu's just get unfolded [(s (? Mu? t)) (cgen V X s (unfold t))] [((? Mu? s) t) (cgen V X (unfold s) t)] + ;; type application + [((App: (Name: n) args _) + (App: (Name: n*) args* _)) + (unless (free-identifier=? n n*) + (fail! S T)) + (cset-meet* X (for/list ([a args] [a* args*]) (cgen V X a a*)))] + [((Vector: e) (Vector: e*)) + (cset-meet (cgen V X e e*) (cgen V X e* e))] [((Function: (list t-arr ...)) (Function: (list s-arr ...))) (=> unmatch) @@ -173,9 +190,10 @@ [ret-mapping (cgen V X t s)]) (loop (cdr t-arr) (cdr s-arr) (cset-meet* X (list cset arg-mapping ret-mapping))))])]))] - [(_ _) (cond [(subtype S T) empty] - ;; or, nothing worked, and we fail - [else (fail! S T)])]))) + [(_ _) + (cond [(subtype S T) empty] + ;; or, nothing worked, and we fail + [else (fail! S T)])]))) (define (subst-gen C R) (for/list ([(k v) (cset-map C)]) @@ -189,23 +207,27 @@ [Covariant S] [Contravariant T] [Invariant (unless (type-equal? S T) - (error "invariant and not equal")) + (fail! S T)) S])))]))) ;; X : variables to infer ;; S : actual argument types ;; T : formal argument types -;; R : result type +;; R : result type or #f ;; returns a substitution +;; if R is #f, we don't care about the substituion +;; just return a boolean result (define (infer X S T R) (with-handlers ([exn:infer? (lambda _ #f)]) - (subst-gen (cset-meet* X (for/list ([s S] [t T]) (cgen null X s t))) R))) + (let ([cs (cset-meet* X (for/list ([s S] [t T]) (cgen null X s t)))]) + (if R + (subst-gen cs R) + #t)))) ;; like infer, but T-var is the vararg type: (define (infer/vararg X S T T-var R) (define new-T (extend S T T-var)) - (if (>= (length S) (length T)) - #f ;; fail - (infer X S new-T R))) + (and ((length S) . >= . (length T)) + (infer X S new-T R))) ;; Listof[A] Listof[B] B -> Listof[B] ;; pads out t to be as long as s @@ -215,7 +237,7 @@ (define (infer/simple S T R) (infer (fv/list T) S T R)) -;(trace var-demote) +;(trace infer #;cgen #;cset-meet*) ;(trace cgen) diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss index e138b94234..425c5067e8 100644 --- a/collects/typed-scheme/private/tc-app-unit.ss +++ b/collects/typed-scheme/private/tc-app-unit.ss @@ -187,7 +187,7 @@ [else (cons (car l) (cons v (intersperse v (cdr l))))])) (apply string-append (intersperse between (map (lambda (s) (format "~a" s)) l)))) -(define (tc/funapp f-stx args-stx ftype0 argtys) +(define (tc/funapp f-stx args-stx ftype0 argtys expected) (match-let* ([(list (tc-result: argtypes arg-thn-effs arg-els-effs) ...) argtys]) (let outer-loop ([ftype ftype0] [argtypes argtypes] @@ -252,16 +252,17 @@ (stringify (map stringify msg-doms) "\n") (stringify argtypes))))] [(and (= (length (car doms*)) (length argtypes)) - (infer vars argtypes (car doms*) (car rngs*)) + (infer vars argtypes (car doms*) (if expected #f (car rngs*))) #;(infer/list (car doms*) argtypes vars)) => (lambda (substitution) - (let* ([s (lambda (t) (subst-all substitution t))] - [new-doms* (map s (car doms*))]) - (if (andmap subtype argtypes new-doms*) - (ret (subst-all substitution (car rngs*))) - ;; FIXME - ;; should be an error here, something went horribly wrong!!! - (loop (cdr doms*) (cdr rngs*)))))] + (or expected + (let* ([s (lambda (t) (subst-all substitution t))] + [new-doms* (map s (car doms*))]) + (if (andmap subtype argtypes new-doms*) + (ret (subst-all substitution (car rngs*))) + ;; FIXME + ;; should be an error here, something went horribly wrong!!! + (loop (cdr doms*) (cdr rngs*))))))] #| (printf "subst is:~a~nret is: ~a~nvars is: ~a~nresult is:~a~n" substitution (car rngs*) vars (subst-all substitution (car rngs*))) @@ -280,18 +281,19 @@ (unless (<= (length dom) (length argtypes)) (tc-error "incorrect number of arguments to function: ~a ~a" dom argtypes)) (let ([substitution - (infer/vararg vars argtypes dom rest rng) - #;(infer/list/vararg dom rest argtypes vars)]) - (if substitution - (let* ([s (lambda (t) (subst-all substitution t))] - [new-dom (map s dom)] - [new-rest (s rest)]) - (unless (subtypes/varargs argtypes new-dom new-rest) - (int-err "Inconsistent substitution - arguments not subtypes")) - (ret (subst-all substitution rng))) - (tc-error/expr #:return (ret (Un)) - "no polymorphic function domain matched - domain was: ~a rest type was: ~a arguments were ~a" - (stringify dom) rest (stringify argtypes))))] + (infer/vararg vars argtypes dom rest (if expected #f rng))]) + (cond + [(and expected substitution) expected] + [substitution + (let* ([s (lambda (t) (subst-all substitution t))] + [new-dom (map s dom)] + [new-rest (s rest)]) + (unless (subtypes/varargs argtypes new-dom new-rest) + (int-err "Inconsistent substitution - arguments not subtypes")) + (ret (subst-all substitution rng)))] + [else (tc-error/expr #:return (ret (Un)) + "no polymorphic function domain matched - domain was: ~a rest type was: ~a arguments were ~a" + (stringify dom) rest (stringify argtypes))]))] [(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests thn-effs els-effs) ...)))) (tc-error/expr #:return (ret (Un)) "polymorphic vararg case-lambda application not yet supported")] ;; Union of function types works if we can apply all of them @@ -420,7 +422,7 @@ (and (identifier? #'eq?) (comparator? #'eq?)) (begin ;; make sure the whole expression is type correct - (tc/funapp #'eq? #'(v1 v2) (tc-expr #'eq?) (map tc-expr (syntax->list #'(v1 v2)))) + (tc/funapp #'eq? #'(v1 v2) (tc-expr #'eq?) (map tc-expr (syntax->list #'(v1 v2))) expected) ;; check thn and els with the eq? info (let-values ([(thn-eff els-eff) (tc/eq #'eq? #'v1 #'v2)]) (ret B thn-eff els-eff)))] @@ -493,6 +495,6 @@ [(#%plain-app f args ...) (begin ;(printf "default case~n~a~n" (syntax->datum form)) - (tc/funapp #'f #'(args ...) (tc-expr #'f) (map tc-expr (syntax->list #'(args ...)))))])) + (tc/funapp #'f #'(args ...) (tc-expr #'f) (map tc-expr (syntax->list #'(args ...))) expected))])) ;(trace tc/app/internal) diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss index a39d738c50..2b089da668 100644 --- a/collects/typed-scheme/typed-scheme.ss +++ b/collects/typed-scheme/typed-scheme.ss @@ -60,7 +60,8 @@ [with-handlers ([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e)))) (lambda (e) (tc-error "Internal error: ~a" e))])] - [parameterize (;; this parameter is for parsing types + [parameterize ([delay-errors? #f] + ;; this parameter is for parsing types [current-tvars initial-tvar-env] ;; this parameter is just for printing types ;; this is a parameter to avoid dependency issues