From ede5aadfb060b28860ef5e37174fe19f4d3bbede Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Sat, 16 Nov 2019 13:16:44 -0500 Subject: [PATCH 1/4] numeric-tower: Index>1, Fixnum>1, Int>1 --- .../typed-racket/types/numeric-tower.rkt | 22 +++++++++++++------ 1 file changed, 15 insertions(+), 7 deletions(-) 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)) From 34737420b6f0c1e946400c0c9fb99f4976e96251 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Sat, 16 Nov 2019 13:40:32 -0500 Subject: [PATCH 2/4] sub1: add cases for Byte>1, Index>1, Fixnum>1, Int>1 --- .../typed-racket/base-env/base-env-numeric.rkt | 8 ++++++++ 1 file changed, 8 insertions(+) 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..20b078768 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 @@ -1105,6 +1105,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 +1295,10 @@ [sub1 (from-cases (-> -One -Zero) + (-> -Byte>1 -PosByte) + (-> -Index>1 -PosIndex) + (-> -Fixnum>1 -PosFixnum) + (-> -Int>1 -Pos) (-> -PosByte -Byte) (-> -PosIndex -Index) (-> -Index -Fixnum) From 9798e4b76e1d516ca4964e771d28a6372895297b Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Sat, 16 Nov 2019 14:37:10 -0500 Subject: [PATCH 3/4] fx-: add cases for Byte>1, Index>1, Int>1 --- typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt | 3 +++ 1 file changed, 3 insertions(+) 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 20b078768..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) From 4ff0858cee36cdd55958bb029d27ee229ef95d69 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Sat, 16 Nov 2019 14:39:15 -0500 Subject: [PATCH 4/4] test sub1 on Int>1 returns PosInt --- typed-racket-test/succeed/sub1-int-gt-1.rkt | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 typed-racket-test/succeed/sub1-int-gt-1.rkt 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))])))