add #:pre/desc and #:post/desc to ->i

This commit is contained in:
Robby Findler 2014-12-22 22:31:17 -06:00
parent 9d58a067e3
commit 94d80f0171
6 changed files with 213 additions and 99 deletions

View File

@ -1049,6 +1049,8 @@ symbols, and that return a symbol.
[pre-condition (code:line) [pre-condition (code:line)
(code:line #:pre (id ...) (code:line #:pre (id ...)
boolean-expr pre-condition) boolean-expr pre-condition)
(code:line #:pre/desc (id ...)
expr pre-condition)
(code:line #:pre/name (id ...) (code:line #:pre/name (id ...)
string boolean-expr pre-condition)] string boolean-expr pre-condition)]
[dependent-range any [dependent-range any
@ -1059,6 +1061,8 @@ symbols, and that return a symbol.
[post-condition (code:line) [post-condition (code:line)
(code:line #:post (id ...) (code:line #:post (id ...)
boolean-expr post-condition) boolean-expr post-condition)
(code:line #:post/desc (id ...)
expr post-condition)
(code:line #:post/name (id ...) (code:line #:post/name (id ...)
string boolean-expr post-condition)] string boolean-expr post-condition)]
[id+ctc [id contract-expr] [id+ctc [id contract-expr]
@ -1068,10 +1072,9 @@ symbols, and that return a symbol.
)]{ )]{
The @racket[->i] contract combinator differs from the @racket[->*] The @racket[->i] contract combinator differs from the @racket[->*]
combinator in that the support pre- and post-condition clauses and combinator in that each argument and result is named and these names can
in that each argument and result is named. These names can then
be used in the subcontracts and in the pre-/post-condition clauses. 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 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
@ -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 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 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]. 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 The @racket[dependent-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

View File

@ -646,6 +646,20 @@
'pos 'neg) 'pos 'neg)
(cons #f 1))) (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 (test/spec-passed/result
'->i36 '->i36
'((contract (->i ([f (-> number? number?)]) [res number?]) '((contract (->i ([f (-> number? number?)]) [res number?])
@ -802,6 +816,28 @@
'neg) 'neg)
(cons #f 1))) (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 (test/spec-passed/result
'->i48 '->i48
'(let ([x '()]) '(let ([x '()])

View File

