-- Autumn School Proof and Computation -- 3-8 October 2016 -- Fischbachau, Bayern, DE -- -- Andreas Abel, Agda Tutorial -- -- Part 1: How to Keep Your Neighbours in Order (Conor McBride) 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 _≤_ 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 x y = {!!} module _ {A : Set} (R : Rel A) (compare : Total R) where A+ = Ext A R+ = ext R -- Binary search trees data BST (l u : A+) : Set where leaf : R+ l u → BST l u node : (p : A) (lt : BST l (# p)) (rt : BST (# p) u) → BST l u insert : ∀{l u : A+} (p : A) (l≤p : R+ l (# p)) (p≤u : R+ (# p) u) (t : BST l u) → BST l u insert p l≤p p≤u t = {!!} -- Building a BST tree : (xs : List A) → BST ⊥ ⊤ tree nil = leaf _ tree (cons x xs) = insert x _ _ (tree xs) -- Ordered lists data OList (l u : A+) : Set where onil : R+ l u → OList l u ocons : (p : A) (l≤p : R+ l (# p)) (ps : OList (# p) u) → OList l u -- Flattening a BST _++_ : ∀{l m u} (xs : OList l m) (ys : OList m u) → OList l u xs ++ ys = {!!} infixr 1 _++_ flatten : ∀{l u} (t : BST l u) → OList l u flatten t = {!!} -- Sorting is flatten ∘ tree sort : (xs : List A) → OList ⊥ ⊤ sort xs = flatten (tree xs)