From 6d9066eb224fda89a4d4285e14d07b0c47aba950 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Wed, 4 Aug 2010 18:39:22 -0500 Subject: [PATCH] got #:pre conditions working --- collects/racket/contract/base.rkt | 4 +- .../racket/contract/private/arr-i-parse.rkt | 3 +- collects/racket/contract/private/arr-i.rkt | 43 +++++++++++++++++-- collects/racket/contract/scratch.rkt | 23 +++++----- 4 files changed, 55 insertions(+), 18 deletions(-) diff --git a/collects/racket/contract/base.rkt b/collects/racket/contract/base.rkt index f0fb0bd1e5..4503211cdd 100644 --- a/collects/racket/contract/base.rkt +++ b/collects/racket/contract/base.rkt @@ -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) diff --git a/collects/racket/contract/private/arr-i-parse.rkt b/collects/racket/contract/private/arr-i-parse.rkt index 945ab182b5..a0533dd2bb 100644 --- a/collects/racket/contract/private/arr-i-parse.rkt +++ b/collects/racket/contract/private/arr-i-parse.rkt @@ -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)) \ No newline at end of file + (struct-out rst) + (struct-out pre/post)) \ No newline at end of file diff --git a/collects/racket/contract/private/arr-i.rkt b/collects/racket/contract/private/arr-i.rkt index 4f4e4cf844..94eb5bfe1a 100644 --- a/collects/racket/contract/private/arr-i.rkt +++ b/collects/racket/contract/private/arr-i.rkt @@ -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))) diff --git a/collects/racket/contract/scratch.rkt b/collects/racket/contract/scratch.rkt index ad2ff19ef2..dfac68477f 100644 --- a/collects/racket/contract/scratch.rkt +++ b/collects/racket/contract/scratch.rkt @@ -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 + + |#