module MergeSort where

-- Based on:
-- Altenkirch, McBride, McKinna:
-- Why dependent types matter.

open import Data.List
open import Data.Vec
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Relation.Binary.PropositionalEquality

open import Relation.Nullary
open import Relation.Nullary.Decidable as Dec

open import Data.Product

data Parity : Set where
  p₀ : Parity
  p₁ : Parity

parityToℕ : Parity → ℕ
parityToℕ p₀ = 0
parityToℕ p₁ = 1

data DealTree (A : Set) : (n : ℕ) → Set where
  empty : DealTree A 0
  leaf : A → DealTree A 1
  node : ∀{n : ℕ} → (p : Parity)
    → (DealTree A ((parityToℕ p) + n))
    → (DealTree A n)
    → DealTree A ((parityToℕ p) + n + n)

insert : ∀{A} → {n : ℕ} → A → DealTree A n → DealTree A (1 + n)
insert x empty = leaf x
insert x (leaf y) = node p₀ (leaf y) (leaf x) 
insert x (node p₀ l r) = node p₁ (insert x l) r
insert x (node {m} p₁ l r) = subst (DealTree _) (cong suc (+-suc m m)) (node p₀ l (insert x r)) 

deal : {n : ℕ} → Vec ℕ n → DealTree ℕ n
deal [] = empty
deal (x ∷ l) = insert x (deal l)

list₁ : Vec ℕ _
list₁ = 1 ∷ 2 ∷ 3 ∷ []

testDeal₁ : deal list₁ ≡ node p₁ (node p₀ (leaf 3) (leaf 1)) (leaf 2)
testDeal₁ = refl

merge : {n m : ℕ} → Vec ℕ n → Vec ℕ m → Vec ℕ (n + m)
merge [] r = r
merge {n} l [] = subst (Vec ℕ) (sym (+-right-identity n)) l
merge {suc n} (x ∷ xs) (y ∷ ys) with x ≤? y
... | yes p = x ∷ merge xs (y ∷ ys)
... | no ¬p = y ∷ subst (Vec ℕ)  (sym (+-suc n _)) (merge (x ∷ xs) ys)

mergeTree : {n : ℕ} → DealTree ℕ n → Vec ℕ n
mergeTree empty = []
mergeTree (leaf x) = x ∷ []
mergeTree (node p l r) = merge (mergeTree l) (mergeTree r)

mergeSort : {n : ℕ} → Vec ℕ n → Vec ℕ n
mergeSort l = mergeTree (deal l)

testMergeSort₁ : mergeSort (2 ∷ 3 ∷ 1 ∷ []) ≡ list₁
testMergeSort₁ = refl

testMergeSort₂ : mergeSort list₁ ≡ list₁
testMergeSort₂ = refl