Take.curry 1.08 KB
 Michael Hanus committed Oct 04, 2018 1 ``````--- Example to show the non-equivalence of two versions of the `````` Michael Hanus committed Nov 07, 2018 2 3 ``````--- `take` operation, taken from --- `````` Michael Hanus committed May 08, 2019 4 ``````--- Foner, K. and Zhang, H. and Lampropoulos, L.: Keep Your Laziness in Check `````` Michael Hanus committed Nov 07, 2018 5 6 ``````--- ICFP 2018, --- DOI: 10.1145/3236797 `````` Michael Hanus committed Oct 04, 2018 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 `````` import Test.Prop -- take operation from the Prelude: take1 :: Int -> [a] -> [a] take1 n xs | n <= 0 = [] | otherwise = takep n xs where takep _ [] = [] takep m (y:ys) = y : take1 (m-1) ys -- take operation with different pattern matching: take2 :: Int -> [a] -> [a] take2 n [] = [] take2 n (x:xs) | n > 0 = x : take2 (n-1) xs | otherwise = [] -- The equality of both take operations on ground values always succeeds: take_groundequiv x xs = take1 x xs <~> take2 x xs -- Actually, take1 and take2 are not equivalent, as can be seen -- by evaluating `take... failed [])` or `take... 0 failed`. -- Thus, we check the equivalence with CurryCheck: `````` Michael Hanus committed May 08, 2019 30 ``````-- Equivalence is falsified by the 11th test: `````` Michael Hanus committed Oct 04, 2018 31 ``````take_equiv = take1 <=> take2 `````` Michael Hanus committed May 08, 2019 32 33 34 `````` -- With termination information, equivalence is falsified by the 2nd test: take_equiv'TERMINATE = take1 <=> take2``````