NDInsert.curry 1005 Bytes
Newer Older
1 2 3 4 5
--- Example to show the non-equivalence of two versions of a
--- non-deterministic insert operation.

import Test.Prop

6
-- Non-deterministic list insertion defined by overlapping rules:
7 8 9 10
ndinsert1 :: a -> [a] -> [a]
ndinsert1 x ys     = x : ys
ndinsert1 x (y:ys) = y : ndinsert1 x ys

11
-- Non-deterministic list insertion defined by non-overlapping rules:
12 13 14 15 16 17 18 19 20 21 22 23 24 25
ndinsert2 :: a -> [a] -> [a]
ndinsert2 x []     = [x]
ndinsert2 x (y:ys) = x : y : ys  ?  y : ndinsert2 x ys

-- The equality of both ndinsert operations on ground values always succeeds:
ndinsert_groundequiv x xs = ndinsert1 x xs <~> ndinsert2 x xs

-- Actually, ndinsert1 and ndinsert2 are not equivalent, as can be seen
-- by evaluating `head (ndinsert 1 failed)`.
-- Thus, we check the equivalence with CurryCheck:

-- In PAKCS, the counter example is reported by the 7th test:
ndinsert_equiv = ndinsert1 <=> ndinsert2

26 27 28
-- With termination info, the counter example is reported by the 1st test:
ndinsert_equiv'TERMINATE = ndinsert1 <=> ndinsert2