Skip to content

Instantly share code, notes, and snippets.

@cheery
Created January 23, 2023 18:13
Show Gist options
  • Save cheery/214b2844f0224f7085e38264b03d0916 to your computer and use it in GitHub Desktop.
Save cheery/214b2844f0224f7085e38264b03d0916 to your computer and use it in GitHub Desktop.
Failed normalization by evaluation
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)
--}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment