import Test.Prop

-- This is an example from
--
-- G. Bacci, M. Comini, M.A. Feliu, A. Villanueva:
-- Automatic Synthesis of Specifications for First Order Curry
-- Proc. Principles and Practice of Declarative Programming (PPDP'12),
-- ACM Press, pp. 25-34
--
-- It shows that two operations, which compute the same values,
-- might compute different results in larger contexts.
-- This example is also used in the introduction of the paper
-- explaining the equivalence checking features implemented in CurryCheck:
--
-- Antoy, S., Hanus, M.:
-- Equivalence Checking of Non-deterministic Operations
-- Proc. 14th Int. Symp. on Functional and Logic Programming (FLOPS 2018),
-- Springer LNCS 10818, pp. 149-165, 2018

data AB = A | B
 deriving (Eq,Show)

data C = C AB
 deriving (Eq,Show)

h :: AB -> AB
h A = A

f :: AB -> C
f x = C (h x)

g :: AB -> C
g A = C A


-- The computed result equivalence of f and g on ground values
-- always holds, i.e., f and g always compute same values.
-- Since the domain is finite, this property is actually proved by CurryCheck.
f_and_g :: AB -> Prop
f_and_g x = f x <~> g x

-- The contextual equivalence of f and g  does not hold.
-- The counter-example is found by CurryCheck with the 2nd test
-- (or with the 1st test when option "--equivalence=autoselect" is used).
f_equiv_g :: Prop
f_equiv_g = f <=> g