Well-scoped NbE in Agda

WellScopedNBE.agda

{-# OPTIONS --guardedness #-}

module WellScopedNBE where

record Partial (A : Set) : Set
data PartialState (A : Set) : Set where
  done : A → PartialState A
  delayed : Partial A → PartialState A
record Partial A where
  coinductive
  field next : PartialState A
open Partial

_>>=_ : {A B : Set} → Partial A → (A → Partial B) → Partial B
_>>=ₛ_ : {A B : Set} → PartialState A → (A → Partial B) → Partial B
(a >>= f) .Partial.next = delayed ((a .Partial.next) >>=ₛ f)
done a >>=ₛ f = f a
delayed a >>=ₛ f = a >>= f

-- pure : {A : Set} → A → Partial A
-- pure a .Partial.next = done a

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

_+_ : ℕ → ℕ → ℕ
zero + n = n
suc m + n = suc (m + n)

data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc : {n : ℕ} → Fin n → Fin (suc n)

maxFin : {n : ℕ} → Fin (suc n)
maxFin {zero} = zero
maxFin {suc n} = suc maxFin

-- I don't want to deal with equality, thus this hack
w1 : {n : ℕ} → (k : ℕ) → Fin (suc (k + n)) → Fin (k + suc n)
w1 zero v = v
w1 (suc k) zero = zero
w1 (suc k) (suc v) = suc (w1 k v)

weakenFin : {n : ℕ} → (k : ℕ) → Fin n → Fin (k + n)
weakenFin zero zero = zero
weakenFin (suc k) zero = zero
weakenFin k (suc v) = w1 k (suc (weakenFin k v))

finDecr : {n : ℕ} → Fin n → Fin n
finDecr zero = zero
finDecr (suc f) = weakenFin 1 f

data Tm (Γ : ℕ) : Set where
  var : Fin Γ → Tm Γ
  app : Tm Γ → Tm Γ → Tm Γ
  lam : Tm (suc Γ) → Tm Γ

data Env (Δ : ℕ) : (Γ : ℕ) → Set
record Closure (Γ : ℕ) : Set
data Neu (Γ : ℕ) : Set

data Val (Γ : ℕ) : Set where
  neu : Neu Γ → Val Γ
  clo : Closure Γ → Val Γ

data Neu Γ where
  var : Fin Γ → Neu Γ
  app : Neu Γ → Val Γ → Neu Γ

data Env Δ where
  [] : Env Δ 0
  _∷ₑ_ : {Γ : ℕ} → Val Δ → Env Δ Γ → Env Δ (suc Γ)

record Closure Δ where
  inductive
  field
    Γ : ℕ
    env : Env Δ Γ
    body : Tm (suc Γ)

lookup : {Γ Δ : ℕ} → Env Δ Γ → Fin Γ → Val Δ
lookup (val ∷ₑ _) zero = val
lookup (_ ∷ₑ env) (suc v) = lookup env v

apply : {Γ : ℕ} → Val Γ → Val Γ → Partial (Val Γ)

{-# TERMINATING #-}
eval : {Γ Δ : ℕ} → Env Δ Γ → Tm Γ → Partial (Val Δ)
eval env (var v) .next = done (lookup env v)
eval env (app f a) = do
  f <- eval env f
  a <- eval env a
  apply f a
eval {Γ} {Δ} env (lam body) .next = done (clo (record {
    Γ = Γ;
    env = env;
    body = body
  }))

apply (neu f) a .next = done (neu (app f a))
apply (clo f) a = eval (a ∷ₑ f .Closure.env) (f .Closure.body)

weakenVal : {Γ : ℕ} → (n : ℕ) → Val Γ → Val (n + Γ)
weakenNeu : {Γ : ℕ} → (n : ℕ) → Neu Γ → Neu (n + Γ)
weakenClo : {Γ : ℕ} → (n : ℕ) → Closure Γ → Closure (n + Γ)
weakenEnv : {Γ Δ : ℕ} → (n : ℕ) → Env Δ Γ → Env (n + Δ) Γ

weakenVal n (neu ne) = neu (weakenNeu n ne)
weakenVal n (clo f) = clo (weakenClo n f)

weakenNeu n (var v) = var (weakenFin n v)
weakenNeu n (app f a) = app (weakenNeu n f) (weakenVal n a)


weakenClo n f .Closure.Γ = f .Closure.Γ
weakenClo n f .Closure.env = weakenEnv n (f .Closure.env)
weakenClo n f .Closure.body = f .Closure.body

weakenEnv n [] = []
weakenEnv n (v ∷ₑ env) = weakenVal n v ∷ₑ weakenEnv n env

{-# TERMINATING #-}
quoteVal : {Γ : ℕ} → Val Γ → Partial (Tm Γ)
quoteNeu : {Γ : ℕ} → Neu Γ → Partial (Tm Γ)
quoteVar : {Γ : ℕ} → Fin Γ → Fin Γ

quoteVal (neu n) = quoteNeu n
quoteVal (clo f) = do
  body <- eval (neu (var maxFin) ∷ₑ weakenEnv 1 (f .Closure.env)) (f .Closure.body)
  body <- quoteVal body
  record { next = done (lam body) }

quoteNeu (var v) .next = done (var (quoteVar v))
quoteNeu (app f a) = do
  f <- quoteNeu f
  a <- quoteVal a
  record { next = done (app f a) }

quoteVar {Γ} zero = maxFin
quoteVar {Γ} (suc v) = finDecr (quoteVar (weakenFin 1 v))