Update examples for equivalent operations

docs/manual.tex

@@ -745,13 +745,13 @@ e.g., determinism, postconditions, specifications,
 so that they are not tested:
 \begin{itemize}
 \item
-If there is a proof file \code{proof-$M$-$f$IsDeterministic.*},
+If there is a proof file \code{proof-$M$-$f$-IsDeterministic.*},
 a determinism annotation for operation $M.f$ is not tested.
 \item
-If there is a proof file \code{proof-$M$-$f$SatisfiesPostCondition.*},
+If there is a proof file \code{proof-$M$-$f$-SatisfiesPostCondition.*},
 a postcondition for operation $M.f$ is not tested.
 \item
-If there is a proof file \code{proof-$M$-$f$SatisfiesSpecification.*},
+If there is a proof file \code{proof-$M$-$f$-SatisfiesSpecification.*},
 a specification for operation $M.f$ is not tested.
 \end{itemize}
 Note that the file suffix and all non-alpha-numberic characters

examples/equivalent_operations/BacciEtAl12.curry

+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

examples/equivalent_operations/Intersperse.curry

@@ -22,5 +22,11 @@ intersperse2 sep (x:xs) = x : go xs
   go (y:ys) = sep : y : go ys
 
 
--- These operations are not equivalent:
+-- These operations are not equivalent (falsified by 43th test):
 intersperseEquiv = intersperse1 <=> intersperse2
+
+-- These operations are not equivalent (falsified by 4th test):
+intersperseEquiv'TERMINATE = intersperse1 <=> intersperse2
+
+-- Ground equivalence testing is successful:
+intersperseEquiv'GROUND x xs = intersperse1 x xs <~> intersperse2 x xs

examples/equivalent_operations/Ints12.curry

 -- Testing the equivalence of non-terminating operations:
 
-import Data.Nat
 import Test.Prop
 
 -- Two different infinite lists:

examples/equivalent_operations/NDInsert.curry

@@ -23,3 +23,6 @@ ndinsert_groundequiv x xs = ndinsert1 x xs <~> ndinsert2 x xs
 -- In PAKCS, the counter example is reported by the 7th test:
 ndinsert_equiv = ndinsert1 <=> ndinsert2
 
+-- With termination info, the counter example is reported by the 1st test:
+ndinsert_equiv'TERMINATE = ndinsert1 <=> ndinsert2
+

examples/equivalent_operations/Perm.curry

+import Test.Prop
+
+-- Definition of permute from library Combinatorial
+-- Note that this definition is "spine strict", i.e., it does not return
+-- any partial value for partial lists, e.g.,
+-- head (permute (1:failed))  ---> no value!
+permute        :: [a] -> [a]
+permute []     = []
+permute (x:xs) = ndinsert (permute xs)
+    where ndinsert [] = [x]
+          ndinsert (y:ys) = (x:y:ys) ? (y:ndinsert ys)
+
+-- An alternative, less strict definition of permutations, e.g.,
+-- head (perm (1:failed))  --->  1
+perm :: [a] -> [a]
+perm []     = []
+perm (x:xs) = ndinsert x (perm xs)
+  where ndinsert x ys     = x : ys
+        ndinsert x (y:ys) = y : ndinsert x ys
+
+------------------------------------------------------------------
+
+-- Equivalence falsified by 13th test:
+permEquiv = perm <=> permute
+
+-- Equivalence falsified by 3rd test:
+permEquiv'TERMINATE = perm <=> permute
+
+-- Ground equivalence not falsified:
+permEquiv'GROUND xs = perm xs <~> permute xs

examples/equivalent_operations/README.md

+Equivalence checking with CurryCheck
+====================================
+
 This directory contains some examples for the use
 of CurryCheck to check the equivalence of operations.
 
 Since most of these are examples to test whether CurryCheck
 is able to report counter-examples, their test fails intentionally.
 These are the programs
