module TreeSortBool where
open import Prelude
Compare = True ⊎ True
pattern le = inl _
pattern ge = inr _
compare : (x y : ℕ) → Compare
compare 0 _ = le
compare (suc x) 0 = ge
compare (suc x) (suc y) = compare x y
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)
tree : (xs : List ℕ) → BST ℕ
tree nil = leaf
tree (cons x xs) = insert x (tree xs)
OList = List
pattern [] = nil
pattern _∷_ x xs = cons x xs
_++_ : (xs ys : OList ℕ) → OList ℕ
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
infixr 1 _++_
flatten : (t : BST ℕ) → OList ℕ
flatten leaf = []
flatten (node p lt rt) = flatten lt ++ p ∷ flatten rt
sort : (xs : List ℕ) → OList ℕ
sort xs = flatten (tree xs)