{-# OPTIONS_CYMAKE -Wno-overlapping #-}

-- Contract verification requires option "-s"

--- Non-deterministic list insertion
ins :: a -> [a] -> [a]
ins x ys     = x : ys
ins x (y:ys) = y : ins x ys

-- Postcondition on the length of the list.
ins'post :: a -> [a] -> [a] -> Bool
ins'post _ xs ys = length xs + 1 == length ys

--- Insertion sort with a non-deterministic insert operator.
--- This computes all permutations of the input list, see also
--- Christiansen, J. and Danilenko, N. and Dylus, S.:
--- All sorts of permutations (functional pearl), ICFP 2016,
--- DOI: 10.1145/2951913.2951949
insertionSort  :: [a] -> [a]
insertionSort []     = []
insertionSort (x:xs) = ins x (insertionSort xs)

-- Postcondition: input and output lists have same length.
insertionSort'post ::[a] -> [a] -> Bool
insertionSort'post xs ys = length xs == length ys

-- Compute all permutations of the list [1,2,3]:
main :: [Int]
main = insertionSort [1,2,3]