Added cond-check-below
original commit: 8f98bb6d92aa2aa47910b9aa2cc8301b76f063ed
This commit is contained in:
Eric Dobson
Sam Tobin-Hochstadt
parent
ceb8feedcc
commit
fd7bea8edb
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)])]
|
||||
|
|
|
|||
|
|
@ -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))
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user