diff --git a/collects/typed-scheme/private/check-subforms-unit.ss b/collects/typed-scheme/private/check-subforms-unit.ss index 3b3a5caeed..55cb87616a 100644 --- a/collects/typed-scheme/private/check-subforms-unit.ss +++ b/collects/typed-scheme/private/check-subforms-unit.ss @@ -38,7 +38,7 @@ (define body-ty #f) (define (get-result-ty t) (match t - [(Function: (list (arr: _ rngs _ _ _) ...)) (apply Un rngs)] + [(Function: (list (arr: _ rngs #f _ _ _) ...)) (apply Un rngs)] [_ (tc-error "Internal error in get-result-ty: not a function type: ~n~a" t)])) (let loop ([form form]) (parameterize ([current-orig-stx form]) diff --git a/collects/typed-scheme/private/free-variance.ss b/collects/typed-scheme/private/free-variance.ss index e032900400..006f8a1ad8 100644 --- a/collects/typed-scheme/private/free-variance.ss +++ b/collects/typed-scheme/private/free-variance.ss @@ -1,22 +1,25 @@ #lang scheme/base (require (for-syntax scheme/base) + "tc-utils.ss" mzlib/etc) ;; this file contains support for calculating the free variables/indexes of types ;; actual computation is done in rep-utils.ss and type-rep.ss -(define-values (Covariant Contravariant Invariant Constant) +(define-values (Covariant Contravariant Invariant Constant Dotted) (let () (define-struct Variance () #:inspector #f) (define-struct (Covariant Variance) () #:inspector #f) (define-struct (Contravariant Variance) () #:inspector #f) (define-struct (Invariant Variance) () #:inspector #f) (define-struct (Constant Variance) () #:inspector #f) - (values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant)))) + ;; not really a variance, but is disjoint with the others + (define-struct (Dotted Variance) () #:inspector #f) + (values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted)))) -(provide Covariant Contravariant Invariant Constant) +(provide Covariant Contravariant Invariant Constant Dotted) ;; hashtables for keeping track of free variables and indexes (define index-table (make-weak-hasheq)) @@ -39,6 +42,8 @@ (define (combine-var v w) (cond [(eq? v w) v] + [(or (eq? v Dotted) (eq? w Dotted)) + (int-err "Cannot combine Dotted w/ not Dotted: ~a ~a" v w)] [(eq? v Constant) w] [(eq? w Constant) v] [else Invariant])) @@ -54,6 +59,12 @@ freess) ht) +;; given a set of free variables, remove bound, add bound ... +(define (fix-bound vs bound) + (define vs* (hash-map* (lambda (k v) v) vs)) + (hash-remove! vs* bound) + (hash-set! vs* bound (cons bound Dotted))) + ;; frees -> frees (define (flip-variances vs) (hash-map* @@ -89,7 +100,8 @@ (when (< k n) (hash-remove! new-ht k)))) new-ht) -(provide combine-frees flip-variances without-below unless-in-table var-table index-table empty-hash-table) +(provide combine-frees flip-variances without-below unless-in-table var-table index-table empty-hash-table + fix-bound) (define-syntax (unless-in-table stx) (syntax-case stx () diff --git a/collects/typed-scheme/private/infer-ops.ss b/collects/typed-scheme/private/infer-ops.ss index 33fcbddd03..dec53a6473 100644 --- a/collects/typed-scheme/private/infer-ops.ss +++ b/collects/typed-scheme/private/infer-ops.ss @@ -37,7 +37,7 @@ [#:Param in out (make-Param (var-demote in V) (vp out))] - [#:arr dom rng rest thn els + [#:arr dom rng rest #f thn els (if (apply V-in? V (append thn els)) (make-top-arr) @@ -61,7 +61,7 @@ [#:Param in out (make-Param (var-promote in V) (vd out))] - [#:arr dom rng rest thn els + [#:arr dom rng rest #f thn els (if (apply V-in? V (append thn els)) (make-arr null (Un) Univ null null) (make-arr (for/list ([d dom]) (var-promote d V)) @@ -238,7 +238,7 @@ (for*/list ([t-arr t-arr] [s-arr s-arr]) (with-handlers ([exn:infer? (lambda (_) #f)]) (match* (t-arr s-arr) - [((arr: ts t t-rest t-thn-eff t-els-eff) (arr: ss s s-rest s-thn-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 ts))] diff --git a/collects/typed-scheme/private/infer.ss b/collects/typed-scheme/private/infer.ss index 295c38599c..c4ac9a440a 100644 --- a/collects/typed-scheme/private/infer.ss +++ b/collects/typed-scheme/private/infer.ss @@ -320,7 +320,7 @@ (cond [(and (null? t-arr) (null? s-arr)) mapping] [(or (null? t-arr) (null? s-arr)) (unmatch!)] [else (match (list (car t-arr) (car s-arr)) - [(list (arr: ts t t-rest t-thn-eff t-els-eff) (arr: ss s s-rest s-thn-eff s-els-eff)) + [(list (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))) (infer/int/list (cons t-rest ts) (cons s-rest ss) mapping (swap flag))] @@ -360,7 +360,7 @@ [els-mapping (infer/int/list/eff (apply append t-els-eff) (apply append s-els-eff) mapping flag)]) (U (U arg-mapping ret-mapping) (U thn-mapping els-mapping))))] ;; here, we try to handle a case-lambda as the argument to a polymorphic function - [(list (Function: ftys) (and t (Function: (list (arr: ss s s-rest s-thn-eff s-els-eff))))) + [(list (Function: ftys) (and t (Function: (list (arr: ss s s-rest #f s-thn-eff s-els-eff))))) (=> unmatch) (when (= 1 (length ftys)) (unmatch)) ;; we should have handled this case already (or @@ -371,7 +371,7 @@ (infer/int (make-Function (list fty)) t mapping flag))) ftys) (fail!))] - [(list (and t (Function: (list (arr: ss s s-rest s-thn-eff s-els-eff)))) (Function: ftys)) + [(list (and t (Function: (list (arr: ss s s-rest #f s-thn-eff s-els-eff)))) (Function: ftys)) (=> unmatch) (when (= 1 (length ftys)) (unmatch)) ;; we should have handled this case already (or diff --git a/collects/typed-scheme/private/rep-utils.ss b/collects/typed-scheme/private/rep-utils.ss index 23227f283d..e3cf76e2d1 100644 --- a/collects/typed-scheme/private/rep-utils.ss +++ b/collects/typed-scheme/private/rep-utils.ss @@ -144,7 +144,7 @@ (hash-set! var-table v fvs) (hash-set! index-table v fis)) v)))])]) - #'(begin + #`(begin (define-struct (nm parent) flds #:inspector #f) (define-match-expander ex (lambda (s) @@ -152,7 +152,7 @@ (syntax-case s () [(__ . fs) (quasisyntax/loc s (struct nm #, (syntax/loc #'fs (_ . fs))))])))) (begin-for-syntax - (hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs))) + (hash-set! ht-stx 'kw-stx (list #'ex #'flds bfs-fold-rhs #'#,stx))) intern provides frees)))]))) diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss index 91f0accfb1..5f7e3595be 100644 --- a/collects/typed-scheme/private/subtype.ss +++ b/collects/typed-scheme/private/subtype.ss @@ -99,10 +99,10 @@ (match (list s t) ;; top for functions is above everything [(list _ (top-arr:)) A0] - [(list (arr: s1 s2 #f thn-eff els-eff) (arr: t1 t2 #f thn-eff els-eff)) + [(list (arr: s1 s2 #f #f thn-eff els-eff) (arr: t1 t2 #f #f thn-eff els-eff)) (let ([A1 (subtypes* A0 t1 s1)]) (subtype* A1 s2 t2))] - [(list (arr: s1 s2 s3 thn-eff els-eff) (arr: t1 t2 t3 thn-eff* els-eff*)) + [(list (arr: s1 s2 s3 #f thn-eff els-eff) (arr: t1 t2 t3 #f thn-eff* els-eff*)) (unless (or (and (null? thn-eff*) (null? els-eff*)) (and (effects-equal? thn-eff thn-eff*) diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss index dd716d5867..d6af97670c 100644 --- a/collects/typed-scheme/private/tc-app-unit.ss +++ b/collects/typed-scheme/private/tc-app-unit.ss @@ -132,7 +132,7 @@ (define (printable dom rst) (list dom rst '..)) (match f-ty - [(tc-result: (Function: (list (arr: doms rngs rests thn-effs els-effs) ..1))) + [(tc-result: (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1))) (let loop ([doms* doms] [rngs* rngs] [rests* rests]) (cond [(null? doms*) (if (and (not (null? doms)) (null? (cdr doms))) @@ -148,14 +148,14 @@ [(and (subtypes arg-tys (car doms*)) (car rests*) (subtype tail-ty (make-Listof (car rests*)))) (ret (car rngs*))] [else (loop (cdr doms*) (cdr rngs*) (cdr rests*))]))] - [(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests thn-effs els-effs) ..1)))) + [(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1)))) (for-each (lambda (x) (unless (not (Poly? x)) (tc-error "Polymorphic argument ~a to polymorphic function in apply not allowed" x))) arg-tys0) (let loop ([doms* doms] [rngs* rngs] [rests* rests]) (cond [(null? doms*) (match f-ty - [(tc-result: (Poly-names: vars (Function: (list (arr: doms rngs rests thn-effs els-effs) ..1)))) + [(tc-result: (Poly-names: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1)))) (cond [(null? doms) (int-err "how could doms be null: ~a ~a" doms f-ty)] [(= 1 (length doms)) @@ -223,7 +223,7 @@ [_ (tc-error/expr #:return (ret (Un)) "Wrong number of arguments to parameter - expected 0 or 1, got ~a" (length argtypes))])] - [(tc-result: (Function: (list (arr: doms rngs rests latent-thn-effs latent-els-effs) ..1)) thn-eff els-eff) + [(tc-result: (Function: (list (arr: doms rngs rests #f latent-thn-effs latent-els-effs) ..1)) thn-eff els-eff) (if (= 1 (length doms)) (let-values ([(thn-eff els-eff) (tc-args argtypes arg-thn-effs arg-els-effs (car doms) (car rests) @@ -245,7 +245,7 @@ argtypes)] [(subtypes/varargs argtypes (car doms*) (car rests*)) (ret (car rngs))] [else (loop (cdr doms*) (cdr rngs) (cdr rests*))])))] - [(and rft (tc-result: (Poly: vars (Function: (list (arr: doms rngs #f thn-effs els-effs) ...))))) + [(and rft (tc-result: (Poly: vars (Function: (list (arr: doms rngs #f #f thn-effs els-effs) ...))))) ;(printf "Typechecking poly app~nftype: ~a~n" ftype) ;(printf "ftype again: ~a~n" ftype) ;(printf "resolved ftype: ~a : ~a~n" (equal? rft ftype) rft) @@ -256,7 +256,7 @@ argtypes) (let loop ([doms* doms] [rngs* rngs]) (cond [(null? doms*) - (match-let ([(tc-result: (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs #f _ _) ...)))) ftype]) + (match-let ([(tc-result: (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs #f #f _ _) ...)))) ftype]) (if (= 1 (length doms)) (tc-error/expr #:return (ret (Un)) "Polymorphic function could not be applied to arguments:~nExpected: ~a ~nActual: ~a" @@ -290,7 +290,7 @@ )]|# [else (loop (cdr doms*) (cdr rngs*))]))] ;; polymorphic varargs - [(tc-result: (Poly: vars (Function: (list (arr: dom rng rest thn-eff els-eff))))) + [(tc-result: (Poly: vars (Function: (list (arr: dom rng rest #f thn-eff els-eff))))) (for-each (lambda (x) (unless (not (Poly? x)) (tc-error "Polymorphic argument ~a to polymorphic function not allowed" x))) argtypes) @@ -310,7 +310,7 @@ [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-result: (Poly: vars (Function: (list (arr: doms rngs rests #f 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 [(tc-result: (Union: (list (and fs (Function: _)) ...)) e1 e2) @@ -413,7 +413,7 @@ (match-let* ([(tc-result: prod-t) (tc-expr #'prod)] [(tc-result: con-t) (tc-expr #'con)]) (match (list prod-t con-t) - [(list (Function: (list (arr: (list) vals #f _ _))) (Function: (list (arr: dom rng #f _ _)))) + [(list (Function: (list (arr: (list) vals #f #f _ _))) (Function: (list (arr: dom rng #f #f _ _)))) (=> unmatch) (match (list vals dom) [(list (Values: v) (list t ...)) diff --git a/collects/typed-scheme/private/tc-lambda-unit.ss b/collects/typed-scheme/private/tc-lambda-unit.ss index 1cf62f7e17..bcb79ee56e 100644 --- a/collects/typed-scheme/private/tc-lambda-unit.ss +++ b/collects/typed-scheme/private/tc-lambda-unit.ss @@ -132,10 +132,10 @@ (let loop ([expected expected]) (match expected [(Mu: _ _) (loop (unfold expected))] - [(Function: (list (arr: args ret rest _ _))) + [(Function: (list (arr: args ret rest #f _ _))) (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest) expected] - [(Function: (list (arr: argss rets rests _ _) ...)) + [(Function: (list (arr: argss rets rests #f _ _) ...)) (for ([args argss] [ret rets] [rest rests]) (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest)) expected] diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss index 53aea61515..fed4514fd4 100644 --- a/collects/typed-scheme/private/type-contract.ss +++ b/collects/typed-scheme/private/type-contract.ss @@ -80,13 +80,13 @@ (define (f a) (define-values (dom* rngs* rst) (match a - [(arr: dom (Values: rngs) #f _ _) + [(arr: dom (Values: rngs) #f #f _ _) (values (map t->c dom) (map t->c rngs) #f)] - [(arr: dom rng #f _ _) + [(arr: dom rng #f #f _ _) (values (map t->c dom) (list (t->c rng)) #f)] - [(arr: dom (Values: rngs) rst _ _) + [(arr: dom (Values: rngs) rst #f _ _) (values (map t->c dom) (map t->c rngs) (t->c rst))] - [(arr: dom rng rst _ _) + [(arr: dom rng rst #f _ _) (values (map t->c dom) (list (t->c rng)) (t->c rst))])) (with-syntax ([(dom* ...) dom*] diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss index bbf6008860..22317db1ae 100644 --- a/collects/typed-scheme/private/type-effect-convenience.ss +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -68,8 +68,8 @@ (define make-arr* (case-lambda [(dom rng) (make-arr* dom rng #f (list) (list))] - [(dom rng rest) (make-arr dom rng rest (list) (list))] - [(dom rng rest eff1 eff2) (make-arr dom rng rest eff1 eff2)])) + [(dom rng rest) (make-arr dom rng rest #f (list) (list))] + [(dom rng rest eff1 eff2) (make-arr dom rng rest #f eff1 eff2)])) (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-effect-printer.ss b/collects/typed-scheme/private/type-effect-printer.ss index 22cccaab76..c2a2d940db 100644 --- a/collects/typed-scheme/private/type-effect-printer.ss +++ b/collects/typed-scheme/private/type-effect-printer.ss @@ -46,11 +46,13 @@ (match a [(top-arr:) (fp "Procedure")] - [(arr: dom rng rest thn-eff els-eff) + [(arr: dom rng rest drest thn-eff els-eff) (fp "(") (for-each (lambda (t) (fp "~a " t)) dom) (when rest - (fp "~a .. " rest)) + (fp "~a* " rest)) + (when drest + (fp "~a ..." drest)) (fp "-> ~a" rng) (unless (and (null? thn-eff) (null? els-eff)) (fp " : ~a ~a" thn-eff els-eff)) @@ -96,7 +98,7 @@ [(list) (fp "(case-lambda)")] [(list a) (print-arr a)] [(list a ...) (fp "(case-lambda ") (for-each print-arr a) (fp ")")]))] - [(arr: _ _ _ _ _) (print-arr c)] + [(arr: _ _ _ _ _ _) (print-arr c)] [(Vector: e) (fp "(Vectorof ~a)" e)] [(Box: e) (fp "(Box ~a)" e)] [(Union: elems) (fp "~a" (cons 'U elems))] diff --git a/collects/typed-scheme/private/type-rep.ss b/collects/typed-scheme/private/type-rep.ss index 4c36abdf7f..7e88413b72 100644 --- a/collects/typed-scheme/private/type-rep.ss +++ b/collects/typed-scheme/private/type-rep.ss @@ -21,7 +21,7 @@ ;; n is a Name (dt F (n) [#:frees (make-immutable-hasheq (list (cons n Covariant))) empty-hash-table] [#:fold-rhs #:base]) - + ;; id is an Identifier (dt Name (id) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base]) @@ -54,10 +54,19 @@ ;; n is how many variables are bound here ;; body is a Scope - (dt Poly (n body) #:no-provide [#:frees (free-vars* body) (without-below n (free-idxs* body))] + (dt Poly (n body) #:no-provide + [#:frees (free-vars* body) (without-below n (free-idxs* body))] [#:fold-rhs (let ([body* (remove-scopes n body)]) (*Poly n (add-scopes n (type-rec-id body*))))]) + ;; n is how many variables are bound here + ;; there are n-1 'normal' vars and 1 ... var + ;; body is a Scope + (dt PolyDots (n body) #:no-provide + [#:frees (free-vars* body) (without-below n (free-idxs* body))] + [#:fold-rhs (let ([body* (remove-scopes n body)]) + (*PolyDots n (add-scopes n (type-rec-id body*))))]) + ;; pred : identifier ;; cert : syntax certifier (dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base]) @@ -83,24 +92,37 @@ ;; dom : Listof[Type] ;; rng : Type - ;; rest : Type + ;; rest : Option[Type] + ;; drest : Option[Cons[Type,Name or nat]] + ;; rest and drest NOT both true ;; thn-eff : Effect ;; els-eff : Effect ;; arr is NOT a Type - (dt arr (dom rng rest thn-eff els-eff) - [#:frees (combine-frees (append (map flip-variances (map free-vars* dom)) - (map free-vars* (append (list rng) - (if rest (list rest) null) - thn-eff - els-eff)))) - (combine-frees (append (map flip-variances (map free-idxs* dom)) - (map free-idxs* (append (list rng) - (if rest (list rest) null) - thn-eff - els-eff))))] + (dt arr (dom rng rest drest thn-eff els-eff) + [#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null) dom))) + (match drest + [(cons t (? symbol? bnd)) + (let ([vs (free-vars* t)]) + (flip-variances (fix-bound vs bnd)))] + [(cons t bnd) (flip-variances (free-vars* t))] + [_ null]) + (list (free-vars* rng)) + (map make-invariant + (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)]) + (flip-variances (fix-bound vs bnd)))] + [(cons t bnd) (flip-variances (free-idxs* t))] + [_ null]) + (list (free-idxs* rng)) + (map make-invariant + (map free-idxs* (append thn-eff els-eff)))))] [#:fold-rhs (*arr (map type-rec-id dom) (type-rec-id rng) (and rest (type-rec-id rest)) + (and drest (cons (type-rec-id (car drest)) (cdr drest))) (map effect-rec-id thn-eff) (map effect-rec-id els-eff))]) @@ -203,19 +225,22 @@ [(kw #:matcher mtch pats ... expr) (hash-set! ht (syntax-e #'kw) (list #'mtch (syntax/loc cl (pats ...)) - (lambda (tr er) #'expr)))] + (lambda (tr er) #'expr) + cl))] [(kw pats ... expr) (hash-set! ht (syntax-e #'kw) (list (mk-matcher (syntax-e #'kw)) (syntax/loc cl (pats ...)) - (lambda (tr er) #'expr)))])) + (lambda (tr er) #'expr) + cl))])) (define rid #'type-rec-id) (define erid #'effect-rec-id) (define (gen-clause k v) (define match-ex (car v)) (define pats (cadr v)) (define body-f (caddr v)) - (define pat (quasisyntax/loc pats (#,match-ex . #,pats))) - (define cl (quasisyntax/loc match-ex (#,pat #,(body-f rid erid)))) + (define src (cadddr v)) + (define pat (quasisyntax/loc src (#,match-ex . #,pats))) + (define cl (quasisyntax/loc src (#,pat #,(body-f rid erid)))) cl) (syntax-case stx () [(tc rec-id ty [kw pats ... es] ...) @@ -266,6 +291,9 @@ ;; necessary to avoid infinite loops [#:Union elems (*Union (remove-dups (sort (map sb elems) type Type ;; must be applied to a Mu (define (unfold t) @@ -417,21 +493,26 @@ (provide unfold Mu-name: Poly-names: + PolyDots-names: Type-seq Effect-seq Mu-unsafe: Poly-unsafe: - Mu? Poly? + PolyDots-unsafe: + Mu? Poly? PolyDots? arr Type? Effect? Poly-n + PolyDots-n free-vars* type-equal? type-compare type