{-# OPTIONS --no-positivity-check --no-termination-check #-}
module NaPa.Examples.NBE-short where
open import Level
open import Function
open import Data.Product
open import Data.Maybe
open import Data.Sum
open import Data.Nat using (_+_)
open import NaPa
open import NaPa.Derived
module M (Abs : (World → Set) → World → Set) where
data T α : Set where
V : ∀ (x : Name α) → T α
ƛ : ∀ (abs : Abs T α) → T α
_·_ : ∀ (t u : T α) → T α
module MT = M SynAbs
module MS = M FunAbs
open MS renaming (T to Sem)
open MT renaming (T to Term)
shiftSem : Shift Sem
shiftSem k ⊆w (V a) = V (coe ⊆w (a +nm k))
shiftSem k ⊆w (t · u) = shiftSem k ⊆w t · shiftSem k ⊆w u
shiftSem k ⊆w (ƛ f) = ƛ (shiftFunAbs k ⊆w f)
module NBE (envPack : ShiftableEnvPack _) where
open ShiftableEnvPack envPack
impEnv : ∀ {α β γ} k → α +[ k ] ⊆ β → Env (Sem α) α γ → Env (Sem β) β γ
impEnv k ⊆w = shiftEnv k ⊆w ∘ mapEnv (shiftSem k ⊆w)
app : ∀ {α} → Sem α → Sem α → Sem α
app (ƛ f) v = f 0 ⊆-refl v
app n v = n · v
eval : ∀ {α β} → Env (Sem α) α β → Term β → Sem α
eval Γ (ƛ t) = ƛ (λ k ⊆w v → eval (impEnv k ⊆w Γ ,, v) t)
eval Γ (V x) = [ V , id ]′ (lookupEnv Γ x)
eval Γ (t · u) = eval Γ t ⟨ app ⟩ eval Γ u
reify : ∀ {α} → Sem α → Term α
reify (V a) = MT.V a
reify (n · v) = reify n · reify v where open MT
reify (ƛ f) = MT.ƛ (reify (f 1 ⊆-+1↑1 (V ze)))
nf : ∀ {α β} → Env (Sem α) α β → Term β → Term α
nf Γ = reify ∘ eval Γ
nfC : ∀ {α} → Term α → Term α
nfC = nf emptyEnv
nfø : Term ø → Term ø
nfø = nfC
open NBE shiftableFunEnv