From 94d80f0171d7da2cda40508d831f930d2c4939a4 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Mon, 22 Dec 2014 22:31:17 -0600 Subject: [PATCH] add #:pre/desc and #:post/desc to ->i --- .../scribblings/reference/contracts.scrbl | 11 +- .../tests/racket/contract/arrow-i.rkt | 36 +++++ .../tests/racket/contract/name.rkt | 4 + .../racket/contract/private/arr-i-parse.rkt | 72 +++++++--- .../racket/contract/private/arr-i.rkt | 136 +++++++++++------- .../contract/private/arrow-higher-order.rkt | 53 +++---- 6 files changed, 213 insertions(+), 99 deletions(-) diff --git a/pkgs/racket-doc/scribblings/reference/contracts.scrbl b/pkgs/racket-doc/scribblings/reference/contracts.scrbl index cf73a985ac..8d8ae75374 100644 --- a/pkgs/racket-doc/scribblings/reference/contracts.scrbl +++ b/pkgs/racket-doc/scribblings/reference/contracts.scrbl @@ -1049,6 +1049,8 @@ symbols, and that return a symbol. [pre-condition (code:line) (code:line #:pre (id ...) boolean-expr pre-condition) + (code:line #:pre/desc (id ...) + expr pre-condition) (code:line #:pre/name (id ...) string boolean-expr pre-condition)] [dependent-range any @@ -1059,6 +1061,8 @@ symbols, and that return a symbol. [post-condition (code:line) (code:line #:post (id ...) boolean-expr post-condition) + (code:line #:post/desc (id ...) + expr post-condition) (code:line #:post/name (id ...) string boolean-expr post-condition)] [id+ctc [id contract-expr] @@ -1068,10 +1072,9 @@ symbols, and that return a symbol. )]{ The @racket[->i] contract combinator differs from the @racket[->*] -combinator in that the support pre- and post-condition clauses and -in that each argument and result is named. These names can then +combinator in that each argument and result is named and these names can be used in the subcontracts and in the pre-/post-condition clauses. -In short, contracts now express dependencies among arguments and results. +In other words, @racket[->i] expresses dependencies among arguments and results. 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 @@ -1079,6 +1082,8 @@ 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 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]. +If @racket[#:pre/desc] or @racket[#:post/desc] is used, the the result of +the expression is treated the same way as @racket[->*]. The @racket[dependent-range] non-terminal specifies the possible result contracts. If it is @racket[any], then any value is allowed. Otherwise, the diff --git a/pkgs/racket-test/tests/racket/contract/arrow-i.rkt b/pkgs/racket-test/tests/racket/contract/arrow-i.rkt index 7cb60c55de..26b464272f 100644 --- a/pkgs/racket-test/tests/racket/contract/arrow-i.rkt +++ b/pkgs/racket-test/tests/racket/contract/arrow-i.rkt @@ -646,6 +646,20 @@ 'pos 'neg) (cons #f 1))) + (test/neg-blame + '->i35-g + '((contract (->i ([x any/c]) #:pre/desc (x) (pair? x) #:pre/desc (x) (car x) any) + (λ (x) 1) + 'pos 'neg) + (cons #f 1))) + + (test/neg-blame + '->i35-h + '((contract (->i ([x any/c]) #:pre/desc (x) '("x") any) + (λ (x) 1) + 'pos 'neg) + (cons #f 1))) + (test/spec-passed/result '->i36 '((contract (->i ([f (-> number? number?)]) [res number?]) @@ -802,6 +816,28 @@ 'neg) (cons #f 1))) + (test/pos-blame + '->i47-f + '((contract (->i ([x any/c]) + [y () any/c] + #:post/desc (y) (pair? y) + #:post/desc (y) (car y)) + (lambda (x) x) + 'pos + 'neg) + (cons #f 1))) + + (test/pos-blame + '->i47-g + '((contract (->i ([x any/c]) + [y () any/c] + #:post/desc (y) (pair? y) + #:post/desc (y) "x") + (lambda (x) x) + 'pos + 'neg) + (cons #f 1))) + (test/spec-passed/result '->i48 '(let ([x '()]) diff --git a/pkgs/racket-test/tests/racket/contract/name.rkt b/pkgs/racket-test/tests/racket/contract/name.rkt index a71b58ac94..e1cc20e617 100644 --- a/pkgs/racket-test/tests/racket/contract/name.rkt +++ b/pkgs/racket-test/tests/racket/contract/name.rkt @@ -98,6 +98,8 @@ (->i () #:pre () #t [q number?])) (test-name '(->i () #:pre () #t [q () number?] #:post () #t) (->i () #:pre () #t [q () number?] #:post () #t)) + (test-name '(->i () #:pre () #t [q () number?] #:post/desc () #t) + (->i () #:pre () #t [q () number?] #:post/desc () #t)) (test-name '(->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) (>/c x)]) @@ -108,6 +110,8 @@ #:post/name (y) "car" (car y)) (->i ([x any/c]) [y () any/c] #:post/name (y) "pair" (pair? y) #:post/name (y) "car" (car y))) + (test-name '(->i () #:pre/desc () #t [q number?]) + (->i () #:pre/desc () #t [q number?])) (test-name '(->i ([p any/c] [q (p) (if (equal? p 10) 'aha any/c)]) #:rest [rest (p) (if (equal? p 11) 'aha any/c)] diff --git a/racket/collects/racket/contract/private/arr-i-parse.rkt b/racket/collects/racket/contract/private/arr-i-parse.rkt index 35afc1c6fe..ea40a51658 100644 --- a/racket/collects/racket/contract/private/arr-i-parse.rkt +++ b/racket/collects/racket/contract/private/arr-i-parse.rkt @@ -49,8 +49,11 @@ code does the parsing and validation of the syntax. ;; vars : (listof identifier?) ;; exp : syntax[expr] -;; str : (or/c #f syntax[expr]) -(struct pre/post (vars str exp quoted-dep-src-code) #:transparent) +;; kind : (or/c syntax[expr] 'desc 'bool) +;; syntax => #:pre/name, where the syntax object holds the literal string +;; 'desc => #:pre/desc or #:post/desc +;; 'bool => #:pre or #:post +(struct pre/post (vars kind exp quoted-dep-src-code) #:transparent) (define (parse-->i stx) (if (identifier? stx) @@ -375,6 +378,8 @@ code does the parsing and validation of the syntax. (values '() leftover)] [(dep-range #:post . stuff) (values '() leftover)] + [(dep-range #:post/desc . stuff) + (values '() leftover)] [(dep-range #:post/name . stuff) (values '() leftover)] [((opts ...) . rest) @@ -412,27 +417,38 @@ code does the parsing and validation of the syntax. (let loop ([leftover leftover] [conditions '()]) (syntax-case leftover () - [(#:pre (id ...) pre-cond . pre-leftover) + [(kwd (id ...) pre-cond . pre-leftover) + (or (equal? (syntax-e #'kwd) '#:pre) + (equal? (syntax-e #'kwd) '#:pre/desc)) (begin (syntax-case #'pre-leftover () [() (raise-syntax-error #f - (string-append - "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") + (format + (string-append + "expected ~a to be followed by at least three subterms" + " (a sequence of identifiers, the pre-condition, and the" + " range contract), but found only two") + (syntax-e #'kwd)) stx (car (syntax->list leftover)))] [x (void)]) (for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...))) (loop #'pre-leftover - (cons (pre/post (syntax->list #'(id ...)) #f #'pre-cond + (cons (pre/post (syntax->list #'(id ...)) + (if (equal? '#:pre/desc (syntax-e #'kwd)) + 'desc + 'bool) + #'pre-cond (compute-quoted-src-expression #'pre-cond)) conditions)))] - [(#:pre . rest) + [(kwd . rest) + (or (equal? (syntax-e #'kwd) '#:pre) + (equal? (syntax-e #'kwd) '#:pre/desc)) (raise-syntax-error #f - "expected a sequence of identifiers and an expression to follow #:pre" + (format "expected a sequence of identifiers and an expression to follow ~a" + (syntax-e #'kwd)) stx (car (syntax->list leftover)))] [(#:pre/name (id ...) str pre-cond . pre-leftover) @@ -455,7 +471,9 @@ code does the parsing and validation of the syntax. stx #'str)) (loop #'pre-leftover - (cons (pre/post (syntax->list #'(id ...)) (syntax-e #'str) #'pre-cond + (cons (pre/post (syntax->list #'(id ...)) + (syntax-e #'str) + #'pre-cond (compute-quoted-src-expression #'pre-cond)) conditions)))] [(#:pre/name . rest) @@ -481,25 +499,43 @@ code does the parsing and validation of the syntax. (let loop ([leftover leftover] [post-conds '()]) (syntax-case leftover () - [(#:post (id ...) post-cond . leftover) + [(kwd (id ...) post-cond . leftover) + (or (equal? (syntax-e #'kwd) '#:post/desc) + (equal? (syntax-e #'kwd) '#:post)) (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)] + #f + (format "cannot have a ~a with any as the range" + (syntax-e #'kwd)) + stx #'post-cond)] [_ (void)]) (loop #'leftover - (cons (pre/post (syntax->list #'(id ...)) #f #'post-cond + (cons (pre/post (syntax->list #'(id ...)) + (if (equal? (syntax-e #'kwd) '#:post/desc) + 'desc + 'bool) + #'post-cond (compute-quoted-src-expression #'post-cond)) post-conds)))] - [(#:post a b . stuff) + [(kwd a b . stuff) + (or (equal? (syntax-e #'kwd) '#:post/desc) + (equal? (syntax-e #'kwd) '#:post)) (begin (raise-syntax-error - #f "expected a sequence of variables to follow #:post" stx #'a))] - [(#:post a) + #f + (format "expected a sequence of variables to follow ~a" + (syntax-e #'kwd)) + stx #'a))] + [(kwd a) + (or (equal? (syntax-e #'kwd) '#:post/desc) + (equal? (syntax-e #'kwd) '#:post)) (begin (raise-syntax-error - #f "expected a sequence of variables and an expression to follow #:post" + #f + (format "expected a sequence of variables and an expression to follow ~a" + (syntax-e #'kwd)) stx #'a))] [(#:post/name (id ...) str post-cond . leftover) (begin diff --git a/racket/collects/racket/contract/private/arr-i.rkt b/racket/collects/racket/contract/private/arr-i.rkt index 9ab3284a6e..eed7834476 100644 --- a/racket/collects/racket/contract/private/arr-i.rkt +++ b/racket/collects/racket/contract/private/arr-i.rkt @@ -7,6 +7,7 @@ "misc.rkt" "blame.rkt" "generate.rkt" + "arrow-higher-order.rkt" syntax/location racket/private/performance-hint (for-syntax racket/base @@ -263,9 +264,13 @@ (define ids (list-ref pre-info 0)) (define name (list-ref pre-info 1)) (define code (list-ref pre-info 2)) - (if name - `(#:pre/name ,ids ,name ,code) - `(#:pre ,ids ,code)))) + (cond + [(string? name) + `(#:pre/name ,ids ,name ,code)] + [(equal? name 'bool) + `(#:pre ,ids ,code)] + [(equal? name 'desc) + `(#:pre/desc ,ids ,code)]))) ,(cond [(not rng-info) 'any] @@ -285,9 +290,13 @@ (define ids (list-ref post-info 0)) (define name (list-ref post-info 1)) (define code (list-ref post-info 2)) - (if name - `(#:post/name ,ids ,name ,code) - `(#:post ,ids ,code))))))) + (cond + [(string? name) + `(#:post/name ,ids ,name ,code)] + [(equal? name 'bool) + `(#:post ,ids ,code)] + [(equal? name 'desc) + `(#:post/desc ,ids ,code)])))))) #:first-order (λ (ctc) (let ([has-rest (->i-rest ctc)] @@ -540,44 +549,58 @@ evaluted left-to-right.) (define-for-syntax (maybe-generate-temporary x) (and x (car (generate-temporaries (list x))))) -(define (signal-pre/post pre? val str blame . var-infos) - (define pre-str (or str - (string-append - (if pre? "#:pre" "#:post") - " condition violation" - (if (null? var-infos) - "" - "; variables are:")))) - (raise-blame-error blame val - (apply - string-append - pre-str - (for/list ([var-info (in-list var-infos)]) - (format "\n ~s: ~e" - (list-ref var-info 0) - (list-ref var-info 1)))))) +(define (signal-pre/post pre? val kind blame condition-result . var-infos) + (define vars-str + (apply + string-append + (for/list ([var-info (in-list var-infos)]) + (format "\n ~s: ~e" + (list-ref var-info 0) + (list-ref var-info 1))))) + (define msg + (cond + [(string? kind) (string-append kind vars-str)] + [(or (equal? kind 'bool) + (and (equal? kind 'desc) + (equal? condition-result #f))) + (string-append + (if pre? "#:pre" "#:post") + " condition violation" + (if (null? var-infos) + "" + "; variables are:") + vars-str)] + [else + (pre-post/desc-result->string condition-result pre? '->i)])) + (raise-blame-error blame val "~a" msg)) (define-for-syntax (add-pre-cond an-istx indy-arg-vars ordered-args indy-res-vars ordered-ress call-stx) #`(begin #,@(for/list ([pre (in-list (istx-pre an-istx))] [i (in-naturals)]) (define id (string->symbol (format "pre-proc~a" i))) - #`(unless (#,id #,@(map (λ (var) (arg/res-to-indy-var indy-arg-vars - ordered-args - indy-res-vars - ordered-ress - var)) - (pre/post-vars pre))) - (signal-pre/post #t - val - #,(pre/post-str pre) - swapped-blame - #,@(map (λ (x) #`(list '#,x #,(arg/res-to-indy-var indy-arg-vars - ordered-args - indy-res-vars - ordered-ress - x))) - (pre/post-vars pre))))) + #`(let ([condition-result + (#,id #,@(map (λ (var) (arg/res-to-indy-var indy-arg-vars + ordered-args + indy-res-vars + ordered-ress + var)) + (pre/post-vars pre)))]) + (unless #,(if (equal? (pre/post-kind pre) 'desc) + #'(equal? condition-result #t) + #'condition-result) + (signal-pre/post #t + val + '#,(pre/post-kind pre) + swapped-blame + condition-result + #,@(map (λ (x) #`(list '#,x + #,(arg/res-to-indy-var indy-arg-vars + ordered-args + indy-res-vars + ordered-ress + x))) + (pre/post-vars pre)))))) #,call-stx)) (define-for-syntax (add-post-cond an-istx indy-arg-vars ordered-args indy-res-vars ordered-ress @@ -585,23 +608,28 @@ evaluted left-to-right.) #`(begin #,@(for/list ([post (in-list (istx-post an-istx))] [i (in-naturals)]) (define id (string->symbol (format "post-proc~a" i))) - #`(unless (#,id #,@(map (λ (var) (arg/res-to-indy-var indy-arg-vars + #`(let ([condition-result + (#,id #,@(map (λ (var) (arg/res-to-indy-var indy-arg-vars + ordered-args + indy-res-vars + ordered-ress + var)) + (pre/post-vars post)))]) + (unless #,(if (equal? (pre/post-kind post) 'desc) + #'(equal? condition-result #t) + #'condition-result) + (signal-pre/post + #f + val + '#,(pre/post-kind post) + blame + condition-result + #,@(map (λ (x) #`(list '#,x #,(arg/res-to-indy-var indy-arg-vars ordered-args indy-res-vars ordered-ress - var)) - (pre/post-vars post))) - (signal-pre/post - #f - val - #,(pre/post-str post) - blame - #,@(map (λ (x) #`(list '#,x #,(arg/res-to-indy-var indy-arg-vars - ordered-args - indy-res-vars - ordered-ress - x))) - (pre/post-vars post))))) + x))) + (pre/post-vars post)))))) #,call-stx)) ;; add-wrapper-let : @@ -1254,7 +1282,7 @@ evaluted left-to-right.) #f) #,(for/list ([pre (in-list (istx-pre an-istx))]) (list (map syntax-e (pre/post-vars pre)) - (pre/post-str pre) + (pre/post-kind pre) (pre/post-quoted-dep-src-code pre))) #,(and (istx-ress an-istx) (for/list ([a-res (in-list (istx-ress an-istx))]) @@ -1270,7 +1298,7 @@ evaluted left-to-right.) ,(arg/res-quoted-dep-src-code a-res)))) #,(for/list ([post (in-list (istx-post an-istx))]) (list (map syntax-e (pre/post-vars post)) - (pre/post-str post) + (pre/post-kind post) (pre/post-quoted-dep-src-code post))))) 'racket/contract:contract (let () diff --git a/racket/collects/racket/contract/private/arrow-higher-order.rkt b/racket/collects/racket/contract/private/arrow-higher-order.rkt index b5f18cd2be..ecdbfaf845 100644 --- a/racket/collects/racket/contract/private/arrow-higher-order.rkt +++ b/racket/collects/racket/contract/private/arrow-higher-order.rkt @@ -14,7 +14,8 @@ (provide (for-syntax build-chaperone-constructor/real) ->-proj check-pre-cond - check-post-cond) + check-post-cond + pre-post/desc-result->string) (define-for-syntax (build-chaperone-constructor/real this-args mandatory-dom-projs @@ -79,33 +80,37 @@ (void)] [else (define msg - (cond - [(equal? condition-result #f) - (if pre? - "#:pre condition" - "#:post condition")] - [(string? condition-result) condition-result] - [(and (list? condition-result) - (andmap string? condition-result)) - (apply - string-append - (let loop ([s condition-result]) - (cond - [(null? s) '()] - [(null? (cdr s)) s] - [else (list* (car s) - "\n " - (loop (cdr s)))])))] - [else - (error - '->* - "expected #:~a/desc to produce (or/c boolean? string? (listof string?)), got ~e" - (if pre? "pre" "post") - condition-result)])) + (pre-post/desc-result->string condition-result pre? '->*)) (raise-blame-error (if pre? (blame-swap blame) blame) #:missing-party neg-party val "~a" msg)])) +(define (pre-post/desc-result->string condition-result pre? who) + (cond + [(equal? condition-result #f) + (if pre? + "#:pre condition" + "#:post condition")] + [(string? condition-result) + condition-result] + [(and (list? condition-result) + (andmap string? condition-result)) + (apply + string-append + (let loop ([s condition-result]) + (cond + [(null? s) '()] + [(null? (cdr s)) s] + [else (list* (car s) + "\n " + (loop (cdr s)))])))] + [else + (error + who + "expected #:~a/desc to produce (or/c boolean? string? (listof string?)), got ~e" + (if pre? "pre" "post") + condition-result)])) + (define-for-syntax (create-chaperone blame val this-args doms opt-doms