Failed normalization by evaluation

demo.agda

module demo where

open import Agda.Builtin.Equality
open import Data.List
open import Data.Vec
open import Data.Nat
open import Data.Fin
open import Data.Fin.Base
open import Data.Product
open import Data.Sum
open import Data.Maybe

data Term : Set where
    var : ℕ → Term
    app : Term → Term → Term
    lam : Term → Term
    pi : Term → Term → Term
    u : ℕ → Term

Env : Set
Env = List Term

load : Env → ℕ → Maybe Term
load [] n = nothing
load (x ∷ e) 0F = just x
load (x ∷ e) (suc n) = load e n

hit : ℕ → ℕ → Maybe ℕ
hit 0F 0F = nothing
hit 0F (suc b) = just 0F
hit (suc a) 0F = just a
hit (suc a) (suc b) = hit a b Data.Maybe.>>= λ x → just (suc x)

subst : Term → Term → ℕ → Term
subst (var x) v n with hit x n
subst (var x) v n | just y = var y
subst (var x) v n | nothing = v
subst (app t w) v n = app (subst t v n) (subst w v n)
subst (lam t) v n = lam (subst t v (suc n))
subst (pi t w) v n = pi (subst t v n) (subst w v (suc n))
subst (u x) v n = u x

data Conv : Term → Term → Set where
    id : {t : Term} → Conv t t
    beta : {t x u : Term} → Conv (subst t x 0) u → Conv (app (lam t) x) u

data Typed : Term → Term → Env → Set where
    var : {e : Env} (x : ℕ) {t : Term} → load e x ≡ just t → Typed (var x) t e
    app : {e : Env} {f y a b c : Term}
        → Typed f (pi a b) e
        → Typed y a e
        → Conv (app b y) c
        → Typed (app f y) c e
    lam : {e : Env} {x a b : Term}
        → Typed x b (a ∷ e)
        → Typed (lam x) (pi a b) e
    pi : ∀{n} {e : Env} {x y : Term}
        → Typed x (u n) e
        → Typed y (u n) (x ∷ e)
        → Typed (pi x y) (u n) e
    u : ∀{n} {e : Env} → Typed (u n) (u (suc n)) e
    ↑ : ∀{n} {e : Env} → {x : Term} → Typed x (u n) e → Typed x (u (suc n)) e

simpleLambda : Σ Term (λ x → Σ Term λ t → Typed x t [])
simpleLambda = (lam (var 0) , pi (u 0) (u 0) , lam (var 0 refl))

data Scope (f : Term → Set) : Env → Set where
  [] : Scope f []
  _∷_ : {e : Env} → {x : Term} → f x → Scope f e → Scope f (x ∷ e)
  
Closure : (Term → Set) → Term → Term → Env → Set
Closure f a t e = Σ Term (λ x → Scope f e × Typed x t (a ∷ e))

data TVal : Term → Set where
  var : ℕ → {t : Term} → TVal t
  app : {x f y : Term} → {e : Env} → TVal (pi x f) → (t : Term) → Typed t x e → Conv (app f t) y → TVal y
  lam : {a b : Term} → {e : Env} → Closure TVal a b e → TVal (pi a b)
  pi : ∀{n} → {a : Term} → {e : Env} → TVal (u n) → Closure TVal a (u n) e → TVal (u n)
  u : (n : ℕ) → TVal (u (suc n))
  ↑ : {n : ℕ} → TVal (u n) → TVal (u (suc n))

load' : {e : Env} → {type : Term}
      → (x : ℕ)
      → (env : Scope TVal e)
      → load e x ≡ just type
      → TVal type
load' {x ∷ e} 0F (y ∷ env) refl = y
load' {x₁ ∷ e} (suc x) (x₂ ∷ env) pf = load' {e} x env pf

eval : {e : Env} → (t u : Term) → Typed t u e → Scope TVal e → TVal u
eval .(var x) type (var x pf) scope = load' x scope pf
eval .(app _ _) type (app relx rely conv) scope with eval _ _ relx scope
eval .(app _ _) type (app relx rely conv) scope | var x = app (var x) _ rely conv
eval .(app _ _) type (app relx rely conv) scope | app w ww v x = app (app w ww v x) _ rely conv
eval .(app _ _) type (app relx rely conv) scope | lam (t , scop , relz) = eval t _ {!!} (eval _ _ rely scope ∷ scop)
eval .(lam _) .(pi _ _) (lam rel) scope = lam (_ , scope , rel)
eval .(pi _ _) .(u _) (pi relx rely) scope = pi (eval _ _ relx scope) (_ , scope , rely)
eval .(u _) .(u (suc _)) u scope = u _
eval term .(u (suc _)) (↑ rel) scope = ↑ (eval term _ rel scope)

{--
top : (n : ℕ) → Fin (suc n)
top 0F = zero
top (suc x) = suc (top x)

postulate unreachable : {X : Set} → X

lvl2ix : (n : ℕ) → Fin n → Fin n
lvl2ix (suc n) 0F = top n
lvl2ix (suc n) (suc m) = inject₁ (lvl2ix n m)

mutual
  riseVal : ∀ {n} → Val n → Val (suc n)
  riseVal (var x) = var (inject₁ x)
  riseVal (vapp x y) = vapp (riseVal x) (riseVal y)
  riseVal (vlam x) = vlam (rise x)
  riseVal (vpi val x) = vpi (riseVal val) (rise x)
  riseVal vu = vu

  riseEnv : ∀ {n m} → (Env n m) → Env n (suc m)
  riseEnv [] = []
  riseEnv (x ∷ env) = riseVal x ∷ riseEnv env

  rise : ∀ {n} (c : Closure n) → Closure (suc n)
  rise (n , env , term) = n , riseEnv env , term

{-# TERMINATING #-}
quot : (n : ℕ) → Val n → Term n
quot l (var x) = var (lvl2ix l x)
quot l (vapp v t) = app (quot l v) (quot l t)
quot l (vlam c) = lam (quot (suc l) (capp (rise c) (var (top l))))
quot l (vpi v c) = pi (quot l v) (quot (suc l) (capp (rise c) (var (top l))))
quot l vu = u

nf : ∀{n} → Env n n → Term n → Term n
nf {n} env t = quot n (eval env t)
--}