module TreeSortOrd where
open import Prelude
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 zero y = le _
compare (suc x) zero = ge _
compare (suc x) (suc y) = compare x y
data Ext (A : Set) : Set where
⊤ : Ext A
# : A → Ext A
⊥ : Ext A
ext : ∀{A} → Rel A → Rel (Ext A)
ext R x ⊤ = True
ext R ⊤ y = False
ext R (# x) (# y) = R x y
ext R ⊥ y = True
ext R x ⊥ = False
module _ {A : Set} (R : Rel A) (compare : Total R) where
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 l≤u) = node p (leaf l≤p) (leaf p≤u)
insert p l≤p p≤u (node q lt rt) with compare p q
... | le p≤q = node q (insert p l≤p p≤q lt) rt
... | ge q≤p = node q lt (insert p q≤p p≤u rt)
tree : (xs : List A) → BST ⊥ ⊤
tree [] = leaf _
tree (x ∷ xs) = insert x _ _ (tree xs)
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
append : ∀{l m u} (xs : OList l m) (ys : OList m u) → OList l u
append (onil x) ys = onil {!!}
append (ocons p l≤p xs) ys = ocons p l≤p (append xs ys)
_++_ : ∀{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 1 _++_
flatten : ∀{l u} (t : BST l u) → OList l u
flatten (leaf l≤u) = onil l≤u
flatten (node p lt rt) = flatten lt ++ λ prf → ocons p prf (flatten rt)
sort : (xs : List A) → OList ⊥ ⊤
sort xs = flatten (tree xs)