open import Data.Fin using (Fin)
open import Data.Nat using (ℕ; suc)

module CBV.Base.Terms where

variable n : ℕ
variable m : Fin n

mutual
  data Value (n : ℕ) : Set where
    unit : Value n
    ƛ_ : Exp (suc n) → Value n
    #_ : Fin n → Value n
    inl : Value n → Value n
    inr : Value n → Value n
    ⟨_,_⟩ : Value n → Value n → Value n

  data Exp (n : ℕ) : Set where
    val : Value n → Exp n
    _·_ : Exp n → Exp n → Exp n
    _»_ : Exp n → Exp n → Exp n
    inl : Exp n → Exp n
    inr : Exp n → Exp n
    ⟨_,_⟩ : Exp n → Exp n → Exp n
    case_inl⇒_inr⇒_ : Exp n → Exp (suc n) → Exp (suc n) → Exp n
    $≔_⋯_ : Exp n → Exp (suc (suc n)) → Exp n

variable v v₁ v₂ : Value n
variable e e₁ e₂ : Exp n

infix  ƛ_
infixl  _»_
infixl  _·_
infix  #_
infixl  case_inl⇒_inr⇒_
infixr  $≔_⋯_