diff --git a/collects/racket/contract/private/arr-i-old.rkt b/collects/racket/contract/private/arr-i-old.rkt index da2dc6ab27..cafc586d73 100644 --- a/collects/racket/contract/private/arr-i-old.rkt +++ b/collects/racket/contract/private/arr-i-old.rkt @@ -29,7 +29,7 @@ (values '() leftover)] [(dep-range) (values '() leftover)] - [(dep-range #:post expr) + [(dep-range #:post . more) (values '() leftover)] [((opts ...) . rest) (values #'(opts ...) #'rest)] diff --git a/collects/racket/contract/private/arr-i-parse.rkt b/collects/racket/contract/private/arr-i-parse.rkt index 23b473deb8..945ab182b5 100644 --- a/collects/racket/contract/private/arr-i-parse.rkt +++ b/collects/racket/contract/private/arr-i-parse.rkt @@ -19,9 +19,9 @@ code does the parsing and validation of the syntax. ;; args : (listof arg?) ;; rst : (or/c #f rst?) -;; pre : (or/c stx[expr] #f) +;; pre : (or/c pre/post? #f) ;; ress : (or/c #f (listof eres?) (listof lres?)) -;; post : (or/c stx[expr] #f) +;; post : (or/c pre/post? #f) (struct istx (args rst pre ress post)) ;; NOTE: the ress field may contain a mixture of eres and lres structs ;; but only temporarily; in that case, a syntax error @@ -52,6 +52,10 @@ code does the parsing and validation of the syntax. ;; ctc : syntax[expr] (struct rst (var vars ctc)) +;; vars : (listof identifier?) +;; exp : syntax[expr] +(struct pre/post (vars exp)) + (define (parse-->i stx) (let-values ([(raw-mandatory-doms raw-optional-doms id/rest-id pre-cond range post-cond) @@ -99,12 +103,15 @@ code does the parsing and validation of the syntax. stx var)))) ;; not-range-bound : (listof identifier[used-by-an-arg]) -> void - (define (not-range-bound arg-vars) + (define (not-range-bound arg-vars arg?) (when (istx-ress istx) (for ([arg-var (in-list arg-vars)]) (when (ormap (λ (a-res) (free-identifier=? (res-var a-res) arg-var)) (istx-ress istx)) - (raise-syntax-error #f "an argument cannot depend on a result" + (raise-syntax-error #f + (if arg? + "an argument cannot depend on a result" + "the #:pre condition cannot depend on a result") stx arg-var))))) ;; no dups in the domains @@ -134,7 +141,7 @@ code does the parsing and validation of the syntax. ;; no dups in the rest var (when (istx-rst istx) (when (rst-vars (istx-rst istx)) - (not-range-bound (rst-vars (istx-rst istx)))) + (not-range-bound (rst-vars (istx-rst istx)) #t)) (no-var-dups (rst-var (istx-rst istx)))) ;; dependent arg variables are all bound, but not to a range variable @@ -142,13 +149,24 @@ code does the parsing and validation of the syntax. (let ([a-vars (arg-vars an-arg)]) (when a-vars (ensure-bound a-vars) - (not-range-bound a-vars)))) + (not-range-bound a-vars #t)))) + ;; pre-condition variables are all bound, but not to a range variable + (when (istx-pre istx) + (let ([vars (pre/post-vars (istx-pre istx))]) + (ensure-bound vars) + (not-range-bound vars #f))) + ;; dependent range variables are all bound. (when (istx-ress istx) (for ([a-res (in-list (istx-ress istx))]) (when (res-vars a-res) - (ensure-bound (res-vars a-res))))))) + (ensure-bound (res-vars a-res))))) + + ;; post-condition variables are all bound + (when (istx-post istx) + (let ([vars (pre/post-vars (istx-post istx))]) + (ensure-bound vars))))) (define (ensure-no-cycles stx istx) (let ([neighbors (make-free-identifier-mapping)] @@ -312,7 +330,7 @@ code does the parsing and validation of the syntax. (values '() leftover)] [(dep-range) (values '() leftover)] - [(dep-range #:post expr) + [(dep-range #:post . stuff) (values '() leftover)] [((opts ...) . rest) (values #'(opts ...) #'rest)] @@ -349,11 +367,15 @@ code does the parsing and validation of the syntax. [(#:pre (id ...) pre-cond . leftover) (begin (for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...))) - (values #'pre-cond #'leftover))] + (values (pre/post (syntax->list #'(id ...)) #'pre-cond) #'leftover))] [_ (values #f leftover)])] [(range leftover) (syntax-case leftover () - [(range . leftover) (values #'range #'leftover)] + [(range . leftover) + (not (keyword? (syntax-e #'range))) + (values #'range #'leftover)] + [(a . b) + (raise-syntax-error #f "expected a range expression" stx #'a)] [() (raise-syntax-error #f "expected a range expression, but found nothing" stx leftover)])] [(post-cond leftover) @@ -364,7 +386,7 @@ code does the parsing and validation of the syntax. (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))] + (values (pre/post (syntax->list #'(id ...)) #'post-cond) #'leftover))] [_ (values #f leftover)])]) (syntax-case leftover () [() diff --git a/collects/racket/contract/scratch.rkt b/collects/racket/contract/scratch.rkt index b217f02c15..ad2ff19ef2 100644 --- a/collects/racket/contract/scratch.rkt +++ b/collects/racket/contract/scratch.rkt @@ -2,6 +2,7 @@ (require racket/contract racket/pretty) +#; (->i ([x number?]) [res any/c] #:post () #t) #; @@ -116,6 +117,14 @@ test cases: any) ; => unknown dependent variable + +(->i ([x number?]) #:pre (y) #t any) +;; => unknown dependent variable + + +(->i ([x number?]) #:pre (x) #t [res any/c] #:post (y) #t) +;; => unknown dependent variable + (->i ([x (y) number?]) [y number?]) ; => domain cannot depend on a range variable @@ -125,6 +134,9 @@ test cases: [y number?]) ; => domain cannot depend on a range variable +(->i ([x number?]) #:pre (res) #t [res any/c] #:post (x) #t) +;; => pre cannot depend on a range variables + (->i ([x (x) number?]) any) ; => cyclic dependencies not allowed diff --git a/collects/tests/racket/contract-test.rktl b/collects/tests/racket/contract-test.rktl index d22dfbb2df..ac807eae9d 100644 --- a/collects/tests/racket/contract-test.rktl +++ b/collects/tests/racket/contract-test.rktl @@ -2304,7 +2304,7 @@ '->i-protect-shared-state '(let ([x 1]) ((contract (let ([save #f]) - (-> (->i () () #:pre (x) (set! save x) [range any/c] #:post (x) (= save x)) + (-> (->i () () #:pre () (set! save x) [range any/c] #:post () (= save x)) any)) (λ (t) (t)) 'pos @@ -2414,8 +2414,9 @@ ([a number?] [b number?] #:c [c number?] #:d [d number?]) #:rest [rest any/c] (values [p number?] [q number?] [r number?]) - #: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))) + #:post (x y z w a b c d) + (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 @@ -2448,10 +2449,11 @@ ([a number?] [b number?] #:c [c number?] #:d [d number?]) #:rest [rest any/c] (values [p number?] [q number?] [r number?]) - #: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))) + #:post (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 + '() 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 @@ -2465,7 +2467,7 @@ ([a number?]) #:rest [rest any/c] [_ any/c] - #:post (equal? (list a rest) (list the-unsupplied-arg '()))) + #:post (a) (equal? (list a rest) (list the-unsupplied-arg '()))) (λ ([a 1] . rest) 1) 'pos 'neg)))