open import Level hiding (zero ; suc)

open import Chapter5.IDesc
open import Chapter5.IDesc.Tagged
open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.InitialAlgebra

module Chapter6.IDesc.FreeMonad.Monad
         {ℓ k : Level}
         {I : Set k}
         (D : tagDesc ℓ I)
       where

open import Function

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

open import Chapter2.Logic

open import Chapter6.IDesc.FreeMonad
open import Chapter6.IDesc.FreeMonad.IMonad

apply : ∀{X Y} → (D : tagDesc ℓ I) → 
        ({i : I} → X i → (D * Y) i) →
        {i : I} → ⟦ toDesc (D *D X) ⟧func (D * Y) i → 
        (D * Y) i
apply (cs , ds) σ (lift zero , xs , lift tt) = σ xs
apply (cs , ds) σ (lift (suc k) , xs) = ⟨ lift (suc k) , xs ⟩

subst : ∀{X Y i} → 
        (D * X) i → ({i : I} → X i → (D * Y) i) → 
        (D * Y) i
subst {X} dx σ = fold (toDesc (D *D X)) (apply D σ) dx 

monad : RawIMonad {I = I} (_*_ D)
monad = record 
  { return = `v {D = D}
  ; _>>=_ = subst 
  }