From 570544cb4f2e788f3e071eee1155f626277b0df0 Mon Sep 17 00:00:00 2001 From: Michael Hanus Date: Thu, 4 Oct 2018 17:16:48 +0200 Subject: [PATCH] Adds example for non-equivalence of take operations --- examples/equivalent_operations/Take.curry | 27 +++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 examples/equivalent_operations/Take.curry diff --git a/examples/equivalent_operations/Take.curry b/examples/equivalent_operations/Take.curry new file mode 100644 index 0000000..a42731b --- /dev/null +++ b/examples/equivalent_operations/Take.curry @@ -0,0 +1,27 @@ +--- Example to show the non-equivalence of two versions of the +--- `take` operation. + +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: + +-- In PAKCS, the counter example is reported by the 11th test: +take_equiv = take1 <=> take2 -- GitLab