From c43c3baa67512954b0f2e477aafde6f8461bd99a Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Mon, 7 Jul 2008 11:01:42 -0400 Subject: [PATCH] values with dots --- collects/typed-scheme/private/base-env.ss | 3 ++ collects/typed-scheme/private/extra-procs.ss | 7 ++-- collects/typed-scheme/private/infer-unit.ss | 33 +++++++++++++++++++ collects/typed-scheme/private/parse-type.ss | 13 ++++++++ .../private/type-effect-printer.ss | 1 + collects/typed-scheme/private/type-rep.ss | 17 ++++++++-- collects/typed-scheme/private/type-utils.ss | 25 ++++++++++++-- collects/typed-scheme/values-dots-test.ss | 11 +++++++ 8 files changed, 103 insertions(+), 7 deletions(-) create mode 100644 collects/typed-scheme/values-dots-test.ss diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 07999859cd..88b2e8fbec 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -506,6 +506,9 @@ [syntax? (make-pred-ty (-Syntax Univ))] [syntax-property (-poly (a) (cl->* (-> (-Syntax a) Univ Univ (-Syntax a)) (-> (-Syntax Univ) Univ Univ)))] + + [values* (-polydots (a) (null (a a) . ->... . (make-ValuesDots null a 'a)))] + [call-with-values* (-polydots (b a) ((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> . b))] ))) (begin-for-syntax diff --git a/collects/typed-scheme/private/extra-procs.ss b/collects/typed-scheme/private/extra-procs.ss index 7c793ccf28..83aa9c4036 100644 --- a/collects/typed-scheme/private/extra-procs.ss +++ b/collects/typed-scheme/private/extra-procs.ss @@ -1,5 +1,5 @@ #lang scheme/base -(provide assert) +(provide assert call-with-values* values*) (define (assert v) (unless v @@ -12,4 +12,7 @@ c (apply f (apply fold-right f c (cdr as) (map cdr bss)) - (car as) (map car bss)))) \ No newline at end of file + (car as) (map car bss)))) + +(define call-with-values* call-with-values) +(define values* values) \ 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 f19428cb15..eb2e46cbfc 100644 --- a/collects/typed-scheme/private/infer-unit.ss +++ b/collects/typed-scheme/private/infer-unit.ss @@ -339,6 +339,39 @@ (let ([x (instantiate-poly (lookup-type-name n) args)] [y (instantiate-poly (lookup-type-name n) args*)]) (cg x y))] + [((Values: ss) (Values: ts)) + (unless (= (length ss) (length ts)) + (fail! ss ts)) + (cgen/list V X ss ts)] + [((Values: ss) (ValuesDots: ts t-dty dbound)) + (unless (>= (length ss) (length ts)) + (fail! ss ts)) + (unless (memq dbound X) + (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 t-dty))] + [new-cset (cgen/list V X ss (append ts new-tys))]) + (move-vars-to-dmap new-cset vars dbound))] + [((ValuesDots: ss s-dty dbound) (Values: ts)) + (unless (>= (length ts) (length ss)) + (fail! ss ts)) + (unless (memq dbound X) + (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 s-dty))] + [new-cset (cgen/list V X (append ss new-tys) ts)]) + (move-vars-to-dmap new-cset vars dbound))] + [((ValuesDots: ss s-dty dbound) (ValuesDots: ts t-dty dbound)) + (unless (= (length ss) (length ts)) + (fail! ss ts)) + (when (memq dbound X) (fail! ss ts)) + (cgen/list V X (cons s-dty ss) (cons t-dty ts))] [((Vector: e) (Vector: e*)) (cset-meet (cg e e*) (cg e* e))] [((Box: e) (Box: e*)) diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index a5f61ed0b8..88da572e4d 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -101,6 +101,19 @@ (begin (add-type-name-reference #'->) (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rng)))] + [(values tys ... dty dd bound) + (and (eq? (syntax-e #'dd) '...) + (identifier? #'bound) + (eq? (syntax-e #'values) 'values)) + (let ([var (lookup (current-tvars) (syntax-e #'bound) (lambda (_) #f))]) + (if (not (Dotted? var)) + (tc-error/stx #'bound "Used a type variable (~a) not bound with ... as a bound on a ..." (syntax-e #'bound)) + (make-ValuesDots (map parse-type (syntax->list #'(tys ...))) + (parameterize ([current-tvars (extend-env (list (syntax-e #'bound)) + (list (make-DottedBoth (make-F (syntax-e #'bound)))) + (current-tvars))]) + (parse-type #'dty)) + (syntax-e #'bound))))] [(values tys ...) (eq? (syntax-e #'values) 'values) (-values (map parse-type (syntax->list #'(tys ...))))] diff --git a/collects/typed-scheme/private/type-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss index e7554d2265..1f30170540 100644 --- a/collects/typed-scheme/private/type-effect-printer.ss +++ b/collects/typed-scheme/private/type-effect-printer.ss @@ -110,6 +110,7 @@ [(Pair: l r) (fp "(Pair ~a ~a)" l r)] [(F: nm) (fp "~a" nm)] [(Values: (list v ...)) (fp "~a" (cons 'values v))] + [(ValuesDots: v dty dbound) (fp "~a" (cons 'values (append v (list dty '... dbound))))] [(Param: in out) (if (equal? in out) (fp "(Parameter ~a)" in) diff --git a/collects/typed-scheme/private/type-rep.ss b/collects/typed-scheme/private/type-rep.ss index 12d80c3fc3..02b59e3f96 100644 --- a/collects/typed-scheme/private/type-rep.ss +++ b/collects/typed-scheme/private/type-rep.ss @@ -111,9 +111,6 @@ (map free-vars* (append thn-eff els-eff))))) (combine-frees (append (map flip-variances (map free-idxs* (append (if rest (list rest) null) dom))) (match drest - #;[(cons t (? number? bnd)) - (let ([vs (free-idxs* t)]) - (list (flip-variances vs)))] [(cons t bnd) (list (flip-variances (free-idxs* t)))] [_ null]) (list (free-idxs* rng)) @@ -150,6 +147,11 @@ (combine-frees (map free-idxs* types))] [#:fold-rhs (*Values (map type-rec-id types))]) +(dt ValuesDots (types dty dbound) + [#:frees (combine-frees (map free-vars* (cons dty types))) + (combine-frees (map free-idxs* (cons dty types)))] + [#:fold-rhs (*ValuesDots (map type-rec-id types) (type-rec-id dty) dbound)]) + ;; in : Type ;; out : Type (dt Param (in out)) @@ -301,6 +303,10 @@ #f) (map (lambda (e) (sub-eff sb e)) thn-eff) (map (lambda (e) (sub-eff sb e)) els-eff))] + [#:ValuesDots tys dty dbound + (*ValuesDots (map sb tys) + (sb dty) + (if (eq? dbound name) (+ count outer) dbound))] [#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))] [#:PolyDots n body* (let ([body (remove-scopes n body*)]) @@ -341,6 +347,11 @@ #f) (map (lambda (e) (sub-eff sb e)) thn-eff) (map (lambda (e) (sub-eff sb e)) els-eff))] + [#:ValuesDots tys dty dbound + (*ValuesDots (map sb tys) + (sb dty) + + (if (eqv? dbound (+ count outer)) (F-n image) dbound))] [#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))] [#:PolyDots n body* (let ([body (remove-scopes n body*)]) diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss index d6e191f1c8..08a022b6ef 100644 --- a/collects/typed-scheme/private/type-utils.ss +++ b/collects/typed-scheme/private/type-utils.ss @@ -7,6 +7,7 @@ (only-in "free-variance.ss" combine-frees) mzlib/plt-match scheme/list + mzlib/trace (for-syntax scheme/base)) (provide fv fv/list @@ -46,7 +47,12 @@ (and rest (sb rest)) (and drest (cons (sb (car drest)) (cdr drest))) (map (lambda (e) (sub-eff sb e)) thn-eff) - (map (lambda (e) (sub-eff sb e)) els-eff)))]) + (map (lambda (e) (sub-eff sb e)) els-eff)))] + [#:ValuesDots types dty dbound + (begin + (when (eq? name dbound) + (int-err "substitute used on ... variable ~a in type ~a" name target)) + (make-ValuesDots (map sb types) (sb dty) dbound))]) target)) ;; substitute-dots : Listof[Type] Option[type] Name Type -> Type @@ -54,6 +60,15 @@ (define (sb t) (substitute-dots images rimage name t)) (if (hash-ref (free-vars* target) name #f) (type-case sb target + [#:ValuesDots types dty dbound + (if (eq? name dbound) + (make-Values + (append + (map sb types) + ;; We need to recur first, just to expand out any dotted usages of this. + (let ([expanded (sb dty)]) + (map (lambda (img) (substitute img name expanded)) images)))) + (make-ValuesDots (map sb types) (sb dty) dbound))] [#:arr dom rng rest drest thn-eff els-eff (if (and (pair? drest) (eq? name (cdr drest))) @@ -81,6 +96,10 @@ (define (sb t) (substitute-dotted image image-bound name t)) (if (hash-ref (free-vars* target) name #f) (type-case sb target + [#:ValuesDots types dty dbound + (make-ValuesDots (map sb types) + (sb dty) + (if (eq? name dbound) image-bound dbound))] [#:F name* (if (eq? name* name) image @@ -94,7 +113,9 @@ (if (eq? name (cdr drest)) image-bound (cdr drest)))) (map (lambda (e) (sub-eff sb e)) thn-eff) (map (lambda (e) (sub-eff sb e)) els-eff))]) - target)) + target)) + +(trace substitute-dots) ;; substitute many variables ;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]] diff --git a/collects/typed-scheme/values-dots-test.ss b/collects/typed-scheme/values-dots-test.ss new file mode 100644 index 0000000000..985f298481 --- /dev/null +++ b/collects/typed-scheme/values-dots-test.ss @@ -0,0 +1,11 @@ +#lang typed-scheme + +(require "private/extra-procs.ss") + + +(call-with-values (lambda () (values 1 2)) (lambda: ([x : Number] [y : Number]) (+ x y))) + +(#{call-with-values* @ Integer Integer Integer} (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y))) + + +(call-with-values* (lambda () (values 1 2)) (lambda: ([x : Integer] [y : Integer]) (+ x y)))