Fix filters on odd? and even?

Closes PR 13233
This commit is contained in:
Asumu Takikawa 2013-01-15 16:42:53 -05:00 committed by Vincent St-Amour
parent 1b48b5049f
commit e1b6e84089
5 changed files with 64 additions and 2 deletions

View File

@ -0,0 +1,15 @@
#;
(exn:pred #rx"Expected Zero, but got (U Nonpositive-Integer Byte-Larger-Than-One Positive-Index-Not-Byte Positive-Fixnum-Not-Index Positive-Integer-Not-Fixnum)")
#lang typed/racket
;; test odd? filter
(: foo (Integer -> String))
(define (foo n)
(if (odd? n)
"dummy"
(o n)))
(: o (One -> String))
(define (o x) "dummy")

View File

@ -0,0 +1,15 @@
#;
(exn:pred #rx"Expected Zero, but got (U Negative-Integer Positive-Integer)")
#lang typed/racket
;; test even? filter
(: foo (Integer -> String))
(define (foo n)
(if (even? n)
"dummy"
(z n)))
(: z (Zero -> String))
(define (z x) "dummy")

View File

@ -0,0 +1,15 @@
#;
(exn:pred #rx"Expected One, but got (U Nonpositive-Integer Byte-Larger-Than-One Positive-Index-Not-Byte Positive-Fixnum-Not-Index Positive-Integer-Not-Fixnum)")
#lang typed/racket
;; test even? filter
(: foo (Integer -> String))
(define (foo n)
(if (even? n)
(o n)
"dummy"))
(: o (One -> String))
(define (o x) "dummy")

View File

@ -0,0 +1,17 @@
#;
(exn-pred "Expected Zero, but got")
#lang typed/racket
;; test odd? filter
(: foo (Integer -> Zero))
(define (foo n)
(if (odd? n)
0
n))
(: ZERO Zero)
(define ZERO (foo 2))
ZERO

View File

@ -720,8 +720,8 @@
[exact-positive-integer? (make-pred-ty -Pos)]
[exact-nonnegative-integer? (make-pred-ty -Nat)]
[odd? (-> -Int B : (-FS -top (-filter -Zero 0)))]
[even? (-> -Int B)]
[odd? (-> -Int B : (-FS (-not-filter -Zero 0) (-not-filter -One 0)))]
[even? (-> -Int B : (-FS (-not-filter -One 0) (-not-filter -Zero 0)))]
[=
(from-cases