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