adjusted the syntax of ->i so that #:post and #:pre get a list of variables now

This commit is contained in:
Robby Findler 2010-08-04 16:38:03 -05:00
parent 3b431c6ff2
commit c1b558e1a3
8 changed files with 154 additions and 116 deletions

View File

@ -4,7 +4,7 @@
;; the PLT code base where appropriate.
(require "private/arrow.rkt"
"private/arr-i.rkt"
"private/arr-i-old.rkt"
"private/base.rkt"
"private/misc.rkt"
"private/provide.rkt"
@ -24,7 +24,7 @@
check-procedure
check-procedure/more
make-contracted-function)
(all-from-out "private/arr-i.rkt")
(all-from-out "private/arr-i-old.rkt")
(except-out (all-from-out "private/misc.rkt")
check-between/c
check-unary-between/c)

View File

@ -29,7 +29,7 @@
(values '() leftover)]
[(dep-range)
(values '() leftover)]
[(dep-range #:post-cond expr)
[(dep-range #:post expr)
(values '() leftover)]
[((opts ...) . rest)
(values #'(opts ...) #'rest)]
@ -50,7 +50,7 @@
[_ (values #f leftover)])]
[(pre-cond leftover)
(syntax-case leftover ()
[(#:pre-cond pre-cond . leftover)
[(#:pre (id ...) pre-cond . leftover)
(values #'pre-cond #'leftover)]
[_ (values #f leftover)])]
[(range leftover)
@ -60,10 +60,10 @@
(raise-syntax-error #f "expected a range expression, but found nothing" stx)])]
[(post-cond leftover)
(syntax-case leftover ()
[(#:post-cond post-cond . leftover)
[(#:post (id ...) post-cond . leftover)
(begin
(syntax-case range (any)
[any (raise-syntax-error #f "cannot have a #:post-cond with any as the range" stx #'post-cond)]
[any (raise-syntax-error #f "cannot have a #:post with any as the range" stx #'post-cond)]
[_ (void)])
(values #'post-cond #'leftover))]
[_ (values #f leftover)])])
@ -132,11 +132,11 @@
[(pair? stx)
(when (and (syntax? (car stx))
(eq? (syntax-e (car stx))
'#:pre-cond))
'#:pre))
(set! pre (car stx)))
(when (and (syntax? (car stx))
(eq? (syntax-e (car stx))
'#:post-cond))
'#:post))
(set! post (car stx)))
(loop (cdr stx))]
[else (void)]))
@ -388,7 +388,7 @@
(unless (apply (->d-pre-cond ->d-stct) dep-pre-args)
(raise-blame-error (blame-swap blame)
val
"#:pre-cond violation~a"
"#:pre violation~a"
(build-values-string ", argument" dep-pre-args))))
(call-with-immediate-continuation-mark
->d-tail-key
@ -413,7 +413,7 @@
(unless (apply (->d-post-cond ->d-stct) dep-post-args)
(raise-blame-error blame
val
"#:post-cond violation~a~a"
"#:post violation~a~a"
(build-values-string ", argument" dep-pre-args)
(build-values-string (if (null? dep-pre-args)
", result"
@ -571,7 +571,7 @@
(list '#:rest (next-id) '...)
'())
,@(if (->d-pre-cond ctc)
(list '#:pre-cond '...)
(list '#:pre '...)
(list))
,(let ([range (->d-range ctc)])
(cond
@ -590,7 +590,7 @@
[else
`(values ,@(map (λ (x) `(,(next-id) ...)) range))]))
,@(if (->d-post-cond ctc)
(list '#:post-cond '...)
(list '#:post '...)
(list)))))
#:first-order (λ (ctc) (λ (x) #f))

View File

@ -312,7 +312,7 @@ code does the parsing and validation of the syntax.
(values '() leftover)]
[(dep-range)
(values '() leftover)]
[(dep-range #:post-cond expr)
[(dep-range #:post expr)
(values '() leftover)]
[((opts ...) . rest)
(values #'(opts ...) #'rest)]
@ -346,8 +346,10 @@ code does the parsing and validation of the syntax.
[_ (values #f leftover)])]
[(pre-cond leftover)
(syntax-case leftover ()
[(#:pre-cond pre-cond . leftover)
(values #'pre-cond #'leftover)]
[(#:pre (id ...) pre-cond . leftover)
(begin
(for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...)))
(values #'pre-cond #'leftover))]
[_ (values #f leftover)])]
[(range leftover)
(syntax-case leftover ()
@ -356,17 +358,20 @@ code does the parsing and validation of the syntax.
(raise-syntax-error #f "expected a range expression, but found nothing" stx leftover)])]
[(post-cond leftover)
(syntax-case leftover ()
[(#:post-cond post-cond . leftover)
[(#:post (id ...) 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-cond with any as the range" stx #'post-cond)]
[any (raise-syntax-error #f "cannot have a #:post with any as the range" stx #'post-cond)]
[_ (void)])
(values #'post-cond #'leftover))]
[_ (values #f leftover)])])
(syntax-case leftover ()
[()
(values raw-mandatory-doms raw-optional-doms id/rest-id pre-cond range post-cond)]
[_
[(a . b)
(raise-syntax-error #f "bad syntax" stx #'a)]
[_
(raise-syntax-error #f "bad syntax" stx)])))
;(define (ensure-no-cycles istx)

View File

@ -231,6 +231,7 @@
(chk val #,(and (syntax-parameter-value #'making-a-method) #t))
(make-contracted-function
(λ #,(args/vars->arglist (istx-args an-istx) wrapper-args)
;; WRONG: need to include the pre- and post-condition checking somewhere in here.
#,(for/fold ([body (args/vars->callsite #'val (istx-args an-istx) wrapper-args)])
([indy-arg (in-list indy-args)]
[arg (in-list ordered-args)]
@ -267,7 +268,7 @@
ctc))))))
(define (un-dep ctc obj blame)
;; WRONG (well, just need to avoid calling coerce-contract if 'ctc' is something simple)
;; WRONG (well, just need to avoid calling coerce-contract if 'ctc' is something simple)
(let ([ctc (coerce-contract '->i ctc)])
(((contract-projection ctc) blame) obj)))
@ -293,8 +294,20 @@
(istx-args an-istx))))]
[(arg-exps ...)
(filter values (map (λ (arg) (and (not (arg-vars arg)) (arg-ctc arg)))
(istx-args an-istx)))])
#`(let ([arg-exp-xs arg-exps] ...)
(istx-args an-istx)))]
[(res-exp-xs ...)
(if (istx-ress an-istx)
(generate-temporaries (filter values (map (λ (res) (and (not (res-vars res)) (res-var res)))
(istx-ress an-istx))))
'())]
[(res-exps ...)
(if (istx-ress an-istx)
(filter values (map (λ (res) (and (not (res-vars res)) (res-ctc res)))
(istx-ress an-istx)))
'())])
#`(let ([arg-exp-xs arg-exps] ...
[res-exp-xs res-exps] ...)
(->i
;; all of the non-dependent argument contracts
(list arg-exp-xs ...)
@ -311,17 +324,15 @@
#,(if (istx-ress an-istx)
#`(list #,@(filter values (map (λ (arg) (and (not (res-vars arg)) (res-ctc arg)))
(istx-ress an-istx))))
#`(list res-exp-xs ...)
#''())
#,(if (istx-ress an-istx)
#`(list #,@(filter values (map (λ (arg) (and (res-vars arg) #`(λ #,(res-vars arg) (opt/c #,(res-ctc arg)))))
(istx-ress an-istx))))
#''())
;; WRONG! this needs to be a subset of the previuos^2 (and to generate a let to share appropriately)
;; WRONG! this needs to be a subset of the previuos^2
#,(if (istx-ress an-istx)
#`(list #,@(filter values (map (λ (arg) (and (not (res-vars arg)) (res-ctc arg)))
(istx-ress an-istx))))
#`(list res-exp-xs ...)
#''())
#,(length (filter values (map (λ (arg) (and (not (arg-kwd arg)) (not (arg-optional? arg))))

View File

@ -651,6 +651,8 @@ v4 todo:
(values '() leftover)]
[(dep-range #:post-cond expr)
(values '() leftover)]
[(dep-range #:post expr)
(values '() leftover)]
[((opts ...) . rest)
(values #'(opts ...) #'rest)]
[_ (values '() leftover)])]
@ -669,6 +671,8 @@ v4 todo:
[_ (values #f leftover)])]
[(pre-cond leftover)
(syntax-case leftover ()
[(#:pre pre-cond . leftover)
(values #'pre-cond #'leftover)]
[(#:pre-cond pre-cond . leftover)
(values #'pre-cond #'leftover)]
[_ (values #f leftover)])]
@ -679,6 +683,12 @@ v4 todo:
(raise-syntax-error #f "expected a range expression, but found nothing" stx)])]
[(post-cond leftover)
(syntax-case leftover ()
[(#:post post-cond . leftover)
(begin
(syntax-case range (any)
[any (raise-syntax-error #f "cannot have a #:post with any as the range" stx #'post-cond)]
[_ (void)])
(values #'post-cond #'leftover))]
[(#:post-cond post-cond . leftover)
(begin
(syntax-case range (any)
@ -940,7 +950,7 @@ v4 todo:
(unless (apply (->d-pre-cond ->d-stct) dep-pre-args)
(raise-blame-error (blame-swap blame)
val
"#:pre-cond violation~a"
"#:pre violation~a"
(build-values-string ", argument" dep-pre-args))))
(call-with-immediate-continuation-mark
->d-tail-key
@ -965,7 +975,7 @@ v4 todo:
(unless (apply (->d-post-cond ->d-stct) dep-post-args)
(raise-blame-error blame
val
"#:post-cond violation~a~a"
"#:post violation~a~a"
(build-values-string ", argument" dep-pre-args)
(build-values-string (if (null? dep-pre-args)
", result"
@ -1126,7 +1136,7 @@ v4 todo:
(list '#:rest (next-id) '...)
'())
,@(if (->d-pre-cond ctc)
(list '#:pre-cond '...)
(list '#:pre '...)
(list))
,(let ([range (->d-range ctc)])
(cond
@ -1145,7 +1155,7 @@ v4 todo:
[else
`(values ,@(map (λ (x) `(,(next-id) ...)) range))]))
,@(if (->d-post-cond ctc)
(list '#:post-cond '...)
(list '#:post '...)
(list)))))
#:first-order (λ (ctc) (λ (x) #f))

View File

@ -2,30 +2,24 @@
(require racket/contract
racket/pretty)
(->i ([x number?]) [res any/c] #:post () #t)
#;
(pretty-print
(syntax->datum (expand-once
#'(->i ([x number?]
[y (x z) (between/c x z)]
[z number?])
any))))
#'(->i () #:pre-cond #f any #:post-cond #f))))
#;
(pretty-print
(syntax->datum (expand
#'(->i ([x number?]
[y (x z) (between/c x z)]
[z number?])
any))))
#'(->i () [x integer?]))))
((contract (->i ([x number?]
[y (x z) (between/c x z)]
[z number?])
any)
(λ (x y z) (+ x y z))
'pos 'neg)
1 2 3)
;; => 6
#;
((contract (->i () #:pre-cond #f any)
(λ () 1)
'pos 'neg))
;; => 1
#|
;; timing tests:

View File

@ -517,13 +517,13 @@ symbols, and that return a symbol.
[optional-dependent-dom id+ctc
(code:line keyword id+ctc)]
[dependent-rest (code:line) (code:line #:rest id+ctc)]
[pre-condition (code:line) (code:line #:pre-cond boolean-expr)]
[pre-condition (code:line) (code:line #:pre (id ...) boolean-expr)]
[dependent-range any
id+ctc
un+ctc
(values id+ctc ...)
(values un+ctc ...)]
[post-condition (code:line) (code:line #:post-cond boolean-expr)]
[post-condition (code:line) (code:line #:post (id ...) boolean-expr)]
[id+ctc [id contract-expr]
[id (id ...) contract-expr]]
[un+ctc [_ contract-expr]
@ -542,14 +542,19 @@ The first subforms of a @racket[->i] contract covers the
mandatory and the second (optional) subform covers the optional
arguments. Following that is an
optional rest-args contract, and an optional
pre-condition. The @racket[dep-range] non-terminal covers
the possible post-condition contracts. If it is
pre-condition. The pre-condition is specified with
the @racket[#:pre] keyword, and must be followed
with the argument variables that it depends on.
The @racket[dep-range] non-terminal covers
the possible result contracts. If it is
@racket[any], then any result (or results) are
allowed. Otherwise, the result contract can be a name and a
result contract, or a multiple values return and, in either
of the last two cases, it may be optionally followed by a
post-condition (the post-condition expression is not allowed
if the range is @racket[any]).
if the range is @racket[any]). Like the pre-condition, the
post-condition must specify the variables that it depends on.
Each of the @racket[id]s on an argument (including the rest
argument) is visible in the pre- and post-conditions sub-expressions of
@ -601,7 +606,7 @@ called @racket[the-unsupplied-arg] value.
([mandatory-dependent-dom [id dom-expr] (code:line keyword [id dom-expr])]
[optional-dependent-dom [id dom-expr] (code:line keyword [id dom-expr])]
[dependent-rest (code:line) (code:line #:rest id rest-expr)]
[pre-condition (code:line) (code:line #:pre-cond boolean-expr)]
[pre-condition (code:line) (code:line #:pre boolean-expr) (code:line #:pre-cond boolean-expr)]
[dependent-range any
[_ range-expr]
(values [_ range-expr] ...)
@ -617,13 +622,16 @@ This contract is similar to @racket[->i], but is ``lax'', meaning
that it does not enforce contracts internally. For example, using
this contract
@racketblock[(->d ([f (-> integer? integer?)])
#:pre-cond
#:pre
(zero? (f #f))
any)]
will allow @racket[f] to be called with @racket[#f], trigger whatever bad
behavior the author of @scheme[f] was trying to prohibit by insisting that
@racket[f]'s contract accept ony integers.
The @racket[#:pre-cond] and @racket[#:post-cond] keywords are synonyms for
@racket[#:pre] and @racket[#:post] and are provided for backwards compatibility.
}
@defform*/subs[#:literals (any values ->)

View File

@ -1412,6 +1412,14 @@
'->d-arity10
'(contract (->d () (#:x [x integer?]) any) (λ (#:x [x 1]) 1) 'pos 'neg))
(test/spec-passed
'->d-pp0
'((contract (->d ([x number?]) () #:pre (= x 1) [result number?] #:post (= x 1))
(λ (x) x)
'pos
'neg)
1))
(test/pos-blame
'->d-pp1
'((contract (->d ([x number?]) () #:pre-cond (= x 1) [result number?] #:post-cond (= x 2))
@ -2182,7 +2190,7 @@
(test/pos-blame
'->i-pp1
'((contract (->i ([x number?]) () #:pre-cond (= x 1) [result number?] #:post-cond (= x 2))
'((contract (->i ([x number?]) () #:pre (x) (= x 1) [result number?] #:post (x) (= x 2))
(λ (x) x)
'pos
'neg)
@ -2190,7 +2198,7 @@
(test/neg-blame
'->i-pp2
'((contract (->i ([x number?]) () #:pre-cond (= x 1) [result number?] #:post-cond (= x 2))
'((contract (->i ([x number?]) () #:pre (x) (= x 1) [result number?] #:post (x) (= x 2))
(λ (x) x)
'pos
'neg)
@ -2198,7 +2206,7 @@
(test/pos-blame
'->i-pp3
'((contract (->i ([x number?]) () #:pre-cond (= x 1) [result number?] #:post-cond (= result 2))
'((contract (->i ([x number?]) () #:pre (x) (= x 1) [result number?] #:post (result) (= result 2))
(λ (x) x)
'pos
'neg)
@ -2206,7 +2214,7 @@
(test/spec-passed
'->i-pp3.5
'((contract (->i ([x number?]) () #:pre-cond (= x 1) [result number?] #:post-cond (= result 2))
'((contract (->i ([x number?]) () #:pre (x) (= x 1) [result number?] #:post (result) (= result 2))
(λ (x) 2)
'pos
'neg)
@ -2214,7 +2222,7 @@
(test/neg-blame
'->i-pp4
'((contract (->i ([x number?]) () #:pre-cond (= x 1) any)
'((contract (->i ([x number?]) () #:pre (x) (= x 1) any)
(λ (x) x)
'pos
'neg)
@ -2222,7 +2230,7 @@
(test/neg-blame
'->i-pp5
'((contract (->i ([x number?]) () #:pre-cond (= x 1) (values [z number?] [y number?]) #:post-cond (= x y z 3))
'((contract (->i ([x number?]) () #:pre (x) (= x 1) (values [z number?] [y number?]) #:post (x y z) (= x y z 3))
(λ (x) (values 4 5))
'pos
'neg)
@ -2230,7 +2238,7 @@
(test/pos-blame
'->i-pp6
'((contract (->i ([x number?]) () #:pre-cond (= x 1) (values [z number?] [y number?]) #:post-cond (= z y 3))
'((contract (->i ([x number?]) () #:pre (x) (= x 1) (values [z number?] [y number?]) #:post (z y) (= z y 3))
(λ (x) (values 4 5))
'pos
'neg)
@ -2238,7 +2246,7 @@
(test/pos-blame
'->i-pp-r1
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre-cond (= x 1) [result number?] #:post-cond (= x 2))
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre (x) (= x 1) [result number?] #:post (x) (= x 2))
(λ (x . rst) x)
'pos
'neg)
@ -2246,7 +2254,7 @@
(test/neg-blame
'->i-pp-r2
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre-cond (= x 1) [result number?] #:post-cond (= x 2))
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre (x) (= x 1) [result number?] #:post (x) (= x 2))
(λ (x . rst) x)
'pos
'neg)
@ -2254,7 +2262,7 @@
(test/pos-blame
'->i-pp-r3
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre-cond (= x 1) [result number?] #:post-cond (= result 2))
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre (x) (= x 1) [result number?] #:post (result) (= result 2))
(λ (x . rst) x)
'pos
'neg)
@ -2262,7 +2270,7 @@
(test/spec-passed
'->i-pp-r3.5
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre-cond (= x 1) [result number?] #:post-cond (= result 2))
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre (x) (= x 1) [result number?] #:post (result) (= result 2))
(λ (x . rst) 2)
'pos
'neg)
@ -2270,7 +2278,7 @@
(test/neg-blame
'->i-pp-r4
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre-cond (= x 1) any)
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre (x) (= x 1) any)
(λ (x . rst) x)
'pos
'neg)
@ -2278,7 +2286,7 @@
(test/neg-blame
'->i-pp-r5
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre-cond (= x 1) (values [z number?] [y number?]) #:post-cond (= x y z 3))
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre (x) (= x 1) (values [z number?] [y number?]) #:post (x y z) (= x y z 3))
(λ (x . rst) (values 4 5))
'pos
'neg)
@ -2286,7 +2294,7 @@
(test/pos-blame
'->i-pp-r6
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre-cond (= x 1) (values [z number?] [y number?]) #:post-cond (= z x y 3))
'((contract (->i ([x number?]) () #:rest [rst any/c] #:pre (x) (= x 1) (values [z number?] [y number?]) #:post (x y z) (= z x y 3))
(λ (x . rst) (values 4 5))
'pos
'neg)
@ -2296,7 +2304,7 @@
'->i-protect-shared-state
'(let ([x 1])
((contract (let ([save #f])
(-> (->i () () #:pre-cond (set! save x) [range any/c] #:post-cond (= save x))
(-> (->i () () #:pre (x) (set! save x) [range any/c] #:post (x) (= save x))
any))
(λ (t) (t))
'pos
@ -2320,42 +2328,42 @@
(test/spec-passed
'->i-optopt3
'((contract (->i ([x number?]) #:pre-cond #t any)
'((contract (->i ([x number?]) #:pre () #t any)
(λ (x) x)
'pos 'neg)
1))
(test/spec-passed
'->i-optopt4
'((contract (->i ([x number?]) #:rest [rst any/c] #:pre-cond #t any)
'((contract (->i ([x number?]) #:rest [rst any/c] #:pre () #t any)
(λ (x . y) x)
'pos 'neg)
1))
(test/spec-passed
'->i-optopt5
'((contract (->i ([x number?]) #:rest [rst any/c] #:pre-cond #t [res any/c] #:post-cond #t)
'((contract (->i ([x number?]) #:rest [rst any/c] #:pre () #t [res any/c] #:post () #t)
(λ (x . y) x)
'pos 'neg)
1))
(test/spec-passed
'->i-optopt6
'((contract (->i ([x number?]) #:rest [rst any/c] [res any/c] #:post-cond #t)
'((contract (->i ([x number?]) #:rest [rst any/c] [res any/c] #:post () #t)
(λ (x . y) x)
'pos 'neg)
1))
(test/spec-passed
'->i-optopt7
'((contract (->i ([x number?]) #:pre-cond #t [res any/c] #:post-cond #t)
'((contract (->i ([x number?]) #:pre () #t [res any/c] #:post () #t)
(λ (x . y) x)
'pos 'neg)
1))
(test/spec-passed
'->i-optopt8
'((contract (->i ([x number?]) [res any/c] #:post-cond #t)
'((contract (->i ([x number?]) [res any/c] #:post () #t)
(λ (x . y) x)
'pos 'neg)
1))
@ -2368,7 +2376,7 @@
(test/spec-passed
'->i-binding1
'((contract (->i ([x number?]) () #:rest [rest any/c] [range any/c] #:post-cond (equal? rest '(2 3 4)))
'((contract (->i ([x number?]) () #:rest [rest any/c] [range any/c] #:post (rest) (equal? rest '(2 3 4)))
(λ (x . y) y)
'pos
'neg)
@ -2376,7 +2384,7 @@
(test/spec-passed
'->i-binding2
'((contract (->i ([x number?]) () #:rest [rest any/c] [range any/c] #:post-cond (equal? x 1))
'((contract (->i ([x number?]) () #:rest [rest any/c] [range any/c] #:post (x) (equal? x 1))
(λ (x . y) y)
'pos
'neg)
@ -2390,8 +2398,9 @@
((contract (->i ([x number?] [y number?] #:z [z number?] #:w [w number?])
([a number?] [b number?] #:c [c number?] #:d [d number?])
#:rest [rest any/c]
#:pre-cond (equal? (list x y z w a b c d rest p q r)
(list 1 2 3 4 5 6 7 8 '(z) 'p 'q 'r))
#:pre (x y z w a b c d rest)
(equal? (list x y z w a b c d rest p q r)
(list 1 2 3 4 5 6 7 8 '(z) 'p 'q 'r))
(values [p number?] [q number?] [r number?]))
(λ (x y #:z z #:w w [a 101] [b 102] #:c [c 103] #:d [d 104] . rest)
(values 11 12 13))
@ -2405,8 +2414,8 @@
([a number?] [b number?] #:c [c number?] #:d [d number?])
#:rest [rest any/c]
(values [p number?] [q number?] [r number?])
#:post-cond (equal? (list x y z w a b c d rest p q r)
(list 1 2 3 4 5 6 7 8 '(z) 11 12 13)))
#:post (equal? (list x y z w a b c d rest p q r)
(list 1 2 3 4 5 6 7 8 '(z) 11 12 13)))
(λ (x y #:z z #:w w [a 101] [b 102] #:c [c 103] #:d [d 104] . rest)
(values 11 12 13))
'pos
@ -2421,10 +2430,11 @@
((contract (->i ([x number?] [y number?] #:z [z number?] #:w [w number?])
([a number?] [b number?] #:c [c number?] #:d [d number?])
#:rest [rest any/c]
#:pre-cond (equal? (list x y z w a b c d rest p q r)
(list 1 2 3 4
the-unsupplied-arg the-unsupplied-arg the-unsupplied-arg the-unsupplied-arg
'() 'p 'q 'r))
#:pre (x y z w a b c d rest)
(equal? (list x y z w a b c d rest p q r)
(list 1 2 3 4
the-unsupplied-arg the-unsupplied-arg the-unsupplied-arg the-unsupplied-arg
'() 'p 'q 'r))
(values [p number?] [q number?] [r number?]))
(λ (x y #:z z #:w w [a 101] [b 102] #:c [c 103] #:d [d 104] . rest)
(values 11 12 13))
@ -2438,10 +2448,10 @@
([a number?] [b number?] #:c [c number?] #:d [d number?])
#:rest [rest any/c]
(values [p number?] [q number?] [r number?])
#:post-cond (equal? (list x y z w a b c d rest p q r)
(list 1 2 3 4
the-unsupplied-arg the-unsupplied-arg the-unsupplied-arg the-unsupplied-arg
'() 11 12 13)))
#:post (equal? (list x y z w a b c d rest p q r)
(list 1 2 3 4
the-unsupplied-arg the-unsupplied-arg the-unsupplied-arg the-unsupplied-arg
'() 11 12 13)))
(λ (x y #:z z #:w w [a 101] [b 102] #:c [c 103] #:d [d 104] . rest)
(values 11 12 13))
'pos
@ -2455,7 +2465,7 @@
([a number?])
#:rest [rest any/c]
[_ any/c]
#:post-cond (equal? (list a rest) (list the-unsupplied-arg '())))
#:post (equal? (list a rest) (list the-unsupplied-arg '())))
(λ ([a 1] . rest) 1)
'pos
'neg)))
@ -4964,7 +4974,7 @@
(test/spec-passed
'object-contract-->i-pp1
'(send (contract (object-contract (m (->i ([x number?]) () #:pre-cond #t [unused (x) (<=/c x)] #:post-cond #t)))
'(send (contract (object-contract (m (->i ([x number?]) () #:pre () #t [unused (x) (<=/c x)] #:post () #t)))
(new (class object% (define/public m (lambda (x) (- x 1))) (super-new)))
'pos
'neg)
@ -4973,7 +4983,7 @@
(test/spec-passed
'object-contract-->i-pp1b
'(send (contract (object-contract (m (->i ([x number?]) () #:pre-cond #t [unused (x) (<=/c x)] #:post-cond #t)))
'(send (contract (object-contract (m (->i ([x number?]) () #:pre () #t [unused (x) (<=/c x)] #:post () #t)))
(new (class object%
(define/public m (case-lambda [(x) (- x 1)]
[(x y) y]))
@ -4985,7 +4995,7 @@
(test/pos-blame
'object-contract-->i-pp2
'(send (contract (object-contract (m (->i ([x number?]) () #:pre-cond #t [unused (x) (<=/c x)] #:post-cond #t)))
'(send (contract (object-contract (m (->i ([x number?]) () #:pre () #t [unused (x) (<=/c x)] #:post () #t)))
(new (class object% (define/public m (lambda (x) (+ x 1))) (super-new)))
'pos
'neg)
@ -4994,7 +5004,7 @@
(test/pos-blame
'object-contract-->i-pp2b
'(send (contract (object-contract (m (->i ([x number?]) () #:pre-cond #t [unused (x) (<=/c x)] #:post-cond #t)))
'(send (contract (object-contract (m (->i ([x number?]) () #:pre () #t [unused (x) (<=/c x)] #:post () #t)))
(new (class object%
(define/public m (case-lambda [(x) (+ x 1)]))
(super-new)))
@ -5005,7 +5015,7 @@
(test/spec-passed
'object-contract-->i-pp3
'(send (contract (object-contract (m (->i () () #:rest [rst (listof number?)] #:pre-cond #t [unused any/c] #:post-cond #t)))
'(send (contract (object-contract (m (->i () () #:rest [rst (listof number?)] #:pre () #t [unused any/c] #:post () #t)))
(new (class object% (define/public m (lambda w 1)) (super-new)))
'pos
'neg)
@ -5014,7 +5024,7 @@
(test/neg-blame
'object-contract-->i-pp4
'(send (contract (object-contract (m (->i () () #:rest [rst (listof number?)] #:pre-cond #t [unused any/c] #:post-cond #t)))
'(send (contract (object-contract (m (->i () () #:rest [rst (listof number?)] #:pre () #t [unused any/c] #:post () #t)))
(new (class object% (define/public m (lambda w 1)) (super-new)))
'pos
'neg)
@ -5023,7 +5033,7 @@
(test/spec-passed
'object-contract-->i-pp5
'(send (contract (object-contract (m (->i () () #:pre-cond #t any)))
'(send (contract (object-contract (m (->i () () #:pre () #t any)))
(new (class object% (define/public m (lambda () 1)) (super-new)))
'pos
'neg)
@ -5031,7 +5041,7 @@
(test/spec-passed
'object-contract-->i-pp6
'(send (contract (object-contract (m (->i () () #:pre-cond #t (values [x number?] [y (x) (>=/c x)]) #:post-cond #t)))
'(send (contract (object-contract (m (->i () () #:pre () #t (values [x number?] [y (x) (>=/c x)]) #:post () #t)))
(new (class object% (define/public m (lambda () (values 1 2))) (super-new)))
'pos
'neg)
@ -5039,7 +5049,7 @@
(test/pos-blame
'object-contract-->i-pp7
'(send (contract (object-contract (m (->i () () #:pre-cond #t (values [x number?] [y (>=/c x)]) #:post-cond #t)))
'(send (contract (object-contract (m (->i () () #:pre () #t (values [x number?] [y (>=/c x)]) #:post () #t)))
(new (class object% (define/public m (lambda () (values 2 1))) (super-new)))
'pos
'neg)
@ -5049,9 +5059,9 @@
'object-contract-->i-pp/this-1
'(send (contract (object-contract (m (->i ()
()
#:pre-cond (= 1 (get-field f this))
#:pre () (= 1 (get-field f this))
[result-x any/c]
#:post-cond (= 2 (get-field f this)))))
#:post () (= 2 (get-field f this)))))
(new (class object% (field [f 2]) (define/public m (lambda () (set! f 3))) (super-new)))
'pos
'neg)
@ -5060,9 +5070,9 @@
(test/pos-blame
'object-contract-->i-pp/this-2
'(send (contract (object-contract (m (->i () ()
#:pre-cond (= 1 (get-field f this))
#:pre () (= 1 (get-field f this))
[result-x any/c]
#:post-cond (= 2 (get-field f this)))))
#:post () (= 2 (get-field f this)))))
(new (class object% (field [f 1]) (define/public m (lambda () (set! f 3))) (super-new)))
'pos
'neg)
@ -5071,9 +5081,9 @@
(test/spec-passed
'object-contract-->i-pp/this-3
'(send (contract (object-contract (m (->i () ()
#:pre-cond (= 1 (get-field f this))
#:pre () (= 1 (get-field f this))
[result-x any/c]
#:post-cond (= 2 (get-field f this)))))
#:post () (= 2 (get-field f this)))))
(new (class object% (field [f 1]) (define/public m (lambda () (set! f 2))) (super-new)))
'pos
'neg)
@ -5083,9 +5093,9 @@
'object-contract-->i-pp/this-4
'(send (contract (object-contract (m (->i () ()
#:rest [rest-id any/c]
#:pre-cond (= 1 (get-field f this))
#:pre () (= 1 (get-field f this))
[result-x any/c]
#:post-cond (= 2 (get-field f this)))))
#:post () (= 2 (get-field f this)))))
(new (class object% (field [f 2]) (define/public m (lambda args (set! f 3))) (super-new)))
'pos
'neg)
@ -5095,9 +5105,9 @@
'object-contract-->i-pp/this-5
'(send (contract (object-contract (m (->i () ()
#:rest [rest-id any/c]
#:pre-cond (= 1 (get-field f this))
#:pre () (= 1 (get-field f this))
[result-x any/c]
#:post-cond (= 2 (get-field f this)))))
#:post () (= 2 (get-field f this)))))
(new (class object% (field [f 1]) (define/public m (lambda args (set! f 3))) (super-new)))
'pos
'neg)
@ -5107,9 +5117,9 @@
'object-contract-->i-pp/this-6
'(send (contract (object-contract (m (->i () ()
#:rest [rest-id any/c]
#:pre-cond (= 1 (get-field f this))
#:pre () (= 1 (get-field f this))
[result-x any/c]
#:post-cond (= 2 (get-field f this)))))
#:post () (= 2 (get-field f this)))))
(new (class object% (field [f 1]) (define/public m (lambda args (set! f 2))) (super-new)))
'pos
'neg)
@ -8352,18 +8362,18 @@ so that propagation occurs.
(test-name '(->d ([x ...] #:y [y ...]) ([z ...] #:w [w ...]) any) (->d ([x integer?] #:y [y integer?]) ([z integer?] #:w [w integer?]) any))
(test-name '(->d () () (values [x ...] [y ...])) (->d () () (values [x number?] [y number?])))
(test-name '(->d () () [x ...]) (->d () () [q number?]))
(test-name '(->d () () #:pre-cond ... [x ...]) (->d () () #:pre-cond #t [q number?]))
(test-name '(->d () () #:pre-cond ... [x ...] #:post-cond ...) (->d () () #:pre-cond #t [q number?] #:post-cond #t))
(test-name '(->d () () [x ...] #:post-cond ...) (->d () () [q number?] #:post-cond #t))
(test-name '(->d () () #:pre ... [x ...]) (->d () () #:pre #t [q number?]))
(test-name '(->d () () #:pre ... [x ...] #:post ...) (->d () () #:pre #t [q number?] #:post #t))
(test-name '(->d () () [x ...] #:post ...) (->d () () [q number?] #:post #t))
#| ->i FIXME
(test-name '(->i () () any) (->i () () any))
(test-name '(->i ([x integer?] #:y [y integer?]) ([z integer?] #:w [w integer?]) any) (->i ([x integer?] #:y [y integer?]) ([z integer?] #:w [w integer?]) any))
(test-name '(->i () () (values [x ...] [y ...])) (->i () () (values [x number?] [y number?])))
(test-name '(->i () () [x ...]) (->i () () [q number?]))
(test-name '(->i () () #:pre-cond ... [x ...]) (->i () () #:pre-cond #t [q number?]))
(test-name '(->i () () #:pre-cond ... [x ...] #:post-cond ...) (->i () () #:pre-cond #t [q number?] #:post-cond #t))
(test-name '(->i () () [x ...] #:post-cond ...) (->i () () [q number?] #:post-cond #t))
(test-name '(->i () () #:pre ... [x ...]) (->i () () #:pre () #t [q number?]))
(test-name '(->i () () #:pre ... [x ...] #:post ...) (->i () () #:pre () #t [q number?] #:post () #t))
(test-name '(->i () () [x ...] #:post ...) (->i () () [q number?] #:post () #t))
|#
(test-name '(case->) (case->))