Skip to content

Commit d3183fc

Browse files
authored
unify types for quotient, remainder and quotient/remainder (#1040)
use the same spec to generate types for them. Also do random testing on quotient/remainder closes #1039
1 parent adcc138 commit d3183fc

File tree

3 files changed

+73
-66
lines changed

3 files changed

+73
-66
lines changed

typed-racket-lib/typed-racket/base-env/base-env-numeric.rkt

Lines changed: 55 additions & 63 deletions
Original file line numberDiff line numberDiff line change
@@ -682,6 +682,56 @@
682682
((Un -PosReal -NegReal) . -> . -PosReal)
683683
(-Real . -> . -NonNegReal)))
684684

685+
686+
(define (quotient-reminder-cases . cases)
687+
(for/lists (qs rs qrs)
688+
([i (in-list cases)])
689+
(match-define (list a b (list c d)) i)
690+
(values (-> a b c)
691+
(-> a b d)
692+
(-> a b (-values (list c d))))))
693+
694+
(define-values (quotient-spec remainder-spec quotient/remainder-spec)
695+
(quotient-reminder-cases
696+
(list -Zero -Int (list -Zero -Zero))
697+
(list -One -One (list -Zero -One))
698+
;; division by one is identity, and has no remainder
699+
(list -PosByte -One (list -PosByte -Zero))
700+
(list -Byte -One (list -Byte -Zero))
701+
(list -PosIndex -One (list -PosIndex -Zero))
702+
(list -Index -One (list -Index -Zero))
703+
(list -PosFixnum -One (list -PosFixnum -Zero))
704+
(list -NonNegFixnum -One (list -NonNegFixnum -Zero))
705+
(list -NegFixnum -One (list -NegFixnum -Zero))
706+
(list -NonPosFixnum -One (list -NonPosFixnum -Zero))
707+
(list -Fixnum -One (list -Fixnum -Zero))
708+
(list -Byte -Nat (list -Byte -Byte))
709+
(list -Byte -Int (list -Fixnum -Byte))
710+
(list -Index -Nat (list -Index -Index))
711+
(list -Index -Int (list -Fixnum -Index))
712+
(list -NonNegFixnum -Byte (list -NonNegFixnum -Byte))
713+
(list -NonNegFixnum -NonNegFixnum (list -NonNegFixnum -NonNegFixnum))
714+
(list -NonNegFixnum -NonPosFixnum (list -NonPosFixnum -NonNegFixnum))
715+
(list -NonPosFixnum -NonNegFixnum (list -NonPosFixnum -NonPosFixnum))
716+
(list -NonPosFixnum -NonPosFixnum (list -Nat -NonPosFixnum))
717+
(list -NonNegFixnum -Nat (list -NonNegFixnum -NonNegFixnum))
718+
(list -NonNegFixnum -Int (list -Fixnum -NonNegFixnum))
719+
(list -Nat -Byte (list -Nat -Byte))
720+
(list -Nat -Index (list -Nat -Index))
721+
(list -Nat -NonNegFixnum (list -Nat -NonNegFixnum))
722+
;; in the following cases, we can't guarantee that the quotient is within
723+
;; fixnum range: (quotient min-fixnum -1) -> max-fixnum + 1
724+
(list -NonPosFixnum -Int (list -Int -NonPosFixnum))
725+
(list -Fixnum -Int (list -Int -Fixnum))
726+
(list -Int -Fixnum (list -Int -Fixnum))
727+
(list -Nat -Nat (list -Nat -Nat))
728+
(list -Nat -NonPosInt (list -NonPosInt -Nat))
729+
(list -Nat -Int (list -Int -Nat))
730+
(list -NonPosInt -Nat (list -NonPosInt -NonPosInt))
731+
(list -NonPosInt -NonPosInt (list -Nat -NonPosInt))
732+
(list -NonPosInt -Int (list -Int -NonPosInt))
733+
(list -Int -Int (list -Int -Int))))
734+
685735
;Check to ensure we fail fast if the flonum bindings change
686736
(define-namespace-anchor anchor)
687737
(let ((flonum-ops #'([unsafe-flround flround]
@@ -1309,36 +1359,10 @@
13091359
(-> -NonPosReal -NegReal)
13101360
(map unop (list -Real -FloatComplex -SingleFlonumComplex -InexactComplex N)))]
13111361

1312-
[quotient
1313-
(from-cases
1314-
(-Zero -Int . -> . -Zero)
1315-
(map (lambda (t) (-> t -One t)) ; division by one is identity
1316-
(list -PosByte -Byte -PosIndex -Index
1317-
-PosFixnum -NonNegFixnum -NegFixnum -NonPosFixnum -Fixnum))
1318-
(-Byte -Nat . -> . -Byte)
1319-
(-Byte -Int . -> . -Fixnum) ; may be negative
1320-
(-Index -Nat . -> . -Index)
1321-
(-Index -Int . -> . -Fixnum) ; same.
1322-
;; we don't have equivalent for fixnums:
1323-
;; (quotient min-fixnum -1) -> max-fixnum + 1
1324-
(commutative-binop -NonNegFixnum -NonPosFixnum -NonPosFixnum)
1325-
(-NonPosFixnum -NonPosFixnum . -> . -Nat)
1326-
(-NonNegFixnum -Nat . -> . -NonNegFixnum)
1327-
(-NonNegFixnum -Int . -> . -Fixnum)
1328-
(binop -Nat)
1329-
(commutative-binop -Nat -NonPosInt -NonPosInt)
1330-
(-NonPosInt -NonPosInt . -> . -Nat)
1331-
(binop -Int))]
1332-
[remainder ; result has same sign as first arg
1333-
(from-cases
1334-
(-One -One . -> . -Zero)
1335-
(map (lambda (t) (list (-> -Nat t t)
1336-
(-> t -Int t)))
1337-
(list -Byte -Index -NonNegFixnum -Nat))
1338-
(-NonPosFixnum -Int . -> . -NonPosFixnum)
1339-
(-NonPosInt -Int . -> . -NonPosInt)
1340-
(commutative-binop -Fixnum -Int)
1341-
(binop -Int))]
1362+
[quotient (from-cases quotient-spec)]
1363+
1364+
[remainder (from-cases remainder-spec)]; result has same sign as first arg
1365+
13421366
[modulo ; result has same sign as second arg
13431367
(from-cases
13441368
(-One -One . -> . -Zero)
@@ -1350,39 +1374,7 @@
13501374
(commutative-binop -Fixnum -Int)
13511375
(binop -Int))]
13521376
;; should be consistent with quotient and remainder
1353-
[quotient/remainder
1354-
(from-cases
1355-
(-Zero -Int . -> . (-values (list -Zero -Zero)))
1356-
(-One -One . -> . (-values (list -Zero -One)))
1357-
;; division by one is identity, and has no remainder
1358-
(map (lambda (t) (t -One . -> . (-values (list t -Zero))))
1359-
(list -PosByte -Byte -PosIndex -Index
1360-
-PosFixnum -NonNegFixnum -NegFixnum -NonPosFixnum -Fixnum))
1361-
(-Byte -Nat . -> . (-values (list -Byte -Byte)))
1362-
(-Byte -Int . -> . (-values (list -Fixnum -Byte)))
1363-
(-Index -Nat . -> . (-values (list -Index -Index)))
1364-
(-Index -Int . -> . (-values (list -Fixnum -Index)))
1365-
(-Nat -Byte . -> . (-values (list -Nat -Byte)))
1366-
(-Nat -Index . -> . (-values (list -Nat -Index)))
1367-
(-NonNegFixnum -NonNegFixnum . -> . (-values (list -NonNegFixnum -NonNegFixnum)))
1368-
(-NonNegFixnum -NonPosFixnum . -> . (-values (list -NonPosFixnum -NonNegFixnum)))
1369-
(-NonPosFixnum -NonNegFixnum . -> . (-values (list -NonPosFixnum -NonPosFixnum)))
1370-
(-NonPosFixnum -NonPosFixnum . -> . (-values (list -NonNegFixnum -NonPosFixnum)))
1371-
(-NonNegFixnum -Nat . -> . (-values (list -NonNegFixnum -NonNegFixnum)))
1372-
(-NonNegFixnum -Int . -> . (-values (list -Fixnum -NonNegFixnum)))
1373-
(-Nat -NonNegFixnum . -> . (-values (list -Nat -NonNegFixnum)))
1374-
;; in the following cases, we can't guarantee that the quotient is within
1375-
;; fixnum range: (quotient min-fixnum -1) -> max-fixnum + 1
1376-
(-NonPosFixnum -Int . -> . (-values (list -Int -NonPosFixnum)))
1377-
(-Fixnum -Int . -> . (-values (list -Int -Fixnum)))
1378-
(-Int -Fixnum . -> . (-values (list -Int -Fixnum)))
1379-
(-Nat -Nat . -> . (-values (list -Nat -Nat)))
1380-
(-Nat -NonPosInt . -> . (-values (list -NonPosInt -Nat)))
1381-
(-Nat -Int . -> . (-values (list -Int -Nat)))
1382-
(-NonPosInt -Nat . -> . (-values (list -NonPosInt -NonPosInt)))
1383-
(-NonPosInt -NonPosInt . -> . (-values (list -Nat -NonPosInt)))
1384-
(-NonPosInt -Int . -> . (-values (list -Int -NonPosInt)))
1385-
(-Int -Int . -> . (-values (list -Int -Int))))]
1377+
[quotient/remainder (from-cases quotient/remainder-spec)]
13861378

13871379
[arithmetic-shift (cl->* (-Zero -NonPosInt . -> . -Zero)
13881380
(-Byte -NonPosInt . -> . -Byte)
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#lang typed/racket/base
2+
3+
(: my-remainder1 (-> Integer Fixnum Fixnum))
4+
(define (my-remainder1 x y)
5+
(define-values [q r]
6+
(quotient/remainder x y))
7+
r)
8+
9+
(: my-remainder2 (-> Integer Fixnum Fixnum))
10+
(define (my-remainder2 x y)
11+
(remainder x y))

typed-racket-test/tr-random-testing.rkt

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -107,6 +107,10 @@
107107
(modulo I* I*)
108108
(remainder I* I*)
109109
(quotient I* I*)
110+
(let-values ([(x y) (quotient/remainder I* I*)])
111+
x)
112+
(let-values ([(x y) (quotient/remainder I* I*)])
113+
y)
110114
(gcd I*)
111115
(gcd I* I*)
112116
(gcd I* I* I*)
@@ -372,13 +376,13 @@
372376
(printf "seed: ~s~n" seed)
373377
(flush-output) ; DrDr doesn't print the above if the testing segfaults.
374378

375-
;; start with 1000 small, deterministic test cases, to catch regressions
379+
;; start with 2000 small, deterministic test cases, to catch regressions
376380
(redex-check tr-arith E #:in-order (check-all-reals (term E) verbose?)
377-
#:attempts 1000
381+
#:attempts 2000
378382
#:prepare exp->real-exp
379383
#:keep-going? #t)
380384
(redex-check tr-arith C #:in-order (check-all-reals (term C) verbose?)
381-
#:attempts 1000
385+
#:attempts 2000
382386
#:prepare exp->real-exp
383387
#:keep-going? #t)
384388
;; then switch to purely random to get different ones every run

0 commit comments

Comments
 (0)