{- 
  Computer Aided Formal Reasoning (G53CFR, G54CFR)
  Peter Morris

  Lecture 17: Merge Sort (II)

  In Merge.agda, we wrote a naive sorting algorithm that we might write in
  Haskell, but Agda didn't beleive that it was terminating. If we want to 
  verify this algorithm as 'correct' we must first prove it is terminating.

  To do this, we observe that sorting proceeds in 2 phases. In the 1st 
  the input list is repeatedly 'dealt' in to two roughly even length lists until
  the constituent lists are of length 1 (which we know, trivially, to be 
  sorted). We observed this 1st stage amounts to building a balance tree of 
  numbers.
 
  The second stage amounts to repeatedly merging this tree back into a single
  list. We shall now see that by exposing the tree built from the 1st stage, we 
  can  show that our algorithm terminates.

-}

module l17ii where

open import Data.List
open import Data.Nat
open import Data.Product

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

mutual
 merge : List ℕ → List ℕ → List ℕ 
 merge [] ns = ns 
 merge (m ∷ ms) [] = m ∷ ms
 merge (m ∷ ms) (n ∷ ns) with order m n 
 ...                     | le = m ∷ merge ms (n ∷ ns) 
 ...                     | gt = n ∷ merge' m ms ns

 merge' : ℕ → List ℕ → List ℕ → List ℕ
 merge' m ms [] = m ∷ ms
 merge' m ms (n ∷ ns) with order m n
 ...                  | le = m ∷ merge ms (n ∷ ns)
 ...                  | gt = n ∷ merge' m ms ns

{-
  We define another copy of the Booleans, which we will use to store information
  on the balancing of the tree, p0 will denoted a tree with as many elements in 
  the left sub tree as the right. And p1 will denote a tree where there is one
  more bit of payload in the left hand tree as in the right. 

  Trees are then empty, leaves, or nodes with parity information:
-}

data Parity : Set where p0 p1 : Parity

data DealT (X : Set) : Set where
  empT : DealT X
  leafT : X → DealT X
  nodeT : Parity → DealT X → DealT X → DealT X

{- 
  We explain how to insert a new bit of payload into a tree, in the node case
  we decide where to put the new data by looking at the parity bit. if it is p0
  we insert in the left and return a tree with parity p1. If it is p1 we 
  insert on the right and return a p0 (balanced) tree:
-}

insert : {X : Set} → X → DealT X → DealT X
insert x empT = leafT x
insert x (leafT y) = nodeT p0 (leafT y) (leafT x)
insert x (nodeT p0 l r) = nodeT p1 (insert x l) r
insert x (nodeT p1 l r) = nodeT p0 l (insert x r)

{-
  'Dealing' then amounts to repeated inserting into a balanced tree, note
  that this operation differs from the previous deal in that it performs _all_
  the dealing in one go.
-}
 
deal : List ℕ → DealT ℕ
deal [] = empT
deal (n ∷ ns) = insert n (deal ns)

{-
  We now explain how to turn a tree into a sorted list by recursively merging
  the sub trees:
-}

mergeT : DealT ℕ → List ℕ
mergeT empT = []
mergeT (leafT n) = [ n ]
mergeT (nodeT p l r) = merge (mergeT l) (mergeT r)

{- 
  Our sorting algorithm then proceeds by first building and then recursively 
  merging a tree.

  Hopefully you can observe that this is equivalent to the naive implementation
  but now Agda can see that it terminates:
-}

sort : List ℕ → List ℕ
sort ns = mergeT (deal ns)

ex1 : List ℕ 
ex1 =  ∷  ∷  ∷  ∷  ∷  ∷ []

ex2 : List ℕ 
ex2 =  ∷  ∷  ∷  ∷  ∷  ∷ []