gistfile1.agda

open import Data.Bool
open import Data.List
open import Data.Maybe
open import Data.Nat
open import Data.Product

data Tree (A : Set) : Set where
  leaf : Tree A
  branch : Tree A → A → Tree A → Tree A


unfoldTree : ∀ {A : Set} (B : ℕ → Set) → (f : ∀ {n} → B (suc n) → Maybe (B n × A × B n)) → ∀ {n} → B n → Tree A
unfoldTree B f {zero} s = leaf
unfoldTree B f {suc n} s with f s
... | nothing = leaf
... | just (sl , x , sr) = branch (unfoldTree B f sl) x (unfoldTree B f sr)


unfoldTreeList : ∀ {A : Set} (B : ℕ → Set) → ∀ {n} → B n → (f : ∀ {n} → B (suc n) → Maybe (B n × A × B n)) → List A
unfoldTreeList B {zero} s f = []
unfoldTreeList B {suc n} s f with f s
... | nothing = []
... | just (sl , x , sr) = unfoldTreeList B sl f ++ [ x ] ++ unfoldTreeList B sr f

data BList (A : Set) : ℕ → Set where
  [] : ∀ {n} → BList A n
  _∷_ : ∀ {n} → A → BList A n → BList A (suc n)

listToBList : ∀ {A} → (xs : List A) → BList A (length xs)
listToBList [] = []
listToBList (x ∷ xs) = x ∷ listToBList xs

sucBL : ∀ {A n} → BList A n → BList A (suc n)
sucBL [] = []
sucBL (x ∷ xs) = x ∷ sucBL xs

filterBL : ∀ {A n} → (A → Bool) → BList A n → BList A n
filterBL p [] = []
filterBL p (x ∷ xs) with p x
... | true = x ∷ filterBL p xs
... | false = sucBL (filterBL p xs)

quicksort : ∀ {A : Set} → (A → A → Bool) → List A → List A
quicksort {A} _~_ xs = unfoldTreeList (BList A) (listToBList xs) λ
                       { [] → nothing
                       ; (x ∷ xs) → just (filterBL (λ y → y ~ x) xs , x , filterBL (λ y → x ~ y) xs)
                       }