Fix new inference algorithm to handle all test cases.
svn: r9538
This commit is contained in:
Sam Tobin-Hochstadt
parent
ab81b1d64f
commit
8307bf835b
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user