got #:pre conditions working

This commit is contained in:
Robby Findler 2010-08-04 18:39:22 -05:00
parent 5922ceda74
commit 6d9066eb22
4 changed files with 55 additions and 18 deletions

View File

@ -4,7 +4,7 @@
;; the PLT code base where appropriate.
(require "private/arrow.rkt"
"private/arr-i-old.rkt"
"private/arr-i.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-old.rkt")
(all-from-out "private/arr-i.rkt")
(except-out (all-from-out "private/misc.rkt")
check-between/c
check-unary-between/c)

View File

@ -407,4 +407,5 @@ code does the parsing and validation of the syntax.
(struct-out istx)
(struct-out res)
(struct-out arg)
(struct-out rst))
(struct-out rst)
(struct-out pre/post))

View File

@ -33,6 +33,7 @@
;; mk-wrapper : creates the a wrapper function that implements the contract checking
(struct ->i (arg-ctcs arg-dep-ctcs indy-arg-ctcs
rng-ctcs rng-dep-ctcs indy-rng-ctcs
pre/post-procs
mandatory-args opt-args mandatory-kwds opt-kwds rest?
here
mk-wrapper)
@ -65,7 +66,8 @@
(check-procedure/more val mtd? (->i-mandatory-args ctc) (->i-mandatory-kwds ctc) (->i-opt-kwds ctc) blame)
(check-procedure val mtd? (->i-mandatory-args ctc) (->i-opt-args ctc) (->i-mandatory-kwds ctc) (->i-opt-kwds ctc) blame)))
ctc
(append partial-doms
(append (->i-pre/post-procs ctc)
partial-doms
(->i-arg-dep-ctcs ctc)
partial-indy-doms
partial-rngs
@ -185,6 +187,20 @@
(define-for-syntax (maybe-generate-temporary x)
(and x (car (generate-temporaries (list x)))))
(define (check-pre bool val blame)
(unless bool
(raise-blame-error blame val "#:pre condition violation")))
(define-for-syntax (add-pre-cond an-istx arg-to-indy-var call-stx)
(cond
[(istx-pre an-istx)
#`(begin (check-pre (pre-proc #,@(map arg-to-indy-var (pre/post-vars (istx-pre an-istx))))
val
swapped-blame)
#,call-stx)]
[else
call-stx]))
(define-for-syntax (mk-wrapper-func an-istx used-indy-vars)
(let-values ([(ordered-args arg-indicies) (find-ordering (istx-args an-istx))])
@ -194,7 +210,7 @@
;; this list is parallel to arg-proj-vars (so use arg-indicies to find the right ones in the loop below)
;; but it contains #fs in places where we don't need the indy projections (because the corresponding
;; argument is not dependened on anywhere)
;; argument is not dependened on by anything)
[indy-arg-proj-vars (list->vector (map (λ (x) (maybe-generate-temporary
(and (not (arg-vars x))
(free-identifier-mapping-get used-indy-vars
@ -217,6 +233,11 @@
[else (loop (cdr iargs) (cdr args))]))])))
#`(λ (blame swapped-blame indy-dom-blame indy-rng-blame chk ctc
;; the pre- and post-condition procs
#,@(if (istx-pre an-istx) (list #'pre-proc) '())
#,@(if (istx-post an-istx) (list #'post-proc) '())
;; first the non-dependent arg projections
#,@(filter values (map (λ (arg arg-proj-var) (and (not (arg-vars arg)) arg-proj-var))
(istx-args an-istx)
@ -231,8 +252,8 @@
(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)])
;; WRONG: need to include the post-condition checking somewhere in here.
#,(for/fold ([body (add-pre-cond an-istx arg-to-indy-var (args/vars->callsite #'val (istx-args an-istx) wrapper-args))])
([indy-arg (in-list indy-args)]
[arg (in-list ordered-args)]
[arg-index arg-indicies]
@ -278,6 +299,12 @@
(when (arg-vars an-arg)
(for ([var (in-list (arg-vars an-arg))])
(free-identifier-mapping-put! vars var #t))))
(when (istx-pre an-istx)
(for ([var (in-list (pre/post-vars (istx-pre an-istx)))])
(free-identifier-mapping-put! vars var #t)))
(when (istx-post an-istx)
(for ([var (in-list (pre/post-vars (istx-post an-istx)))])
(free-identifier-mapping-put! vars var #t)))
(when (istx-ress an-istx)
(for ([a-res (in-list (istx-ress an-istx))])
(when (res-vars a-res)
@ -335,6 +362,14 @@
#`(list res-exp-xs ...)
#''())
#,(let ([func (λ (pre/post) #`(λ #,(pre/post-vars pre/post) #,(pre/post-exp pre/post)))])
#`(list #,@(if (istx-pre an-istx)
(list (func (istx-pre an-istx)))
'())
#,@(if (istx-post an-istx)
(list (func (istx-post an-istx)))
'())))
#,(length (filter values (map (λ (arg) (and (not (arg-kwd arg)) (not (arg-optional? arg))))
(istx-args an-istx))))
#,(length (filter values (map (λ (arg) (and (not (arg-kwd arg)) (arg-optional? arg)))

View File

@ -2,25 +2,20 @@
(require racket/contract
racket/pretty)
#;
(->i ([x number?]) [res any/c] #:post () #t)
#;
(pretty-print
(syntax->datum (expand-once
#'(->i () #:pre-cond #f any #:post-cond #f))))
#'(->i ([f (-> number? number?)]) #:pre (f) (= (f #f) 11) any))))
#;
(pretty-print
(syntax->datum (expand
#'(->i () [x integer?]))))
#;
((contract (->i () #:pre-cond #f any)
(λ () 1)
'pos 'neg))
;; => 1
((contract (->i ([f (-> number? number?)]) #:pre (f) (= (f #f) 11) any)
(λ (x) 1)
'pos 'neg)
(λ (n) (+ n 1)))
;; => indy violation, during pre-condition checking
#|
;; timing tests:
@ -182,4 +177,10 @@ test cases:
1 2 3)
;; => 6
((contract (->i ([x number?]) #:pre () (= 1 2) any)
(λ (x) 1)
'pos 'neg) 2)
;; => pre-condition violation
|#