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])