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') =  2 λ { 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)