diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 115f783814..07999859cd 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -130,6 +130,8 @@ ((-lst b) b) . ->... . -Void))] [fold-left (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a)) ((-lst b) b) . ->... . c))] + [fold-right (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a)) + ((-lst b) b) . ->... . c))] [foldl (-poly (a b c) (cl-> [((a b . -> . b) b (make-lst a)) b] diff --git a/collects/typed-scheme/private/constraint-structs.ss b/collects/typed-scheme/private/constraint-structs.ss index abc78e85ff..911f7ae883 100644 --- a/collects/typed-scheme/private/constraint-structs.ss +++ b/collects/typed-scheme/private/constraint-structs.ss @@ -11,7 +11,11 @@ ;; rest : option[c] (define-struct dcon (fixed rest) #:prefab) -;; map : hash mapping variable to dcon +;; type : c +;; bound : vars +(define-struct dcon-dotted (type bound) #:prefab) + +;; map : hash mapping variable to dcon or dcon-dotted (define-struct dmap (map) #:prefab) ;; maps is a list of pairs of @@ -32,5 +36,6 @@ (provide/contract (struct c ([S Type?] [X symbol?] [T Type?])) (struct dcon ([fixed (listof c?)] [rest (or/c c? false/c)])) - (struct dmap ([map (hashof symbol? dcon?)])) + (struct dcon-dotted ([type c?] [bound symbol?])) + (struct dmap ([map (hashof symbol? (lambda (e) (or (dcon? e) (dcon-dotted? e))))])) (struct cset ([maps (listof (cons/c (hashof symbol? c?) dmap?))]))) \ No newline at end of file diff --git a/collects/typed-scheme/private/dmap.ss b/collects/typed-scheme/private/dmap.ss index 1a2aa2c07e..9a26803485 100644 --- a/collects/typed-scheme/private/dmap.ss +++ b/collects/typed-scheme/private/dmap.ss @@ -37,6 +37,14 @@ [c2 (in-list-forever shorter srest)]) (c-meet c1 c2 (c-X c1))) (c-meet lrest srest (c-X lrest))))] + [((struct dcon-dotted (c1 bound1)) (struct dcon-dotted (c2 bound2))) + (unless (eq? bound1 bound2) + (fail! bound1 bound2)) + (make-dcon-dotted (c-meet c1 c2 bound1) bound1)] + [((struct dcon _) (struct dcon-dotted _)) + (fail! dc1 dc2)] + [((struct dcon-dotted _) (struct dcon _)) + (fail! dc1 dc2)] [(_ _) (int-err "Got non-dcons: ~a ~a" dc1 dc2)])) (define (dmap-meet dm1 dm2) diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss index e2c6b97bf7..7c793ccf28 100644 --- a/collects/typed-scheme/private/extra-procs.ss +++ b/collects/typed-scheme/private/extra-procs.ss @@ -6,5 +6,10 @@ (error "Assertion failed - value was #f")) v) - - +(define (fold-right f c as . bss) + (if (or (null? as) + (ormap null? bss)) + c + (apply f + (apply fold-right f c (cdr as) (map cdr bss)) + (car as) (map car bss)))) \ No newline at end of file diff --git a/collects/typed-scheme/private/infer-unit.ss b/collects/typed-scheme/private/infer-unit.ss index 1f6c0a4fe2..f8add2261b 100644 --- a/collects/typed-scheme/private/infer-unit.ss +++ b/collects/typed-scheme/private/infer-unit.ss @@ -35,6 +35,10 @@ (if (eq? dbound v) rest (hash-ref fixed v (no-constraint v)))] + [(struct dcon-dotted (type bound)) + (if (eq? bound v) + type + (no-constraint v))] [_ (no-constraint v)]))) (define (map/cset f cset) @@ -107,95 +111,106 @@ (define (cgen/arr V X t-arr s-arr) (define (cg S T) (cgen V X S T)) (match* (t-arr s-arr) - [((arr: ts t #f #f t-thn-eff t-els-eff) - (arr: ss s #f #f s-thn-eff s-els-eff)) - (cset-meet* - (list (cgen/list X V ss ts) - (cg t s) - (cgen/eff/list V X t-thn-eff s-thn-eff) - (cgen/eff/list V X t-els-eff s-els-eff)))] - [((arr: ts t t-rest #f t-thn-eff t-els-eff) - (arr: ss s s-rest #f s-thn-eff s-els-eff)) - (let ([arg-mapping - (cond [(and t-rest s-rest (<= (length ts) (length ss))) - (cgen/list X V (cons s-rest ss) (cons t-rest (extend ss ts t-rest)))] - [(and t-rest s-rest (>= (length ts) (length ss))) - (cgen/list X V (cons s-rest (extend ts ss s-rest)) (cons t-rest ts))] - [(and t-rest (not s-rest) (<= (length ts) (length ss))) - (cgen/list X V ss (extend ss ts t-rest))] - [(and s-rest (not t-rest) (>= (length ts) (length ss))) - (cgen/list X V (extend ts ss s-rest) ts)] - [else (fail! S T)])] - [ret-mapping (cg t s)]) - (cset-meet* - (list arg-mapping ret-mapping - (cgen/eff/list V X t-thn-eff s-thn-eff) - (cgen/eff/list V X t-els-eff s-els-eff))))] - [((arr: ts t #f (cons dty dbound) t-thn-eff t-els-eff) - (arr: ss s #f #f s-thn-eff s-els-eff)) - (unless (memq dbound X) - (fail! S T)) - (unless (<= (length ts) (length ss)) - (fail! S T)) - (let* ([num-vars (- (length ss) (length ts))] - [vars (for/list ([n (in-range num-vars)]) - (gensym dbound))] - [new-tys (for/list ([var vars]) - (substitute (make-F var) dbound dty))] - [new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f t-thn-eff t-els-eff) s-arr)]) - (move-vars-to-dmap new-cset dbound vars))] - [((arr: ts t #f #f t-thn-eff t-els-eff) - (arr: ss s #f (cons dty dbound) s-thn-eff s-els-eff)) - (unless (memq dbound X) - (fail! S T)) - (unless (<= (length ss) (length ts)) - (fail! S T)) - (let* ([num-vars (- (length ts) (length ss))] - [vars (for/list ([n (in-range num-vars)]) - (gensym dbound))] - [new-tys (for/list ([var vars]) - (substitute (make-F var) dbound dty))] - [new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f s-thn-eff s-els-eff))]) - (move-vars-to-dmap new-cset dbound vars))] - [((arr: ts t #f (cons t-dty dbound) t-thn-eff t-els-eff) - (arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff)) - (unless (= (length ts) (length ss)) - (fail! S T)) - ;; If we want to infer the dotted bound, then why is it in both types? - (when (memq dbound X) - (fail! S T)) - (let* ([arg-mapping (cgen/list X V ss ts)] - [darg-mapping (cgen (cons dbound V) X s-dty t-dty)] - [ret-mapping (cg t s)]) - (cset-meet* - (list arg-mapping darg-mapping ret-mapping - (cgen/eff/list V X t-thn-eff s-thn-eff) - (cgen/eff/list V X t-els-eff s-els-eff))))] - [((arr: ts t t-rest #f t-thn-eff t-els-eff) - (arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff)) - (unless (memq dbound X) - (fail! S T)) - (if (<= (length ts) (length ss)) - ;; the simple case - (let* ([arg-mapping (cgen/list X V ss (extend ss ts t-rest))] - [darg-mapping (move-rest-to-dmap (cgen (cons dbound V) X s-dty t-rest) dbound)] - [ret-mapping (cg t s)]) - (cset-meet* (list arg-mapping darg-mapping ret-mapping - (cgen/eff/list V X t-thn-eff s-thn-eff) - (cgen/eff/list V X t-els-eff s-els-eff)))) - ;; the hard case - (let* ([num-vars (- (length ts) (length ss))] - [vars (for/list ([n (in-range num-vars)]) - (gensym dbound))] - [new-tys (for/list ([var vars]) - (substitute (make-F var) dbound s-dty))] - [new-cset (cgen/arr V (append vars X) t-arr - (make-arr (append ss new-tys) s #f (cons s-dty dbound) s-thn-eff s-els-eff))]) - (move-vars+rest-to-dmap new-cset dbound vars)))] - ;; If dotted <: starred is correct, add it below. Not sure it is. - [(_ _) (fail! S T)])) + [((arr: ts t #f #f t-thn-eff t-els-eff) + (arr: ss s #f #f s-thn-eff s-els-eff)) + (cset-meet* + (list (cgen/list X V ss ts) + (cg t s) + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff)))] + [((arr: ts t t-rest #f t-thn-eff t-els-eff) + (arr: ss s s-rest #f s-thn-eff s-els-eff)) + (let ([arg-mapping + (cond [(and t-rest s-rest (<= (length ts) (length ss))) + (cgen/list X V (cons s-rest ss) (cons t-rest (extend ss ts t-rest)))] + [(and t-rest s-rest (>= (length ts) (length ss))) + (cgen/list X V (cons s-rest (extend ts ss s-rest)) (cons t-rest ts))] + [(and t-rest (not s-rest) (<= (length ts) (length ss))) + (cgen/list X V ss (extend ss ts t-rest))] + [(and s-rest (not t-rest) (>= (length ts) (length ss))) + (cgen/list X V (extend ts ss s-rest) ts)] + [else (fail! S T)])] + [ret-mapping (cg t s)]) + (cset-meet* + (list arg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff))))] + [((arr: ts t #f (cons dty dbound) t-thn-eff t-els-eff) + (arr: ss s #f #f s-thn-eff s-els-eff)) + (unless (memq dbound X) + (fail! S T)) + (unless (<= (length ts) (length ss)) + (fail! S T)) + (let* ([num-vars (- (length ss) (length ts))] + [vars (for/list ([n (in-range num-vars)]) + (gensym dbound))] + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound dty))] + [new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f t-thn-eff t-els-eff) s-arr)]) + (move-vars-to-dmap new-cset dbound vars))] + [((arr: ts t #f #f t-thn-eff t-els-eff) + (arr: ss s #f (cons dty dbound) s-thn-eff s-els-eff)) + (unless (memq dbound X) + (fail! S T)) + (unless (<= (length ss) (length ts)) + (fail! S T)) + (let* ([num-vars (- (length ts) (length ss))] + [vars (for/list ([n (in-range num-vars)]) + (gensym dbound))] + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound dty))] + [new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f s-thn-eff s-els-eff))]) + (move-vars-to-dmap new-cset dbound vars))] + [((arr: ts t #f (cons t-dty dbound) t-thn-eff t-els-eff) + (arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff)) + (unless (= (length ts) (length ss)) + (fail! S T)) + ;; If we want to infer the dotted bound, then why is it in both types? + (when (memq dbound X) + (fail! S T)) + (let* ([arg-mapping (cgen/list X V ss ts)] + [darg-mapping (cgen (cons dbound V) X s-dty t-dty)] + [ret-mapping (cg t s)]) + (cset-meet* + (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff))))] + [((arr: ts t #f (cons t-dty dbound) t-thn-eff t-els-eff) + (arr: ss s #f (cons s-dty dbound*) s-thn-eff s-els-eff)) + (unless (= (length ts) (length ss)) + (fail! S T)) + (let* ([arg-mapping (cgen/list X V ss ts)] + [darg-mapping (cgen V (cons dbound* X) s-dty t-dty)] + [ret-mapping (cg t s)]) + (cset-meet* + (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff))))] + [((arr: ts t t-rest #f t-thn-eff t-els-eff) + (arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff)) + (unless (memq dbound X) + (fail! S T)) + (if (<= (length ts) (length ss)) + ;; the simple case + (let* ([arg-mapping (cgen/list X V ss (extend ss ts t-rest))] + [darg-mapping (move-rest-to-dmap (cgen (cons dbound V) X s-dty t-rest) dbound)] + [ret-mapping (cg t s)]) + (cset-meet* (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff)))) + ;; the hard case + (let* ([num-vars (- (length ts) (length ss))] + [vars (for/list ([n (in-range num-vars)]) + (gensym dbound))] + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound s-dty))] + [new-cset (cgen/arr V (append vars X) t-arr + (make-arr (append ss new-tys) s #f (cons s-dty dbound) s-thn-eff s-els-eff))]) + (move-vars+rest-to-dmap new-cset dbound vars)))] + ;; If dotted <: starred is correct, add it below. Not sure it is. + [(_ _) (fail! S T)])) -(define (cgen V X S T) +(define (cgen V X S T) (define (cg S T) (cgen V X S T)) (define empty (empty-cset X)) (define (singleton S X T) @@ -224,7 +239,6 @@ (fail! S T)) (singleton (var-promote S V) v Univ)] - ;; two unions with the same number of elements, so we just try to unify them pairwise #;[((Union: l1) (Union: l2)) (=> unmatch) diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss index 533309abdc..e1091d655a 100644 --- a/collects/typed-scheme/private/tc-app-unit.ss +++ b/collects/typed-scheme/private/tc-app-unit.ss @@ -13,6 +13,7 @@ "type-annotation.ss" "resolve-type.ss" "type-environments.ss" + (only-in srfi/1 alist-delete) (only-in scheme/private/class-internal make-object do-make-object) mzlib/trace mzlib/pretty syntax/kerncase scheme/match (for-template @@ -324,7 +325,7 @@ (car rests*) (car rngs*))) => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] - ;; ... function, ... arg + ;; ... function, ... arg, same bound on ... [(and (car drests*) tail-bound (eq? tail-bound (cdr (car drests*))) @@ -332,6 +333,24 @@ (length arg-tys)) (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*))) => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] + ;; ... function, ... arg, different bound on ... + [(and (car drests*) + tail-bound + (not (eq? tail-bound (cdr (car drests*)))) + (= (length (car doms*)) + (length arg-tys)) + (parameterize ([current-tvars (extend-env (list tail-bound (cdr (car drests*))) + (list (make-DottedBoth (make-F tail-bound)) + (make-DottedBoth (make-F (cdr (car drests*))))) + (current-tvars))]) + (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*)))) + => (lambda (substitution) + (define drest-bound (cdr (car drests*))) + (ret (substitute-dotted (cadr (assq drest-bound substitution)) + tail-bound + drest-bound + (subst-all (alist-delete drest-bound substitution eq?) + (car rngs*)))))] ;; if nothing matches, around the loop again [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [(tc-result: (PolyDots: vars (Function: '()))) diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss index 5987266e33..4022514d43 100644 --- a/collects/typed-scheme/private/type-utils.ss +++ b/collects/typed-scheme/private/type-utils.ss @@ -12,6 +12,7 @@ (provide fv fv/list substitute substitute-dots + substitute-dotted subst-all subst ret @@ -76,7 +77,7 @@ target)) ;; implements sd from the formalism -;; substitute-dotted : Type Name Type Name -> Type +;; substitute-dotted : Type Name Name Type -> Type (define (substitute-dotted image image-bound name target) (define (sb t) (substitute-dotted image image-bound name t)) (if (hash-ref (free-vars* target) name #f)