import Test.Prop
-- This is an example which shows the "non-referentiality" of Curry (according
-- to [Bacci et al. PPDP'12]), i.e., it shows that two operations, which
-- compute the same values, might compute different results in larger
-- contexts:
data AB = A | B
deriving (Eq,Show)
data C = C AB
deriving (Eq,Show)
h A = A
g x = C (h x)
g' A = C A
-- The computed result equivalence of g and g' on ground values
-- always holds, i.e., g and g' always compute same values:
g_and_g' :: AB -> Prop
g_and_g' x = g x <~> g' x
-- The contextual equivalence of g and g' does not hold:
g_equiv_g' = g <=> g'