suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

added the #:pre/name and #:post/name keywords to ->i

Browse Source
This commit is contained in:
Robby Findler 2011-02-25 09:45:21 -06:00
parent 4b68377af1
commit 07a2ace943
4 changed files with 282 additions and 127 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

152
collects/racket/contract/private/arr-i-parse.rkt
View File

@ -19,9 +19,9 @@ code does the parsing and validation of the syntax.
;; args : (listof arg?) ;; args : (listof arg?)
;; rst : (or/c #f arg/res?) ;; rst : (or/c #f arg/res?)
;; pre : (or/c pre/post? #f) ;; pre : (listof pre/post?)
;; ress : (or/c #f (listof eres?) (listof lres?)) ;; ress : (or/c #f (listof eres?) (listof lres?))
;; post : (or/c pre/post? #f) ;; post : (listof pre/post?)
(struct istx (args rst pre ress post) #:transparent) (struct istx (args rst pre ress post) #:transparent)
;; NOTE: the ress field may contain a mixture of eres and lres structs ;; NOTE: the ress field may contain a mixture of eres and lres structs
;; but only temporarily; in that case, a syntax error ;; but only temporarily; in that case, a syntax error
@ -46,7 +46,8 @@ code does the parsing and validation of the syntax.
;; vars : (listof identifier?) ;; vars : (listof identifier?)
;; exp : syntax[expr] ;; exp : syntax[expr]
(struct pre/post (vars exp) #:transparent) ;; str : (or/c #f syntax[expr])
(struct pre/post (vars str exp) #:transparent)
(define (parse-->i stx) (define (parse-->i stx)
(if (identifier? stx) (if (identifier? stx)
@ -105,7 +106,7 @@ code does the parsing and validation of the syntax.
(raise-syntax-error #f (raise-syntax-error #f
(if arg? (if arg?
"an argument cannot depend on a result" "an argument cannot depend on a result"
"the #:pre condition cannot depend on a result") "a #:pre or #:pre/name condition cannot depend on a result")
stx arg-var))))) stx arg-var)))))
;; no dups in the domains ;; no dups in the domains
@ -146,8 +147,8 @@ code does the parsing and validation of the syntax.
(not-range-bound a-vars #t)))) (not-range-bound a-vars #t))))
;; pre-condition variables are all bound, but not to a range variable ;; pre-condition variables are all bound, but not to a range variable
(when (istx-pre istx) (for ([pre (in-list (istx-pre istx))])
(let ([vars (pre/post-vars (istx-pre istx))]) (let ([vars (pre/post-vars pre)])
(ensure-bound vars) (ensure-bound vars)
(not-range-bound vars #f))) (not-range-bound vars #f)))
@ -158,8 +159,8 @@ code does the parsing and validation of the syntax.
(ensure-bound (arg/res-vars a-res))))) (ensure-bound (arg/res-vars a-res)))))
;; post-condition variables are all bound ;; post-condition variables are all bound
(when (istx-post istx) (for ([post (in-list (istx-post istx))])
(let ([vars (pre/post-vars (istx-post istx))]) (let ([vars (pre/post-vars post)])
(ensure-bound vars))))) (ensure-bound vars)))))
(define (ensure-no-cycles stx istx) (define (ensure-no-cycles stx istx)
@ -328,6 +329,8 @@ code does the parsing and validation of the syntax.
(values '() leftover)] (values '() leftover)]
[(dep-range #:post . stuff) [(dep-range #:post . stuff)
(values '() leftover)] (values '() leftover)]
[(dep-range #:post/name . stuff)
(values '() leftover)]
[((opts ...) . rest) [((opts ...) . rest)
(values #'(opts ...) #'rest)] (values #'(opts ...) #'rest)]
[_ (values '() leftover)])] [_ (values '() leftover)])]
@ -358,48 +361,103 @@ code does the parsing and validation of the syntax.
"expected something to follow #:rest" "expected something to follow #:rest"
stx #'x)] stx #'x)]
[_ (values #f leftover)])] [_ (values #f leftover)])]
[(pre-cond leftover) [(pre-conds leftover)
(syntax-case leftover () (let loop ([leftover leftover]
[(#:pre (id ...) pre-cond . pre-leftover) [conditions '()])
(begin (syntax-case leftover ()
(syntax-case #'pre-leftover () [(#:pre (id ...) pre-cond . pre-leftover)
[() (raise-syntax-error (begin
#f (syntax-case #'pre-leftover ()
"expected #:pre to be followed by at least three subterms (a sequence of identifiers, the pre-condition and the range contract), but found only two" [() (raise-syntax-error
stx #f
(car (syntax->list leftover)))] "expected #:pre to be followed by at least three subterms (a sequence of identifiers, the pre-condition, and the range contract), but found only two"
[x (void)]) stx
(for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...))) (car (syntax->list leftover)))]
(values (pre/post (syntax->list #'(id ...)) #'pre-cond) #'pre-leftover))] [x (void)])
[_ (values #f leftover)])] (for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...)))
(loop #'pre-leftover
(cons (pre/post (syntax->list #'(id ...)) #f #'pre-cond) conditions)))]
[(#:pre . rest)
(raise-syntax-error #f
"expected a sequence of identifiers and an expression to follow #:pre"
stx
(car (syntax->list leftover)))]
[(#:pre/name (id ...) str pre-cond . pre-leftover)
(begin
(syntax-case #'pre-leftover ()
[() (raise-syntax-error
#f
"expected #:pre/name to be followed by at least four subterms (a sequence of identifiers, a name, the pre-condition, and the range contract), but found only three"
stx
(car (syntax->list leftover)))]
[x (void)])
(for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...)))
(unless (string? (syntax-e #'str))
(raise-syntax-error
#f
"expected #:pre/name to have a string after the sequence of variables"
stx
#'str))
(loop #'pre-leftover
(cons (pre/post (syntax->list #'(id ...)) (syntax-e #'str) #'pre-cond) conditions)))]
[(#:pre/name . rest)
(raise-syntax-error #f
"expected a sequence of identifiers, a string, and an expression to follow #:pre/name"
stx
(car (syntax->list leftover)))]
[_ (values (reverse conditions) leftover)]))]
[(range leftover) [(range leftover)
(syntax-case leftover () (begin
[(range . leftover) (syntax-case leftover ()
(not (keyword? (syntax-e #'range))) [(range . leftover)
(values #'range #'leftover)] (not (keyword? (syntax-e #'range)))
[(a . b) (values #'range #'leftover)]
(raise-syntax-error #f "expected a range expression" stx #'a)] [(a . b)
[() (raise-syntax-error #f "expected a range expression" stx #'a)]
(raise-syntax-error #f "expected a range expression, but found nothing" stx)])] [()
[(post-cond leftover) (raise-syntax-error #f "expected a range expression, but found nothing" stx)]))]
(syntax-case leftover () [(post-conds leftover)
[(#:post (id ...) post-cond . leftover) (let loop ([leftover leftover]
(begin [post-conds '()])
(for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...))) (syntax-case leftover ()
(syntax-case range (any) [(#:post (id ...) post-cond . leftover)
[any (raise-syntax-error #f "cannot have a #:post with any as the range" stx #'post-cond)] (begin
[_ (void)]) (for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...)))
(values (pre/post (syntax->list #'(id ...)) #'post-cond) #'leftover))] (syntax-case range (any)
[(#:post a b . stuff) [any (raise-syntax-error #f "cannot have a #:post with any as the range" stx #'post-cond)]
(begin [_ (void)])
(raise-syntax-error #f "expected a sequence of variables to follow #:post" stx #'a))] (loop #'leftover
[(#:post a) (cons (pre/post (syntax->list #'(id ...)) #f #'post-cond) post-conds)))]
(begin [(#:post a b . stuff)
(raise-syntax-error #f "expected a sequence of variables and an expression to follow #:post" stx #'a))] (begin
[_ (values #f leftover)])]) (raise-syntax-error #f "expected a sequence of variables to follow #:post" stx #'a))]
[(#:post a)
(begin
(raise-syntax-error #f "expected a sequence of variables and an expression to follow #:post" stx #'a))]
[(#:post/name (id ...) str post-cond . leftover)
(begin
(for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...)))
(syntax-case range (any)
[any (raise-syntax-error #f "cannot have a #:post with any as the range" stx #'post-cond)]
[_ (void)])
(unless (string? (syntax-e #'str))
(raise-syntax-error #f
"expected the error message part of a #:post/name declaraction to be a string"
stx
#'str))
(loop #'leftover
(cons (pre/post (syntax->list #'(id ...)) (syntax-e #'str) #'post-cond) post-conds)))]
[(#:post/name . stuff)
(begin
(raise-syntax-error #f "expected a sequence of variables, a string, and an expression to follow #:post/name"
stx
(car (syntax-e leftover))))]
[_
(values (reverse post-conds) leftover)]))])
(syntax-case leftover () (syntax-case leftover ()
[() [()
(values raw-mandatory-doms raw-optional-doms id/rest-id pre-cond range post-cond)] (values raw-mandatory-doms raw-optional-doms id/rest-id pre-conds range post-conds)]
[(a . b) [(a . b)
(raise-syntax-error #f "bad syntax" stx #'a)] (raise-syntax-error #f "bad syntax" stx #'a)]
[_ [_

96
collects/racket/contract/private/arr-i.rkt
View File

@ -111,9 +111,9 @@
(let* ([name-info (->i-name-info ctc)] (let* ([name-info (->i-name-info ctc)]
[args-info (vector-ref name-info 0)] [args-info (vector-ref name-info 0)]
[rest-info (vector-ref name-info 1)] [rest-info (vector-ref name-info 1)]
[pre-info (vector-ref name-info 2)] [pre-infos (vector-ref name-info 2)]
[rng-info (vector-ref name-info 3)] [rng-info (vector-ref name-info 3)]
[post-info (vector-ref name-info 4)]) [post-infos (vector-ref name-info 4)])
`(->i ,(arg/ress->spec args-info `(->i ,(arg/ress->spec args-info
(->i-arg-ctcs ctc) (->i-arg-ctcs ctc)
(->i-arg-dep-ctcs ctc) (->i-arg-dep-ctcs ctc)
@ -130,9 +130,12 @@
[(nodep) `(#:rest [,(list-ref rest-info 1) ,(contract-name (car (reverse (->i-arg-ctcs ctc))))])] [(nodep) `(#:rest [,(list-ref rest-info 1) ,(contract-name (car (reverse (->i-arg-ctcs ctc))))])]
[(dep) `(#:rest [,(list-ref rest-info 1) ,(list-ref rest-info 2) ...])]) [(dep) `(#:rest [,(list-ref rest-info 1) ,(list-ref rest-info 2) ...])])
'()) '())
,@(if pre-info ,@(apply
`(#:pre ,pre-info ...) append
'()) (for/list ([pre-info pre-infos])
(if (cadr pre-info)
`(#:pre/name ,@pre-info ...)
`(#:pre ,(car pre-info) ...))))
,(cond ,(cond
[(not rng-info) [(not rng-info)
'any] 'any]
@ -146,9 +149,12 @@
`(values ,@infos)] `(values ,@infos)]
[else [else
(car infos)]))]) (car infos)]))])
,@(if post-info ,@(apply
`(#:post ,post-info ...) append
'())))) (for/list ([post-info post-infos])
(if (cadr post-info)
`(#:post/name ,@post-info ...)
`(#:post ,(car post-info) ...)))))))
#:first-order #:first-order
(λ (ctc) (λ (ctc)
(let ([has-rest? (->i-rest? ctc)] (let ([has-rest? (->i-rest? ctc)]
@ -331,33 +337,33 @@
(define-for-syntax (maybe-generate-temporary x) (define-for-syntax (maybe-generate-temporary x)
(and x (car (generate-temporaries (list x))))) (and x (car (generate-temporaries (list x)))))
(define (check-pre bool val blame) (define (check-pre bool val str blame)
(unless bool (unless bool
(raise-blame-error blame val "#:pre condition violation"))) (raise-blame-error blame val (or str "#:pre condition violation"))))
(define (check-post bool val blame) (define (check-post bool val str blame)
(unless bool (unless bool
(raise-blame-error blame val "#:post condition violation"))) (raise-blame-error blame val (or str "#:post condition violation"))))
(define-for-syntax (add-pre-cond an-istx arg/res-to-indy-var call-stx) (define-for-syntax (add-pre-cond an-istx arg/res-to-indy-var call-stx)
(cond #`(begin #,@(for/list ([pre (in-list (istx-pre an-istx))]
[(istx-pre an-istx) [i (in-naturals)])
#`(begin (check-pre (pre-proc #,@(map arg/res-to-indy-var (pre/post-vars (istx-pre an-istx)))) (define id (string->symbol (format "pre-proc~a" i)))
val #`(check-pre (#,id #,@(map arg/res-to-indy-var (pre/post-vars pre)))
swapped-blame) val
#,call-stx)] #,(pre/post-str pre)
[else swapped-blame))
call-stx])) #,call-stx))
(define-for-syntax (add-post-cond an-istx arg/res-to-indy-var call-stx) (define-for-syntax (add-post-cond an-istx arg/res-to-indy-var call-stx)
(cond #`(begin #,@(for/list ([post (in-list (istx-post an-istx))]
[(istx-post an-istx) [i (in-naturals)])
#`(begin (check-post (post-proc #,@(map arg/res-to-indy-var (pre/post-vars (istx-post an-istx)))) (define id (string->symbol (format "post-proc~a" i)))
val #`(check-post (#,id #,@(map arg/res-to-indy-var (pre/post-vars post)))
blame) val
#,call-stx)] #,(pre/post-str post)
[else blame))
call-stx])) #,call-stx))
;; add-wrapper-let : syntax ;; add-wrapper-let : syntax
;; (listof arg/res) -- sorted version of the arg/res structs, ordered by evaluation order ;; (listof arg/res) -- sorted version of the arg/res structs, ordered by evaluation order
@ -530,8 +536,12 @@
#`(λ (blame swapped-blame indy-dom-blame indy-rng-blame chk ctc #`(λ (blame swapped-blame indy-dom-blame indy-rng-blame chk ctc
;; the pre- and post-condition procs ;; the pre- and post-condition procs
#,@(if (istx-pre an-istx) (list #'pre-proc) '()) #,@(for/list ([pres (istx-pre an-istx)]
#,@(if (istx-post an-istx) (list #'post-proc) '()) [i (in-naturals)])
(string->symbol (format "pre-proc~a" i)))
#,@(for/list ([pres (istx-post an-istx)]
[i (in-naturals)])
(string->symbol (format "post-proc~a" i)))
;; first the non-dependent arg projections ;; first the non-dependent arg projections
#,@(filter values (map (λ (arg/res arg-proj-var) (and (not (arg/res-vars arg/res)) arg-proj-var)) #,@(filter values (map (λ (arg/res arg-proj-var) (and (not (arg/res-vars arg/res)) arg-proj-var))
@ -617,8 +627,8 @@
(free-identifier-mapping-put! vars var #t))))) (free-identifier-mapping-put! vars var #t)))))
;; pre-condition ;; pre-condition
(when (istx-pre an-istx) (for ([pre (in-list (istx-pre an-istx))])
(for ([var (in-list (pre/post-vars (istx-pre an-istx)))]) (for ([var (in-list (pre/post-vars pre))])
(free-identifier-mapping-put! vars var #t))) (free-identifier-mapping-put! vars var #t)))
;; results ;; results
@ -629,8 +639,8 @@
(free-identifier-mapping-put! vars var #t))))) (free-identifier-mapping-put! vars var #t)))))
;; post-condition ;; post-condition
(when (istx-post an-istx) (for ([post (in-list (istx-post an-istx))])
(for ([var (in-list (pre/post-vars (istx-post an-istx)))]) (for ([var (in-list (pre/post-vars post))])
(free-identifier-mapping-put! vars var #t))) (free-identifier-mapping-put! vars var #t)))
vars)) vars))
@ -742,12 +752,10 @@
#''()) #''())
#,(let ([func (λ (pre/post) #`(λ #,(pre/post-vars pre/post) #,(pre/post-exp pre/post)))]) #,(let ([func (λ (pre/post) #`(λ #,(pre/post-vars pre/post) #,(pre/post-exp pre/post)))])
#`(list #,@(if (istx-pre an-istx) #`(list #,@(for/list ([pre (in-list (istx-pre an-istx))])
(list (func (istx-pre an-istx))) (func pre))
'()) #,@(for/list ([post (in-list (istx-post an-istx))])
#,@(if (istx-post an-istx) (func post))))
(list (func (istx-post an-istx)))
'())))
#,(length (filter values (map (λ (arg) (and (not (arg-kwd arg)) (not (arg-optional? arg)))) #,(length (filter values (map (λ (arg) (and (not (arg-kwd arg)) (not (arg-optional? arg))))
(istx-args an-istx)))) (istx-args an-istx))))
@ -778,7 +786,9 @@
,(map syntax-e (arg/res-vars (istx-rst an-istx)))) ,(map syntax-e (arg/res-vars (istx-rst an-istx))))
`(nodep ,(syntax-e (arg/res-var (istx-rst an-istx))))) `(nodep ,(syntax-e (arg/res-var (istx-rst an-istx)))))
#f) #f)
#,(and (istx-pre an-istx) (map syntax-e (pre/post-vars (istx-pre an-istx)))) #,(for/list ([pre (in-list (istx-pre an-istx))])
(list (map syntax-e (pre/post-vars pre))
(pre/post-str pre)))
#,(and (istx-ress an-istx) #,(and (istx-ress an-istx)
(for/list ([a-res (in-list (istx-ress an-istx))]) (for/list ([a-res (in-list (istx-ress an-istx))])
`(,(if (arg/res-vars a-res) 'dep 'nodep) `(,(if (arg/res-vars a-res) 'dep 'nodep)
@ -790,7 +800,9 @@
'()) '())
#f #f
#f))) #f)))
#,(and (istx-post an-istx) (map syntax-e (pre/post-vars (istx-post an-istx)))))) #,(for/list ([post (in-list (istx-post an-istx))])
(list (map syntax-e (pre/post-vars post))
(pre/post-str post)))))
'racket/contract:contract 'racket/contract:contract
(let () (let ()
(define (find-kwd kwd) (define (find-kwd kwd)

23
collects/scribblings/reference/contracts.scrbl
View File

@ -600,13 +600,17 @@ symbols, and that return a symbol.
[optional-dependent-dom id+ctc [optional-dependent-dom id+ctc
(code:line keyword id+ctc)] (code:line keyword id+ctc)]
[dependent-rest (code:line) (code:line #:rest id+ctc)] [dependent-rest (code:line) (code:line #:rest id+ctc)]
[pre-condition (code:line) (code:line #:pre (id ...) boolean-expr)] [pre-condition (code:line)
(code:line #:pre (id ...) boolean-expr pre-condition)
(code:line #:pre/name (id ...) string boolean-expr pre-condition)]
[dependent-range any [dependent-range any
id+ctc id+ctc
un+ctc un+ctc
(values id+ctc ...) (values id+ctc ...)
(values un+ctc ...)] (values un+ctc ...)]
[post-condition (code:line) (code:line #:post (id ...) boolean-expr)] [post-condition (code:line)
(code:line #:post (id ...) boolean-expr post-condition)
(code:line #:post/name (id ...) string boolean-expr post-condition)]
[id+ctc [id contract-expr] [id+ctc [id contract-expr]
[id (id ...) contract-expr]] [id (id ...) contract-expr]]
[un+ctc [_ contract-expr] [un+ctc [_ contract-expr]
@ -623,7 +627,8 @@ The first sub-form of a @racket[->i] contract covers the mandatory and the
second sub-form covers the optional arguments. Following that is an optional second sub-form covers the optional arguments. Following that is an optional
rest-args contract, and an optional pre-condition. The pre-condition is rest-args contract, and an optional pre-condition. The pre-condition is
introduced with the @racket[#:pre] keyword followed by the list of names on introduced with the @racket[#:pre] keyword followed by the list of names on
which it depends. which it depends. If the @racket[#:pre/name] keyword is used, the string
supplied is used as part of the error message; similarly with @racket[#:post/name].
The @racket[dep-range] non-terminal specifies the possible result The @racket[dep-range] non-terminal specifies the possible result
contracts. If it is @racket[any], then any value is allowed. Otherwise, the contracts. If it is @racket[any], then any value is allowed. Otherwise, the
@ -642,14 +647,14 @@ second argument (@scheme[y]) demands that it is greater than the first
argument. The result contract promises a number that is greater than the argument. The result contract promises a number that is greater than the
sum of the two arguments. While the dependency specification for @scheme[y] sum of the two arguments. While the dependency specification for @scheme[y]
signals that the argument contract depends on the value of the first signals that the argument contract depends on the value of the first
argument, the dependency list for @scheme[result] indicates that the argument, the dependency sequence for @scheme[result] indicates that the
contract depends on both argument values. @margin-note*{In general, an contract depends on both argument values. @margin-note*{In general, an
empty list is (nearly) equivalent to not adding empty sequence is (nearly) equivalent to not adding
a list at all except that the former is more expensive than the latter.} a sequence at all except that the former is more expensive than the latter.}
Since the contract for @racket[x] does not depend on anything else, it does Since the contract for @racket[x] does not depend on anything else, it does
not come with any dependency list, not even @scheme[()]. not come with any dependency sequence, not even @scheme[()].
The contract expressions are not evaluated in The contract expressions are not always evaluated in
order. First, if there is no dependency for a given contract expression, order. First, if there is no dependency for a given contract expression,
the contract expression is evaluated at the time that the @racket[->i] the contract expression is evaluated at the time that the @racket[->i]
expression is evaluated rather than the time when the function is called or expression is evaluated rather than the time when the function is called or
@ -664,7 +669,7 @@ argument, with its contract checked, is available for the other). When
there is no dependency between two arguments (or the result and an there is no dependency between two arguments (or the result and an
argument), then the contract that appears earlier in the source text is argument), then the contract that appears earlier in the source text is
evaluated first. evaluated first.
#;
Finally, if all of the identifier positions of the range Finally, if all of the identifier positions of the range
contract are @racket[_]s (underscores), then the range contract expressions contract are @racket[_]s (underscores), then the range contract expressions
are evaluated when the function is called and the underscore is not bound are evaluated when the function is called and the underscore is not bound

132
collects/tests/racket/contract-test.rktl
View File

@ -2501,6 +2501,38 @@
(λ (x) 1) (λ (x) 1)
'pos 'neg) 2)) 'pos 'neg) 2))
(test/neg-blame
'->i35-b
'((contract (->i ([x number?]) #:pre () #t #:pre () (= 1 2) any)
(λ (x) 1)
'pos 'neg) 2))
(test/neg-blame
'->i35-c
'((contract (->i ([x number?]) #:pre (x) (even? x) #:pre (x) (positive? x) any)
(λ (x) 1)
'pos 'neg) 3))
(test/neg-blame
'->i35-d
'((contract (->i ([x number?]) #:pre (x) (even? x) #:pre (x) (positive? x) any)
(λ (x) 1)
'pos 'neg) -2))
(test/neg-blame
'->i35-e
'((contract (->i ([x any/c]) #:pre (x) (pair? x) #:pre (x) (car x) any)
(λ (x) 1)
'pos 'neg)
(cons #f 1)))
(test/neg-blame
'->i35-f
'((contract (->i ([x any/c]) #:pre/name (x) "pair" (pair? x) #:pre/name (x) "car" (car x) any)
(λ (x) 1)
'pos 'neg)
(cons #f 1)))
(test/spec-passed/result (test/spec-passed/result
'->i36 '->i36
'((contract (->i ([f (-> number? number?)]) [res number?]) '((contract (->i ([f (-> number? number?)]) [res number?])
@ -2570,51 +2602,95 @@
(test/spec-passed/result (test/spec-passed/result
'->i44 '->i44
'((contract (->i ([x () any/c]) '((contract (->i ([x () any/c])
[y any/c] [y any/c]
#:post (x) x) #:post (x) x)
(lambda (x) x) (lambda (x) x)
'pos 'pos
'neg) 'neg)
#t) #t)
'#t) '#t)
(test/pos-blame (test/pos-blame
'->i45 '->i45
'((contract (->i ([x () any/c]) '((contract (->i ([x () any/c])
[y any/c] [y any/c]
#:post (x) x) #:post (x) x)
(lambda (x) x) (lambda (x) x)
'pos 'pos
'neg) 'neg)
#f)) #f))
(test/spec-passed/result (test/spec-passed/result
'->i46 '->i46
'((contract (->i ([x any/c]) '((contract (->i ([x any/c])
[y () any/c] [y () any/c]
#:post (y) y) #:post (y) y)
(lambda (x) x) (lambda (x) x)
'pos 'pos
'neg) 'neg)
#t) #t)
'#t) '#t)
(test/pos-blame (test/pos-blame
'->i47 '->i47
'((contract (->i ([x any/c]) '((contract (->i ([x any/c])
[y () any/c] [y () any/c]
#:post (y) y) #:post (y) y)
(lambda (x) x) (lambda (x) x)
'pos 'pos
'neg) 'neg)
#f)) #f))
(test/pos-blame
'->i47-b
'((contract (->i ([x any/c])
[y () any/c]
#:post (y) (even? y)
#:post (y) (positive? y))
(lambda (x) x)
'pos
'neg)
-2))
(test/pos-blame
'->i47-c
'((contract (->i ([x any/c])
[y () any/c]
#:post (y) (even? y)
#:post (y) (positive? y))
(lambda (x) x)
'pos
'neg)
3))
(test/pos-blame
'->i47-d
'((contract (->i ([x any/c])
[y () any/c]
#:post (y) (pair? y)
#:post (y) (car y))
(lambda (x) x)
'pos
'neg)
(cons #f 1)))
(test/pos-blame
'->i47-e
'((contract (->i ([x any/c])
[y () any/c]
#:post/name (y) "pair" (pair? y)
#:post/name (y) "car" (car y))
(lambda (x) x)
'pos
'neg)
(cons #f 1)))
(test/spec-passed/result (test/spec-passed/result
'->i48 '->i48
'(let ([x '()]) '(let ([x '()])
((contract (->i ([arg (begin (set! x (cons 'arg-eval x)) integer?)]) ((contract (->i ([arg (begin (set! x (cons 'arg-eval x)) integer?)])
[res () (begin [res () (begin
(set! x (cons 'res-eval x)) (set! x (cons 'res-eval x))
(λ (res) (λ (res)
(set! x (cons 'res-check x))))]) (set! x (cons 'res-check x))))])
(λ (arg) (λ (arg)
@ -9538,6 +9614,10 @@ so that propagation occurs.
(->i ([x integer?]) #:pre (x) #t [q (x) number?] #:post (x) #t)) (->i ([x integer?]) #:pre (x) #t [q (x) number?] #:post (x) #t))
(test-name '(->i ([x real?]) [_ (x) ...]) (test-name '(->i ([x real?]) [_ (x) ...])
(->i ([x real?]) [_ (x) (>/c x)])) (->i ([x real?]) [_ (x) (>/c x)]))
(test-name '(->i ([x any/c]) #:pre/name (x) "pair" ... #:pre/name (x) "car" ... any)
(->i ([x any/c]) #:pre/name (x) "pair" (pair? x) #:pre/name (x) "car" (car x) any))
(test-name '(->i ([x any/c]) [y () ...] #:post/name (y) "pair" ... #:post/name (y) "car" ...)
(->i ([x any/c]) [y () any/c] #:post/name (y) "pair" (pair? y) #:post/name (y) "car" (car y)))
(test-name '(case->) (case->)) (test-name '(case->) (case->))
(test-name '(case-> (-> integer? any) (-> boolean? boolean? any) (-> char? char? char? any)) (test-name '(case-> (-> integer? any) (-> boolean? boolean? any) (-> char? char? char? any))