1 module FixedTest ( 2 main 3 ) where 4 5 import Data.Ratio (numerator, denominator, (%)) 6 import Fixed 7 import Test.QuickCheck hiding (Fixed, scale) 8 9 -- for makeFixed use FP 10 11 siGen :: Gen Integer -- signed integer 12 siGen = choose (-499,499) 13 14 piGen :: Gen Integer -- positive integer 15 piGen = choose (1,499) 16 17 type R = Decimal -- Binary 18 19 ssGen :: Gen (Scale R) -- scale 20 ssGen = choose (0,4) >>= (return . Scale) 21 22 tpGen :: Gen Integer -- tiny positive integer 23 tpGen = choose (1,10) 24 25 tsGen :: Gen (Fixed R) -- tiny scaled decimal 26 tsGen = 27 let tiGen = choose (-5,5) 28 txGen = choose (0,2) >>= (return . Scale) 29 in do i <- tiGen 30 s <- txGen 31 return $ FP i s 32 33 sdGen :: Gen (Fixed R) -- scaled decimal 34 sdGen = 35 do i <- siGen 36 s <- ssGen 37 return $ FP i s 38 39 nzGen :: Gen (Fixed R) -- non-zero scaled decimal 40 nzGen = 41 do j <- piGen 42 n <- elements [False,True] 43 let i = if n then negate j else j 44 s <- ssGen 45 return $ FP i s 46 47 prop_integers_have_scale_zero = 48 forAll siGen $ \i -> 49 scale (fromInteger i :: Fixed R) == 0 50 51 prop_fromInteger_is_invertible = 52 forAll siGen $ \i -> 53 toInteger (fromInteger i :: Fixed R) == i 54 {- 55 56 prop_scale = 57 forAll siGen $ \i -> 58 forAll ssGen $ \s -> 59 scale (toScaledDecimal i s) == s 60 61 prop_scale_of_make = 62 forAll siGen $ \i -> 63 forAll ssGen $ \s -> 64 let x = makeScaledDecimal i s in 65 scale x == s && toScaledDecimal x s == x 66 67 prop_ratio = 68 forAll siGen $ \n -> 69 forAll piGen $ \d -> 70 forAll ssGen $ \s -> 71 ratio (toScaledDecimal n s) (toScaledDecimal d s) == ratio n d 72 73 prop_equality_ignores_scale = 74 forAll siGen $ \n -> 75 forAll ssGen $ \s -> 76 forAll ssGen $ \t -> 77 toScaledDecimal n s == toScaledDecimal n t 78 79 -} 80 81 prop_equality_is_reflexive = 82 forAll sdGen $ \x -> 83 x == x 84 85 prop_equality_is_symmetric = 86 forAll sdGen $ \x -> 87 forAll sdGen $ \y -> 88 (x == y) == (y == x) 89 90 prop_equality_is_transitive = 91 forAll tsGen $ \x -> 92 forAll tsGen $ \y -> 93 forAll tsGen $ \z -> 94 x == y ==> (y == z) == (x == z) 95 96 prop_order_trichotomy = 97 forAll sdGen $ \x -> 98 forAll sdGen $ \y -> 99 (length $ filter id $ [x < y, x == y, x > y]) == 1 100 101 prop_order_is_irreflexive = 102 forAll sdGen $ \x -> 103 not (x < x) 104 105 prop_order_is_transitive = 106 forAll sdGen $ \x -> 107 forAll sdGen $ \y -> 108 forAll sdGen $ \z -> 109 if x < y && y < z then x < z else 110 if x > y && y > z then x > z else True 111 112 prop_negate_matches_minus = 113 forAll sdGen $ \x -> 114 negate x == fromInteger 0 - x 115 116 prop_negate_negates_sign = 117 forAll sdGen $ \x -> 118 signum (negate x) == negate (signum x) 119 120 prop_negate_cancels = 121 forAll sdGen $ \x -> 122 negate (negate x) == x 123 124 prop_abs_is_not_negative = 125 forAll sdGen $ \x -> 126 abs x >= 0 && (abs x == 0) == (x == 0) 127 128 prop_abs_of_negate_is_abs = 129 forAll sdGen $ \x -> 130 abs (negate x) == abs x 131 132 prop_abs_times_sign_is_identity = 133 forAll sdGen $ \x -> 134 abs x * signum x == x 135 136 prop_gcd_is_ok = 137 forAll nzGen $ \x -> 138 forAll nzGen $ \y -> 139 lia_gcd x y `lia_divides` x && 140 lia_gcd x y `lia_divides` y 141 142 prop_lcm_is_ok = 143 forAll nzGen $ \x -> 144 forAll nzGen $ \y -> 145 x `lia_divides` lia_lcm x y && 146 y `lia_divides` lia_lcm x y 147 148 prop_lia_dim = 149 forAll sdGen $ \x -> 150 forAll sdGen $ \y -> 151 (lia_dim x y) == max (x - y) (fromInteger 0) 152 153 prop_lia_signum = 154 forAll sdGen $ \x -> 155 lia_signum x == signum x || 156 (lia_signum x == 1 && x == 0) 157 158 {- 159 prop_less_and_greater_are_opposites = 160 forAll sdGen $ \x -> 161 forAll sdGen $ \y -> 162 (x < y) == (y > x) 163 164 prop_less_and_greater_equal_are_complements = 165 forAll sdGen $ \x -> 166 forAll sdGen $ \y -> 167 (x < y) /= (x >= y) 168 169 prop_to_integer_is_inverse_of_from_integer = 170 forAll siGen $ \i -> 171 toInteger (fromInteger i :: ScaledDecimal) == i 172 173 prop_addition_distributes_over_make = 174 forAll siGen $ \i -> 175 forAll siGen $ \j -> 176 forAll ssGen $ \s -> 177 makeScaledDecimal i s + makeScaledDecimal j s == makeScaledDecimal (i+j) s 178 179 -} 180 181 prop_zero_is_additive_identity = 182 forAll sdGen $ \x -> 183 forAll ssGen $ \s -> 184 let z = FP 0 s in 185 z + x == x && x + z == x && x - z == x 186 187 prop_addition_commutes = 188 forAll sdGen $ \x -> 189 forAll sdGen $ \y -> 190 x + y == y + x 191 192 prop_addition_associates = 193 forAll sdGen $ \x -> 194 forAll sdGen $ \y -> 195 forAll sdGen $ \z -> 196 x + (y + z) == (x + y) + z 197 198 prop_negation_is_compatible_with_subtraction = 199 forAll sdGen $ \x -> 200 forAll sdGen $ \y -> 201 x - y == x + negate y 202 203 prop_subtraction_is_skew_commutative = 204 forAll sdGen $ \x -> 205 forAll sdGen $ \y -> 206 x - y == negate (y - x) 207 208 prop_zero_is_multiplicative_zero = 209 forAll sdGen $ \x -> 210 forAll ssGen $ \s -> 211 let z = toFixed 0 s in 212 z * x == z && x * z == z 213 214 prop_one_is_multiplicative_identity = 215 forAll sdGen $ \x -> 216 forAll ssGen $ \s -> 217 let w = toFixed 1 s in 218 w * x == x && x * w == x 219 220 prop_minus_one_is_multiplicative_negater = 221 forAll sdGen $ \x -> 222 forAll ssGen $ \s -> 223 let m = toFixed (negate 1) s in 224 m * x == negate x && x * m == negate x 225 226 prop_multiplication_commutes = 227 forAll sdGen $ \x -> 228 forAll sdGen $ \y -> 229 x * y == y * x 230 231 prop_multiplication_associates = 232 forAll sdGen $ \x -> 233 forAll sdGen $ \y -> 234 forAll sdGen $ \z -> 235 x * (y * z) == (x * y) * z 236 {- 237 prop_multiplication_distributes_over_make = 238 forAll siGen $ \i -> 239 forAll siGen $ \j -> 240 forAll ssGen $ \s -> 241 forAll ssGen $ \t -> 242 makeScaledDecimal i s * makeScaledDecimal j t == 243 makeScaledDecimal (i*j) (s+t) 244 -} 245 prop_left_distribution_holds = 246 forAll sdGen $ \x -> 247 forAll sdGen $ \y -> 248 forAll sdGen $ \z -> 249 x * (y + z) == x * y + x * z 250 251 prop_signum_abstracts_times = 252 forAll sdGen $ \x -> 253 forAll sdGen $ \y -> 254 signum (x * y) == signum x * signum y 255 256 prop_right_distribution_holds = 257 forAll sdGen $ \x -> 258 forAll sdGen $ \y -> 259 forAll sdGen $ \z -> 260 (y + z) * x == y * x + z * x 261 262 prop_zero_pow_is_zero = 263 forAll ssGen $ \s -> 264 let z = toFixed 0 s in 265 forAll tpGen $ \n -> 266 z ^ n == z 267 268 prop_one_pow_is_one = 269 forAll ssGen $ \s -> 270 let w = toFixed 1 s in 271 forAll tpGen $ \n -> 272 w ^ n == w 273 274 prop_pow_zero_is_unity = 275 forAll sdGen $ \x -> 276 x ^ 0 == 1 277 278 prop_pow_one_is_identity = 279 forAll sdGen $ \x -> 280 x ^ 1 == x 281 282 prop_pow_two_is_square = 283 forAll sdGen $ \x -> 284 x ^ 2 == x * x 285 286 {- 287 was_power_of_10 :: Integer -> Bool 288 289 was_power_of_10 n 290 | n`mod`2 == 0 = was_power_of_10 (n`div`2) 291 | n`mod`5 == 0 = was_power_of_10 (n`div`5) 292 | True = n == 1 293 294 prop_sds_are_rationals = 295 forAll siGen $ \n -> 296 forAll ssGen $ \s -> 297 toRational (toScaledDecimal n s) == ratio n 1 298 299 prop_sds_are_decimal_rationals = 300 forAll sdGen $ \x -> 301 was_power_of_10 (denominator (toRational x)) 302 303 prop_recip_is_trivial = 304 forAll nzGen $ \x -> 305 recip x == 1 / x 306 307 -- I want to say something about division. For example, 308 -- (n*x)/x == n && (n*x)/n == x. 309 -- But I can't; these "laws" are NOT valid for scaled (/). 310 311 prop_div_mod_fit_together = 312 forAll sdGen $ \x -> 313 forAll nzGen $ \y -> 314 let (q,r) = x `divMod` y in 315 scale q == 0 && 316 scale r == max (scale x) (scale y) && 317 q * y + r == x 318 319 prop_div_is_floored_division = 320 forAll sdGen $ \x -> 321 forAll nzGen $ \y -> 322 x `div` y == fromInteger (floor (ratio x y)) 323 324 prop_quot_rem_fit_together = 325 forAll sdGen $ \x -> 326 forAll nzGen $ \y -> 327 let (q,r) = x `quotRem` y in 328 scale q == 0 && 329 scale r == max (scale x) (scale y) && 330 q * y + r == x 331 332 prop_quot_is_truncated_division = 333 forAll sdGen $ \x -> 334 forAll nzGen $ \y -> 335 x `quot` y == fromInteger (truncate (ratio x y)) 336 -} 337 338 prop_succ_is_greater = 339 forAll sdGen $ \x -> 340 succ x > x 341 342 prop_pred_is_less = 343 forAll sdGen $ \x -> 344 pred x < x 345 346 prop_pred_is_inverse_of_succ = 347 forAll sdGen $ \x -> 348 succ (pred x) == x 349 350 prop_succ_is_inverse_of_pred = 351 forAll sdGen $ \x -> 352 pred (succ x) == x 353 354 prop_succ_increments_bottom_digit = 355 forAll sdGen $ \x -> 356 succ x == x + FP 1 (scale x) 357 358 prop_pred_decrements_bottom_digit = 359 forAll sdGen $ \x -> 360 pred x == x - FP 1 (scale x) 361 362 prop_enum_empty = 363 forAll sdGen $ \x -> 364 forAll sdGen $ \y -> 365 length (if x < y then [y..x] else if x > y then [x..y] else[]) == 0 366 367 prop_enum_single = 368 forAll sdGen $ \x -> 369 [x..x] == [x] 370 371 {- 372 prop_read_of_integer_is_ok = 373 forAll siGen $ \n -> 374 read (show n) == toScaledDecimal n 0 375 376 prop_read_of_show_is_exact = 377 forAll sdGen $ \x -> 378 read (show x) == x 379 380 prop_show_of_integer_is_ok = 381 forAll siGen $ \n -> 382 show (fromIntegral n :: ScaledDecimal) == show n 383 384 trim :: String -> String 385 trim str = loop (reverse str) 386 where loop ('0' : cs) = loop cs 387 loop cs = if '.' `elem` cs then reverse cs else str 388 389 prop_show_of_read_is_almost_identity = 390 forAll sdGen $ \x -> 391 let str = show x in 392 trim (show (read str :: ScaledDecimal)) == trim str 393 394 prop_truncate_truncates = 395 forAll sdGen $ \x -> 396 let t = fromIntegral (truncate x) in 397 if x < 0 then x <= t && t-1 < x else t <= x && x < t+1 398 399 prop_floor_floors = 400 forAll sdGen $ \x -> 401 let t = fromIntegral (floor x) in 402 t <= x && x < t+1 403 404 prop_ceiling_ceilings = 405 forAll sdGen $ \x -> 406 let t = fromIntegral (ceiling x) in 407 t >= x && x > t-1 408 409 prop_round_rounds = 410 forAll sdGen $ \x -> 411 let t = fromIntegral (round x) in 412 abs (x - t)*2 <= 1 413 -} 414 415 prop_convert_Down = 416 forAll sdGen $ \x -> 417 let (y,z) = convertFixed Down x in 418 fromInteger y <= x && x < fromInteger (y + 1) && 419 fromInteger y + z == x 420 421 prop_convert_Up = 422 forAll sdGen $ \x -> 423 let (y,z) = convertFixed Up x in 424 fromInteger y >= x && x > fromInteger (y - 1) && 425 fromInteger y + z == x 426 427 prop_convert_In = 428 forAll sdGen $ \x -> 429 let (y,z) = convertFixed In x in 430 (if x > 0 then y >= 0 && fromInteger y <= x && x < fromInteger (y+1) else 431 if x < 0 then y <= 0 && fromInteger y >= x && x > fromInteger (y-1) else 432 y == 0 && z == x) && 433 fromInteger y + z == x 434 435 prop_convert_Out_zero = 436 forAll ssGen $ \s -> 437 let x = FP 0 s in 438 let (y,z) = convertFixed Out x in 439 y == 0 && z == x && fromInteger y + z == x 440 441 prop_convert_Out = 442 forAll sdGen $ \x -> 443 let (y,z) = convertFixed Out x in 444 (if x > 0 then y > 0 && fromInteger y >= x && x > fromInteger (y-1) else 445 if x < 0 then y < 0 && fromInteger y <= x && x < fromInteger (y+11) else 446 y == 0 && z == x) && 447 fromInteger y + z == x 448 449 prop_convert_Even = 450 forAll sdGen $ \x -> 451 let (y,z) = convertFixed Even x in 452 even y && 453 fromInteger y + z == x 454 455 to_integer round x = y where (y,_) = convertFixed round x 456 457 prop_convert_In_symmetry = 458 forAll sdGen $ \x -> 459 to_integer In (negate x) == negate (to_integer In x) 460 461 prop_convert_Out_symmetry = 462 forAll sdGen $ \x -> 463 to_integer Out (negate x) == negate (to_integer Out x) 464 465 prop_convert_Even_symmetry = 466 forAll sdGen $ \x -> 467 to_integer Even (negate x) == negate (to_integer Even x) 468 469 prop_convert_Nearest_In_symmetry = 470 forAll sdGen $ \x -> 471 to_integer (Nearest In) (negate x) == negate (to_integer (Nearest In) x) 472 473 prop_convert_Nearest_Out_symmetry = 474 forAll sdGen $ \x -> 475 to_integer (Nearest Out) (negate x) == negate (to_integer (Nearest Out) x) 476 477 prop_convert_Nearest_Even_symmetry = 478 forAll sdGen $ \x -> 479 to_integer (Nearest Even) (negate x) == negate (to_integer (Nearest Even) x) 480 481 {- 482 prop_read_inverts_show = 483 forAll sdGen $ \x -> 484 case readFixedDecimal (show x) of 485 [(y,"")] -> y == x 486 _ -> False 487 -} 488 main = 489 do {- 490 check prop_scale 491 check prop_scale_of_make 492 check prop_ratio 493 check prop_equality_ignores_scale 494 -} 495 putStrLn "convert:" 496 497 check prop_convert_Down 498 check prop_convert_Up 499 check prop_convert_In 500 check prop_convert_Out 501 check prop_convert_Out_zero 502 check prop_convert_Even 503 504 putStrLn "convert symmetries:" 505 506 check prop_convert_In_symmetry 507 check prop_convert_Out_symmetry 508 check prop_convert_Even_symmetry 509 check prop_convert_Nearest_In_symmetry 510 check prop_convert_Nearest_Out_symmetry 511 check prop_convert_Nearest_Even_symmetry 512 513 putStrLn "integer:" 514 515 check prop_integers_have_scale_zero 516 check prop_fromInteger_is_invertible 517 518 putStrLn "equality:" 519 520 check prop_equality_is_reflexive 521 check prop_equality_is_symmetric 522 check prop_equality_is_transitive 523 524 putStrLn "order:" 525 526 check prop_order_trichotomy 527 check prop_order_is_irreflexive 528 check prop_order_is_transitive 529 530 putStrLn "negation:" 531 532 check prop_negate_matches_minus 533 check prop_negate_negates_sign 534 check prop_negate_cancels 535 536 putStrLn "abs:" 537 538 check prop_abs_is_not_negative 539 check prop_abs_of_negate_is_abs 540 check prop_abs_times_sign_is_identity 541 542 putStrLn "addition and subtraction:" 543 544 check prop_zero_is_additive_identity 545 check prop_addition_commutes 546 check prop_addition_associates 547 check prop_negation_is_compatible_with_subtraction 548 check prop_subtraction_is_skew_commutative 549 550 putStrLn "multiplication:" 551 552 check prop_zero_is_multiplicative_zero 553 check prop_one_is_multiplicative_identity 554 check prop_minus_one_is_multiplicative_negater 555 check prop_signum_abstracts_times 556 check prop_multiplication_commutes 557 check prop_multiplication_associates 558 check prop_left_distribution_holds 559 check prop_right_distribution_holds 560 561 putStrLn "power:" 562 563 check prop_zero_pow_is_zero 564 check prop_one_pow_is_one 565 check prop_pow_zero_is_unity 566 check prop_pow_one_is_identity 567 check prop_pow_two_is_square 568 569 putStrLn "gcd and lcm:" 570 571 check prop_gcd_is_ok 572 check prop_lcm_is_ok 573 check prop_lia_dim 574 check prop_lia_signum 575 576 putStrLn "succ and pred:" 577 578 check prop_succ_is_greater 579 check prop_pred_is_less 580 check prop_pred_is_inverse_of_succ 581 check prop_succ_is_inverse_of_pred 582 check prop_succ_increments_bottom_digit 583 check prop_pred_decrements_bottom_digit 584 585 putStrLn "enum:" 586 587 check prop_enum_empty 588 check prop_enum_single 589 590 {- 591 check prop_read_inverts_show 592 check prop_less_and_greater_are_opposites 593 check prop_less_and_greater_equal_are_complements 594 check prop_to_integer_is_inverse_of_from_integer 595 check prop_addition_distributes_over_make 596 check prop_multiplication_distributes_over_make 597 598 check prop_sds_are_rationals 599 check prop_sds_are_decimal_rationals 600 check prop_recip_is_trivial 601 check prop_div_mod_fit_together 602 check prop_div_is_floored_division 603 check prop_quot_rem_fit_together 604 check prop_quot_is_truncated_division 605 check prop_read_of_integer_is_ok 606 check prop_read_of_show_is_exact 607 check prop_show_of_integer_is_ok 608 check prop_show_of_read_is_almost_identity 609 check prop_truncate_truncates 610 check prop_floor_floors 611 check prop_ceiling_ceilings 612 check prop_round_rounds 613 -} 614 return () 615 where check = quickCheckWith myArgs 616 myArgs = Args {replay = Nothing, maxSuccess = 1000, 617 maxDiscardRatio = 500, maxSize = 100, chatty = True} 618