{- An implementation of merge sort using braun trees.
This is mostly adapted from the formalisation in the iowa agda library (https://github.com/cedille/ial)
-}

-- These imports depend on the agda standard library (https://github.com/agda/agda-stdlib)
open import Data.List using (List ; [] ; _∷_ ; length)
open import Data.Bool using (Bool ; true ; false ; if_then_else_)
open import Data.Nat
open import Data.Nat.Properties using (+-comm)
open import Data.Sum
open import Relation.Binary.PropositionalEquality

module merge where

  module braun-tree {ℓ} (A : Set ℓ) (_<A_ : A → A → Bool) where

    data braun-tree : (n : ℕ) → Set ℓ where
      bt-leaf : A → braun-tree 1
      bt-node : ∀ {n m : ℕ} →
        braun-tree n → braun-tree m →
        (n ≡ m) ⊎ (n ≡ suc m) →
        braun-tree (n + m)

    bt-insert : ∀ {n : ℕ} → A → braun-tree n → braun-tree (suc n)
    bt-insert a (bt-leaf a') = bt-node (bt-leaf a) (bt-leaf a') (inj₁ refl)
    bt-insert a (bt-node {n} {m} l r (inj₁ n≡m))
      = subst braun-tree (cong suc (+-comm m n))
          (bt-node (bt-insert a r)
                   l
                   (inj₂ (cong suc (sym n≡m))))
    bt-insert a (bt-node {n} {m} l r (inj₂ n≡sm))
      = subst braun-tree (cong suc (+-comm m n))
          (bt-node (bt-insert a r)
                   l
                   (inj₁ (sym n≡sm)))

    bt-from-list : A → (l : List A) → braun-tree (suc (length l))
    bt-from-list a [] = bt-leaf a
    bt-from-list a (a' ∷ as) = bt-insert a (bt-from-list a' as)


    {- Now the tricky part of making the agda termination checker believe
       that `merge` indeed terminates
    -}

    {- Simple pattern matching on `x <A y` fails:

    merge : List A → List A → List A
    merge [] ys = ys
    merge xs [] = xs
    merge (x ∷ xs) (y ∷ ys) with x <A y
    ... | false = x ∷ (merge xs (y ∷ ys))
    ... | true  = y ∷ (merge (x ∷ xs) ys)

    -}

    {- This is how it is implemented in the iowa library.
       It works, but is a rather bizarre solution (imo).

    merge : List A → List A → List A
    merge [] ys = ys
    merge (x ∷ xs) [] = (x ∷ xs)
    merge (x ∷ xs) (y ∷ ys) with (merge xs (y ∷ ys)) | merge (x ∷ xs) ys | x <A y
    ... | _ | r | false = y ∷ r
    ... | l | _ | true  = x ∷ l
    -}

    {- We arrive at this very simple solution. Notice that if_then_else is just a function imported from `Data.Bool`
       Somehow the termination checker is fine with this.
    -}
    merge : List A → List A → List A
    merge [] ys = ys
    merge (x ∷ xs) [] = (x ∷ xs)
    merge (x ∷ xs) (y ∷ ys)
      = if (x <A y) then
          x ∷ merge xs (y ∷ ys)
        else
          y ∷ merge (x ∷ xs) ys

    bt-merge : ∀ {n} → braun-tree n → List A
    bt-merge (bt-leaf a) = a ∷ []
    bt-merge (bt-node l r p) = merge (bt-merge l) (bt-merge r)

    merge-sort : List A → List A
    merge-sort [] = []
    merge-sort (a ∷ as) = bt-merge (bt-from-list a as)

  module test where
    open braun-tree ℕ _<ᵇ_
    t = merge-sort (4 ∷ 5 ∷ 1 ∷ 6 ∷ 2 ∷ [])