-- Big Proof @ Newton Institute -- 30 June 2017 -- Cambridge, UK -- -- Andreas Abel, Agda Tutorial -- -- Part 1: How to Keep Your Neighbours in Order (Conor McBride) {-# OPTIONS --allow-unsolved-metas #-} module TreeSortOrd where open import Data.Empty using () renaming (⊥ to False) open import Data.Unit using () renaming (⊤ to True) open import Data.Sum using (_⊎_) renaming (inj₁ to inl; inj₂ to inr) open import Data.List.Base using (List; []; _∷_) open import Data.Nat.Base using (ℕ; zero; suc) Rel : Set → Set₁ Rel A = (x y : A) → Set -- Total relations 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 -- Comparing natural numbers module LEℕ where _≤_ : Rel ℕ _≤_ = {!!} compare : Total _≤_ compare = {!!} -- Tree sort module _ {A : Set} (R : Rel A) (compare : Total R) where -- Extension by a least and a greatest element data [A] : Set where ⊤ : [A] # : A → [A] ⊥ : [A] _≤_ : Rel [A] _ ≤ ⊤ = True # x ≤ # y = R x y ⊥ ≤ _ = True _ ≤ _ = False -- Binary search trees (BST) data BST (l u : [A]) : Set where leaf : (l≤u : 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 : l ≤ # p) (p≤u : # p ≤ u) (t : BST l u) → BST l u insert = {!!} -- Building a BST tree : (xs : List A) → BST ⊥ ⊤ tree [] = leaf _ tree (x ∷ xs) = insert x _ _ (tree xs) -- Ordered lists data OList (l u : [A]) : Set where onil : l ≤ u → OList l u ocons : (p : A) (l≤p : l ≤ (# p)) (ps : OList (# p) u) → OList l u -- Flattening a BST _++_ : ∀ {l m u} (xs : OList l m) (ys : ∀{k} (k≤m : k ≤ m) → OList k u) → OList l u _++_ = {!!} infixr 1 _++_ flatten : ∀ {l u} (t : BST l u) → OList l u flatten = {!!} -- Sorting is flatten ∘ tree sort : (xs : List A) → OList ⊥ ⊤ sort xs = flatten (tree xs)