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

  Lecture 18: Merge Sort (III)

  In the last lecture, we showed that our Merge Sort implementation was 
  terminating. Now we will try to show that sorting preserves the size of the 
  input list. We do this by adapting the implementation to use Vectors, rather 
  than plain Lists. By doing so we can also ensure that the Tree we build
  is balanced, and therefore our algorithm has the right time complexity.

-}

module l18 where

open import Algebra
open import Data.Vec
open import Data.Nat
open import Data.Nat.Properties
private
  module ℕ = CommutativeSemiring commutativeSemiring
open import Data.Product
open import Relation.Binary.PropositionalEquality
import Algebra.RingSolver.AlmostCommutativeRing as ACR
import Algebra.RingSolver.Simple as Solver

open Solver (ACR.fromCommutativeSemiring commutativeSemiring)

zeroLem : (n : ℕ) → n ≡ n + 
zeroLem = solve  (\n → n := n :+ con ) refl 

sucLem₁ : (m n : ℕ) → ( + (m + n)) ≡ (m + ( + n))
sucLem₁ = solve  (\m n → con  :+ (m :+ n) := m :+ (con  :+ n)) refl

sucLem₂ : (m n : ℕ) → (m + ( + n)) ≡ ( + (m + n)) 
sucLem₂ m n = sym (sucLem₁ m n)   

{-

  Ordering things doesn't talk about size, so this code stays the same:

-}

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

{-

  However, merge, does talk about size, here we must ensure that if we merge
  two vectors, then the result as as many elements as both lists added together:

-}

mutual
 merge : {m n : ℕ} → Vec ℕ m → Vec ℕ n  → Vec ℕ (m + n) 
 merge [] ns = ns 
{-
  In the first base case (above), everything works, in the second (below)
  though, we have to fixe up the types since ms has type Vec ℕ lm and the in 
  hole we need something of type Vec ℕ (lm + 0), so we use subst to coerce
  between these types
-}
 merge {suc lm} {zero} (m ∷ ms) [] = m ∷ subst (Vec ℕ) (zeroLem lm) ms 
 merge {suc lm} {suc ln} (m ∷ ms) (n ∷ ns) with order m n 
 ... | le = m ∷ merge ms (n ∷ ns) 
{-
  Again, in the 2nd recursive case, we must appeal to subst to fix up the types 
  when the definition of + does not provide the equality we need
-}
 ... | gt = n ∷ subst (Vec ℕ) (sucLem₁ lm ln) (merge' m ms ns)  

{- 

  merge' incorporates the same tweaks as merge:

-}

 merge' : {m n : ℕ} → ℕ → Vec ℕ m → Vec ℕ n → Vec ℕ ( + (m + n))
 merge' {lm} {zero} m ms [] = m ∷ subst (Vec ℕ) (zeroLem lm) ms 
 merge' {lm} {suc ln} m ms (n ∷ ns) with order m n
 ... | le = m ∷ merge ms (n ∷ ns) 
 ... | gt = n ∷ subst (Vec ℕ) (sucLem₁ lm ln) (merge' m ms ns)  

{- 

  We now must adapt our DealT type to take account of size, first of all we'll
  need to embed our Parity type in the the Natural Numbers:

-}

data Parity : Set where p0 p1 : Parity

pℕ : Parity → ℕ
pℕ p0 = 
pℕ p1 = 

{-

  Now we can index our trees by their size, empT and leafT have obvious sizes:

-}

data DealT (X : Set) : ℕ → Set where
  empT : DealT X 
  leafT : X → DealT X 
{-

  But what about nodeT? We want the two sub trees to have approximately the same
  size. We use the parity bit (and it's embedding in the natural numbers) to
  describe the difference in size between those two trees:

-}
  nodeT : {n : ℕ} (p : Parity) → DealT X (pℕ p + n) → DealT X n 
                               → DealT X (((pℕ p + n) + n))


{- 

  Inserting into a DealT increases its size by 1, note that if we insert into 
  an unbalanced tree (to obtain a balanced one, we must again use subst to fix 
  up the types DealT ℕ (1 + (1 + n) + n) and DealT ℕ (0 + (1 + n) + (1 + n))

-}

insert : {X : Set}{n : ℕ} → X → DealT X n → DealT X ( + n)
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} x (nodeT {n} p1 l r) = subst (\n → DealT X n) (cong suc (sucLem₂ n n)) (nodeT p0 l (insert x r))

{-

  The rest of the code however, does through with out a hitch when we adapt the 
  types to use Vectors:

-}
 
deal : {n : ℕ} → Vec ℕ n → DealT ℕ n
deal [] = empT
deal (n ∷ ns) = insert n (deal ns)

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

sort : {n : ℕ} → Vec ℕ n → Vec ℕ n
sort ns = mergeT (deal ns)

ex1 : Vec ℕ  
ex1 =  ∷  ∷  ∷  ∷  ∷  ∷ []

ex2 : Vec ℕ 
ex2 =  ∷  ∷  ∷  ∷  ∷  ∷ []