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

module CBPV.Effects.Terms where

variable n n′ : ℕ
variable m : Fin n

mutual
  data Val (n : ℕ) : Set where
    ♯_ : Fin n → Val n
    unit : Val n
    ⟪_⟫ : Comp n → Val n
    ⟨_,_⟩ : Val n → Val n → Val n
    inl : Val n → Val n
    inr : Val n → Val n

  data Comp (n : ℕ) : Set where
    ƛ_ : Comp (suc n) → Comp n
    _·_ : Comp n → Val n → Comp n
    _»_ : Val n → Comp n → Comp n
    _! : Val n → Comp n
    ⟨_,_⟩ : Comp n → Comp n → Comp n
    projl : Comp n → Comp n
    projr : Comp n → Comp n
    return_ : Val n → Comp n
    $⟵_⋯_ : Comp n → Comp (suc n) → Comp n
    $≔_⋯_ : Val n → Comp (suc (suc n)) → Comp n
    case_inl⇒_inr⇒_ : Val n → Comp (suc n) → Comp (suc n) → Comp n
    tick : Comp n

variable V V′ V₁ V₂ : Val n
variable M M′ M″ N N′ M₁ M₂ : Comp n

infix  ƛ_
infixl  _»_
infix  _!
infix  return_
infixl  _·_
infix  ♯_
infixr  $⟵_⋯_
infixr  $≔_⋯_
infixl  case_inl⇒_inr⇒_
infix  ⟪_⟫