```------------------------------------------------------------------------
-- A specification of the language χ
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

open import Atom

-- The specification is parametrised by an instance of χ-atoms.

module Chi (atoms : χ-atoms) where

open import Equality.Propositional
open import Prelude hiding (const)

open χ-atoms atoms

-- Abstract syntax.

mutual

data Exp : Set where
apply  : Exp → Exp → Exp
lambda : Var → Exp → Exp
case   : Exp → List Br → Exp
rec    : Var → Exp → Exp
var    : Var → Exp
const  : Const → List Exp → Exp

data Br : Set where
branch : Const → List Var → Exp → Br

-- Substitution.

mutual

infix 6 _[_←_] _[_←_]B _[_←_]⋆ _[_←_]B⋆

_[_←_] : Exp → Var → Exp → Exp
apply e₁ e₂ [ x ← e′ ] = apply (e₁ [ x ← e′ ]) (e₂ [ x ← e′ ])
lambda y e  [ x ← e′ ] = lambda y (if x V.≟ y
then e
else e [ x ← e′ ])
case e bs [ x ← e′ ]   = case (e [ x ← e′ ]) (bs [ x ← e′ ]B⋆)
rec y e   [ x ← e′ ]   = rec y (if x V.≟ y
then e
else e [ x ← e′ ])

var y [ x ← e′ ]       = if x V.≟ y then e′ else var y
const c es  [ x ← e′ ] = const c (es [ x ← e′ ]⋆)

_[_←_]B : Br → Var → Exp → Br
branch c xs e [ x ← e′ ]B with V.member x xs
... | yes _ = branch c xs e
... | no  _ = branch c xs (e [ x ← e′ ])

_[_←_]⋆ : List Exp → Var → Exp → List Exp
[]       [ x ← e′ ]⋆ = []
(e ∷ es) [ x ← e′ ]⋆ = e [ x ← e′ ] ∷ es [ x ← e′ ]⋆

_[_←_]B⋆ : List Br → Var → Exp → List Br
[]       [ x ← e′ ]B⋆ = []
(b ∷ bs) [ x ← e′ ]B⋆ = b [ x ← e′ ]B ∷ bs [ x ← e′ ]B⋆

infix 5 ∷_
infix 4 _[_←_]↦_

data _[_←_]↦_ (e : Exp) : List Var → List Exp → Exp → Set where
[] : e [ [] ← [] ]↦ e
∷_ : ∀ {x xs e′ es′ e″} →
e [ xs ← es′ ]↦ e″ → e [ x ∷ xs ← e′ ∷ es′ ]↦ e″ [ x ← e′ ]

-- Operational semantics.

data Lookup (c : Const) : List Br → List Var → Exp → Set where
here  : ∀ {xs e bs} → Lookup c (branch c xs e ∷ bs) xs e
there : ∀ {c′ xs′ e′ bs xs e} →
c ≢ c′ → Lookup c bs xs e →
Lookup c (branch c′ xs′ e′ ∷ bs) xs e

infixr 5 _∷_
infix 4 _⇓_ _⇓⋆_

mutual

data _⇓_ : Exp → Exp → Set where
apply  : ∀ {e₁ e₂ x e v₂ v} →
e₁ ⇓ lambda x e → e₂ ⇓ v₂ → e [ x ← v₂ ] ⇓ v →
apply e₁ e₂ ⇓ v
case   : ∀ {e bs c es xs e′ e″ v} →
e ⇓ const c es → Lookup c bs xs e′ →
e′ [ xs ← es ]↦ e″ → e″ ⇓ v →
case e bs ⇓ v
rec    : ∀ {x e v} → e [ x ← rec x e ] ⇓ v → rec x e ⇓ v
lambda : ∀ {x e} → lambda x e ⇓ lambda x e
const  : ∀ {c es vs} → es ⇓⋆ vs → const c es ⇓ const c vs

data _⇓⋆_ : List Exp → List Exp → Set where
[]  : [] ⇓⋆ []
_∷_ : ∀ {e es v vs} → e ⇓ v → es ⇓⋆ vs → e ∷ es ⇓⋆ v ∷ vs
```