module testFixed

/*
	Pieter Koopman, 2010
	Radboud Universty, Nijmegen
	The Netherlands
	pieter@cs.ru.nl

	Run with
	- environment gast
	- "Basic Values Only" in the project options 
*/

import StdEnv, gast, fixed

gEq{|Fixed|} x y = x==y

genShow{|Fixed|} sep b fixed rest = [toString fixed:rest]

ggen{|Fixed|} n r = map (\(n,m).n/m) (diag2 numbersPN numbers)
where
	numbers = map toFixed [1..]
	numbersPN = f numbers
	f [a:x] = [a,~a:f x]

pDistMulFixed :: !Fixed !Fixed !Fixed -> Bool
pDistMulFixed a b c = (a+b)*c == a*c+b*c

pAssocMulFixed :: !Fixed !Fixed !Fixed -> Bool
pAssocMulFixed a b c = (a*b)*c == a*(b*c)

pAssocAddFixed :: !Fixed !Fixed !Fixed -> Bool
pAssocAddFixed a b c = (a+b)+c == a+(b+c)

pAddSubFixed :: !Fixed !Fixed !Fixed -> Bool
pAddSubFixed a b c = a-b-c == a-(b+c)

pAbs :: Fixed -> Bool
pAbs f = abs f >= zero

fac :: !BigInt -> BigInt
fac n
	| n <= one
		= one
		= n * fac (n-one)

pFac :: Int -> Property
pFac n = n>0 ==> fac (toBigInt n) == fac (toBigInt (n-1)) * toBigInt n

Start =
	[ Test [Tests 100000, Fails 10, Quiet] pAssocAddFixed
	, Test [Tests 100000, Fails 10, Quiet] pAddSubFixed
	, Test [Tests 100000, Fails 2] pDistMulFixed
	, Test [Tests 100000, Fails 2] pAssocMulFixed
	, Test [] pAbs
	, Test [] (pFac For [1..20])
	]
/*
Expected result:
 Passed after 100000 tests
 Passed after 100000 tests
Counterexample 1 found after 75 tests: -0.33333 1.00000 0.50000
Counterexample 2 found after 84 tests: 0.33333 -1.00000 0.50000
2 counterexamples found, after 84 tests
Counterexample 1 found after 259 tests: 0.33333 0.50000 2.00000
Counterexample 2 found after 334 tests: -0.33333 0.50000 2.00000
2 counterexamples found, after 334 tests
 Passed after 1000 tests
 Proof: success for all arguments after 20 tests
*/