suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Cleanup types of fixnum comparisons.

Browse Source 
Unify Zero and One cases, and remove extraneous ones.
This commit is contained in:
Eric Dobson 2015-04-09 23:13:02 -07:00
parent 114b9376f1
commit 93b538b694
1 changed files with 16 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

60
typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt
View File

@ -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))