module Examples.Giralf.Reverse where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function
open import Calf.Core.Cost
open import Calf.Value
open import Calf.Computation.CList1
open import Calf.Computation.CList2
open import Calf.Giralf

snoc : ∀ p → X → CList₁ ( +ℂ p) X , p ⊢ CList₁ p X
snoc p x =
  payᴳ (+ℂ-identityʳ _) $
  foldr₁ᴳ
    ( getᴳ p (+ℂ-identityʳ p) $
      cons₁ᴳ (+ℂ-identityʳ p) x $
      nil₁ᴳ
    )
    (λ y →
      spendᴳ  refl $
      getᴳ p refl $
      cons₁ᴳ refl y $
      payᴳ (+ℂ-identityʳ p) $
      idᴳ refl
    )
    (idᴳ refl)

qreverse : CList₂   X , 0ℂ ⊢ CList₁  X
qreverse {X} =
  foldr₂ᴳ
    (λ r → CList₁ r X)
    (λ r → nil₁ᴳ)
    snoc
    (idᴳ refl)