------------------------------------------------------------------------
-- The Agda standard library
--
-- An implementation of merge sort
------------------------------------------------------------------------

-- Unless you are need a particular property of MergeSort, you should
-- import and use the sorting algorithm from `Data.List.Sort` instead
-- of this file.

{-# OPTIONS --cubical-compatible --safe #-}

open import Relation.Binary.Bundles using (DecTotalOrder)

module Data.List.Sort.MergeSort.Base
  {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where

open import Data.List.Base
  using (List; []; _∷_; merge; length; map; [_])

open import Data.Nat.Base using (_<_; _>_; z<s; s<s)
open import Data.Nat.Induction
open import Data.Nat.Properties using (m<n⇒m<1+n)

open DecTotalOrder O renaming (Carrier to A)

------------------------------------------------------------------------
-- Definition

mergePairs : List (List A)  List (List A)
mergePairs (xs  ys  yss) = merge _≤?_ xs ys  mergePairs yss
mergePairs xss             = xss

private
  length-mergePairs :  xs ys yss  let zss = xs  ys  yss in
                      length (mergePairs zss) < length zss
  length-mergePairs _ _ []              = s<s z<s
  length-mergePairs _ _ (xs  [])       = s<s (s<s z<s)
  length-mergePairs _ _ (xs  ys  yss) = s<s (m<n⇒m<1+n (length-mergePairs xs ys yss))

mergeAll : (xss : List (List A))  Acc _<_ (length xss)  List A
mergeAll []        _               = []
mergeAll (xs  []) _               = xs
mergeAll xss@(xs  ys  yss) (acc rec) = mergeAll
  (mergePairs xss) (rec (length-mergePairs xs ys yss))

sort : List A  List A
sort xs = mergeAll (map [_] xs) (<-wellFounded-fast _)