make contract-stronger? recognize that predicates are stronger than

values that they accept (for certain, well-known predicates, anyway)
This commit is contained in:
Robby Findler 2014-05-15 09:18:13 -05:00
parent cd4dde5865
commit ae298ae353
4 changed files with 55 additions and 15 deletions

View File

@ -128,6 +128,20 @@
(define x (flat-rec-contract x (or/c (cons/c x '()) '())))
(,test #t contract-stronger? x (or/c (cons/c x '()) '()))))
(ctest #t contract-stronger? "x" string?)
(ctest #f contract-stronger? string? "x")
(ctest #t contract-stronger? 1 real?)
(ctest #f contract-stronger? real? 1)
(ctest #t contract-stronger? 'x symbol?)
(ctest #f contract-stronger? symbol? 'x)
;; chances are, this predicate will accept "x", but
;; we don't want to consider it stronger, since it
;; will not always accept "x".
(ctest #f contract-stronger? "x" (λ (x) (not (zero? (random 10000)))))
(contract-eval
`(let ()
(define (non-zero? x) (not (zero? x)))

View File

@ -5,9 +5,9 @@
"prop.rkt"
"rand.rkt"
"generate-base.rkt"
racket/pretty)
(require (for-syntax racket/base))
racket/pretty
(for-syntax racket/base
"helpers.rkt"))
(provide coerce-contract
coerce-contracts
@ -151,7 +151,7 @@
"contract?"
x)))
;; coerce-contracts : symbols (listof any) -> (listof contract)
;; coerce-contracts : symbol (listof any) -> (listof contract)
;; turns all of the arguments in 'xs' into contracts
;; the error messages assume that the function named by 'name'
;; got 'xs' as it argument directly
@ -173,13 +173,20 @@
(cond
[(contract-struct? x) x]
[(and (procedure? x) (procedure-arity-includes? x 1))
(make-predicate-contract (or (object-name x) '???) x #f)]
(make-predicate-contract (or (object-name x) '???)
x
#f
(memq x the-known-good-contracts))]
[(or (symbol? x) (boolean? x) (char? x) (null? x) (keyword? x)) (make-eq-contract x)]
[(or (bytes? x) (string? x)) (make-equal-contract x)]
[(number? x) (make-=-contract x)]
[(or (regexp? x) (byte-regexp? x)) (make-regexp/c x)]
[else #f]))
(define the-known-good-contracts
(let-syntax ([m (λ (x) #`(list #,@(known-good-contracts)))])
(m)))
(struct wrapped-extra-arg-arrow (real-func extra-neg-party-argument)
#:property prop:procedure 0)
@ -300,8 +307,12 @@
(λ (fuel) (λ () v)))
#:stronger
(λ (this that)
(and (eq-contract? that)
(eq? (eq-contract-val this) (eq-contract-val that))))))
(define this-val (eq-contract-val this))
(or (and (eq-contract? that)
(eq? this-val (eq-contract-val that)))
(and (predicate-contract? that)
(predicate-contract-sane? that)
((predicate-contract-pred that) this-val))))))
(define-struct equal-contract (val)
#:property prop:custom-write custom-write-property-proc
@ -311,8 +322,12 @@
#:name (λ (ctc) (equal-contract-val ctc))
#:stronger
(λ (this that)
(and (equal-contract? that)
(equal? (equal-contract-val this) (equal-contract-val that))))
(define this-val (equal-contract-val this))
(or (and (equal-contract? that)
(equal? this-val (equal-contract-val that)))
(and (predicate-contract? that)
(predicate-contract-sane? that)
((predicate-contract-pred that) this-val))))
#:generate
(λ (ctc)
(define v (equal-contract-val ctc))
@ -326,8 +341,12 @@
#:name (λ (ctc) (=-contract-val ctc))
#:stronger
(λ (this that)
(and (=-contract? that)
(= (=-contract-val this) (=-contract-val that))))
(define this-val (=-contract-val this))
(or (and (=-contract? that)
(= this-val (=-contract-val that)))
(and (predicate-contract? that)
(predicate-contract-sane? that)
((predicate-contract-pred that) this-val))))
#:generate
(λ (ctc)
(define v (=-contract-val ctc))
@ -349,7 +368,9 @@
(and (regexp/c? that) (eq? (regexp/c-reg this) (regexp/c-reg that))))))
(define-struct predicate-contract (name pred generate)
;; sane? : boolean -- indicates if we know that the predicate is well behaved
;; (for now, basically amounts to trusting primitive procedures)
(define-struct predicate-contract (name pred generate sane?)
#:property prop:custom-write custom-write-property-proc
#:property prop:flat-contract
(build-flat-contract-property
@ -391,7 +412,7 @@
(define (check-flat-named-contract predicate) (coerce-flat-contract 'flat-named-contract predicate))
(define (check-flat-contract predicate) (coerce-flat-contract 'flat-contract predicate))
(define (build-flat-contract name pred [generate #f])
(make-predicate-contract name pred generate))
(make-predicate-contract name pred generate #f))
;; Key used by the continuation mark that holds blame information for the current contract.

View File

@ -7,6 +7,7 @@
add-name-prop
all-but-last
known-good-contract?
known-good-contracts
update-loc)
(require setup/main-collects
@ -370,3 +371,7 @@
(and (symbol? r-id)
(hash-ref known-good-syms-ht r-id #f)
(free-identifier=? id (datum->syntax #'here r-id))))
(define (known-good-contracts)
(for/list ([(k v) (in-hash known-good-syms-ht)])
(datum->syntax #'here k)))

View File

@ -1447,9 +1447,9 @@
(cond
[(and (procedure? predicate)
(procedure-arity-includes? predicate 1))
(make-predicate-contract name predicate generate)]
(make-predicate-contract name predicate generate #f)]
[(flat-contract? predicate)
(make-predicate-contract name (flat-contract-predicate predicate) generate)]
(make-predicate-contract name (flat-contract-predicate predicate) generate #f)]
[else
(raise-argument-error 'flat-named-contract
(format "~s" `(or/c flat-contract?