Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
7
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
curry-packages
currycheck
Commits
8450c6e8
Commit
8450c6e8
authored
Oct 04, 2018
by
Michael Hanus
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Adds example for non-equivalence of take operations
parent
dd8ab9f8
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
27 additions
and
0 deletions
+27
-0
examples/equivalent_operations/Take.curry
examples/equivalent_operations/Take.curry
+27
-0
No files found.
examples/equivalent_operations/Take.curry
0 → 100644
View file @
8450c6e8
--- 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
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment