From 93b538b694506786cc3017ff374bd64aa07046e8 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Thu, 9 Apr 2015 23:13:02 -0700 Subject: [PATCH] Cleanup types of fixnum comparisons. Unify Zero and One cases, and remove extraneous ones. --- .../base-env/base-env-numeric.rkt | 60 +++++-------------- 1 file changed, 16 insertions(+), 44 deletions(-) diff --git a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt index ed528968..478d3b00 100644 --- a/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt @@ -207,23 +207,15 @@ (define fx<-type (lambda () (fx-from-cases - (-> -Pos -One B : (-FS (-filter (Un) 0) -top)) ; can't happen - (-> -Nat -One B : (-FS (-filter -Zero 0) -top)) (-> -Int -One B : (-FS (-filter -NonPosFixnum 0) (-filter -PosFixnum 0))) - ;; bleh, this repeats cases below, but since we can only match a single - ;; case, we need to put it here as well, or we would not gain that info, - ;; as another unrelated case would match - (-> -Byte -Zero B : (-FS (-filter (Un) 0) -top)) - (-> -Byte -One B : (-FS (-filter -Zero 0) -top)) - (-> -Zero -Byte B : (-FS (-filter -PosByte 1) (-filter -Zero 1))) + (-> -Int -Zero B : (-FS (-filter -NegFixnum 0) (-filter -NonNegFixnum 0))) + (-> -Zero -Int B : (-FS (-filter -PosFixnum 1) (-filter -NonPosFixnum 1))) + (-> -Byte -PosByte B : (-FS -top (-filter -PosByte 0))) (-> -Byte -Byte B : (-FS (-filter -PosByte 1) -top)) (-> -Pos -Byte B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top)) (-> -Byte -Pos B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1)))) (-> -Byte -Nat B : (-FS -top (-filter -Byte 1))) - (-> -Index -Zero B : (-FS (-filter (Un) 0) -top)) - (-> -Index -One B : (-FS (-filter -Zero 0) -top)) - (-> -Zero -Index B : (-FS (-filter -PosIndex 1) (-filter -Zero 1))) (-> -Index -PosIndex B : (-FS -top (-filter -PosIndex 0))) (-> -Index -Index B : (-FS (-filter -PosIndex 1) -top)) (-> -Pos -Index B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top)) @@ -232,8 +224,6 @@ (-> -Nat -Index B : (-FS (-and (-filter -Index 0) (-filter -PosIndex 1)) -top)) (-> -Index -Nat B : (-FS -top (-filter -Index 1))) ;; general integer cases - (-> -Int -Zero B : (-FS (-filter -NegFixnum 0) (-filter -NonNegFixnum 0))) - (-> -Zero -Int B : (-FS (-filter -PosFixnum 1) (-filter -NonPosFixnum 1))) (-> -Int -PosInt B : (-FS -top (-filter -PosFixnum 0))) (-> -Int -Nat B : (-FS -top (-filter -NonNegFixnum 0))) (-> -Nat -Int B : (-FS (-filter -PosFixnum 1) -top)) @@ -244,20 +234,15 @@ (define fx>-type (lambda () (fx-from-cases - (-> -One -Pos B : (-FS (-filter (Un) 1) -top)) ; can't happen - (-> -One -Nat B : (-FS (-filter -Zero 1) -top)) (-> -One -Int B : (-FS (-filter -NonPosFixnum 1) (-filter -PosFixnum 1))) - (-> -Byte -Zero B : (-FS (-filter -PosByte 0) (-filter -Zero 0))) - (-> -Zero -Byte B : (-FS (-filter (Un) 1) -top)) - (-> -One -Byte B : (-FS (-filter -Zero 1) (-filter -PosByte 1))) + (-> -Zero -Int B : (-FS (-filter -NegFixnum 1) (-filter -NonNegFixnum 1))) + (-> -Int -Zero B : (-FS (-filter -PosFixnum 0) (-filter -NonPosFixnum 0))) + (-> -PosByte -Byte B : (-FS -top (-filter -PosByte 1))) (-> -Byte -Byte B : (-FS (-filter -PosByte 0) -top)) (-> -Byte -Pos B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top)) (-> -Pos -Byte B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1)))) (-> -Byte -Nat B : (-FS (-and (-filter -PosByte 0) (-filter -Byte 1)) -top)) - (-> -Zero -Index B : (-FS (-filter (Un) 1) -top)) - (-> -One -Index B : (-FS (-filter -Zero 1) -top)) - (-> -Index -Zero B : (-FS (-filter -PosIndex 0) (-filter -Zero 0))) (-> -PosIndex -Index B : (-FS -top (-filter -PosIndex 1))) (-> -Index -Index B : (-FS (-filter -PosIndex 0) -top)) (-> -Index -Pos B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top)) @@ -266,8 +251,6 @@ (-> -Nat -Byte B : (-FS -top (-filter -Byte 0))) (-> -Nat -Index B : (-FS -top (-filter -Index 0))) ;; general integer cases - (-> -Zero -Int B : (-FS (-filter -NegFixnum 1) (-filter -NonNegFixnum 1))) - (-> -Int -Zero B : (-FS (-filter -PosFixnum 0) (-filter -NonPosFixnum 0))) (-> -PosInt -Int B : (-FS -top (-filter -PosFixnum 1))) (-> -Nat -Int B : (-FS -top (-filter -NonNegFixnum 1))) (-> -Int -Nat B : (-FS (-filter -PosFixnum 0) -top)) @@ -278,18 +261,16 @@ (define fx<=-type (lambda () (fx-from-cases - (-> -Pos -One B : (-FS (-filter -One 0) -top)) - (-> -Byte -Zero B : (-FS (-filter -Zero 0) (-filter -PosByte 0))) - (-> -Zero -Byte B : (-FS -top (-filter (Un) 1))) - (-> -One -Byte B : (-FS (-filter -PosByte 1) (-filter -Zero 1))) + (-> -Int -One B : (-FS (-filter (Un -NonPosFixnum -One) 0) (-filter -PosFixnum 0))) + (-> -One -Int B : (-FS (-filter -PosFixnum 1) (-filter -NonPosFixnum 1))) + (-> -Int -Zero B : (-FS (-filter -NonPosFixnum 0) (-filter -PosFixnum 0))) + (-> -Zero -Int B : (-FS (-filter -NonNegFixnum 1) (-filter -NegFixnum 1))) + (-> -PosByte -Byte B : (-FS (-filter -PosByte 1) -top)) (-> -Byte -Byte B : (-FS -top (-filter -PosByte 0))) (-> -Pos -Byte B : (-FS (-and (-filter -PosByte 0) (-filter -PosByte 1)) -top)) (-> -Byte -Pos B : (-FS -top (-and (-filter -PosByte 0) (-filter -PosByte 1)))) (-> -Byte -Nat B : (-FS -top (-and (-filter -PosByte 0) (-filter -Byte 1)))) - (-> -Index -Zero B : (-FS (-filter -Zero 0) (-filter -PosIndex 0))) - (-> -Zero -Index B : (-FS -top (-filter (Un) 1))) - (-> -One -Index B : (-FS (-filter -PosIndex 1) (-filter -Zero 1))) (-> -PosIndex -Index B : (-FS (-filter -PosIndex 1) -top)) (-> -Index -Index B : (-FS -top (-filter -PosIndex 0))) (-> -Pos -Index B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top)) @@ -298,10 +279,6 @@ (-> -Nat -Index B : (-FS (-filter -Index 0) -top)) (-> -Index -Nat B : (-FS -top (-and (-filter -PosIndex 0) (-filter -Index 1)))) ;; general integer cases - (-> -Nat -Zero B : (-FS (-filter -Zero 0) -top)) - (-> -One -Nat B : (-FS (-filter -PosFixnum 1) (-filter -Zero 1))) - (-> -Int -Zero B : (-FS (-filter -NonPosFixnum 0) (-filter -PosFixnum 0))) - (-> -Zero -Int B : (-FS (-filter -NonNegFixnum 1) (-filter -NegFixnum 1))) (-> -PosInt -Int B : (-FS (-filter -PosFixnum 1) -top)) (-> -Int -Nat B : (-FS -top (-filter -PosFixnum 0))) (-> -Nat -Int B : (-FS (-filter -NonNegFixnum 1) -top)) @@ -312,18 +289,17 @@ (define fx>=-type (lambda () (fx-from-cases - (-> -One -Pos B : (-FS (-filter -One 1) -top)) - (-> -Zero -Byte B : (-FS (-filter -Zero 1) (-filter -PosByte 1))) - (-> -Byte -Zero B : (-FS -top (-filter (Un) 0))) - (-> -Byte -One B : (-FS (-filter -PosByte 0) (-filter -Zero 0))) + (-> -One -Int B : (-FS (-filter (Un -One -NonPosInt) 1) (-filter -PosFixnum 1))) + (-> -Int -One B : (-FS (-filter -PosFixnum 0) (-filter -NonPosFixnum 0))) + (-> -Zero -Int B : (-FS (-filter -NonPosFixnum 1) (-filter -PosFixnum 1))) + (-> -Int -Zero B : (-FS (-filter -NonNegFixnum 0) (-filter -NegFixnum 0))) + (-> -Byte -PosByte B : (-FS (-filter -PosByte 0) -top)) (-> -Byte -Byte B : (-FS -top (-filter -PosByte 1))) (-> -Byte -Pos B : (-FS (-and (-filter -PosByte 1) (-filter -PosByte 0)) -top)) (-> -Pos -Byte B : (-FS -top (-and (-filter -PosByte 1) (-filter -PosByte 0)))) (-> -Byte -Nat B : (-FS (-filter -Byte 1) -top)) (-> -Zero -Index B : (-FS (-filter -Zero 1) (-filter -PosIndex 1))) - (-> -Index -Zero B : (-FS -top (-filter (Un) 0))) - (-> -Index -One B : (-FS (-filter -PosIndex 0) (-filter -Zero 0))) (-> -Index -PosIndex B : (-FS (-filter -PosIndex 0) -top)) (-> -Index -Index B : (-FS -top (-filter -PosIndex 1))) (-> -Index -Pos B : (-FS (-and (-filter -PosIndex 0) (-filter -PosIndex 1)) -top)) @@ -332,10 +308,6 @@ (-> -Nat -Byte B : (-FS -top (-and (-filter -Byte 0) (-filter -PosByte 1)))) (-> -Nat -Index B : (-FS -top (-and (-filter -Index 0) (-filter -PosIndex 1)))) ;; general integer cases - (-> -Zero -Nat B : (-FS (-filter -Zero 1) -top)) - (-> -Nat -One B : (-FS (-filter -PosFixnum 0) (-filter -Zero 0))) - (-> -Zero -Int B : (-FS (-filter -NonPosFixnum 1) (-filter -PosFixnum 1))) - (-> -Int -Zero B : (-FS (-filter -NonNegFixnum 0) (-filter -NegFixnum 0))) (-> -Int -PosInt B : (-FS (-filter -PosFixnum 0) -top)) (-> -Nat -Int B : (-FS -top (-filter -PosFixnum 1))) (-> -Int -Nat B : (-FS (-filter -NonNegFixnum 0) -top))