{-
Computer Aided Formal Reasoning (G53CFR, G54CFR)
Peter Morris
Coursework 9: Quick Sort (II)
You job is to redefine quicksort in an obviously terminating way
again the key observation to make is that we should rather build concrete
trees, than complex recursive calls.
Complete all missing definitions, and follow all instructions in comments!!!
-}
module ex09ii where
open import Data.List
open import Data.Nat
open import Data.Product
{-
Order and order are as before:
-}
data Order : Set where le gt : Order
order : ℕ → ℕ → Order
order zero n = le
order (suc m) zero = gt
order (suc m) (suc n) = order m n
{-
As opposed to Merge Sort, the building of the tree is intertwined with
sorting.
We'll need to store the pivot at each level, and put things less or equal than
it in the left, and things greater than it in the right sub tree. Thus QS
trees must have data in the nodes, rather than the leaves:
-}
data Tree (X : Set) : Set where
leaf : Tree X
node : Tree X → X → Tree X → Tree X
{-
The key operation is no 'insert' which puts a natural number its right
place in an already sorted tree:
-}
insert : ℕ → Tree ℕ → Tree ℕ
insert n t = {!!}
{-
We build sorted a sorted list by inserting the elems one at a time:
-}
insertAll : List ℕ → Tree ℕ
insertAll [] = leaf
insertAll (n ∷ ns) = insert n (insertAll ns)
{-
Once we've built a sorted tree, all that now remains is to flatten it back
into a list:
-}
flatten : {X : Set} → Tree X → List X
flatten t = {!!}
{-
We can sort by building the tree and then flattening it
Convince yoursefl that this algorithm is equivalent to QS and make sure your
definition works on some examples:
-}
sort : List ℕ → List ℕ
sort ns = flatten (insertAll ns)
{-
!!! IMPORTANT FINAL EXERCISE: !!!
Show that that sort gives back a list of the same length as the input,
by adapting it to work on Vectors. You will need to index your tree type
by a size as well.
(nb. there is no balancing with these Trees, so you do not need Partity)
Please submit 2 files, one with length, and one without.
-}
ex1 : List ℕ
ex1 = 5 ∷ 2 ∷ 0 ∷ 1 ∷ 4 ∷ 3 ∷ []
ex2 : List ℕ
ex2 = 100 ∷ 1 ∷ 10 ∷ 1 ∷ 100 ∷ 10 ∷ []