dissection

test.agda

module test where

data ty : Set where
  unit : ty
  _⇒_ : ty → ty → ty

data env : Set where
  ∅ : env
  _▸_ : env → ty → env

data _∈_ (x : ty) : env → Set where
  top : ∀ {Γ} → x ∈ (Γ ▸ x)
  pop : ∀ {Γ y} → x ∈ Γ → x ∈ (Γ ▸ y)

data tm (Γ : env) : ty → Set where
  var : ∀ {a} → a ∈ Γ → tm Γ a
  lam : ∀ {a b} → tm (Γ ▸ a) b → tm Γ (a ⇒ b)
  app : ∀ {a b} → tm Γ (a ⇒ b) → tm Γ a → tm Γ b
  ⋆ : tm Γ unit

data val (Γ : env) : ty → Set where
  var : ∀ {a} → a ∈ Γ → val Γ a
  lam : ∀ {a b} → tm (Γ ▸ a) b → val Γ (a ⇒ b)
  ⋆ : val Γ unit

data ctxₑ (Γ : env) (y : ty) : ty → Set where
  □ : ctxₑ Γ y y
  appₗ : ∀ {a b} → ctxₑ Γ y b → tm Γ a → ctxₑ Γ y (a ⇒ b)
  appᵣ : ∀ {a b} → ctxₑ Γ y b → val Γ (a ⇒ b) → ctxₑ Γ y a

data tmₑ (Γ : env) (x : ty) : Set where
  tval : val Γ x → tmₑ Γ x
  tred : ∀ {a b} → ctxₑ Γ x b → val Γ (a ⇒ b) → val Γ a → tmₑ Γ x

focus : ∀ {Γ x y} → ctxₑ Γ y x → tm Γ x → tmₑ Γ y
focus-val : ∀ {Γ x y} → ctxₑ Γ y x → val Γ x → tmₑ Γ y

focus E (var i)   = focus-val E (var i)
focus E (lam a)   = focus-val E (lam a)
focus E (app a b) = focus (appₗ E b) a
focus E ⋆         = focus-val E ⋆

focus-val □         v = tval v
focus-val (appₗ E a) v = focus (appᵣ E v) a
focus-val (appᵣ E u) v = tred E u v