module Chapter5.IDesc.Examples.Expr where

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

open import Data.Unit hiding (_≟_)
open import Data.Bool hiding (_≟_)
open import Data.Nat hiding (_≟_)
open import Data.Fin hiding (lift)
open import Data.Vec 
open import Data.Product

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

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

infix 4 _≟_


data Ty : Set where
 `nat `bool : Ty

_≟_ : Decidable {A = Ty} _≡_
`nat  `nat = yes refl
`nat  `bool = no  ())
`bool  `nat = no  ())
`bool  `bool = yes refl


Val : Ty  Set
Val `nat = 
Val `bool = Bool

ExprD : tagDesc zeroL Ty
ExprD = (2 , λ ty  ( (Val ty) λ _  `1)  
                    (`var `bool  `var ty  `var ty  `1)  []) ,
        ((λ { `nat  1 
            ; `bool  1 })) , 
          { `nat  `var `nat  `var `nat  `1  [] 
            ; `bool  `var `nat  `var `nat  `1  [] })

Expr : Ty  Set
Expr = μ (toDesc ExprD)


val : ∀{ty}  Val ty  Expr ty
val v =  lift zero , v , lift tt 

cond : ∀{ty}  Expr `bool  Expr ty  Expr ty  Expr ty
cond b tr fs =  lift (suc zero) , b , tr , fs , lift tt 

plus : Expr `nat  Expr `nat  Expr `nat 
plus x y =  lift (suc (suc zero)) , x , y , lift tt 

le : Expr `nat  Expr `nat  Expr `bool
le x y =  lift (suc (suc zero)) , x , y , lift tt