liquidhaskell-0.8.10.7: benchmarks/vector-algorithms-0.5.4.2/Data/Vector/Algorithms/Merge.hs
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ScopedTypeVariables #-}
-- ---------------------------------------------------------------------------
-- |
-- Module : Data.Vector.Algorithms.Merge
-- Copyright : (c) 2008-2011 Dan Doel
-- Maintainer : Dan Doel <dan.doel@gmail.com>
-- Stability : Experimental
-- Portability : Portable
--
-- This module implements a simple top-down merge sort. The temporary buffer
-- is preallocated to 1/2 the size of the input array, and shared through
-- the entire sorting process to ease the amount of allocation performed in
-- total. This is a stable sort.
module Data.Vector.Algorithms.Merge
( sort
, sortBy
, Comparison
) where
import Prelude hiding (read, length)
import Control.Monad.Primitive
import Data.Bits
import Data.Vector.Generic.Mutable
import Data.Vector.Algorithms.Common (Comparison, copyOffset, shiftRI)
import qualified Data.Vector.Algorithms.Optimal as O
import qualified Data.Vector.Algorithms.Insertion as I
{- qualif Plus(v:Int, x:Int, y:Int): v = x + y @-}
{-@ qualif_plus :: x:Int -> y:Int -> {v:Int | v = x + y} @-}
qualif_plus :: Int -> Int -> Int
qualif_plus = undefined
-- | Sorts an array using the default comparison.
sort :: (PrimMonad m, MVector v e, Ord e) => v (PrimState m) e -> m ()
sort = sortBy compare
{-# INLINABLE sort #-}
-- | Sorts an array using a custom comparison.
sortBy :: (PrimMonad m, MVector v e) => Comparison e -> v (PrimState m) e -> m ()
sortBy cmp vec
| len <= 1 = return ()
| len == 2 = O.sort2ByOffset cmp vec 0
| len == 3 = O.sort3ByOffset cmp vec 0
| len == 4 = O.sort4ByOffset cmp vec 0
| otherwise = do buf <- new len
mergeSortWithBuf cmp vec buf
where
len = length vec
{-# INLINE sortBy #-}
mergeSortWithBuf :: (PrimMonad m, MVector v e)
=> Comparison e -> v (PrimState m) e -> v (PrimState m) e -> m ()
mergeSortWithBuf cmp src buf = loop (length src) 0 (length src)
where
{- LIQUID WITNESS -}
loop (twit :: Int) l u
| len < threshold = I.sortByBounds cmp src l u
| otherwise = do loop (mid - l) l mid
loop (u - mid) mid u
merge cmp (unsafeSlice l len src) buf (mid - l)
where len = u - l
mid = (u + l) `shiftRI` 1
{-# INLINE mergeSortWithBuf #-}
merge :: (PrimMonad m, MVector v e)
=> Comparison e -> v (PrimState m) e -> v (PrimState m) e
-> Int -> m ()
merge cmp src buf mid = do unsafeCopy low lower
eLow <- unsafeRead low 0
eHigh <- unsafeRead high 0
loopMerge (length low + length high) 0 0 eLow 0 eHigh 0
where
lower = unsafeSlice 0 mid src
high = unsafeSlice mid nHi src -- upper
low = unsafeSlice 0 mid buf -- tmp
nHi = nSrc - mid
nSrc = length src
{-@ decrease wroteHigh 1 2 @-}
{-@ decrease wroteLow 1 2 @-}
{-@ decrease loopMerge 1 2 @-}
{- LIQUID WITNESS -}
wroteHigh d1 (d2::Int) iLow eLow iHigh iIns
| iHigh >= length high = unsafeCopy (unsafeSlice iIns (length low - iLow) src)
(unsafeSlice iLow (length low - iLow) low)
| otherwise = do eHigh <- unsafeRead high iHigh
loopMerge d1 0 iLow eLow iHigh eHigh iIns
{- LIQUID WITNESS -}
wroteLow d1 (d2::Int) iLow iHigh eHigh iIns
| iLow >= length low = return ()
| otherwise = do eLow <- unsafeRead low iLow
loopMerge d1 0 iLow eLow iHigh eHigh iIns
{- LIQUID WITNESS -}
loopMerge (d::Int) (d2::Int) !iLow !eLow !iHigh !eHigh !iIns = case cmp eHigh eLow of
LT -> do unsafeWrite src iIns eHigh
wroteHigh (d-1) 1 iLow eLow (iHigh + 1) (iIns + 1)
_ -> do unsafeWrite src iIns eLow
wroteLow (d-1) 1 (iLow + 1) iHigh eHigh (iIns + 1)
{-# INLINE merge #-}
{-@ threshold :: {v:Int | v = 25} @-}
threshold :: Int
threshold = 25
{-# INLINE threshold #-}