TimSortMerge.hs

import Test.QuickCheck
import Control.Applicative ((<$>))
import Data.List (scanl)

-- To test whether my timsort implementation has the bug described in
-- http://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/
-- Answer: yes :-(

runLengthInvariantBroken :: (Num i, Ord i) => i -> i -> i -> i -> Bool
runLengthInvariantBroken a b c i = (b - a <= i - b) || (c - b <= i - c)

performMerges :: (Num i, Ord i) => [i] -> i -> [i]
performMerges [b,a] i | i - b >= b - a = performMerges [a] i
performMerges (c:b:a:ss) i | runLengthInvariantBroken a b c i =
  if i - c <= b - a
    then performMerges (b:a:ss) i
    else performMerges (c:a:ss) i
performMerges s _ = s

-- the output of `performMerges [245, 225, 200, 120, 0] 275` violates the
-- invariants.

-- fixed version of 'performMerges'
performMerges' :: (Num i, Ord i) => [i] -> i -> [i]
performMerges' [b,a] i | i - b >= b - a = performMerges' [a] i
performMerges' (c:b:a:ss) i | runLengthInvariantBroken a b c i =
  if i - c <= b - a
    then performMerges' (b:a:ss) i
    else performMerges' (c : performMerges' (a:ss) c) i
performMerges' s _ = s

invariantsHold :: (Num i, Ord i) => [i] -> i -> Bool
invariantsHold [] _ = True
invariantsHold [a] i = a <= i
invariantsHold [b,a] i = b-a > i-b
invariantsHold (c:b:a:ss) i =
  i-c < c-b && i-b < b-a && invariantsHold (b:a:ss) c

data Runs = Runs { runIndices :: [Integer]
                 , currIndex :: Integer
                 } deriving (Show, Eq)

mkFibby :: Num i => [i] -> [i]
mkFibby = iter 0 0
  where
    iter _ _ [] = []
    iter i j (x:xs) =
      let x' = i + j + x
      in x' : iter j x' xs

instance Arbitrary Runs where
  arbitrary = do
    is <- scanr (+) 0 . mkFibby <$> listOf1 (pos <$> arbitrary)
    i <- (+) (head is) . pos <$> arbitrary
    return $ Runs is i
    where pos n = 1 + abs n

prop_performMerges_invariantsHold :: Runs -> Bool
prop_performMerges_invariantsHold (Runs is i) =
  invariantsHold (performMerges' is i) i