Fix a bunch of uses of `infer' et al.

This commit is contained in:
Sam Tobin-Hochstadt 2010-06-02 14:21:22 -04:00
parent 99e499a503
commit 18f45c4138
4 changed files with 31 additions and 19 deletions

View File

@ -4,6 +4,6 @@
(require (rep type-rep) (utils tc-utils) mzlib/trace) (require (rep type-rep) (utils tc-utils) mzlib/trace)
(define infer-param (make-parameter (lambda e (int-err "infer not initialized")))) (define infer-param (make-parameter (lambda e (int-err "infer not initialized"))))
(define (unify X S T) ((infer-param) X S T (make-Univ) null)) (define (unify X S T) ((infer-param) X null S T (make-Univ) null null))
;(trace unify) ;(trace unify)
(provide unify infer-param) (provide unify infer-param)

View File

@ -510,10 +510,11 @@
;; just return a boolean result ;; just return a boolean result
(define (infer X Y S T R must-vars must-idxs [expected #f]) (define (infer X Y S T R must-vars must-idxs [expected #f])
(with-handlers ([exn:infer? (lambda _ #f)]) (with-handlers ([exn:infer? (lambda _ #f)])
(let ([cs (cgen/list null X Y S T)]) (let* ([cs (cgen/list null (append X Y) S T)]
(if (not expected) [cs* (if expected
(subst-gen cs R (append must-vars must-idxs)) (cset-meet cs (cgen null (append X Y) R expected))
(subst-gen (cset-meet cs (cgen null X Y R expected)) R must-vars))))) cs)])
(subst-gen cs* R (append must-vars must-idxs)))))
;; like infer, but T-var is the vararg type: ;; like infer, but T-var is the vararg type:
(define (infer/vararg X Y S T T-var R must-vars must-idxs [expected #f]) (define (infer/vararg X Y S T T-var R must-vars must-idxs [expected #f])

View File

@ -23,7 +23,7 @@
[(subtype t1 t2) t1] ;; already a subtype [(subtype t1 t2) t1] ;; already a subtype
[(match t2 [(match t2
[(Poly: vars t) [(Poly: vars t)
(let ([subst (infer vars (list t1) (list t) t1 vars)]) (let ([subst (infer vars null (list t1) (list t) t1 (fv t1) (fi t1))])
(and subst (restrict* t1 (subst-all subst t1))))] (and subst (restrict* t1 (subst-all subst t1))))]
[_ #f])] [_ #f])]
[(Union? t1) (union-map (lambda (e) (restrict* e t2)) t1)] [(Union? t1) (union-map (lambda (e) (restrict* e t2)) t1)]

View File

@ -319,26 +319,28 @@
(not tail-bound) (not tail-bound)
(<= (length (car doms*)) (<= (length (car doms*))
(length arg-tys)) (length arg-tys))
(infer/vararg vars (infer/vararg vars null
(cons tail-ty arg-tys) (cons tail-ty arg-tys)
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*) (car rngs*)
(fv (car rngs*)))) (fv (car rngs*))
(fi (car rngs*))))
=> (lambda (substitution) (do-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
(<= (length (car doms*)) (<= (length (car doms*))
(length arg-tys)) (length arg-tys))
(infer/vararg vars (infer/vararg vars null
(cons (make-Listof tail-ty) arg-tys) (cons (make-Listof tail-ty) arg-tys)
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*) (car rngs*)
(fv (car rngs*)))) (fv (car rngs*))
(fi (car rngs*))))
=> (lambda (substitution) (do-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*)
@ -346,7 +348,8 @@
(eq? tail-bound (cdr (car drests*))) (eq? tail-bound (cdr (car drests*)))
(= (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 null (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*))
(car rngs*) (fv (car rngs*)) (fi (car rngs*))))
=> (lambda (substitution) (do-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*))])))]
@ -373,26 +376,26 @@
(not tail-bound) (not tail-bound)
(<= (length (car doms*)) (<= (length (car doms*))
(length arg-tys)) (length arg-tys))
(infer/vararg vars (infer/vararg fixed-vars (list dotted-var)
(cons tail-ty arg-tys) (cons tail-ty arg-tys)
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*) (car rngs*)
(fv (car rngs*)))) (fv (car rngs*)) (fi (car rngs*))))
=> (lambda (substitution) (do-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
(<= (length (car doms*)) (<= (length (car doms*))
(length arg-tys)) (length arg-tys))
(infer/vararg vars (infer/vararg fixed-vars (list dotted-var)
(cons (make-Listof tail-ty) arg-tys) (cons (make-Listof tail-ty) arg-tys)
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*) (car rngs*)
(fv (car rngs*)))) (fv (car rngs*)) (fi (car rngs*))))
=> (lambda (substitution) => (lambda (substitution)
(do-ret (subst-all substitution (car rngs*))))] (do-ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg, same bound on ... ;; ... function, ... arg, same bound on ...
@ -401,7 +404,11 @@
(eq? tail-bound (cdr (car drests*))) (eq? tail-bound (cdr (car drests*)))
(= (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 fixed-vars (list dotted-var)
(cons tail-ty arg-tys)
(cons (car (car drests*)) (car doms*))
(car rngs*)
(fv (car rngs*)) (fi (car rngs*))))
=> (lambda (substitution) => (lambda (substitution)
(do-ret (subst-all substitution (car rngs*))))] (do-ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg, different bound on ... ;; ... function, ... arg, different bound on ...
@ -413,7 +420,11 @@
(extend-tvars (list tail-bound (cdr (car drests*))) (extend-tvars (list tail-bound (cdr (car drests*)))
(extend-indexes (cdr (car drests*)) (extend-indexes (cdr (car drests*))
;; don't need to add tail-bound - it must already be an index ;; don't need to add tail-bound - it must already be an index
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*)))))) (infer fixed-vars (list dotted-var)
(cons tail-ty arg-tys)
(cons (car (car drests*)) (car doms*))
(car rngs*)
(fv (car rngs*)) (fi (car rngs*))))))
=> (lambda (substitution) => (lambda (substitution)
(define drest-bound (cdr (car drests*))) (define drest-bound (cdr (car drests*)))
(do-ret (substitute-dotted (cadr (assq drest-bound substitution)) (do-ret (substitute-dotted (cadr (assq drest-bound substitution))
@ -610,7 +621,7 @@
(fail)) (fail))
(match (map single-value (syntax->list #'pos-args)) (match (map single-value (syntax->list #'pos-args))
[(list (tc-result1: argtys-t) ...) [(list (tc-result1: argtys-t) ...)
(let* ([subst (infer vars argtys-t dom rng (fv rng) (and expected (tc-results->values expected)))]) (let* ([subst (infer vars null argtys-t dom rng (fv rng) (fi rng) (and expected (tc-results->values expected)))])
(tc-keywords form (list (subst-all subst ar)) (tc-keywords form (list (subst-all subst ar))
(type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected))])] (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected))])]
[(tc-result1: (Function: arities)) [(tc-result1: (Function: arities))
@ -843,7 +854,7 @@
(lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys))) (lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys)))
;; only try to infer the free vars of the rng (which includes the vars in filters/objects) ;; only try to infer the free vars of the rng (which includes the vars in filters/objects)
;; note that we have to use argtys-t here, since argtys is a list of tc-results ;; note that we have to use argtys-t here, since argtys is a list of tc-results
(lambda (dom rng rest a) (infer/vararg vars argtys-t dom rest rng (fv rng) (and expected (tc-results->values expected)))) (lambda (dom rng rest a) (infer/vararg vars null argtys-t dom rest rng (fv rng) (fi rng) (and expected (tc-results->values expected))))
t argtys expected)] t argtys expected)]
;; procedural structs ;; procedural structs
[((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _ _))) _) [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _ _))) _)