module Msort2 where

open import Level renaming (zero to lzero)
open import Data.Bool
open import Data.Nat renaming (ℕ to nat)
open import Data.List renaming (_∷_ to _::_)
open import Relation.Binary using (Rel)
open import Induction.WellFounded as WF
open import Induction.Nat

_<l_ : Rel (List (List nat)) lzero
xs <l ys = length xs <′ length ys

<l-well-founded : Well-founded _<l_
<l-well-founded xs = f xs (<-well-founded(length xs))
    where
      f : forall xs -> Acc _<′_ (length xs) -> Acc _<l_ xs
      f xs (acc rs) = acc (\ys h -> f ys (rs (length ys) h))

open WF.All <l-well-founded public

merge : (nat -> nat -> Bool) -> List nat -> List nat -> List nat
merge _ [] ys = ys
merge _ xs [] = xs
merge _<?_ (x :: xs) (y :: ys) = if x <? y then x :: merge _<?_ xs (y :: ys) else y :: merge _<?_ (x :: xs) ys

msort' : (nat -> nat -> Bool) -> List (List nat) -> List (List nat)
msort' _<?_ [] = []
msort' _<?_ (xs :: []) = xs :: []
msort' _<?_ (xs :: ys :: zss) = merge _<?_ xs ys :: msort' _<?_ zss

msort'_ind : (p : nat -> nat -> Bool) -> (P : List (List nat) -> List (List nat) -> Set) -> P [] [] -> (forall {x : List nat} -> P (x :: []) (x :: [])) ->
    (forall (x y : List nat)(zs : List (List nat)) -> P zs zs -> P (x :: y :: zs) (x :: y :: zs)) -> forall (l : List (List nat)) -> P l l
msort'_ind p P Pnn Poo Pi [] = Pnn
msort'_ind p P Pnn Poo Pi (x :: []) = Poo
msort'_ind p P Pnn Poo Pi (x :: y :: zs) = Pi x y zs (msort'_ind p P Pnn Poo Pi zs)

<-step2 : {n m : nat} -> n ≤′ m -> suc n ≤′ suc m
<-step2 ≤′-refl = ≤′-refl
<-step2 (≤′-step p) = ≤′-step (<-step2 p)

helper : (p : nat -> nat -> Bool)(x y z w : List nat)(zs : List (List nat)) -> msort' p (z :: w :: zs) <l ( z :: w :: zs) ->
    (merge p x y :: (msort' p (z :: w :: zs))) <l ( x :: y :: z :: w :: zs )
helper p x y z w zs Pzs = <-step2 (≤′-step Pzs)

msort'len : (x x' : List nat) (p : nat -> nat -> Bool) -> (xs : List (List nat)) -> msort' p (x :: x' :: xs) <l (x :: x' :: xs)
msort'len x y p zs = msort'_ind p (\l l' -> msort' p ( x :: y :: l' ) <l ( x :: y :: l )) ≤′-refl ≤′-refl (helper p x y) zs

checker : (nat -> nat -> Bool) -> List (List nat) -> List (List nat)
checker p = wfRec (\_ -> List (List nat)) checker'
    where
      checker' : (xs : List (List nat)) -> ((ys : List (List nat)) -> ys <l xs -> List (List nat)) -> List (List nat)
      checker' [] _ = []
      checker' (x :: []) _ = x :: []
      checker' (x :: x' :: xs) f = f (msort' p (x :: x' :: xs)) (msort'len x x' p xs)

msort : (nat -> nat -> Bool) -> List nat -> List nat
msort _<?_ xs = concat (checker _<?_ (map [_] xs))