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

improved parsing of #:pre and #:post for ->i (fixed bugs and added more checks to the syntax)

Browse Source
This commit is contained in:
Robby Findler 2010-08-04 17:38:10 -05:00
parent c1b558e1a3
commit 5922ceda74
4 changed files with 56 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -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)]

44
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?)
;; 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 ()
[()

12
collects/racket/contract/scratch.rkt
View File

@ -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

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

@ -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)))