module TreeSortInstance where

open import Prelude

record ⌜_⌝ (P : Set) : Set where
  constructor !
  field {{prf}} : P

-- Comparing natural numbers

Total : ∀{A} (R : Rel A) → Set
Total R = ∀ x y → ⌜ R (x , y) ⌝ ⊎ ⌜ R (y , x) ⌝

pattern le = inl !
pattern ge = inr !

compare : Total LEℕ
compare        _       = le
compare (suc x)        = ge
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 , # y) = R (x , y)
ext R (⊥   , _  ) = True
ext R _           = False

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

  -- Binary search trees

  data BST (lu : Ext A × Ext A) : Set where
    leaf : {{l≤u : ext R lu}} → BST lu
    node : (p : A)
           (let (l , u) = lu)
           (lt : BST (l , # p))
           (rt : BST (# p , u)) → BST lu

  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 leaf = node p leaf leaf
  insert p (node q lt rt) with compare p q
  ... | le = node q (insert p lt) rt
  ... | ge = node q lt (insert p rt)


  -- Building a BST

  tree : (xs : List A) → BST (⊥ , ⊤)
  tree nil         = leaf
  tree (cons x xs) = insert x (tree xs)

  -- Ordered lists

  data OList (lu : Ext A × Ext A) : Set where
    []  : {{l≤u : ext R lu}} → OList lu
    _∷_ : (p : A)
            (let (l , u) = lu)
            {{l≤p : ext R (l , # p)}}
            (ps : OList (# p , u)) → OList lu

  -- Flattening a BST

  _++_ : ∀{l m u}
         (xs : OList (l , m))
         (ys : ∀{k} {{k≤m : ext R (k , m)}} → OList (k , u)) → OList (l , u)
  (x ∷ xs) ++ ys = x ∷ (xs ++ ys)
  []       ++ ys = ys

  infixr  _++_

  flatten : ∀{lu} (t : BST lu) → OList lu
  flatten leaf     = []
  flatten (node p lt rt) = flatten lt ++ (p ∷ flatten rt)

  -- Sorting is flatten ∘ tree

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