@ -98,6 +98,8 @@
(->i () #:pre () #t [q number?])) (->i () #:pre () #t [q number?]))
(test-name '(->i () #:pre () #t [q () number?] #:post () #t) (test-name '(->i () #:pre () #t [q () number?] #:post () #t)
(->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) (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)) (->i ([x integer?]) #:pre (x) #t [q (x) number?] #:post (x) #t))
(test-name '(->i ([x real?]) [_ (x) (>/c x)]) (test-name '(->i ([x real?]) [_ (x) (>/c x)])
@ -108,6 +110,8 @@
#:post/name (y) "car" (car y)) #:post/name (y) "car" (car y))
(->i ([x any/c]) [y () any/c] #:post/name (y) "pair" (pair? y) (->i ([x any/c]) [y () any/c] #:post/name (y) "pair" (pair? y)
#:post/name (y) "car" (car 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] (test-name '(->i ([p any/c]
[q (p) (if (equal? p 10) 'aha any/c)]) [q (p) (if (equal? p 10) 'aha any/c)])
#:rest [rest (p) (if (equal? p 11) 'aha any/c)] #:rest [rest (p) (if (equal? p 11) 'aha any/c)]

View File

@ -49,8 +49,11 @@ code does the parsing and validation of the syntax.
;; vars : (listof identifier?) ;; vars : (listof identifier?)
;; exp : syntax[expr] ;; exp : syntax[expr]
;; str : (or/c #f syntax[expr]) ;; kind : (or/c syntax[expr] 'desc 'bool)
(struct pre/post (vars str exp quoted-dep-src-code) #:transparent) ;; 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) (define (parse-->i stx)
(if (identifier? stx) (if (identifier? stx)
@ -375,6 +378,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/desc . stuff)
(values '() leftover)]
[(dep-range #:post/name . stuff) [(dep-range #:post/name . stuff)
(values '() leftover)] (values '() leftover)]
[((opts ...) . rest) [((opts ...) . rest)
@ -412,27 +417,38 @@ code does the parsing and validation of the syntax.
(let loop ([leftover leftover] (let loop ([leftover leftover]
[conditions '()]) [conditions '()])
(syntax-case leftover () (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 (begin
(syntax-case #'pre-leftover () (syntax-case #'pre-leftover ()
[() (raise-syntax-error [() (raise-syntax-error
#f #f
(string-append (format
"expected #:pre to be followed by at least three subterms" (string-append
" (a sequence of identifiers, the pre-condition, and the" "expected ~a to be followed by at least three subterms"
" range contract), but found only two") " (a sequence of identifiers, the pre-condition, and the"
" range contract), but found only two")
(syntax-e #'kwd))
stx stx
(car (syntax->list leftover)))] (car (syntax->list leftover)))]
[x (void)]) [x (void)])
(for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...))) (for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...)))
(loop #'pre-leftover (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)) (compute-quoted-src-expression #'pre-cond))
conditions)))] conditions)))]
[(#:pre . rest) [(kwd . rest)
(or (equal? (syntax-e #'kwd) '#:pre)
(equal? (syntax-e #'kwd) '#:pre/desc))
(raise-syntax-error (raise-syntax-error
#f #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 stx
(car (syntax->list leftover)))] (car (syntax->list leftover)))]
[(#:pre/name (id ...) str pre-cond . pre-leftover) [(#:pre/name (id ...) str pre-cond . pre-leftover)
@ -455,7 +471,9 @@ code does the parsing and validation of the syntax.
stx stx
#'str)) #'str))
(loop #'pre-leftover (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)) (compute-quoted-src-expression #'pre-cond))
conditions)))] conditions)))]
[(#:pre/name . rest) [(#:pre/name . rest)
@ -481,25 +499,43 @@ code does the parsing and validation of the syntax.
(let loop ([leftover leftover] (let loop ([leftover leftover]
[post-conds '()]) [post-conds '()])
(syntax-case leftover () (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 (begin
(for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...))) (for-each (λ (x) (check-id stx x)) (syntax->list #'(id ...)))
(syntax-case range (any) (syntax-case range (any)
[any (raise-syntax-error [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)]) [_ (void)])
(loop #'leftover (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)) (compute-quoted-src-expression #'post-cond))
post-conds)))] post-conds)))]
[(#:post a b . stuff) [(kwd a b . stuff)
(or (equal? (syntax-e #'kwd) '#:post/desc)
(equal? (syntax-e #'kwd) '#:post))
(begin (begin
(raise-syntax-error (raise-syntax-error
#f "expected a sequence of variables to follow #:post" stx #'a))] #f
[(#:post a) (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 (begin
(raise-syntax-error (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))] stx #'a))]
[(#:post/name (id ...) str post-cond . leftover) [(#:post/name (id ...) str post-cond . leftover)
(begin (begin

View File

@ -7,6 +7,7 @@
"misc.rkt" "misc.rkt"
"blame.rkt" "blame.rkt"
"generate.rkt" "generate.rkt"
"arrow-higher-order.rkt"
syntax/location syntax/location
racket/private/performance-hint racket/private/performance-hint
(for-syntax racket/base (for-syntax racket/base
@ -263,9 +264,13 @@
(define ids (list-ref pre-info 0)) (define ids (list-ref pre-info 0))
(define name (list-ref pre-info 1)) (define name (list-ref pre-info 1))
(define code (list-ref pre-info 2)) (define code (list-ref pre-info 2))
(if name (cond
`(#:pre/name ,ids ,name ,code) [(string? name)
`(#:pre ,ids ,code)))) `(#:pre/name ,ids ,name ,code)]
[(equal? name 'bool)
`(#:pre ,ids ,code)]
[(equal? name 'desc)
`(#:pre/desc ,ids ,code)])))
,(cond ,(cond
[(not rng-info) [(not rng-info)
'any] 'any]
@ -285,9 +290,13 @@
(define ids (list-ref post-info 0)) (define ids (list-ref post-info 0))
(define name (list-ref post-info 1)) (define name (list-ref post-info 1))
(define code (list-ref post-info 2)) (define code (list-ref post-info 2))
(if name (cond
`(#:post/name ,ids ,name ,code) [(string? name)
`(#:post ,ids ,code))))))) `(#:post/name ,ids ,name ,code)]
[(equal? name 'bool)
`(#:post ,ids ,code)]
[(equal? name 'desc)
`(#:post/desc ,ids ,code)]))))))
#:first-order #:first-order
(λ (ctc) (λ (ctc)
(let ([has-rest (->i-rest ctc)] (let ([has-rest (->i-rest ctc)]
@ -540,44 +549,58 @@ evaluted left-to-right.)
(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 (signal-pre/post pre? val str blame . var-infos) (define (signal-pre/post pre? val kind blame condition-result . var-infos)
(define pre-str (or str (define vars-str
(string-append (apply
(if pre? "#:pre" "#:post") string-append
" condition violation" (for/list ([var-info (in-list var-infos)])
(if (null? var-infos) (format "\n ~s: ~e"
"" (list-ref var-info 0)
"; variables are:")))) (list-ref var-info 1)))))
(raise-blame-error blame val (define msg
(apply (cond
string-append [(string? kind) (string-append kind vars-str)]
pre-str [(or (equal? kind 'bool)
(for/list ([var-info (in-list var-infos)]) (and (equal? kind 'desc)
(format "\n ~s: ~e" (equal? condition-result #f)))
(list-ref var-info 0) (string-append
(list-ref var-info 1)))))) (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 (define-for-syntax (add-pre-cond an-istx indy-arg-vars ordered-args indy-res-vars ordered-ress
call-stx) call-stx)
#`(begin #,@(for/list ([pre (in-list (istx-pre an-istx))] #`(begin #,@(for/list ([pre (in-list (istx-pre an-istx))]
[i (in-naturals)]) [i (in-naturals)])
(define id (string->symbol (format "pre-proc~a" i))) (define id (string->symbol (format "pre-proc~a" i)))
#`(unless (#,id #,@(map (λ (var) (arg/res-to-indy-var indy-arg-vars #`(let ([condition-result
ordered-args (#,id #,@(map (λ (var) (arg/res-to-indy-var indy-arg-vars
indy-res-vars ordered-args
ordered-ress indy-res-vars
var)) ordered-ress
(pre/post-vars pre))) var))
(signal-pre/post #t (pre/post-vars pre)))])
val (unless #,(if (equal? (pre/post-kind pre) 'desc)
#,(pre/post-str pre) #'(equal? condition-result #t)
swapped-blame #'condition-result)
#,@(map (λ (x) #`(list '#,x #,(arg/res-to-indy-var indy-arg-vars (signal-pre/post #t
ordered-args val
indy-res-vars '#,(pre/post-kind pre)
ordered-ress swapped-blame
x))) condition-result
(pre/post-vars pre))))) #,@(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)) #,call-stx))
(define-for-syntax (add-post-cond an-istx indy-arg-vars ordered-args indy-res-vars ordered-ress (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))] #`(begin #,@(for/list ([post (in-list (istx-post an-istx))]
[i (in-naturals)]) [i (in-naturals)])
(define id (string->symbol (format "post-proc~a" i))) (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 ordered-args
indy-res-vars indy-res-vars
ordered-ress ordered-ress
var)) x)))
(pre/post-vars post))) (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)))))
#,call-stx)) #,call-stx))
;; add-wrapper-let : ;; add-wrapper-let :
@ -1254,7 +1282,7 @@ evaluted left-to-right.)
#f) #f)
#,(for/list ([pre (in-list (istx-pre an-istx))]) #,(for/list ([pre (in-list (istx-pre an-istx))])
(list (map syntax-e (pre/post-vars pre)) (list (map syntax-e (pre/post-vars pre))
(pre/post-str pre) (pre/post-kind pre)
(pre/post-quoted-dep-src-code pre))) (pre/post-quoted-dep-src-code 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))])
@ -1270,7 +1298,7 @@ evaluted left-to-right.)
,(arg/res-quoted-dep-src-code a-res)))) ,(arg/res-quoted-dep-src-code a-res))))
#,(for/list ([post (in-list (istx-post an-istx))]) #,(for/list ([post (in-list (istx-post an-istx))])
(list (map syntax-e (pre/post-vars post)) (list (map syntax-e (pre/post-vars post))
(pre/post-str post) (pre/post-kind post)
(pre/post-quoted-dep-src-code post))))) (pre/post-quoted-dep-src-code post)))))
'racket/contract:contract 'racket/contract:contract
(let () (let ()

View File

@ -14,7 +14,8 @@
(provide (for-syntax build-chaperone-constructor/real) (provide (for-syntax build-chaperone-constructor/real)
->-proj ->-proj
check-pre-cond check-pre-cond
check-post-cond) check-post-cond
pre-post/desc-result->string)
(define-for-syntax (build-chaperone-constructor/real this-args (define-for-syntax (build-chaperone-constructor/real this-args
mandatory-dom-projs mandatory-dom-projs
@ -79,33 +80,37 @@
(void)] (void)]
[else [else
(define msg (define msg
(cond (pre-post/desc-result->string condition-result pre? '->*))
[(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)]))
(raise-blame-error (if pre? (blame-swap blame) blame) (raise-blame-error (if pre? (blame-swap blame) blame)
#:missing-party neg-party #:missing-party neg-party
val "~a" msg)])) 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 (define-for-syntax (create-chaperone blame val
this-args this-args
doms opt-doms doms opt-doms