-- Advanced Functional Programming course 2019
-- Chalmers TDA342 / GU DIT260
--
-- 2019-03-04 Guest lecture by Andreas Abel
--
-- Introduction to Agda
--
-- File 2: 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
-- Total R = (x y : _) → R x y ⊎ R y x

pattern le z = inl z
pattern ge z = inr z

compare : Total _≤_
compare zero y = le _
compare (suc x) zero = ge (record {})
compare (suc x) (suc y) = 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 _     ⊤     = True
ext R ⊤     (# x) = False
ext R _     ⊥     = False
ext R (# x) (# y) = R x y
ext R ⊥     y     = True

module _ {A : Set} (R : Rel A) (compare : Total R) where

  -- Binary search trees

  data BST (l u : Ext A) : Set where
    leaf : ext R l u → BST l u
    node : (p : A)
           (lt : BST l (# p))
           (rt : BST (# p) u) → BST l u

  insert : ∀{l u : Ext A} (p : A) (l≤p : ext R l (# p)) (p≤u : ext R (# p) u)
           (t : BST l u) → BST l u
  insert p l≤p p≤u (leaf x) = node p (leaf l≤p) (leaf p≤u)
  insert p l≤p p≤u (node q t t') with compare p q
  insert p l≤p p≤u (node q t t') | le p≤q = node q (insert p l≤p p≤q t) t'
  insert p l≤p p≤u (node q t t') | ge q≤p = node q t (insert p q≤p p≤u t')
  -- If we tried to insert into the wrong subtree, we could not provide
  -- the necessary evidence.  The following line cannot be completed:
  -- insert p l≤p p≤u (node q t t') | ge q≤p = node q (insert p l≤p {!!} t) t'

  -- C-c C-r refine

  -- Building a BST

  tree : (xs : List A) → BST ⊥ ⊤
  tree []       = leaf _
  tree (x ∷ xs) = insert x _ _ (tree xs)

  -- Ordered lists

  data OList (l u : Ext A) : Set where
    onil  : ext R l u → OList l u
    ocons : (p : A)
            (l≤p : ext R l (# p))
            (ps : OList (# p) u) → OList l u

  -- Flattening a BST

  _++_ : ∀{l m u}
         (xs : OList l m)
         (ys : ∀{k} (k≤m : ext R k m) → OList k u) → OList l u
  ocons x l≤x xs ++ ys = ocons x l≤x (xs ++ ys)
  onil l≤m       ++ ys = ys l≤m

  infixr  _++_

  flatten : ∀{l u} (t : BST l u) → OList l u
  flatten (leaf l≤u)     = onil l≤u
  flatten (node p lt rt) = flatten lt ++ λ k≤p → ocons p k≤p (flatten rt)

  -- Sorting is flatten ∘ tree

  sort : (xs : List A) → OList ⊥ ⊤
  sort xs = flatten (tree xs)

-- -}