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  _≟_


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 = ( , λ ty → (`Σ (Val ty) λ _ → `1) ∷ 
                    (`var `bool `× `var ty `× `var ty `× `1) ∷ []) ,
        ((λ { `nat →  
            ; `bool →  })) , 
         (λ { `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 ⟩