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