Adjust and/c so that it cooperates with between/c

Specifically, when it sees these contracts:

  (and/c real? negative?)
  (and/c real? positive?)
  (and/c real? (not/c positive?))
  (and/c real? (not/c negative?))

it generates the corresponding use of >=/c, <=/c, </c, or >/c, but
those contracts have also been adjusted to report their names as
(and/c real? ...).

This mostly is an improvement for contract-stronger, but also make it
so that (between/c -inf.0 +inf.0) just uses the real? predicate
directly, instead of a more complex function
This commit is contained in:
Robby Findler 2016-12-29 09:03:59 -06:00
parent 9019e8b318
commit 66b199307c
6 changed files with 76 additions and 17 deletions

View File

@ -53,6 +53,11 @@
(test-flat-contract 'natural-number/c 0 -1) (test-flat-contract 'natural-number/c 0 -1)
(test-flat-contract 'false/c #f #t) (test-flat-contract 'false/c #f #t)
(test-flat-contract 'contract? #f (λ (x y) 'whatever)) (test-flat-contract 'contract? #f (λ (x y) 'whatever))
(test-flat-contract '(and/c real? negative?) -1 0)
(test-flat-contract '(and/c real? positive?) 1 0)
(test-flat-contract '(and/c real? (not/c positive?)) 0 1)
(test-flat-contract '(and/c real? (not/c negative?)) 0 -1)
(test-flat-contract #t #t "x") (test-flat-contract #t #t "x")
(test-flat-contract #f #f "x") (test-flat-contract #f #f "x")

View File

@ -229,6 +229,15 @@
(test-name '(and/c (-> boolean? boolean?) (-> integer? integer?)) (test-name '(and/c (-> boolean? boolean?) (-> integer? integer?))
(and/c (-> boolean? boolean?) (-> integer? integer?))) (and/c (-> boolean? boolean?) (-> integer? integer?)))
(test-name '(and/c real? positive?) (and/c real? positive?))
(test-name '(and/c real? (not/c positive?)) (and/c real? (not/c positive?)))
(test-name '(and/c real? negative?) (and/c real? negative?))
(test-name '(and/c real? (not/c negative?)) (and/c real? (not/c negative?)))
(test-name '(and/c real? positive?) (>/c 0))
(test-name '(and/c real? (not/c positive?)) (<=/c 0))
(test-name '(and/c real? negative?) (</c 0))
(test-name '(and/c real? (not/c negative?)) (>=/c 0))
(test-name '(not/c integer?) (not/c integer?)) (test-name '(not/c integer?) (not/c integer?))
(test-name '(=/c 5) (=/c 5)) (test-name '(=/c 5) (=/c 5))
(test-name '(>=/c 5) (>=/c 5)) (test-name '(>=/c 5) (>=/c 5))
@ -434,13 +443,13 @@
(test-name '(class/c (absent a b c (field d e f))) (class/c (absent a b c (field d e f)))) (test-name '(class/c (absent a b c (field d e f))) (class/c (absent a b c (field d e f))))
(test-name '(class/c (absent a b c)) (class/c (absent a b c))) (test-name '(class/c (absent a b c)) (class/c (absent a b c)))
(test-name '(class/c (inherit [f integer?]) (test-name '(class/c (inherit [f integer?])
(super [m (->m (<=/c 0) integer?)]) (super [m (->m (<=/c -1) integer?)])
(inner [n (->m (<=/c 1) integer?)]) (inner [n (->m (<=/c 1) integer?)])
(override [o (->m (<=/c 2) integer?)]) (override [o (->m (<=/c 2) integer?)])
(augment [p (->m (<=/c 3) integer?)]) (augment [p (->m (<=/c 3) integer?)])
(augride [q (->m (<=/c 4) integer?)])) (augride [q (->m (<=/c 4) integer?)]))
(class/c (inherit [f integer?]) (class/c (inherit [f integer?])
(super [m (->m (<=/c 0) integer?)]) (super [m (->m (<=/c -1) integer?)])
(inner [n (->m (<=/c 1) integer?)]) (inner [n (->m (<=/c 1) integer?)])
(override [o (->m (<=/c 2) integer?)]) (override [o (->m (<=/c 2) integer?)])
(augment [p (->m (<=/c 3) integer?)]) (augment [p (->m (<=/c 3) integer?)])

View File

@ -42,6 +42,16 @@
(ctest #f contract-stronger? (<=/c 2) (>/c 2)) (ctest #f contract-stronger? (<=/c 2) (>/c 2))
(ctest #f contract-stronger? (>=/c 2) (>/c 2)) (ctest #f contract-stronger? (>=/c 2) (>/c 2))
(ctest #t contract-stronger? (>=/c 3) (>/c 2)) (ctest #t contract-stronger? (>=/c 3) (>/c 2))
(ctest #t contract-stronger? (>/c 0) (and/c real? positive?))
(ctest #t contract-stronger? (and/c real? positive?) (>/c 0))
(ctest #t contract-stronger? (</c 0) (and/c real? negative?))
(ctest #t contract-stronger? (and/c real? negative?) (</c 0))
(ctest #t contract-stronger? (<=/c 0) (and/c real? (not/c positive?)))
(ctest #t contract-stronger? (and/c real? (not/c positive?)) (<=/c 0))
(ctest #t contract-stronger? (>=/c 0) (and/c real? (not/c negative?)))
(ctest #t contract-stronger? (and/c real? (not/c negative?)) (>=/c 0))
(ctest #t contract-stronger? (recursive-contract (<=/c 2)) (recursive-contract (<=/c 3))) (ctest #t contract-stronger? (recursive-contract (<=/c 2)) (recursive-contract (<=/c 3)))
(ctest #f contract-stronger? (recursive-contract (<=/c 3)) (recursive-contract (<=/c 2))) (ctest #f contract-stronger? (recursive-contract (<=/c 3)) (recursive-contract (<=/c 2)))
(let ([f (contract-eval '(λ (x) (recursive-contract (<=/c x))))]) (let ([f (contract-eval '(λ (x) (recursive-contract (<=/c x))))])

View File

@ -183,8 +183,28 @@
(cond (cond
[(null? contracts) any/c] [(null? contracts) any/c]
[(andmap flat-contract? contracts) [(andmap flat-contract? contracts)
(let ([preds (map flat-contract-predicate contracts)]) (define preds (map flat-contract-predicate contracts))
(make-first-order-and/c contracts preds))] (cond
[(and (chaperone-of? (car preds) real?)
(pair? (cdr preds))
(null? (cddr preds)))
(define second-pred (cadr preds))
(cond
[(chaperone-of? second-pred negative?)
(</c 0)]
[(chaperone-of? second-pred positive?)
(>/c 0)]
[else
(define second-contract (cadr contracts))
(cond
[(equal? (contract-name second-contract) '(not/c positive?))
(<=/c 0)]
[(equal? (contract-name second-contract) '(not/c negative?))
(>=/c 0)]
[else
(make-first-order-and/c contracts preds)])])]
[else
(make-first-order-and/c contracts preds)])]
[(andmap chaperone-contract? contracts) [(andmap chaperone-contract? contracts)
(make-chaperone-and/c contracts)] (make-chaperone-and/c contracts)]
[else (make-impersonator-and/c contracts)]))) [else (make-impersonator-and/c contracts)])))

View File

@ -118,9 +118,11 @@
(define (between/c-first-order ctc) (define (between/c-first-order ctc)
(define n (between/c-s-low ctc)) (define n (between/c-s-low ctc))
(define m (between/c-s-high ctc)) (define m (between/c-s-high ctc))
(λ (x) (cond
(and (real? x) [(and (= n -inf.0) (= m +inf.0))
(<= n x m)))) real?]
[else
(λ (x) (and (real? x) (<= n x m)))]))
(define ((between/c-generate ctc) fuel) (define ((between/c-generate ctc) fuel)
(define n (between/c-s-low ctc)) (define n (between/c-s-low ctc))
@ -180,8 +182,8 @@
(cond (cond
[(and (= n -inf.0) (= m +inf.0)) [(and (= n -inf.0) (= m +inf.0))
'real?] 'real?]
[(= n -inf.0) `(<=/c ,m)] [(= n -inf.0) (if (= m 0) `(and/c real? (not/c positive?)) `(<=/c ,m))]
[(= m +inf.0) `(>=/c ,n)] [(= m +inf.0) (if (= n 0) `(and/c real? (not/c negative?)) `(>=/c ,n))]
[(= n m) `(=/c ,n)] [(= n m) `(=/c ,n)]
[else `(,name ,n ,m)])) [else `(,name ,n ,m)]))
#:stronger between/c-stronger #:stronger between/c-stronger
@ -214,7 +216,12 @@
(define (make-</c->/c-contract-property name </> -/+ less/greater) (define (make-</c->/c-contract-property name </> -/+ less/greater)
(build-flat-contract-property (build-flat-contract-property
#:name (λ (c) `(,name ,(</>-ctc-x c))) #:name (λ (c)
(cond
[(= (</>-ctc-x c) 0)
`(and/c real? ,(if (equal? name '>/c) 'positive? 'negative?))]
[else
`(,name ,(</>-ctc-x c))]))
#:first-order (λ (ctc) (define x (</>-ctc-x ctc)) (λ (y) (and (real? y) (</> y x)))) #:first-order (λ (ctc) (define x (</>-ctc-x ctc)) (λ (y) (and (real? y) (</> y x))))
#:late-neg-projection #:late-neg-projection
(λ (ctc) (λ (ctc)

View File

@ -217,7 +217,8 @@
'(expected: "a number between ~a and ~a" given: "~e") '(expected: "a number between ~a and ~a" given: "~e")
lo hi val)) lo hi val))
(define-for-syntax (single-comparison-opter opt/info stx check-arg comparison arg name predicate?) (define-for-syntax (single-comparison-opter opt/info stx check-arg comparison arg name predicate?
special-name)
(with-syntax ([comparison comparison] (with-syntax ([comparison comparison]
[predicate? predicate?]) [predicate? predicate?])
(let*-values ([(lift-low lifts2) (lift/binding arg 'single-comparison-val empty-lifts)]) (let*-values ([(lift-low lifts2) (lift/binding arg 'single-comparison-val empty-lifts)])
@ -247,7 +248,9 @@
[that that]) [that that])
(syntax (comparison this that)))))) (syntax (comparison this that))))))
#:chaperone #t #:chaperone #t
#:name #`'(#,name m)))))))) #:name #`(if (= m 0)
'#,special-name
'(#,name m)))))))))
(define (raise-opt-single-comparison-opter-error blame val comparison m predicate?) (define (raise-opt-single-comparison-opter-error blame val comparison m predicate?)
(raise-blame-error (raise-blame-error
@ -271,7 +274,8 @@
#'= #'=
#'x #'x
'=/c '=/c
#'number?)])) #'number?
'(= 0))]))
(define/opter (>=/c opt/i opt/info stx) (define/opter (>=/c opt/i opt/info stx)
(syntax-case stx (>=/c) (syntax-case stx (>=/c)
@ -284,7 +288,8 @@
#'>= #'>=
#'low #'low
'>=/c '>=/c
#'real?)])) #'real?
'(and/c real? (not/c negative?)))]))
(define/opter (<=/c opt/i opt/info stx) (define/opter (<=/c opt/i opt/info stx)
(syntax-case stx (<=/c) (syntax-case stx (<=/c)
@ -297,7 +302,8 @@
#'<= #'<=
#'high #'high
'<=/c '<=/c
#'real?)])) #'real?
'(and/c real? (not/c positive?)))]))
(define/opter (>/c opt/i opt/info stx) (define/opter (>/c opt/i opt/info stx)
(syntax-case stx (>/c) (syntax-case stx (>/c)
@ -310,7 +316,8 @@
#'> #'>
#'low #'low
'>/c '>/c
#'real?)])) #'real?
'(and/c real? positive?))]))
(define/opter (</c opt/i opt/info stx) (define/opter (</c opt/i opt/info stx)
(syntax-case stx (</c) (syntax-case stx (</c)
@ -323,7 +330,8 @@
#'< #'<
#'high #'high
'</c '</c
#'real?)])) #'real?
'(and/c real? negative?))]))
(define/opter (cons/c opt/i opt/info stx) (define/opter (cons/c opt/i opt/info stx)
(define (opt/cons-ctc hdp tlp) (define (opt/cons-ctc hdp tlp)