module TreeSortBool where

open import Prelude

-- Comparing natural numbers

Compare = True ⊎ True

pattern le = inl _
pattern ge = inr _

compare : (x y : ℕ) → Compare
compare        _       = le
compare (suc x)        = ge
compare (suc x) (suc y) = compare x y

-- Binary search trees

data BST (A : Set) : Set where
  leaf : BST A
  node : (p : A) (lt rt : BST A) → BST A

insert : (p : ℕ) (t : BST ℕ) → BST ℕ
insert p leaf = node p leaf leaf
insert p (node q lt rt) with compare p q
... | le = node q (insert p lt) rt
... | ge = node q lt (insert p rt)

-- Building a BST

tree : (xs : List ℕ) → BST ℕ
tree nil         = leaf
tree (cons x xs) = insert x (tree xs)

-- Ordered list constructor names

OList = List

pattern []       = nil
pattern _∷_ x xs = cons x xs

-- Flattening a BST

_++_ : (xs ys : OList ℕ) → OList ℕ
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

infixr  _++_

flatten : (t : BST ℕ) → OList ℕ
flatten leaf           = []
flatten (node p lt rt) = flatten lt ++ p ∷ flatten rt

-- Sorting is flatten ∘ tree

sort : (xs : List ℕ) → OList ℕ
sort xs = flatten (tree xs)