module TreeSortBool where open import Prelude -- Comparing natural numbers Compare = True ⊎ True pattern le = inl _ pattern ge = inr _ compare : (x y : ℕ) → Compare compare zero y = le compare (suc x) zero = 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 l r) with compare p q insert p (node q l r) | le = node q (insert p l) r insert p (node q l r) | ge = node q l (insert p r) -- Building a BST tree : (xs : List ℕ) → BST ℕ tree nil = leaf tree (cons x xs) = insert x (tree xs) -- Ordered list constructor names data OList (A : Set) : Set where onil : OList A ocons : (x : A) (xs : OList A) → OList A -- Flattening a BST _++_ : (xs ys : OList ℕ) → OList ℕ onil ++ ys = ys (ocons x xs) ++ ys = ocons x (xs ++ ys) infixr 1 _++_ flatten : (t : BST ℕ) → OList ℕ flatten leaf = onil flatten (node p l r) = flatten l ++ ocons p (flatten r) -- Sorting is flatten ∘ tree sort : (xs : List ℕ) → OList ℕ sort xs = flatten (tree xs) infixr 4 _∷_ _∷_ : {A : Set} (x : A) (xs : List A) → List A _∷_ = cons sorted : OList ℕ sorted = sort (2 ∷ 1 ∷ 8 ∷ 0 ∷ 9 ∷ 3 ∷ 1 ∷ 5 ∷ nil)