Take.curry 1.08 KB
Newer Older
1
--- Example to show the non-equivalence of two versions of the
Michael Hanus 's avatar
Michael Hanus committed
2 3
--- `take` operation, taken from
---
4
--- Foner, K. and Zhang, H. and Lampropoulos, L.: Keep Your Laziness in Check
Michael Hanus 's avatar
Michael Hanus committed
5 6
--- ICFP 2018,
--- DOI: 10.1145/3236797
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:

30
-- Equivalence is falsified by the 11th test:
31
take_equiv = take1 <=> take2
32 33 34

-- With termination information, equivalence is falsified by the 2nd test:
take_equiv'TERMINATE = take1 <=> take2