diff --git a/collects/typed-racket/typecheck/check-below.rkt b/collects/typed-racket/typecheck/check-below.rkt index c10185ca..c11c9c4b 100644 --- a/collects/typed-racket/typecheck/check-below.rkt +++ b/collects/typed-racket/typecheck/check-below.rkt @@ -12,13 +12,19 @@ (only-in srfi/1 split-at)) (provide/cond-contract - [check-below (-->d ([s (-or/c Type/c tc-results?)] [t (-or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])]) + [check-below (-->d ([s (-or/c Type/c tc-results?)] [t (-or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])] + [cond-check-below (-->d ([s (-or/c Type/c tc-results?)] [t (-or/c #f Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])]) (define (print-object o) (match o [(Empty:) "no object"] [_ (format "object ~a" o)])) +;; If expected is #f, then just return tr1 +;; else behave as check-below +(define (cond-check-below tr1 expected) + (if expected (check-below tr1 expected) tr1)) + ;; check-below : (/\ (Results Type -> Result) ;; (Results Results -> Result) ;; (Type Results -> Type) diff --git a/collects/typed-racket/typecheck/tc-app.rkt b/collects/typed-racket/typecheck/tc-app.rkt index c3ceb05c..25d3fd23 100644 --- a/collects/typed-racket/typecheck/tc-app.rkt +++ b/collects/typed-racket/typecheck/tc-app.rkt @@ -60,23 +60,23 @@ (match* ((single-value v1) (single-value v2)) [((tc-result1: t _ o) (tc-result1: (Value: (? ok? val)))) (ret -Boolean - (-FS (-filter-at (-val val) o) - (-not-filter-at (-val val) o)))] + (-FS (-filter-at (-val val) o) + (-not-filter-at (-val val) o)))] [((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o)) (ret -Boolean - (-FS (-filter-at (-val val) o) - (-not-filter-at (-val val) o)))] + (-FS (-filter-at (-val val) o) + (-not-filter-at (-val val) o)))] [((tc-result1: t _ o) (or (and (? (lambda _ (free-identifier=? #'member comparator))) - (tc-result1: (app untuple (list (and ts (Value: _)) ...)))) - (and (? (lambda _ (free-identifier=? #'memv comparator))) - (tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...)))) - (and (? (lambda _ (free-identifier=? #'memq comparator))) - (tc-result1: (app untuple (list (and ts (Value: (? eq?-able))) ...)))))) + (tc-result1: (app untuple (list (and ts (Value: _)) ...)))) + (and (? (lambda _ (free-identifier=? #'memv comparator))) + (tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...)))) + (and (? (lambda _ (free-identifier=? #'memq comparator))) + (tc-result1: (app untuple (list (and ts (Value: (? eq?-able))) ...)))))) (let ([ty (apply Un ts)]) (ret (Un (-val #f) t) - (-FS (-filter-at ty o) - (-not-filter-at ty o))))] + (-FS (-filter-at ty o) + (-not-filter-at ty o))))] [(_ _) (ret -Boolean)])) @@ -257,8 +257,7 @@ (let* ([infer-t (or (type-annotation f #:infer #t) (find-annotation #'(begin . body*) f))]) (if infer-t - (begin (check-below (tc-expr/t ac) infer-t) - infer-t) + (check-below (tc-expr/t ac) infer-t) (generalize (tc-expr/t ac)))))]) (add-typeof-expr lam (tc/rec-lambda/check form args body lp ts expected)) expected)])) @@ -324,15 +323,13 @@ [_ #f]))]) (cond [(not ival) (check-below e-t -Integer) - (if expected - (check-below (ret (apply Un flds)) expected) - (ret (apply Un flds)))] + (cond-check-below (ret (apply Un flds)) expected)] [(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length flds)))) (let ([result (if (list-ref muts ival) (ret (list-ref flds ival)) ;; FIXME - could do something with paths here (ret (list-ref flds ival)))]) - (if expected (check-below result expected) result))] + (cond-check-below result expected))] [(not (and (integer? ival) (exact? ival))) (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) "expected exact integer for struct index, but got ~a" ival)] @@ -365,9 +362,7 @@ (match e-t [(tc-result1: t) t]))] [(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length flds)))) (tc-expr/check #'val (ret (list-ref flds ival))) - (if expected - (check-below (ret -Void) expected) - (ret -Void))] + (cond-check-below (ret -Void) expected)] [(not (and (integer? ival) (exact? ival))) (single-value #'val) (tc-error/expr @@ -391,74 +386,68 @@ v e:expr) (let ([e-t (single-value #'e)]) (let loop ((v-t (single-value #'v))) - (match v-t + (match v-t [(tc-result1: (and t (HeterogenousVector: es))) - (let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f]) - (match e-t - [(tc-result1: (Value: (? number? i))) i] - [_ #f]))]) - (cond [(not ival) - (check-below e-t -Integer) - (if expected - (check-below (ret (apply Un es)) expected) - (ret (apply Un es)))] - [(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length es)))) - (if expected - (check-below (ret (list-ref es ival)) expected) - (ret (list-ref es ival)))] - [(not (and (integer? ival) (exact? ival))) - (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) + (let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f]) + (match e-t + [(tc-result1: (Value: (? number? i))) i] + [_ #f]))]) + (cond [(not ival) + (check-below e-t -Integer) + (cond-check-below (ret (apply Un es)) expected)] + [(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length es)))) + (cond-check-below (ret (list-ref es ival)) expected)] + [(not (and (integer? ival) (exact? ival))) + (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) "expected exact integer for vector index, but got ~a" ival)] - [(< ival 0) - (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) + [(< ival 0) + (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) "index ~a too small for vector ~a" ival t)] - [(not (<= ival (sub1 (length es)))) - (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) + [(not (<= ival (sub1 (length es)))) + (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) "index ~a too large for vector ~a" ival t)]))] - [(tc-result1: (? needs-resolving? e) f o) - (loop (ret (resolve-once e) f o))] - [v-ty - (let ([arg-tys (list v-ty e-t)]) - (tc/funapp #'op #'(v e) (single-value #'op) arg-tys expected))])))] + [(tc-result1: (? needs-resolving? e) f o) + (loop (ret (resolve-once e) f o))] + [v-ty + (let ([arg-tys (list v-ty e-t)]) + (tc/funapp #'op #'(v e) (single-value #'op) arg-tys expected))])))] [(#%plain-app (~and op:normal-op (~or (~literal vector-set!) (~literal unsafe-vector-set!) (~literal unsafe-vector*-set!))) v e:expr val:expr) (let ([e-t (single-value #'e)]) (let loop ((v-t (single-value #'v))) - (match v-t + (match v-t [(tc-result1: (and t (HeterogenousVector: es))) - (let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f]) - (match e-t - [(tc-result1: (Value: (? number? i))) i] - [_ #f]))]) - (cond [(not ival) - (tc-error/expr - #:stx #'e #:return (or expected (ret -Void)) - "expected statically known index for heterogeneous vector, but got ~a" - (match e-t [(tc-result1: t) t]))] - [(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length es)))) - (tc-expr/check #'val (ret (list-ref es ival))) - (if expected - (check-below (ret -Void) expected) - (ret -Void))] - [(not (and (integer? ival) (exact? ival))) - (single-value #'val) - (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) + (let ([ival (or (syntax-parse #'e [((~literal quote) i:number) (syntax-e #'i)] [_ #f]) + (match e-t + [(tc-result1: (Value: (? number? i))) i] + [_ #f]))]) + (cond [(not ival) + (tc-error/expr + #:stx #'e #:return (or expected (ret -Void)) + "expected statically known index for heterogeneous vector, but got ~a" + (match e-t [(tc-result1: t) t]))] + [(and (integer? ival) (exact? ival) (<= 0 ival (sub1 (length es)))) + (tc-expr/check #'val (ret (list-ref es ival))) + (cond-check-below (ret -Void) expected)] + [(not (and (integer? ival) (exact? ival))) + (single-value #'val) + (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) "expected exact integer for vector index, but got ~a" ival)] - [(< ival 0) - (single-value #'val) - (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) + [(< ival 0) + (single-value #'val) + (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) "index ~a too small for vector ~a" ival t)] - [(not (<= ival (sub1 (length es)))) - (single-value #'val) - (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) + [(not (<= ival (sub1 (length es)))) + (single-value #'val) + (tc-error/expr #:stx #'e #:return (or expected (ret (Un))) "index ~a too large for vector ~a" ival t)]))] - [(tc-result1: (? needs-resolving? e) f o) - (loop (ret (resolve-once e) f o))] - [v-ty - (let ([arg-tys (list v-ty e-t (single-value #'val))]) - (tc/funapp #'op #'(v e val) (single-value #'op) arg-tys expected))])))] + [(tc-result1: (? needs-resolving? e) f o) + (loop (ret (resolve-once e) f o))] + [v-ty + (let ([arg-tys (list v-ty e-t (single-value #'val))]) + (tc/funapp #'op #'(v e val) (single-value #'op) arg-tys expected))])))] [(#%plain-app (~and op:normal-op (~or (~literal vector-immutable) (~literal vector))) args:expr ...) (let loop ([expected expected]) (match expected @@ -496,15 +485,14 @@ (ret (make-HeterogenousVector (map (lambda (x) (generalize (tc-expr/t x))) (syntax->list #'(args ...))))) expected)])] - - ;; since vectors are mutable, if there is no expected type, + + ;; since vectors are mutable, if there is no expected type, ;; we want to generalize the element type [(or #f (tc-result1: _)) - ((if expected - (lambda (t) (check-below t expected)) - values) + (cond-check-below (ret (make-HeterogenousVector (map (lambda (x) (generalize (tc-expr/t x))) - (syntax->list #'(args ...))))))] + (syntax->list #'(args ...))))) + expected)] [_ (int-err "bad expected: ~a" expected)]))] ;; since vectors are mutable, if there is no expected type, ;; we want to generalize the element type @@ -752,9 +740,7 @@ [_ (match (single-value #'arg) [(tc-result1: (List: ts)) - (if expected - (check-below (ret (-Tuple (reverse ts))) expected) - (ret (-Tuple (reverse ts))))] + (cond-check-below (ret (-Tuple (reverse ts))) expected)] [arg-ty (tc/funapp #'reverse #'(arg) (single-value #'reverse) (list arg-ty) expected)])])] ;; inference for ((lambda diff --git a/collects/typed-racket/typecheck/tc-expr-unit.rkt b/collects/typed-racket/typecheck/tc-expr-unit.rkt index 1110867a..93244d34 100644 --- a/collects/typed-racket/typecheck/tc-expr-unit.rkt +++ b/collects/typed-racket/typecheck/tc-expr-unit.rkt @@ -121,10 +121,8 @@ [vs (hash-map h (lambda (x y) (tc-literal y)))]) (make-Hashtable (generalize (apply Un ks)) (generalize (apply Un vs))))])] [_ Univ])) - - (if expected - (check-below r expected) - r)) + + (cond-check-below r expected)) ;; do-inst : syntax type -> type @@ -497,9 +495,7 @@ (let* ([ftype (cond [(assq s methods) => cadr] [else (tc-error/expr "send: method ~a not understood by class ~a" s c)])] [ret-ty (tc/funapp rcvr args (ret ftype) (map tc-expr (syntax->list args)) expected)] - [retval (if expected - (begin (check-below ret-ty expected) expected) - ret-ty)]) + [retval (cond-check-below ret-ty expected)]) (add-typeof-expr form retval) retval)] [(tc-result1: t) (int-err "non-symbol methods not supported by Typed Racket: ~a" t)])] diff --git a/collects/typed-racket/typecheck/tc-if.rkt b/collects/typed-racket/typecheck/tc-if.rkt index f70a1b89..a94019ae 100644 --- a/collects/typed-racket/typecheck/tc-if.rkt +++ b/collects/typed-racket/typecheck/tc-if.rkt @@ -92,12 +92,12 @@ [object (if (object-equal? o2 o3) o2 (make-Empty))]) ;(printf "result filter is: ~a\n" filter) (ret type filter object))))]) - (if expected (check-below r expected) r))] + (cond-check-below r expected))] ;; special case if one of the branches is unreachable [(and (= 1 (length us)) (type-equal? (car us) (Un))) - (if expected (check-below (ret ts fs2 os2) expected) (ret ts fs2 os2))] + (cond-check-below (ret ts fs2 os2) expected)] [(and (= 1 (length ts)) (type-equal? (car ts) (Un))) - (if expected (check-below (ret us fs3 os3) expected) (ret us fs3 os3))] + (cond-check-below (ret us fs3 os3) expected)] ;; otherwise, error [else (tc-error/expr #:return (ret (or expected Err)) diff --git a/collects/typed-racket/typecheck/tc-lambda-unit.rkt b/collects/typed-racket/typecheck/tc-lambda-unit.rkt index d2ca1f83..ef3b69e2 100644 --- a/collects/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/collects/typed-racket/typecheck/tc-lambda-unit.rkt @@ -271,9 +271,8 @@ (define (tc/mono-lambda/type formals bodies expected) (define t (make-Function (map lam-result->type (tc/mono-lambda formals bodies expected)))) - (if expected - (and (check-below (ret t true-filter) expected) t) - t)) + (cond-check-below (ret t true-filter) expected) + t) (define (plambda-prop stx) (define d (syntax-property stx 'typechecker:plambda)) @@ -332,10 +331,7 @@ ;(printf "plambda: ~a ~a ~a \n" literal-tvars new-tvars ty) (make-Poly tvars ty))])] [(tc-result1: t) - (unless (check-below (tc/plambda form formals bodies #f) t) - (tc-error/expr #:return expected - "Expected a value of type ~a, but got a polymorphic function." t)) - t] + (check-below (tc/plambda form formals bodies #f) t)] [_ (int-err "not a good expected value: ~a" expected)])) ;; typecheck a sequence of case-lambda clauses, which is possibly polymorphic