module Chapter6.Desc.FreeMonad.Examples.TermIO 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 Data.String

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


ΣIO : tagDesc zeroL
ΣIO =  , 
      (`Σ String λ _ → (`Π ⊤ λ _ → `var) `× `1) ∷ 
      ((`Π String λ _ → `var) `× `1) ∷ []

TermIO : Set → Set
TermIO X = ΣIO * X

return : ∀{X} → X → TermIO X
return = `v

putString : String → TermIO ⊤
putString s = ⟨ lift (suc zero) , s , return , lift tt ⟩

getString : TermIO String
getString = ⟨ lift (suc (suc zero)) , return , lift tt ⟩

example : TermIO ⊤
example = getString >>= λ s₁ →
          getString >>= λ s₂ →
          putString (s₁ ++ s₂)
  where open RawMonad (monad ΣIO)