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 fbc6d7b32..d03919e56 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 @@ -134,6 +134,9 @@ (fx-from-cases (-> -Int -Zero -Fixnum : -true-propset : (-arg-path 0)) (-One -One . -> . -Zero) + (-Byte>1 -One . -> . -PosByte) + (-Index>1 -One . -> . -PosIndex) + (-Int>1 -One . -> . -PosFixnum) (-PosByte -One . -> . -Byte) (-PosIndex -One . -> . -Index) (-PosInt -One . -> . -NonNegFixnum) @@ -1105,6 +1108,10 @@ (-> N -Zero N : -true-propset : (-arg-path 0)) (-> -One -One -Zero) + (-> -Byte>1 -One -PosByte) + (-> -Index>1 -One -PosIndex) + (-> -Fixnum>1 -One -PosFixnum) + (-> -Int>1 -One -PosInt) (-> -PosByte -One -Byte) (-> -PosIndex -One -Index) (-> -PosFixnum -One -NonNegFixnum) @@ -1291,6 +1298,10 @@ [sub1 (from-cases (-> -One -Zero) + (-> -Byte>1 -PosByte) + (-> -Index>1 -PosIndex) + (-> -Fixnum>1 -PosFixnum) + (-> -Int>1 -Pos) (-> -PosByte -Byte) (-> -PosIndex -Index) (-> -Index -Fixnum) diff --git a/typed-racket-lib/typed-racket/types/numeric-tower.rkt b/typed-racket-lib/typed-racket/types/numeric-tower.rkt index 590bc33e3..89f48d444 100644 --- a/typed-racket-lib/typed-racket/types/numeric-tower.rkt +++ b/typed-racket-lib/typed-racket/types/numeric-tower.rkt @@ -10,9 +10,9 @@ (for-template racket/base racket/contract/base (types numeric-predicates))) (provide portable-fixnum? portable-index? - -Zero -One -PosByte -Byte -PosIndex -Index - -PosFixnum -NonNegFixnum -NegFixnum -NonPosFixnum -Fixnum - -PosInt -Nat -NegInt -NonPosInt -Int + -Zero -One -Byte>1 -PosByte -Byte -Index>1 -PosIndex -Index + -Fixnum>1 -PosFixnum -NonNegFixnum -NegFixnum -NonPosFixnum -Fixnum + -Int>1 -PosInt -Nat -NegInt -NonPosInt -Int -PosRat -NonNegRat -NegRat -NonPosRat -Rat -FlonumPosZero -FlonumNegZero -FlonumZero -FlonumNan -PosFlonum -NonNegFlonum -NegFlonum -NonPosFlonum -Flonum @@ -46,15 +46,18 @@ (define/decl -PosByte (Un -One -Byte>1)) (define/decl -Byte (Un -Zero -PosByte)) -(define/decl -PosIndex (Un -One -Byte>1 -PosIndexNotByte)) +(define/decl -Index>1 (Un -Byte>1 -PosIndexNotByte)) +(define/decl -PosIndex (Un -One -Index>1)) (define/decl -Index (Un -Zero -PosIndex)) +(define/decl -Fixnum>1 (Un -PosFixnumNotIndex -Index>1)) (define/decl -PosFixnum (Un -PosFixnumNotIndex -PosIndex)) (define/decl -NonNegFixnum (Un -PosFixnum -Zero)) (define/decl -NonPosFixnum (Un -NegFixnum -Zero)) (define/decl -Fixnum (Un -NegFixnum -Zero -PosFixnum)) +(define/decl -Int>1 (Un -PosIntNotFixnum -Fixnum>1)) (define/decl -PosInt (Un -PosIntNotFixnum -PosFixnum)) (define/decl -NonNegInt (Un -PosInt -Zero)) (define/decl -Nat -NonNegInt) @@ -132,6 +135,7 @@ (BaseUnion-nbits -Byte) (cons 0 255) (BaseUnion-nbits -PosByte) (cons 1 255) (Base-bits -Byte>1) (cons 2 255) + (BaseUnion-nbits -Int>1) (cons 2 #f) (BaseUnion-nbits -PosInt) (cons 1 #f) (BaseUnion-nbits -Nat) (cons 0 #f) (BaseUnion-nbits -NonPosInt) (cons #f 0) @@ -158,12 +162,15 @@ (BaseUnion-nbits -Byte) (cons 0 255) (BaseUnion-nbits -PosByte) (cons 1 255) (Base-bits -Byte>1) (cons 2 255) + (BaseUnion-nbits -Int>1) (cons 2 #f) (BaseUnion-nbits -PosInt) (cons 1 #f) (BaseUnion-nbits -Nat) (cons 0 #f) (BaseUnion-nbits -NonPosInt) (cons #f 0) (BaseUnion-nbits -NegInt) (cons #f -1) (BaseUnion-nbits -Index) (cons 0 #f) + (BaseUnion-nbits -Index>1) (cons 2 #f) (BaseUnion-nbits -PosIndex) (cons 1 #f) + (BaseUnion-nbits -Fixnum>1) (cons 2 #f) (BaseUnion-nbits -PosFixnum) (cons 1 #f) (BaseUnion-nbits -NonNegFixnum) (cons 0 #f) (BaseUnion-nbits -NonPosFixnum) (cons #f 0) @@ -179,9 +186,10 @@ (define all-bounded-int-types ;; relies on numeric bits being eq? - (for/hasheq ([t (in-list (list -Zero -One -PosByte -Byte>1 -Byte -PosIndex -Index - -PosFixnum -NonNegFixnum -NegFixnum -NonPosFixnum - -PosInt -Nat -NegInt -NonPosInt))]) + (for/hasheq ([t (in-list (list -Zero -One -PosByte -Byte>1 -Byte + -Index>1 -PosIndex -Index + -Fixnum>1 -PosFixnum -NonNegFixnum -NegFixnum -NonPosFixnum + -Int>1 -PosInt -Nat -NegInt -NonPosInt))]) (values (if (BaseUnion? t) (BaseUnion-nbits t) (Base-bits t)) diff --git a/typed-racket-test/succeed/sub1-int-gt-1.rkt b/typed-racket-test/succeed/sub1-int-gt-1.rkt new file mode 100644 index 000000000..e9c135ca8 --- /dev/null +++ b/typed-racket-test/succeed/sub1-int-gt-1.rkt @@ -0,0 +1,13 @@ +#lang typed/racket + +;; From this stack overflow question by Lyu Yao Ting: +;; Type mismatch issue of sub1 +;; https://stackoverflow.com/questions/58887937/type-mismatch-issue-of-sub1 + +(define-predicate one? One) +(: pick1 (-> Positive-Integer (Listof Any) Any)) +(define pick1 + (λ (n lat) + (cond [(one? n) (car lat)] + [else (pick1 (sub1 n) + (cdr lat))])))