module Chapter5.IDesc.Examples.ToIDesc where

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

open import Data.Unit
open import Data.Nat
open import Data.Fin

open import Chapter4.Desc
open import Chapter5.IDesc

toIDesc : (D : Desc zeroL) → IDesc zeroL ⊤
toIDesc `var = `var tt
toIDesc `1 = `1
toIDesc (D `× D') = toIDesc D `× toIDesc D'
toIDesc (D `+ D') = `σ  λ { zero → toIDesc D 
                           ; (suc zero) → toIDesc D' 
                           ; (suc (suc ())) }
toIDesc (`Σ S T) = `Σ S λ s → toIDesc (T s) 
toIDesc (`Π S T) = `Π S λ s → toIDesc (T s)