From 80ed6585fb763c52fe8d406094100502ee5de30e Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sun, 20 Jan 2013 14:49:06 -0800 Subject: [PATCH] Remove tc-results? and other minor improvements. original commit: a2f33f17e900c48fe242d10f86d43a9d2f1ce808 --- collects/typed-racket/base-env/base-env.rkt | 4 +- collects/typed-racket/infer/infer-unit.rkt | 3 +- collects/typed-racket/private/parse-type.rkt | 4 +- .../typed-racket/private/type-annotation.rkt | 9 +++- collects/typed-racket/rep/type-rep.rkt | 51 ++++++++++--------- .../typed-racket/typecheck/check-below.rkt | 13 ++++- .../typecheck/tc-app/tc-app-values.rkt | 2 +- .../typed-racket/typecheck/tc-lambda-unit.rkt | 2 +- .../typed-racket/typecheck/tc-let-unit.rkt | 3 +- .../typecheck/tc-metafunctions.rkt | 2 +- collects/typed-racket/types/base-abbrev.rkt | 7 +-- collects/typed-racket/types/tc-result.rkt | 3 +- 12 files changed, 57 insertions(+), 46 deletions(-) diff --git a/collects/typed-racket/base-env/base-env.rkt b/collects/typed-racket/base-env/base-env.rkt index 70a2aea0..c40abb64 100644 --- a/collects/typed-racket/base-env/base-env.rkt +++ b/collects/typed-racket/base-env/base-env.rkt @@ -2028,7 +2028,9 @@ (-> (-> b) Univ)))] [abort-current-continuation (-polydots (a b d e c) - (->... (list (make-Prompt-Tagof b (->... '() (c c) d))) (c c) e))] + (cl->* + (->... (list (make-Prompt-Tagof b (->... '() (c c) d))) (c c) e) + (->... (list (make-Prompt-Tagof b (->... '() (c c) ManyUniv))) (c c) e)))] [make-continuation-prompt-tag (-poly (a b) (->opt [Sym] (make-Prompt-Tagof a b)))] ;; default-continuation-prompt-tag is defined in "base-contracted.rkt" diff --git a/collects/typed-racket/infer/infer-unit.rkt b/collects/typed-racket/infer/infer-unit.rkt index 19a4fe75..0a94076d 100644 --- a/collects/typed-racket/infer/infer-unit.rkt +++ b/collects/typed-racket/infer/infer-unit.rkt @@ -312,7 +312,7 @@ ;; the index variables from the TOPLAS paper (define/cond-contract (cgen V X Y S T) ((listof symbol?) (listof symbol?) (listof symbol?) - (or/c Values/c ValuesDots?) (or/c Values/c ValuesDots?). -> . cset?) + (or/c Values/c ValuesDots? AnyValues?) (or/c Values/c ValuesDots? AnyValues?) . -> . cset?) ;; useful quick loop (define/cond-contract (cg S T) (Type/c Type/c . -> . cset?) @@ -334,6 +334,7 @@ [(a a) empty] ;; CG-Top [(_ (Univ:)) empty] + [(_ (AnyValues:)) empty] ;; check all non Type/c first so that calling subtype is safe diff --git a/collects/typed-racket/private/parse-type.rkt b/collects/typed-racket/private/parse-type.rkt index 2def7930..a63685b0 100644 --- a/collects/typed-racket/private/parse-type.rkt +++ b/collects/typed-racket/private/parse-type.rkt @@ -21,8 +21,8 @@ (provide/cond-contract [parse-type (syntax? . c:-> . Type/c)] [parse-type/id (syntax? c:any/c . c:-> . Type/c)] - [parse-tc-results (syntax? . c:-> . tc-results?)] - [parse-tc-results/id (syntax? c:any/c . c:-> . tc-results?)]) + [parse-tc-results (syntax? . c:-> . tc-results/c)] + [parse-tc-results/id (syntax? c:any/c . c:-> . tc-results/c)]) (provide star ddd/bound) (define enable-mu-parsing (make-parameter #t)) diff --git a/collects/typed-racket/private/type-annotation.rkt b/collects/typed-racket/private/type-annotation.rkt index c788afb1..b9a312a7 100644 --- a/collects/typed-racket/private/type-annotation.rkt +++ b/collects/typed-racket/private/type-annotation.rkt @@ -117,6 +117,11 @@ (tc-expr/check expr (ret anns)) (let ([ty (tc-expr expr)]) (match ty + [(tc-any-results:) + (ret + (tc-error/expr + "Expression should produce ~a values, but produces an unknown number of values" + (length stxs)))] [(tc-results: tys fs os) (if (not (= (length stxs) (length tys))) (begin @@ -127,8 +132,8 @@ (combine-results (for/list ([stx stxs] [ty tys] [a anns] [f fs] [o os]) (cond [a (check-type stx ty a) (ret a f o)] - ;; mutated variables get generalized, so that we don't infer too small a type - [(is-var-mutated? stx) (ret (generalize ty) f o)] + ;; mutated variables get generalized, so that we don't infer too small a type + [(is-var-mutated? stx) (ret (generalize ty) f o)] [else (ret ty f o)]))))]))))])) ;; check that e-type is compatible with ty in context of stx diff --git a/collects/typed-racket/rep/type-rep.rkt b/collects/typed-racket/rep/type-rep.rkt index 1f102661..86299155 100644 --- a/collects/typed-racket/rep/type-rep.rkt +++ b/collects/typed-racket/rep/type-rep.rkt @@ -15,6 +15,30 @@ (define name-table (make-weak-hasheq)) +(define Type/c? + (λ (e) + (and (Type? e) + (not (Scope? e)) + (not (arr? e)) + (not (fld? e)) + (not (Values? e)) + (not (ValuesDots? e)) + (not (AnyValues? e)) + (not (Result? e))))) + +;; (or/c Type/c Values? Results?) +;; Anything that can be treated as a Values by sufficient expansion +(define Values/c? + (λ (e) + (and (Type? e) + (not (Scope? e)) + (not (arr? e)) + (not (fld? e)) + (not (ValuesDots? e)) + (not (AnyValues? e))))) + +(define Type/c (flat-named-contract 'Type Type/c?)) +(define Values/c (flat-named-contract 'Values Values/c?)) ;; Name = Symbol @@ -215,6 +239,8 @@ (combine-frees (map free-idxs* (cons dty rs))))] [#:fold-rhs (*ValuesDots (map type-rec-id rs) (type-rec-id dty) dbound)]) +(define SomeValues/c (or/c Values? AnyValues? ValuesDots?)) + ;; arr is NOT a Type (def-type arr ([dom (listof Type/c)] [rng SomeValues/c] @@ -743,31 +769,6 @@ ;(trace subst subst-all) -(define Type/c? - (λ (e) - (and (Type? e) - (not (Scope? e)) - (not (arr? e)) - (not (fld? e)) - (not (Values? e)) - (not (ValuesDots? e)) - (not (AnyValues? e)) - (not (Result? e))))) - -;; (or/c Type/c Values? Results?) -;; Anything that can be treated as a Values by sufficient expansion -(define Values/c? - (λ (e) - (and (Type? e) - (not (Scope? e)) - (not (arr? e)) - (not (fld? e)) - (not (ValuesDots? e)) - (not (AnyValues? e))))) - -(define Type/c (flat-named-contract 'Type Type/c?)) -(define Values/c (flat-named-contract 'Values Values/c?)) -(define SomeValues/c (or/c Values? AnyValues? ValuesDots?)) (provide Mu-name: diff --git a/collects/typed-racket/typecheck/check-below.rkt b/collects/typed-racket/typecheck/check-below.rkt index 92b87f4a..dbaf9cdf 100644 --- a/collects/typed-racket/typecheck/check-below.rkt +++ b/collects/typed-racket/typecheck/check-below.rkt @@ -12,8 +12,10 @@ (only-in srfi/1 split-at)) (provide/cond-contract - [check-below (-->d ([s (-or/c Type/c tc-results/c)] [t (-or/c Type/c tc-results/c)]) () [_ (if (Type? s) Type/c tc-results/c)])] - [cond-check-below (-->d ([s (-or/c Type/c tc-results/c)] [t (-or/c #f Type/c tc-results/c)]) () [_ (if (Type? s) Type/c tc-results/c)])]) + [check-below (-->d ([s (-or/c Type/c tc-results/c)] [t (-or/c Type/c tc-results/c)]) () + [_ (if (Type/c? s) Type/c tc-results/c)])] + [cond-check-below (-->d ([s (-or/c Type/c tc-results/c)] [t (-or/c #f Type/c tc-results/c)]) () + [_ (if (Type/c? s) Type/c tc-results/c)])]) (define (print-object o) (match o @@ -103,6 +105,13 @@ (unless (for/and ([t t1] [s t2]) (subtype t s)) (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1))) expected] + [((tc-any-results:) (or (? Type/c? t) (tc-result1: t _ _))) + (tc-error/expr "Expected 1 value, but got unknown number") + expected] + [((tc-any-results:) (tc-results: t2 fs os)) + (tc-error/expr "Expected ~a values, but got unknown number" (length t2)) + expected] + [((tc-result1: t1 f o) (? Type/c? t2)) (unless (subtype t1 t2) (tc-error/expr "Expected ~a, but got ~a" t2 t1)) diff --git a/collects/typed-racket/typecheck/tc-app/tc-app-values.rkt b/collects/typed-racket/typecheck/tc-app/tc-app-values.rkt index 83220ea2..45655ac2 100644 --- a/collects/typed-racket/typecheck/tc-app/tc-app-values.rkt +++ b/collects/typed-racket/typecheck/tc-app/tc-app-values.rkt @@ -27,7 +27,7 @@ ;; we just ignore the values, except that it forces arg to return one value (pattern (values arg) (match expected - [#f (single-value #'arg)] + [(or #f (tc-any-results:)) (single-value #'arg)] [(tc-result1: tp) (single-value #'arg expected)] [(tc-results: ts) diff --git a/collects/typed-racket/typecheck/tc-lambda-unit.rkt b/collects/typed-racket/typecheck/tc-lambda-unit.rkt index 656d7ab2..dd0cfac2 100644 --- a/collects/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/collects/typed-racket/typecheck/tc-lambda-unit.rkt @@ -242,7 +242,7 @@ (match (find-expected expected f*) ;; very conservative -- only do anything interesting if we get exactly one thing that matches [(list) - (if (and (= 1 (length formals*)) (tc-results? expected)) + (if (and (= 1 (length formals*)) (match expected ((tc-results: _) #t) (_ #f))) (tc-error/expr #:return (list (lam-result null null (list #'here Univ) #f (ret (Un)))) "Expected a function of type ~a, but got a function with the wrong arity" (match expected [(tc-result1: t) t])) diff --git a/collects/typed-racket/typecheck/tc-let-unit.rkt b/collects/typed-racket/typecheck/tc-let-unit.rkt index 0f300178..b289831f 100644 --- a/collects/typed-racket/typecheck/tc-let-unit.rkt +++ b/collects/typed-racket/typecheck/tc-let-unit.rkt @@ -29,7 +29,7 @@ (define/cond-contract (do-check expr->type namess results expected-results form exprs body clauses expected #:abstract [abstract null]) (((syntax? syntax? tc-results/c . c:-> . any/c) - (listof (listof identifier?)) (listof tc-results?) (listof tc-results?) + (listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c) syntax? (listof syntax?) syntax? (listof syntax?) (or/c #f tc-results/c)) (#:abstract any/c) . c:->* . @@ -130,7 +130,6 @@ (cond ;; after everything, check the body expressions [(null? names) - ;(if expected (tc-exprs/check (syntax->list body) expected) (tc-exprs (syntax->list body))) (do-check void null null null form null body null expected #:abstract orig-flat-names)] ;; if none of the names bound in the letrec are free vars of this rhs [(not (ormap (lambda (n) (s:member n flat-names bound-identifier=?)) diff --git a/collects/typed-racket/typecheck/tc-metafunctions.rkt b/collects/typed-racket/typecheck/tc-metafunctions.rkt index 9fcdd03d..ae62ddd9 100644 --- a/collects/typed-racket/typecheck/tc-metafunctions.rkt +++ b/collects/typed-racket/typecheck/tc-metafunctions.rkt @@ -13,7 +13,7 @@ (define/cond-contract (abstract-results results arg-names) - (tc-results? (listof identifier?) . -> . SomeValues/c) + (tc-results/c (listof identifier?) . -> . SomeValues/c) (define keys (for/list ([(nm k) (in-indexed arg-names)]) k)) (match results [(tc-any-results:) (make-AnyValues)] diff --git a/collects/typed-racket/types/base-abbrev.rkt b/collects/typed-racket/types/base-abbrev.rkt index fc25dc94..b40f2e1d 100644 --- a/collects/typed-racket/types/base-abbrev.rkt +++ b/collects/typed-racket/types/base-abbrev.rkt @@ -17,12 +17,7 @@ ;A Type that corresponds to the any contract for the ;return type of functions -;FIXME -;This is not correct as Univ is only a single value. -(define ManyUniv Univ) - - - +(define ManyUniv (make-AnyValues)) ;; Char type (needed because of how sequences are checked in subtype) (define -Char (make-Base 'Char #'char? char? #'-Char #f)) diff --git a/collects/typed-racket/types/tc-result.rkt b/collects/typed-racket/types/tc-result.rkt index a5030220..1be7664f 100644 --- a/collects/typed-racket/types/tc-result.rkt +++ b/collects/typed-racket/types/tc-result.rkt @@ -110,7 +110,7 @@ Object?)] [dty Type/c] [dbound symbol?]) - [res tc-results?])]) + [res tc-results/c])]) (define (combine-results tcs) (match tcs @@ -124,7 +124,6 @@ (tc-any-results* tc-any-results))) (provide/cond-contract [combine-results ((listof tc-results?) . -> . tc-results?)] - [tc-result? (any/c . -> . boolean?)] [tc-result-t (tc-result? . -> . Type/c)] [tc-result-equal? (tc-result? tc-result? . -> . boolean?)] [tc-results? (any/c . -> . boolean?)]