+- BacciEtAl12 (simple example from Bacci et al PPDP'12)
 - Intersperse (inserting separators in a list [Christiansen/Seidel'11])
 - Ints12 (generators for infinite lists)
 - NDInsert (non-deterministic list insertion)
+- Perm (permutation from library Combinatorial vs. less strict version)
 - RevRev (double reverse)
-- SimpleExample
 - SortEquiv (two variants of permutation sort)
+- SortPermute (two variants of permutation sort with a stricter permutation)
 - Take (two variants of take [Foner/Zhang/Lampropoulos'18])
 - Unzip (two variants of unzip [Chitil'11])
 

examples/equivalent_operations/RevRev.curry

@@ -6,4 +6,12 @@ revrev xs = reverse (reverse xs)
 -- Test: is double reverse equivalent to the identity?
 -- This is not the case if both are applied to the context
 --     head (... (1:failed))
+
+-- Equivalence falsified by 13th test:
+revrevid = revrev <=> id
+
+-- Equivalence falsified by 3rd test:
 revrevid'TERMINATE = revrev <=> id
+
+-- Ground equivalence not falsified:
+revrevid'GROUND xs = revrev xs <~> id xs

examples/equivalent_operations/SimpleExample.curry

-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'

examples/equivalent_operations/SortPermute.curry

+import Test.Prop
+
+-- Definition of permute from library `Combinatorial` (part of PAKCS
+-- distribution up to version 2.0.2 and contained in Curry package
+-- `combinatorial` version 1.0.0).
+--
+-- Note that this definition is "spine strict", i.e., it does not return
+-- any partial value for partial lists, e.g.,
+-- head (permute (1:failed))  ---> no value!
+permute        :: [a] -> [a]
+permute []     = []
+permute (x:xs) = ndinsert (permute xs)
+    where ndinsert [] = [x]
+          ndinsert (y:ys) = (x:y:ys) ? (y:ndinsert ys)
+
+------------------------------------------------------------------
+
+sorted :: Ord a => [a] -> Bool
+sorted [] = True
+sorted [_] = True
+sorted (x:y:zs) = x<=y && sorted (y:zs)
+
+psort :: Ord a => [a] -> [a]
+psort xs | sorted ys = ys where ys = permute xs
+
+------------------------------------------------------------------
+
+idSorted :: Ord a => [a] -> [a]
+idSorted [] = []
+idSorted [x] = [x]
+idSorted (x:y:zs) | x<=y = x : idSorted (y:zs)
+
+isort :: Ord a => [a] -> [a]
+isort xs = idSorted (permute xs)
+
+------------------------------------------------------------------
+
+-- Equivalence falsified by 1174th test:
+equiv = psort <=> (isort :: [Int] -> [Int])
+
+-- Equivalence falsified by 46th test:
+equiv'TERMINATE = psort <=> (isort :: [Int] -> [Int])

examples/equivalent_operations/Take.curry

 --- Example to show the non-equivalence of two versions of the
 --- `take` operation, taken from
 ---
---- Foner, K. and Zhang, H. and Lampropoulos, L.: {Keep Your Laziness in Check
+--- Foner, K. and Zhang, H. and Lampropoulos, L.: Keep Your Laziness in Check
 --- ICFP 2018,
 --- DOI: 10.1145/3236797
 
@@ -27,5 +27,8 @@ take_groundequiv x xs = take1 x xs <~> take2 x xs
 -- 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:
+-- Equivalence is falsified by the 11th test:
 take_equiv = take1 <=> take2
+
+-- With termination information, equivalence is falsified by the 2nd test:
+take_equiv'TERMINATE = take1 <=> take2

examples/equivalent_operations/Unzip.curry

@@ -14,7 +14,13 @@ unzip1 ((x,y):ps) = (x:xs,y:ys) where (xs,ys) = unzip1 ps
 
 --- Definition from Chitil'11:
 unzip2 :: [(a,b)] -> ([a],[b])
-unzip2 xs = foldr (\(a,b) (as,bs) -> (a:as,b:bs)) ([],[]) xs
+unzip2 xs = foldr (\ (a,b) (as,bs) -> (a:as,b:bs)) ([],[]) xs
 
--- These operations are not equivalent:
+-- Equivalence falsified by 27th test:
 unzipEquiv = unzip1 <=> unzip2
+
+-- Equivalence falsified by 6th test:
+unzipEquiv'TERMINATE = unzip1 <=> unzip2
+
+-- Ground equivalence is not falsified:
+unzipEquiv'GROUND xs = unzip1 xs <~> unzip2 xs

package.json

@@ -15,15 +15,14 @@
         "easycheck"     : ">= 0.0.1",
         "flatcurry"     : ">= 2.0.0",
         "frontend-exec" : ">= 0.0.1",
-        "peano"         : ">= 1.0.0",
         "profiling"     : ">= 1.0.0",
         "rewriting"     : ">= 2.0.0",
         "setfunctions"  : ">= 0.0.1",
         "wl-pprint"     : ">= 0.0.1"
     },
     "compilerCompatibility": {
-        "pakcs": ">= 2.0.0",
-        "kics2": ">= 2.0.0"
+        "pakcs": ">= 2.0.0, < 3.0.0",
+        "kics2": ">= 2.0.0, < 3.0.0"
     },
     "configModule": "CC.Config",
     "executable": {