Add contract enforcing expected values don't get returned.

original commit: 67805b9f046bfba716d04c3f7395b115250be7d6
This commit is contained in:
Eric Dobson 2014-03-13 21:12:19 -07:00
parent 404fceb7d6
commit 04482d9cc2
7 changed files with 45 additions and 28 deletions

View File

@ -9,12 +9,12 @@
(only-in (types printer) pretty-format-type))
(provide/cond-contract
[check-below (-->i ([s (-or/c Type/c tc-results/c)]
[check-below (-->i ([s (-or/c Type/c full-tc-results/c)]
[t (s) (if (Type/c? s) Type/c tc-results/c)])
[_ (s) (if (Type/c? s) Type/c tc-results/c)])]
[cond-check-below (-->i ([s (-or/c Type/c tc-results/c)]
[_ (s) (if (Type/c? s) Type/c full-tc-results/c)])]
[cond-check-below (-->i ([s (-or/c Type/c full-tc-results/c)]
[t (s) (-or/c #f (if (Type/c? s) Type/c tc-results/c))])
[_ (s) (-or/c #f (if (Type/c? s) Type/c tc-results/c))])]
[_ (s) (-or/c #f (if (Type/c? s) Type/c full-tc-results/c))])]
[type-mismatch (-->* ((-or/c Type/c string?) (-or/c Type/c string?))
((-or/c string? #f))
-any)])

View File

@ -6,13 +6,13 @@
(provide (all-defined-out))
(define-signature tc-expr^
([cond-contracted tc-expr (syntax? . -> . tc-results/c)]
[cond-contracted tc-expr/check (syntax? tc-results/c . -> . tc-results/c)]
([cond-contracted tc-expr (syntax? . -> . full-tc-results/c)]
[cond-contracted tc-expr/check (syntax? tc-results/c . -> . full-tc-results/c)]
[cond-contracted tc-expr/check/t (syntax? tc-results/c . -> . Type/c)]
[cond-contracted tc-body (syntax? . -> . tc-results/c)]
[cond-contracted tc-body/check (syntax? tc-results/c . -> . tc-results/c)]
[cond-contracted tc-body (syntax? . -> . full-tc-results/c)]
[cond-contracted tc-body/check (syntax? tc-results/c . -> . full-tc-results/c)]
[cond-contracted tc-expr/t (syntax? . -> . Type/c)]
[cond-contracted single-value ((syntax?) ((or/c tc-results/c #f)) . ->* . tc-results/c)]))
[cond-contracted single-value ((syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]))
(define-signature check-subforms^
([cond-contracted check-subforms/ignore (syntax? . -> . any)]
@ -20,34 +20,34 @@
[cond-contracted check-subforms/with-handlers/check (syntax? tc-results/c . -> . any)]))
(define-signature check-class^
([cond-contracted check-class (syntax? (or/c tc-results/c #f) . -> . tc-results/c)]))
([cond-contracted check-class (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]))
(define-signature tc-if^
([cond-contracted tc/if-twoarm ((syntax? syntax? syntax?) (tc-results/c) . ->* . tc-results/c)]))
([cond-contracted tc/if-twoarm ((syntax? syntax? syntax?) (tc-results/c) . ->* . full-tc-results/c)]))
(define-signature tc-literal^
([cond-contracted tc-literal (->* (syntax?) ((or/c Type/c #f)) Type/c)]))
(define-signature tc-send^
([cond-contracted tc/send ((syntax? syntax? syntax? syntax?) ((or/c tc-results/c #f)) . ->* . tc-results/c)]))
([cond-contracted tc/send ((syntax? syntax? syntax? syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]))
(define-signature tc-lambda^
([cond-contracted tc/lambda (syntax? syntax? syntax? . -> . tc-results/c)]
[cond-contracted tc/lambda/check (syntax? syntax? syntax? tc-results/c . -> . tc-results/c)]
([cond-contracted tc/lambda (syntax? syntax? syntax? . -> . full-tc-results/c)]
[cond-contracted tc/lambda/check (syntax? syntax? syntax? tc-results/c . -> . full-tc-results/c)]
[cond-contracted tc/rec-lambda/check (syntax? syntax? syntax? (listof Type/c) tc-results/c . -> .
(values tc-results/c tc-results/c))]))
(values full-tc-results/c full-tc-results/c))]))
(define-signature tc-app^
([cond-contracted tc/app (syntax? . -> . tc-results/c)]
[cond-contracted tc/app/check (syntax? tc-results/c . -> . tc-results/c)]
[cond-contracted tc/app-regular (syntax? (or/c tc-results/c #f) . -> . tc-results/c)]))
([cond-contracted tc/app (syntax? . -> . full-tc-results/c)]
[cond-contracted tc/app/check (syntax? tc-results/c . -> . full-tc-results/c)]
[cond-contracted tc/app-regular (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]))
(define-signature tc-apply^
([cond-contracted tc/apply (syntax? syntax? . -> . tc-results/c)]))
([cond-contracted tc/apply (syntax? syntax? . -> . full-tc-results/c)]))
(define-signature tc-let^
([cond-contracted tc/let-values ((syntax? syntax? syntax?) ((or/c #f tc-results/c)) . ->* . tc-results/c)]
[cond-contracted tc/letrec-values ((syntax? syntax? syntax?) ((or/c #f tc-results/c)) . ->* . tc-results/c)]))
([cond-contracted tc/let-values ((syntax? syntax? syntax?) ((or/c #f tc-results/c)) . ->* . full-tc-results/c)]
[cond-contracted tc/letrec-values ((syntax? syntax? syntax?) ((or/c #f tc-results/c)) . ->* . full-tc-results/c)]))
(define-signature tc-dots^
([cond-contracted tc/dots (syntax? . -> . (values Type/c symbol?))]))

View File

@ -16,7 +16,7 @@
[tc/funapp1
((syntax? stx-list? arr? (listof tc-results/c) (or/c #f tc-results/c))
(#:check boolean?)
. ->* . tc-results/c)])
. ->* . full-tc-results/c)])
(define (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t])
(match* (ftype0 argtys)
;; we check that all kw args are optional

View File

@ -53,7 +53,7 @@
(define/cond-contract
(let-loop-check lam lp actuals args body expected)
(syntax? syntax? syntax? syntax? syntax? tc-results/c . --> . tc-results/c)
(syntax? syntax? syntax? syntax? syntax? tc-results/c . --> . full-tc-results/c)
(syntax-parse #`(#,args #,body #,actuals)
#:literal-sets (kernel-literals lambda-literals)
[((val acc ...)

View File

@ -140,7 +140,7 @@
;; the identifier has variable effect
;; tc-id : identifier -> tc-results
(define/cond-contract (tc-id id)
(--> identifier? tc-results/c)
(--> identifier? full-tc-results/c)
(let* ([ty (lookup-type/lexical id)])
(ret ty
(make-FilterSet (-not-filter (-val #f) id)
@ -226,7 +226,7 @@
;; tc-expr/check : syntax tc-results -> tc-results
(define/cond-contract (tc-expr/check/internal form expected)
(--> syntax? tc-results/c tc-results/c)
(--> syntax? tc-results/c full-tc-results/c)
(parameterize ([current-orig-stx form])
;(printf "form: ~a\n" (syntax-object->datum form))
;; the argument must be syntax

View File

@ -6,7 +6,7 @@
(for-syntax syntax/parse racket/base)
(types utils union subtype resolve abbrev
substitute classes)
(typecheck tc-metafunctions tc-app-helper)
(typecheck tc-metafunctions tc-app-helper check-below)
(rep type-rep)
(r:infer infer))
@ -14,7 +14,7 @@
[tc/funapp
(syntax? stx-list? tc-results/c (c:listof tc-results/c)
(c:or/c #f tc-results/c)
. c:-> . tc-results/c)])
. c:-> . full-tc-results/c)])
(define-syntax (handle-clauses stx)
(syntax-parse stx

View File

@ -21,6 +21,22 @@
(or (tc-results? v)
(tc-any-results? v)))
;; Contract to check that values are tc-results/c and do not contain -no-filter or -no-obj.
;; Used to contract the return values of typechecking functions.
(define (full-tc-results/c r)
(match r
[(tc-any-results:) #t]
[(tc-results: _ fs os)
(and
(not (member -no-filter fs))
(not (member -no-obj os)))]
[(tc-results: _ fs os _ _)
(and
(not (member -no-filter fs))
(not (member -no-obj os)))]
[else #f]))
(define-match-expander tc-result:
(syntax-rules ()
[(_ tp fp op) (struct tc-result (tp fp op))]
@ -139,4 +155,5 @@
[rename tc-results-ts* tc-results-ts (tc-results? . c:-> . (c:listof Type/c))]
[tc-result-equal? (tc-result? tc-result? . c:-> . boolean?)]
[tc-results? (c:any/c . c:-> . boolean?)]
[tc-results/c c:flat-contract?])
[tc-results/c c:flat-contract?]
[full-tc-results/c c:flat-contract?])