module MergeSort where

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

open import Data.Vec using (Vec; []; _∷_)
open import Data.Nat
open import Data.Nat.Properties.Simple using (+-right-identity; +-suc)
open import Data.Sum using (inj₁; inj₂)
import Level
open import Relation.Binary.PropositionalEquality using (cong; refl; subst; sym; _≡_)
open import Relation.Binary using (DecTotalOrder) 

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