-- 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)