module Chapter6.Desc.FreeMonad.Examples.List where

open import Level 
  renaming ( zero to zeroL 
           ; suc to sucL )

open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Nat hiding (_*_)
open import Data.Fin hiding (lift)
open import Data.Vec hiding (_>>=_)

open import Relation.Binary.PropositionalEquality

open import Category.Monad

open import Chapter4.Desc
open import Chapter4.Desc.Tagged
open import Chapter4.Desc.Fixpoint
open import Chapter4.Desc.InitialAlgebra

open import Chapter6.Desc.FreeMonad
open import Chapter6.Desc.FreeMonad.Monad


ΣList : Set → tagDesc zeroL
ΣList A =  , 
          (`Σ A λ _ → `var `× `1) ∷ []

List : Set → Set
List A = (ΣList A) * ⊤

nil : ∀{A} → List A
nil = ⟨ lift zero , tt , lift tt ⟩

cons : ∀{A} → A → List A → List A
cons a xs = ⟨ lift (suc zero) , a , xs , lift tt ⟩


append : ∀{A} → List A → List A → List A
append {A} xs ys = xs >>= λ { tt → ys }
  where open RawMonad (monad (ΣList A))

module Test where
  test-nil : ∀{A xs} → append {A} nil xs ≡ xs
  test-nil = refl

  test-cons : ∀{A a xs ys} → append {A} (cons a xs) ys ≡ cons a (append xs ys)
  test-cons = refl