-- The `insert` function used in insertion sort upgraded to work with vectors, ordered lists, and ordered vectors.

open import Data.Product using (Σ; Σ-syntax; _,_; proj₁; proj₂; _×_) renaming (map to _**_)
open import Relation.Nullary using (¬_; Dec; yes; no)

module Examples.Insertion
  (Val : Set) (_≤_ : Val  Val  Set)
    (≤-refl :  {x}  x  x)
    (≤-trans :  {x y z}  x  y  y  z  x  z)
    (_≤?_ : (x y : Val)  Dec (x  y))
    (≰-invert :  {x y}  ¬ (x  y)  y  x) where

open import Prelude.Function
open import Prelude.Product
open import Prelude.InverseImage
open import Refinement
open import Description
open import Ornament hiding ([]; _∷_)
open import Ornament.ParallelComposition
open import Ornament.RefinementSemantics
open import Ornament.ParallelComposition.Swap
open import Examples.Nat
open import Examples.List
open import Examples.List.Vec
import Examples.List.Ordered as Ordered; open Ordered Val _≤_

open import Function using (_∘_)
open import Data.Empty using (; ⊥-elim)
open import Data.Unit using (; tt)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; _≢_; cong; proof-irrelevance)


--------
-- ordered vectors indexed by lower bound

OrdVecOD : OrnDesc (!  π₁) pull  ListOD Val 
OrdVecOD =  OrdListOD   VecO Val

OrdVec : Val  Nat  Set
OrdVec b n = μ  OrdVecOD  (ok b , ok (ok tt , ok (tt , n)))

ovnil : {b : Val}  OrdVec b zero
ovnil = con tt

ovcons : (x : Val) {b : Val}  b  x  {n : Nat}  OrdVec x n  OrdVec b (suc n)
ovcons x le xs = con (x , le , xs , tt)


--------
-- the insertion example

mutual

  insert : Val  List Val  List Val
  insert y (con (`nil  ,          _)) = y  []
  insert y (con (`cons , x , xs , _)) = insert-with y x xs (y ≤? x)

  -- avoiding with-matching to circumvent a possible error of Agda

  insert-with : (y x : Val)  List Val  Dec (y  x)  List Val
  insert-with y x xs (yes _) = y  x  xs
  insert-with y x xs (no  _) = x  insert y xs

mutual

  insert-length : (y : Val) {n : Nat} (xs : List Val)  length xs  n  length (insert y xs)  suc n
  insert-length y (con (`nil  ,          _)) refl = refl
  insert-length y (con (`cons , x , xs , _)) refl = insert-length-with y x xs refl (y ≤? x)
  
  insert-length-with : (y x : Val) {n : Nat} (xs : List Val)  length (x  xs)  n  (d : Dec (y  x))  length (insert-with y x xs d)  suc n
  insert-length-with y x xs refl (yes _) = refl
  insert-length-with y x xs refl (no  _) = cong suc (insert-length y xs refl)

vinsert : Val  {n : Nat}  Vec Val n  Vec Val (suc n)
vinsert = Upgrade.u upg insert insert-length
  where ref : (n : Nat)  Refinement (List Val) (Vec Val n)
        ref n = FRefinement.comp (toFRefinement (Length-FSwap Val)) (ok (ok tt , ok (tt , n)))
        upg : Upgrade (Val  List Val  List Val) (Val  {n : Nat}  Vec Val n  Vec Val (suc n))
        upg = ∀[ _  Val ] (∀⁺[[ n  Nat ]] (ref n  toUpgrade (ref (suc n))))

mutual

  insert-ordered : (y : Val) {b : Val} (xs : List Val)  Ordered b xs 
                   {b' : Val}  b'  b  b'  y  Ordered b' (insert y xs)
  insert-ordered y {b} (con (`nil  ,          _)) s                   b'≤b b'≤y = ordered-cons y b'≤y ordered-nil
  insert-ordered y {b} (con (`cons , x , xs , _)) (con (b≤x , s , _)) b'≤b b'≤y = insert-ordered-with y x xs b≤x s (y ≤? x) b'≤b b'≤y

  insert-ordered-with : (y : Val) {b : Val} (x : Val) (xs : List Val)  b  x  Ordered x xs  (d : Dec (y  x)) 
                        {b' : Val}  b'  b  b'  y  Ordered b' (insert-with y x xs d)
  insert-ordered-with y {b} x xs b≤x s (yes y≤x) b'≤b b'≤y = ordered-cons y b'≤y (ordered-cons x y≤x s)
  insert-ordered-with y {b} x xs b≤x s (no  y≰x) b'≤b b'≤y = ordered-cons x (≤-trans b'≤b b≤x) (insert-ordered y xs s ≤-refl (≰-invert y≰x))

oinsert : (y : Val) {b : Val}  OrdList b  {b' : Val}  b'  b  b'  y  OrdList b'
oinsert = Upgrade.u upg insert insert-ordered
  where ref : (b : Val)  Refinement (List Val) (OrdList b)
        ref b = FRefinement.comp (RSem'  OrdListOD ) (ok b)
        upg : Upgrade (Val  List Val  List Val) ((y : Val) {b : Val}  OrdList b  {b' : Val}  b'  b  b'  y  OrdList b')
        upg = ∀[ y  Val ] ∀⁺[[ b  Val ]] (ref b  (∀⁺[[ b'  Val ]] ∀⁺[ _  b'  b ] ∀⁺[ _  b'  y ] toUpgrade (ref b')))

ovinsert : (y : Val) {b : Val} {n : Nat}  OrdVec b n  {b' : Val}  b'  b  b'  y  OrdVec b' (suc n)
ovinsert = Upgrade.u upg insert
             λ { y xs (ordered-xs , length-xs) b'≤b b'≤y  insert-ordered y xs ordered-xs b'≤b b'≤y , insert-length y xs length-xs }
  where
    ref : (b : Val) (n : Nat)  Refinement (List Val) (OrdVec b n)
    ref b n = FRefinement.comp (toFRefinement (⊗-FSwap  OrdListOD  (VecO Val) id-FSwap (Length-FSwap Val))) (ok (ok b , ok (ok tt , ok (tt , n))))
    upg : Upgrade (Val  List Val  List Val)
                  ((y : Val) {b : Val} {n : Nat}  OrdVec b n  {b' : Val}  b'  b  b'  y  OrdVec b' (suc n))
    upg = ∀[ y  Val ] ∀⁺[[ b  Val ]] ∀⁺[[ n  Nat ]] (ref b n  (∀⁺[[ b'  Val ]] ∀⁺[ _  b'  b ] ∀⁺[ _  b'  y ] toUpgrade (ref b' (suc n))))