module NaiveSort2 where
-- Selection Sort from Permutation Sort
permute :: [a] -> [a]
permute [] = [] -- (1)
permute (h:ts) = let (x,rest) = pick (h:ts) in x:(permute rest) -- (2)
pick :: [a] -> (a,[a])
pick [x] = (x,[]) -- (3)
pick (x:y:zs) = (x,y:zs) -- (4)
pick (x:y:zs) = let (w,rest) = pick (y:zs) in (w,x:rest) -- (5)
isSorted :: Ord a => [a] -> Bool
isSorted [] = True -- (6)
isSorted [_] = True -- (7)
isSorted (x:y:zs) = x <= y && isSorted (y:zs) -- (8)
naivesort :: Ord a => [a] -> [a]
naivesort xs | isSorted ys = ys where ys = permute xs -- (9)
-- LEMMATA:
-- forall x,xs. isSorted x:xs => all (x<=) xs -- (10)
-- forall p,xs. all p xs <=> all p (permute xs) -- (11)
-- unfold (1,2) in (10), simplify:
-- naivesort [] = [] -- (12)
-- naivesort (h:ts) | isSorted ys = ys
-- where ys = x:(permute rest)
-- where (x,rest) = pick (h:ts) -- (13)
-- applying lemma (10) in (13):
-- naivesort (h:ts) | all (x<=) (permute rest) && isSorted ys = ys
-- where ys = x:(permute rest)
-- where (x,rest) = pick (h:ts) -- (14)
-- applying lemma (11) in (14):
-- naivesort (h:ts) | all (x<=) rest && isSorted ys = ys
-- where ys = x:(permute rest)
-- where (x,rest) = pick (h:ts) -- (15)
-- applying lemma (10) in (15):
-- naivesort (h:ts) | isSorted ys = ys
-- where ys = x:(permute rest)
-- where (x,rest) = pick (h:ts) -- (16)
-- summarizing:
-- not_so_naive_sort :: Ord a => [a] -> [a]
-- not_so_naive_sort [] = []
-- not_so_naive_sort (h:ts) | all (x<=) rest && isSorted ys = ys where ys = x:(permute rest)
-- where (x,rest) = pick (h:ts)
-- hmmm, Sloth had problems parsing the previous definition, so I had
-- to rephrase it in the following way :(
cut :: Int -> a
cut 42 = cut 0
not_so_naive_sort :: Ord a => [a] -> [a]
not_so_naive_sort [] = []
not_so_naive_sort (h:ts) =
let (x,rest) = pick (h:ts) in
let ys = x:(permute rest) in
if isSorted ys
then ys
else cut 0