module Examples.Giralf.InsertionSort where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Calf.Core.Cost
open import Calf.Value
open import Calf.Computation
open import Calf.Computation.Product
open import Calf.Computation.Tensor
open import Calf.Computation.Credit
open import Calf.Computation.Debit
open import Calf.Computation.CList1
open import Calf.Computation.CList2
open import Calf.Giralf

open import Cubical.Data.Bool
open import Cubical.Data.Nat
import Cubical.Data.Nat.Properties as Nat
open import Cubical.Data.Nat.Order
open import Cubical.Relation.Nullary

_≤ᵇ_ : ℕ → ℕ → Bool
m ≤ᵇ n with ≤Dec m n
... | yes p = true
... | no ¬p = false

insert : ∀ p → ℕ → CList₁ ( +ℂ p) ℕ , p ⊢ CList₁ p ℕ
insert p x =
  payᴳ (+ℂ-identityʳ p) $
  proj₁ᴳ {B = CList₁ p ℕ} $
  foldr₁ᴳ
    {A = (◁[ p ] CList₁ p ℕ) ×ᶜ CList₁ p ℕ}
    (pairᴳ
      (getᴳ p (+ℂ-identityʳ p) (cons₁ᴳ (+ℂ-identityʳ p) x nil₁ᴳ))
      nil₁ᴳ
    )
    (λ y →
      spendᴳ  refl $
      pairᴳ
        ( getᴳ p refl $
          if x ≤ᵇ y
            then cons₁ᴳ refl x (cons₁ᴳ (+ℂ-identityʳ p) y (proj₂ᴳ (idᴳ refl)))
            else cons₁ᴳ refl y (payᴳ (+ℂ-identityʳ p) (proj₁ᴳ {B = CList₁ p ℕ} (idᴳ refl)))
        )
        (cons₁ᴳ (+ℂ-identityʳ p) y (proj₂ᴳ {A = ◁[ p ] CList₁ p ℕ} (idᴳ refl)))
    )
    (idᴳ refl)

isort : CList₂   ℕ , 0ℂ ⊢ CList₁  ℕ
isort =
  foldr₂ᴳ
    (λ r → CList₁ r ℕ)
    (λ r → nil₁ᴳ)
    insert
    (idᴳ refl)