diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss index 5f7e3595..04f3c89b 100644 --- a/collects/typed-scheme/private/subtype.ss +++ b/collects/typed-scheme/private/subtype.ss @@ -1,6 +1,6 @@ #lang scheme/base -(require "type-rep.ss" "unify.ss" "type-utils.ss" +(require (except-in "type-rep.ss" sub-eff) "unify.ss" "type-utils.ss" "tc-utils.ss" "effect-rep.ss" "type-comparison.ss" diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss index 22317db1..73c11ef9 100644 --- a/collects/typed-scheme/private/type-effect-convenience.ss +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -69,7 +69,11 @@ (define make-arr* (case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))] [(dom rng rest) (make-arr dom rng rest #f (list) (list))] - [(dom rng rest eff1 eff2) (make-arr dom rng rest #f eff1 eff2)])) + [(dom rng rest eff1 eff2) (make-arr dom rng rest #f eff1 eff2)] + [(dom rng rest drest eff1 eff2) (make-arr dom rng rest drest eff1 eff2)])) + +(define (make-arr-dots dom rng dty dbound) + (make-arr* dom rng #f (cons dty dbound) null null)) (define (make-promise-ty t) (make-Struct (string->uninterned-symbol "Promise") #f (list t) #f #f #'promise? values)) diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss index b82bf64a..a67bc677 100644 --- a/collects/typed-scheme/private/type-utils.ss +++ b/collects/typed-scheme/private/type-utils.ss @@ -10,6 +10,7 @@ (provide fv fv/list substitute + substitute-dots subst-all subst ret @@ -26,7 +27,45 @@ (define (sb t) (substitute image name t)) (if (hash-ref (free-vars* target) name #f) (type-case sb target - [#:F name* (if (eq? name* name) image target)]) + [#:F name* (if (eq? name* name) image target)] + [#:arr dom rng rest drest thn-eff els-eff + (begin + (when (and (pair? drest) + (eq? name (cdr drest))) + (int-err "substitute used on ... variable ~a" name)) + (make-arr (map sb dom) + (sb rng) + (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)))]) + target)) + +;; substitute-dots : Listof[Type] Name Type -> Type +(define (substitute-dots images name target) + (define (sb t) (substitute-dots images name t)) + (if (hash-ref (free-vars* target) name #f) + (type-case sb target + [#:F name* (if (eq? name* name) + (int-err "substitute-dots: got single variable ~a" name*) + target)] + [#:arr dom rng rest drest thn-eff els-eff + (if (and (pair? drest) + (eq? name (cdr drest))) + (make-arr (append + (map sb dom) + (map (lambda (img) (substitute img name (car drest))) images)) + (sb rng) + #f + #f + (map (lambda (e) (sub-eff sb e)) thn-eff) + (map (lambda (e) (sub-eff sb e)) els-eff)) + (make-arr (map sb dom) + (sb rng) + (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)))]) target)) ;; substitute many variables