```module TreeSortOrd where

open import Prelude

-- Comparing natural numbers

Total : ∀{A} (R : Rel A) → Set
Total R = ∀ x y → R (x , y) ⊎ R (y , x)

pattern le z = inl z
pattern ge z = inr z

compare : Total LEℕ
compare 0       _       = le _
compare (suc x) 0       = ge _
compare (suc x) (suc y) = compare x y

-- Extension by a least and a greatest element

data Ext (A : Set) : Set where
⊤ : Ext A
# : A → Ext A
⊥ : Ext A

ext : ∀{A} → Rel A → Rel (Ext A)
ext R (_   , ⊤  ) = True
ext R (# x , # y) = R (x , y)
ext R (⊥   , _  ) = True
ext R _           = False

module _ {A : Set} (R : Rel A) (compare : Total R) where

-- Binary search trees

data BST (lu : Ext A × Ext A) : Set where
leaf : ext R lu → BST lu
node : (p : A)
(let (l , u) = lu)
(lt : BST (l , # p))
(rt : BST (# p , u)) → BST lu

insert : ∀{l u : Ext A} (p : A) (l≤p : ext R (l , # p)) (p≤u : ext R (# p , u))
(t : BST (l , u)) → BST (l , u)
insert p l≤p p≤u (leaf l≤u) = node p (leaf l≤p) (leaf p≤u)
insert p l≤p p≤u (node q lt rt) with compare p q
... | le p≤q = node q (insert p l≤p p≤q lt) rt
... | ge q≤p = node q lt (insert p q≤p p≤u rt)

-- Building a BST

tree : (xs : List A) → BST (⊥ , ⊤)
tree nil         = leaf _
tree (cons x xs) = insert x _ _ (tree xs)

-- Ordered lists

data OList (lu : Ext A × Ext A) : Set where
onil  : ext R lu → OList lu
ocons : (p : A)
(let (l , u) = lu)
(l≤p : ext R (l , # p))
(ps : OList (# p , u)) → OList lu

-- Flattening a BST

_++_ : ∀{l m u}
(xs : OList (l , m))
(ys : ∀{k} (k≤m : ext R (k , m)) → OList (k , u)) → OList (l , u)
ocons x l≤x xs ++ ys = ocons x l≤x (xs ++ ys)
onil l≤m       ++ ys = ys l≤m

infixr 1 _++_

flatten : ∀{lu} (t : BST lu) → OList lu
flatten (leaf l≤u)     = onil l≤u
flatten (node p lt rt) = flatten lt ++ λ prf → ocons p prf (flatten rt)

-- Sorting is flatten ∘ tree

sort : (xs : List A) → OList (⊥ , ⊤)
sort xs = flatten (tree xs)
```