module Chapter6.IDesc.FreeMonad.Examples.IDesc where

open import Level 
  hiding (zero)
  renaming (suc to sucL)

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

open import Chapter2.Logic

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

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

IDescD : (ℓ : Level){k : Level} → tagDesc (k ⊔ (sucL ℓ)) ⊤
IDescD ℓ {k} = ( , (λ _ → 
            `1 ∷ 
            `var tt `× `var tt `× `1 ∷ 
            (`Σ (Lift ℕ) λ { (lift n) → (`Π (Lift (Fin n)) λ _ → `var tt) `× `1 }) ∷
            (`Σ (Lift {sucL ℓ}{k} (Set ℓ)) λ { (lift S) → (`Π (Lift {sucL ℓ}{k} (Lift {ℓ}{sucL ℓ} S)) λ _ → `var tt) `× `1 } ) ∷ 
            (`Σ (Lift {sucL ℓ}{k} (Set ℓ)) λ { (lift S) → (`Π (Lift {sucL ℓ}{k} (Lift {ℓ}{sucL ℓ} S)) λ _ → `var tt) `× `1 }) ∷ [])) ,
           (λ _ → ) , λ _ → []

IDesc' : ∀(ℓ : Level){k} → Set k → Set (k ⊔ (sucL ℓ))
IDesc' ℓ {k} I = (IDescD ℓ {k} * (λ _ → Lift {k}{sucL ℓ} I)) tt

record func' (ℓ : Level){k : Level}(I J : Set k) : Set (k ⊔ sucL ℓ) where
  constructor mk
  field
    out : J → IDesc' ℓ I


`var' : ∀{ℓ k}{I : Set k} → I → IDesc' ℓ I
`var' {ℓ} i = `v {D = IDescD ℓ} (lift i)

`1' : ∀{ℓ k}{I : Set k} → IDesc' ℓ I
`1' = ⟨ lift (suc zero) , lift tt ⟩

_`×'_ : ∀{ℓ k}{I : Set k} (A B : IDesc' ℓ I) → IDesc'  ℓ I
A `×' B = ⟨ lift (suc (suc zero)) , A , B , lift tt ⟩

`σ' : ∀{ℓ k}{I : Set k} (n : ℕ)(T : Fin n → IDesc' ℓ I) → IDesc' ℓ I
`σ' n T = ⟨ lift (suc (suc (suc zero))) , lift n , (λ { (lift k) → T k }) , lift tt ⟩

`Σ' : ∀{ℓ k}{I : Set k} (S : Set ℓ)(T : S → IDesc' ℓ I) → IDesc' ℓ I
`Σ' S T = ⟨ lift (suc (suc (suc (suc zero)))) , lift S , (λ { (lift (lift s)) → T s }) , lift tt ⟩

`Π' : ∀{ℓ k}{I : Set k} (S : Set ℓ)(T : S → IDesc' ℓ I) → IDesc' ℓ I
`Π' S T = ⟨ lift (suc (suc (suc (suc (suc zero))))) , lift S , (λ { (lift (lift s)) → T s }) , lift tt ⟩


_∘_ : ∀{ℓ k}{I J K : Set k} → func' ℓ J K → func' ℓ I J → func' ℓ I K
_∘_ {ℓ} D E = func'.mk (λ k → func'.out D k >>= (λ { (lift j) → func'.out E j }))
  where open RawIMonad (monad (IDescD ℓ))