open import Data::List::Core
open import Data::Tree::RedBlack::Base

variable A : Type

open data RBTree (A : Type) : Type
| rbLeaf
| rbNode Color (RBTree A) A (RBTree A)

def rbTreeToList (RBTree A) (List A) : List A
| rbLeaf, r ⇒ r
| rbNode x t1 a t2, r ⇒ rbTreeToList t1 (a :< rbTreeToList t2 r)

def repaint (RBTree A) : RBTree A
| rbNode c l a r ⇒ rbNode black l a r
| rbLeaf ⇒ rbLeaf

def balanceLeft Color (RBTree A) A (RBTree A) : RBTree A
| black, rbNode red (rbNode red a x b) y c, v, r ⇒
    rbNode red (rbNode black a x b) y (rbNode black c v r)
| black, rbNode red a x (rbNode red b y c), v, r ⇒
    rbNode red (rbNode black a x b) y (rbNode black c v r)
| c, a, v, r ⇒ rbNode c a v r

def balanceRight Color (RBTree A) A (RBTree A) : RBTree A
| black, l, v, rbNode red (rbNode red b y c) z d ⇒
    rbNode red (rbNode black l v b) y (rbNode black c z d)
| black, l, v, rbNode red b y (rbNode red c z d) ⇒
    rbNode red (rbNode black l v b) y (rbNode black c z d)
| c, l, v, b ⇒ rbNode c l v b

def insert A (RBTree A) (Decider A) : RBTree A
| a, rbLeaf, _ ⇒ rbNode red rbLeaf a rbLeaf
| a, rbNode c l1 a1 l2, dec< ⇒ match dec< a1 a {
| true ⇒ balanceRight c l1 a1 (insert a l2 dec<)
| false ⇒ balanceLeft c (insert a l1 dec<) a1 l2
}

private def aux (List A) (RBTree A) (Decider A) : RBTree A
| nil, r, _ ⇒ r
| a :< l, r, dec< ⇒ aux l (repaint (insert a r dec<)) dec<

def tree-sort (dec< : Decider A) (l : List A) ⇒ rbTreeToList (aux l rbLeaf dec<) nil